PyRes---1.5.CSA-Sat.s

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

% Computer : n028.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.29s 1.47s
% Output   : Saturation 1.32s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : NLP226+1 : TPTP v8.1.2. Released v2.4.0.
% 0.03/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34  % Computer : n028.cluster.edu
% 0.14/0.34  % Model    : x86_64 x86_64
% 0.14/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34  % Memory   : 8042.1875MB
% 0.14/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34  % CPULimit : 300
% 0.14/0.34  % WCLimit  : 300
% 0.14/0.34  % DateTime : Wed May  8 13:38:07 EDT 2024
% 0.14/0.34  % CPUTime  : 
% 1.29/1.47  % Version:  1.5
% 1.29/1.47  % SZS status CounterSatisfiable
% 1.29/1.47  % SZS output start Saturation
% 1.29/1.47  fof(co1,conjecture,(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:((((((((((((((((((of(U,W,V)&man(U,V))&vincent_forename(U,W))&forename(U,W))&proposition(U,Y))&agent(U,X,V))&theme(U,X,Y))&event(U,X))&present(U,X))&think_believe_consider(U,X))&accessible_world(U,Y))&(![X3]:(man(Y,X3)=>(?[X4]:(((event(Y,X4)&agent(Y,X4,X3))&present(Y,X4))&smoke(Y,X4))))))&of(U,Z,X1))&man(U,X1))&jules_forename(U,Z))&forename(U,Z))&man(U,X1))&state(U,X2))&be(U,X2,X1,X1)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 1.29/1.47  fof(c36,negated_conjecture,(~(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:((((((((((((((((((of(U,W,V)&man(U,V))&vincent_forename(U,W))&forename(U,W))&proposition(U,Y))&agent(U,X,V))&theme(U,X,Y))&event(U,X))&present(U,X))&think_believe_consider(U,X))&accessible_world(U,Y))&(![X3]:(man(Y,X3)=>(?[X4]:(((event(Y,X4)&agent(Y,X4,X3))&present(Y,X4))&smoke(Y,X4))))))&of(U,Z,X1))&man(U,X1))&jules_forename(U,Z))&forename(U,Z))&man(U,X1))&state(U,X2))&be(U,X2,X1,X1))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 1.29/1.47  fof(c37,negated_conjecture,(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:((((((((((((((((((of(U,W,V)&man(U,V))&vincent_forename(U,W))&forename(U,W))&proposition(U,Y))&agent(U,X,V))&theme(U,X,Y))&event(U,X))&present(U,X))&think_believe_consider(U,X))&accessible_world(U,Y))&(![X3]:(~man(Y,X3)|(?[X4]:(((event(Y,X4)&agent(Y,X4,X3))&present(Y,X4))&smoke(Y,X4))))))&of(U,Z,X1))&man(U,X1))&jules_forename(U,Z))&forename(U,Z))&man(U,X1))&state(U,X2))&be(U,X2,X1,X1))))))))))),inference(fof_nnf,[status(thm)],[c36])).
% 1.29/1.47  fof(c38,negated_conjecture,(?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:((((((((((((((((((of(X2,X4,X3)&man(X2,X3))&vincent_forename(X2,X4))&forename(X2,X4))&proposition(X2,X6))&agent(X2,X5,X3))&theme(X2,X5,X6))&event(X2,X5))&present(X2,X5))&think_believe_consider(X2,X5))&accessible_world(X2,X6))&(![X10]:(~man(X6,X10)|(?[X11]:(((event(X6,X11)&agent(X6,X11,X10))&present(X6,X11))&smoke(X6,X11))))))&of(X2,X7,X8))&man(X2,X8))&jules_forename(X2,X7))&forename(X2,X7))&man(X2,X8))&state(X2,X9))&be(X2,X9,X8,X8))))))))))),inference(variable_rename,[status(thm)],[c37])).
% 1.29/1.47  fof(c40,negated_conjecture,(![X10]:(actual_world(skolem0001)&((((((((((((((((((of(skolem0001,skolem0003,skolem0002)&man(skolem0001,skolem0002))&vincent_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&proposition(skolem0001,skolem0005))&agent(skolem0001,skolem0004,skolem0002))&theme(skolem0001,skolem0004,skolem0005))&event(skolem0001,skolem0004))&present(skolem0001,skolem0004))&think_believe_consider(skolem0001,skolem0004))&accessible_world(skolem0001,skolem0005))&(~man(skolem0005,X10)|(((event(skolem0005,skolem0009(X10))&agent(skolem0005,skolem0009(X10),X10))&present(skolem0005,skolem0009(X10)))&smoke(skolem0005,skolem0009(X10)))))&of(skolem0001,skolem0006,skolem0007))&man(skolem0001,skolem0007))&jules_forename(skolem0001,skolem0006))&forename(skolem0001,skolem0006))&man(skolem0001,skolem0007))&state(skolem0001,skolem0008))&be(skolem0001,skolem0008,skolem0007,skolem0007)))),inference(shift_quantors,[status(thm)],[fof(c39,negated_conjecture,(actual_world(skolem0001)&((((((((((((((((((of(skolem0001,skolem0003,skolem0002)&man(skolem0001,skolem0002))&vincent_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&proposition(skolem0001,skolem0005))&agent(skolem0001,skolem0004,skolem0002))&theme(skolem0001,skolem0004,skolem0005))&event(skolem0001,skolem0004))&present(skolem0001,skolem0004))&think_believe_consider(skolem0001,skolem0004))&accessible_world(skolem0001,skolem0005))&(![X10]:(~man(skolem0005,X10)|(((event(skolem0005,skolem0009(X10))&agent(skolem0005,skolem0009(X10),X10))&present(skolem0005,skolem0009(X10)))&smoke(skolem0005,skolem0009(X10))))))&of(skolem0001,skolem0006,skolem0007))&man(skolem0001,skolem0007))&jules_forename(skolem0001,skolem0006))&forename(skolem0001,skolem0006))&man(skolem0001,skolem0007))&state(skolem0001,skolem0008))&be(skolem0001,skolem0008,skolem0007,skolem0007))),inference(skolemize,[status(esa)],[c38])).])).
% 1.29/1.47  fof(c41,negated_conjecture,(![X10]:(actual_world(skolem0001)&((((((((((((((((((of(skolem0001,skolem0003,skolem0002)&man(skolem0001,skolem0002))&vincent_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&proposition(skolem0001,skolem0005))&agent(skolem0001,skolem0004,skolem0002))&theme(skolem0001,skolem0004,skolem0005))&event(skolem0001,skolem0004))&present(skolem0001,skolem0004))&think_believe_consider(skolem0001,skolem0004))&accessible_world(skolem0001,skolem0005))&((((~man(skolem0005,X10)|event(skolem0005,skolem0009(X10)))&(~man(skolem0005,X10)|agent(skolem0005,skolem0009(X10),X10)))&(~man(skolem0005,X10)|present(skolem0005,skolem0009(X10))))&(~man(skolem0005,X10)|smoke(skolem0005,skolem0009(X10)))))&of(skolem0001,skolem0006,skolem0007))&man(skolem0001,skolem0007))&jules_forename(skolem0001,skolem0006))&forename(skolem0001,skolem0006))&man(skolem0001,skolem0007))&state(skolem0001,skolem0008))&be(skolem0001,skolem0008,skolem0007,skolem0007)))),inference(distribute,[status(thm)],[c40])).
% 1.29/1.47  cnf(c55,negated_conjecture,~man(skolem0005,X471)|agent(skolem0005,skolem0009(X471),X471),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  cnf(c53,negated_conjecture,accessible_world(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  cnf(c44,negated_conjecture,man(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  fof(ax59,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&man(V,U))=>man(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax59)).
% 1.29/1.47  fof(c102,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~man(V,U))|man(W,U))))),inference(fof_nnf,[status(thm)],[ax59])).
% 1.29/1.47  fof(c103,plain,(![X55]:(![X56]:(![X57]:((~accessible_world(X56,X57)|~man(X56,X55))|man(X57,X55))))),inference(variable_rename,[status(thm)],[c102])).
% 1.29/1.47  cnf(c104,plain,~accessible_world(X528,X526)|~man(X528,X527)|man(X526,X527),inference(split_conjunct,[status(thm)],[c103])).
% 1.29/1.47  cnf(c569,plain,~accessible_world(skolem0001,X547)|man(X547,skolem0002),inference(resolution,[status(thm)],[c104, c44])).
% 1.29/1.47  cnf(c592,plain,man(skolem0005,skolem0002),inference(resolution,[status(thm)],[c569, c53])).
% 1.29/1.47  cnf(c596,plain,agent(skolem0005,skolem0009(skolem0002),skolem0002),inference(resolution,[status(thm)],[c592, c55])).
% 1.29/1.47  cnf(c49,negated_conjecture,theme(skolem0001,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  fof(ax37,axiom,(![U]:(![V]:(![W]:(![X]:((accessible_world(W,X)&theme(W,U,V))=>theme(X,U,V)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax37)).
% 1.29/1.47  fof(c168,plain,(![U]:(![V]:(![W]:(![X]:((~accessible_world(W,X)|~theme(W,U,V))|theme(X,U,V)))))),inference(fof_nnf,[status(thm)],[ax37])).
% 1.29/1.47  fof(c169,plain,(![X123]:(![X124]:(![X125]:(![X126]:((~accessible_world(X125,X126)|~theme(X125,X123,X124))|theme(X126,X123,X124)))))),inference(variable_rename,[status(thm)],[c168])).
% 1.29/1.47  cnf(c170,plain,~accessible_world(X634,X632)|~theme(X634,X633,X631)|theme(X632,X633,X631),inference(split_conjunct,[status(thm)],[c169])).
% 1.29/1.47  cnf(c771,plain,~accessible_world(skolem0001,X840)|theme(X840,skolem0004,skolem0005),inference(resolution,[status(thm)],[c170, c49])).
% 1.29/1.47  cnf(c961,plain,theme(skolem0005,skolem0004,skolem0005),inference(resolution,[status(thm)],[c771, c53])).
% 1.29/1.47  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/sandbox/benchmark/theBenchmark.p', ax69)).
% 1.29/1.47  fof(c72,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.29/1.47  fof(c73,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)],[c72])).
% 1.29/1.47  cnf(c74,plain,~think_believe_consider(X484,X485)|~proposition(X484,X482)|~theme(X484,X485,X482)|~agent(X484,X485,X486)|~think_believe_consider(X484,X483)|~proposition(X484,X487)|~theme(X484,X483,X487)|~agent(X484,X483,X486)|X482=X487,inference(split_conjunct,[status(thm)],[c73])).
% 1.29/1.47  cnf(c48,negated_conjecture,agent(skolem0001,skolem0004,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  fof(ax39,axiom,(![U]:(![V]:(![W]:(![X]:((accessible_world(W,X)&agent(W,U,V))=>agent(X,U,V)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax39)).
% 1.29/1.47  fof(c162,plain,(![U]:(![V]:(![W]:(![X]:((~accessible_world(W,X)|~agent(W,U,V))|agent(X,U,V)))))),inference(fof_nnf,[status(thm)],[ax39])).
% 1.29/1.47  fof(c163,plain,(![X116]:(![X117]:(![X118]:(![X119]:((~accessible_world(X118,X119)|~agent(X118,X116,X117))|agent(X119,X116,X117)))))),inference(variable_rename,[status(thm)],[c162])).
% 1.29/1.47  cnf(c164,plain,~accessible_world(X618,X621)|~agent(X618,X620,X619)|agent(X621,X620,X619),inference(split_conjunct,[status(thm)],[c163])).
% 1.29/1.47  cnf(c764,plain,~accessible_world(skolem0001,X836)|agent(X836,skolem0004,skolem0002),inference(resolution,[status(thm)],[c164, c48])).
% 1.29/1.47  cnf(c955,plain,agent(skolem0005,skolem0004,skolem0002),inference(resolution,[status(thm)],[c764, c53])).
% 1.29/1.47  cnf(c958,plain,~think_believe_consider(skolem0005,X1295)|~proposition(skolem0005,X1296)|~theme(skolem0005,X1295,X1296)|~agent(skolem0005,X1295,skolem0002)|~think_believe_consider(skolem0005,skolem0004)|~proposition(skolem0005,X1297)|~theme(skolem0005,skolem0004,X1297)|X1296=X1297,inference(resolution,[status(thm)],[c955, c74])).
% 1.29/1.47  cnf(c1264,plain,~think_believe_consider(skolem0005,X1354)|~proposition(skolem0005,X1355)|~theme(skolem0005,X1354,X1355)|~agent(skolem0005,X1354,skolem0002)|~think_believe_consider(skolem0005,skolem0004)|~proposition(skolem0005,skolem0005)|X1355=skolem0005,inference(resolution,[status(thm)],[c958, c961])).
% 1.29/1.47  cnf(c1289,plain,~think_believe_consider(skolem0005,skolem0009(skolem0002))|~proposition(skolem0005,X1356)|~theme(skolem0005,skolem0009(skolem0002),X1356)|~think_believe_consider(skolem0005,skolem0004)|~proposition(skolem0005,skolem0005)|X1356=skolem0005,inference(resolution,[status(thm)],[c1264, c596])).
% 1.29/1.47  cnf(c534,plain,~think_believe_consider(skolem0001,X1064)|~proposition(skolem0001,X1065)|~theme(skolem0001,X1064,X1065)|~agent(skolem0001,X1064,skolem0002)|~think_believe_consider(skolem0001,skolem0004)|~proposition(skolem0001,X1066)|~theme(skolem0001,skolem0004,X1066)|X1065=X1066,inference(resolution,[status(thm)],[c74, c48])).
% 1.29/1.47  cnf(c1112,plain,~think_believe_consider(skolem0001,X1349)|~proposition(skolem0001,X1348)|~theme(skolem0001,X1349,X1348)|~agent(skolem0001,X1349,skolem0002)|~think_believe_consider(skolem0001,skolem0004)|~proposition(skolem0001,skolem0005)|X1348=skolem0005,inference(resolution,[status(thm)],[c534, c49])).
% 1.29/1.47  cnf(c533,plain,~think_believe_consider(X1055,X1057)|~proposition(X1055,X1054)|~theme(X1055,X1057,X1054)|~agent(X1055,X1057,X1053)|~proposition(X1055,X1056)|~theme(X1055,X1057,X1056)|X1054=X1056,inference(factor,[status(thm)],[c74])).
% 1.29/1.47  cnf(c1106,plain,~think_believe_consider(skolem0005,skolem0004)|~proposition(skolem0005,X1343)|~theme(skolem0005,skolem0004,X1343)|~agent(skolem0005,skolem0004,X1344)|~proposition(skolem0005,skolem0005)|X1343=skolem0005,inference(resolution,[status(thm)],[c533, c961])).
% 1.29/1.47  cnf(c1285,plain,~think_believe_consider(skolem0005,skolem0004)|~proposition(skolem0005,X1346)|~theme(skolem0005,skolem0004,X1346)|~proposition(skolem0005,skolem0005)|X1346=skolem0005,inference(resolution,[status(thm)],[c1106, c955])).
% 1.29/1.47  cnf(c1105,plain,~think_believe_consider(skolem0001,skolem0004)|~proposition(skolem0001,X1333)|~theme(skolem0001,skolem0004,X1333)|~agent(skolem0001,skolem0004,X1334)|~proposition(skolem0001,skolem0005)|X1333=skolem0005,inference(resolution,[status(thm)],[c533, c49])).
% 1.29/1.47  cnf(c1281,plain,~think_believe_consider(skolem0001,skolem0004)|~proposition(skolem0001,X1345)|~theme(skolem0001,skolem0004,X1345)|~proposition(skolem0001,skolem0005)|X1345=skolem0005,inference(resolution,[status(thm)],[c1105, c48])).
% 1.29/1.47  cnf(reflexivity,axiom,X201=X201,theory(equality)).
% 1.29/1.47  cnf(c34,axiom,X458!=X463|X456!=X462|X460!=X461|X457!=X459|~be(X458,X456,X460,X457)|be(X463,X462,X461,X459),theory(equality)).
% 1.29/1.47  cnf(c64,negated_conjecture,be(skolem0001,skolem0008,skolem0007,skolem0007),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  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/sandbox/benchmark/theBenchmark.p', ax68)).
% 1.29/1.47  fof(c75,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.29/1.47  fof(c76,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)],[c75])).
% 1.29/1.47  cnf(c77,plain,~accessible_world(X495,X494)|~be(X495,X496,X493,X492)|be(X494,X496,X493,X492),inference(split_conjunct,[status(thm)],[c76])).
% 1.29/1.47  cnf(c535,plain,~accessible_world(skolem0001,X1031)|be(X1031,skolem0008,skolem0007,skolem0007),inference(resolution,[status(thm)],[c77, c64])).
% 1.29/1.47  cnf(c1086,plain,be(skolem0005,skolem0008,skolem0007,skolem0007),inference(resolution,[status(thm)],[c535, c53])).
% 1.29/1.47  cnf(c1089,plain,skolem0005!=X1329|skolem0008!=X1326|skolem0007!=X1327|skolem0007!=X1328|be(X1329,X1326,X1327,X1328),inference(resolution,[status(thm)],[c1086, c34])).
% 1.29/1.47  cnf(c1279,plain,skolem0005!=X1340|skolem0008!=X1339|skolem0007!=X1338|be(X1340,X1339,X1338,skolem0007),inference(resolution,[status(thm)],[c1089, reflexivity])).
% 1.29/1.47  cnf(c1278,plain,skolem0005!=X1332|skolem0008!=X1331|skolem0007!=X1330|be(X1332,X1331,X1330,X1330),inference(factor,[status(thm)],[c1089])).
% 1.29/1.47  cnf(c1280,plain,skolem0005!=X1336|skolem0008!=X1335|be(X1336,X1335,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1278, reflexivity])).
% 1.29/1.47  cnf(c1282,plain,skolem0005!=X1337|be(X1337,skolem0008,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1280, reflexivity])).
% 1.29/1.47  cnf(c510,plain,skolem0001!=X1030|skolem0008!=X1027|skolem0007!=X1028|skolem0007!=X1029|be(X1030,X1027,X1028,X1029),inference(resolution,[status(thm)],[c34, c64])).
% 1.29/1.47  cnf(c1085,plain,skolem0001!=X1317|skolem0008!=X1319|skolem0007!=X1318|be(X1317,X1319,X1318,skolem0007),inference(resolution,[status(thm)],[c510, reflexivity])).
% 1.29/1.47  cnf(c1084,plain,skolem0001!=X1311|skolem0008!=X1312|skolem0007!=X1313|be(X1311,X1312,X1313,X1313),inference(factor,[status(thm)],[c510])).
% 1.29/1.47  cnf(c1274,plain,skolem0001!=X1315|skolem0008!=X1314|be(X1315,X1314,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1084, reflexivity])).
% 1.29/1.47  cnf(c1275,plain,skolem0001!=X1316|be(X1316,skolem0008,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1274, reflexivity])).
% 1.29/1.47  cnf(c29,axiom,X416!=X420|X415!=X419|X417!=X418|~theme(X416,X415,X417)|theme(X420,X419,X418),theory(equality)).
% 1.29/1.47  cnf(c963,plain,skolem0005!=X1303|skolem0004!=X1304|skolem0005!=X1302|theme(X1303,X1304,X1302),inference(resolution,[status(thm)],[c961, c29])).
% 1.29/1.47  cnf(c1269,plain,skolem0005!=X1309|skolem0004!=X1308|theme(X1309,X1308,skolem0005),inference(resolution,[status(thm)],[c963, reflexivity])).
% 1.29/1.47  cnf(c1272,plain,skolem0005!=X1310|theme(X1310,skolem0004,skolem0005),inference(resolution,[status(thm)],[c1269, reflexivity])).
% 1.29/1.47  cnf(c1268,plain,skolem0005!=X1306|skolem0004!=X1305|theme(X1306,X1305,X1306),inference(factor,[status(thm)],[c963])).
% 1.29/1.47  cnf(c1270,plain,skolem0005!=X1307|theme(X1307,skolem0004,X1307),inference(resolution,[status(thm)],[c1268, reflexivity])).
% 1.29/1.47  cnf(c31,axiom,X434!=X438|X433!=X437|X435!=X436|~agent(X434,X433,X435)|agent(X438,X437,X436),theory(equality)).
% 1.29/1.47  cnf(c59,negated_conjecture,man(skolem0001,skolem0007),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  cnf(c570,plain,~accessible_world(skolem0001,X563)|man(X563,skolem0007),inference(resolution,[status(thm)],[c104, c59])).
% 1.29/1.47  cnf(c663,plain,man(skolem0005,skolem0007),inference(resolution,[status(thm)],[c570, c53])).
% 1.29/1.47  cnf(c667,plain,agent(skolem0005,skolem0009(skolem0007),skolem0007),inference(resolution,[status(thm)],[c663, c55])).
% 1.29/1.47  cnf(c775,plain,skolem0005!=X1221|skolem0009(skolem0007)!=X1220|skolem0007!=X1219|agent(X1221,X1220,X1219),inference(resolution,[status(thm)],[c667, c31])).
% 1.29/1.47  cnf(c1211,plain,skolem0005!=X1299|skolem0007!=X1300|agent(X1299,skolem0009(skolem0007),X1300),inference(resolution,[status(thm)],[c775, reflexivity])).
% 1.29/1.47  cnf(c1266,plain,skolem0005!=X1301|agent(X1301,skolem0009(skolem0007),skolem0007),inference(resolution,[status(thm)],[c1211, reflexivity])).
% 1.29/1.47  cnf(c753,plain,skolem0005!=X1206|skolem0009(skolem0002)!=X1205|skolem0002!=X1204|agent(X1206,X1205,X1204),inference(resolution,[status(thm)],[c596, c31])).
% 1.29/1.47  cnf(c1203,plain,skolem0005!=X1294|skolem0002!=X1293|agent(X1294,skolem0009(skolem0002),X1293),inference(resolution,[status(thm)],[c753, reflexivity])).
% 1.29/1.47  cnf(c1262,plain,skolem0005!=X1298|agent(X1298,skolem0009(skolem0002),skolem0002),inference(resolution,[status(thm)],[c1203, reflexivity])).
% 1.29/1.47  cnf(c957,plain,skolem0005!=X1289|skolem0004!=X1288|skolem0002!=X1287|agent(X1289,X1288,X1287),inference(resolution,[status(thm)],[c955, c31])).
% 1.29/1.47  cnf(c1259,plain,skolem0005!=X1290|skolem0004!=X1291|agent(X1290,X1291,skolem0002),inference(resolution,[status(thm)],[c957, reflexivity])).
% 1.29/1.47  cnf(c1260,plain,skolem0005!=X1292|agent(X1292,skolem0004,skolem0002),inference(resolution,[status(thm)],[c1259, reflexivity])).
% 1.29/1.47  cnf(c33,axiom,X449!=X453|X448!=X452|X450!=X451|~of(X449,X448,X450)|of(X453,X452,X451),theory(equality)).
% 1.29/1.47  cnf(c58,negated_conjecture,of(skolem0001,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  fof(ax42,axiom,(![U]:(![V]:(![W]:(![X]:((accessible_world(W,X)&of(W,U,V))=>of(X,U,V)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax42)).
% 1.29/1.47  fof(c153,plain,(![U]:(![V]:(![W]:(![X]:((~accessible_world(W,X)|~of(W,U,V))|of(X,U,V)))))),inference(fof_nnf,[status(thm)],[ax42])).
% 1.29/1.47  fof(c154,plain,(![X106]:(![X107]:(![X108]:(![X109]:((~accessible_world(X108,X109)|~of(X108,X106,X107))|of(X109,X106,X107)))))),inference(variable_rename,[status(thm)],[c153])).
% 1.29/1.47  cnf(c155,plain,~accessible_world(X599,X600)|~of(X599,X601,X598)|of(X600,X601,X598),inference(split_conjunct,[status(thm)],[c154])).
% 1.29/1.47  cnf(c752,plain,~accessible_world(skolem0001,X825)|of(X825,skolem0006,skolem0007),inference(resolution,[status(thm)],[c155, c58])).
% 1.29/1.47  cnf(c947,plain,of(skolem0005,skolem0006,skolem0007),inference(resolution,[status(thm)],[c752, c53])).
% 1.29/1.47  cnf(c950,plain,skolem0005!=X1282|skolem0006!=X1283|skolem0007!=X1281|of(X1282,X1283,X1281),inference(resolution,[status(thm)],[c947, c33])).
% 1.29/1.47  cnf(c1256,plain,skolem0005!=X1285|skolem0006!=X1284|of(X1285,X1284,skolem0007),inference(resolution,[status(thm)],[c950, reflexivity])).
% 1.29/1.47  cnf(c1257,plain,skolem0005!=X1286|of(X1286,skolem0006,skolem0007),inference(resolution,[status(thm)],[c1256, reflexivity])).
% 1.29/1.47  cnf(c43,negated_conjecture,of(skolem0001,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  cnf(c751,plain,~accessible_world(skolem0001,X824)|of(X824,skolem0003,skolem0002),inference(resolution,[status(thm)],[c155, c43])).
% 1.29/1.47  cnf(c943,plain,of(skolem0005,skolem0003,skolem0002),inference(resolution,[status(thm)],[c751, c53])).
% 1.29/1.47  cnf(c945,plain,skolem0005!=X1268|skolem0003!=X1269|skolem0002!=X1267|of(X1268,X1269,X1267),inference(resolution,[status(thm)],[c943, c33])).
% 1.29/1.47  cnf(c1247,plain,skolem0005!=X1278|skolem0003!=X1279|of(X1278,X1279,skolem0002),inference(resolution,[status(thm)],[c945, reflexivity])).
% 1.29/1.47  cnf(c1254,plain,skolem0005!=X1280|of(X1280,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1247, reflexivity])).
% 1.29/1.47  cnf(c503,plain,skolem0001!=X1021|skolem0006!=X1022|skolem0007!=X1020|of(X1021,X1022,X1020),inference(resolution,[status(thm)],[c33, c58])).
% 1.29/1.47  cnf(c1080,plain,skolem0001!=X1275|skolem0006!=X1276|of(X1275,X1276,skolem0007),inference(resolution,[status(thm)],[c503, reflexivity])).
% 1.29/1.47  cnf(c1252,plain,skolem0001!=X1277|of(X1277,skolem0006,skolem0007),inference(resolution,[status(thm)],[c1080, reflexivity])).
% 1.29/1.47  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/sandbox/benchmark/theBenchmark.p', ax70)).
% 1.29/1.47  fof(c68,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.29/1.47  fof(c70,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(c69,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)],[c68])).])).
% 1.29/1.47  cnf(c71,plain,~entity(X478,X475)|~forename(X478,X477)|~of(X478,X477,X475)|~forename(X478,X476)|X476=X477|~of(X478,X476,X475),inference(split_conjunct,[status(thm)],[c70])).
% 1.29/1.47  cnf(c949,plain,~entity(skolem0005,skolem0007)|~forename(skolem0005,X1274)|~of(skolem0005,X1274,skolem0007)|~forename(skolem0005,skolem0006)|skolem0006=X1274,inference(resolution,[status(thm)],[c947, c71])).
% 1.29/1.47  cnf(c502,plain,skolem0001!=X1013|skolem0003!=X1014|skolem0002!=X1012|of(X1013,X1014,X1012),inference(resolution,[status(thm)],[c33, c43])).
% 1.29/1.47  cnf(c1076,plain,skolem0001!=X1272|skolem0003!=X1271|of(X1272,X1271,skolem0002),inference(resolution,[status(thm)],[c502, reflexivity])).
% 1.29/1.47  cnf(c1249,plain,skolem0001!=X1273|of(X1273,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1076, reflexivity])).
% 1.29/1.47  cnf(c489,plain,skolem0001!=X999|skolem0004!=X998|skolem0002!=X997|agent(X999,X998,X997),inference(resolution,[status(thm)],[c31, c48])).
% 1.29/1.47  cnf(c1067,plain,skolem0001!=X1265|skolem0004!=X1266|agent(X1265,X1266,skolem0002),inference(resolution,[status(thm)],[c489, reflexivity])).
% 1.29/1.47  cnf(c1246,plain,skolem0001!=X1270|agent(X1270,skolem0004,skolem0002),inference(resolution,[status(thm)],[c1067, reflexivity])).
% 1.29/1.47  cnf(c468,plain,skolem0001!=X981|skolem0004!=X982|skolem0005!=X980|theme(X981,X982,X980),inference(resolution,[status(thm)],[c29, c49])).
% 1.29/1.47  cnf(c1054,plain,skolem0001!=X1262|skolem0004!=X1263|theme(X1262,X1263,skolem0005),inference(resolution,[status(thm)],[c468, reflexivity])).
% 1.29/1.47  cnf(c1244,plain,skolem0001!=X1264|theme(X1264,skolem0004,skolem0005),inference(resolution,[status(thm)],[c1054, reflexivity])).
% 1.29/1.47  cnf(c1087,plain,~accessible_world(skolem0005,X1261)|be(X1261,skolem0008,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1086, c77])).
% 1.29/1.47  cnf(c944,plain,~entity(skolem0005,skolem0002)|~forename(skolem0005,X1260)|~of(skolem0005,X1260,skolem0002)|~forename(skolem0005,skolem0003)|skolem0003=X1260,inference(resolution,[status(thm)],[c943, c71])).
% 1.29/1.47  cnf(c0,axiom,X210!=X209|X208!=X211|~vincent_forename(X210,X208)|vincent_forename(X209,X211),theory(equality)).
% 1.29/1.47  cnf(c45,negated_conjecture,vincent_forename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  fof(ax35,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&vincent_forename(V,U))=>vincent_forename(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax35)).
% 1.29/1.47  fof(c174,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~vincent_forename(V,U))|vincent_forename(W,U))))),inference(fof_nnf,[status(thm)],[ax35])).
% 1.29/1.47  fof(c175,plain,(![X130]:(![X131]:(![X132]:((~accessible_world(X131,X132)|~vincent_forename(X131,X130))|vincent_forename(X132,X130))))),inference(variable_rename,[status(thm)],[c174])).
% 1.29/1.47  cnf(c176,plain,~accessible_world(X644,X645)|~vincent_forename(X644,X646)|vincent_forename(X645,X646),inference(split_conjunct,[status(thm)],[c175])).
% 1.29/1.47  cnf(c779,plain,~accessible_world(skolem0001,X707)|vincent_forename(X707,skolem0003),inference(resolution,[status(thm)],[c176, c45])).
% 1.29/1.47  cnf(c880,plain,vincent_forename(skolem0005,skolem0003),inference(resolution,[status(thm)],[c779, c53])).
% 1.29/1.47  cnf(c883,plain,skolem0005!=X1256|skolem0003!=X1257|vincent_forename(X1256,X1257),inference(resolution,[status(thm)],[c880, c0])).
% 1.29/1.47  cnf(c1240,plain,skolem0005!=X1259|vincent_forename(X1259,skolem0003),inference(resolution,[status(thm)],[c883, reflexivity])).
% 1.29/1.47  cnf(c2,axiom,X228!=X227|X226!=X229|~proposition(X228,X226)|proposition(X227,X229),theory(equality)).
% 1.29/1.47  cnf(c47,negated_conjecture,proposition(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  fof(ax36,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&proposition(V,U))=>proposition(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax36)).
% 1.29/1.47  fof(c171,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~proposition(V,U))|proposition(W,U))))),inference(fof_nnf,[status(thm)],[ax36])).
% 1.29/1.47  fof(c172,plain,(![X127]:(![X128]:(![X129]:((~accessible_world(X128,X129)|~proposition(X128,X127))|proposition(X129,X127))))),inference(variable_rename,[status(thm)],[c171])).
% 1.29/1.47  cnf(c173,plain,~accessible_world(X639,X640)|~proposition(X639,X638)|proposition(X640,X638),inference(split_conjunct,[status(thm)],[c172])).
% 1.29/1.47  cnf(c774,plain,~accessible_world(skolem0001,X704)|proposition(X704,skolem0005),inference(resolution,[status(thm)],[c173, c47])).
% 1.29/1.47  cnf(c875,plain,proposition(skolem0005,skolem0005),inference(resolution,[status(thm)],[c774, c53])).
% 1.29/1.47  cnf(c876,plain,skolem0005!=X1253|skolem0005!=X1254|proposition(X1253,X1254),inference(resolution,[status(thm)],[c875, c2])).
% 1.29/1.47  cnf(c1238,plain,skolem0005!=X1258|proposition(X1258,skolem0005),inference(resolution,[status(thm)],[c876, reflexivity])).
% 1.29/1.47  cnf(c1237,plain,skolem0005!=X1255|proposition(X1255,X1255),inference(factor,[status(thm)],[c876])).
% 1.29/1.47  cnf(c30,axiom,X429!=X428|X427!=X430|~think_believe_consider(X429,X427)|think_believe_consider(X428,X430),theory(equality)).
% 1.29/1.47  cnf(c52,negated_conjecture,think_believe_consider(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  fof(ax38,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&think_believe_consider(V,U))=>think_believe_consider(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax38)).
% 1.29/1.47  fof(c165,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.29/1.47  fof(c166,plain,(![X120]:(![X121]:(![X122]:((~accessible_world(X121,X122)|~think_believe_consider(X121,X120))|think_believe_consider(X122,X120))))),inference(variable_rename,[status(thm)],[c165])).
% 1.29/1.47  cnf(c167,plain,~accessible_world(X627,X626)|~think_believe_consider(X627,X625)|think_believe_consider(X626,X625),inference(split_conjunct,[status(thm)],[c166])).
% 1.29/1.47  cnf(c768,plain,~accessible_world(skolem0001,X703)|think_believe_consider(X703,skolem0004),inference(resolution,[status(thm)],[c167, c52])).
% 1.29/1.47  cnf(c872,plain,think_believe_consider(skolem0005,skolem0004),inference(resolution,[status(thm)],[c768, c53])).
% 1.29/1.47  cnf(c873,plain,skolem0005!=X1251|skolem0004!=X1250|think_believe_consider(X1251,X1250),inference(resolution,[status(thm)],[c872, c30])).
% 1.29/1.47  cnf(c1235,plain,skolem0005!=X1252|think_believe_consider(X1252,skolem0004),inference(resolution,[status(thm)],[c873, reflexivity])).
% 1.29/1.47  cnf(c32,axiom,X444!=X443|X442!=X445|~present(X444,X442)|present(X443,X445),theory(equality)).
% 1.29/1.47  cnf(c51,negated_conjecture,present(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  fof(ax40,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&present(V,U))=>present(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax40)).
% 1.29/1.47  fof(c159,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~present(V,U))|present(W,U))))),inference(fof_nnf,[status(thm)],[ax40])).
% 1.29/1.47  fof(c160,plain,(![X113]:(![X114]:(![X115]:((~accessible_world(X114,X115)|~present(X114,X113))|present(X115,X113))))),inference(variable_rename,[status(thm)],[c159])).
% 1.29/1.47  cnf(c161,plain,~accessible_world(X611,X613)|~present(X611,X612)|present(X613,X612),inference(split_conjunct,[status(thm)],[c160])).
% 1.29/1.47  cnf(c760,plain,~accessible_world(skolem0001,X700)|present(X700,skolem0004),inference(resolution,[status(thm)],[c161, c51])).
% 1.29/1.47  cnf(c868,plain,present(skolem0005,skolem0004),inference(resolution,[status(thm)],[c760, c53])).
% 1.29/1.47  cnf(c869,plain,skolem0005!=X1248|skolem0004!=X1247|present(X1248,X1247),inference(resolution,[status(thm)],[c868, c32])).
% 1.29/1.47  cnf(c1233,plain,skolem0005!=X1249|present(X1249,skolem0004),inference(resolution,[status(thm)],[c869, reflexivity])).
% 1.29/1.47  cnf(c6,axiom,X258!=X257|X256!=X259|~jules_forename(X258,X256)|jules_forename(X257,X259),theory(equality)).
% 1.29/1.47  cnf(c60,negated_conjecture,jules_forename(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  fof(ax43,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&jules_forename(V,U))=>jules_forename(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax43)).
% 1.29/1.47  fof(c150,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~jules_forename(V,U))|jules_forename(W,U))))),inference(fof_nnf,[status(thm)],[ax43])).
% 1.29/1.47  fof(c151,plain,(![X103]:(![X104]:(![X105]:((~accessible_world(X104,X105)|~jules_forename(X104,X103))|jules_forename(X105,X103))))),inference(variable_rename,[status(thm)],[c150])).
% 1.29/1.47  cnf(c152,plain,~accessible_world(X593,X592)|~jules_forename(X593,X594)|jules_forename(X592,X594),inference(split_conjunct,[status(thm)],[c151])).
% 1.29/1.47  cnf(c748,plain,~accessible_world(skolem0001,X699)|jules_forename(X699,skolem0006),inference(resolution,[status(thm)],[c152, c60])).
% 1.29/1.47  cnf(c864,plain,jules_forename(skolem0005,skolem0006),inference(resolution,[status(thm)],[c748, c53])).
% 1.29/1.47  cnf(c866,plain,skolem0005!=X1245|skolem0006!=X1244|jules_forename(X1245,X1244),inference(resolution,[status(thm)],[c864, c6])).
% 1.29/1.47  cnf(c1231,plain,skolem0005!=X1246|jules_forename(X1246,skolem0006),inference(resolution,[status(thm)],[c866, reflexivity])).
% 1.29/1.47  cnf(c9,axiom,X278!=X277|X276!=X279|~general(X278,X276)|general(X277,X279),theory(equality)).
% 1.29/1.47  fof(ax6,axiom,(![U]:(![V]:(abstraction(U,V)=>general(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax6)).
% 1.29/1.47  fof(c265,plain,(![U]:(![V]:(~abstraction(U,V)|general(U,V)))),inference(fof_nnf,[status(thm)],[ax6])).
% 1.29/1.47  fof(c266,plain,(![X189]:(![X190]:(~abstraction(X189,X190)|general(X189,X190)))),inference(variable_rename,[status(thm)],[c265])).
% 1.29/1.47  cnf(c267,plain,~abstraction(X336,X337)|general(X336,X337),inference(split_conjunct,[status(thm)],[c266])).
% 1.29/1.47  fof(ax9,axiom,(![U]:(![V]:(relation(U,V)=>abstraction(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax9)).
% 1.29/1.47  fof(c256,plain,(![U]:(![V]:(~relation(U,V)|abstraction(U,V)))),inference(fof_nnf,[status(thm)],[ax9])).
% 1.29/1.47  fof(c257,plain,(![X183]:(![X184]:(~relation(X183,X184)|abstraction(X183,X184)))),inference(variable_rename,[status(thm)],[c256])).
% 1.29/1.47  cnf(c258,plain,~relation(X323,X322)|abstraction(X323,X322),inference(split_conjunct,[status(thm)],[c257])).
% 1.29/1.47  fof(ax2,axiom,(![U]:(![V]:(proposition(U,V)=>relation(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax2)).
% 1.29/1.47  fof(c277,plain,(![U]:(![V]:(~proposition(U,V)|relation(U,V)))),inference(fof_nnf,[status(thm)],[ax2])).
% 1.29/1.47  fof(c278,plain,(![X197]:(![X198]:(~proposition(X197,X198)|relation(X197,X198)))),inference(variable_rename,[status(thm)],[c277])).
% 1.29/1.47  cnf(c279,plain,~proposition(X356,X357)|relation(X356,X357),inference(split_conjunct,[status(thm)],[c278])).
% 1.29/1.47  cnf(c392,plain,relation(skolem0001,skolem0005),inference(resolution,[status(thm)],[c279, c47])).
% 1.29/1.47  fof(ax47,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&relation(V,U))=>relation(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax47)).
% 1.29/1.47  fof(c138,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~relation(V,U))|relation(W,U))))),inference(fof_nnf,[status(thm)],[ax47])).
% 1.29/1.47  fof(c139,plain,(![X91]:(![X92]:(![X93]:((~accessible_world(X92,X93)|~relation(X92,X91))|relation(X93,X91))))),inference(variable_rename,[status(thm)],[c138])).
% 1.29/1.47  cnf(c140,plain,~accessible_world(X574,X573)|~relation(X574,X575)|relation(X573,X575),inference(split_conjunct,[status(thm)],[c139])).
% 1.29/1.47  cnf(c711,plain,~accessible_world(skolem0001,X675)|relation(X675,skolem0005),inference(resolution,[status(thm)],[c140, c392])).
% 1.29/1.47  cnf(c832,plain,relation(skolem0005,skolem0005),inference(resolution,[status(thm)],[c711, c53])).
% 1.29/1.47  cnf(c833,plain,abstraction(skolem0005,skolem0005),inference(resolution,[status(thm)],[c832, c258])).
% 1.29/1.47  cnf(c839,plain,general(skolem0005,skolem0005),inference(resolution,[status(thm)],[c833, c267])).
% 1.29/1.47  cnf(c845,plain,skolem0005!=X1239|skolem0005!=X1240|general(X1239,X1240),inference(resolution,[status(thm)],[c839, c9])).
% 1.29/1.47  cnf(c1227,plain,skolem0005!=X1243|general(X1243,skolem0005),inference(resolution,[status(thm)],[c845, reflexivity])).
% 1.29/1.47  cnf(c10,axiom,X284!=X283|X282!=X285|~nonhuman(X284,X282)|nonhuman(X283,X285),theory(equality)).
% 1.29/1.47  fof(ax7,axiom,(![U]:(![V]:(abstraction(U,V)=>nonhuman(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax7)).
% 1.29/1.47  fof(c262,plain,(![U]:(![V]:(~abstraction(U,V)|nonhuman(U,V)))),inference(fof_nnf,[status(thm)],[ax7])).
% 1.29/1.47  fof(c263,plain,(![X187]:(![X188]:(~abstraction(X187,X188)|nonhuman(X187,X188)))),inference(variable_rename,[status(thm)],[c262])).
% 1.29/1.47  cnf(c264,plain,~abstraction(X335,X334)|nonhuman(X335,X334),inference(split_conjunct,[status(thm)],[c263])).
% 1.29/1.47  cnf(c837,plain,nonhuman(skolem0005,skolem0005),inference(resolution,[status(thm)],[c833, c264])).
% 1.29/1.47  cnf(c842,plain,skolem0005!=X1236|skolem0005!=X1235|nonhuman(X1236,X1235),inference(resolution,[status(thm)],[c837, c10])).
% 1.29/1.47  cnf(c1223,plain,skolem0005!=X1242|nonhuman(X1242,skolem0005),inference(resolution,[status(thm)],[c842, reflexivity])).
% 1.29/1.47  cnf(c1226,plain,skolem0005!=X1241|general(X1241,X1241),inference(factor,[status(thm)],[c845])).
% 1.29/1.47  cnf(c7,axiom,X264!=X263|X262!=X265|~abstraction(X264,X262)|abstraction(X263,X265),theory(equality)).
% 1.29/1.47  cnf(c841,plain,skolem0005!=X1232|skolem0005!=X1233|abstraction(X1232,X1233),inference(resolution,[status(thm)],[c833, c7])).
% 1.29/1.47  cnf(c1220,plain,skolem0005!=X1238|abstraction(X1238,skolem0005),inference(resolution,[status(thm)],[c841, reflexivity])).
% 1.29/1.47  cnf(c1222,plain,skolem0005!=X1237|nonhuman(X1237,X1237),inference(factor,[status(thm)],[c842])).
% 1.29/1.47  cnf(c1219,plain,skolem0005!=X1234|abstraction(X1234,X1234),inference(factor,[status(thm)],[c841])).
% 1.29/1.47  cnf(c3,axiom,X236!=X235|X234!=X237|~relation(X236,X234)|relation(X235,X237),theory(equality)).
% 1.29/1.47  cnf(c835,plain,skolem0005!=X1225|skolem0005!=X1226|relation(X1225,X1226),inference(resolution,[status(thm)],[c832, c3])).
% 1.29/1.47  cnf(c1215,plain,skolem0005!=X1231|relation(X1231,skolem0005),inference(resolution,[status(thm)],[c835, reflexivity])).
% 1.29/1.47  cnf(c776,plain,~think_believe_consider(skolem0005,X1228)|~proposition(skolem0005,X1229)|~theme(skolem0005,X1228,X1229)|~agent(skolem0005,X1228,skolem0007)|~think_believe_consider(skolem0005,skolem0009(skolem0007))|~proposition(skolem0005,X1230)|~theme(skolem0005,skolem0009(skolem0007),X1230)|X1229=X1230,inference(resolution,[status(thm)],[c667, c74])).
% 1.29/1.47  cnf(c1214,plain,skolem0005!=X1227|relation(X1227,X1227),inference(factor,[status(thm)],[c835])).
% 1.29/1.47  fof(ax10,axiom,(![U]:(![V]:(relname(U,V)=>relation(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax10)).
% 1.29/1.47  fof(c253,plain,(![U]:(![V]:(~relname(U,V)|relation(U,V)))),inference(fof_nnf,[status(thm)],[ax10])).
% 1.29/1.47  fof(c254,plain,(![X181]:(![X182]:(~relname(X181,X182)|relation(X181,X182)))),inference(variable_rename,[status(thm)],[c253])).
% 1.29/1.47  cnf(c255,plain,~relname(X321,X320)|relation(X321,X320),inference(split_conjunct,[status(thm)],[c254])).
% 1.29/1.47  fof(ax11,axiom,(![U]:(![V]:(forename(U,V)=>relname(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax11)).
% 1.29/1.47  fof(c250,plain,(![U]:(![V]:(~forename(U,V)|relname(U,V)))),inference(fof_nnf,[status(thm)],[ax11])).
% 1.29/1.47  fof(c251,plain,(![X179]:(![X180]:(~forename(X179,X180)|relname(X179,X180)))),inference(variable_rename,[status(thm)],[c250])).
% 1.29/1.47  cnf(c252,plain,~forename(X315,X314)|relname(X315,X314),inference(split_conjunct,[status(thm)],[c251])).
% 1.29/1.47  cnf(c46,negated_conjecture,forename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  fof(ax49,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&forename(V,U))=>forename(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax49)).
% 1.29/1.47  fof(c132,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~forename(V,U))|forename(W,U))))),inference(fof_nnf,[status(thm)],[ax49])).
% 1.29/1.47  fof(c133,plain,(![X85]:(![X86]:(![X87]:((~accessible_world(X86,X87)|~forename(X86,X85))|forename(X87,X85))))),inference(variable_rename,[status(thm)],[c132])).
% 1.29/1.47  cnf(c134,plain,~accessible_world(X567,X568)|~forename(X567,X569)|forename(X568,X569),inference(split_conjunct,[status(thm)],[c133])).
% 1.29/1.47  cnf(c692,plain,~accessible_world(skolem0001,X659)|forename(X659,skolem0003),inference(resolution,[status(thm)],[c134, c46])).
% 1.29/1.47  cnf(c805,plain,forename(skolem0005,skolem0003),inference(resolution,[status(thm)],[c692, c53])).
% 1.29/1.47  cnf(c808,plain,relname(skolem0005,skolem0003),inference(resolution,[status(thm)],[c805, c252])).
% 1.29/1.47  cnf(c809,plain,relation(skolem0005,skolem0003),inference(resolution,[status(thm)],[c808, c255])).
% 1.29/1.47  cnf(c812,plain,abstraction(skolem0005,skolem0003),inference(resolution,[status(thm)],[c809, c258])).
% 1.29/1.47  cnf(c819,plain,general(skolem0005,skolem0003),inference(resolution,[status(thm)],[c812, c267])).
% 1.29/1.47  cnf(c824,plain,skolem0005!=X1222|skolem0003!=X1223|general(X1222,X1223),inference(resolution,[status(thm)],[c819, c9])).
% 1.29/1.47  cnf(c1212,plain,skolem0005!=X1224|general(X1224,skolem0003),inference(resolution,[status(thm)],[c824, reflexivity])).
% 1.29/1.47  cnf(c817,plain,nonhuman(skolem0005,skolem0003),inference(resolution,[status(thm)],[c812, c264])).
% 1.29/1.47  cnf(c822,plain,skolem0005!=X1217|skolem0003!=X1216|nonhuman(X1217,X1216),inference(resolution,[status(thm)],[c817, c10])).
% 1.29/1.47  cnf(c1209,plain,skolem0005!=X1218|nonhuman(X1218,skolem0003),inference(resolution,[status(thm)],[c822, reflexivity])).
% 1.29/1.47  cnf(c821,plain,skolem0005!=X1210|skolem0003!=X1211|abstraction(X1210,X1211),inference(resolution,[status(thm)],[c812, c7])).
% 1.29/1.47  cnf(c1206,plain,skolem0005!=X1215|abstraction(X1215,skolem0003),inference(resolution,[status(thm)],[c821, reflexivity])).
% 1.29/1.47  cnf(c754,plain,~think_believe_consider(skolem0005,X1212)|~proposition(skolem0005,X1213)|~theme(skolem0005,X1212,X1213)|~agent(skolem0005,X1212,skolem0002)|~think_believe_consider(skolem0005,skolem0009(skolem0002))|~proposition(skolem0005,X1214)|~theme(skolem0005,skolem0009(skolem0002),X1214)|X1213=X1214,inference(resolution,[status(thm)],[c596, c74])).
% 1.29/1.47  cnf(c814,plain,skolem0005!=X1207|skolem0003!=X1208|relation(X1207,X1208),inference(resolution,[status(thm)],[c809, c3])).
% 1.29/1.47  cnf(c1204,plain,skolem0005!=X1209|relation(X1209,skolem0003),inference(resolution,[status(thm)],[c814, reflexivity])).
% 1.29/1.47  cnf(c12,axiom,X300!=X299|X298!=X301|~relname(X300,X298)|relname(X299,X301),theory(equality)).
% 1.29/1.47  cnf(c810,plain,skolem0005!=X1201|skolem0003!=X1202|relname(X1201,X1202),inference(resolution,[status(thm)],[c808, c12])).
% 1.29/1.47  cnf(c1201,plain,skolem0005!=X1203|relname(X1203,skolem0003),inference(resolution,[status(thm)],[c810, reflexivity])).
% 1.29/1.47  cnf(c27,axiom,X407!=X406|X405!=X408|~singleton(X407,X405)|singleton(X406,X408),theory(equality)).
% 1.29/1.47  fof(ax28,axiom,(![U]:(![V]:(thing(U,V)=>singleton(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax28)).
% 1.29/1.47  fof(c199,plain,(![U]:(![V]:(~thing(U,V)|singleton(U,V)))),inference(fof_nnf,[status(thm)],[ax28])).
% 1.29/1.47  fof(c200,plain,(![X145]:(![X146]:(~thing(X145,X146)|singleton(X145,X146)))),inference(variable_rename,[status(thm)],[c199])).
% 1.29/1.47  cnf(c201,plain,~thing(X233,X232)|singleton(X233,X232),inference(split_conjunct,[status(thm)],[c200])).
% 1.29/1.47  fof(ax29,axiom,(![U]:(![V]:(eventuality(U,V)=>thing(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax29)).
% 1.29/1.47  fof(c196,plain,(![U]:(![V]:(~eventuality(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax29])).
% 1.29/1.47  fof(c197,plain,(![X143]:(![X144]:(~eventuality(X143,X144)|thing(X143,X144)))),inference(variable_rename,[status(thm)],[c196])).
% 1.29/1.47  cnf(c198,plain,~eventuality(X231,X230)|thing(X231,X230),inference(split_conjunct,[status(thm)],[c197])).
% 1.29/1.47  fof(ax23,axiom,(![U]:(![V]:(event(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax23)).
% 1.29/1.47  fof(c214,plain,(![U]:(![V]:(~event(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax23])).
% 1.29/1.47  fof(c215,plain,(![X155]:(![X156]:(~event(X155,X156)|eventuality(X155,X156)))),inference(variable_rename,[status(thm)],[c214])).
% 1.29/1.47  cnf(c216,plain,~event(X251,X250)|eventuality(X251,X250),inference(split_conjunct,[status(thm)],[c215])).
% 1.29/1.47  cnf(c54,negated_conjecture,~man(skolem0005,X382)|event(skolem0005,skolem0009(X382)),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  cnf(c670,plain,event(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c663, c54])).
% 1.29/1.47  cnf(c716,plain,eventuality(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c670, c216])).
% 1.29/1.47  cnf(c722,plain,thing(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c716, c198])).
% 1.29/1.47  cnf(c734,plain,singleton(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c722, c201])).
% 1.29/1.47  cnf(c736,plain,skolem0005!=X1199|skolem0009(skolem0007)!=X1198|singleton(X1199,X1198),inference(resolution,[status(thm)],[c734, c27])).
% 1.29/1.47  cnf(c1199,plain,skolem0005!=X1200|singleton(X1200,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c736, reflexivity])).
% 1.29/1.47  cnf(c1,axiom,X214!=X213|X212!=X215|~forename(X214,X212)|forename(X213,X215),theory(equality)).
% 1.29/1.47  cnf(c806,plain,skolem0005!=X1196|skolem0003!=X1195|forename(X1196,X1195),inference(resolution,[status(thm)],[c805, c1])).
% 1.29/1.47  cnf(c1197,plain,skolem0005!=X1197|forename(X1197,skolem0003),inference(resolution,[status(thm)],[c806, reflexivity])).
% 1.29/1.47  cnf(c11,axiom,X292!=X291|X290!=X293|~thing(X292,X290)|thing(X291,X293),theory(equality)).
% 1.29/1.47  cnf(c735,plain,skolem0005!=X1193|skolem0009(skolem0007)!=X1192|thing(X1193,X1192),inference(resolution,[status(thm)],[c722, c11])).
% 1.29/1.47  cnf(c1195,plain,skolem0005!=X1194|thing(X1194,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c735, reflexivity])).
% 1.29/1.47  cnf(c61,negated_conjecture,forename(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  cnf(c691,plain,~accessible_world(skolem0001,X654)|forename(X654,skolem0006),inference(resolution,[status(thm)],[c134, c61])).
% 1.29/1.47  cnf(c782,plain,forename(skolem0005,skolem0006),inference(resolution,[status(thm)],[c691, c53])).
% 1.29/1.47  cnf(c785,plain,relname(skolem0005,skolem0006),inference(resolution,[status(thm)],[c782, c252])).
% 1.29/1.47  cnf(c786,plain,relation(skolem0005,skolem0006),inference(resolution,[status(thm)],[c785, c255])).
% 1.29/1.47  cnf(c789,plain,abstraction(skolem0005,skolem0006),inference(resolution,[status(thm)],[c786, c258])).
% 1.29/1.47  cnf(c796,plain,general(skolem0005,skolem0006),inference(resolution,[status(thm)],[c789, c267])).
% 1.29/1.47  cnf(c801,plain,skolem0005!=X1189|skolem0006!=X1190|general(X1189,X1190),inference(resolution,[status(thm)],[c796, c9])).
% 1.29/1.47  cnf(c1193,plain,skolem0005!=X1191|general(X1191,skolem0006),inference(resolution,[status(thm)],[c801, reflexivity])).
% 1.29/1.47  cnf(c23,axiom,X376!=X375|X374!=X377|~specific(X376,X374)|specific(X375,X377),theory(equality)).
% 1.29/1.47  fof(ax27,axiom,(![U]:(![V]:(eventuality(U,V)=>specific(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax27)).
% 1.29/1.47  fof(c202,plain,(![U]:(![V]:(~eventuality(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax27])).
% 1.29/1.47  fof(c203,plain,(![X147]:(![X148]:(~eventuality(X147,X148)|specific(X147,X148)))),inference(variable_rename,[status(thm)],[c202])).
% 1.29/1.47  cnf(c204,plain,~eventuality(X238,X239)|specific(X238,X239),inference(split_conjunct,[status(thm)],[c203])).
% 1.29/1.47  cnf(c720,plain,specific(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c716, c204])).
% 1.29/1.47  cnf(c731,plain,skolem0005!=X1186|skolem0009(skolem0007)!=X1187|specific(X1186,X1187),inference(resolution,[status(thm)],[c720, c23])).
% 1.29/1.47  cnf(c1191,plain,skolem0005!=X1188|specific(X1188,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c731, reflexivity])).
% 1.29/1.47  cnf(c794,plain,nonhuman(skolem0005,skolem0006),inference(resolution,[status(thm)],[c789, c264])).
% 1.29/1.47  cnf(c799,plain,skolem0005!=X1184|skolem0006!=X1183|nonhuman(X1184,X1183),inference(resolution,[status(thm)],[c794, c10])).
% 1.29/1.47  cnf(c1189,plain,skolem0005!=X1185|nonhuman(X1185,skolem0006),inference(resolution,[status(thm)],[c799, reflexivity])).
% 1.29/1.47  cnf(c26,axiom,X399!=X398|X397!=X400|~nonexistent(X399,X397)|nonexistent(X398,X400),theory(equality)).
% 1.29/1.47  fof(ax26,axiom,(![U]:(![V]:(eventuality(U,V)=>nonexistent(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax26)).
% 1.29/1.47  fof(c205,plain,(![U]:(![V]:(~eventuality(U,V)|nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[ax26])).
% 1.29/1.47  fof(c206,plain,(![X149]:(![X150]:(~eventuality(X149,X150)|nonexistent(X149,X150)))),inference(variable_rename,[status(thm)],[c205])).
% 1.29/1.47  cnf(c207,plain,~eventuality(X241,X240)|nonexistent(X241,X240),inference(split_conjunct,[status(thm)],[c206])).
% 1.29/1.47  cnf(c718,plain,nonexistent(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c716, c207])).
% 1.29/1.47  cnf(c725,plain,skolem0005!=X1181|skolem0009(skolem0007)!=X1180|nonexistent(X1181,X1180),inference(resolution,[status(thm)],[c718, c26])).
% 1.29/1.47  cnf(c1187,plain,skolem0005!=X1182|nonexistent(X1182,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c725, reflexivity])).
% 1.29/1.47  cnf(c798,plain,skolem0005!=X1177|skolem0006!=X1178|abstraction(X1177,X1178),inference(resolution,[status(thm)],[c789, c7])).
% 1.29/1.47  cnf(c1185,plain,skolem0005!=X1179|abstraction(X1179,skolem0006),inference(resolution,[status(thm)],[c798, reflexivity])).
% 1.29/1.47  cnf(c8,axiom,X272!=X271|X270!=X273|~unisex(X272,X270)|unisex(X271,X273),theory(equality)).
% 1.29/1.47  fof(ax25,axiom,(![U]:(![V]:(eventuality(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax25)).
% 1.29/1.47  fof(c208,plain,(![U]:(![V]:(~eventuality(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax25])).
% 1.29/1.47  fof(c209,plain,(![X151]:(![X152]:(~eventuality(X151,X152)|unisex(X151,X152)))),inference(variable_rename,[status(thm)],[c208])).
% 1.29/1.47  cnf(c210,plain,~eventuality(X246,X247)|unisex(X246,X247),inference(split_conjunct,[status(thm)],[c209])).
% 1.29/1.47  cnf(c717,plain,unisex(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c716, c210])).
% 1.29/1.47  cnf(c724,plain,skolem0005!=X1174|skolem0009(skolem0007)!=X1175|unisex(X1174,X1175),inference(resolution,[status(thm)],[c717, c8])).
% 1.29/1.47  cnf(c1183,plain,skolem0005!=X1176|unisex(X1176,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c724, reflexivity])).
% 1.29/1.47  cnf(c791,plain,skolem0005!=X1171|skolem0006!=X1172|relation(X1171,X1172),inference(resolution,[status(thm)],[c786, c3])).
% 1.29/1.47  cnf(c1181,plain,skolem0005!=X1173|relation(X1173,skolem0006),inference(resolution,[status(thm)],[c791, reflexivity])).
% 1.29/1.47  cnf(c24,axiom,X386!=X385|X384!=X387|~eventuality(X386,X384)|eventuality(X385,X387),theory(equality)).
% 1.29/1.47  cnf(c719,plain,skolem0005!=X1169|skolem0009(skolem0007)!=X1168|eventuality(X1169,X1168),inference(resolution,[status(thm)],[c716, c24])).
% 1.29/1.47  cnf(c1179,plain,skolem0005!=X1170|eventuality(X1170,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c719, reflexivity])).
% 1.29/1.47  cnf(c787,plain,skolem0005!=X1165|skolem0006!=X1166|relname(X1165,X1166),inference(resolution,[status(thm)],[c785, c12])).
% 1.29/1.47  cnf(c1177,plain,skolem0005!=X1167|relname(X1167,skolem0006),inference(resolution,[status(thm)],[c787, reflexivity])).
% 1.29/1.47  cnf(c5,axiom,X254!=X253|X252!=X255|~event(X254,X252)|event(X253,X255),theory(equality)).
% 1.29/1.47  cnf(c715,plain,skolem0005!=X1162|skolem0009(skolem0007)!=X1163|event(X1162,X1163),inference(resolution,[status(thm)],[c670, c5])).
% 1.29/1.47  cnf(c1175,plain,skolem0005!=X1164|event(X1164,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c715, reflexivity])).
% 1.29/1.47  cnf(c783,plain,skolem0005!=X1160|skolem0006!=X1159|forename(X1160,X1159),inference(resolution,[status(thm)],[c782, c1])).
% 1.29/1.47  cnf(c1173,plain,skolem0005!=X1161|forename(X1161,skolem0006),inference(resolution,[status(thm)],[c783, reflexivity])).
% 1.29/1.47  cnf(c777,plain,~accessible_world(skolem0005,X1158)|agent(X1158,skolem0009(skolem0007),skolem0007),inference(resolution,[status(thm)],[c667, c164])).
% 1.29/1.47  cnf(c56,negated_conjecture,~man(skolem0005,X383)|present(skolem0005,skolem0009(X383)),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  cnf(c666,plain,present(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c663, c56])).
% 1.29/1.47  cnf(c710,plain,skolem0005!=X1156|skolem0009(skolem0007)!=X1155|present(X1156,X1155),inference(resolution,[status(thm)],[c666, c32])).
% 1.29/1.47  cnf(c1171,plain,skolem0005!=X1157|present(X1157,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c710, reflexivity])).
% 1.29/1.47  cnf(c765,plain,~accessible_world(skolem0005,X1154)|agent(X1154,skolem0009(skolem0002),skolem0002),inference(resolution,[status(thm)],[c164, c596])).
% 1.29/1.47  cnf(c4,axiom,X244!=X243|X242!=X245|~smoke(X244,X242)|smoke(X243,X245),theory(equality)).
% 1.29/1.47  cnf(c57,negated_conjecture,~man(skolem0005,X388)|smoke(skolem0005,skolem0009(X388)),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.47  cnf(c665,plain,smoke(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c663, c57])).
% 1.29/1.47  cnf(c709,plain,skolem0005!=X1150|skolem0009(skolem0007)!=X1151|smoke(X1150,X1151),inference(resolution,[status(thm)],[c665, c4])).
% 1.29/1.47  cnf(c1168,plain,skolem0005!=X1153|smoke(X1153,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c709, reflexivity])).
% 1.29/1.47  cnf(c22,axiom,X366!=X365|X364!=X367|~existent(X366,X364)|existent(X365,X367),theory(equality)).
% 1.29/1.47  fof(ax17,axiom,(![U]:(![V]:(entity(U,V)=>existent(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax17)).
% 1.29/1.47  fof(c232,plain,(![U]:(![V]:(~entity(U,V)|existent(U,V)))),inference(fof_nnf,[status(thm)],[ax17])).
% 1.29/1.47  fof(c233,plain,(![X167]:(![X168]:(~entity(X167,X168)|existent(X167,X168)))),inference(variable_rename,[status(thm)],[c232])).
% 1.29/1.47  cnf(c234,plain,~entity(X287,X286)|existent(X287,X286),inference(split_conjunct,[status(thm)],[c233])).
% 1.29/1.47  fof(ax20,axiom,(![U]:(![V]:(organism(U,V)=>entity(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax20)).
% 1.29/1.47  fof(c223,plain,(![U]:(![V]:(~organism(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax20])).
% 1.29/1.47  fof(c224,plain,(![X161]:(![X162]:(~organism(X161,X162)|entity(X161,X162)))),inference(variable_rename,[status(thm)],[c223])).
% 1.29/1.47  cnf(c225,plain,~organism(X268,X269)|entity(X268,X269),inference(split_conjunct,[status(thm)],[c224])).
% 1.29/1.47  fof(ax21,axiom,(![U]:(![V]:(human_person(U,V)=>organism(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax21)).
% 1.29/1.47  fof(c220,plain,(![U]:(![V]:(~human_person(U,V)|organism(U,V)))),inference(fof_nnf,[status(thm)],[ax21])).
% 1.29/1.47  fof(c221,plain,(![X159]:(![X160]:(~human_person(X159,X160)|organism(X159,X160)))),inference(variable_rename,[status(thm)],[c220])).
% 1.29/1.47  cnf(c222,plain,~human_person(X266,X267)|organism(X266,X267),inference(split_conjunct,[status(thm)],[c221])).
% 1.29/1.47  fof(ax22,axiom,(![U]:(![V]:(man(U,V)=>human_person(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax22)).
% 1.29/1.47  fof(c217,plain,(![U]:(![V]:(~man(U,V)|human_person(U,V)))),inference(fof_nnf,[status(thm)],[ax22])).
% 1.29/1.47  fof(c218,plain,(![X157]:(![X158]:(~man(X157,X158)|human_person(X157,X158)))),inference(variable_rename,[status(thm)],[c217])).
% 1.29/1.47  cnf(c219,plain,~man(X260,X261)|human_person(X260,X261),inference(split_conjunct,[status(thm)],[c218])).
% 1.29/1.47  cnf(c671,plain,human_person(skolem0005,skolem0007),inference(resolution,[status(thm)],[c663, c219])).
% 1.29/1.47  cnf(c678,plain,organism(skolem0005,skolem0007),inference(resolution,[status(thm)],[c671, c222])).
% 1.29/1.47  cnf(c686,plain,entity(skolem0005,skolem0007),inference(resolution,[status(thm)],[c678, c225])).
% 1.29/1.47  cnf(c697,plain,existent(skolem0005,skolem0007),inference(resolution,[status(thm)],[c686, c234])).
% 1.29/1.47  cnf(c707,plain,skolem0005!=X1149|skolem0007!=X1148|existent(X1149,X1148),inference(resolution,[status(thm)],[c697, c22])).
% 1.29/1.47  cnf(c1167,plain,skolem0005!=X1152|existent(X1152,skolem0007),inference(resolution,[status(thm)],[c707, reflexivity])).
% 1.29/1.47  cnf(c599,plain,event(skolem0005,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c592, c54])).
% 1.29/1.47  cnf(c638,plain,eventuality(skolem0005,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c599, c216])).
% 1.29/1.47  cnf(c647,plain,thing(skolem0005,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c638, c198])).
% 1.29/1.47  cnf(c659,plain,singleton(skolem0005,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c647, c201])).
% 1.29/1.47  cnf(c661,plain,skolem0005!=X1145|skolem0009(skolem0002)!=X1144|singleton(X1145,X1144),inference(resolution,[status(thm)],[c659, c27])).
% 1.29/1.47  cnf(c1164,plain,skolem0005!=X1147|singleton(X1147,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c661, reflexivity])).
% 1.29/1.47  cnf(c20,axiom,X354!=X353|X352!=X355|~impartial(X354,X352)|impartial(X353,X355),theory(equality)).
% 1.29/1.47  fof(ax16,axiom,(![U]:(![V]:(organism(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax16)).
% 1.29/1.47  fof(c235,plain,(![U]:(![V]:(~organism(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax16])).
% 1.29/1.47  fof(c236,plain,(![X169]:(![X170]:(~organism(X169,X170)|impartial(X169,X170)))),inference(variable_rename,[status(thm)],[c235])).
% 1.29/1.47  cnf(c237,plain,~organism(X288,X289)|impartial(X288,X289),inference(split_conjunct,[status(thm)],[c236])).
% 1.29/1.47  cnf(c687,plain,impartial(skolem0005,skolem0007),inference(resolution,[status(thm)],[c678, c237])).
% 1.29/1.47  cnf(c702,plain,skolem0005!=X1142|skolem0007!=X1143|impartial(X1142,X1143),inference(resolution,[status(thm)],[c687, c20])).
% 1.29/1.47  cnf(c1163,plain,skolem0005!=X1146|impartial(X1146,skolem0007),inference(resolution,[status(thm)],[c702, reflexivity])).
% 1.29/1.47  cnf(c660,plain,skolem0005!=X1139|skolem0009(skolem0002)!=X1138|thing(X1139,X1138),inference(resolution,[status(thm)],[c647, c11])).
% 1.29/1.47  cnf(c1160,plain,skolem0005!=X1141|thing(X1141,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c660, reflexivity])).
% 1.29/1.47  cnf(c21,axiom,X360!=X359|X358!=X361|~entity(X360,X358)|entity(X359,X361),theory(equality)).
% 1.29/1.47  cnf(c699,plain,skolem0005!=X1137|skolem0007!=X1136|entity(X1137,X1136),inference(resolution,[status(thm)],[c686, c21])).
% 1.29/1.47  cnf(c1159,plain,skolem0005!=X1140|entity(X1140,skolem0007),inference(resolution,[status(thm)],[c699, reflexivity])).
% 1.29/1.47  cnf(c645,plain,specific(skolem0005,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c638, c204])).
% 1.29/1.47  cnf(c653,plain,skolem0005!=X1132|skolem0009(skolem0002)!=X1133|specific(X1132,X1133),inference(resolution,[status(thm)],[c645, c23])).
% 1.29/1.47  cnf(c1156,plain,skolem0005!=X1135|specific(X1135,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c653, reflexivity])).
% 1.29/1.47  cnf(c19,axiom,X346!=X345|X344!=X347|~living(X346,X344)|living(X345,X347),theory(equality)).
% 1.29/1.47  fof(ax15,axiom,(![U]:(![V]:(organism(U,V)=>living(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax15)).
% 1.29/1.47  fof(c238,plain,(![U]:(![V]:(~organism(U,V)|living(U,V)))),inference(fof_nnf,[status(thm)],[ax15])).
% 1.29/1.47  fof(c239,plain,(![X171]:(![X172]:(~organism(X171,X172)|living(X171,X172)))),inference(variable_rename,[status(thm)],[c238])).
% 1.29/1.47  cnf(c240,plain,~organism(X295,X294)|living(X295,X294),inference(split_conjunct,[status(thm)],[c239])).
% 1.29/1.47  cnf(c684,plain,living(skolem0005,skolem0007),inference(resolution,[status(thm)],[c678, c240])).
% 1.29/1.47  cnf(c696,plain,skolem0005!=X1131|skolem0007!=X1130|living(X1131,X1130),inference(resolution,[status(thm)],[c684, c19])).
% 1.29/1.47  cnf(c1155,plain,skolem0005!=X1134|living(X1134,skolem0007),inference(resolution,[status(thm)],[c696, reflexivity])).
% 1.29/1.47  cnf(c643,plain,nonexistent(skolem0005,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c638, c207])).
% 1.29/1.47  cnf(c650,plain,skolem0005!=X1127|skolem0009(skolem0002)!=X1126|nonexistent(X1127,X1126),inference(resolution,[status(thm)],[c643, c26])).
% 1.29/1.47  cnf(c1152,plain,skolem0005!=X1129|nonexistent(X1129,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c650, reflexivity])).
% 1.29/1.47  cnf(c16,axiom,X326!=X325|X324!=X327|~animate(X326,X324)|animate(X325,X327),theory(equality)).
% 1.29/1.47  fof(ax13,axiom,(![U]:(![V]:(human_person(U,V)=>animate(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax13)).
% 1.29/1.47  fof(c244,plain,(![U]:(![V]:(~human_person(U,V)|animate(U,V)))),inference(fof_nnf,[status(thm)],[ax13])).
% 1.29/1.47  fof(c245,plain,(![X175]:(![X176]:(~human_person(X175,X176)|animate(X175,X176)))),inference(variable_rename,[status(thm)],[c244])).
% 1.29/1.47  cnf(c246,plain,~human_person(X303,X302)|animate(X303,X302),inference(split_conjunct,[status(thm)],[c245])).
% 1.29/1.47  cnf(c680,plain,animate(skolem0005,skolem0007),inference(resolution,[status(thm)],[c671, c246])).
% 1.29/1.47  cnf(c694,plain,skolem0005!=X1124|skolem0007!=X1125|animate(X1124,X1125),inference(resolution,[status(thm)],[c680, c16])).
% 1.29/1.47  cnf(c1151,plain,skolem0005!=X1128|animate(X1128,skolem0007),inference(resolution,[status(thm)],[c694, reflexivity])).
% 1.29/1.47  cnf(c642,plain,unisex(skolem0005,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c638, c210])).
% 1.29/1.47  cnf(c649,plain,skolem0005!=X1120|skolem0009(skolem0002)!=X1121|unisex(X1120,X1121),inference(resolution,[status(thm)],[c642, c8])).
% 1.29/1.47  cnf(c1148,plain,skolem0005!=X1123|unisex(X1123,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c649, reflexivity])).
% 1.29/1.47  cnf(c17,axiom,X332!=X331|X330!=X333|~human(X332,X330)|human(X331,X333),theory(equality)).
% 1.29/1.47  fof(ax14,axiom,(![U]:(![V]:(human_person(U,V)=>human(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax14)).
% 1.29/1.47  fof(c241,plain,(![U]:(![V]:(~human_person(U,V)|human(U,V)))),inference(fof_nnf,[status(thm)],[ax14])).
% 1.29/1.47  fof(c242,plain,(![X173]:(![X174]:(~human_person(X173,X174)|human(X173,X174)))),inference(variable_rename,[status(thm)],[c241])).
% 1.29/1.47  cnf(c243,plain,~human_person(X296,X297)|human(X296,X297),inference(split_conjunct,[status(thm)],[c242])).
% 1.29/1.47  cnf(c679,plain,human(skolem0005,skolem0007),inference(resolution,[status(thm)],[c671, c243])).
% 1.29/1.47  cnf(c688,plain,skolem0005!=X1119|skolem0007!=X1118|human(X1119,X1118),inference(resolution,[status(thm)],[c679, c17])).
% 1.29/1.47  cnf(c1147,plain,skolem0005!=X1122|human(X1122,skolem0007),inference(resolution,[status(thm)],[c688, reflexivity])).
% 1.29/1.48  cnf(c644,plain,skolem0005!=X1115|skolem0009(skolem0002)!=X1114|eventuality(X1115,X1114),inference(resolution,[status(thm)],[c638, c24])).
% 1.29/1.48  cnf(c1144,plain,skolem0005!=X1117|eventuality(X1117,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c644, reflexivity])).
% 1.29/1.48  cnf(c18,axiom,X340!=X339|X338!=X341|~organism(X340,X338)|organism(X339,X341),theory(equality)).
% 1.29/1.48  cnf(c685,plain,skolem0005!=X1113|skolem0007!=X1112|organism(X1113,X1112),inference(resolution,[status(thm)],[c678, c18])).
% 1.29/1.48  cnf(c1143,plain,skolem0005!=X1116|organism(X1116,skolem0007),inference(resolution,[status(thm)],[c685, reflexivity])).
% 1.29/1.48  cnf(c637,plain,skolem0005!=X1108|skolem0009(skolem0002)!=X1109|event(X1108,X1109),inference(resolution,[status(thm)],[c599, c5])).
% 1.29/1.48  cnf(c1140,plain,skolem0005!=X1111|event(X1111,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c637, reflexivity])).
% 1.29/1.48  cnf(c15,axiom,X318!=X317|X316!=X319|~human_person(X318,X316)|human_person(X317,X319),theory(equality)).
% 1.29/1.48  cnf(c682,plain,skolem0005!=X1107|skolem0007!=X1106|human_person(X1107,X1106),inference(resolution,[status(thm)],[c671, c15])).
% 1.29/1.48  cnf(c1139,plain,skolem0005!=X1110|human_person(X1110,skolem0007),inference(resolution,[status(thm)],[c682, reflexivity])).
% 1.29/1.48  cnf(c595,plain,present(skolem0005,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c592, c56])).
% 1.29/1.48  cnf(c635,plain,skolem0005!=X1103|skolem0009(skolem0002)!=X1102|present(X1103,X1102),inference(resolution,[status(thm)],[c595, c32])).
% 1.29/1.48  cnf(c1136,plain,skolem0005!=X1105|present(X1105,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c635, reflexivity])).
% 1.29/1.48  cnf(c14,axiom,X312!=X311|X310!=X313|~male(X312,X310)|male(X311,X313),theory(equality)).
% 1.29/1.48  fof(ax12,axiom,(![U]:(![V]:(man(U,V)=>male(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax12)).
% 1.29/1.48  fof(c247,plain,(![U]:(![V]:(~man(U,V)|male(U,V)))),inference(fof_nnf,[status(thm)],[ax12])).
% 1.29/1.48  fof(c248,plain,(![X177]:(![X178]:(~man(X177,X178)|male(X177,X178)))),inference(variable_rename,[status(thm)],[c247])).
% 1.29/1.48  cnf(c249,plain,~man(X309,X308)|male(X309,X308),inference(split_conjunct,[status(thm)],[c248])).
% 1.29/1.48  cnf(c668,plain,male(skolem0005,skolem0007),inference(resolution,[status(thm)],[c663, c249])).
% 1.29/1.48  cnf(c675,plain,skolem0005!=X1100|skolem0007!=X1101|male(X1100,X1101),inference(resolution,[status(thm)],[c668, c14])).
% 1.29/1.48  cnf(c1135,plain,skolem0005!=X1104|male(X1104,skolem0007),inference(resolution,[status(thm)],[c675, reflexivity])).
% 1.29/1.48  cnf(c594,plain,smoke(skolem0005,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c592, c57])).
% 1.29/1.48  cnf(c634,plain,skolem0005!=X1096|skolem0009(skolem0002)!=X1097|smoke(X1096,X1097),inference(resolution,[status(thm)],[c594, c4])).
% 1.29/1.48  cnf(c1132,plain,skolem0005!=X1099|smoke(X1099,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c634, reflexivity])).
% 1.29/1.48  cnf(c13,axiom,X306!=X305|X304!=X307|~man(X306,X304)|man(X305,X307),theory(equality)).
% 1.29/1.48  cnf(c664,plain,skolem0005!=X1095|skolem0007!=X1094|man(X1095,X1094),inference(resolution,[status(thm)],[c663, c13])).
% 1.29/1.48  cnf(c1131,plain,skolem0005!=X1098|man(X1098,skolem0007),inference(resolution,[status(thm)],[c664, reflexivity])).
% 1.29/1.48  cnf(c600,plain,human_person(skolem0005,skolem0002),inference(resolution,[status(thm)],[c592, c219])).
% 1.29/1.48  cnf(c605,plain,organism(skolem0005,skolem0002),inference(resolution,[status(thm)],[c600, c222])).
% 1.29/1.48  cnf(c613,plain,entity(skolem0005,skolem0002),inference(resolution,[status(thm)],[c605, c225])).
% 1.29/1.48  cnf(c621,plain,existent(skolem0005,skolem0002),inference(resolution,[status(thm)],[c613, c234])).
% 1.29/1.48  cnf(c629,plain,skolem0005!=X1091|skolem0002!=X1090|existent(X1091,X1090),inference(resolution,[status(thm)],[c621, c22])).
% 1.29/1.48  cnf(c1128,plain,skolem0005!=X1093|existent(X1093,skolem0002),inference(resolution,[status(thm)],[c629, reflexivity])).
% 1.29/1.48  cnf(c614,plain,impartial(skolem0005,skolem0002),inference(resolution,[status(thm)],[c605, c237])).
% 1.29/1.48  cnf(c626,plain,skolem0005!=X1088|skolem0002!=X1089|impartial(X1088,X1089),inference(resolution,[status(thm)],[c614, c20])).
% 1.29/1.48  cnf(c1127,plain,skolem0005!=X1092|impartial(X1092,skolem0002),inference(resolution,[status(thm)],[c626, reflexivity])).
% 1.29/1.48  cnf(c623,plain,skolem0005!=X1085|skolem0002!=X1084|entity(X1085,X1084),inference(resolution,[status(thm)],[c613, c21])).
% 1.29/1.48  cnf(c1124,plain,skolem0005!=X1087|entity(X1087,skolem0002),inference(resolution,[status(thm)],[c623, reflexivity])).
% 1.29/1.48  cnf(c611,plain,living(skolem0005,skolem0002),inference(resolution,[status(thm)],[c605, c240])).
% 1.29/1.48  cnf(c620,plain,skolem0005!=X1083|skolem0002!=X1082|living(X1083,X1082),inference(resolution,[status(thm)],[c611, c19])).
% 1.29/1.48  cnf(c1123,plain,skolem0005!=X1086|living(X1086,skolem0002),inference(resolution,[status(thm)],[c620, reflexivity])).
% 1.29/1.48  cnf(c607,plain,animate(skolem0005,skolem0002),inference(resolution,[status(thm)],[c600, c246])).
% 1.29/1.48  cnf(c617,plain,skolem0005!=X1078|skolem0002!=X1079|animate(X1078,X1079),inference(resolution,[status(thm)],[c607, c16])).
% 1.29/1.48  cnf(c1120,plain,skolem0005!=X1081|animate(X1081,skolem0002),inference(resolution,[status(thm)],[c617, reflexivity])).
% 1.29/1.48  cnf(c606,plain,human(skolem0005,skolem0002),inference(resolution,[status(thm)],[c600, c243])).
% 1.29/1.48  cnf(c615,plain,skolem0005!=X1077|skolem0002!=X1076|human(X1077,X1076),inference(resolution,[status(thm)],[c606, c17])).
% 1.29/1.48  cnf(c1119,plain,skolem0005!=X1080|human(X1080,skolem0002),inference(resolution,[status(thm)],[c615, reflexivity])).
% 1.29/1.48  cnf(c612,plain,skolem0005!=X1073|skolem0002!=X1072|organism(X1073,X1072),inference(resolution,[status(thm)],[c605, c18])).
% 1.29/1.48  cnf(c1116,plain,skolem0005!=X1075|organism(X1075,skolem0002),inference(resolution,[status(thm)],[c612, reflexivity])).
% 1.29/1.48  cnf(c609,plain,skolem0005!=X1071|skolem0002!=X1070|human_person(X1071,X1070),inference(resolution,[status(thm)],[c600, c15])).
% 1.29/1.48  cnf(c1115,plain,skolem0005!=X1074|human_person(X1074,skolem0002),inference(resolution,[status(thm)],[c609, reflexivity])).
% 1.29/1.48  cnf(c597,plain,male(skolem0005,skolem0002),inference(resolution,[status(thm)],[c592, c249])).
% 1.29/1.48  cnf(c601,plain,skolem0005!=X1067|skolem0002!=X1068|male(X1067,X1068),inference(resolution,[status(thm)],[c597, c14])).
% 1.29/1.48  cnf(c1113,plain,skolem0005!=X1069|male(X1069,skolem0002),inference(resolution,[status(thm)],[c601, reflexivity])).
% 1.29/1.48  cnf(c593,plain,skolem0005!=X1062|skolem0002!=X1061|man(X1062,X1061),inference(resolution,[status(thm)],[c592, c13])).
% 1.29/1.48  cnf(c1109,plain,skolem0005!=X1063|man(X1063,skolem0002),inference(resolution,[status(thm)],[c593, reflexivity])).
% 1.29/1.48  cnf(c50,negated_conjecture,event(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.48  fof(ax60,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&event(V,U))=>event(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax60)).
% 1.29/1.48  fof(c99,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~event(V,U))|event(W,U))))),inference(fof_nnf,[status(thm)],[ax60])).
% 1.29/1.48  fof(c100,plain,(![X52]:(![X53]:(![X54]:((~accessible_world(X53,X54)|~event(X53,X52))|event(X54,X52))))),inference(variable_rename,[status(thm)],[c99])).
% 1.29/1.48  cnf(c101,plain,~accessible_world(X519,X521)|~event(X519,X520)|event(X521,X520),inference(split_conjunct,[status(thm)],[c100])).
% 1.29/1.48  cnf(c565,plain,~accessible_world(skolem0001,X542)|event(X542,skolem0004),inference(resolution,[status(thm)],[c101, c50])).
% 1.29/1.48  cnf(c585,plain,event(skolem0005,skolem0004),inference(resolution,[status(thm)],[c565, c53])).
% 1.29/1.48  cnf(c587,plain,skolem0005!=X1058|skolem0004!=X1059|event(X1058,X1059),inference(resolution,[status(thm)],[c585, c5])).
% 1.29/1.48  cnf(c1107,plain,skolem0005!=X1060|event(X1060,skolem0004),inference(resolution,[status(thm)],[c587, reflexivity])).
% 1.29/1.48  fof(ax5,axiom,(![U]:(![V]:(abstraction(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax5)).
% 1.29/1.48  fof(c268,plain,(![U]:(![V]:(~abstraction(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax5])).
% 1.29/1.48  fof(c269,plain,(![X191]:(![X192]:(~abstraction(X191,X192)|unisex(X191,X192)))),inference(variable_rename,[status(thm)],[c268])).
% 1.29/1.48  cnf(c270,plain,~abstraction(X343,X342)|unisex(X343,X342),inference(split_conjunct,[status(thm)],[c269])).
% 1.29/1.48  cnf(c393,plain,abstraction(skolem0001,skolem0005),inference(resolution,[status(thm)],[c392, c258])).
% 1.29/1.48  cnf(c397,plain,unisex(skolem0001,skolem0005),inference(resolution,[status(thm)],[c393, c270])).
% 1.29/1.48  fof(ax61,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&unisex(V,U))=>unisex(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax61)).
% 1.29/1.48  fof(c96,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~unisex(V,U))|unisex(W,U))))),inference(fof_nnf,[status(thm)],[ax61])).
% 1.29/1.48  fof(c97,plain,(![X49]:(![X50]:(![X51]:((~accessible_world(X50,X51)|~unisex(X50,X49))|unisex(X51,X49))))),inference(variable_rename,[status(thm)],[c96])).
% 1.29/1.48  cnf(c98,plain,~accessible_world(X513,X514)|~unisex(X513,X512)|unisex(X514,X512),inference(split_conjunct,[status(thm)],[c97])).
% 1.29/1.48  cnf(c561,plain,~accessible_world(skolem0001,X536)|unisex(X536,skolem0005),inference(resolution,[status(thm)],[c98, c397])).
% 1.29/1.48  cnf(c580,plain,unisex(skolem0005,skolem0005),inference(resolution,[status(thm)],[c561, c53])).
% 1.29/1.48  cnf(c581,plain,skolem0005!=X1049|skolem0005!=X1050|unisex(X1049,X1050),inference(resolution,[status(thm)],[c580, c8])).
% 1.29/1.48  cnf(c1101,plain,skolem0005!=X1052|unisex(X1052,skolem0005),inference(resolution,[status(thm)],[c581, reflexivity])).
% 1.29/1.48  cnf(c1100,plain,skolem0005!=X1051|unisex(X1051,X1051),inference(factor,[status(thm)],[c581])).
% 1.29/1.48  cnf(c530,plain,~entity(skolem0001,skolem0007)|~forename(skolem0001,X1048)|~of(skolem0001,X1048,skolem0007)|~forename(skolem0001,skolem0006)|skolem0006=X1048,inference(resolution,[status(thm)],[c71, c58])).
% 1.29/1.48  cnf(c347,plain,relname(skolem0001,skolem0006),inference(resolution,[status(thm)],[c252, c61])).
% 1.29/1.48  cnf(c353,plain,relation(skolem0001,skolem0006),inference(resolution,[status(thm)],[c255, c347])).
% 1.29/1.48  cnf(c358,plain,abstraction(skolem0001,skolem0006),inference(resolution,[status(thm)],[c258, c353])).
% 1.29/1.48  cnf(c384,plain,unisex(skolem0001,skolem0006),inference(resolution,[status(thm)],[c270, c358])).
% 1.29/1.48  cnf(c560,plain,~accessible_world(skolem0001,X535)|unisex(X535,skolem0006),inference(resolution,[status(thm)],[c98, c384])).
% 1.29/1.48  cnf(c577,plain,unisex(skolem0005,skolem0006),inference(resolution,[status(thm)],[c560, c53])).
% 1.29/1.48  cnf(c578,plain,skolem0005!=X1045|skolem0006!=X1046|unisex(X1045,X1046),inference(resolution,[status(thm)],[c577, c8])).
% 1.29/1.48  cnf(c1097,plain,skolem0005!=X1047|unisex(X1047,skolem0006),inference(resolution,[status(thm)],[c578, reflexivity])).
% 1.29/1.48  cnf(c348,plain,relname(skolem0001,skolem0003),inference(resolution,[status(thm)],[c252, c46])).
% 1.29/1.48  cnf(c354,plain,relation(skolem0001,skolem0003),inference(resolution,[status(thm)],[c255, c348])).
% 1.29/1.48  cnf(c357,plain,abstraction(skolem0001,skolem0003),inference(resolution,[status(thm)],[c258, c354])).
% 1.29/1.48  cnf(c383,plain,unisex(skolem0001,skolem0003),inference(resolution,[status(thm)],[c270, c357])).
% 1.29/1.48  cnf(c558,plain,~accessible_world(skolem0001,X530)|unisex(X530,skolem0003),inference(resolution,[status(thm)],[c98, c383])).
% 1.29/1.48  cnf(c572,plain,unisex(skolem0005,skolem0003),inference(resolution,[status(thm)],[c558, c53])).
% 1.29/1.48  cnf(c573,plain,skolem0005!=X1041|skolem0003!=X1042|unisex(X1041,X1042),inference(resolution,[status(thm)],[c572, c8])).
% 1.29/1.48  cnf(c1094,plain,skolem0005!=X1044|unisex(X1044,skolem0003),inference(resolution,[status(thm)],[c573, reflexivity])).
% 1.29/1.48  cnf(c529,plain,~entity(skolem0001,skolem0002)|~forename(skolem0001,X1043)|~of(skolem0001,X1043,skolem0002)|~forename(skolem0001,skolem0003)|skolem0003=X1043,inference(resolution,[status(thm)],[c71, c43])).
% 1.29/1.48  cnf(c309,plain,human_person(skolem0001,skolem0002),inference(resolution,[status(thm)],[c219, c44])).
% 1.29/1.48  cnf(c312,plain,organism(skolem0001,skolem0002),inference(resolution,[status(thm)],[c222, c309])).
% 1.29/1.48  cnf(c313,plain,entity(skolem0001,skolem0002),inference(resolution,[status(thm)],[c225, c312])).
% 1.29/1.48  fof(ax18,axiom,(![U]:(![V]:(entity(U,V)=>specific(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax18)).
% 1.29/1.48  fof(c229,plain,(![U]:(![V]:(~entity(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax18])).
% 1.29/1.48  fof(c230,plain,(![X165]:(![X166]:(~entity(X165,X166)|specific(X165,X166)))),inference(variable_rename,[status(thm)],[c229])).
% 1.29/1.48  cnf(c231,plain,~entity(X281,X280)|specific(X281,X280),inference(split_conjunct,[status(thm)],[c230])).
% 1.29/1.48  cnf(c322,plain,specific(skolem0001,skolem0002),inference(resolution,[status(thm)],[c231, c313])).
% 1.29/1.48  fof(ax63,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&specific(V,U))=>specific(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax63)).
% 1.29/1.48  fof(c90,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~specific(V,U))|specific(W,U))))),inference(fof_nnf,[status(thm)],[ax63])).
% 1.29/1.48  fof(c91,plain,(![X43]:(![X44]:(![X45]:((~accessible_world(X44,X45)|~specific(X44,X43))|specific(X45,X43))))),inference(variable_rename,[status(thm)],[c90])).
% 1.29/1.48  cnf(c92,plain,~accessible_world(X501,X503)|~specific(X501,X502)|specific(X503,X502),inference(split_conjunct,[status(thm)],[c91])).
% 1.29/1.48  cnf(c539,plain,~accessible_world(skolem0001,X505)|specific(X505,skolem0002),inference(resolution,[status(thm)],[c92, c322])).
% 1.29/1.48  cnf(c547,plain,specific(skolem0005,skolem0002),inference(resolution,[status(thm)],[c539, c53])).
% 1.29/1.48  cnf(c548,plain,skolem0005!=X1038|skolem0002!=X1039|specific(X1038,X1039),inference(resolution,[status(thm)],[c547, c23])).
% 1.29/1.48  cnf(c1092,plain,skolem0005!=X1040|specific(X1040,skolem0002),inference(resolution,[status(thm)],[c548, reflexivity])).
% 1.29/1.48  cnf(c310,plain,human_person(skolem0001,skolem0007),inference(resolution,[status(thm)],[c219, c59])).
% 1.29/1.48  cnf(c311,plain,organism(skolem0001,skolem0007),inference(resolution,[status(thm)],[c222, c310])).
% 1.29/1.48  cnf(c314,plain,entity(skolem0001,skolem0007),inference(resolution,[status(thm)],[c225, c311])).
% 1.29/1.48  cnf(c321,plain,specific(skolem0001,skolem0007),inference(resolution,[status(thm)],[c231, c314])).
% 1.29/1.48  cnf(c538,plain,~accessible_world(skolem0001,X504)|specific(X504,skolem0007),inference(resolution,[status(thm)],[c92, c321])).
% 1.29/1.48  cnf(c544,plain,specific(skolem0005,skolem0007),inference(resolution,[status(thm)],[c538, c53])).
% 1.29/1.48  cnf(c545,plain,skolem0005!=X1032|skolem0007!=X1033|specific(X1032,X1033),inference(resolution,[status(thm)],[c544, c23])).
% 1.29/1.48  cnf(c1090,plain,skolem0005!=X1034|specific(X1034,skolem0007),inference(resolution,[status(thm)],[c545, reflexivity])).
% 1.29/1.48  fof(ax8,axiom,(![U]:(![V]:(abstraction(U,V)=>thing(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax8)).
% 1.29/1.48  fof(c259,plain,(![U]:(![V]:(~abstraction(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax8])).
% 1.29/1.48  fof(c260,plain,(![X185]:(![X186]:(~abstraction(X185,X186)|thing(X185,X186)))),inference(variable_rename,[status(thm)],[c259])).
% 1.29/1.48  cnf(c261,plain,~abstraction(X329,X328)|thing(X329,X328),inference(split_conjunct,[status(thm)],[c260])).
% 1.29/1.48  cnf(c363,plain,thing(skolem0001,skolem0003),inference(resolution,[status(thm)],[c261, c357])).
% 1.29/1.48  fof(ax65,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&thing(V,U))=>thing(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax65)).
% 1.29/1.48  fof(c84,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~thing(V,U))|thing(W,U))))),inference(fof_nnf,[status(thm)],[ax65])).
% 1.29/1.48  fof(c85,plain,(![X37]:(![X38]:(![X39]:((~accessible_world(X38,X39)|~thing(X38,X37))|thing(X39,X37))))),inference(variable_rename,[status(thm)],[c84])).
% 1.29/1.48  cnf(c86,plain,~accessible_world(X425,X424)|~thing(X425,X423)|thing(X424,X423),inference(split_conjunct,[status(thm)],[c85])).
% 1.29/1.48  cnf(c477,plain,~accessible_world(skolem0001,X454)|thing(X454,skolem0003),inference(resolution,[status(thm)],[c86, c363])).
% 1.29/1.48  cnf(c505,plain,thing(skolem0005,skolem0003),inference(resolution,[status(thm)],[c477, c53])).
% 1.29/1.48  cnf(c507,plain,singleton(skolem0005,skolem0003),inference(resolution,[status(thm)],[c505, c201])).
% 1.29/1.48  cnf(c509,plain,skolem0005!=X1025|skolem0003!=X1024|singleton(X1025,X1024),inference(resolution,[status(thm)],[c507, c27])).
% 1.29/1.48  cnf(c1082,plain,skolem0005!=X1026|singleton(X1026,skolem0003),inference(resolution,[status(thm)],[c509, reflexivity])).
% 1.29/1.48  cnf(c508,plain,skolem0005!=X1019|skolem0003!=X1018|thing(X1019,X1018),inference(resolution,[status(thm)],[c505, c11])).
% 1.29/1.48  cnf(c1079,plain,skolem0005!=X1023|thing(X1023,skolem0003),inference(resolution,[status(thm)],[c508, reflexivity])).
% 1.29/1.48  cnf(c364,plain,thing(skolem0001,skolem0006),inference(resolution,[status(thm)],[c261, c358])).
% 1.29/1.48  cnf(c476,plain,~accessible_world(skolem0001,X447)|thing(X447,skolem0006),inference(resolution,[status(thm)],[c86, c364])).
% 1.29/1.48  cnf(c498,plain,thing(skolem0005,skolem0006),inference(resolution,[status(thm)],[c476, c53])).
% 1.29/1.48  cnf(c500,plain,singleton(skolem0005,skolem0006),inference(resolution,[status(thm)],[c498, c201])).
% 1.29/1.48  cnf(c504,plain,skolem0005!=X1016|skolem0006!=X1015|singleton(X1016,X1015),inference(resolution,[status(thm)],[c500, c27])).
% 1.29/1.48  cnf(c1077,plain,skolem0005!=X1017|singleton(X1017,skolem0006),inference(resolution,[status(thm)],[c504, reflexivity])).
% 1.29/1.48  cnf(c501,plain,skolem0005!=X1010|skolem0006!=X1009|thing(X1010,X1009),inference(resolution,[status(thm)],[c498, c11])).
% 1.29/1.48  cnf(c1074,plain,skolem0005!=X1011|thing(X1011,skolem0006),inference(resolution,[status(thm)],[c501, reflexivity])).
% 1.29/1.48  fof(ax19,axiom,(![U]:(![V]:(entity(U,V)=>thing(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax19)).
% 1.29/1.48  fof(c226,plain,(![U]:(![V]:(~entity(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax19])).
% 1.29/1.48  fof(c227,plain,(![X163]:(![X164]:(~entity(X163,X164)|thing(X163,X164)))),inference(variable_rename,[status(thm)],[c226])).
% 1.29/1.48  cnf(c228,plain,~entity(X274,X275)|thing(X274,X275),inference(split_conjunct,[status(thm)],[c227])).
% 1.29/1.48  cnf(c318,plain,thing(skolem0001,skolem0002),inference(resolution,[status(thm)],[c228, c313])).
% 1.29/1.48  cnf(c474,plain,~accessible_world(skolem0001,X441)|thing(X441,skolem0002),inference(resolution,[status(thm)],[c86, c318])).
% 1.29/1.48  cnf(c491,plain,thing(skolem0005,skolem0002),inference(resolution,[status(thm)],[c474, c53])).
% 1.29/1.48  cnf(c493,plain,singleton(skolem0005,skolem0002),inference(resolution,[status(thm)],[c491, c201])).
% 1.29/1.48  cnf(c496,plain,skolem0005!=X1007|skolem0002!=X1006|singleton(X1007,X1006),inference(resolution,[status(thm)],[c493, c27])).
% 1.29/1.48  cnf(c1072,plain,skolem0005!=X1008|singleton(X1008,skolem0002),inference(resolution,[status(thm)],[c496, reflexivity])).
% 1.29/1.48  cnf(c495,plain,skolem0001!=X1004|skolem0004!=X1003|present(X1004,X1003),inference(resolution,[status(thm)],[c32, c51])).
% 1.29/1.48  cnf(c1070,plain,skolem0001!=X1005|present(X1005,skolem0004),inference(resolution,[status(thm)],[c495, reflexivity])).
% 1.29/1.48  cnf(c494,plain,skolem0005!=X1001|skolem0002!=X1000|thing(X1001,X1000),inference(resolution,[status(thm)],[c491, c11])).
% 1.29/1.48  cnf(c1068,plain,skolem0005!=X1002|thing(X1002,skolem0002),inference(resolution,[status(thm)],[c494, reflexivity])).
% 1.29/1.48  cnf(c395,plain,thing(skolem0001,skolem0005),inference(resolution,[status(thm)],[c393, c261])).
% 1.29/1.48  cnf(c470,plain,~accessible_world(skolem0001,X431)|thing(X431,skolem0005),inference(resolution,[status(thm)],[c86, c395])).
% 1.29/1.48  cnf(c484,plain,thing(skolem0005,skolem0005),inference(resolution,[status(thm)],[c470, c53])).
% 1.29/1.48  cnf(c486,plain,singleton(skolem0005,skolem0005),inference(resolution,[status(thm)],[c484, c201])).
% 1.29/1.48  cnf(c488,plain,skolem0005!=X994|skolem0005!=X993|singleton(X994,X993),inference(resolution,[status(thm)],[c486, c27])).
% 1.29/1.48  cnf(c1064,plain,skolem0005!=X996|singleton(X996,skolem0005),inference(resolution,[status(thm)],[c488, reflexivity])).
% 1.29/1.48  cnf(c1063,plain,skolem0005!=X995|singleton(X995,X995),inference(factor,[status(thm)],[c488])).
% 1.29/1.48  cnf(c487,plain,skolem0005!=X989|skolem0005!=X988|thing(X989,X988),inference(resolution,[status(thm)],[c484, c11])).
% 1.29/1.48  cnf(c1059,plain,skolem0005!=X992|thing(X992,skolem0005),inference(resolution,[status(thm)],[c487, reflexivity])).
% 1.29/1.48  cnf(c317,plain,thing(skolem0001,skolem0007),inference(resolution,[status(thm)],[c228, c314])).
% 1.29/1.48  cnf(c469,plain,~accessible_world(skolem0001,X426)|thing(X426,skolem0007),inference(resolution,[status(thm)],[c86, c317])).
% 1.29/1.48  cnf(c478,plain,thing(skolem0005,skolem0007),inference(resolution,[status(thm)],[c469, c53])).
% 1.29/1.48  cnf(c480,plain,singleton(skolem0005,skolem0007),inference(resolution,[status(thm)],[c478, c201])).
% 1.29/1.48  cnf(c483,plain,skolem0005!=X987|skolem0007!=X986|singleton(X987,X986),inference(resolution,[status(thm)],[c480, c27])).
% 1.29/1.48  cnf(c1057,plain,skolem0005!=X991|singleton(X991,skolem0007),inference(resolution,[status(thm)],[c483, reflexivity])).
% 1.29/1.48  cnf(c1058,plain,skolem0005!=X990|thing(X990,X990),inference(factor,[status(thm)],[c487])).
% 1.29/1.48  cnf(c482,plain,skolem0001!=X984|skolem0004!=X983|think_believe_consider(X984,X983),inference(resolution,[status(thm)],[c30, c52])).
% 1.29/1.48  cnf(c1055,plain,skolem0001!=X985|think_believe_consider(X985,skolem0004),inference(resolution,[status(thm)],[c482, reflexivity])).
% 1.29/1.48  cnf(c481,plain,skolem0005!=X978|skolem0007!=X977|thing(X978,X977),inference(resolution,[status(thm)],[c478, c11])).
% 1.29/1.48  cnf(c1052,plain,skolem0005!=X979|thing(X979,skolem0007),inference(resolution,[status(thm)],[c481, reflexivity])).
% 1.29/1.48  cnf(c298,plain,eventuality(skolem0001,skolem0004),inference(resolution,[status(thm)],[c216, c50])).
% 1.29/1.48  fof(ax66,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&eventuality(V,U))=>eventuality(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax66)).
% 1.29/1.48  fof(c81,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~eventuality(V,U))|eventuality(W,U))))),inference(fof_nnf,[status(thm)],[ax66])).
% 1.29/1.48  fof(c82,plain,(![X34]:(![X35]:(![X36]:((~accessible_world(X35,X36)|~eventuality(X35,X34))|eventuality(X36,X34))))),inference(variable_rename,[status(thm)],[c81])).
% 1.29/1.48  cnf(c83,plain,~accessible_world(X404,X403)|~eventuality(X404,X402)|eventuality(X403,X402),inference(split_conjunct,[status(thm)],[c82])).
% 1.29/1.48  cnf(c442,plain,~accessible_world(skolem0001,X410)|eventuality(X410,skolem0004),inference(resolution,[status(thm)],[c83, c298])).
% 1.29/1.48  cnf(c453,plain,eventuality(skolem0005,skolem0004),inference(resolution,[status(thm)],[c442, c53])).
% 1.29/1.48  cnf(c459,plain,thing(skolem0005,skolem0004),inference(resolution,[status(thm)],[c453, c198])).
% 1.29/1.48  cnf(c465,plain,singleton(skolem0005,skolem0004),inference(resolution,[status(thm)],[c459, c201])).
% 1.29/1.48  cnf(c467,plain,skolem0005!=X975|skolem0004!=X974|singleton(X975,X974),inference(resolution,[status(thm)],[c465, c27])).
% 1.29/1.48  cnf(c1050,plain,skolem0005!=X976|singleton(X976,skolem0004),inference(resolution,[status(thm)],[c467, reflexivity])).
% 1.29/1.48  cnf(c466,plain,skolem0005!=X972|skolem0004!=X971|thing(X972,X971),inference(resolution,[status(thm)],[c459, c11])).
% 1.29/1.48  cnf(c1048,plain,skolem0005!=X973|thing(X973,skolem0004),inference(resolution,[status(thm)],[c466, reflexivity])).
% 1.29/1.48  cnf(c457,plain,specific(skolem0005,skolem0004),inference(resolution,[status(thm)],[c453, c204])).
% 1.29/1.48  cnf(c464,plain,skolem0005!=X968|skolem0004!=X969|specific(X968,X969),inference(resolution,[status(thm)],[c457, c23])).
% 1.29/1.48  cnf(c1046,plain,skolem0005!=X970|specific(X970,skolem0004),inference(resolution,[status(thm)],[c464, reflexivity])).
% 1.29/1.48  cnf(c455,plain,nonexistent(skolem0005,skolem0004),inference(resolution,[status(thm)],[c453, c207])).
% 1.29/1.48  cnf(c462,plain,skolem0005!=X966|skolem0004!=X965|nonexistent(X966,X965),inference(resolution,[status(thm)],[c455, c26])).
% 1.29/1.48  cnf(c1044,plain,skolem0005!=X967|nonexistent(X967,skolem0004),inference(resolution,[status(thm)],[c462, reflexivity])).
% 1.29/1.48  cnf(c28,axiom,X413!=X412|X411!=X414|~accessible_world(X413,X411)|accessible_world(X412,X414),theory(equality)).
% 1.29/1.48  cnf(c461,plain,skolem0001!=X962|skolem0005!=X963|accessible_world(X962,X963),inference(resolution,[status(thm)],[c28, c53])).
% 1.29/1.48  cnf(c1042,plain,skolem0001!=X964|accessible_world(X964,skolem0005),inference(resolution,[status(thm)],[c461, reflexivity])).
% 1.29/1.48  cnf(c454,plain,unisex(skolem0005,skolem0004),inference(resolution,[status(thm)],[c453, c210])).
% 1.29/1.48  cnf(c460,plain,skolem0005!=X959|skolem0004!=X960|unisex(X959,X960),inference(resolution,[status(thm)],[c454, c8])).
% 1.29/1.48  cnf(c1040,plain,skolem0005!=X961|unisex(X961,skolem0004),inference(resolution,[status(thm)],[c460, reflexivity])).
% 1.29/1.48  cnf(c456,plain,skolem0005!=X957|skolem0004!=X956|eventuality(X957,X956),inference(resolution,[status(thm)],[c453, c24])).
% 1.29/1.48  cnf(c1038,plain,skolem0005!=X958|eventuality(X958,skolem0004),inference(resolution,[status(thm)],[c456, reflexivity])).
% 1.29/1.48  cnf(c320,plain,singleton(skolem0001,skolem0002),inference(resolution,[status(thm)],[c318, c201])).
% 1.29/1.48  cnf(c451,plain,skolem0001!=X954|skolem0002!=X953|singleton(X954,X953),inference(resolution,[status(thm)],[c27, c320])).
% 1.29/1.48  cnf(c1036,plain,skolem0001!=X955|singleton(X955,skolem0002),inference(resolution,[status(thm)],[c451, reflexivity])).
% 1.29/1.48  cnf(c63,negated_conjecture,state(skolem0001,skolem0008),inference(split_conjunct,[status(thm)],[c41])).
% 1.29/1.48  fof(ax30,axiom,(![U]:(![V]:(state(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax30)).
% 1.29/1.48  fof(c193,plain,(![U]:(![V]:(~state(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax30])).
% 1.29/1.48  fof(c194,plain,(![X141]:(![X142]:(~state(X141,X142)|eventuality(X141,X142)))),inference(variable_rename,[status(thm)],[c193])).
% 1.29/1.48  cnf(c195,plain,~state(X225,X224)|eventuality(X225,X224),inference(split_conjunct,[status(thm)],[c194])).
% 1.29/1.48  cnf(c289,plain,eventuality(skolem0001,skolem0008),inference(resolution,[status(thm)],[c195, c63])).
% 1.29/1.48  cnf(c291,plain,thing(skolem0001,skolem0008),inference(resolution,[status(thm)],[c198, c289])).
% 1.29/1.48  cnf(c292,plain,singleton(skolem0001,skolem0008),inference(resolution,[status(thm)],[c201, c291])).
% 1.29/1.48  cnf(c450,plain,skolem0001!=X951|skolem0008!=X950|singleton(X951,X950),inference(resolution,[status(thm)],[c27, c292])).
% 1.29/1.48  cnf(c1034,plain,skolem0001!=X952|singleton(X952,skolem0008),inference(resolution,[status(thm)],[c450, reflexivity])).
% 1.29/1.48  fof(ax67,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&state(V,U))=>state(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax67)).
% 1.29/1.48  fof(c78,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~state(V,U))|state(W,U))))),inference(fof_nnf,[status(thm)],[ax67])).
% 1.29/1.48  fof(c79,plain,(![X31]:(![X32]:(![X33]:((~accessible_world(X32,X33)|~state(X32,X31))|state(X33,X31))))),inference(variable_rename,[status(thm)],[c78])).
% 1.29/1.48  cnf(c80,plain,~accessible_world(X391,X390)|~state(X391,X389)|state(X390,X389),inference(split_conjunct,[status(thm)],[c79])).
% 1.29/1.48  cnf(c419,plain,~accessible_world(skolem0001,X392)|state(X392,skolem0008),inference(resolution,[status(thm)],[c80, c63])).
% 1.29/1.48  cnf(c420,plain,state(skolem0005,skolem0008),inference(resolution,[status(thm)],[c419, c53])).
% 1.29/1.48  cnf(c421,plain,eventuality(skolem0005,skolem0008),inference(resolution,[status(thm)],[c420, c195])).
% 1.29/1.48  cnf(c428,plain,thing(skolem0005,skolem0008),inference(resolution,[status(thm)],[c421, c198])).
% 1.29/1.48  cnf(c436,plain,singleton(skolem0005,skolem0008),inference(resolution,[status(thm)],[c428, c201])).
% 1.29/1.48  cnf(c449,plain,skolem0005!=X948|skolem0008!=X947|singleton(X948,X947),inference(resolution,[status(thm)],[c27, c436])).
% 1.29/1.48  cnf(c1032,plain,skolem0005!=X949|singleton(X949,skolem0008),inference(resolution,[status(thm)],[c449, reflexivity])).
% 1.29/1.48  cnf(c319,plain,singleton(skolem0001,skolem0007),inference(resolution,[status(thm)],[c317, c201])).
% 1.29/1.48  cnf(c448,plain,skolem0001!=X945|skolem0007!=X944|singleton(X945,X944),inference(resolution,[status(thm)],[c27, c319])).
% 1.32/1.48  cnf(c1030,plain,skolem0001!=X946|singleton(X946,skolem0007),inference(resolution,[status(thm)],[c448, reflexivity])).
% 1.32/1.48  cnf(c400,plain,singleton(skolem0001,skolem0005),inference(resolution,[status(thm)],[c395, c201])).
% 1.32/1.48  cnf(c447,plain,skolem0001!=X942|skolem0005!=X941|singleton(X942,X941),inference(resolution,[status(thm)],[c27, c400])).
% 1.32/1.48  cnf(c1028,plain,skolem0001!=X943|singleton(X943,skolem0005),inference(resolution,[status(thm)],[c447, reflexivity])).
% 1.32/1.48  cnf(c367,plain,singleton(skolem0001,skolem0006),inference(resolution,[status(thm)],[c364, c201])).
% 1.32/1.48  cnf(c446,plain,skolem0001!=X939|skolem0006!=X938|singleton(X939,X938),inference(resolution,[status(thm)],[c27, c367])).
% 1.32/1.48  cnf(c1026,plain,skolem0001!=X940|singleton(X940,skolem0006),inference(resolution,[status(thm)],[c446, reflexivity])).
% 1.32/1.48  cnf(c365,plain,singleton(skolem0001,skolem0003),inference(resolution,[status(thm)],[c363, c201])).
% 1.32/1.48  cnf(c445,plain,skolem0001!=X936|skolem0003!=X935|singleton(X936,X935),inference(resolution,[status(thm)],[c27, c365])).
% 1.32/1.48  cnf(c1024,plain,skolem0001!=X937|singleton(X937,skolem0003),inference(resolution,[status(thm)],[c445, reflexivity])).
% 1.32/1.48  cnf(c305,plain,thing(skolem0001,skolem0004),inference(resolution,[status(thm)],[c298, c198])).
% 1.32/1.48  cnf(c308,plain,singleton(skolem0001,skolem0004),inference(resolution,[status(thm)],[c305, c201])).
% 1.32/1.48  cnf(c444,plain,skolem0001!=X933|skolem0004!=X932|singleton(X933,X932),inference(resolution,[status(thm)],[c27, c308])).
% 1.32/1.48  cnf(c1022,plain,skolem0001!=X934|singleton(X934,skolem0004),inference(resolution,[status(thm)],[c444, reflexivity])).
% 1.32/1.48  cnf(c425,plain,nonexistent(skolem0005,skolem0008),inference(resolution,[status(thm)],[c421, c207])).
% 1.32/1.48  cnf(c440,plain,skolem0005!=X930|skolem0008!=X929|nonexistent(X930,X929),inference(resolution,[status(thm)],[c26, c425])).
% 1.32/1.48  cnf(c1020,plain,skolem0005!=X931|nonexistent(X931,skolem0008),inference(resolution,[status(thm)],[c440, reflexivity])).
% 1.32/1.48  cnf(c294,plain,nonexistent(skolem0001,skolem0008),inference(resolution,[status(thm)],[c207, c289])).
% 1.32/1.48  cnf(c439,plain,skolem0001!=X927|skolem0008!=X926|nonexistent(X927,X926),inference(resolution,[status(thm)],[c26, c294])).
% 1.32/1.48  cnf(c1018,plain,skolem0001!=X928|nonexistent(X928,skolem0008),inference(resolution,[status(thm)],[c439, reflexivity])).
% 1.32/1.48  cnf(c304,plain,nonexistent(skolem0001,skolem0004),inference(resolution,[status(thm)],[c298, c207])).
% 1.32/1.48  cnf(c438,plain,skolem0001!=X924|skolem0004!=X923|nonexistent(X924,X923),inference(resolution,[status(thm)],[c26, c304])).
% 1.32/1.48  cnf(c1016,plain,skolem0001!=X925|nonexistent(X925,skolem0004),inference(resolution,[status(thm)],[c438, reflexivity])).
% 1.32/1.48  cnf(c437,plain,skolem0005!=X921|skolem0008!=X920|thing(X921,X920),inference(resolution,[status(thm)],[c428, c11])).
% 1.32/1.48  cnf(c1014,plain,skolem0005!=X922|thing(X922,skolem0008),inference(resolution,[status(thm)],[c437, reflexivity])).
% 1.32/1.48  cnf(c427,plain,specific(skolem0005,skolem0008),inference(resolution,[status(thm)],[c421, c204])).
% 1.32/1.48  cnf(c435,plain,skolem0005!=X917|skolem0008!=X918|specific(X917,X918),inference(resolution,[status(thm)],[c427, c23])).
% 1.32/1.48  cnf(c1012,plain,skolem0005!=X919|specific(X919,skolem0008),inference(resolution,[status(thm)],[c435, reflexivity])).
% 1.32/1.48  cnf(c424,plain,unisex(skolem0005,skolem0008),inference(resolution,[status(thm)],[c421, c210])).
% 1.32/1.48  cnf(c433,plain,skolem0005!=X914|skolem0008!=X915|unisex(X914,X915),inference(resolution,[status(thm)],[c424, c8])).
% 1.32/1.48  cnf(c1010,plain,skolem0005!=X916|unisex(X916,skolem0008),inference(resolution,[status(thm)],[c433, reflexivity])).
% 1.32/1.48  fof(ax24,axiom,(![U]:(![V]:(state(U,V)=>event(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax24)).
% 1.32/1.48  fof(c211,plain,(![U]:(![V]:(~state(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax24])).
% 1.32/1.48  fof(c212,plain,(![X153]:(![X154]:(~state(X153,X154)|event(X153,X154)))),inference(variable_rename,[status(thm)],[c211])).
% 1.32/1.48  cnf(c213,plain,~state(X248,X249)|event(X248,X249),inference(split_conjunct,[status(thm)],[c212])).
% 1.32/1.48  cnf(c423,plain,event(skolem0005,skolem0008),inference(resolution,[status(thm)],[c420, c213])).
% 1.32/1.48  cnf(c431,plain,skolem0005!=X911|skolem0008!=X912|event(X911,X912),inference(resolution,[status(thm)],[c423, c5])).
% 1.32/1.48  cnf(c1008,plain,skolem0005!=X913|event(X913,skolem0008),inference(resolution,[status(thm)],[c431, reflexivity])).
% 1.32/1.48  cnf(c25,axiom,X395!=X394|X393!=X396|~state(X395,X393)|state(X394,X396),theory(equality)).
% 1.32/1.48  cnf(c430,plain,skolem0005!=X909|skolem0008!=X908|state(X909,X908),inference(resolution,[status(thm)],[c25, c420])).
% 1.32/1.48  cnf(c1006,plain,skolem0005!=X910|state(X910,skolem0008),inference(resolution,[status(thm)],[c430, reflexivity])).
% 1.32/1.48  cnf(c429,plain,skolem0001!=X906|skolem0008!=X905|state(X906,X905),inference(resolution,[status(thm)],[c25, c63])).
% 1.32/1.48  cnf(c1004,plain,skolem0001!=X907|state(X907,skolem0008),inference(resolution,[status(thm)],[c429, reflexivity])).
% 1.32/1.48  cnf(c426,plain,skolem0005!=X903|skolem0008!=X902|eventuality(X903,X902),inference(resolution,[status(thm)],[c421, c24])).
% 1.32/1.48  cnf(c1002,plain,skolem0005!=X904|eventuality(X904,skolem0008),inference(resolution,[status(thm)],[c426, reflexivity])).
% 1.32/1.48  cnf(c418,plain,skolem0001!=X900|skolem0004!=X899|eventuality(X900,X899),inference(resolution,[status(thm)],[c24, c298])).
% 1.32/1.48  cnf(c1000,plain,skolem0001!=X901|eventuality(X901,skolem0004),inference(resolution,[status(thm)],[c418, reflexivity])).
% 1.32/1.48  cnf(c417,plain,skolem0001!=X897|skolem0008!=X896|eventuality(X897,X896),inference(resolution,[status(thm)],[c24, c289])).
% 1.32/1.48  cnf(c998,plain,skolem0001!=X898|eventuality(X898,skolem0008),inference(resolution,[status(thm)],[c417, reflexivity])).
% 1.32/1.48  cnf(c415,plain,skolem0001!=X893|skolem0007!=X894|specific(X893,X894),inference(resolution,[status(thm)],[c23, c321])).
% 1.32/1.48  cnf(c996,plain,skolem0001!=X895|specific(X895,skolem0007),inference(resolution,[status(thm)],[c415, reflexivity])).
% 1.32/1.48  cnf(c414,plain,skolem0001!=X890|skolem0002!=X891|specific(X890,X891),inference(resolution,[status(thm)],[c23, c322])).
% 1.32/1.48  cnf(c994,plain,skolem0001!=X892|specific(X892,skolem0002),inference(resolution,[status(thm)],[c414, reflexivity])).
% 1.32/1.48  cnf(c303,plain,specific(skolem0001,skolem0004),inference(resolution,[status(thm)],[c298, c204])).
% 1.32/1.48  cnf(c413,plain,skolem0001!=X887|skolem0004!=X888|specific(X887,X888),inference(resolution,[status(thm)],[c23, c303])).
% 1.32/1.48  cnf(c992,plain,skolem0001!=X889|specific(X889,skolem0004),inference(resolution,[status(thm)],[c413, reflexivity])).
% 1.32/1.48  cnf(c293,plain,specific(skolem0001,skolem0008),inference(resolution,[status(thm)],[c204, c289])).
% 1.32/1.48  cnf(c412,plain,skolem0001!=X884|skolem0008!=X885|specific(X884,X885),inference(resolution,[status(thm)],[c23, c293])).
% 1.32/1.48  cnf(c990,plain,skolem0001!=X886|specific(X886,skolem0008),inference(resolution,[status(thm)],[c412, reflexivity])).
% 1.32/1.48  cnf(c324,plain,existent(skolem0001,skolem0002),inference(resolution,[status(thm)],[c234, c313])).
% 1.32/1.48  cnf(c410,plain,skolem0001!=X882|skolem0002!=X881|existent(X882,X881),inference(resolution,[status(thm)],[c22, c324])).
% 1.32/1.48  cnf(c988,plain,skolem0001!=X883|existent(X883,skolem0002),inference(resolution,[status(thm)],[c410, reflexivity])).
% 1.32/1.48  cnf(c323,plain,existent(skolem0001,skolem0007),inference(resolution,[status(thm)],[c234, c314])).
% 1.32/1.48  cnf(c409,plain,skolem0001!=X879|skolem0007!=X878|existent(X879,X878),inference(resolution,[status(thm)],[c22, c323])).
% 1.32/1.48  cnf(c986,plain,skolem0001!=X880|existent(X880,skolem0007),inference(resolution,[status(thm)],[c409, reflexivity])).
% 1.32/1.48  cnf(c398,plain,general(skolem0001,skolem0005),inference(resolution,[status(thm)],[c393, c267])).
% 1.32/1.48  cnf(c406,plain,skolem0001!=X875|skolem0005!=X876|general(X875,X876),inference(resolution,[status(thm)],[c398, c9])).
% 1.32/1.48  cnf(c984,plain,skolem0001!=X877|general(X877,skolem0005),inference(resolution,[status(thm)],[c406, reflexivity])).
% 1.32/1.48  cnf(c405,plain,skolem0001!=X872|skolem0005!=X873|unisex(X872,X873),inference(resolution,[status(thm)],[c397, c8])).
% 1.32/1.48  cnf(c982,plain,skolem0001!=X874|unisex(X874,skolem0005),inference(resolution,[status(thm)],[c405, reflexivity])).
% 1.32/1.48  cnf(c404,plain,skolem0001!=X870|skolem0002!=X869|entity(X870,X869),inference(resolution,[status(thm)],[c21, c313])).
% 1.32/1.48  cnf(c980,plain,skolem0001!=X871|entity(X871,skolem0002),inference(resolution,[status(thm)],[c404, reflexivity])).
% 1.32/1.48  cnf(c403,plain,skolem0001!=X867|skolem0007!=X866|entity(X867,X866),inference(resolution,[status(thm)],[c21, c314])).
% 1.32/1.48  cnf(c978,plain,skolem0001!=X868|entity(X868,skolem0007),inference(resolution,[status(thm)],[c403, reflexivity])).
% 1.32/1.48  cnf(c396,plain,nonhuman(skolem0001,skolem0005),inference(resolution,[status(thm)],[c393, c264])).
% 1.32/1.48  cnf(c402,plain,skolem0001!=X864|skolem0005!=X863|nonhuman(X864,X863),inference(resolution,[status(thm)],[c396, c10])).
% 1.32/1.48  cnf(c976,plain,skolem0001!=X865|nonhuman(X865,skolem0005),inference(resolution,[status(thm)],[c402, reflexivity])).
% 1.32/1.48  cnf(c401,plain,skolem0001!=X861|skolem0005!=X860|thing(X861,X860),inference(resolution,[status(thm)],[c395, c11])).
% 1.32/1.48  cnf(c974,plain,skolem0001!=X862|thing(X862,skolem0005),inference(resolution,[status(thm)],[c401, reflexivity])).
% 1.32/1.48  cnf(c399,plain,skolem0001!=X857|skolem0005!=X858|abstraction(X857,X858),inference(resolution,[status(thm)],[c393, c7])).
% 1.32/1.48  cnf(c972,plain,skolem0001!=X859|abstraction(X859,skolem0005),inference(resolution,[status(thm)],[c399, reflexivity])).
% 1.32/1.48  cnf(c394,plain,skolem0001!=X854|skolem0005!=X855|relation(X854,X855),inference(resolution,[status(thm)],[c392, c3])).
% 1.32/1.48  cnf(c970,plain,skolem0001!=X856|relation(X856,skolem0005),inference(resolution,[status(thm)],[c394, reflexivity])).
% 1.32/1.48  cnf(c326,plain,impartial(skolem0001,skolem0007),inference(resolution,[status(thm)],[c237, c311])).
% 1.32/1.48  cnf(c391,plain,skolem0001!=X851|skolem0007!=X852|impartial(X851,X852),inference(resolution,[status(thm)],[c20, c326])).
% 1.32/1.48  cnf(c968,plain,skolem0001!=X853|impartial(X853,skolem0007),inference(resolution,[status(thm)],[c391, reflexivity])).
% 1.32/1.48  cnf(c962,plain,~accessible_world(skolem0005,X850)|theme(X850,skolem0004,skolem0005),inference(resolution,[status(thm)],[c961, c170])).
% 1.32/1.48  cnf(c325,plain,impartial(skolem0001,skolem0002),inference(resolution,[status(thm)],[c237, c312])).
% 1.32/1.48  cnf(c390,plain,skolem0001!=X847|skolem0002!=X848|impartial(X847,X848),inference(resolution,[status(thm)],[c20, c325])).
% 1.32/1.48  cnf(c966,plain,skolem0001!=X849|impartial(X849,skolem0002),inference(resolution,[status(thm)],[c390, reflexivity])).
% 1.32/1.48  cnf(c959,plain,~accessible_world(skolem0005,X846)|agent(X846,skolem0004,skolem0002),inference(resolution,[status(thm)],[c955, c164])).
% 1.32/1.48  cnf(c951,plain,~accessible_world(skolem0005,X845)|of(X845,skolem0006,skolem0007),inference(resolution,[status(thm)],[c947, c155])).
% 1.32/1.48  cnf(c946,plain,~accessible_world(skolem0005,X844)|of(X844,skolem0003,skolem0002),inference(resolution,[status(thm)],[c943, c155])).
% 1.32/1.48  cnf(c388,plain,skolem0001!=X841|skolem0006!=X842|unisex(X841,X842),inference(resolution,[status(thm)],[c384, c8])).
% 1.32/1.48  cnf(c964,plain,skolem0001!=X843|unisex(X843,skolem0006),inference(resolution,[status(thm)],[c388, reflexivity])).
% 1.32/1.48  cnf(c387,plain,skolem0001!=X837|skolem0003!=X838|unisex(X837,X838),inference(resolution,[status(thm)],[c383, c8])).
% 1.32/1.48  cnf(c956,plain,skolem0001!=X839|unisex(X839,skolem0003),inference(resolution,[status(thm)],[c387, reflexivity])).
% 1.32/1.48  cnf(c762,plain,~accessible_world(skolem0005,X835)|present(X835,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c161, c595])).
% 1.32/1.48  cnf(c761,plain,~accessible_world(skolem0005,X834)|present(X834,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c161, c666])).
% 1.32/1.48  cnf(c331,plain,living(skolem0001,skolem0002),inference(resolution,[status(thm)],[c240, c312])).
% 1.32/1.48  cnf(c386,plain,skolem0001!=X832|skolem0002!=X831|living(X832,X831),inference(resolution,[status(thm)],[c19, c331])).
% 1.32/1.48  cnf(c953,plain,skolem0001!=X833|living(X833,skolem0002),inference(resolution,[status(thm)],[c386, reflexivity])).
% 1.32/1.48  fof(ax41,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&smoke(V,U))=>smoke(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax41)).
% 1.32/1.48  fof(c156,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~smoke(V,U))|smoke(W,U))))),inference(fof_nnf,[status(thm)],[ax41])).
% 1.32/1.48  fof(c157,plain,(![X110]:(![X111]:(![X112]:((~accessible_world(X111,X112)|~smoke(X111,X110))|smoke(X112,X110))))),inference(variable_rename,[status(thm)],[c156])).
% 1.32/1.48  cnf(c158,plain,~accessible_world(X605,X606)|~smoke(X605,X607)|smoke(X606,X607),inference(split_conjunct,[status(thm)],[c157])).
% 1.32/1.48  cnf(c758,plain,~accessible_world(skolem0005,X830)|smoke(X830,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c158, c594])).
% 1.32/1.48  cnf(c757,plain,~accessible_world(skolem0005,X829)|smoke(X829,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c158, c665])).
% 1.32/1.48  cnf(c332,plain,living(skolem0001,skolem0007),inference(resolution,[status(thm)],[c240, c311])).
% 1.32/1.48  cnf(c385,plain,skolem0001!=X827|skolem0007!=X826|living(X827,X826),inference(resolution,[status(thm)],[c19, c332])).
% 1.32/1.48  cnf(c948,plain,skolem0001!=X828|living(X828,skolem0007),inference(resolution,[status(thm)],[c385, reflexivity])).
% 1.32/1.48  cnf(c376,plain,general(skolem0001,skolem0006),inference(resolution,[status(thm)],[c267, c358])).
% 1.32/1.48  cnf(c381,plain,skolem0001!=X821|skolem0006!=X822|general(X821,X822),inference(resolution,[status(thm)],[c376, c9])).
% 1.32/1.48  cnf(c941,plain,skolem0001!=X823|general(X823,skolem0006),inference(resolution,[status(thm)],[c381, reflexivity])).
% 1.32/1.48  fof(ax64,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&singleton(V,U))=>singleton(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax64)).
% 1.32/1.48  fof(c87,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~singleton(V,U))|singleton(W,U))))),inference(fof_nnf,[status(thm)],[ax64])).
% 1.32/1.48  fof(c88,plain,(![X40]:(![X41]:(![X42]:((~accessible_world(X41,X42)|~singleton(X41,X40))|singleton(X42,X40))))),inference(variable_rename,[status(thm)],[c87])).
% 1.32/1.48  cnf(c89,plain,~accessible_world(X469,X470)|~singleton(X469,X468)|singleton(X470,X468),inference(split_conjunct,[status(thm)],[c88])).
% 1.32/1.48  cnf(c737,plain,~accessible_world(skolem0005,X820)|singleton(X820,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c734, c89])).
% 1.32/1.48  cnf(c733,plain,~accessible_world(skolem0005,X819)|thing(X819,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c722, c86])).
% 1.32/1.48  cnf(c732,plain,~accessible_world(skolem0005,X818)|specific(X818,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c720, c92])).
% 1.32/1.48  cnf(c375,plain,general(skolem0001,skolem0003),inference(resolution,[status(thm)],[c267, c357])).
% 1.32/1.48  cnf(c379,plain,skolem0001!=X815|skolem0003!=X816|general(X815,X816),inference(resolution,[status(thm)],[c375, c9])).
% 1.32/1.48  cnf(c939,plain,skolem0001!=X817|general(X817,skolem0003),inference(resolution,[status(thm)],[c379, reflexivity])).
% 1.32/1.48  fof(ax62,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&nonexistent(V,U))=>nonexistent(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax62)).
% 1.32/1.48  fof(c93,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~nonexistent(V,U))|nonexistent(W,U))))),inference(fof_nnf,[status(thm)],[ax62])).
% 1.32/1.48  fof(c94,plain,(![X46]:(![X47]:(![X48]:((~accessible_world(X47,X48)|~nonexistent(X47,X46))|nonexistent(X48,X46))))),inference(variable_rename,[status(thm)],[c93])).
% 1.32/1.48  cnf(c95,plain,~accessible_world(X506,X508)|~nonexistent(X506,X507)|nonexistent(X508,X507),inference(split_conjunct,[status(thm)],[c94])).
% 1.32/1.48  cnf(c727,plain,~accessible_world(skolem0005,X814)|nonexistent(X814,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c718, c95])).
% 1.32/1.48  cnf(c723,plain,~accessible_world(skolem0005,X813)|unisex(X813,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c717, c98])).
% 1.32/1.48  cnf(c721,plain,~accessible_world(skolem0005,X812)|eventuality(X812,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c716, c83])).
% 1.32/1.48  cnf(c378,plain,skolem0001!=X810|skolem0007!=X809|organism(X810,X809),inference(resolution,[status(thm)],[c18, c311])).
% 1.32/1.48  cnf(c937,plain,skolem0001!=X811|organism(X811,skolem0007),inference(resolution,[status(thm)],[c378, reflexivity])).
% 1.32/1.48  cnf(c714,plain,~accessible_world(skolem0005,X808)|event(X808,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c670, c101])).
% 1.32/1.48  cnf(c662,plain,~accessible_world(skolem0005,X807)|singleton(X807,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c659, c89])).
% 1.32/1.48  cnf(c658,plain,~accessible_world(skolem0005,X806)|thing(X806,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c647, c86])).
% 1.32/1.48  cnf(c377,plain,skolem0001!=X804|skolem0002!=X803|organism(X804,X803),inference(resolution,[status(thm)],[c18, c312])).
% 1.32/1.48  cnf(c935,plain,skolem0001!=X805|organism(X805,skolem0002),inference(resolution,[status(thm)],[c377, reflexivity])).
% 1.32/1.48  cnf(c654,plain,~accessible_world(skolem0005,X802)|specific(X802,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c645, c92])).
% 1.32/1.48  cnf(c652,plain,~accessible_world(skolem0005,X801)|nonexistent(X801,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c643, c95])).
% 1.32/1.48  cnf(c648,plain,~accessible_world(skolem0005,X800)|unisex(X800,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c642, c98])).
% 1.32/1.48  cnf(c372,plain,nonhuman(skolem0001,skolem0006),inference(resolution,[status(thm)],[c264, c358])).
% 1.32/1.48  cnf(c374,plain,skolem0001!=X798|skolem0006!=X797|nonhuman(X798,X797),inference(resolution,[status(thm)],[c372, c10])).
% 1.32/1.48  cnf(c933,plain,skolem0001!=X799|nonhuman(X799,skolem0006),inference(resolution,[status(thm)],[c374, reflexivity])).
% 1.32/1.48  cnf(c646,plain,~accessible_world(skolem0005,X796)|eventuality(X796,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c638, c83])).
% 1.32/1.48  cnf(c636,plain,~accessible_world(skolem0005,X795)|event(X795,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c599, c101])).
% 1.32/1.48  cnf(c371,plain,nonhuman(skolem0001,skolem0003),inference(resolution,[status(thm)],[c264, c357])).
% 1.32/1.48  cnf(c373,plain,skolem0001!=X793|skolem0003!=X792|nonhuman(X793,X792),inference(resolution,[status(thm)],[c371, c10])).
% 1.32/1.48  cnf(c931,plain,skolem0001!=X794|nonhuman(X794,skolem0003),inference(resolution,[status(thm)],[c373, reflexivity])).
% 1.32/1.48  cnf(c333,plain,human(skolem0001,skolem0007),inference(resolution,[status(thm)],[c243, c310])).
% 1.32/1.48  cnf(c370,plain,skolem0001!=X788|skolem0007!=X787|human(X788,X787),inference(resolution,[status(thm)],[c17, c333])).
% 1.32/1.48  cnf(c927,plain,skolem0001!=X791|human(X791,skolem0007),inference(resolution,[status(thm)],[c370, reflexivity])).
% 1.32/1.48  cnf(c334,plain,human(skolem0001,skolem0002),inference(resolution,[status(thm)],[c243, c309])).
% 1.32/1.48  cnf(c369,plain,skolem0001!=X784|skolem0002!=X783|human(X784,X783),inference(resolution,[status(thm)],[c17, c334])).
% 1.32/1.48  cnf(c924,plain,skolem0001!=X790|human(X790,skolem0002),inference(resolution,[status(thm)],[c369, reflexivity])).
% 1.32/1.48  cnf(c368,plain,skolem0001!=X779|skolem0006!=X778|thing(X779,X778),inference(resolution,[status(thm)],[c364, c11])).
% 1.32/1.48  cnf(c920,plain,skolem0001!=X789|thing(X789,skolem0006),inference(resolution,[status(thm)],[c368, reflexivity])).
% 1.32/1.48  cnf(c366,plain,skolem0001!=X775|skolem0003!=X774|thing(X775,X774),inference(resolution,[status(thm)],[c363, c11])).
% 1.32/1.48  cnf(c917,plain,skolem0001!=X786|thing(X786,skolem0003),inference(resolution,[status(thm)],[c366, reflexivity])).
% 1.32/1.48  cnf(c362,plain,skolem0001!=X769|skolem0006!=X770|abstraction(X769,X770),inference(resolution,[status(thm)],[c358, c7])).
% 1.32/1.48  cnf(c913,plain,skolem0001!=X785|abstraction(X785,skolem0006),inference(resolution,[status(thm)],[c362, reflexivity])).
% 1.32/1.48  cnf(c337,plain,animate(skolem0001,skolem0007),inference(resolution,[status(thm)],[c246, c310])).
% 1.32/1.48  cnf(c361,plain,skolem0001!=X765|skolem0007!=X766|animate(X765,X766),inference(resolution,[status(thm)],[c16, c337])).
% 1.32/1.48  cnf(c910,plain,skolem0001!=X782|animate(X782,skolem0007),inference(resolution,[status(thm)],[c361, reflexivity])).
% 1.32/1.48  cnf(c338,plain,animate(skolem0001,skolem0002),inference(resolution,[status(thm)],[c246, c309])).
% 1.32/1.48  cnf(c360,plain,skolem0001!=X759|skolem0002!=X760|animate(X759,X760),inference(resolution,[status(thm)],[c16, c338])).
% 1.32/1.48  cnf(c907,plain,skolem0001!=X781|animate(X781,skolem0002),inference(resolution,[status(thm)],[c360, reflexivity])).
% 1.32/1.48  cnf(c359,plain,skolem0001!=X753|skolem0003!=X754|abstraction(X753,X754),inference(resolution,[status(thm)],[c357, c7])).
% 1.32/1.48  cnf(c905,plain,skolem0001!=X780|abstraction(X780,skolem0003),inference(resolution,[status(thm)],[c359, reflexivity])).
% 1.32/1.48  cnf(c356,plain,skolem0001!=X749|skolem0003!=X750|relation(X749,X750),inference(resolution,[status(thm)],[c354, c3])).
% 1.32/1.48  cnf(c902,plain,skolem0001!=X777|relation(X777,skolem0003),inference(resolution,[status(thm)],[c356, reflexivity])).
% 1.32/1.48  cnf(c355,plain,skolem0001!=X744|skolem0006!=X745|relation(X744,X745),inference(resolution,[status(thm)],[c353, c3])).
% 1.32/1.48  cnf(c898,plain,skolem0001!=X776|relation(X776,skolem0006),inference(resolution,[status(thm)],[c355, reflexivity])).
% 1.32/1.48  cnf(c352,plain,skolem0001!=X739|skolem0002!=X738|human_person(X739,X738),inference(resolution,[status(thm)],[c15, c309])).
% 1.32/1.48  cnf(c896,plain,skolem0001!=X773|human_person(X773,skolem0002),inference(resolution,[status(thm)],[c352, reflexivity])).
% 1.32/1.48  cnf(c351,plain,skolem0001!=X734|skolem0007!=X733|human_person(X734,X733),inference(resolution,[status(thm)],[c15, c310])).
% 1.32/1.48  cnf(c893,plain,skolem0001!=X772|human_person(X772,skolem0007),inference(resolution,[status(thm)],[c351, reflexivity])).
% 1.32/1.48  cnf(c350,plain,skolem0001!=X727|skolem0003!=X728|relname(X727,X728),inference(resolution,[status(thm)],[c348, c12])).
% 1.32/1.48  cnf(c891,plain,skolem0001!=X771|relname(X771,skolem0003),inference(resolution,[status(thm)],[c350, reflexivity])).
% 1.32/1.48  cnf(c349,plain,skolem0001!=X721|skolem0006!=X722|relname(X721,X722),inference(resolution,[status(thm)],[c347, c12])).
% 1.32/1.48  cnf(c889,plain,skolem0001!=X768|relname(X768,skolem0006),inference(resolution,[status(thm)],[c349, reflexivity])).
% 1.32/1.48  cnf(c342,plain,male(skolem0001,skolem0007),inference(resolution,[status(thm)],[c249, c59])).
% 1.32/1.48  cnf(c346,plain,skolem0001!=X715|skolem0007!=X716|male(X715,X716),inference(resolution,[status(thm)],[c14, c342])).
% 1.32/1.48  cnf(c887,plain,skolem0001!=X767|male(X767,skolem0007),inference(resolution,[status(thm)],[c346, reflexivity])).
% 1.32/1.48  cnf(c341,plain,male(skolem0001,skolem0002),inference(resolution,[status(thm)],[c249, c44])).
% 1.32/1.48  cnf(c345,plain,skolem0001!=X709|skolem0002!=X710|male(X709,X710),inference(resolution,[status(thm)],[c14, c341])).
% 1.32/1.48  cnf(c885,plain,skolem0001!=X764|male(X764,skolem0002),inference(resolution,[status(thm)],[c345, reflexivity])).
% 1.32/1.48  cnf(c881,plain,~accessible_world(skolem0005,X763)|vincent_forename(X763,skolem0003),inference(resolution,[status(thm)],[c880, c176])).
% 1.32/1.48  cnf(c340,plain,skolem0001!=X706|skolem0007!=X705|man(X706,X705),inference(resolution,[status(thm)],[c13, c59])).
% 1.32/1.48  cnf(c879,plain,skolem0001!=X762|man(X762,skolem0007),inference(resolution,[status(thm)],[c340, reflexivity])).
% 1.32/1.48  cnf(c878,plain,~accessible_world(skolem0005,X761)|proposition(X761,skolem0005),inference(resolution,[status(thm)],[c875, c173])).
% 1.32/1.48  cnf(c874,plain,~accessible_world(skolem0005,X758)|think_believe_consider(X758,skolem0004),inference(resolution,[status(thm)],[c872, c167])).
% 1.32/1.48  cnf(c339,plain,skolem0001!=X702|skolem0002!=X701|man(X702,X701),inference(resolution,[status(thm)],[c13, c44])).
% 1.32/1.48  cnf(c871,plain,skolem0001!=X757|man(X757,skolem0002),inference(resolution,[status(thm)],[c339, reflexivity])).
% 1.32/1.48  cnf(c870,plain,~accessible_world(skolem0005,X756)|present(X756,skolem0004),inference(resolution,[status(thm)],[c868, c161])).
% 1.32/1.48  cnf(c867,plain,~accessible_world(skolem0005,X755)|jules_forename(X755,skolem0006),inference(resolution,[status(thm)],[c864, c152])).
% 1.32/1.48  cnf(c330,plain,skolem0001!=X698|skolem0004!=X697|thing(X698,X697),inference(resolution,[status(thm)],[c11, c305])).
% 1.32/1.48  cnf(c863,plain,skolem0001!=X752|thing(X752,skolem0004),inference(resolution,[status(thm)],[c330, reflexivity])).
% 1.32/1.48  cnf(c329,plain,skolem0001!=X694|skolem0002!=X693|thing(X694,X693),inference(resolution,[status(thm)],[c11, c318])).
% 1.32/1.48  cnf(c860,plain,skolem0001!=X751|thing(X751,skolem0002),inference(resolution,[status(thm)],[c329, reflexivity])).
% 1.32/1.48  cnf(c328,plain,skolem0001!=X689|skolem0007!=X688|thing(X689,X688),inference(resolution,[status(thm)],[c11, c317])).
% 1.32/1.48  cnf(c856,plain,skolem0001!=X748|thing(X748,skolem0007),inference(resolution,[status(thm)],[c328, reflexivity])).
% 1.32/1.48  cnf(c327,plain,skolem0001!=X685|skolem0008!=X684|thing(X685,X684),inference(resolution,[status(thm)],[c11, c291])).
% 1.32/1.48  cnf(c853,plain,skolem0001!=X747|thing(X747,skolem0008),inference(resolution,[status(thm)],[c327, reflexivity])).
% 1.32/1.48  cnf(c302,plain,unisex(skolem0001,skolem0004),inference(resolution,[status(thm)],[c298, c210])).
% 1.32/1.48  cnf(c316,plain,skolem0001!=X679|skolem0004!=X680|unisex(X679,X680),inference(resolution,[status(thm)],[c8, c302])).
% 1.32/1.48  cnf(c849,plain,skolem0001!=X746|unisex(X746,skolem0004),inference(resolution,[status(thm)],[c316, reflexivity])).
% 1.32/1.48  fof(ax44,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&general(V,U))=>general(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax44)).
% 1.32/1.48  fof(c147,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~general(V,U))|general(W,U))))),inference(fof_nnf,[status(thm)],[ax44])).
% 1.32/1.48  fof(c148,plain,(![X100]:(![X101]:(![X102]:((~accessible_world(X101,X102)|~general(X101,X100))|general(X102,X100))))),inference(variable_rename,[status(thm)],[c147])).
% 1.32/1.48  cnf(c149,plain,~accessible_world(X587,X586)|~general(X587,X588)|general(X586,X588),inference(split_conjunct,[status(thm)],[c148])).
% 1.32/1.48  cnf(c846,plain,~accessible_world(skolem0005,X743)|general(X743,skolem0005),inference(resolution,[status(thm)],[c839, c149])).
% 1.32/1.48  cnf(c296,plain,unisex(skolem0001,skolem0008),inference(resolution,[status(thm)],[c210, c289])).
% 1.32/1.48  cnf(c315,plain,skolem0001!=X676|skolem0008!=X677|unisex(X676,X677),inference(resolution,[status(thm)],[c8, c296])).
% 1.32/1.48  cnf(c844,plain,skolem0001!=X742|unisex(X742,skolem0008),inference(resolution,[status(thm)],[c315, reflexivity])).
% 1.32/1.48  fof(ax45,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&nonhuman(V,U))=>nonhuman(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax45)).
% 1.32/1.48  fof(c144,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~nonhuman(V,U))|nonhuman(W,U))))),inference(fof_nnf,[status(thm)],[ax45])).
% 1.32/1.48  fof(c145,plain,(![X97]:(![X98]:(![X99]:((~accessible_world(X98,X99)|~nonhuman(X98,X97))|nonhuman(X99,X97))))),inference(variable_rename,[status(thm)],[c144])).
% 1.32/1.48  cnf(c146,plain,~accessible_world(X581,X580)|~nonhuman(X581,X582)|nonhuman(X580,X582),inference(split_conjunct,[status(thm)],[c145])).
% 1.32/1.48  cnf(c843,plain,~accessible_world(skolem0005,X741)|nonhuman(X741,skolem0005),inference(resolution,[status(thm)],[c837, c146])).
% 1.32/1.48  fof(ax46,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&abstraction(V,U))=>abstraction(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax46)).
% 1.32/1.48  fof(c141,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~abstraction(V,U))|abstraction(W,U))))),inference(fof_nnf,[status(thm)],[ax46])).
% 1.32/1.48  fof(c142,plain,(![X94]:(![X95]:(![X96]:((~accessible_world(X95,X96)|~abstraction(X95,X94))|abstraction(X96,X94))))),inference(variable_rename,[status(thm)],[c141])).
% 1.32/1.48  cnf(c143,plain,~accessible_world(X577,X578)|~abstraction(X577,X576)|abstraction(X578,X576),inference(split_conjunct,[status(thm)],[c142])).
% 1.32/1.48  cnf(c840,plain,~accessible_world(skolem0005,X740)|abstraction(X740,skolem0005),inference(resolution,[status(thm)],[c833, c143])).
% 1.32/1.48  cnf(c834,plain,~accessible_world(skolem0005,X737)|relation(X737,skolem0005),inference(resolution,[status(thm)],[c832, c140])).
% 1.32/1.48  cnf(c307,plain,skolem0001!=X674|skolem0006!=X673|jules_forename(X674,X673),inference(resolution,[status(thm)],[c6, c60])).
% 1.32/1.48  cnf(c831,plain,skolem0001!=X736|jules_forename(X736,skolem0006),inference(resolution,[status(thm)],[c307, reflexivity])).
% 1.32/1.48  cnf(c297,plain,event(skolem0001,skolem0008),inference(resolution,[status(thm)],[c213, c63])).
% 1.32/1.48  cnf(c301,plain,skolem0001!=X668|skolem0008!=X669|event(X668,X669),inference(resolution,[status(thm)],[c5, c297])).
% 1.32/1.48  cnf(c828,plain,skolem0001!=X735|event(X735,skolem0008),inference(resolution,[status(thm)],[c301, reflexivity])).
% 1.32/1.48  cnf(c300,plain,skolem0001!=X662|skolem0004!=X663|event(X662,X663),inference(resolution,[status(thm)],[c5, c50])).
% 1.32/1.48  cnf(c827,plain,skolem0001!=X732|event(X732,skolem0004),inference(resolution,[status(thm)],[c300, reflexivity])).
% 1.32/1.48  cnf(c825,plain,~accessible_world(skolem0005,X731)|general(X731,skolem0003),inference(resolution,[status(thm)],[c819, c149])).
% 1.32/1.48  cnf(c823,plain,~accessible_world(skolem0005,X730)|nonhuman(X730,skolem0003),inference(resolution,[status(thm)],[c817, c146])).
% 1.32/1.48  cnf(c820,plain,~accessible_world(skolem0005,X729)|abstraction(X729,skolem0003),inference(resolution,[status(thm)],[c812, c143])).
% 1.32/1.48  cnf(c290,plain,skolem0001!=X660|skolem0005!=X661|proposition(X660,X661),inference(resolution,[status(thm)],[c2, c47])).
% 1.32/1.48  cnf(c815,plain,skolem0001!=X726|proposition(X726,skolem0005),inference(resolution,[status(thm)],[c290, reflexivity])).
% 1.32/1.48  cnf(c813,plain,~accessible_world(skolem0005,X725)|relation(X725,skolem0003),inference(resolution,[status(thm)],[c809, c140])).
% 1.32/1.48  fof(ax48,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&relname(V,U))=>relname(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax48)).
% 1.32/1.48  fof(c135,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~relname(V,U))|relname(W,U))))),inference(fof_nnf,[status(thm)],[ax48])).
% 1.32/1.48  fof(c136,plain,(![X88]:(![X89]:(![X90]:((~accessible_world(X89,X90)|~relname(X89,X88))|relname(X90,X88))))),inference(variable_rename,[status(thm)],[c135])).
% 1.32/1.48  cnf(c137,plain,~accessible_world(X572,X570)|~relname(X572,X571)|relname(X570,X571),inference(split_conjunct,[status(thm)],[c136])).
% 1.32/1.48  cnf(c811,plain,~accessible_world(skolem0005,X724)|relname(X724,skolem0003),inference(resolution,[status(thm)],[c808, c137])).
% 1.32/1.48  cnf(c807,plain,~accessible_world(skolem0005,X723)|forename(X723,skolem0003),inference(resolution,[status(thm)],[c805, c134])).
% 1.32/1.48  cnf(c288,plain,skolem0001!=X658|skolem0003!=X657|forename(X658,X657),inference(resolution,[status(thm)],[c1, c46])).
% 1.32/1.48  cnf(c804,plain,skolem0001!=X720|forename(X720,skolem0003),inference(resolution,[status(thm)],[c288, reflexivity])).
% 1.32/1.48  cnf(c802,plain,~accessible_world(skolem0005,X719)|general(X719,skolem0006),inference(resolution,[status(thm)],[c796, c149])).
% 1.32/1.48  cnf(c800,plain,~accessible_world(skolem0005,X718)|nonhuman(X718,skolem0006),inference(resolution,[status(thm)],[c794, c146])).
% 1.32/1.48  cnf(c797,plain,~accessible_world(skolem0005,X717)|abstraction(X717,skolem0006),inference(resolution,[status(thm)],[c789, c143])).
% 1.32/1.48  cnf(c287,plain,skolem0001!=X656|skolem0006!=X655|forename(X656,X655),inference(resolution,[status(thm)],[c1, c61])).
% 1.32/1.48  cnf(c792,plain,skolem0001!=X714|forename(X714,skolem0006),inference(resolution,[status(thm)],[c287, reflexivity])).
% 1.32/1.48  cnf(c790,plain,~accessible_world(skolem0005,X713)|relation(X713,skolem0006),inference(resolution,[status(thm)],[c786, c140])).
% 1.32/1.48  cnf(c788,plain,~accessible_world(skolem0005,X712)|relname(X712,skolem0006),inference(resolution,[status(thm)],[c785, c137])).
% 1.32/1.48  cnf(c784,plain,~accessible_world(skolem0005,X711)|forename(X711,skolem0006),inference(resolution,[status(thm)],[c782, c134])).
% 1.32/1.48  cnf(c286,plain,skolem0001!=X651|skolem0003!=X652|vincent_forename(X651,X652),inference(resolution,[status(thm)],[c0, c45])).
% 1.32/1.48  cnf(c781,plain,skolem0001!=X708|vincent_forename(X708,skolem0003),inference(resolution,[status(thm)],[c286, reflexivity])).
% 1.32/1.49  cnf(c745,plain,~accessible_world(skolem0001,X696)|general(X696,skolem0005),inference(resolution,[status(thm)],[c149, c398])).
% 1.32/1.49  cnf(c744,plain,~accessible_world(skolem0001,X695)|general(X695,skolem0006),inference(resolution,[status(thm)],[c149, c376])).
% 1.32/1.49  cnf(c743,plain,~accessible_world(skolem0001,X692)|general(X692,skolem0003),inference(resolution,[status(thm)],[c149, c375])).
% 1.32/1.49  cnf(c740,plain,~accessible_world(skolem0001,X691)|nonhuman(X691,skolem0003),inference(resolution,[status(thm)],[c146, c371])).
% 1.32/1.49  cnf(c739,plain,~accessible_world(skolem0001,X690)|nonhuman(X690,skolem0006),inference(resolution,[status(thm)],[c146, c372])).
% 1.32/1.49  cnf(c738,plain,~accessible_world(skolem0001,X687)|nonhuman(X687,skolem0005),inference(resolution,[status(thm)],[c146, c396])).
% 1.32/1.49  cnf(c730,plain,~accessible_world(skolem0001,X686)|abstraction(X686,skolem0006),inference(resolution,[status(thm)],[c143, c358])).
% 1.32/1.49  cnf(c729,plain,~accessible_world(skolem0001,X683)|abstraction(X683,skolem0005),inference(resolution,[status(thm)],[c143, c393])).
% 1.32/1.49  cnf(c728,plain,~accessible_world(skolem0001,X682)|abstraction(X682,skolem0003),inference(resolution,[status(thm)],[c143, c357])).
% 1.32/1.49  cnf(c713,plain,~accessible_world(skolem0001,X681)|relation(X681,skolem0006),inference(resolution,[status(thm)],[c140, c353])).
% 1.32/1.49  cnf(c712,plain,~accessible_world(skolem0001,X678)|relation(X678,skolem0003),inference(resolution,[status(thm)],[c140, c354])).
% 1.32/1.49  fof(ax33,axiom,(![U]:(![V]:(specific(U,V)=>(~general(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax33)).
% 1.32/1.49  fof(c181,plain,(![U]:(![V]:(specific(U,V)=>~general(U,V)))),inference(fof_simplification,[status(thm)],[ax33])).
% 1.32/1.49  fof(c182,plain,(![U]:(![V]:(~specific(U,V)|~general(U,V)))),inference(fof_nnf,[status(thm)],[c181])).
% 1.32/1.49  fof(c183,plain,(![X135]:(![X136]:(~specific(X135,X136)|~general(X135,X136)))),inference(variable_rename,[status(thm)],[c182])).
% 1.32/1.49  cnf(c184,plain,~specific(X219,X218)|~general(X219,X218),inference(split_conjunct,[status(thm)],[c183])).
% 1.32/1.49  cnf(c847,plain,~specific(skolem0005,skolem0005),inference(resolution,[status(thm)],[c839, c184])).
% 1.32/1.49  fof(ax55,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&existent(V,U))=>existent(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax55)).
% 1.32/1.49  fof(c114,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~existent(V,U))|existent(W,U))))),inference(fof_nnf,[status(thm)],[ax55])).
% 1.32/1.49  fof(c115,plain,(![X67]:(![X68]:(![X69]:((~accessible_world(X68,X69)|~existent(X68,X67))|existent(X69,X67))))),inference(variable_rename,[status(thm)],[c114])).
% 1.32/1.49  cnf(c116,plain,~accessible_world(X549,X548)|~existent(X549,X550)|existent(X548,X550),inference(split_conjunct,[status(thm)],[c115])).
% 1.32/1.49  cnf(c706,plain,~accessible_world(skolem0005,X672)|existent(X672,skolem0007),inference(resolution,[status(thm)],[c697, c116])).
% 1.32/1.49  cnf(c705,plain,~accessible_world(skolem0001,X671)|relname(X671,skolem0003),inference(resolution,[status(thm)],[c137, c348])).
% 1.32/1.49  cnf(c704,plain,~accessible_world(skolem0001,X670)|relname(X670,skolem0006),inference(resolution,[status(thm)],[c137, c347])).
% 1.32/1.49  fof(ax54,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&impartial(V,U))=>impartial(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax54)).
% 1.32/1.49  fof(c117,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~impartial(V,U))|impartial(W,U))))),inference(fof_nnf,[status(thm)],[ax54])).
% 1.32/1.49  fof(c118,plain,(![X70]:(![X71]:(![X72]:((~accessible_world(X71,X72)|~impartial(X71,X70))|impartial(X72,X70))))),inference(variable_rename,[status(thm)],[c117])).
% 1.32/1.49  cnf(c119,plain,~accessible_world(X553,X552)|~impartial(X553,X551)|impartial(X552,X551),inference(split_conjunct,[status(thm)],[c118])).
% 1.32/1.49  cnf(c703,plain,~accessible_world(skolem0005,X667)|impartial(X667,skolem0007),inference(resolution,[status(thm)],[c687, c119])).
% 1.32/1.49  fof(ax56,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&entity(V,U))=>entity(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax56)).
% 1.32/1.49  fof(c111,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~entity(V,U))|entity(W,U))))),inference(fof_nnf,[status(thm)],[ax56])).
% 1.32/1.49  fof(c112,plain,(![X64]:(![X65]:(![X66]:((~accessible_world(X65,X66)|~entity(X65,X64))|entity(X66,X64))))),inference(variable_rename,[status(thm)],[c111])).
% 1.32/1.49  cnf(c113,plain,~accessible_world(X545,X543)|~entity(X545,X544)|entity(X543,X544),inference(split_conjunct,[status(thm)],[c112])).
% 1.32/1.49  cnf(c698,plain,~accessible_world(skolem0005,X666)|entity(X666,skolem0007),inference(resolution,[status(thm)],[c686, c113])).
% 1.32/1.49  fof(ax53,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&living(V,U))=>living(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax53)).
% 1.32/1.49  fof(c120,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~living(V,U))|living(W,U))))),inference(fof_nnf,[status(thm)],[ax53])).
% 1.32/1.49  fof(c121,plain,(![X73]:(![X74]:(![X75]:((~accessible_world(X74,X75)|~living(X74,X73))|living(X75,X73))))),inference(variable_rename,[status(thm)],[c120])).
% 1.32/1.49  cnf(c122,plain,~accessible_world(X554,X556)|~living(X554,X555)|living(X556,X555),inference(split_conjunct,[status(thm)],[c121])).
% 1.32/1.49  cnf(c695,plain,~accessible_world(skolem0005,X665)|living(X665,skolem0007),inference(resolution,[status(thm)],[c684, c122])).
% 1.32/1.49  fof(ax51,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&animate(V,U))=>animate(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax51)).
% 1.32/1.49  fof(c126,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~animate(V,U))|animate(W,U))))),inference(fof_nnf,[status(thm)],[ax51])).
% 1.32/1.49  fof(c127,plain,(![X79]:(![X80]:(![X81]:((~accessible_world(X80,X81)|~animate(X80,X79))|animate(X81,X79))))),inference(variable_rename,[status(thm)],[c126])).
% 1.32/1.49  cnf(c128,plain,~accessible_world(X561,X562)|~animate(X561,X560)|animate(X562,X560),inference(split_conjunct,[status(thm)],[c127])).
% 1.32/1.49  cnf(c693,plain,~accessible_world(skolem0005,X664)|animate(X664,skolem0007),inference(resolution,[status(thm)],[c680, c128])).
% 1.32/1.49  cnf(c826,plain,~specific(skolem0005,skolem0003),inference(resolution,[status(thm)],[c819, c184])).
% 1.32/1.49  cnf(c803,plain,~specific(skolem0005,skolem0006),inference(resolution,[status(thm)],[c796, c184])).
% 1.32/1.49  fof(ax52,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&human(V,U))=>human(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax52)).
% 1.32/1.49  fof(c123,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~human(V,U))|human(W,U))))),inference(fof_nnf,[status(thm)],[ax52])).
% 1.32/1.49  fof(c124,plain,(![X76]:(![X77]:(![X78]:((~accessible_world(X77,X78)|~human(X77,X76))|human(X78,X76))))),inference(variable_rename,[status(thm)],[c123])).
% 1.32/1.49  cnf(c125,plain,~accessible_world(X557,X558)|~human(X557,X559)|human(X558,X559),inference(split_conjunct,[status(thm)],[c124])).
% 1.32/1.49  cnf(c689,plain,~accessible_world(skolem0005,X653)|human(X653,skolem0007),inference(resolution,[status(thm)],[c679, c125])).
% 1.32/1.49  fof(ax57,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&organism(V,U))=>organism(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax57)).
% 1.32/1.49  fof(c108,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~organism(V,U))|organism(W,U))))),inference(fof_nnf,[status(thm)],[ax57])).
% 1.32/1.49  fof(c109,plain,(![X61]:(![X62]:(![X63]:((~accessible_world(X62,X63)|~organism(X62,X61))|organism(X63,X61))))),inference(variable_rename,[status(thm)],[c108])).
% 1.32/1.49  cnf(c110,plain,~accessible_world(X539,X537)|~organism(X539,X538)|organism(X537,X538),inference(split_conjunct,[status(thm)],[c109])).
% 1.32/1.49  cnf(c683,plain,~accessible_world(skolem0005,X650)|organism(X650,skolem0007),inference(resolution,[status(thm)],[c678, c110])).
% 1.32/1.49  fof(ax58,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&human_person(V,U))=>human_person(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax58)).
% 1.32/1.49  fof(c105,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~human_person(V,U))|human_person(W,U))))),inference(fof_nnf,[status(thm)],[ax58])).
% 1.32/1.49  fof(c106,plain,(![X58]:(![X59]:(![X60]:((~accessible_world(X59,X60)|~human_person(X59,X58))|human_person(X60,X58))))),inference(variable_rename,[status(thm)],[c105])).
% 1.32/1.49  cnf(c107,plain,~accessible_world(X533,X531)|~human_person(X533,X532)|human_person(X531,X532),inference(split_conjunct,[status(thm)],[c106])).
% 1.32/1.49  cnf(c681,plain,~accessible_world(skolem0005,X649)|human_person(X649,skolem0007),inference(resolution,[status(thm)],[c671, c107])).
% 1.32/1.49  fof(ax50,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&male(V,U))=>male(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax50)).
% 1.32/1.49  fof(c129,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~male(V,U))|male(W,U))))),inference(fof_nnf,[status(thm)],[ax50])).
% 1.32/1.49  fof(c130,plain,(![X82]:(![X83]:(![X84]:((~accessible_world(X83,X84)|~male(X83,X82))|male(X84,X82))))),inference(variable_rename,[status(thm)],[c129])).
% 1.32/1.49  cnf(c131,plain,~accessible_world(X564,X565)|~male(X564,X566)|male(X565,X566),inference(split_conjunct,[status(thm)],[c130])).
% 1.32/1.49  cnf(c677,plain,~accessible_world(skolem0005,X648)|male(X648,skolem0007),inference(resolution,[status(thm)],[c668, c131])).
% 1.32/1.49  cnf(c674,plain,~accessible_world(skolem0001,X647)|male(X647,skolem0007),inference(resolution,[status(thm)],[c131, c342])).
% 1.32/1.49  cnf(c673,plain,~accessible_world(skolem0005,X643)|male(X643,skolem0002),inference(resolution,[status(thm)],[c131, c597])).
% 1.32/1.49  cnf(c672,plain,~accessible_world(skolem0001,X642)|male(X642,skolem0002),inference(resolution,[status(thm)],[c131, c341])).
% 1.32/1.49  cnf(c669,plain,~accessible_world(skolem0005,X641)|man(X641,skolem0007),inference(resolution,[status(thm)],[c663, c104])).
% 1.32/1.49  cnf(c657,plain,~accessible_world(skolem0001,X637)|animate(X637,skolem0007),inference(resolution,[status(thm)],[c128, c337])).
% 1.32/1.49  cnf(c656,plain,~accessible_world(skolem0001,X636)|animate(X636,skolem0002),inference(resolution,[status(thm)],[c128, c338])).
% 1.32/1.49  cnf(c655,plain,~accessible_world(skolem0005,X635)|animate(X635,skolem0002),inference(resolution,[status(thm)],[c128, c607])).
% 1.32/1.49  cnf(c641,plain,~accessible_world(skolem0005,X630)|human(X630,skolem0002),inference(resolution,[status(thm)],[c125, c606])).
% 1.32/1.49  cnf(c640,plain,~accessible_world(skolem0001,X629)|human(X629,skolem0007),inference(resolution,[status(thm)],[c125, c333])).
% 1.32/1.49  cnf(c639,plain,~accessible_world(skolem0001,X628)|human(X628,skolem0002),inference(resolution,[status(thm)],[c125, c334])).
% 1.32/1.49  cnf(c632,plain,~accessible_world(skolem0001,X624)|living(X624,skolem0002),inference(resolution,[status(thm)],[c122, c331])).
% 1.32/1.49  cnf(c631,plain,~accessible_world(skolem0005,X623)|living(X623,skolem0002),inference(resolution,[status(thm)],[c122, c611])).
% 1.32/1.49  cnf(c630,plain,~accessible_world(skolem0001,X622)|living(X622,skolem0007),inference(resolution,[status(thm)],[c122, c332])).
% 1.32/1.49  cnf(c628,plain,~accessible_world(skolem0005,X617)|existent(X617,skolem0002),inference(resolution,[status(thm)],[c621, c116])).
% 1.32/1.49  cnf(c627,plain,~accessible_world(skolem0005,X616)|impartial(X616,skolem0002),inference(resolution,[status(thm)],[c614, c119])).
% 1.32/1.49  cnf(c622,plain,~accessible_world(skolem0005,X615)|entity(X615,skolem0002),inference(resolution,[status(thm)],[c613, c113])).
% 1.32/1.49  cnf(c619,plain,~accessible_world(skolem0001,X614)|impartial(X614,skolem0007),inference(resolution,[status(thm)],[c119, c326])).
% 1.32/1.49  cnf(c618,plain,~accessible_world(skolem0001,X610)|impartial(X610,skolem0002),inference(resolution,[status(thm)],[c119, c325])).
% 1.32/1.49  cnf(c610,plain,~accessible_world(skolem0005,X609)|organism(X609,skolem0002),inference(resolution,[status(thm)],[c605, c110])).
% 1.32/1.49  cnf(c608,plain,~accessible_world(skolem0005,X608)|human_person(X608,skolem0002),inference(resolution,[status(thm)],[c600, c107])).
% 1.32/1.49  cnf(c604,plain,~accessible_world(skolem0001,X604)|existent(X604,skolem0002),inference(resolution,[status(thm)],[c116, c324])).
% 1.32/1.49  cnf(c603,plain,~accessible_world(skolem0001,X603)|existent(X603,skolem0007),inference(resolution,[status(thm)],[c116, c323])).
% 1.32/1.49  cnf(c598,plain,~accessible_world(skolem0005,X602)|man(X602,skolem0002),inference(resolution,[status(thm)],[c592, c104])).
% 1.32/1.49  cnf(c590,plain,~accessible_world(skolem0001,X597)|entity(X597,skolem0002),inference(resolution,[status(thm)],[c113, c313])).
% 1.32/1.49  cnf(c589,plain,~accessible_world(skolem0001,X596)|entity(X596,skolem0007),inference(resolution,[status(thm)],[c113, c314])).
% 1.32/1.49  cnf(c586,plain,~accessible_world(skolem0005,X595)|event(X595,skolem0004),inference(resolution,[status(thm)],[c585, c101])).
% 1.32/1.49  cnf(c584,plain,~accessible_world(skolem0001,X591)|organism(X591,skolem0007),inference(resolution,[status(thm)],[c110, c311])).
% 1.32/1.49  cnf(c583,plain,~accessible_world(skolem0001,X590)|organism(X590,skolem0002),inference(resolution,[status(thm)],[c110, c312])).
% 1.32/1.49  cnf(c582,plain,~accessible_world(skolem0005,X589)|unisex(X589,skolem0005),inference(resolution,[status(thm)],[c580, c98])).
% 1.32/1.49  cnf(c579,plain,~accessible_world(skolem0005,X585)|unisex(X585,skolem0006),inference(resolution,[status(thm)],[c577, c98])).
% 1.32/1.49  cnf(c576,plain,~accessible_world(skolem0001,X584)|human_person(X584,skolem0002),inference(resolution,[status(thm)],[c107, c309])).
% 1.32/1.49  cnf(c575,plain,~accessible_world(skolem0001,X583)|human_person(X583,skolem0007),inference(resolution,[status(thm)],[c107, c310])).
% 1.32/1.49  cnf(c574,plain,~accessible_world(skolem0005,X579)|unisex(X579,skolem0003),inference(resolution,[status(thm)],[c572, c98])).
% 1.32/1.49  fof(ax31,axiom,(![U]:(![V]:(existent(U,V)=>(~nonexistent(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax31)).
% 1.32/1.49  fof(c189,plain,(![U]:(![V]:(existent(U,V)=>~nonexistent(U,V)))),inference(fof_simplification,[status(thm)],[ax31])).
% 1.32/1.49  fof(c190,plain,(![U]:(![V]:(~existent(U,V)|~nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[c189])).
% 1.32/1.49  fof(c191,plain,(![X139]:(![X140]:(~existent(X139,X140)|~nonexistent(X139,X140)))),inference(variable_rename,[status(thm)],[c190])).
% 1.32/1.49  cnf(c192,plain,~existent(X222,X223)|~nonexistent(X222,X223),inference(split_conjunct,[status(thm)],[c191])).
% 1.32/1.49  cnf(c726,plain,~existent(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c718, c192])).
% 1.32/1.49  fof(ax32,axiom,(![U]:(![V]:(nonhuman(U,V)=>(~human(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax32)).
% 1.32/1.49  fof(c185,plain,(![U]:(![V]:(nonhuman(U,V)=>~human(U,V)))),inference(fof_simplification,[status(thm)],[ax32])).
% 1.32/1.49  fof(c186,plain,(![U]:(![V]:(~nonhuman(U,V)|~human(U,V)))),inference(fof_nnf,[status(thm)],[c185])).
% 1.32/1.49  fof(c187,plain,(![X137]:(![X138]:(~nonhuman(X137,X138)|~human(X137,X138)))),inference(variable_rename,[status(thm)],[c186])).
% 1.32/1.49  cnf(c188,plain,~nonhuman(X221,X220)|~human(X221,X220),inference(split_conjunct,[status(thm)],[c187])).
% 1.32/1.49  cnf(c690,plain,~nonhuman(skolem0005,skolem0007),inference(resolution,[status(thm)],[c679, c188])).
% 1.32/1.49  fof(ax34,axiom,(![U]:(![V]:(unisex(U,V)=>(~male(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax34)).
% 1.32/1.49  fof(c177,plain,(![U]:(![V]:(unisex(U,V)=>~male(U,V)))),inference(fof_simplification,[status(thm)],[ax34])).
% 1.32/1.49  fof(c178,plain,(![U]:(![V]:(~unisex(U,V)|~male(U,V)))),inference(fof_nnf,[status(thm)],[c177])).
% 1.32/1.49  fof(c179,plain,(![X133]:(![X134]:(~unisex(X133,X134)|~male(X133,X134)))),inference(variable_rename,[status(thm)],[c178])).
% 1.32/1.49  cnf(c180,plain,~unisex(X216,X217)|~male(X216,X217),inference(split_conjunct,[status(thm)],[c179])).
% 1.32/1.49  cnf(c676,plain,~unisex(skolem0005,skolem0007),inference(resolution,[status(thm)],[c668, c180])).
% 1.32/1.49  cnf(c651,plain,~existent(skolem0005,skolem0009(skolem0002)),inference(resolution,[status(thm)],[c643, c192])).
% 1.32/1.49  cnf(c616,plain,~nonhuman(skolem0005,skolem0002),inference(resolution,[status(thm)],[c606, c188])).
% 1.32/1.49  cnf(c602,plain,~unisex(skolem0005,skolem0002),inference(resolution,[status(thm)],[c597, c180])).
% 1.32/1.49  cnf(c566,plain,~accessible_world(skolem0001,X546)|event(X546,skolem0008),inference(resolution,[status(thm)],[c101, c297])).
% 1.32/1.49  cnf(c564,plain,~accessible_world(skolem0005,X541)|event(X541,skolem0008),inference(resolution,[status(thm)],[c101, c423])).
% 1.32/1.49  cnf(c562,plain,~accessible_world(skolem0005,X540)|unisex(X540,skolem0008),inference(resolution,[status(thm)],[c98, c424])).
% 1.32/1.49  cnf(c559,plain,~accessible_world(skolem0005,X534)|unisex(X534,skolem0004),inference(resolution,[status(thm)],[c98, c454])).
% 1.32/1.49  cnf(c557,plain,~accessible_world(skolem0001,X529)|unisex(X529,skolem0004),inference(resolution,[status(thm)],[c98, c302])).
% 1.32/1.49  cnf(c556,plain,~accessible_world(skolem0001,X525)|unisex(X525,skolem0008),inference(resolution,[status(thm)],[c98, c296])).
% 1.32/1.49  cnf(c553,plain,~accessible_world(skolem0005,X524)|nonexistent(X524,skolem0004),inference(resolution,[status(thm)],[c95, c455])).
% 1.32/1.49  cnf(c552,plain,~accessible_world(skolem0005,X523)|nonexistent(X523,skolem0008),inference(resolution,[status(thm)],[c95, c425])).
% 1.32/1.49  cnf(c551,plain,~accessible_world(skolem0001,X522)|nonexistent(X522,skolem0008),inference(resolution,[status(thm)],[c95, c294])).
% 1.32/1.49  cnf(c550,plain,~accessible_world(skolem0001,X518)|nonexistent(X518,skolem0004),inference(resolution,[status(thm)],[c95, c304])).
% 1.32/1.49  cnf(c549,plain,~accessible_world(skolem0005,X517)|specific(X517,skolem0002),inference(resolution,[status(thm)],[c547, c92])).
% 1.32/1.49  cnf(c546,plain,~accessible_world(skolem0005,X516)|specific(X516,skolem0007),inference(resolution,[status(thm)],[c544, c92])).
% 1.32/1.49  cnf(c543,plain,~accessible_world(skolem0005,X515)|specific(X515,skolem0008),inference(resolution,[status(thm)],[c92, c427])).
% 1.32/1.49  cnf(c542,plain,~accessible_world(skolem0001,X511)|specific(X511,skolem0004),inference(resolution,[status(thm)],[c92, c303])).
% 1.32/1.49  cnf(c541,plain,~accessible_world(skolem0001,X510)|specific(X510,skolem0008),inference(resolution,[status(thm)],[c92, c293])).
% 1.32/1.49  cnf(c540,plain,~accessible_world(skolem0005,X509)|specific(X509,skolem0004),inference(resolution,[status(thm)],[c92, c457])).
% 1.32/1.49  cnf(c524,plain,~accessible_world(skolem0001,X500)|singleton(X500,skolem0002),inference(resolution,[status(thm)],[c89, c320])).
% 1.32/1.49  cnf(c523,plain,~accessible_world(skolem0005,X499)|singleton(X499,skolem0007),inference(resolution,[status(thm)],[c89, c480])).
% 1.32/1.49  cnf(c522,plain,~accessible_world(skolem0001,X498)|singleton(X498,skolem0008),inference(resolution,[status(thm)],[c89, c292])).
% 1.32/1.49  cnf(c521,plain,~accessible_world(skolem0005,X497)|singleton(X497,skolem0004),inference(resolution,[status(thm)],[c89, c465])).
% 1.32/1.49  cnf(c520,plain,~accessible_world(skolem0005,X491)|singleton(X491,skolem0008),inference(resolution,[status(thm)],[c89, c436])).
% 1.32/1.49  cnf(c519,plain,~accessible_world(skolem0005,X490)|singleton(X490,skolem0005),inference(resolution,[status(thm)],[c89, c486])).
% 1.32/1.49  cnf(c518,plain,~accessible_world(skolem0005,X489)|singleton(X489,skolem0003),inference(resolution,[status(thm)],[c89, c507])).
% 1.32/1.49  cnf(c517,plain,~accessible_world(skolem0005,X488)|singleton(X488,skolem0006),inference(resolution,[status(thm)],[c89, c500])).
% 1.32/1.49  cnf(c516,plain,~accessible_world(skolem0001,X481)|singleton(X481,skolem0007),inference(resolution,[status(thm)],[c89, c319])).
% 1.32/1.49  cnf(c515,plain,~accessible_world(skolem0005,X480)|singleton(X480,skolem0002),inference(resolution,[status(thm)],[c89, c493])).
% 1.32/1.49  cnf(c514,plain,~accessible_world(skolem0001,X479)|singleton(X479,skolem0005),inference(resolution,[status(thm)],[c89, c400])).
% 1.32/1.49  cnf(c513,plain,~accessible_world(skolem0001,X474)|singleton(X474,skolem0006),inference(resolution,[status(thm)],[c89, c367])).
% 1.32/1.49  cnf(c512,plain,~accessible_world(skolem0001,X473)|singleton(X473,skolem0003),inference(resolution,[status(thm)],[c89, c365])).
% 1.32/1.49  cnf(c511,plain,~accessible_world(skolem0001,X472)|singleton(X472,skolem0004),inference(resolution,[status(thm)],[c89, c308])).
% 1.32/1.49  cnf(c506,plain,~accessible_world(skolem0005,X467)|thing(X467,skolem0003),inference(resolution,[status(thm)],[c505, c86])).
% 1.32/1.49  cnf(c499,plain,~accessible_world(skolem0005,X466)|thing(X466,skolem0006),inference(resolution,[status(thm)],[c498, c86])).
% 1.32/1.49  cnf(c492,plain,~accessible_world(skolem0005,X465)|thing(X465,skolem0002),inference(resolution,[status(thm)],[c491, c86])).
% 1.32/1.49  cnf(c485,plain,~accessible_world(skolem0005,X464)|thing(X464,skolem0005),inference(resolution,[status(thm)],[c484, c86])).
% 1.32/1.49  cnf(c479,plain,~accessible_world(skolem0005,X455)|thing(X455,skolem0007),inference(resolution,[status(thm)],[c478, c86])).
% 1.32/1.49  cnf(c475,plain,~accessible_world(skolem0001,X446)|thing(X446,skolem0008),inference(resolution,[status(thm)],[c86, c291])).
% 1.32/1.49  cnf(c473,plain,~accessible_world(skolem0005,X440)|thing(X440,skolem0004),inference(resolution,[status(thm)],[c86, c459])).
% 1.32/1.49  cnf(c472,plain,~accessible_world(skolem0001,X439)|thing(X439,skolem0004),inference(resolution,[status(thm)],[c86, c305])).
% 1.32/1.49  cnf(c471,plain,~accessible_world(skolem0005,X432)|thing(X432,skolem0008),inference(resolution,[status(thm)],[c86, c428])).
% 1.32/1.49  cnf(c458,plain,~accessible_world(skolem0005,X422)|eventuality(X422,skolem0004),inference(resolution,[status(thm)],[c453, c83])).
% 1.32/1.49  cnf(c443,plain,~accessible_world(skolem0005,X421)|eventuality(X421,skolem0008),inference(resolution,[status(thm)],[c83, c421])).
% 1.32/1.49  cnf(c463,plain,~existent(skolem0005,skolem0004),inference(resolution,[status(thm)],[c455, c192])).
% 1.32/1.49  cnf(c441,plain,~accessible_world(skolem0001,X409)|eventuality(X409,skolem0008),inference(resolution,[status(thm)],[c83, c289])).
% 1.32/1.49  cnf(c422,plain,~accessible_world(skolem0005,X401)|state(X401,skolem0008),inference(resolution,[status(thm)],[c420, c80])).
% 1.32/1.49  cnf(c434,plain,~existent(skolem0005,skolem0008),inference(resolution,[status(thm)],[c425, c192])).
% 1.32/1.49  fof(ax71,axiom,(![U]:(![V]:(![W]:(![X]:(be(U,V,W,X)=>W=X))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax71)).
% 1.32/1.49  fof(c65,plain,(![U]:(![V]:(![W]:(![X]:(~be(U,V,W,X)|W=X))))),inference(fof_nnf,[status(thm)],[ax71])).
% 1.32/1.49  fof(c66,plain,(![X12]:(![X13]:(![X14]:(![X15]:(~be(X12,X13,X14,X15)|X14=X15))))),inference(variable_rename,[status(thm)],[c65])).
% 1.32/1.49  cnf(c67,plain,~be(X378,X381,X379,X380)|X379=X380,inference(split_conjunct,[status(thm)],[c66])).
% 1.32/1.49  cnf(c35,axiom,X372!=X371|~actual_world(X372)|actual_world(X371),theory(equality)).
% 1.32/1.49  fof(ax1,axiom,(![U]:(![V]:(vincent_forename(U,V)=>forename(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax1)).
% 1.32/1.49  fof(c280,plain,(![U]:(![V]:(~vincent_forename(U,V)|forename(U,V)))),inference(fof_nnf,[status(thm)],[ax1])).
% 1.32/1.49  fof(c281,plain,(![X199]:(![X200]:(~vincent_forename(X199,X200)|forename(X199,X200)))),inference(variable_rename,[status(thm)],[c280])).
% 1.32/1.49  cnf(c282,plain,~vincent_forename(X362,X363)|forename(X362,X363),inference(split_conjunct,[status(thm)],[c281])).
% 1.32/1.49  cnf(c407,plain,~specific(skolem0001,skolem0005),inference(resolution,[status(thm)],[c398, c184])).
% 1.32/1.49  fof(ax3,axiom,(![U]:(![V]:(smoke(U,V)=>event(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax3)).
% 1.32/1.49  fof(c274,plain,(![U]:(![V]:(~smoke(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax3])).
% 1.32/1.49  fof(c275,plain,(![X195]:(![X196]:(~smoke(X195,X196)|event(X195,X196)))),inference(variable_rename,[status(thm)],[c274])).
% 1.32/1.49  cnf(c276,plain,~smoke(X350,X351)|event(X350,X351),inference(split_conjunct,[status(thm)],[c275])).
% 1.32/1.49  fof(ax4,axiom,(![U]:(![V]:(jules_forename(U,V)=>forename(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax4)).
% 1.32/1.49  fof(c271,plain,(![U]:(![V]:(~jules_forename(U,V)|forename(U,V)))),inference(fof_nnf,[status(thm)],[ax4])).
% 1.32/1.49  fof(c272,plain,(![X193]:(![X194]:(~jules_forename(X193,X194)|forename(X193,X194)))),inference(variable_rename,[status(thm)],[c271])).
% 1.32/1.49  cnf(c273,plain,~jules_forename(X349,X348)|forename(X349,X348),inference(split_conjunct,[status(thm)],[c272])).
% 1.32/1.49  cnf(c382,plain,~specific(skolem0001,skolem0006),inference(resolution,[status(thm)],[c376, c184])).
% 1.32/1.49  cnf(c380,plain,~specific(skolem0001,skolem0003),inference(resolution,[status(thm)],[c375, c184])).
% 1.32/1.49  cnf(c344,plain,~unisex(skolem0001,skolem0007),inference(resolution,[status(thm)],[c342, c180])).
% 1.32/1.49  cnf(c343,plain,~unisex(skolem0001,skolem0002),inference(resolution,[status(thm)],[c341, c180])).
% 1.32/1.49  cnf(c336,plain,~nonhuman(skolem0001,skolem0002),inference(resolution,[status(thm)],[c334, c188])).
% 1.32/1.49  cnf(c335,plain,~nonhuman(skolem0001,skolem0007),inference(resolution,[status(thm)],[c333, c188])).
% 1.32/1.49  cnf(c306,plain,~existent(skolem0001,skolem0004),inference(resolution,[status(thm)],[c304, c192])).
% 1.32/1.49  cnf(c295,plain,~existent(skolem0001,skolem0008),inference(resolution,[status(thm)],[c294, c192])).
% 1.32/1.49  cnf(transitivity,axiom,X206!=X205|X205!=X207|X206=X207,theory(equality)).
% 1.32/1.49  cnf(symmetry,axiom,X203!=X202|X202=X203,theory(equality)).
% 1.32/1.49  cnf(c42,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c41])).
% 1.32/1.49  % SZS output end Saturation
% 1.32/1.49  
% 1.32/1.49  % Initial clauses    : 133
% 1.32/1.49  % Processed clauses  : 868
% 1.32/1.49  % Factors computed   : 19
% 1.32/1.49  % Resolvents computed: 989
% 1.32/1.49  % Tautologies deleted: 3
% 1.32/1.49  % Forward subsumed   : 270
% 1.32/1.49  % Backward subsumed  : 2
% 1.32/1.49  % -------- CPU Time ---------
% 1.32/1.49  % User time          : 1.119 s
% 1.32/1.49  % System time        : 0.019 s
% 1.32/1.49  % Total time         : 1.138 s
%------------------------------------------------------------------------------