PyRes---1.5.CSA-Sat.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : PyRes---1.5
% Problem  : NLP224+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s

% Computer : n018.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:41 EDT 2024

% Result   : CounterSatisfiable 1.54s 1.73s
% Output   : Saturation 1.54s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12  % Problem  : NLP224+1 : TPTP v8.1.2. Released v2.4.0.
% 0.10/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34  % Computer : n018.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 300
% 0.13/0.34  % DateTime : Wed May  8 13:26:23 EDT 2024
% 0.13/0.34  % CPUTime  : 
% 1.54/1.73  % Version:  1.5
% 1.54/1.73  % SZS status CounterSatisfiable
% 1.54/1.73  % SZS output start Saturation
% 1.54/1.73  fof(co1,conjecture,(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(?[X3]:((((((((((((((((((of(U,W,V)&man(U,V))&jules_forename(U,W))&forename(U,W))&of(U,Y,X))&man(U,X))&vincent_forename(U,Y))&forename(U,Y))&proposition(U,X1))&agent(U,Z,X))&theme(U,Z,X1))&event(U,Z))&present(U,Z))&think_believe_consider(U,Z))&accessible_world(U,X1))&(![X4]:(man(X1,X4)=>(?[X5]:(((event(X1,X5)&agent(X1,X5,X4))&present(X1,X5))&smoke(X1,X5))))))&man(U,X2))&state(U,X3))&be(U,X3,V,X2))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 1.54/1.73  fof(c36,negated_conjecture,(~(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(?[X3]:((((((((((((((((((of(U,W,V)&man(U,V))&jules_forename(U,W))&forename(U,W))&of(U,Y,X))&man(U,X))&vincent_forename(U,Y))&forename(U,Y))&proposition(U,X1))&agent(U,Z,X))&theme(U,Z,X1))&event(U,Z))&present(U,Z))&think_believe_consider(U,Z))&accessible_world(U,X1))&(![X4]:(man(X1,X4)=>(?[X5]:(((event(X1,X5)&agent(X1,X5,X4))&present(X1,X5))&smoke(X1,X5))))))&man(U,X2))&state(U,X3))&be(U,X3,V,X2)))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 1.54/1.73  fof(c37,negated_conjecture,(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(?[X3]:((((((((((((((((((of(U,W,V)&man(U,V))&jules_forename(U,W))&forename(U,W))&of(U,Y,X))&man(U,X))&vincent_forename(U,Y))&forename(U,Y))&proposition(U,X1))&agent(U,Z,X))&theme(U,Z,X1))&event(U,Z))&present(U,Z))&think_believe_consider(U,Z))&accessible_world(U,X1))&(![X4]:(~man(X1,X4)|(?[X5]:(((event(X1,X5)&agent(X1,X5,X4))&present(X1,X5))&smoke(X1,X5))))))&man(U,X2))&state(U,X3))&be(U,X3,V,X2)))))))))))),inference(fof_nnf,[status(thm)],[c36])).
% 1.54/1.73  fof(c38,negated_conjecture,(?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(?[X10]:((((((((((((((((((of(X2,X4,X3)&man(X2,X3))&jules_forename(X2,X4))&forename(X2,X4))&of(X2,X6,X5))&man(X2,X5))&vincent_forename(X2,X6))&forename(X2,X6))&proposition(X2,X8))&agent(X2,X7,X5))&theme(X2,X7,X8))&event(X2,X7))&present(X2,X7))&think_believe_consider(X2,X7))&accessible_world(X2,X8))&(![X11]:(~man(X8,X11)|(?[X12]:(((event(X8,X12)&agent(X8,X12,X11))&present(X8,X12))&smoke(X8,X12))))))&man(X2,X9))&state(X2,X10))&be(X2,X10,X3,X9)))))))))))),inference(variable_rename,[status(thm)],[c37])).
% 1.54/1.73  fof(c40,negated_conjecture,(![X11]:(actual_world(skolem0001)&((((((((((((((((((of(skolem0001,skolem0003,skolem0002)&man(skolem0001,skolem0002))&jules_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&of(skolem0001,skolem0005,skolem0004))&man(skolem0001,skolem0004))&vincent_forename(skolem0001,skolem0005))&forename(skolem0001,skolem0005))&proposition(skolem0001,skolem0007))&agent(skolem0001,skolem0006,skolem0004))&theme(skolem0001,skolem0006,skolem0007))&event(skolem0001,skolem0006))&present(skolem0001,skolem0006))&think_believe_consider(skolem0001,skolem0006))&accessible_world(skolem0001,skolem0007))&(~man(skolem0007,X11)|(((event(skolem0007,skolem0010(X11))&agent(skolem0007,skolem0010(X11),X11))&present(skolem0007,skolem0010(X11)))&smoke(skolem0007,skolem0010(X11)))))&man(skolem0001,skolem0008))&state(skolem0001,skolem0009))&be(skolem0001,skolem0009,skolem0002,skolem0008)))),inference(shift_quantors,[status(thm)],[fof(c39,negated_conjecture,(actual_world(skolem0001)&((((((((((((((((((of(skolem0001,skolem0003,skolem0002)&man(skolem0001,skolem0002))&jules_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&of(skolem0001,skolem0005,skolem0004))&man(skolem0001,skolem0004))&vincent_forename(skolem0001,skolem0005))&forename(skolem0001,skolem0005))&proposition(skolem0001,skolem0007))&agent(skolem0001,skolem0006,skolem0004))&theme(skolem0001,skolem0006,skolem0007))&event(skolem0001,skolem0006))&present(skolem0001,skolem0006))&think_believe_consider(skolem0001,skolem0006))&accessible_world(skolem0001,skolem0007))&(![X11]:(~man(skolem0007,X11)|(((event(skolem0007,skolem0010(X11))&agent(skolem0007,skolem0010(X11),X11))&present(skolem0007,skolem0010(X11)))&smoke(skolem0007,skolem0010(X11))))))&man(skolem0001,skolem0008))&state(skolem0001,skolem0009))&be(skolem0001,skolem0009,skolem0002,skolem0008))),inference(skolemize,[status(esa)],[c38])).])).
% 1.54/1.73  fof(c41,negated_conjecture,(![X11]:(actual_world(skolem0001)&((((((((((((((((((of(skolem0001,skolem0003,skolem0002)&man(skolem0001,skolem0002))&jules_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&of(skolem0001,skolem0005,skolem0004))&man(skolem0001,skolem0004))&vincent_forename(skolem0001,skolem0005))&forename(skolem0001,skolem0005))&proposition(skolem0001,skolem0007))&agent(skolem0001,skolem0006,skolem0004))&theme(skolem0001,skolem0006,skolem0007))&event(skolem0001,skolem0006))&present(skolem0001,skolem0006))&think_believe_consider(skolem0001,skolem0006))&accessible_world(skolem0001,skolem0007))&((((~man(skolem0007,X11)|event(skolem0007,skolem0010(X11)))&(~man(skolem0007,X11)|agent(skolem0007,skolem0010(X11),X11)))&(~man(skolem0007,X11)|present(skolem0007,skolem0010(X11))))&(~man(skolem0007,X11)|smoke(skolem0007,skolem0010(X11)))))&man(skolem0001,skolem0008))&state(skolem0001,skolem0009))&be(skolem0001,skolem0009,skolem0002,skolem0008)))),inference(distribute,[status(thm)],[c40])).
% 1.54/1.73  cnf(c59,negated_conjecture,~man(skolem0007,X458)|agent(skolem0007,skolem0010(X458),X458),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.73  cnf(c57,negated_conjecture,accessible_world(skolem0001,skolem0007),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.73  cnf(c48,negated_conjecture,man(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.73  fof(ax59,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&man(V,U))=>man(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax59)).
% 1.54/1.73  fof(c102,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~man(V,U))|man(W,U))))),inference(fof_nnf,[status(thm)],[ax59])).
% 1.54/1.73  fof(c103,plain,(![X56]:(![X57]:(![X58]:((~accessible_world(X57,X58)|~man(X57,X56))|man(X58,X56))))),inference(variable_rename,[status(thm)],[c102])).
% 1.54/1.73  cnf(c104,plain,~accessible_world(X519,X518)|~man(X519,X517)|man(X518,X517),inference(split_conjunct,[status(thm)],[c103])).
% 1.54/1.73  cnf(c605,plain,~accessible_world(skolem0001,X601)|man(X601,skolem0004),inference(resolution,[status(thm)],[c104, c48])).
% 1.54/1.73  cnf(c809,plain,man(skolem0007,skolem0004),inference(resolution,[status(thm)],[c605, c57])).
% 1.54/1.73  cnf(c815,plain,agent(skolem0007,skolem0010(skolem0004),skolem0004),inference(resolution,[status(thm)],[c809, c59])).
% 1.54/1.73  cnf(c53,negated_conjecture,theme(skolem0001,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.73  fof(ax37,axiom,(![U]:(![V]:(![W]:(![X]:((accessible_world(W,X)&theme(W,U,V))=>theme(X,U,V)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax37)).
% 1.54/1.73  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.54/1.73  fof(c169,plain,(![X124]:(![X125]:(![X126]:(![X127]:((~accessible_world(X126,X127)|~theme(X126,X124,X125))|theme(X127,X124,X125)))))),inference(variable_rename,[status(thm)],[c168])).
% 1.54/1.73  cnf(c170,plain,~accessible_world(X612,X614)|~theme(X612,X615,X613)|theme(X614,X615,X613),inference(split_conjunct,[status(thm)],[c169])).
% 1.54/1.73  cnf(c855,plain,~accessible_world(skolem0001,X1002)|theme(X1002,skolem0006,skolem0007),inference(resolution,[status(thm)],[c170, c53])).
% 1.54/1.73  cnf(c1193,plain,theme(skolem0007,skolem0006,skolem0007),inference(resolution,[status(thm)],[c855, c57])).
% 1.54/1.73  fof(ax69,axiom,(![U]:(![V]:(![W]:(![X]:(![Y]:(![Z]:((((((((think_believe_consider(U,V)&proposition(U,Y))&theme(U,V,Y))&agent(U,V,X))&think_believe_consider(U,W))&proposition(U,Z))&theme(U,W,Z))&agent(U,W,X))=>Y=Z))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax69)).
% 1.54/1.73  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.54/1.73  fof(c73,plain,(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:((((((((~think_believe_consider(X21,X22)|~proposition(X21,X25))|~theme(X21,X22,X25))|~agent(X21,X22,X24))|~think_believe_consider(X21,X23))|~proposition(X21,X26))|~theme(X21,X23,X26))|~agent(X21,X23,X24))|X25=X26))))))),inference(variable_rename,[status(thm)],[c72])).
% 1.54/1.73  cnf(c74,plain,~think_believe_consider(X467,X472)|~proposition(X467,X470)|~theme(X467,X472,X470)|~agent(X467,X472,X469)|~think_believe_consider(X467,X468)|~proposition(X467,X471)|~theme(X467,X468,X471)|~agent(X467,X468,X469)|X470=X471,inference(split_conjunct,[status(thm)],[c73])).
% 1.54/1.73  cnf(c52,negated_conjecture,agent(skolem0001,skolem0006,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.73  fof(ax39,axiom,(![U]:(![V]:(![W]:(![X]:((accessible_world(W,X)&agent(W,U,V))=>agent(X,U,V)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax39)).
% 1.54/1.73  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.54/1.73  fof(c163,plain,(![X117]:(![X118]:(![X119]:(![X120]:((~accessible_world(X119,X120)|~agent(X119,X117,X118))|agent(X120,X117,X118)))))),inference(variable_rename,[status(thm)],[c162])).
% 1.54/1.73  cnf(c164,plain,~accessible_world(X608,X606)|~agent(X608,X607,X605)|agent(X606,X607,X605),inference(split_conjunct,[status(thm)],[c163])).
% 1.54/1.73  cnf(c831,plain,~accessible_world(skolem0001,X997)|agent(X997,skolem0006,skolem0004),inference(resolution,[status(thm)],[c164, c52])).
% 1.54/1.73  cnf(c1187,plain,agent(skolem0007,skolem0006,skolem0004),inference(resolution,[status(thm)],[c831, c57])).
% 1.54/1.73  cnf(c1188,plain,~think_believe_consider(skolem0007,X1490)|~proposition(skolem0007,X1491)|~theme(skolem0007,X1490,X1491)|~agent(skolem0007,X1490,skolem0004)|~think_believe_consider(skolem0007,skolem0006)|~proposition(skolem0007,X1492)|~theme(skolem0007,skolem0006,X1492)|X1491=X1492,inference(resolution,[status(thm)],[c1187, c74])).
% 1.54/1.73  cnf(c1528,plain,~think_believe_consider(skolem0007,X1609)|~proposition(skolem0007,X1610)|~theme(skolem0007,X1609,X1610)|~agent(skolem0007,X1609,skolem0004)|~think_believe_consider(skolem0007,skolem0006)|~proposition(skolem0007,skolem0007)|X1610=skolem0007,inference(resolution,[status(thm)],[c1188, c1193])).
% 1.54/1.73  cnf(c1617,plain,~think_believe_consider(skolem0007,skolem0010(skolem0004))|~proposition(skolem0007,X1737)|~theme(skolem0007,skolem0010(skolem0004),X1737)|~think_believe_consider(skolem0007,skolem0006)|~proposition(skolem0007,skolem0007)|X1737=skolem0007,inference(resolution,[status(thm)],[c1528, c815])).
% 1.54/1.73  cnf(c34,axiom,X449!=X452|X450!=X445|X446!=X451|X448!=X447|~be(X449,X450,X446,X448)|be(X452,X445,X451,X447),theory(equality)).
% 1.54/1.73  fof(ax68,axiom,(![U]:(![V]:(![W]:(![X]:(![Y]:((accessible_world(X,Y)&be(X,U,V,W))=>be(Y,U,V,W))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax68)).
% 1.54/1.73  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.54/1.73  fof(c76,plain,(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:((~accessible_world(X30,X31)|~be(X30,X27,X28,X29))|be(X31,X27,X28,X29))))))),inference(variable_rename,[status(thm)],[c75])).
% 1.54/1.73  cnf(c77,plain,~accessible_world(X476,X478)|~be(X476,X480,X477,X479)|be(X478,X480,X477,X479),inference(split_conjunct,[status(thm)],[c76])).
% 1.54/1.73  cnf(reflexivity,axiom,X202=X202,theory(equality)).
% 1.54/1.73  cnf(c64,negated_conjecture,be(skolem0001,skolem0009,skolem0002,skolem0008),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.73  fof(ax71,axiom,(![U]:(![V]:(![W]:(![X]:(be(U,V,W,X)=>W=X))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax71)).
% 1.54/1.73  fof(c65,plain,(![U]:(![V]:(![W]:(![X]:(~be(U,V,W,X)|W=X))))),inference(fof_nnf,[status(thm)],[ax71])).
% 1.54/1.73  fof(c66,plain,(![X13]:(![X14]:(![X15]:(![X16]:(~be(X13,X14,X15,X16)|X15=X16))))),inference(variable_rename,[status(thm)],[c65])).
% 1.54/1.73  cnf(c67,plain,~be(X393,X392,X394,X391)|X394=X391,inference(split_conjunct,[status(thm)],[c66])).
% 1.54/1.73  cnf(c447,plain,skolem0002=skolem0008,inference(resolution,[status(thm)],[c67, c64])).
% 1.54/1.73  cnf(c511,plain,skolem0001!=X1101|skolem0009!=X1102|skolem0002!=X1104|skolem0008!=X1103|be(X1101,X1102,X1104,X1103),inference(resolution,[status(thm)],[c34, c64])).
% 1.54/1.73  cnf(c1252,plain,skolem0001!=X1522|skolem0009!=X1521|skolem0002!=X1520|be(X1522,X1521,X1520,skolem0008),inference(resolution,[status(thm)],[c511, reflexivity])).
% 1.54/1.73  cnf(c1547,plain,skolem0001!=X1560|skolem0009!=X1559|be(X1560,X1559,skolem0008,skolem0008),inference(resolution,[status(thm)],[c1252, c447])).
% 1.54/1.73  cnf(c1586,plain,skolem0001!=X1561|be(X1561,skolem0009,skolem0008,skolem0008),inference(resolution,[status(thm)],[c1547, reflexivity])).
% 1.54/1.73  cnf(c1587,plain,be(skolem0001,skolem0009,skolem0008,skolem0008),inference(resolution,[status(thm)],[c1586, reflexivity])).
% 1.54/1.73  cnf(c1590,plain,~accessible_world(skolem0001,X1563)|be(X1563,skolem0009,skolem0008,skolem0008),inference(resolution,[status(thm)],[c1587, c77])).
% 1.54/1.73  cnf(c1591,plain,be(skolem0007,skolem0009,skolem0008,skolem0008),inference(resolution,[status(thm)],[c1590, c57])).
% 1.54/1.73  cnf(c1593,plain,skolem0007!=X1717|skolem0009!=X1718|skolem0008!=X1720|skolem0008!=X1719|be(X1717,X1718,X1720,X1719),inference(resolution,[status(thm)],[c1591, c34])).
% 1.54/1.73  cnf(c1654,plain,skolem0007!=X1723|skolem0009!=X1722|skolem0008!=X1721|be(X1723,X1722,X1721,X1721),inference(factor,[status(thm)],[c1593])).
% 1.54/1.73  cnf(c1589,plain,skolem0001!=X1700|skolem0009!=X1701|skolem0008!=X1703|skolem0008!=X1702|be(X1700,X1701,X1703,X1702),inference(resolution,[status(thm)],[c1587, c34])).
% 1.54/1.73  cnf(c1649,plain,skolem0001!=X1704|skolem0009!=X1705|skolem0008!=X1706|be(X1704,X1705,X1706,X1706),inference(factor,[status(thm)],[c1589])).
% 1.54/1.73  cnf(symmetry,axiom,X203!=X204|X204=X203,theory(equality)).
% 1.54/1.73  cnf(c449,plain,skolem0008=skolem0002,inference(resolution,[status(thm)],[c447, symmetry])).
% 1.54/1.73  cnf(c1251,plain,skolem0001!=X1516|skolem0009!=X1515|skolem0002!=X1514|be(X1516,X1515,X1514,skolem0002),inference(resolution,[status(thm)],[c511, c449])).
% 1.54/1.73  cnf(c1543,plain,skolem0001!=X1552|skolem0009!=X1551|be(X1552,X1551,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1251, reflexivity])).
% 1.54/1.73  cnf(c1576,plain,skolem0001!=X1554|be(X1554,skolem0009,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1543, reflexivity])).
% 1.54/1.73  cnf(c1577,plain,be(skolem0001,skolem0009,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1576, reflexivity])).
% 1.54/1.73  cnf(c1580,plain,~accessible_world(skolem0001,X1555)|be(X1555,skolem0009,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1577, c77])).
% 1.54/1.73  cnf(c1581,plain,be(skolem0007,skolem0009,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1580, c57])).
% 1.54/1.73  cnf(c1583,plain,skolem0007!=X1669|skolem0009!=X1670|skolem0002!=X1672|skolem0002!=X1671|be(X1669,X1670,X1672,X1671),inference(resolution,[status(thm)],[c1581, c34])).
% 1.54/1.73  cnf(c1642,plain,skolem0007!=X1682|skolem0009!=X1680|skolem0002!=X1681|be(X1682,X1680,X1681,X1681),inference(factor,[status(thm)],[c1583])).
% 1.54/1.73  cnf(c1579,plain,skolem0001!=X1665|skolem0009!=X1666|skolem0002!=X1668|skolem0002!=X1667|be(X1665,X1666,X1668,X1667),inference(resolution,[status(thm)],[c1577, c34])).
% 1.54/1.73  cnf(c1639,plain,skolem0001!=X1675|skolem0009!=X1673|skolem0002!=X1674|be(X1675,X1673,X1674,X1674),inference(factor,[status(thm)],[c1579])).
% 1.54/1.73  cnf(c1542,plain,skolem0001!=X1545|skolem0009!=X1544|be(X1545,X1544,skolem0008,skolem0002),inference(resolution,[status(thm)],[c1251, c447])).
% 1.54/1.73  cnf(c1566,plain,skolem0001!=X1546|be(X1546,skolem0009,skolem0008,skolem0002),inference(resolution,[status(thm)],[c1542, reflexivity])).
% 1.54/1.73  cnf(c1567,plain,be(skolem0001,skolem0009,skolem0008,skolem0002),inference(resolution,[status(thm)],[c1566, reflexivity])).
% 1.54/1.73  cnf(c1570,plain,~accessible_world(skolem0001,X1549)|be(X1549,skolem0009,skolem0008,skolem0002),inference(resolution,[status(thm)],[c1567, c77])).
% 1.54/1.73  cnf(c1572,plain,be(skolem0007,skolem0009,skolem0008,skolem0002),inference(resolution,[status(thm)],[c1570, c57])).
% 1.54/1.73  cnf(c1574,plain,skolem0007!=X1646|skolem0009!=X1647|skolem0008!=X1649|skolem0002!=X1648|be(X1646,X1647,X1649,X1648),inference(resolution,[status(thm)],[c1572, c34])).
% 1.54/1.73  cnf(c1633,plain,skolem0007!=X1658|skolem0009!=X1660|skolem0008!=X1659|be(X1658,X1660,X1659,skolem0002),inference(resolution,[status(thm)],[c1574, reflexivity])).
% 1.54/1.73  cnf(c545,plain,~think_believe_consider(X1142,X1139)|~proposition(X1142,X1140)|~theme(X1142,X1139,X1140)|~agent(X1142,X1139,X1138)|~proposition(X1142,X1141)|~theme(X1142,X1139,X1141)|X1140=X1141,inference(factor,[status(thm)],[c74])).
% 1.54/1.73  cnf(c1283,plain,~think_believe_consider(skolem0001,skolem0006)|~proposition(skolem0001,X1547)|~theme(skolem0001,skolem0006,X1547)|~agent(skolem0001,skolem0006,X1548)|~proposition(skolem0001,skolem0007)|X1547=skolem0007,inference(resolution,[status(thm)],[c545, c53])).
% 1.54/1.74  cnf(c1571,plain,~think_believe_consider(skolem0001,skolem0006)|~proposition(skolem0001,X1657)|~theme(skolem0001,skolem0006,X1657)|~proposition(skolem0001,skolem0007)|X1657=skolem0007,inference(resolution,[status(thm)],[c1283, c52])).
% 1.54/1.74  cnf(c1632,plain,skolem0007!=X1650|skolem0009!=X1652|skolem0008!=X1651|be(X1650,X1652,X1651,skolem0008),inference(resolution,[status(thm)],[c1574, c447])).
% 1.54/1.74  cnf(c1282,plain,~think_believe_consider(skolem0007,skolem0006)|~proposition(skolem0007,X1542)|~theme(skolem0007,skolem0006,X1542)|~agent(skolem0007,skolem0006,X1543)|~proposition(skolem0007,skolem0007)|X1542=skolem0007,inference(resolution,[status(thm)],[c545, c1193])).
% 1.54/1.74  cnf(c1565,plain,~think_believe_consider(skolem0007,skolem0006)|~proposition(skolem0007,X1645)|~theme(skolem0007,skolem0006,X1645)|~proposition(skolem0007,skolem0007)|X1645=skolem0007,inference(resolution,[status(thm)],[c1282, c1187])).
% 1.54/1.74  cnf(c1569,plain,skolem0001!=X1624|skolem0009!=X1625|skolem0008!=X1627|skolem0002!=X1626|be(X1624,X1625,X1627,X1626),inference(resolution,[status(thm)],[c1567, c34])).
% 1.54/1.74  cnf(c1625,plain,skolem0001!=X1640|skolem0009!=X1638|skolem0008!=X1639|be(X1640,X1638,X1639,skolem0002),inference(resolution,[status(thm)],[c1569, reflexivity])).
% 1.54/1.74  cnf(c31,axiom,X424!=X427|X425!=X422|X423!=X426|~agent(X424,X425,X423)|agent(X427,X422,X426),theory(equality)).
% 1.54/1.74  cnf(c62,negated_conjecture,man(skolem0001,skolem0008),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.74  cnf(c604,plain,~accessible_world(skolem0001,X584)|man(X584,skolem0008),inference(resolution,[status(thm)],[c104, c62])).
% 1.54/1.74  cnf(c736,plain,man(skolem0007,skolem0008),inference(resolution,[status(thm)],[c604, c57])).
% 1.54/1.74  cnf(c739,plain,agent(skolem0007,skolem0010(skolem0008),skolem0008),inference(resolution,[status(thm)],[c736, c59])).
% 1.54/1.74  cnf(c1008,plain,skolem0007!=X1439|skolem0010(skolem0008)!=X1440|skolem0008!=X1441|agent(X1439,X1440,X1441),inference(resolution,[status(thm)],[c739, c31])).
% 1.54/1.74  cnf(c1491,plain,skolem0007!=X1530|skolem0008!=X1531|agent(X1530,skolem0010(skolem0008),X1531),inference(resolution,[status(thm)],[c1008, reflexivity])).
% 1.54/1.74  cnf(c1556,plain,skolem0007!=X1532|agent(X1532,skolem0010(skolem0008),skolem0002),inference(resolution,[status(thm)],[c1491, c449])).
% 1.54/1.74  cnf(c1558,plain,agent(skolem0007,skolem0010(skolem0008),skolem0002),inference(resolution,[status(thm)],[c1556, reflexivity])).
% 1.54/1.74  cnf(c1559,plain,~think_believe_consider(skolem0007,X1631)|~proposition(skolem0007,X1632)|~theme(skolem0007,X1631,X1632)|~agent(skolem0007,X1631,skolem0002)|~think_believe_consider(skolem0007,skolem0010(skolem0008))|~proposition(skolem0007,X1633)|~theme(skolem0007,skolem0010(skolem0008),X1633)|X1632=X1633,inference(resolution,[status(thm)],[c1558, c74])).
% 1.54/1.74  cnf(c1624,plain,skolem0001!=X1630|skolem0009!=X1628|skolem0008!=X1629|be(X1630,X1628,X1629,skolem0008),inference(resolution,[status(thm)],[c1569, c447])).
% 1.54/1.74  cnf(c1561,plain,skolem0007!=X1614|skolem0010(skolem0008)!=X1615|skolem0002!=X1616|agent(X1614,X1615,X1616),inference(resolution,[status(thm)],[c1558, c31])).
% 1.54/1.74  cnf(c1620,plain,skolem0007!=X1620|skolem0002!=X1621|agent(X1620,skolem0010(skolem0008),X1621),inference(resolution,[status(thm)],[c1561, reflexivity])).
% 1.54/1.74  cnf(c44,negated_conjecture,man(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.74  cnf(c603,plain,~accessible_world(skolem0001,X568)|man(X568,skolem0002),inference(resolution,[status(thm)],[c104, c44])).
% 1.54/1.74  cnf(c661,plain,man(skolem0007,skolem0002),inference(resolution,[status(thm)],[c603, c57])).
% 1.54/1.74  cnf(c664,plain,agent(skolem0007,skolem0010(skolem0002),skolem0002),inference(resolution,[status(thm)],[c661, c59])).
% 1.54/1.74  cnf(c920,plain,skolem0007!=X1410|skolem0010(skolem0002)!=X1411|skolem0002!=X1412|agent(X1410,X1411,X1412),inference(resolution,[status(thm)],[c664, c31])).
% 1.54/1.74  cnf(c1469,plain,skolem0007!=X1518|skolem0002!=X1519|agent(X1518,skolem0010(skolem0002),X1519),inference(resolution,[status(thm)],[c920, reflexivity])).
% 1.54/1.74  cnf(c1545,plain,skolem0007!=X1523|agent(X1523,skolem0010(skolem0002),skolem0008),inference(resolution,[status(thm)],[c1469, c447])).
% 1.54/1.74  cnf(c1549,plain,agent(skolem0007,skolem0010(skolem0002),skolem0008),inference(resolution,[status(thm)],[c1545, reflexivity])).
% 1.54/1.74  cnf(c1550,plain,~think_believe_consider(skolem0007,X1617)|~proposition(skolem0007,X1618)|~theme(skolem0007,X1617,X1618)|~agent(skolem0007,X1617,skolem0008)|~think_believe_consider(skolem0007,skolem0010(skolem0002))|~proposition(skolem0007,X1619)|~theme(skolem0007,skolem0010(skolem0002),X1619)|X1618=X1619,inference(resolution,[status(thm)],[c1549, c74])).
% 1.54/1.74  cnf(c549,plain,~accessible_world(skolem0001,X1137)|be(X1137,skolem0009,skolem0002,skolem0008),inference(resolution,[status(thm)],[c77, c64])).
% 1.54/1.74  cnf(c1277,plain,be(skolem0007,skolem0009,skolem0002,skolem0008),inference(resolution,[status(thm)],[c549, c57])).
% 1.54/1.74  cnf(c1279,plain,skolem0007!=X1526|skolem0009!=X1527|skolem0002!=X1529|skolem0008!=X1528|be(X1526,X1527,X1529,X1528),inference(resolution,[status(thm)],[c1277, c34])).
% 1.54/1.74  cnf(c1555,plain,skolem0007!=X1604|skolem0009!=X1603|skolem0002!=X1605|be(X1604,X1603,X1605,skolem0008),inference(resolution,[status(thm)],[c1279, reflexivity])).
% 1.54/1.74  cnf(c1613,plain,skolem0007!=X1612|skolem0009!=X1611|be(X1612,X1611,skolem0002,skolem0008),inference(resolution,[status(thm)],[c1555, reflexivity])).
% 1.54/1.74  cnf(c1618,plain,skolem0007!=X1613|be(X1613,skolem0009,skolem0002,skolem0008),inference(resolution,[status(thm)],[c1613, reflexivity])).
% 1.54/1.74  cnf(c1612,plain,skolem0007!=X1607|skolem0009!=X1606|be(X1607,X1606,skolem0008,skolem0008),inference(resolution,[status(thm)],[c1555, c447])).
% 1.54/1.74  cnf(c1614,plain,skolem0007!=X1608|be(X1608,skolem0009,skolem0008,skolem0008),inference(resolution,[status(thm)],[c1612, reflexivity])).
% 1.54/1.74  cnf(c1554,plain,skolem0007!=X1593|skolem0009!=X1592|skolem0002!=X1594|be(X1593,X1592,X1594,skolem0002),inference(resolution,[status(thm)],[c1279, c449])).
% 1.54/1.74  cnf(c1606,plain,skolem0007!=X1599|skolem0009!=X1600|be(X1599,X1600,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1554, reflexivity])).
% 1.54/1.74  cnf(c1610,plain,skolem0007!=X1601|be(X1601,skolem0009,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1606, reflexivity])).
% 1.54/1.74  cnf(c1605,plain,skolem0007!=X1596|skolem0009!=X1597|be(X1596,X1597,skolem0008,skolem0002),inference(resolution,[status(thm)],[c1554, c447])).
% 1.54/1.74  cnf(c1608,plain,skolem0007!=X1598|be(X1598,skolem0009,skolem0008,skolem0002),inference(resolution,[status(thm)],[c1605, reflexivity])).
% 1.54/1.74  fof(ax70,axiom,(![U]:(![V]:(![W]:(((entity(U,V)&forename(U,W))&of(U,W,V))=>(~(?[X]:((forename(U,X)&X!=W)&of(U,X,V)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax70)).
% 1.54/1.74  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.54/1.74  fof(c70,plain,(![X17]:(![X18]:(![X19]:(![X20]:(((~entity(X17,X18)|~forename(X17,X19))|~of(X17,X19,X18))|((~forename(X17,X20)|X20=X19)|~of(X17,X20,X18))))))),inference(shift_quantors,[status(thm)],[fof(c69,plain,(![X17]:(![X18]:(![X19]:(((~entity(X17,X18)|~forename(X17,X19))|~of(X17,X19,X18))|(![X20]:((~forename(X17,X20)|X20=X19)|~of(X17,X20,X18))))))),inference(variable_rename,[status(thm)],[c68])).])).
% 1.54/1.74  cnf(c71,plain,~entity(X463,X462)|~forename(X463,X465)|~of(X463,X465,X462)|~forename(X463,X464)|X464=X465|~of(X463,X464,X462),inference(split_conjunct,[status(thm)],[c70])).
% 1.54/1.74  fof(ax42,axiom,(![U]:(![V]:(![W]:(![X]:((accessible_world(W,X)&of(W,U,V))=>of(X,U,V)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax42)).
% 1.54/1.74  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.54/1.74  fof(c154,plain,(![X107]:(![X108]:(![X109]:(![X110]:((~accessible_world(X109,X110)|~of(X109,X107,X108))|of(X110,X107,X108)))))),inference(variable_rename,[status(thm)],[c153])).
% 1.54/1.74  cnf(c155,plain,~accessible_world(X597,X595)|~of(X597,X596,X594)|of(X595,X596,X594),inference(split_conjunct,[status(thm)],[c154])).
% 1.54/1.74  cnf(c43,negated_conjecture,of(skolem0001,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.74  cnf(c33,axiom,X441!=X444|X442!=X439|X440!=X443|~of(X441,X442,X440)|of(X444,X439,X443),theory(equality)).
% 1.54/1.74  cnf(c503,plain,skolem0001!=X1082|skolem0003!=X1081|skolem0002!=X1080|of(X1082,X1081,X1080),inference(resolution,[status(thm)],[c33, c43])).
% 1.54/1.74  cnf(c1238,plain,skolem0001!=X1473|skolem0003!=X1474|of(X1473,X1474,skolem0008),inference(resolution,[status(thm)],[c503, c447])).
% 1.54/1.74  cnf(c1511,plain,skolem0001!=X1475|of(X1475,skolem0003,skolem0008),inference(resolution,[status(thm)],[c1238, reflexivity])).
% 1.54/1.74  cnf(c1512,plain,of(skolem0001,skolem0003,skolem0008),inference(resolution,[status(thm)],[c1511, reflexivity])).
% 1.54/1.74  cnf(c1513,plain,~accessible_world(skolem0001,X1477)|of(X1477,skolem0003,skolem0008),inference(resolution,[status(thm)],[c1512, c155])).
% 1.54/1.74  cnf(c1517,plain,of(skolem0007,skolem0003,skolem0008),inference(resolution,[status(thm)],[c1513, c57])).
% 1.54/1.74  cnf(c1520,plain,~entity(skolem0007,skolem0008)|~forename(skolem0007,X1595)|~of(skolem0007,X1595,skolem0008)|~forename(skolem0007,skolem0003)|skolem0003=X1595,inference(resolution,[status(thm)],[c1517, c71])).
% 1.54/1.74  cnf(c1552,plain,skolem0007!=X1584|skolem0010(skolem0002)!=X1585|skolem0008!=X1586|agent(X1584,X1585,X1586),inference(resolution,[status(thm)],[c1549, c31])).
% 1.54/1.74  cnf(c1601,plain,skolem0007!=X1589|skolem0008!=X1588|agent(X1589,skolem0010(skolem0002),X1588),inference(resolution,[status(thm)],[c1552, reflexivity])).
% 1.54/1.74  cnf(c1515,plain,~entity(skolem0001,skolem0008)|~forename(skolem0001,X1587)|~of(skolem0001,X1587,skolem0008)|~forename(skolem0001,skolem0003)|skolem0003=X1587,inference(resolution,[status(thm)],[c1512, c71])).
% 1.54/1.74  cnf(c1519,plain,skolem0007!=X1579|skolem0003!=X1578|skolem0008!=X1577|of(X1579,X1578,X1577),inference(resolution,[status(thm)],[c1517, c33])).
% 1.54/1.74  cnf(c1514,plain,skolem0001!=X1571|skolem0003!=X1570|skolem0008!=X1569|of(X1571,X1570,X1569),inference(resolution,[status(thm)],[c1512, c33])).
% 1.54/1.74  cnf(c1548,plain,skolem0001!=X1567|skolem0009!=X1566|be(X1567,X1566,skolem0002,skolem0008),inference(resolution,[status(thm)],[c1252, reflexivity])).
% 1.54/1.74  cnf(c1595,plain,skolem0001!=X1568|be(X1568,skolem0009,skolem0002,skolem0008),inference(resolution,[status(thm)],[c1548, reflexivity])).
% 1.54/1.74  cnf(c1594,plain,~accessible_world(skolem0007,X1564)|be(X1564,skolem0009,skolem0008,skolem0008),inference(resolution,[status(thm)],[c1591, c77])).
% 1.54/1.74  cnf(c1584,plain,~accessible_world(skolem0007,X1558)|be(X1558,skolem0009,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1581, c77])).
% 1.54/1.74  cnf(c546,plain,~think_believe_consider(skolem0001,X1149)|~proposition(skolem0001,X1150)|~theme(skolem0001,X1149,X1150)|~agent(skolem0001,X1149,skolem0004)|~think_believe_consider(skolem0001,skolem0006)|~proposition(skolem0001,X1151)|~theme(skolem0001,skolem0006,X1151)|X1150=X1151,inference(resolution,[status(thm)],[c74, c52])).
% 1.54/1.74  cnf(c1289,plain,~think_believe_consider(skolem0001,X1556)|~proposition(skolem0001,X1557)|~theme(skolem0001,X1556,X1557)|~agent(skolem0001,X1556,skolem0004)|~think_believe_consider(skolem0001,skolem0006)|~proposition(skolem0001,skolem0007)|X1557=skolem0007,inference(resolution,[status(thm)],[c546, c53])).
% 1.54/1.74  cnf(c1575,plain,~accessible_world(skolem0007,X1550)|be(X1550,skolem0009,skolem0008,skolem0002),inference(resolution,[status(thm)],[c1572, c77])).
% 1.54/1.74  cnf(c1032,plain,skolem0007!=X1455|skolem0010(skolem0004)!=X1456|skolem0004!=X1457|agent(X1455,X1456,X1457),inference(resolution,[status(thm)],[c815, c31])).
% 1.54/1.74  cnf(c1500,plain,skolem0007!=X1539|skolem0004!=X1540|agent(X1539,skolem0010(skolem0004),X1540),inference(resolution,[status(thm)],[c1032, reflexivity])).
% 1.54/1.74  cnf(c1563,plain,skolem0007!=X1541|agent(X1541,skolem0010(skolem0004),skolem0004),inference(resolution,[status(thm)],[c1500, reflexivity])).
% 1.54/1.74  cnf(c1560,plain,~accessible_world(skolem0007,X1538)|agent(X1538,skolem0010(skolem0008),skolem0002),inference(resolution,[status(thm)],[c1558, c164])).
% 1.54/1.74  cnf(c1557,plain,skolem0007!=X1533|agent(X1533,skolem0010(skolem0008),skolem0008),inference(resolution,[status(thm)],[c1491, reflexivity])).
% 1.54/1.74  cnf(c1551,plain,~accessible_world(skolem0007,X1525)|agent(X1525,skolem0010(skolem0002),skolem0008),inference(resolution,[status(thm)],[c1549, c164])).
% 1.54/1.74  cnf(c1546,plain,skolem0007!=X1524|agent(X1524,skolem0010(skolem0002),skolem0002),inference(resolution,[status(thm)],[c1469, reflexivity])).
% 1.54/1.74  cnf(c29,axiom,X410!=X413|X411!=X408|X409!=X412|~theme(X410,X411,X409)|theme(X413,X408,X412),theory(equality)).
% 1.54/1.74  cnf(c1195,plain,skolem0007!=X1506|skolem0006!=X1508|skolem0007!=X1507|theme(X1506,X1508,X1507),inference(resolution,[status(thm)],[c1193, c29])).
% 1.54/1.74  cnf(c1538,plain,skolem0007!=X1513|skolem0006!=X1512|theme(X1513,X1512,skolem0007),inference(resolution,[status(thm)],[c1195, reflexivity])).
% 1.54/1.74  cnf(c1541,plain,skolem0007!=X1517|theme(X1517,skolem0006,skolem0007),inference(resolution,[status(thm)],[c1538, reflexivity])).
% 1.54/1.74  cnf(c1537,plain,skolem0007!=X1510|skolem0006!=X1509|theme(X1510,X1509,X1510),inference(factor,[status(thm)],[c1195])).
% 1.54/1.74  cnf(c1539,plain,skolem0007!=X1511|theme(X1511,skolem0006,X1511),inference(resolution,[status(thm)],[c1537, reflexivity])).
% 1.54/1.74  cnf(c1190,plain,skolem0007!=X1497|skolem0006!=X1498|skolem0004!=X1499|agent(X1497,X1498,X1499),inference(resolution,[status(thm)],[c1187, c31])).
% 1.54/1.74  cnf(c1532,plain,skolem0007!=X1504|skolem0006!=X1503|agent(X1504,X1503,skolem0004),inference(resolution,[status(thm)],[c1190, reflexivity])).
% 1.54/1.74  cnf(c1535,plain,skolem0007!=X1505|agent(X1505,skolem0006,skolem0004),inference(resolution,[status(thm)],[c1532, reflexivity])).
% 1.54/1.74  cnf(c47,negated_conjecture,of(skolem0001,skolem0005,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.74  cnf(c787,plain,~accessible_world(skolem0001,X974)|of(X974,skolem0005,skolem0004),inference(resolution,[status(thm)],[c155, c47])).
% 1.54/1.74  cnf(c1175,plain,of(skolem0007,skolem0005,skolem0004),inference(resolution,[status(thm)],[c787, c57])).
% 1.54/1.74  cnf(c1178,plain,skolem0007!=X1484|skolem0005!=X1483|skolem0004!=X1482|of(X1484,X1483,X1482),inference(resolution,[status(thm)],[c1175, c33])).
% 1.54/1.74  cnf(c1523,plain,skolem0007!=X1500|skolem0005!=X1501|of(X1500,X1501,skolem0004),inference(resolution,[status(thm)],[c1178, reflexivity])).
% 1.54/1.74  cnf(c1533,plain,skolem0007!=X1502|of(X1502,skolem0005,skolem0004),inference(resolution,[status(thm)],[c1523, reflexivity])).
% 1.54/1.74  cnf(c786,plain,~accessible_world(skolem0001,X970)|of(X970,skolem0003,skolem0002),inference(resolution,[status(thm)],[c155, c43])).
% 1.54/1.74  cnf(c1169,plain,of(skolem0007,skolem0003,skolem0002),inference(resolution,[status(thm)],[c786, c57])).
% 1.54/1.74  cnf(c1173,plain,skolem0007!=X1471|skolem0003!=X1470|skolem0002!=X1469|of(X1471,X1470,X1469),inference(resolution,[status(thm)],[c1169, c33])).
% 1.54/1.74  cnf(c1509,plain,skolem0007!=X1495|skolem0003!=X1494|of(X1495,X1494,skolem0002),inference(resolution,[status(thm)],[c1173, reflexivity])).
% 1.54/1.74  cnf(c1530,plain,skolem0007!=X1496|of(X1496,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1509, reflexivity])).
% 1.54/1.74  cnf(c1508,plain,skolem0007!=X1489|skolem0003!=X1488|of(X1489,X1488,skolem0008),inference(resolution,[status(thm)],[c1173, c447])).
% 1.54/1.74  cnf(c1526,plain,skolem0007!=X1493|of(X1493,skolem0003,skolem0008),inference(resolution,[status(thm)],[c1508, reflexivity])).
% 1.54/1.74  cnf(c504,plain,skolem0001!=X1090|skolem0005!=X1089|skolem0004!=X1088|of(X1090,X1089,X1088),inference(resolution,[status(thm)],[c33, c47])).
% 1.54/1.74  cnf(c1243,plain,skolem0001!=X1485|skolem0005!=X1486|of(X1485,X1486,skolem0004),inference(resolution,[status(thm)],[c504, reflexivity])).
% 1.54/1.74  cnf(c1524,plain,skolem0001!=X1487|of(X1487,skolem0005,skolem0004),inference(resolution,[status(thm)],[c1243, reflexivity])).
% 1.54/1.74  cnf(c1239,plain,skolem0001!=X1479|skolem0003!=X1480|of(X1479,X1480,skolem0002),inference(resolution,[status(thm)],[c503, reflexivity])).
% 1.54/1.74  cnf(c1521,plain,skolem0001!=X1481|of(X1481,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1239, reflexivity])).
% 1.54/1.74  cnf(c1518,plain,~accessible_world(skolem0007,X1478)|of(X1478,skolem0003,skolem0008),inference(resolution,[status(thm)],[c1517, c155])).
% 1.54/1.74  cnf(c1176,plain,~entity(skolem0007,skolem0004)|~forename(skolem0007,X1476)|~of(skolem0007,X1476,skolem0004)|~forename(skolem0007,skolem0005)|skolem0005=X1476,inference(resolution,[status(thm)],[c1175, c71])).
% 1.54/1.74  cnf(c488,plain,skolem0001!=X1065|skolem0006!=X1066|skolem0004!=X1067|agent(X1065,X1066,X1067),inference(resolution,[status(thm)],[c31, c52])).
% 1.54/1.74  cnf(c1229,plain,skolem0001!=X1468|skolem0006!=X1467|agent(X1468,X1467,skolem0004),inference(resolution,[status(thm)],[c488, reflexivity])).
% 1.54/1.74  cnf(c1507,plain,skolem0001!=X1472|agent(X1472,skolem0006,skolem0004),inference(resolution,[status(thm)],[c1229, reflexivity])).
% 1.54/1.74  cnf(c467,plain,skolem0001!=X1040|skolem0006!=X1042|skolem0007!=X1041|theme(X1040,X1042,X1041),inference(resolution,[status(thm)],[c29, c53])).
% 1.54/1.74  cnf(c1213,plain,skolem0001!=X1464|skolem0006!=X1465|theme(X1464,X1465,skolem0007),inference(resolution,[status(thm)],[c467, reflexivity])).
% 1.54/1.74  cnf(c1505,plain,skolem0001!=X1466|theme(X1466,skolem0006,skolem0007),inference(resolution,[status(thm)],[c1213, reflexivity])).
% 1.54/1.74  cnf(c1280,plain,~accessible_world(skolem0007,X1463)|be(X1463,skolem0009,skolem0002,skolem0008),inference(resolution,[status(thm)],[c1277, c77])).
% 1.54/1.74  cnf(c1171,plain,~entity(skolem0007,skolem0002)|~forename(skolem0007,X1462)|~of(skolem0007,X1462,skolem0002)|~forename(skolem0007,skolem0003)|skolem0003=X1462,inference(resolution,[status(thm)],[c1169, c71])).
% 1.54/1.74  cnf(c0,axiom,X209!=X212|X211!=X210|~vincent_forename(X209,X211)|vincent_forename(X212,X210),theory(equality)).
% 1.54/1.74  cnf(c49,negated_conjecture,vincent_forename(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.74  fof(ax35,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&vincent_forename(V,U))=>vincent_forename(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax35)).
% 1.54/1.74  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.54/1.74  fof(c175,plain,(![X131]:(![X132]:(![X133]:((~accessible_world(X132,X133)|~vincent_forename(X132,X131))|vincent_forename(X133,X131))))),inference(variable_rename,[status(thm)],[c174])).
% 1.54/1.74  cnf(c176,plain,~accessible_world(X621,X620)|~vincent_forename(X621,X619)|vincent_forename(X620,X619),inference(split_conjunct,[status(thm)],[c175])).
% 1.54/1.74  cnf(c880,plain,~accessible_world(skolem0001,X768)|vincent_forename(X768,skolem0005),inference(resolution,[status(thm)],[c176, c49])).
% 1.54/1.74  cnf(c1044,plain,vincent_forename(skolem0007,skolem0005),inference(resolution,[status(thm)],[c880, c57])).
% 1.54/1.74  cnf(c1046,plain,skolem0007!=X1459|skolem0005!=X1460|vincent_forename(X1459,X1460),inference(resolution,[status(thm)],[c1044, c0])).
% 1.54/1.74  cnf(c1502,plain,skolem0007!=X1461|vincent_forename(X1461,skolem0005),inference(resolution,[status(thm)],[c1046, reflexivity])).
% 1.54/1.74  cnf(c2,axiom,X227!=X230|X229!=X228|~proposition(X227,X229)|proposition(X230,X228),theory(equality)).
% 1.54/1.74  cnf(c51,negated_conjecture,proposition(skolem0001,skolem0007),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.74  fof(ax36,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&proposition(V,U))=>proposition(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax36)).
% 1.54/1.74  fof(c171,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~proposition(V,U))|proposition(W,U))))),inference(fof_nnf,[status(thm)],[ax36])).
% 1.54/1.74  fof(c172,plain,(![X128]:(![X129]:(![X130]:((~accessible_world(X129,X130)|~proposition(X129,X128))|proposition(X130,X128))))),inference(variable_rename,[status(thm)],[c171])).
% 1.54/1.74  cnf(c173,plain,~accessible_world(X618,X616)|~proposition(X618,X617)|proposition(X616,X617),inference(split_conjunct,[status(thm)],[c172])).
% 1.54/1.74  cnf(c869,plain,~accessible_world(skolem0001,X767)|proposition(X767,skolem0007),inference(resolution,[status(thm)],[c173, c51])).
% 1.54/1.74  cnf(c1040,plain,proposition(skolem0007,skolem0007),inference(resolution,[status(thm)],[c869, c57])).
% 1.54/1.74  cnf(c1043,plain,skolem0007!=X1453|skolem0007!=X1452|proposition(X1453,X1452),inference(resolution,[status(thm)],[c1040, c2])).
% 1.54/1.74  cnf(c1498,plain,skolem0007!=X1458|proposition(X1458,skolem0007),inference(resolution,[status(thm)],[c1043, reflexivity])).
% 1.54/1.74  cnf(c1497,plain,skolem0007!=X1454|proposition(X1454,X1454),inference(factor,[status(thm)],[c1043])).
% 1.54/1.74  cnf(c30,axiom,X418!=X421|X420!=X419|~think_believe_consider(X418,X420)|think_believe_consider(X421,X419),theory(equality)).
% 1.54/1.74  cnf(c56,negated_conjecture,think_believe_consider(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.74  fof(ax38,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&think_believe_consider(V,U))=>think_believe_consider(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax38)).
% 1.54/1.74  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.54/1.74  fof(c166,plain,(![X121]:(![X122]:(![X123]:((~accessible_world(X122,X123)|~think_believe_consider(X122,X121))|think_believe_consider(X123,X121))))),inference(variable_rename,[status(thm)],[c165])).
% 1.54/1.74  cnf(c167,plain,~accessible_world(X610,X611)|~think_believe_consider(X610,X609)|think_believe_consider(X611,X609),inference(split_conjunct,[status(thm)],[c166])).
% 1.54/1.74  cnf(c849,plain,~accessible_world(skolem0001,X763)|think_believe_consider(X763,skolem0006),inference(resolution,[status(thm)],[c167, c56])).
% 1.54/1.74  cnf(c1036,plain,think_believe_consider(skolem0007,skolem0006),inference(resolution,[status(thm)],[c849, c57])).
% 1.54/1.74  cnf(c1037,plain,skolem0007!=X1446|skolem0006!=X1447|think_believe_consider(X1446,X1447),inference(resolution,[status(thm)],[c1036, c30])).
% 1.54/1.74  cnf(c1494,plain,skolem0007!=X1451|think_believe_consider(X1451,skolem0006),inference(resolution,[status(thm)],[c1037, reflexivity])).
% 1.54/1.74  cnf(c1030,plain,~think_believe_consider(skolem0007,X1448)|~proposition(skolem0007,X1449)|~theme(skolem0007,X1448,X1449)|~agent(skolem0007,X1448,skolem0004)|~think_believe_consider(skolem0007,skolem0010(skolem0004))|~proposition(skolem0007,X1450)|~theme(skolem0007,skolem0010(skolem0004),X1450)|X1449=X1450,inference(resolution,[status(thm)],[c815, c74])).
% 1.54/1.74  cnf(c1031,plain,~accessible_world(skolem0007,X1445)|agent(X1445,skolem0010(skolem0004),skolem0004),inference(resolution,[status(thm)],[c815, c164])).
% 1.54/1.74  cnf(c32,axiom,X433!=X436|X435!=X434|~present(X433,X435)|present(X436,X434),theory(equality)).
% 1.54/1.74  cnf(c55,negated_conjecture,present(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.74  fof(ax40,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&present(V,U))=>present(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax40)).
% 1.54/1.74  fof(c159,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~present(V,U))|present(W,U))))),inference(fof_nnf,[status(thm)],[ax40])).
% 1.54/1.74  fof(c160,plain,(![X114]:(![X115]:(![X116]:((~accessible_world(X115,X116)|~present(X115,X114))|present(X116,X114))))),inference(variable_rename,[status(thm)],[c159])).
% 1.54/1.74  cnf(c161,plain,~accessible_world(X602,X603)|~present(X602,X604)|present(X603,X604),inference(split_conjunct,[status(thm)],[c160])).
% 1.54/1.74  cnf(c811,plain,~accessible_world(skolem0001,X749)|present(X749,skolem0006),inference(resolution,[status(thm)],[c161, c55])).
% 1.54/1.74  cnf(c1027,plain,present(skolem0007,skolem0006),inference(resolution,[status(thm)],[c811, c57])).
% 1.54/1.74  cnf(c1028,plain,skolem0007!=X1442|skolem0006!=X1443|present(X1442,X1443),inference(resolution,[status(thm)],[c1027, c32])).
% 1.54/1.74  cnf(c1492,plain,skolem0007!=X1444|present(X1444,skolem0006),inference(resolution,[status(thm)],[c1028, reflexivity])).
% 1.54/1.74  cnf(c6,axiom,X257!=X260|X259!=X258|~jules_forename(X257,X259)|jules_forename(X260,X258),theory(equality)).
% 1.54/1.74  cnf(c45,negated_conjecture,jules_forename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.74  fof(ax43,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&jules_forename(V,U))=>jules_forename(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax43)).
% 1.54/1.74  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.54/1.74  fof(c151,plain,(![X104]:(![X105]:(![X106]:((~accessible_world(X105,X106)|~jules_forename(X105,X104))|jules_forename(X106,X104))))),inference(variable_rename,[status(thm)],[c150])).
% 1.54/1.74  cnf(c152,plain,~accessible_world(X591,X593)|~jules_forename(X591,X592)|jules_forename(X593,X592),inference(split_conjunct,[status(thm)],[c151])).
% 1.54/1.74  cnf(c778,plain,~accessible_world(skolem0001,X745)|jules_forename(X745,skolem0003),inference(resolution,[status(thm)],[c152, c45])).
% 1.54/1.74  cnf(c1022,plain,jules_forename(skolem0007,skolem0003),inference(resolution,[status(thm)],[c778, c57])).
% 1.54/1.74  cnf(c1024,plain,skolem0007!=X1436|skolem0003!=X1437|jules_forename(X1436,X1437),inference(resolution,[status(thm)],[c1022, c6])).
% 1.54/1.74  cnf(c1489,plain,skolem0007!=X1438|jules_forename(X1438,skolem0003),inference(resolution,[status(thm)],[c1024, reflexivity])).
% 1.54/1.74  cnf(c1007,plain,~accessible_world(skolem0007,X1435)|agent(X1435,skolem0010(skolem0008),skolem0008),inference(resolution,[status(thm)],[c739, c164])).
% 1.54/1.74  cnf(c1006,plain,~think_believe_consider(skolem0007,X1432)|~proposition(skolem0007,X1433)|~theme(skolem0007,X1432,X1433)|~agent(skolem0007,X1432,skolem0008)|~think_believe_consider(skolem0007,skolem0010(skolem0008))|~proposition(skolem0007,X1434)|~theme(skolem0007,skolem0010(skolem0008),X1434)|X1433=X1434,inference(resolution,[status(thm)],[c739, c74])).
% 1.54/1.74  cnf(c10,axiom,X281!=X284|X283!=X282|~nonhuman(X281,X283)|nonhuman(X284,X282),theory(equality)).
% 1.54/1.74  fof(ax7,axiom,(![U]:(![V]:(abstraction(U,V)=>nonhuman(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax7)).
% 1.54/1.74  fof(c262,plain,(![U]:(![V]:(~abstraction(U,V)|nonhuman(U,V)))),inference(fof_nnf,[status(thm)],[ax7])).
% 1.54/1.74  fof(c263,plain,(![X188]:(![X189]:(~abstraction(X188,X189)|nonhuman(X188,X189)))),inference(variable_rename,[status(thm)],[c262])).
% 1.54/1.74  cnf(c264,plain,~abstraction(X347,X348)|nonhuman(X347,X348),inference(split_conjunct,[status(thm)],[c263])).
% 1.54/1.74  fof(ax9,axiom,(![U]:(![V]:(relation(U,V)=>abstraction(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax9)).
% 1.54/1.74  fof(c256,plain,(![U]:(![V]:(~relation(U,V)|abstraction(U,V)))),inference(fof_nnf,[status(thm)],[ax9])).
% 1.54/1.74  fof(c257,plain,(![X184]:(![X185]:(~relation(X184,X185)|abstraction(X184,X185)))),inference(variable_rename,[status(thm)],[c256])).
% 1.54/1.74  cnf(c258,plain,~relation(X335,X336)|abstraction(X335,X336),inference(split_conjunct,[status(thm)],[c257])).
% 1.54/1.74  fof(ax2,axiom,(![U]:(![V]:(proposition(U,V)=>relation(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax2)).
% 1.54/1.74  fof(c277,plain,(![U]:(![V]:(~proposition(U,V)|relation(U,V)))),inference(fof_nnf,[status(thm)],[ax2])).
% 1.54/1.74  fof(c278,plain,(![X198]:(![X199]:(~proposition(X198,X199)|relation(X198,X199)))),inference(variable_rename,[status(thm)],[c277])).
% 1.54/1.74  cnf(c279,plain,~proposition(X365,X366)|relation(X365,X366),inference(split_conjunct,[status(thm)],[c278])).
% 1.54/1.74  cnf(c421,plain,relation(skolem0001,skolem0007),inference(resolution,[status(thm)],[c279, c51])).
% 1.54/1.74  fof(ax47,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&relation(V,U))=>relation(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax47)).
% 1.54/1.74  fof(c138,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~relation(V,U))|relation(W,U))))),inference(fof_nnf,[status(thm)],[ax47])).
% 1.54/1.74  fof(c139,plain,(![X92]:(![X93]:(![X94]:((~accessible_world(X93,X94)|~relation(X93,X92))|relation(X94,X92))))),inference(variable_rename,[status(thm)],[c138])).
% 1.54/1.74  cnf(c140,plain,~accessible_world(X580,X579)|~relation(X580,X578)|relation(X579,X578),inference(split_conjunct,[status(thm)],[c139])).
% 1.54/1.74  cnf(c712,plain,~accessible_world(skolem0001,X708)|relation(X708,skolem0007),inference(resolution,[status(thm)],[c140, c421])).
% 1.54/1.74  cnf(c979,plain,relation(skolem0007,skolem0007),inference(resolution,[status(thm)],[c712, c57])).
% 1.54/1.74  cnf(c982,plain,abstraction(skolem0007,skolem0007),inference(resolution,[status(thm)],[c979, c258])).
% 1.54/1.74  cnf(c985,plain,nonhuman(skolem0007,skolem0007),inference(resolution,[status(thm)],[c982, c264])).
% 1.54/1.74  cnf(c995,plain,skolem0007!=X1428|skolem0007!=X1427|nonhuman(X1428,X1427),inference(resolution,[status(thm)],[c985, c10])).
% 1.54/1.74  cnf(c1484,plain,skolem0007!=X1431|nonhuman(X1431,skolem0007),inference(resolution,[status(thm)],[c995, reflexivity])).
% 1.54/1.74  cnf(c9,axiom,X275!=X278|X277!=X276|~general(X275,X277)|general(X278,X276),theory(equality)).
% 1.54/1.74  fof(ax6,axiom,(![U]:(![V]:(abstraction(U,V)=>general(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax6)).
% 1.54/1.74  fof(c265,plain,(![U]:(![V]:(~abstraction(U,V)|general(U,V)))),inference(fof_nnf,[status(thm)],[ax6])).
% 1.54/1.74  fof(c266,plain,(![X190]:(![X191]:(~abstraction(X190,X191)|general(X190,X191)))),inference(variable_rename,[status(thm)],[c265])).
% 1.54/1.74  cnf(c267,plain,~abstraction(X350,X349)|general(X350,X349),inference(split_conjunct,[status(thm)],[c266])).
% 1.54/1.74  cnf(c984,plain,general(skolem0007,skolem0007),inference(resolution,[status(thm)],[c982, c267])).
% 1.54/1.74  cnf(c990,plain,skolem0007!=X1423|skolem0007!=X1424|general(X1423,X1424),inference(resolution,[status(thm)],[c984, c9])).
% 1.54/1.74  cnf(c1480,plain,skolem0007!=X1430|general(X1430,skolem0007),inference(resolution,[status(thm)],[c990, reflexivity])).
% 1.54/1.74  cnf(c1483,plain,skolem0007!=X1429|nonhuman(X1429,X1429),inference(factor,[status(thm)],[c995])).
% 1.54/1.74  cnf(c7,axiom,X263!=X266|X265!=X264|~abstraction(X263,X265)|abstraction(X266,X264),theory(equality)).
% 1.54/1.74  cnf(c987,plain,skolem0007!=X1419|skolem0007!=X1418|abstraction(X1419,X1418),inference(resolution,[status(thm)],[c982, c7])).
% 1.54/1.74  cnf(c1475,plain,skolem0007!=X1426|abstraction(X1426,skolem0007),inference(resolution,[status(thm)],[c987, reflexivity])).
% 1.54/1.74  cnf(c1479,plain,skolem0007!=X1425|general(X1425,X1425),inference(factor,[status(thm)],[c990])).
% 1.54/1.74  cnf(c3,axiom,X235!=X238|X237!=X236|~relation(X235,X237)|relation(X238,X236),theory(equality)).
% 1.54/1.74  cnf(c981,plain,skolem0007!=X1417|skolem0007!=X1416|relation(X1417,X1416),inference(resolution,[status(thm)],[c979, c3])).
% 1.54/1.74  cnf(c1473,plain,skolem0007!=X1422|relation(X1422,skolem0007),inference(resolution,[status(thm)],[c981, reflexivity])).
% 1.54/1.74  cnf(c1474,plain,skolem0007!=X1421|abstraction(X1421,X1421),inference(factor,[status(thm)],[c987])).
% 1.54/1.74  cnf(c1472,plain,skolem0007!=X1420|relation(X1420,X1420),inference(factor,[status(thm)],[c981])).
% 1.54/1.74  fof(ax10,axiom,(![U]:(![V]:(relname(U,V)=>relation(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax10)).
% 1.54/1.74  fof(c253,plain,(![U]:(![V]:(~relname(U,V)|relation(U,V)))),inference(fof_nnf,[status(thm)],[ax10])).
% 1.54/1.74  fof(c254,plain,(![X182]:(![X183]:(~relname(X182,X183)|relation(X182,X183)))),inference(variable_rename,[status(thm)],[c253])).
% 1.54/1.74  cnf(c255,plain,~relname(X330,X329)|relation(X330,X329),inference(split_conjunct,[status(thm)],[c254])).
% 1.54/1.74  fof(ax11,axiom,(![U]:(![V]:(forename(U,V)=>relname(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax11)).
% 1.54/1.74  fof(c250,plain,(![U]:(![V]:(~forename(U,V)|relname(U,V)))),inference(fof_nnf,[status(thm)],[ax11])).
% 1.54/1.74  fof(c251,plain,(![X180]:(![X181]:(~forename(X180,X181)|relname(X180,X181)))),inference(variable_rename,[status(thm)],[c250])).
% 1.54/1.74  cnf(c252,plain,~forename(X328,X327)|relname(X328,X327),inference(split_conjunct,[status(thm)],[c251])).
% 1.54/1.74  cnf(c50,negated_conjecture,forename(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.74  fof(ax49,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&forename(V,U))=>forename(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax49)).
% 1.54/1.74  fof(c132,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~forename(V,U))|forename(W,U))))),inference(fof_nnf,[status(thm)],[ax49])).
% 1.54/1.74  fof(c133,plain,(![X86]:(![X87]:(![X88]:((~accessible_world(X87,X88)|~forename(X87,X86))|forename(X88,X86))))),inference(variable_rename,[status(thm)],[c132])).
% 1.54/1.74  cnf(c134,plain,~accessible_world(X573,X574)|~forename(X573,X572)|forename(X574,X572),inference(split_conjunct,[status(thm)],[c133])).
% 1.54/1.74  cnf(c692,plain,~accessible_world(skolem0001,X693)|forename(X693,skolem0005),inference(resolution,[status(thm)],[c134, c50])).
% 1.54/1.74  cnf(c950,plain,forename(skolem0007,skolem0005),inference(resolution,[status(thm)],[c692, c57])).
% 1.54/1.74  cnf(c951,plain,relname(skolem0007,skolem0005),inference(resolution,[status(thm)],[c950, c252])).
% 1.54/1.74  cnf(c958,plain,relation(skolem0007,skolem0005),inference(resolution,[status(thm)],[c951, c255])).
% 1.54/1.74  cnf(c961,plain,abstraction(skolem0007,skolem0005),inference(resolution,[status(thm)],[c958, c258])).
% 1.54/1.74  cnf(c964,plain,nonhuman(skolem0007,skolem0005),inference(resolution,[status(thm)],[c961, c264])).
% 1.54/1.74  cnf(c972,plain,skolem0007!=X1414|skolem0005!=X1413|nonhuman(X1414,X1413),inference(resolution,[status(thm)],[c964, c10])).
% 1.54/1.74  cnf(c1470,plain,skolem0007!=X1415|nonhuman(X1415,skolem0005),inference(resolution,[status(thm)],[c972, reflexivity])).
% 1.54/1.74  cnf(c963,plain,general(skolem0007,skolem0005),inference(resolution,[status(thm)],[c961, c267])).
% 1.54/1.74  cnf(c969,plain,skolem0007!=X1407|skolem0005!=X1408|general(X1407,X1408),inference(resolution,[status(thm)],[c963, c9])).
% 1.54/1.74  cnf(c1467,plain,skolem0007!=X1409|general(X1409,skolem0005),inference(resolution,[status(thm)],[c969, reflexivity])).
% 1.54/1.74  cnf(c966,plain,skolem0007!=X1405|skolem0005!=X1404|abstraction(X1405,X1404),inference(resolution,[status(thm)],[c961, c7])).
% 1.54/1.74  cnf(c1465,plain,skolem0007!=X1406|abstraction(X1406,skolem0005),inference(resolution,[status(thm)],[c966, reflexivity])).
% 1.54/1.74  cnf(c918,plain,~think_believe_consider(skolem0007,X1401)|~proposition(skolem0007,X1402)|~theme(skolem0007,X1401,X1402)|~agent(skolem0007,X1401,skolem0002)|~think_believe_consider(skolem0007,skolem0010(skolem0002))|~proposition(skolem0007,X1403)|~theme(skolem0007,skolem0010(skolem0002),X1403)|X1402=X1403,inference(resolution,[status(thm)],[c664, c74])).
% 1.54/1.74  cnf(c960,plain,skolem0007!=X1399|skolem0005!=X1398|relation(X1399,X1398),inference(resolution,[status(thm)],[c958, c3])).
% 1.54/1.74  cnf(c1462,plain,skolem0007!=X1400|relation(X1400,skolem0005),inference(resolution,[status(thm)],[c960, reflexivity])).
% 1.54/1.74  cnf(c27,axiom,X395!=X398|X397!=X396|~singleton(X395,X397)|singleton(X398,X396),theory(equality)).
% 1.54/1.74  fof(ax28,axiom,(![U]:(![V]:(thing(U,V)=>singleton(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax28)).
% 1.54/1.74  fof(c199,plain,(![U]:(![V]:(~thing(U,V)|singleton(U,V)))),inference(fof_nnf,[status(thm)],[ax28])).
% 1.54/1.74  fof(c200,plain,(![X146]:(![X147]:(~thing(X146,X147)|singleton(X146,X147)))),inference(variable_rename,[status(thm)],[c199])).
% 1.54/1.74  cnf(c201,plain,~thing(X234,X233)|singleton(X234,X233),inference(split_conjunct,[status(thm)],[c200])).
% 1.54/1.74  fof(ax29,axiom,(![U]:(![V]:(eventuality(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax29)).
% 1.54/1.74  fof(c196,plain,(![U]:(![V]:(~eventuality(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax29])).
% 1.54/1.74  fof(c197,plain,(![X144]:(![X145]:(~eventuality(X144,X145)|thing(X144,X145)))),inference(variable_rename,[status(thm)],[c196])).
% 1.54/1.74  cnf(c198,plain,~eventuality(X232,X231)|thing(X232,X231),inference(split_conjunct,[status(thm)],[c197])).
% 1.54/1.74  fof(ax23,axiom,(![U]:(![V]:(event(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax23)).
% 1.54/1.74  fof(c214,plain,(![U]:(![V]:(~event(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax23])).
% 1.54/1.74  fof(c215,plain,(![X156]:(![X157]:(~event(X156,X157)|eventuality(X156,X157)))),inference(variable_rename,[status(thm)],[c214])).
% 1.54/1.74  cnf(c216,plain,~event(X251,X252)|eventuality(X251,X252),inference(split_conjunct,[status(thm)],[c215])).
% 1.54/1.74  cnf(c58,negated_conjecture,~man(skolem0007,X405)|event(skolem0007,skolem0010(X405)),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.74  cnf(c813,plain,event(skolem0007,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c809, c58])).
% 1.54/1.74  cnf(c854,plain,eventuality(skolem0007,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c813, c216])).
% 1.54/1.74  cnf(c865,plain,thing(skolem0007,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c854, c198])).
% 1.54/1.74  cnf(c874,plain,singleton(skolem0007,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c865, c201])).
% 1.54/1.74  cnf(c879,plain,skolem0007!=X1395|skolem0010(skolem0004)!=X1396|singleton(X1395,X1396),inference(resolution,[status(thm)],[c874, c27])).
% 1.54/1.74  cnf(c1460,plain,skolem0007!=X1397|singleton(X1397,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c879, reflexivity])).
% 1.54/1.74  cnf(c12,axiom,X293!=X296|X295!=X294|~relname(X293,X295)|relname(X296,X294),theory(equality)).
% 1.54/1.74  cnf(c957,plain,skolem0007!=X1392|skolem0005!=X1393|relname(X1392,X1393),inference(resolution,[status(thm)],[c951, c12])).
% 1.54/1.74  cnf(c1458,plain,skolem0007!=X1394|relname(X1394,skolem0005),inference(resolution,[status(thm)],[c957, reflexivity])).
% 1.54/1.74  cnf(c23,axiom,X367!=X370|X369!=X368|~specific(X367,X369)|specific(X370,X368),theory(equality)).
% 1.54/1.74  fof(ax27,axiom,(![U]:(![V]:(eventuality(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax27)).
% 1.54/1.74  fof(c202,plain,(![U]:(![V]:(~eventuality(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax27])).
% 1.54/1.74  fof(c203,plain,(![X148]:(![X149]:(~eventuality(X148,X149)|specific(X148,X149)))),inference(variable_rename,[status(thm)],[c202])).
% 1.54/1.74  cnf(c204,plain,~eventuality(X240,X239)|specific(X240,X239),inference(split_conjunct,[status(thm)],[c203])).
% 1.54/1.74  cnf(c866,plain,specific(skolem0007,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c854, c204])).
% 1.54/1.74  cnf(c876,plain,skolem0007!=X1389|skolem0010(skolem0004)!=X1390|specific(X1389,X1390),inference(resolution,[status(thm)],[c866, c23])).
% 1.54/1.74  cnf(c1456,plain,skolem0007!=X1391|specific(X1391,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c876, reflexivity])).
% 1.54/1.74  cnf(c1,axiom,X213!=X216|X215!=X214|~forename(X213,X215)|forename(X216,X214),theory(equality)).
% 1.54/1.74  cnf(c953,plain,skolem0007!=X1386|skolem0005!=X1387|forename(X1386,X1387),inference(resolution,[status(thm)],[c950, c1])).
% 1.54/1.74  cnf(c1454,plain,skolem0007!=X1388|forename(X1388,skolem0005),inference(resolution,[status(thm)],[c953, reflexivity])).
% 1.54/1.74  cnf(c11,axiom,X287!=X290|X289!=X288|~thing(X287,X289)|thing(X290,X288),theory(equality)).
% 1.54/1.74  cnf(c873,plain,skolem0007!=X1383|skolem0010(skolem0004)!=X1384|thing(X1383,X1384),inference(resolution,[status(thm)],[c865, c11])).
% 1.54/1.74  cnf(c1452,plain,skolem0007!=X1385|thing(X1385,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c873, reflexivity])).
% 1.54/1.74  cnf(c46,negated_conjecture,forename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.74  cnf(c691,plain,~accessible_world(skolem0001,X688)|forename(X688,skolem0003),inference(resolution,[status(thm)],[c134, c46])).
% 1.54/1.74  cnf(c926,plain,forename(skolem0007,skolem0003),inference(resolution,[status(thm)],[c691, c57])).
% 1.54/1.74  cnf(c927,plain,relname(skolem0007,skolem0003),inference(resolution,[status(thm)],[c926, c252])).
% 1.54/1.74  cnf(c933,plain,relation(skolem0007,skolem0003),inference(resolution,[status(thm)],[c927, c255])).
% 1.54/1.74  cnf(c936,plain,abstraction(skolem0007,skolem0003),inference(resolution,[status(thm)],[c933, c258])).
% 1.54/1.74  cnf(c939,plain,nonhuman(skolem0007,skolem0003),inference(resolution,[status(thm)],[c936, c264])).
% 1.54/1.74  cnf(c947,plain,skolem0007!=X1381|skolem0003!=X1380|nonhuman(X1381,X1380),inference(resolution,[status(thm)],[c939, c10])).
% 1.54/1.74  cnf(c1450,plain,skolem0007!=X1382|nonhuman(X1382,skolem0003),inference(resolution,[status(thm)],[c947, reflexivity])).
% 1.54/1.74  cnf(c26,axiom,X387!=X390|X389!=X388|~nonexistent(X387,X389)|nonexistent(X390,X388),theory(equality)).
% 1.54/1.74  fof(ax26,axiom,(![U]:(![V]:(eventuality(U,V)=>nonexistent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax26)).
% 1.54/1.74  fof(c205,plain,(![U]:(![V]:(~eventuality(U,V)|nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[ax26])).
% 1.54/1.74  fof(c206,plain,(![X150]:(![X151]:(~eventuality(X150,X151)|nonexistent(X150,X151)))),inference(variable_rename,[status(thm)],[c205])).
% 1.54/1.74  cnf(c207,plain,~eventuality(X242,X241)|nonexistent(X242,X241),inference(split_conjunct,[status(thm)],[c206])).
% 1.54/1.74  cnf(c864,plain,nonexistent(skolem0007,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c854, c207])).
% 1.54/1.74  cnf(c872,plain,skolem0007!=X1377|skolem0010(skolem0004)!=X1378|nonexistent(X1377,X1378),inference(resolution,[status(thm)],[c864, c26])).
% 1.54/1.74  cnf(c1448,plain,skolem0007!=X1379|nonexistent(X1379,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c872, reflexivity])).
% 1.54/1.74  cnf(c938,plain,general(skolem0007,skolem0003),inference(resolution,[status(thm)],[c936, c267])).
% 1.54/1.74  cnf(c944,plain,skolem0007!=X1374|skolem0003!=X1375|general(X1374,X1375),inference(resolution,[status(thm)],[c938, c9])).
% 1.54/1.74  cnf(c1446,plain,skolem0007!=X1376|general(X1376,skolem0003),inference(resolution,[status(thm)],[c944, reflexivity])).
% 1.54/1.74  cnf(c8,axiom,X269!=X272|X271!=X270|~unisex(X269,X271)|unisex(X272,X270),theory(equality)).
% 1.54/1.74  fof(ax25,axiom,(![U]:(![V]:(eventuality(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax25)).
% 1.54/1.74  fof(c208,plain,(![U]:(![V]:(~eventuality(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax25])).
% 1.54/1.74  fof(c209,plain,(![X152]:(![X153]:(~eventuality(X152,X153)|unisex(X152,X153)))),inference(variable_rename,[status(thm)],[c208])).
% 1.54/1.74  cnf(c210,plain,~eventuality(X248,X247)|unisex(X248,X247),inference(split_conjunct,[status(thm)],[c209])).
% 1.54/1.74  cnf(c863,plain,unisex(skolem0007,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c854, c210])).
% 1.54/1.74  cnf(c867,plain,skolem0007!=X1371|skolem0010(skolem0004)!=X1372|unisex(X1371,X1372),inference(resolution,[status(thm)],[c863, c8])).
% 1.54/1.74  cnf(c1444,plain,skolem0007!=X1373|unisex(X1373,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c867, reflexivity])).
% 1.54/1.74  cnf(c941,plain,skolem0007!=X1369|skolem0003!=X1368|abstraction(X1369,X1368),inference(resolution,[status(thm)],[c936, c7])).
% 1.54/1.74  cnf(c1442,plain,skolem0007!=X1370|abstraction(X1370,skolem0003),inference(resolution,[status(thm)],[c941, reflexivity])).
% 1.54/1.74  cnf(c24,axiom,X371!=X374|X373!=X372|~eventuality(X371,X373)|eventuality(X374,X372),theory(equality)).
% 1.54/1.74  cnf(c862,plain,skolem0007!=X1366|skolem0010(skolem0004)!=X1365|eventuality(X1366,X1365),inference(resolution,[status(thm)],[c854, c24])).
% 1.54/1.74  cnf(c1440,plain,skolem0007!=X1367|eventuality(X1367,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c862, reflexivity])).
% 1.54/1.74  cnf(c935,plain,skolem0007!=X1363|skolem0003!=X1362|relation(X1363,X1362),inference(resolution,[status(thm)],[c933, c3])).
% 1.54/1.74  cnf(c1438,plain,skolem0007!=X1364|relation(X1364,skolem0003),inference(resolution,[status(thm)],[c935, reflexivity])).
% 1.54/1.74  cnf(c60,negated_conjecture,~man(skolem0007,X406)|present(skolem0007,skolem0010(X406)),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.74  cnf(c819,plain,present(skolem0007,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c809, c60])).
% 1.54/1.74  cnf(c859,plain,skolem0007!=X1359|skolem0010(skolem0004)!=X1360|present(X1359,X1360),inference(resolution,[status(thm)],[c819, c32])).
% 1.54/1.74  cnf(c1436,plain,skolem0007!=X1361|present(X1361,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c859, reflexivity])).
% 1.54/1.74  cnf(c932,plain,skolem0007!=X1356|skolem0003!=X1357|relname(X1356,X1357),inference(resolution,[status(thm)],[c927, c12])).
% 1.54/1.74  cnf(c1434,plain,skolem0007!=X1358|relname(X1358,skolem0003),inference(resolution,[status(thm)],[c932, reflexivity])).
% 1.54/1.74  cnf(c4,axiom,X243!=X246|X245!=X244|~smoke(X243,X245)|smoke(X246,X244),theory(equality)).
% 1.54/1.74  cnf(c61,negated_conjecture,~man(skolem0007,X407)|smoke(skolem0007,skolem0010(X407)),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.74  cnf(c818,plain,smoke(skolem0007,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c809, c61])).
% 1.54/1.74  cnf(c857,plain,skolem0007!=X1354|skolem0010(skolem0004)!=X1353|smoke(X1354,X1353),inference(resolution,[status(thm)],[c818, c4])).
% 1.54/1.74  cnf(c1432,plain,skolem0007!=X1355|smoke(X1355,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c857, reflexivity])).
% 1.54/1.74  cnf(c929,plain,skolem0007!=X1350|skolem0003!=X1351|forename(X1350,X1351),inference(resolution,[status(thm)],[c926, c1])).
% 1.54/1.74  cnf(c1430,plain,skolem0007!=X1352|forename(X1352,skolem0003),inference(resolution,[status(thm)],[c929, reflexivity])).
% 1.54/1.74  cnf(c5,axiom,X253!=X256|X255!=X254|~event(X253,X255)|event(X256,X254),theory(equality)).
% 1.54/1.74  cnf(c853,plain,skolem0007!=X1348|skolem0010(skolem0004)!=X1347|event(X1348,X1347),inference(resolution,[status(thm)],[c813, c5])).
% 1.54/1.74  cnf(c1428,plain,skolem0007!=X1349|event(X1349,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c853, reflexivity])).
% 1.54/1.74  cnf(c919,plain,~accessible_world(skolem0007,X1346)|agent(X1346,skolem0010(skolem0002),skolem0002),inference(resolution,[status(thm)],[c664, c164])).
% 1.54/1.74  cnf(c22,axiom,X357!=X360|X359!=X358|~existent(X357,X359)|existent(X360,X358),theory(equality)).
% 1.54/1.74  fof(ax17,axiom,(![U]:(![V]:(entity(U,V)=>existent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax17)).
% 1.54/1.74  fof(c232,plain,(![U]:(![V]:(~entity(U,V)|existent(U,V)))),inference(fof_nnf,[status(thm)],[ax17])).
% 1.54/1.74  fof(c233,plain,(![X168]:(![X169]:(~entity(X168,X169)|existent(X168,X169)))),inference(variable_rename,[status(thm)],[c232])).
% 1.54/1.74  cnf(c234,plain,~entity(X292,X291)|existent(X292,X291),inference(split_conjunct,[status(thm)],[c233])).
% 1.54/1.74  fof(ax20,axiom,(![U]:(![V]:(organism(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax20)).
% 1.54/1.74  fof(c223,plain,(![U]:(![V]:(~organism(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax20])).
% 1.54/1.74  fof(c224,plain,(![X162]:(![X163]:(~organism(X162,X163)|entity(X162,X163)))),inference(variable_rename,[status(thm)],[c223])).
% 1.54/1.74  cnf(c225,plain,~organism(X273,X274)|entity(X273,X274),inference(split_conjunct,[status(thm)],[c224])).
% 1.54/1.74  fof(ax21,axiom,(![U]:(![V]:(human_person(U,V)=>organism(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax21)).
% 1.54/1.74  fof(c220,plain,(![U]:(![V]:(~human_person(U,V)|organism(U,V)))),inference(fof_nnf,[status(thm)],[ax21])).
% 1.54/1.74  fof(c221,plain,(![X160]:(![X161]:(~human_person(X160,X161)|organism(X160,X161)))),inference(variable_rename,[status(thm)],[c220])).
% 1.54/1.74  cnf(c222,plain,~human_person(X268,X267)|organism(X268,X267),inference(split_conjunct,[status(thm)],[c221])).
% 1.54/1.74  fof(ax22,axiom,(![U]:(![V]:(man(U,V)=>human_person(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax22)).
% 1.54/1.74  fof(c217,plain,(![U]:(![V]:(~man(U,V)|human_person(U,V)))),inference(fof_nnf,[status(thm)],[ax22])).
% 1.54/1.74  fof(c218,plain,(![X158]:(![X159]:(~man(X158,X159)|human_person(X158,X159)))),inference(variable_rename,[status(thm)],[c217])).
% 1.54/1.74  cnf(c219,plain,~man(X262,X261)|human_person(X262,X261),inference(split_conjunct,[status(thm)],[c218])).
% 1.54/1.74  cnf(c820,plain,human_person(skolem0007,skolem0004),inference(resolution,[status(thm)],[c809, c219])).
% 1.54/1.74  cnf(c826,plain,organism(skolem0007,skolem0004),inference(resolution,[status(thm)],[c820, c222])).
% 1.54/1.74  cnf(c832,plain,entity(skolem0007,skolem0004),inference(resolution,[status(thm)],[c826, c225])).
% 1.54/1.74  cnf(c844,plain,existent(skolem0007,skolem0004),inference(resolution,[status(thm)],[c832, c234])).
% 1.54/1.74  cnf(c850,plain,skolem0007!=X1343|skolem0004!=X1342|existent(X1343,X1342),inference(resolution,[status(thm)],[c844, c22])).
% 1.54/1.74  cnf(c1425,plain,skolem0007!=X1345|existent(X1345,skolem0004),inference(resolution,[status(thm)],[c850, reflexivity])).
% 1.54/1.74  cnf(c20,axiom,X343!=X346|X345!=X344|~impartial(X343,X345)|impartial(X346,X344),theory(equality)).
% 1.54/1.74  fof(ax16,axiom,(![U]:(![V]:(organism(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax16)).
% 1.54/1.74  fof(c235,plain,(![U]:(![V]:(~organism(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax16])).
% 1.54/1.74  fof(c236,plain,(![X170]:(![X171]:(~organism(X170,X171)|impartial(X170,X171)))),inference(variable_rename,[status(thm)],[c235])).
% 1.54/1.74  cnf(c237,plain,~organism(X298,X297)|impartial(X298,X297),inference(split_conjunct,[status(thm)],[c236])).
% 1.54/1.74  cnf(c836,plain,impartial(skolem0007,skolem0004),inference(resolution,[status(thm)],[c826, c237])).
% 1.54/1.74  cnf(c847,plain,skolem0007!=X1340|skolem0004!=X1341|impartial(X1340,X1341),inference(resolution,[status(thm)],[c836, c20])).
% 1.54/1.74  cnf(c1424,plain,skolem0007!=X1344|impartial(X1344,skolem0004),inference(resolution,[status(thm)],[c847, reflexivity])).
% 1.54/1.74  cnf(c737,plain,event(skolem0007,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c736, c58])).
% 1.54/1.74  cnf(c783,plain,eventuality(skolem0007,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c737, c216])).
% 1.54/1.74  cnf(c793,plain,thing(skolem0007,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c783, c198])).
% 1.54/1.74  cnf(c803,plain,singleton(skolem0007,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c793, c201])).
% 1.54/1.74  cnf(c808,plain,skolem0007!=X1336|skolem0010(skolem0008)!=X1337|singleton(X1336,X1337),inference(resolution,[status(thm)],[c803, c27])).
% 1.54/1.74  cnf(c1421,plain,skolem0007!=X1339|singleton(X1339,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c808, reflexivity])).
% 1.54/1.74  cnf(c19,axiom,X337!=X340|X339!=X338|~living(X337,X339)|living(X340,X338),theory(equality)).
% 1.54/1.74  fof(ax15,axiom,(![U]:(![V]:(organism(U,V)=>living(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax15)).
% 1.54/1.74  fof(c238,plain,(![U]:(![V]:(~organism(U,V)|living(U,V)))),inference(fof_nnf,[status(thm)],[ax15])).
% 1.54/1.74  fof(c239,plain,(![X172]:(![X173]:(~organism(X172,X173)|living(X172,X173)))),inference(variable_rename,[status(thm)],[c238])).
% 1.54/1.74  cnf(c240,plain,~organism(X299,X300)|living(X299,X300),inference(split_conjunct,[status(thm)],[c239])).
% 1.54/1.74  cnf(c834,plain,living(skolem0007,skolem0004),inference(resolution,[status(thm)],[c826, c240])).
% 1.54/1.74  cnf(c846,plain,skolem0007!=X1334|skolem0004!=X1335|living(X1334,X1335),inference(resolution,[status(thm)],[c834, c19])).
% 1.54/1.74  cnf(c1420,plain,skolem0007!=X1338|living(X1338,skolem0004),inference(resolution,[status(thm)],[c846, reflexivity])).
% 1.54/1.74  cnf(c794,plain,specific(skolem0007,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c783, c204])).
% 1.54/1.74  cnf(c805,plain,skolem0007!=X1330|skolem0010(skolem0008)!=X1331|specific(X1330,X1331),inference(resolution,[status(thm)],[c794, c23])).
% 1.54/1.74  cnf(c1417,plain,skolem0007!=X1333|specific(X1333,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c805, reflexivity])).
% 1.54/1.74  cnf(c21,axiom,X351!=X354|X353!=X352|~entity(X351,X353)|entity(X354,X352),theory(equality)).
% 1.54/1.74  cnf(c841,plain,skolem0007!=X1329|skolem0004!=X1328|entity(X1329,X1328),inference(resolution,[status(thm)],[c832, c21])).
% 1.54/1.74  cnf(c1416,plain,skolem0007!=X1332|entity(X1332,skolem0004),inference(resolution,[status(thm)],[c841, reflexivity])).
% 1.54/1.74  cnf(c802,plain,skolem0007!=X1324|skolem0010(skolem0008)!=X1325|thing(X1324,X1325),inference(resolution,[status(thm)],[c793, c11])).
% 1.54/1.74  cnf(c1413,plain,skolem0007!=X1327|thing(X1327,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c802, reflexivity])).
% 1.54/1.74  cnf(c17,axiom,X323!=X326|X325!=X324|~human(X323,X325)|human(X326,X324),theory(equality)).
% 1.54/1.74  fof(ax14,axiom,(![U]:(![V]:(human_person(U,V)=>human(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax14)).
% 1.54/1.74  fof(c241,plain,(![U]:(![V]:(~human_person(U,V)|human(U,V)))),inference(fof_nnf,[status(thm)],[ax14])).
% 1.54/1.74  fof(c242,plain,(![X174]:(![X175]:(~human_person(X174,X175)|human(X174,X175)))),inference(variable_rename,[status(thm)],[c241])).
% 1.54/1.74  cnf(c243,plain,~human_person(X305,X306)|human(X305,X306),inference(split_conjunct,[status(thm)],[c242])).
% 1.54/1.74  cnf(c828,plain,human(skolem0007,skolem0004),inference(resolution,[status(thm)],[c820, c243])).
% 1.54/1.74  cnf(c839,plain,skolem0007!=X1322|skolem0004!=X1323|human(X1322,X1323),inference(resolution,[status(thm)],[c828, c17])).
% 1.54/1.74  cnf(c1412,plain,skolem0007!=X1326|human(X1326,skolem0004),inference(resolution,[status(thm)],[c839, reflexivity])).
% 1.54/1.74  cnf(c792,plain,nonexistent(skolem0007,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c783, c207])).
% 1.54/1.74  cnf(c799,plain,skolem0007!=X1318|skolem0010(skolem0008)!=X1319|nonexistent(X1318,X1319),inference(resolution,[status(thm)],[c792, c26])).
% 1.54/1.74  cnf(c1409,plain,skolem0007!=X1321|nonexistent(X1321,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c799, reflexivity])).
% 1.54/1.74  cnf(c18,axiom,X331!=X334|X333!=X332|~organism(X331,X333)|organism(X334,X332),theory(equality)).
% 1.54/1.74  cnf(c835,plain,skolem0007!=X1316|skolem0004!=X1317|organism(X1316,X1317),inference(resolution,[status(thm)],[c826, c18])).
% 1.54/1.74  cnf(c1408,plain,skolem0007!=X1320|organism(X1320,skolem0004),inference(resolution,[status(thm)],[c835, reflexivity])).
% 1.54/1.74  cnf(c791,plain,unisex(skolem0007,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c783, c210])).
% 1.54/1.74  cnf(c795,plain,skolem0007!=X1312|skolem0010(skolem0008)!=X1313|unisex(X1312,X1313),inference(resolution,[status(thm)],[c791, c8])).
% 1.54/1.74  cnf(c1405,plain,skolem0007!=X1315|unisex(X1315,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c795, reflexivity])).
% 1.54/1.74  cnf(c16,axiom,X319!=X322|X321!=X320|~animate(X319,X321)|animate(X322,X320),theory(equality)).
% 1.54/1.74  fof(ax13,axiom,(![U]:(![V]:(human_person(U,V)=>animate(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax13)).
% 1.54/1.74  fof(c244,plain,(![U]:(![V]:(~human_person(U,V)|animate(U,V)))),inference(fof_nnf,[status(thm)],[ax13])).
% 1.54/1.74  fof(c245,plain,(![X176]:(![X177]:(~human_person(X176,X177)|animate(X176,X177)))),inference(variable_rename,[status(thm)],[c244])).
% 1.54/1.74  cnf(c246,plain,~human_person(X316,X315)|animate(X316,X315),inference(split_conjunct,[status(thm)],[c245])).
% 1.54/1.74  cnf(c825,plain,animate(skolem0007,skolem0004),inference(resolution,[status(thm)],[c820, c246])).
% 1.54/1.74  cnf(c829,plain,skolem0007!=X1311|skolem0004!=X1310|animate(X1311,X1310),inference(resolution,[status(thm)],[c825, c16])).
% 1.54/1.74  cnf(c1404,plain,skolem0007!=X1314|animate(X1314,skolem0004),inference(resolution,[status(thm)],[c829, reflexivity])).
% 1.54/1.74  cnf(c790,plain,skolem0007!=X1307|skolem0010(skolem0008)!=X1306|eventuality(X1307,X1306),inference(resolution,[status(thm)],[c783, c24])).
% 1.54/1.74  cnf(c1401,plain,skolem0007!=X1309|eventuality(X1309,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c790, reflexivity])).
% 1.54/1.74  cnf(c15,axiom,X311!=X314|X313!=X312|~human_person(X311,X313)|human_person(X314,X312),theory(equality)).
% 1.54/1.74  cnf(c824,plain,skolem0007!=X1305|skolem0004!=X1304|human_person(X1305,X1304),inference(resolution,[status(thm)],[c820, c15])).
% 1.54/1.74  cnf(c1400,plain,skolem0007!=X1308|human_person(X1308,skolem0004),inference(resolution,[status(thm)],[c824, reflexivity])).
% 1.54/1.74  cnf(c743,plain,present(skolem0007,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c736, c60])).
% 1.54/1.74  cnf(c788,plain,skolem0007!=X1300|skolem0010(skolem0008)!=X1301|present(X1300,X1301),inference(resolution,[status(thm)],[c743, c32])).
% 1.54/1.74  cnf(c1397,plain,skolem0007!=X1303|present(X1303,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c788, reflexivity])).
% 1.54/1.74  cnf(c14,axiom,X307!=X310|X309!=X308|~male(X307,X309)|male(X310,X308),theory(equality)).
% 1.54/1.74  fof(ax12,axiom,(![U]:(![V]:(man(U,V)=>male(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax12)).
% 1.54/1.74  fof(c247,plain,(![U]:(![V]:(~man(U,V)|male(U,V)))),inference(fof_nnf,[status(thm)],[ax12])).
% 1.54/1.74  fof(c248,plain,(![X178]:(![X179]:(~man(X178,X179)|male(X178,X179)))),inference(variable_rename,[status(thm)],[c247])).
% 1.54/1.74  cnf(c249,plain,~man(X317,X318)|male(X317,X318),inference(split_conjunct,[status(thm)],[c248])).
% 1.54/1.74  cnf(c816,plain,male(skolem0007,skolem0004),inference(resolution,[status(thm)],[c809, c249])).
% 1.54/1.74  cnf(c821,plain,skolem0007!=X1299|skolem0004!=X1298|male(X1299,X1298),inference(resolution,[status(thm)],[c816, c14])).
% 1.54/1.74  cnf(c1396,plain,skolem0007!=X1302|male(X1302,skolem0004),inference(resolution,[status(thm)],[c821, reflexivity])).
% 1.54/1.74  cnf(c742,plain,smoke(skolem0007,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c736, c61])).
% 1.54/1.74  cnf(c784,plain,skolem0007!=X1295|skolem0010(skolem0008)!=X1294|smoke(X1295,X1294),inference(resolution,[status(thm)],[c742, c4])).
% 1.54/1.74  cnf(c1393,plain,skolem0007!=X1297|smoke(X1297,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c784, reflexivity])).
% 1.54/1.74  cnf(c13,axiom,X301!=X304|X303!=X302|~man(X301,X303)|man(X304,X302),theory(equality)).
% 1.54/1.74  cnf(c817,plain,skolem0007!=X1292|skolem0004!=X1293|man(X1292,X1293),inference(resolution,[status(thm)],[c809, c13])).
% 1.54/1.74  cnf(c1392,plain,skolem0007!=X1296|man(X1296,skolem0004),inference(resolution,[status(thm)],[c817, reflexivity])).
% 1.54/1.74  cnf(c782,plain,skolem0007!=X1288|skolem0010(skolem0008)!=X1287|event(X1288,X1287),inference(resolution,[status(thm)],[c737, c5])).
% 1.54/1.74  cnf(c1390,plain,skolem0007!=X1291|event(X1291,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c782, reflexivity])).
% 1.54/1.74  cnf(c744,plain,human_person(skolem0007,skolem0008),inference(resolution,[status(thm)],[c736, c219])).
% 1.54/1.74  cnf(c753,plain,organism(skolem0007,skolem0008),inference(resolution,[status(thm)],[c744, c222])).
% 1.54/1.74  cnf(c758,plain,entity(skolem0007,skolem0008),inference(resolution,[status(thm)],[c753, c225])).
% 1.54/1.74  cnf(c773,plain,existent(skolem0007,skolem0008),inference(resolution,[status(thm)],[c758, c234])).
% 1.54/1.74  cnf(c779,plain,skolem0007!=X1286|skolem0008!=X1285|existent(X1286,X1285),inference(resolution,[status(thm)],[c773, c22])).
% 1.54/1.74  cnf(c662,plain,event(skolem0007,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c661, c58])).
% 1.54/1.74  cnf(c708,plain,eventuality(skolem0007,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c662, c216])).
% 1.54/1.74  cnf(c719,plain,thing(skolem0007,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c708, c198])).
% 1.54/1.74  cnf(c727,plain,singleton(skolem0007,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c719, c201])).
% 1.54/1.74  cnf(c735,plain,skolem0007!=X1280|skolem0010(skolem0002)!=X1281|singleton(X1280,X1281),inference(resolution,[status(thm)],[c727, c27])).
% 1.54/1.74  cnf(c1386,plain,skolem0007!=X1284|singleton(X1284,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c735, reflexivity])).
% 1.54/1.74  cnf(c762,plain,impartial(skolem0007,skolem0008),inference(resolution,[status(thm)],[c753, c237])).
% 1.54/1.74  cnf(c776,plain,skolem0007!=X1278|skolem0008!=X1279|impartial(X1278,X1279),inference(resolution,[status(thm)],[c762, c20])).
% 1.54/1.74  cnf(c720,plain,specific(skolem0007,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c708, c204])).
% 1.54/1.74  cnf(c732,plain,skolem0007!=X1273|skolem0010(skolem0002)!=X1274|specific(X1273,X1274),inference(resolution,[status(thm)],[c720, c23])).
% 1.54/1.74  cnf(c1382,plain,skolem0007!=X1277|specific(X1277,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c732, reflexivity])).
% 1.54/1.74  cnf(c760,plain,living(skolem0007,skolem0008),inference(resolution,[status(thm)],[c753, c240])).
% 1.54/1.74  cnf(c775,plain,skolem0007!=X1271|skolem0008!=X1272|living(X1271,X1272),inference(resolution,[status(thm)],[c760, c19])).
% 1.54/1.75  cnf(c726,plain,skolem0007!=X1266|skolem0010(skolem0002)!=X1267|thing(X1266,X1267),inference(resolution,[status(thm)],[c719, c11])).
% 1.54/1.75  cnf(c1378,plain,skolem0007!=X1270|thing(X1270,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c726, reflexivity])).
% 1.54/1.75  cnf(c770,plain,skolem0007!=X1265|skolem0008!=X1264|entity(X1265,X1264),inference(resolution,[status(thm)],[c758, c21])).
% 1.54/1.75  cnf(c718,plain,nonexistent(skolem0007,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c708, c207])).
% 1.54/1.75  cnf(c725,plain,skolem0007!=X1259|skolem0010(skolem0002)!=X1260|nonexistent(X1259,X1260),inference(resolution,[status(thm)],[c718, c26])).
% 1.54/1.75  cnf(c1374,plain,skolem0007!=X1263|nonexistent(X1263,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c725, reflexivity])).
% 1.54/1.75  cnf(c755,plain,human(skolem0007,skolem0008),inference(resolution,[status(thm)],[c744, c243])).
% 1.54/1.75  cnf(c768,plain,skolem0007!=X1257|skolem0008!=X1258|human(X1257,X1258),inference(resolution,[status(thm)],[c755, c17])).
% 1.54/1.75  cnf(c717,plain,unisex(skolem0007,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c708, c210])).
% 1.54/1.75  cnf(c721,plain,skolem0007!=X1252|skolem0010(skolem0002)!=X1253|unisex(X1252,X1253),inference(resolution,[status(thm)],[c717, c8])).
% 1.54/1.75  cnf(c1370,plain,skolem0007!=X1256|unisex(X1256,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c721, reflexivity])).
% 1.54/1.75  cnf(c761,plain,skolem0007!=X1250|skolem0008!=X1251|organism(X1250,X1251),inference(resolution,[status(thm)],[c753, c18])).
% 1.54/1.75  cnf(c716,plain,skolem0007!=X1246|skolem0010(skolem0002)!=X1245|eventuality(X1246,X1245),inference(resolution,[status(thm)],[c708, c24])).
% 1.54/1.75  cnf(c1366,plain,skolem0007!=X1249|eventuality(X1249,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c716, reflexivity])).
% 1.54/1.75  cnf(c752,plain,animate(skolem0007,skolem0008),inference(resolution,[status(thm)],[c744, c246])).
% 1.54/1.75  cnf(c756,plain,skolem0007!=X1244|skolem0008!=X1243|animate(X1244,X1243),inference(resolution,[status(thm)],[c752, c16])).
% 1.54/1.75  cnf(c668,plain,present(skolem0007,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c661, c60])).
% 1.54/1.75  cnf(c711,plain,skolem0007!=X1238|skolem0010(skolem0002)!=X1239|present(X1238,X1239),inference(resolution,[status(thm)],[c668, c32])).
% 1.54/1.75  cnf(c1362,plain,skolem0007!=X1242|present(X1242,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c711, reflexivity])).
% 1.54/1.75  cnf(c751,plain,skolem0007!=X1237|skolem0008!=X1236|human_person(X1237,X1236),inference(resolution,[status(thm)],[c744, c15])).
% 1.54/1.75  cnf(c667,plain,smoke(skolem0007,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c661, c61])).
% 1.54/1.75  cnf(c709,plain,skolem0007!=X1232|skolem0010(skolem0002)!=X1231|smoke(X1232,X1231),inference(resolution,[status(thm)],[c667, c4])).
% 1.54/1.75  cnf(c1358,plain,skolem0007!=X1235|smoke(X1235,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c709, reflexivity])).
% 1.54/1.75  cnf(c740,plain,male(skolem0007,skolem0008),inference(resolution,[status(thm)],[c736, c249])).
% 1.54/1.75  cnf(c748,plain,skolem0007!=X1230|skolem0008!=X1229|male(X1230,X1229),inference(resolution,[status(thm)],[c740, c14])).
% 1.54/1.75  cnf(c707,plain,skolem0007!=X1225|skolem0010(skolem0002)!=X1224|event(X1225,X1224),inference(resolution,[status(thm)],[c662, c5])).
% 1.54/1.75  cnf(c1354,plain,skolem0007!=X1228|event(X1228,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c707, reflexivity])).
% 1.54/1.75  cnf(c741,plain,skolem0007!=X1222|skolem0008!=X1223|man(X1222,X1223),inference(resolution,[status(thm)],[c736, c13])).
% 1.54/1.75  cnf(c669,plain,human_person(skolem0007,skolem0002),inference(resolution,[status(thm)],[c661, c219])).
% 1.54/1.75  cnf(c678,plain,organism(skolem0007,skolem0002),inference(resolution,[status(thm)],[c669, c222])).
% 1.54/1.75  cnf(c683,plain,entity(skolem0007,skolem0002),inference(resolution,[status(thm)],[c678, c225])).
% 1.54/1.75  cnf(c697,plain,existent(skolem0007,skolem0002),inference(resolution,[status(thm)],[c683, c234])).
% 1.54/1.75  cnf(c704,plain,skolem0007!=X1219|skolem0002!=X1218|existent(X1219,X1218),inference(resolution,[status(thm)],[c697, c22])).
% 1.54/1.75  cnf(c1349,plain,skolem0007!=X1221|existent(X1221,skolem0002),inference(resolution,[status(thm)],[c704, reflexivity])).
% 1.54/1.75  cnf(c1348,plain,skolem0007!=X1220|existent(X1220,skolem0008),inference(resolution,[status(thm)],[c704, c447])).
% 1.54/1.75  cnf(c687,plain,impartial(skolem0007,skolem0002),inference(resolution,[status(thm)],[c678, c237])).
% 1.54/1.75  cnf(c700,plain,skolem0007!=X1214|skolem0002!=X1215|impartial(X1214,X1215),inference(resolution,[status(thm)],[c687, c20])).
% 1.54/1.75  cnf(c1345,plain,skolem0007!=X1217|impartial(X1217,skolem0002),inference(resolution,[status(thm)],[c700, reflexivity])).
% 1.54/1.75  cnf(c1344,plain,skolem0007!=X1216|impartial(X1216,skolem0008),inference(resolution,[status(thm)],[c700, c447])).
% 1.54/1.75  cnf(c685,plain,living(skolem0007,skolem0002),inference(resolution,[status(thm)],[c678, c240])).
% 1.54/1.75  cnf(c699,plain,skolem0007!=X1209|skolem0002!=X1210|living(X1209,X1210),inference(resolution,[status(thm)],[c685, c19])).
% 1.54/1.75  cnf(c1340,plain,skolem0007!=X1213|living(X1213,skolem0002),inference(resolution,[status(thm)],[c699, reflexivity])).
% 1.54/1.75  cnf(c1339,plain,skolem0007!=X1212|living(X1212,skolem0008),inference(resolution,[status(thm)],[c699, c447])).
% 1.54/1.75  cnf(c694,plain,skolem0007!=X1206|skolem0002!=X1205|entity(X1206,X1205),inference(resolution,[status(thm)],[c683, c21])).
% 1.54/1.75  cnf(c1336,plain,skolem0007!=X1211|entity(X1211,skolem0002),inference(resolution,[status(thm)],[c694, reflexivity])).
% 1.54/1.75  cnf(c1335,plain,skolem0007!=X1208|entity(X1208,skolem0008),inference(resolution,[status(thm)],[c694, c447])).
% 1.54/1.75  cnf(c680,plain,human(skolem0007,skolem0002),inference(resolution,[status(thm)],[c669, c243])).
% 1.54/1.75  cnf(c690,plain,skolem0007!=X1200|skolem0002!=X1201|human(X1200,X1201),inference(resolution,[status(thm)],[c680, c17])).
% 1.54/1.75  cnf(c1331,plain,skolem0007!=X1207|human(X1207,skolem0002),inference(resolution,[status(thm)],[c690, reflexivity])).
% 1.54/1.75  cnf(c1330,plain,skolem0007!=X1204|human(X1204,skolem0008),inference(resolution,[status(thm)],[c690, c447])).
% 1.54/1.75  cnf(c686,plain,skolem0007!=X1198|skolem0002!=X1199|organism(X1198,X1199),inference(resolution,[status(thm)],[c678, c18])).
% 1.54/1.75  cnf(c1329,plain,skolem0007!=X1203|organism(X1203,skolem0002),inference(resolution,[status(thm)],[c686, reflexivity])).
% 1.54/1.75  cnf(c1328,plain,skolem0007!=X1202|organism(X1202,skolem0008),inference(resolution,[status(thm)],[c686, c447])).
% 1.54/1.75  cnf(c677,plain,animate(skolem0007,skolem0002),inference(resolution,[status(thm)],[c669, c246])).
% 1.54/1.75  cnf(c681,plain,skolem0007!=X1195|skolem0002!=X1194|animate(X1195,X1194),inference(resolution,[status(thm)],[c677, c16])).
% 1.54/1.75  cnf(c1325,plain,skolem0007!=X1197|animate(X1197,skolem0002),inference(resolution,[status(thm)],[c681, reflexivity])).
% 1.54/1.75  cnf(c1324,plain,skolem0007!=X1196|animate(X1196,skolem0008),inference(resolution,[status(thm)],[c681, c447])).
% 1.54/1.75  cnf(c676,plain,skolem0007!=X1191|skolem0002!=X1190|human_person(X1191,X1190),inference(resolution,[status(thm)],[c669, c15])).
% 1.54/1.75  cnf(c1321,plain,skolem0007!=X1193|human_person(X1193,skolem0002),inference(resolution,[status(thm)],[c676, reflexivity])).
% 1.54/1.75  cnf(c1320,plain,skolem0007!=X1192|human_person(X1192,skolem0008),inference(resolution,[status(thm)],[c676, c447])).
% 1.54/1.75  cnf(c665,plain,male(skolem0007,skolem0002),inference(resolution,[status(thm)],[c661, c249])).
% 1.54/1.75  cnf(c670,plain,skolem0007!=X1186|skolem0002!=X1185|male(X1186,X1185),inference(resolution,[status(thm)],[c665, c14])).
% 1.54/1.75  cnf(c1316,plain,skolem0007!=X1189|male(X1189,skolem0002),inference(resolution,[status(thm)],[c670, reflexivity])).
% 1.54/1.75  cnf(c1315,plain,skolem0007!=X1188|male(X1188,skolem0008),inference(resolution,[status(thm)],[c670, c447])).
% 1.54/1.75  cnf(c666,plain,skolem0007!=X1182|skolem0002!=X1183|man(X1182,X1183),inference(resolution,[status(thm)],[c661, c13])).
% 1.54/1.75  cnf(c1313,plain,skolem0007!=X1187|man(X1187,skolem0002),inference(resolution,[status(thm)],[c666, reflexivity])).
% 1.54/1.75  cnf(c1312,plain,skolem0007!=X1184|man(X1184,skolem0008),inference(resolution,[status(thm)],[c666, c447])).
% 1.54/1.75  cnf(c54,negated_conjecture,event(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.75  fof(ax60,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&event(V,U))=>event(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax60)).
% 1.54/1.75  fof(c99,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~event(V,U))|event(W,U))))),inference(fof_nnf,[status(thm)],[ax60])).
% 1.54/1.75  fof(c100,plain,(![X53]:(![X54]:(![X55]:((~accessible_world(X54,X55)|~event(X54,X53))|event(X55,X53))))),inference(variable_rename,[status(thm)],[c99])).
% 1.54/1.75  cnf(c101,plain,~accessible_world(X511,X512)|~event(X511,X513)|event(X512,X513),inference(split_conjunct,[status(thm)],[c100])).
% 1.54/1.75  cnf(c599,plain,~accessible_world(skolem0001,X563)|event(X563,skolem0006),inference(resolution,[status(thm)],[c101, c54])).
% 1.54/1.75  cnf(c653,plain,event(skolem0007,skolem0006),inference(resolution,[status(thm)],[c599, c57])).
% 1.54/1.75  cnf(c655,plain,skolem0007!=X1180|skolem0006!=X1179|event(X1180,X1179),inference(resolution,[status(thm)],[c653, c5])).
% 1.54/1.75  cnf(c1310,plain,skolem0007!=X1181|event(X1181,skolem0006),inference(resolution,[status(thm)],[c655, reflexivity])).
% 1.54/1.75  fof(ax5,axiom,(![U]:(![V]:(abstraction(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax5)).
% 1.54/1.75  fof(c268,plain,(![U]:(![V]:(~abstraction(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax5])).
% 1.54/1.75  fof(c269,plain,(![X192]:(![X193]:(~abstraction(X192,X193)|unisex(X192,X193)))),inference(variable_rename,[status(thm)],[c268])).
% 1.54/1.75  cnf(c270,plain,~abstraction(X356,X355)|unisex(X356,X355),inference(split_conjunct,[status(thm)],[c269])).
% 1.54/1.75  cnf(c428,plain,abstraction(skolem0001,skolem0007),inference(resolution,[status(thm)],[c421, c258])).
% 1.54/1.75  cnf(c433,plain,unisex(skolem0001,skolem0007),inference(resolution,[status(thm)],[c428, c270])).
% 1.54/1.75  fof(ax61,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&unisex(V,U))=>unisex(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax61)).
% 1.54/1.75  fof(c96,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~unisex(V,U))|unisex(W,U))))),inference(fof_nnf,[status(thm)],[ax61])).
% 1.54/1.75  fof(c97,plain,(![X50]:(![X51]:(![X52]:((~accessible_world(X51,X52)|~unisex(X51,X50))|unisex(X52,X50))))),inference(variable_rename,[status(thm)],[c96])).
% 1.54/1.75  cnf(c98,plain,~accessible_world(X505,X507)|~unisex(X505,X506)|unisex(X507,X506),inference(split_conjunct,[status(thm)],[c97])).
% 1.54/1.75  cnf(c593,plain,~accessible_world(skolem0001,X557)|unisex(X557,skolem0007),inference(resolution,[status(thm)],[c98, c433])).
% 1.54/1.75  cnf(c646,plain,unisex(skolem0007,skolem0007),inference(resolution,[status(thm)],[c593, c57])).
% 1.54/1.75  cnf(c647,plain,skolem0007!=X1175|skolem0007!=X1176|unisex(X1175,X1176),inference(resolution,[status(thm)],[c646, c8])).
% 1.54/1.75  cnf(c1307,plain,skolem0007!=X1178|unisex(X1178,skolem0007),inference(resolution,[status(thm)],[c647, reflexivity])).
% 1.54/1.75  cnf(c1306,plain,skolem0007!=X1177|unisex(X1177,X1177),inference(factor,[status(thm)],[c647])).
% 1.54/1.75  cnf(c374,plain,relname(skolem0001,skolem0005),inference(resolution,[status(thm)],[c252, c50])).
% 1.54/1.75  cnf(c378,plain,relation(skolem0001,skolem0005),inference(resolution,[status(thm)],[c255, c374])).
% 1.54/1.75  cnf(c385,plain,abstraction(skolem0001,skolem0005),inference(resolution,[status(thm)],[c258, c378])).
% 1.54/1.75  cnf(c413,plain,unisex(skolem0001,skolem0005),inference(resolution,[status(thm)],[c270, c385])).
% 1.54/1.75  cnf(c592,plain,~accessible_world(skolem0001,X556)|unisex(X556,skolem0005),inference(resolution,[status(thm)],[c98, c413])).
% 1.54/1.75  cnf(c643,plain,unisex(skolem0007,skolem0005),inference(resolution,[status(thm)],[c592, c57])).
% 1.54/1.75  cnf(c644,plain,skolem0007!=X1172|skolem0005!=X1173|unisex(X1172,X1173),inference(resolution,[status(thm)],[c643, c8])).
% 1.54/1.75  cnf(c1304,plain,skolem0007!=X1174|unisex(X1174,skolem0005),inference(resolution,[status(thm)],[c644, reflexivity])).
% 1.54/1.75  cnf(c373,plain,relname(skolem0001,skolem0003),inference(resolution,[status(thm)],[c252, c46])).
% 1.54/1.75  cnf(c377,plain,relation(skolem0001,skolem0003),inference(resolution,[status(thm)],[c255, c373])).
% 1.54/1.75  cnf(c384,plain,abstraction(skolem0001,skolem0003),inference(resolution,[status(thm)],[c258, c377])).
% 1.54/1.75  cnf(c414,plain,unisex(skolem0001,skolem0003),inference(resolution,[status(thm)],[c270, c384])).
% 1.54/1.75  cnf(c590,plain,~accessible_world(skolem0001,X551)|unisex(X551,skolem0003),inference(resolution,[status(thm)],[c98, c414])).
% 1.54/1.75  cnf(c637,plain,unisex(skolem0007,skolem0003),inference(resolution,[status(thm)],[c590, c57])).
% 1.54/1.75  cnf(c638,plain,skolem0007!=X1168|skolem0003!=X1169|unisex(X1168,X1169),inference(resolution,[status(thm)],[c637, c8])).
% 1.54/1.75  cnf(c1302,plain,skolem0007!=X1171|unisex(X1171,skolem0003),inference(resolution,[status(thm)],[c638, reflexivity])).
% 1.54/1.75  cnf(c309,plain,human_person(skolem0001,skolem0002),inference(resolution,[status(thm)],[c219, c44])).
% 1.54/1.75  cnf(c313,plain,organism(skolem0001,skolem0002),inference(resolution,[status(thm)],[c222, c309])).
% 1.54/1.75  cnf(c319,plain,entity(skolem0001,skolem0002),inference(resolution,[status(thm)],[c225, c313])).
% 1.54/1.75  fof(ax18,axiom,(![U]:(![V]:(entity(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax18)).
% 1.54/1.75  fof(c229,plain,(![U]:(![V]:(~entity(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax18])).
% 1.54/1.75  fof(c230,plain,(![X166]:(![X167]:(~entity(X166,X167)|specific(X166,X167)))),inference(variable_rename,[status(thm)],[c229])).
% 1.54/1.75  cnf(c231,plain,~entity(X285,X286)|specific(X285,X286),inference(split_conjunct,[status(thm)],[c230])).
% 1.54/1.75  cnf(c328,plain,specific(skolem0001,skolem0002),inference(resolution,[status(thm)],[c231, c319])).
% 1.54/1.75  fof(ax63,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&specific(V,U))=>specific(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax63)).
% 1.54/1.75  fof(c90,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~specific(V,U))|specific(W,U))))),inference(fof_nnf,[status(thm)],[ax63])).
% 1.54/1.75  fof(c91,plain,(![X44]:(![X45]:(![X46]:((~accessible_world(X45,X46)|~specific(X45,X44))|specific(X46,X44))))),inference(variable_rename,[status(thm)],[c90])).
% 1.54/1.75  cnf(c92,plain,~accessible_world(X490,X491)|~specific(X490,X492)|specific(X491,X492),inference(split_conjunct,[status(thm)],[c91])).
% 1.54/1.75  cnf(c582,plain,~accessible_world(skolem0001,X538)|specific(X538,skolem0002),inference(resolution,[status(thm)],[c92, c328])).
% 1.54/1.75  cnf(c625,plain,specific(skolem0007,skolem0002),inference(resolution,[status(thm)],[c582, c57])).
% 1.54/1.75  cnf(c626,plain,skolem0007!=X1165|skolem0002!=X1166|specific(X1165,X1166),inference(resolution,[status(thm)],[c625, c23])).
% 1.54/1.75  cnf(c311,plain,human_person(skolem0001,skolem0004),inference(resolution,[status(thm)],[c219, c48])).
% 1.54/1.75  cnf(c312,plain,organism(skolem0001,skolem0004),inference(resolution,[status(thm)],[c222, c311])).
% 1.54/1.75  cnf(c317,plain,entity(skolem0001,skolem0004),inference(resolution,[status(thm)],[c225, c312])).
% 1.54/1.75  cnf(c326,plain,specific(skolem0001,skolem0004),inference(resolution,[status(thm)],[c231, c317])).
% 1.54/1.75  cnf(c581,plain,~accessible_world(skolem0001,X534)|specific(X534,skolem0004),inference(resolution,[status(thm)],[c92, c326])).
% 1.54/1.75  cnf(c619,plain,specific(skolem0007,skolem0004),inference(resolution,[status(thm)],[c581, c57])).
% 1.54/1.75  cnf(c623,plain,skolem0007!=X1162|skolem0004!=X1163|specific(X1162,X1163),inference(resolution,[status(thm)],[c619, c23])).
% 1.54/1.75  cnf(c1298,plain,skolem0007!=X1164|specific(X1164,skolem0004),inference(resolution,[status(thm)],[c623, reflexivity])).
% 1.54/1.75  cnf(c310,plain,human_person(skolem0001,skolem0008),inference(resolution,[status(thm)],[c219, c62])).
% 1.54/1.75  cnf(c314,plain,organism(skolem0001,skolem0008),inference(resolution,[status(thm)],[c222, c310])).
% 1.54/1.75  cnf(c318,plain,entity(skolem0001,skolem0008),inference(resolution,[status(thm)],[c225, c314])).
% 1.54/1.75  cnf(c327,plain,specific(skolem0001,skolem0008),inference(resolution,[status(thm)],[c231, c318])).
% 1.54/1.75  cnf(c576,plain,~accessible_world(skolem0001,X526)|specific(X526,skolem0008),inference(resolution,[status(thm)],[c92, c327])).
% 1.54/1.75  cnf(c611,plain,specific(skolem0007,skolem0008),inference(resolution,[status(thm)],[c576, c57])).
% 1.54/1.75  cnf(c612,plain,skolem0007!=X1157|skolem0008!=X1158|specific(X1157,X1158),inference(resolution,[status(thm)],[c611, c23])).
% 1.54/1.75  cnf(c1294,plain,skolem0007!=X1161|specific(X1161,skolem0008),inference(resolution,[status(thm)],[c612, reflexivity])).
% 1.54/1.75  cnf(c1293,plain,skolem0007!=X1160|specific(X1160,skolem0002),inference(resolution,[status(thm)],[c612, c449])).
% 1.54/1.75  fof(ax8,axiom,(![U]:(![V]:(abstraction(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax8)).
% 1.54/1.75  fof(c259,plain,(![U]:(![V]:(~abstraction(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax8])).
% 1.54/1.75  fof(c260,plain,(![X186]:(![X187]:(~abstraction(X186,X187)|thing(X186,X187)))),inference(variable_rename,[status(thm)],[c259])).
% 1.54/1.75  cnf(c261,plain,~abstraction(X341,X342)|thing(X341,X342),inference(split_conjunct,[status(thm)],[c260])).
% 1.54/1.75  cnf(c392,plain,thing(skolem0001,skolem0003),inference(resolution,[status(thm)],[c261, c384])).
% 1.54/1.75  fof(ax65,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&thing(V,U))=>thing(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax65)).
% 1.54/1.75  fof(c84,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~thing(V,U))|thing(W,U))))),inference(fof_nnf,[status(thm)],[ax65])).
% 1.54/1.75  fof(c85,plain,(![X38]:(![X39]:(![X40]:((~accessible_world(X39,X40)|~thing(X39,X38))|thing(X40,X38))))),inference(variable_rename,[status(thm)],[c84])).
% 1.54/1.75  cnf(c86,plain,~accessible_world(X455,X454)|~thing(X455,X456)|thing(X454,X456),inference(split_conjunct,[status(thm)],[c85])).
% 1.54/1.75  cnf(c521,plain,~accessible_world(skolem0001,X482)|thing(X482,skolem0003),inference(resolution,[status(thm)],[c86, c392])).
% 1.54/1.75  cnf(c555,plain,thing(skolem0007,skolem0003),inference(resolution,[status(thm)],[c521, c57])).
% 1.54/1.75  cnf(c557,plain,singleton(skolem0007,skolem0003),inference(resolution,[status(thm)],[c555, c201])).
% 1.54/1.75  cnf(c575,plain,skolem0007!=X1155|skolem0003!=X1156|singleton(X1155,X1156),inference(resolution,[status(thm)],[c557, c27])).
% 1.54/1.75  cnf(c1292,plain,skolem0007!=X1159|singleton(X1159,skolem0003),inference(resolution,[status(thm)],[c575, reflexivity])).
% 1.54/1.75  cnf(c556,plain,skolem0007!=X1152|skolem0003!=X1153|thing(X1152,X1153),inference(resolution,[status(thm)],[c555, c11])).
% 1.54/1.75  cnf(c1290,plain,skolem0007!=X1154|thing(X1154,skolem0003),inference(resolution,[status(thm)],[c556, reflexivity])).
% 1.54/1.75  fof(ax19,axiom,(![U]:(![V]:(entity(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax19)).
% 1.54/1.75  fof(c226,plain,(![U]:(![V]:(~entity(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax19])).
% 1.54/1.75  fof(c227,plain,(![X164]:(![X165]:(~entity(X164,X165)|thing(X164,X165)))),inference(variable_rename,[status(thm)],[c226])).
% 1.54/1.75  cnf(c228,plain,~entity(X280,X279)|thing(X280,X279),inference(split_conjunct,[status(thm)],[c227])).
% 1.54/1.75  cnf(c320,plain,thing(skolem0001,skolem0004),inference(resolution,[status(thm)],[c228, c317])).
% 1.54/1.75  cnf(c520,plain,~accessible_world(skolem0001,X481)|thing(X481,skolem0004),inference(resolution,[status(thm)],[c86, c320])).
% 1.54/1.75  cnf(c550,plain,thing(skolem0007,skolem0004),inference(resolution,[status(thm)],[c520, c57])).
% 1.54/1.75  cnf(c552,plain,singleton(skolem0007,skolem0004),inference(resolution,[status(thm)],[c550, c201])).
% 1.54/1.75  cnf(c554,plain,skolem0007!=X1146|skolem0004!=X1147|singleton(X1146,X1147),inference(resolution,[status(thm)],[c552, c27])).
% 1.54/1.75  cnf(c1286,plain,skolem0007!=X1148|singleton(X1148,skolem0004),inference(resolution,[status(thm)],[c554, reflexivity])).
% 1.54/1.75  cnf(c551,plain,skolem0007!=X1143|skolem0004!=X1144|thing(X1143,X1144),inference(resolution,[status(thm)],[c550, c11])).
% 1.54/1.75  cnf(c1284,plain,skolem0007!=X1145|thing(X1145,skolem0004),inference(resolution,[status(thm)],[c551, reflexivity])).
% 1.54/1.75  cnf(c322,plain,thing(skolem0001,skolem0002),inference(resolution,[status(thm)],[c228, c319])).
% 1.54/1.75  cnf(c516,plain,~accessible_world(skolem0001,X466)|thing(X466,skolem0002),inference(resolution,[status(thm)],[c86, c322])).
% 1.54/1.75  cnf(c540,plain,thing(skolem0007,skolem0002),inference(resolution,[status(thm)],[c516, c57])).
% 1.54/1.75  cnf(c542,plain,singleton(skolem0007,skolem0002),inference(resolution,[status(thm)],[c540, c201])).
% 1.54/1.75  cnf(c544,plain,skolem0007!=X1133|skolem0002!=X1134|singleton(X1133,X1134),inference(resolution,[status(thm)],[c542, c27])).
% 1.54/1.75  cnf(c541,plain,skolem0007!=X1129|skolem0002!=X1130|thing(X1129,X1130),inference(resolution,[status(thm)],[c540, c11])).
% 1.54/1.75  cnf(c431,plain,thing(skolem0001,skolem0007),inference(resolution,[status(thm)],[c428, c261])).
% 1.54/1.75  cnf(c515,plain,~accessible_world(skolem0001,X461)|thing(X461,skolem0007),inference(resolution,[status(thm)],[c86, c431])).
% 1.54/1.75  cnf(c532,plain,thing(skolem0007,skolem0007),inference(resolution,[status(thm)],[c515, c57])).
% 1.54/1.75  cnf(c537,plain,singleton(skolem0007,skolem0007),inference(resolution,[status(thm)],[c532, c201])).
% 1.54/1.75  cnf(c539,plain,skolem0007!=X1124|skolem0007!=X1125|singleton(X1124,X1125),inference(resolution,[status(thm)],[c537, c27])).
% 1.54/1.75  cnf(c1269,plain,skolem0007!=X1128|singleton(X1128,skolem0007),inference(resolution,[status(thm)],[c539, reflexivity])).
% 1.54/1.75  cnf(c535,plain,~entity(skolem0001,skolem0004)|~forename(skolem0001,X1127)|~of(skolem0001,X1127,skolem0004)|~forename(skolem0001,skolem0005)|skolem0005=X1127,inference(resolution,[status(thm)],[c71, c47])).
% 1.54/1.75  cnf(c1268,plain,skolem0007!=X1126|singleton(X1126,X1126),inference(factor,[status(thm)],[c539])).
% 1.54/1.75  cnf(c536,plain,skolem0007!=X1119|skolem0007!=X1120|thing(X1119,X1120),inference(resolution,[status(thm)],[c532, c11])).
% 1.54/1.75  cnf(c1264,plain,skolem0007!=X1123|thing(X1123,skolem0007),inference(resolution,[status(thm)],[c536, reflexivity])).
% 1.54/1.75  cnf(c534,plain,~entity(skolem0001,skolem0002)|~forename(skolem0001,X1122)|~of(skolem0001,X1122,skolem0002)|~forename(skolem0001,skolem0003)|skolem0003=X1122,inference(resolution,[status(thm)],[c71, c43])).
% 1.54/1.75  cnf(c1263,plain,skolem0007!=X1121|thing(X1121,X1121),inference(factor,[status(thm)],[c536])).
% 1.54/1.75  cnf(c321,plain,thing(skolem0001,skolem0008),inference(resolution,[status(thm)],[c228, c318])).
% 1.54/1.75  cnf(c514,plain,~accessible_world(skolem0001,X460)|thing(X460,skolem0008),inference(resolution,[status(thm)],[c86, c321])).
% 1.54/1.75  cnf(c527,plain,thing(skolem0007,skolem0008),inference(resolution,[status(thm)],[c514, c57])).
% 1.54/1.75  cnf(c529,plain,singleton(skolem0007,skolem0008),inference(resolution,[status(thm)],[c527, c201])).
% 1.54/1.75  cnf(c531,plain,skolem0007!=X1111|skolem0008!=X1112|singleton(X1111,X1112),inference(resolution,[status(thm)],[c529, c27])).
% 1.54/1.75  cnf(c1259,plain,skolem0007!=X1118|singleton(X1118,skolem0008),inference(resolution,[status(thm)],[c531, reflexivity])).
% 1.54/1.75  cnf(c1258,plain,skolem0007!=X1114|singleton(X1114,skolem0002),inference(resolution,[status(thm)],[c531, c449])).
% 1.54/1.75  cnf(c528,plain,skolem0007!=X1108|skolem0008!=X1109|thing(X1108,X1109),inference(resolution,[status(thm)],[c527, c11])).
% 1.54/1.75  cnf(c1256,plain,skolem0007!=X1113|thing(X1113,skolem0008),inference(resolution,[status(thm)],[c528, reflexivity])).
% 1.54/1.75  cnf(c1255,plain,skolem0007!=X1110|thing(X1110,skolem0002),inference(resolution,[status(thm)],[c528, c449])).
% 1.54/1.75  cnf(c391,plain,thing(skolem0001,skolem0005),inference(resolution,[status(thm)],[c261, c385])).
% 1.54/1.75  cnf(c512,plain,~accessible_world(skolem0001,X457)|thing(X457,skolem0005),inference(resolution,[status(thm)],[c86, c391])).
% 1.54/1.75  cnf(c522,plain,thing(skolem0007,skolem0005),inference(resolution,[status(thm)],[c512, c57])).
% 1.54/1.75  cnf(c524,plain,singleton(skolem0007,skolem0005),inference(resolution,[status(thm)],[c522, c201])).
% 1.54/1.75  cnf(c526,plain,skolem0007!=X1105|skolem0005!=X1106|singleton(X1105,X1106),inference(resolution,[status(thm)],[c524, c27])).
% 1.54/1.75  cnf(c1253,plain,skolem0007!=X1107|singleton(X1107,skolem0005),inference(resolution,[status(thm)],[c526, reflexivity])).
% 1.54/1.75  cnf(c523,plain,skolem0007!=X1098|skolem0005!=X1099|thing(X1098,X1099),inference(resolution,[status(thm)],[c522, c11])).
% 1.54/1.75  cnf(c1249,plain,skolem0007!=X1100|thing(X1100,skolem0005),inference(resolution,[status(thm)],[c523, reflexivity])).
% 1.54/1.75  cnf(c298,plain,eventuality(skolem0001,skolem0006),inference(resolution,[status(thm)],[c216, c54])).
% 1.54/1.75  fof(ax66,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&eventuality(V,U))=>eventuality(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax66)).
% 1.54/1.75  fof(c81,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~eventuality(V,U))|eventuality(W,U))))),inference(fof_nnf,[status(thm)],[ax66])).
% 1.54/1.75  fof(c82,plain,(![X35]:(![X36]:(![X37]:((~accessible_world(X36,X37)|~eventuality(X36,X35))|eventuality(X37,X35))))),inference(variable_rename,[status(thm)],[c81])).
% 1.54/1.75  cnf(c83,plain,~accessible_world(X431,X430)|~eventuality(X431,X429)|eventuality(X430,X429),inference(split_conjunct,[status(thm)],[c82])).
% 1.54/1.75  cnf(c492,plain,~accessible_world(skolem0001,X438)|eventuality(X438,skolem0006),inference(resolution,[status(thm)],[c83, c298])).
% 1.54/1.75  cnf(c495,plain,eventuality(skolem0007,skolem0006),inference(resolution,[status(thm)],[c492, c57])).
% 1.54/1.75  cnf(c500,plain,thing(skolem0007,skolem0006),inference(resolution,[status(thm)],[c495, c198])).
% 1.54/1.75  cnf(c508,plain,singleton(skolem0007,skolem0006),inference(resolution,[status(thm)],[c500, c201])).
% 1.54/1.75  cnf(c510,plain,skolem0007!=X1095|skolem0006!=X1096|singleton(X1095,X1096),inference(resolution,[status(thm)],[c508, c27])).
% 1.54/1.75  cnf(c1247,plain,skolem0007!=X1097|singleton(X1097,skolem0006),inference(resolution,[status(thm)],[c510, reflexivity])).
% 1.54/1.75  cnf(c501,plain,specific(skolem0007,skolem0006),inference(resolution,[status(thm)],[c495, c204])).
% 1.54/1.75  cnf(c509,plain,skolem0007!=X1092|skolem0006!=X1093|specific(X1092,X1093),inference(resolution,[status(thm)],[c501, c23])).
% 1.54/1.75  cnf(c1245,plain,skolem0007!=X1094|specific(X1094,skolem0006),inference(resolution,[status(thm)],[c509, reflexivity])).
% 1.54/1.75  cnf(c507,plain,skolem0007!=X1086|skolem0006!=X1087|thing(X1086,X1087),inference(resolution,[status(thm)],[c500, c11])).
% 1.54/1.75  cnf(c1242,plain,skolem0007!=X1091|thing(X1091,skolem0006),inference(resolution,[status(thm)],[c507, reflexivity])).
% 1.54/1.75  cnf(c499,plain,nonexistent(skolem0007,skolem0006),inference(resolution,[status(thm)],[c495, c207])).
% 1.54/1.75  cnf(c506,plain,skolem0007!=X1083|skolem0006!=X1084|nonexistent(X1083,X1084),inference(resolution,[status(thm)],[c499, c26])).
% 1.54/1.75  cnf(c1240,plain,skolem0007!=X1085|nonexistent(X1085,skolem0006),inference(resolution,[status(thm)],[c506, reflexivity])).
% 1.54/1.75  cnf(c498,plain,unisex(skolem0007,skolem0006),inference(resolution,[status(thm)],[c495, c210])).
% 1.54/1.75  cnf(c502,plain,skolem0007!=X1077|skolem0006!=X1078|unisex(X1077,X1078),inference(resolution,[status(thm)],[c498, c8])).
% 1.54/1.75  cnf(c1236,plain,skolem0007!=X1079|unisex(X1079,skolem0006),inference(resolution,[status(thm)],[c502, reflexivity])).
% 1.54/1.75  cnf(c497,plain,skolem0007!=X1075|skolem0006!=X1074|eventuality(X1075,X1074),inference(resolution,[status(thm)],[c495, c24])).
% 1.54/1.75  cnf(c1234,plain,skolem0007!=X1076|eventuality(X1076,skolem0006),inference(resolution,[status(thm)],[c497, reflexivity])).
% 1.54/1.75  cnf(c493,plain,skolem0001!=X1071|skolem0006!=X1072|present(X1071,X1072),inference(resolution,[status(thm)],[c32, c55])).
% 1.54/1.75  cnf(c1232,plain,skolem0001!=X1073|present(X1073,skolem0006),inference(resolution,[status(thm)],[c493, reflexivity])).
% 1.54/1.75  fof(ax30,axiom,(![U]:(![V]:(state(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax30)).
% 1.54/1.75  fof(c193,plain,(![U]:(![V]:(~state(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax30])).
% 1.54/1.75  fof(c194,plain,(![X142]:(![X143]:(~state(X142,X143)|eventuality(X142,X143)))),inference(variable_rename,[status(thm)],[c193])).
% 1.54/1.75  cnf(c195,plain,~state(X226,X225)|eventuality(X226,X225),inference(split_conjunct,[status(thm)],[c194])).
% 1.54/1.75  cnf(c63,negated_conjecture,state(skolem0001,skolem0009),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.75  fof(ax67,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&state(V,U))=>state(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax67)).
% 1.54/1.75  fof(c78,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~state(V,U))|state(W,U))))),inference(fof_nnf,[status(thm)],[ax67])).
% 1.54/1.75  fof(c79,plain,(![X32]:(![X33]:(![X34]:((~accessible_world(X33,X34)|~state(X33,X32))|state(X34,X32))))),inference(variable_rename,[status(thm)],[c78])).
% 1.54/1.75  cnf(c80,plain,~accessible_world(X414,X416)|~state(X414,X415)|state(X416,X415),inference(split_conjunct,[status(thm)],[c79])).
% 1.54/1.75  cnf(c468,plain,~accessible_world(skolem0001,X417)|state(X417,skolem0009),inference(resolution,[status(thm)],[c80, c63])).
% 1.54/1.75  cnf(c469,plain,state(skolem0007,skolem0009),inference(resolution,[status(thm)],[c468, c57])).
% 1.54/1.75  cnf(c472,plain,eventuality(skolem0007,skolem0009),inference(resolution,[status(thm)],[c469, c195])).
% 1.54/1.75  cnf(c479,plain,thing(skolem0007,skolem0009),inference(resolution,[status(thm)],[c472, c198])).
% 1.54/1.75  cnf(c486,plain,singleton(skolem0007,skolem0009),inference(resolution,[status(thm)],[c479, c201])).
% 1.54/1.75  cnf(c489,plain,skolem0007!=X1068|skolem0009!=X1069|singleton(X1068,X1069),inference(resolution,[status(thm)],[c486, c27])).
% 1.54/1.75  cnf(c1230,plain,skolem0007!=X1070|singleton(X1070,skolem0009),inference(resolution,[status(thm)],[c489, reflexivity])).
% 1.54/1.75  cnf(c480,plain,specific(skolem0007,skolem0009),inference(resolution,[status(thm)],[c472, c204])).
% 1.54/1.75  cnf(c487,plain,skolem0007!=X1062|skolem0009!=X1063|specific(X1062,X1063),inference(resolution,[status(thm)],[c480, c23])).
% 1.54/1.75  cnf(c1227,plain,skolem0007!=X1064|specific(X1064,skolem0009),inference(resolution,[status(thm)],[c487, reflexivity])).
% 1.54/1.75  cnf(c485,plain,skolem0007!=X1059|skolem0009!=X1060|thing(X1059,X1060),inference(resolution,[status(thm)],[c479, c11])).
% 1.54/1.75  cnf(c1225,plain,skolem0007!=X1061|thing(X1061,skolem0009),inference(resolution,[status(thm)],[c485, reflexivity])).
% 1.54/1.75  cnf(c478,plain,nonexistent(skolem0007,skolem0009),inference(resolution,[status(thm)],[c472, c207])).
% 1.54/1.75  cnf(c484,plain,skolem0007!=X1056|skolem0009!=X1057|nonexistent(X1056,X1057),inference(resolution,[status(thm)],[c478, c26])).
% 1.54/1.75  cnf(c1223,plain,skolem0007!=X1058|nonexistent(X1058,skolem0009),inference(resolution,[status(thm)],[c484, reflexivity])).
% 1.54/1.75  cnf(c477,plain,unisex(skolem0007,skolem0009),inference(resolution,[status(thm)],[c472, c210])).
% 1.54/1.75  cnf(c482,plain,skolem0007!=X1053|skolem0009!=X1054|unisex(X1053,X1054),inference(resolution,[status(thm)],[c477, c8])).
% 1.54/1.75  cnf(c1221,plain,skolem0007!=X1055|unisex(X1055,skolem0009),inference(resolution,[status(thm)],[c482, reflexivity])).
% 1.54/1.75  cnf(c481,plain,skolem0001!=X1050|skolem0006!=X1051|think_believe_consider(X1050,X1051),inference(resolution,[status(thm)],[c30, c56])).
% 1.54/1.75  cnf(c1219,plain,skolem0001!=X1052|think_believe_consider(X1052,skolem0006),inference(resolution,[status(thm)],[c481, reflexivity])).
% 1.54/1.75  cnf(c476,plain,skolem0007!=X1048|skolem0009!=X1047|eventuality(X1048,X1047),inference(resolution,[status(thm)],[c472, c24])).
% 1.54/1.75  cnf(c1217,plain,skolem0007!=X1049|eventuality(X1049,skolem0009),inference(resolution,[status(thm)],[c476, reflexivity])).
% 1.54/1.75  fof(ax24,axiom,(![U]:(![V]:(state(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax24)).
% 1.54/1.75  fof(c211,plain,(![U]:(![V]:(~state(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax24])).
% 1.54/1.75  fof(c212,plain,(![X154]:(![X155]:(~state(X154,X155)|event(X154,X155)))),inference(variable_rename,[status(thm)],[c211])).
% 1.54/1.75  cnf(c213,plain,~state(X249,X250)|event(X249,X250),inference(split_conjunct,[status(thm)],[c212])).
% 1.54/1.75  cnf(c470,plain,event(skolem0007,skolem0009),inference(resolution,[status(thm)],[c469, c213])).
% 1.54/1.75  cnf(c474,plain,skolem0007!=X1045|skolem0009!=X1044|event(X1045,X1044),inference(resolution,[status(thm)],[c470, c5])).
% 1.54/1.75  cnf(c1215,plain,skolem0007!=X1046|event(X1046,skolem0009),inference(resolution,[status(thm)],[c474, reflexivity])).
% 1.54/1.75  cnf(c25,axiom,X377!=X380|X379!=X378|~state(X377,X379)|state(X380,X378),theory(equality)).
% 1.54/1.75  cnf(c471,plain,skolem0007!=X1039|skolem0009!=X1038|state(X1039,X1038),inference(resolution,[status(thm)],[c469, c25])).
% 1.54/1.75  cnf(c1212,plain,skolem0007!=X1043|state(X1043,skolem0009),inference(resolution,[status(thm)],[c471, reflexivity])).
% 1.54/1.75  cnf(c28,axiom,X401!=X404|X403!=X402|~accessible_world(X401,X403)|accessible_world(X404,X402),theory(equality)).
% 1.54/1.75  cnf(c466,plain,skolem0001!=X1034|skolem0007!=X1033|accessible_world(X1034,X1033),inference(resolution,[status(thm)],[c28, c57])).
% 1.54/1.75  cnf(c1210,plain,skolem0001!=X1037|accessible_world(X1037,skolem0007),inference(resolution,[status(thm)],[c466, reflexivity])).
% 1.54/1.75  cnf(c325,plain,singleton(skolem0001,skolem0002),inference(resolution,[status(thm)],[c322, c201])).
% 1.54/1.75  cnf(c461,plain,skolem0001!=X1031|skolem0002!=X1032|singleton(X1031,X1032),inference(resolution,[status(thm)],[c27, c325])).
% 1.54/1.75  cnf(c1194,plain,~accessible_world(skolem0007,X1030)|theme(X1030,skolem0006,skolem0007),inference(resolution,[status(thm)],[c1193, c170])).
% 1.54/1.75  cnf(c1189,plain,~accessible_world(skolem0007,X1029)|agent(X1029,skolem0006,skolem0004),inference(resolution,[status(thm)],[c1187, c164])).
% 1.54/1.75  cnf(c394,plain,singleton(skolem0001,skolem0005),inference(resolution,[status(thm)],[c391, c201])).
% 1.54/1.75  cnf(c460,plain,skolem0001!=X1026|skolem0005!=X1027|singleton(X1026,X1027),inference(resolution,[status(thm)],[c27, c394])).
% 1.54/1.75  cnf(c1206,plain,skolem0001!=X1028|singleton(X1028,skolem0005),inference(resolution,[status(thm)],[c460, reflexivity])).
% 1.54/1.75  cnf(c1177,plain,~accessible_world(skolem0007,X1025)|of(X1025,skolem0005,skolem0004),inference(resolution,[status(thm)],[c1175, c155])).
% 1.54/1.75  cnf(c1172,plain,~accessible_world(skolem0007,X1024)|of(X1024,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1169, c155])).
% 1.54/1.75  fof(ax64,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&singleton(V,U))=>singleton(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax64)).
% 1.54/1.75  fof(c87,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~singleton(V,U))|singleton(W,U))))),inference(fof_nnf,[status(thm)],[ax64])).
% 1.54/1.75  fof(c88,plain,(![X41]:(![X42]:(![X43]:((~accessible_world(X42,X43)|~singleton(X42,X41))|singleton(X43,X41))))),inference(variable_rename,[status(thm)],[c87])).
% 1.54/1.75  cnf(c89,plain,~accessible_world(X485,X483)|~singleton(X485,X484)|singleton(X483,X484),inference(split_conjunct,[status(thm)],[c88])).
% 1.54/1.75  cnf(c878,plain,~accessible_world(skolem0007,X1023)|singleton(X1023,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c874, c89])).
% 1.54/1.75  cnf(c289,plain,eventuality(skolem0001,skolem0009),inference(resolution,[status(thm)],[c195, c63])).
% 1.54/1.75  cnf(c291,plain,thing(skolem0001,skolem0009),inference(resolution,[status(thm)],[c198, c289])).
% 1.54/1.75  cnf(c292,plain,singleton(skolem0001,skolem0009),inference(resolution,[status(thm)],[c201, c291])).
% 1.54/1.75  cnf(c459,plain,skolem0001!=X1020|skolem0009!=X1021|singleton(X1020,X1021),inference(resolution,[status(thm)],[c27, c292])).
% 1.54/1.75  cnf(c1204,plain,skolem0001!=X1022|singleton(X1022,skolem0009),inference(resolution,[status(thm)],[c459, reflexivity])).
% 1.54/1.75  cnf(c877,plain,~accessible_world(skolem0007,X1019)|specific(X1019,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c866, c92])).
% 1.54/1.75  cnf(c875,plain,~accessible_world(skolem0007,X1018)|thing(X1018,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c865, c86])).
% 1.54/1.75  fof(ax62,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&nonexistent(V,U))=>nonexistent(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax62)).
% 1.54/1.75  fof(c93,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~nonexistent(V,U))|nonexistent(W,U))))),inference(fof_nnf,[status(thm)],[ax62])).
% 1.54/1.75  fof(c94,plain,(![X47]:(![X48]:(![X49]:((~accessible_world(X48,X49)|~nonexistent(X48,X47))|nonexistent(X49,X47))))),inference(variable_rename,[status(thm)],[c93])).
% 1.54/1.75  cnf(c95,plain,~accessible_world(X499,X498)|~nonexistent(X499,X497)|nonexistent(X498,X497),inference(split_conjunct,[status(thm)],[c94])).
% 1.54/1.75  cnf(c870,plain,~accessible_world(skolem0007,X1017)|nonexistent(X1017,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c864, c95])).
% 1.54/1.75  cnf(c304,plain,thing(skolem0001,skolem0006),inference(resolution,[status(thm)],[c298, c198])).
% 1.54/1.75  cnf(c307,plain,singleton(skolem0001,skolem0006),inference(resolution,[status(thm)],[c304, c201])).
% 1.54/1.75  cnf(c458,plain,skolem0001!=X1014|skolem0006!=X1015|singleton(X1014,X1015),inference(resolution,[status(thm)],[c27, c307])).
% 1.54/1.75  cnf(c1202,plain,skolem0001!=X1016|singleton(X1016,skolem0006),inference(resolution,[status(thm)],[c458, reflexivity])).
% 1.54/1.75  cnf(c868,plain,~accessible_world(skolem0007,X1013)|unisex(X1013,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c863, c98])).
% 1.54/1.75  cnf(c861,plain,~accessible_world(skolem0007,X1012)|eventuality(X1012,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c854, c83])).
% 1.54/1.75  cnf(c860,plain,~accessible_world(skolem0007,X1011)|present(X1011,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c819, c161])).
% 1.54/1.75  cnf(c438,plain,singleton(skolem0001,skolem0007),inference(resolution,[status(thm)],[c431, c201])).
% 1.54/1.75  cnf(c457,plain,skolem0001!=X1008|skolem0007!=X1009|singleton(X1008,X1009),inference(resolution,[status(thm)],[c27, c438])).
% 1.54/1.75  cnf(c1200,plain,skolem0001!=X1010|singleton(X1010,skolem0007),inference(resolution,[status(thm)],[c457, reflexivity])).
% 1.54/1.75  fof(ax41,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&smoke(V,U))=>smoke(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax41)).
% 1.54/1.75  fof(c156,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~smoke(V,U))|smoke(W,U))))),inference(fof_nnf,[status(thm)],[ax41])).
% 1.54/1.75  fof(c157,plain,(![X111]:(![X112]:(![X113]:((~accessible_world(X112,X113)|~smoke(X112,X111))|smoke(X113,X111))))),inference(variable_rename,[status(thm)],[c156])).
% 1.54/1.75  cnf(c158,plain,~accessible_world(X600,X599)|~smoke(X600,X598)|smoke(X599,X598),inference(split_conjunct,[status(thm)],[c157])).
% 1.54/1.75  cnf(c856,plain,~accessible_world(skolem0007,X1007)|smoke(X1007,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c818, c158])).
% 1.54/1.75  cnf(c324,plain,singleton(skolem0001,skolem0008),inference(resolution,[status(thm)],[c321, c201])).
% 1.54/1.75  cnf(c456,plain,skolem0001!=X1003|skolem0008!=X1004|singleton(X1003,X1004),inference(resolution,[status(thm)],[c27, c324])).
% 1.54/1.75  cnf(c1197,plain,skolem0001!=X1006|singleton(X1006,skolem0008),inference(resolution,[status(thm)],[c456, reflexivity])).
% 1.54/1.75  cnf(c1196,plain,skolem0001!=X1005|singleton(X1005,skolem0002),inference(resolution,[status(thm)],[c456, c449])).
% 1.54/1.75  cnf(c852,plain,~accessible_world(skolem0007,X1001)|event(X1001,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c813, c101])).
% 1.54/1.75  cnf(c396,plain,singleton(skolem0001,skolem0003),inference(resolution,[status(thm)],[c392, c201])).
% 1.54/1.75  cnf(c455,plain,skolem0001!=X998|skolem0003!=X999|singleton(X998,X999),inference(resolution,[status(thm)],[c27, c396])).
% 1.54/1.75  cnf(c1191,plain,skolem0001!=X1000|singleton(X1000,skolem0003),inference(resolution,[status(thm)],[c455, reflexivity])).
% 1.54/1.75  cnf(c812,plain,~accessible_world(skolem0007,X996)|present(X996,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c161, c668])).
% 1.54/1.75  cnf(c323,plain,singleton(skolem0001,skolem0004),inference(resolution,[status(thm)],[c320, c201])).
% 1.54/1.75  cnf(c454,plain,skolem0001!=X993|skolem0004!=X994|singleton(X993,X994),inference(resolution,[status(thm)],[c27, c323])).
% 1.54/1.75  cnf(c1185,plain,skolem0001!=X995|singleton(X995,skolem0004),inference(resolution,[status(thm)],[c454, reflexivity])).
% 1.54/1.75  cnf(c810,plain,~accessible_world(skolem0007,X992)|present(X992,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c161, c743])).
% 1.54/1.75  cnf(c807,plain,~accessible_world(skolem0007,X991)|singleton(X991,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c803, c89])).
% 1.54/1.75  cnf(c806,plain,~accessible_world(skolem0007,X990)|specific(X990,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c794, c92])).
% 1.54/1.75  cnf(c303,plain,nonexistent(skolem0001,skolem0006),inference(resolution,[status(thm)],[c298, c207])).
% 1.54/1.75  cnf(c446,plain,skolem0001!=X987|skolem0006!=X988|nonexistent(X987,X988),inference(resolution,[status(thm)],[c26, c303])).
% 1.54/1.75  cnf(c1183,plain,skolem0001!=X989|nonexistent(X989,skolem0006),inference(resolution,[status(thm)],[c446, reflexivity])).
% 1.54/1.75  cnf(c804,plain,~accessible_world(skolem0007,X986)|thing(X986,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c793, c86])).
% 1.54/1.75  cnf(c801,plain,~accessible_world(skolem0007,X985)|smoke(X985,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c158, c742])).
% 1.54/1.75  cnf(c800,plain,~accessible_world(skolem0007,X984)|smoke(X984,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c158, c667])).
% 1.54/1.75  cnf(c294,plain,nonexistent(skolem0001,skolem0009),inference(resolution,[status(thm)],[c207, c289])).
% 1.54/1.75  cnf(c445,plain,skolem0001!=X981|skolem0009!=X982|nonexistent(X981,X982),inference(resolution,[status(thm)],[c26, c294])).
% 1.54/1.75  cnf(c1181,plain,skolem0001!=X983|nonexistent(X983,skolem0009),inference(resolution,[status(thm)],[c445, reflexivity])).
% 1.54/1.75  cnf(c797,plain,~accessible_world(skolem0007,X980)|nonexistent(X980,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c792, c95])).
% 1.54/1.75  cnf(c796,plain,~accessible_world(skolem0007,X979)|unisex(X979,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c791, c98])).
% 1.54/1.75  cnf(c789,plain,~accessible_world(skolem0007,X978)|eventuality(X978,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c783, c83])).
% 1.54/1.75  cnf(c443,plain,skolem0001!=X976|skolem0009!=X975|state(X976,X975),inference(resolution,[status(thm)],[c25, c63])).
% 1.54/1.75  cnf(c1179,plain,skolem0001!=X977|state(X977,skolem0009),inference(resolution,[status(thm)],[c443, reflexivity])).
% 1.54/1.75  cnf(c441,plain,skolem0001!=X971|skolem0007!=X972|unisex(X971,X972),inference(resolution,[status(thm)],[c433, c8])).
% 1.54/1.75  cnf(c1170,plain,skolem0001!=X973|unisex(X973,skolem0007),inference(resolution,[status(thm)],[c441, reflexivity])).
% 1.54/1.75  cnf(c781,plain,~accessible_world(skolem0007,X969)|event(X969,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c737, c101])).
% 1.54/1.75  cnf(c734,plain,~accessible_world(skolem0007,X968)|singleton(X968,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c727, c89])).
% 1.54/1.75  cnf(c440,plain,skolem0001!=X966|skolem0006!=X965|eventuality(X966,X965),inference(resolution,[status(thm)],[c24, c298])).
% 1.54/1.75  cnf(c1167,plain,skolem0001!=X967|eventuality(X967,skolem0006),inference(resolution,[status(thm)],[c440, reflexivity])).
% 1.54/1.75  cnf(c733,plain,~accessible_world(skolem0007,X964)|specific(X964,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c720, c92])).
% 1.54/1.75  cnf(c728,plain,~accessible_world(skolem0007,X963)|thing(X963,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c719, c86])).
% 1.54/1.75  cnf(c723,plain,~accessible_world(skolem0007,X962)|nonexistent(X962,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c718, c95])).
% 1.54/1.75  cnf(c439,plain,skolem0001!=X960|skolem0009!=X959|eventuality(X960,X959),inference(resolution,[status(thm)],[c24, c289])).
% 1.54/1.75  cnf(c1165,plain,skolem0001!=X961|eventuality(X961,skolem0009),inference(resolution,[status(thm)],[c439, reflexivity])).
% 1.54/1.75  cnf(c722,plain,~accessible_world(skolem0007,X958)|unisex(X958,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c717, c98])).
% 1.54/1.75  cnf(c715,plain,~accessible_world(skolem0007,X957)|eventuality(X957,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c708, c83])).
% 1.54/1.75  cnf(c706,plain,~accessible_world(skolem0007,X956)|event(X956,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c662, c101])).
% 1.54/1.75  cnf(c437,plain,skolem0001!=X953|skolem0007!=X954|thing(X953,X954),inference(resolution,[status(thm)],[c431, c11])).
% 1.54/1.75  cnf(c1163,plain,skolem0001!=X955|thing(X955,skolem0007),inference(resolution,[status(thm)],[c437, reflexivity])).
% 1.54/1.75  cnf(c430,plain,nonhuman(skolem0001,skolem0007),inference(resolution,[status(thm)],[c428, c264])).
% 1.54/1.75  cnf(c436,plain,skolem0001!=X950|skolem0007!=X949|nonhuman(X950,X949),inference(resolution,[status(thm)],[c430, c10])).
% 1.54/1.75  cnf(c1160,plain,skolem0001!=X952|nonhuman(X952,skolem0007),inference(resolution,[status(thm)],[c436, reflexivity])).
% 1.54/1.75  cnf(c429,plain,general(skolem0001,skolem0007),inference(resolution,[status(thm)],[c428, c267])).
% 1.54/1.75  cnf(c434,plain,skolem0001!=X943|skolem0007!=X944|general(X943,X944),inference(resolution,[status(thm)],[c429, c9])).
% 1.54/1.75  cnf(c1157,plain,skolem0001!=X951|general(X951,skolem0007),inference(resolution,[status(thm)],[c434, reflexivity])).
% 1.54/1.75  cnf(c432,plain,skolem0001!=X940|skolem0007!=X939|abstraction(X940,X939),inference(resolution,[status(thm)],[c428, c7])).
% 1.54/1.75  cnf(c1154,plain,skolem0001!=X948|abstraction(X948,skolem0007),inference(resolution,[status(thm)],[c432, reflexivity])).
% 1.54/1.75  cnf(c427,plain,skolem0001!=X935|skolem0007!=X934|relation(X935,X934),inference(resolution,[status(thm)],[c421, c3])).
% 1.54/1.75  cnf(c1150,plain,skolem0001!=X947|relation(X947,skolem0007),inference(resolution,[status(thm)],[c427, reflexivity])).
% 1.54/1.75  cnf(c425,plain,skolem0001!=X924|skolem0004!=X925|specific(X924,X925),inference(resolution,[status(thm)],[c23, c326])).
% 1.54/1.75  cnf(c1143,plain,skolem0001!=X942|specific(X942,skolem0004),inference(resolution,[status(thm)],[c425, reflexivity])).
% 1.54/1.75  cnf(c305,plain,specific(skolem0001,skolem0006),inference(resolution,[status(thm)],[c298, c204])).
% 1.54/1.75  cnf(c424,plain,skolem0001!=X919|skolem0006!=X920|specific(X919,X920),inference(resolution,[status(thm)],[c23, c305])).
% 1.54/1.75  cnf(c1140,plain,skolem0001!=X941|specific(X941,skolem0006),inference(resolution,[status(thm)],[c424, reflexivity])).
% 1.54/1.75  cnf(c293,plain,specific(skolem0001,skolem0009),inference(resolution,[status(thm)],[c204, c289])).
% 1.54/1.75  cnf(c423,plain,skolem0001!=X914|skolem0009!=X915|specific(X914,X915),inference(resolution,[status(thm)],[c23, c293])).
% 1.54/1.75  cnf(c1137,plain,skolem0001!=X938|specific(X938,skolem0009),inference(resolution,[status(thm)],[c423, reflexivity])).
% 1.54/1.75  cnf(c422,plain,skolem0001!=X910|skolem0008!=X911|specific(X910,X911),inference(resolution,[status(thm)],[c23, c327])).
% 1.54/1.75  cnf(c1134,plain,skolem0001!=X937|specific(X937,skolem0008),inference(resolution,[status(thm)],[c422, reflexivity])).
% 1.54/1.75  cnf(c1133,plain,skolem0001!=X936|specific(X936,skolem0002),inference(resolution,[status(thm)],[c422, c449])).
% 1.54/1.75  cnf(c419,plain,skolem0001!=X904|skolem0003!=X905|unisex(X904,X905),inference(resolution,[status(thm)],[c414, c8])).
% 1.54/1.75  cnf(c1130,plain,skolem0001!=X933|unisex(X933,skolem0003),inference(resolution,[status(thm)],[c419, reflexivity])).
% 1.54/1.75  cnf(c426,plain,skolem0001!=X929|skolem0002!=X930|specific(X929,X930),inference(resolution,[status(thm)],[c23, c328])).
% 1.54/1.75  cnf(c335,plain,existent(skolem0001,skolem0008),inference(resolution,[status(thm)],[c234, c318])).
% 1.54/1.75  cnf(c417,plain,skolem0001!=X896|skolem0008!=X895|existent(X896,X895),inference(resolution,[status(thm)],[c22, c335])).
% 1.54/1.75  cnf(c1122,plain,skolem0001!=X928|existent(X928,skolem0008),inference(resolution,[status(thm)],[c417, reflexivity])).
% 1.54/1.75  cnf(c1121,plain,skolem0001!=X927|existent(X927,skolem0002),inference(resolution,[status(thm)],[c417, c449])).
% 1.54/1.75  cnf(c334,plain,existent(skolem0001,skolem0004),inference(resolution,[status(thm)],[c234, c317])).
% 1.54/1.75  cnf(c416,plain,skolem0001!=X891|skolem0004!=X890|existent(X891,X890),inference(resolution,[status(thm)],[c22, c334])).
% 1.54/1.75  cnf(c1119,plain,skolem0001!=X926|existent(X926,skolem0004),inference(resolution,[status(thm)],[c416, reflexivity])).
% 1.54/1.75  cnf(c415,plain,skolem0001!=X885|skolem0005!=X886|unisex(X885,X886),inference(resolution,[status(thm)],[c413, c8])).
% 1.54/1.75  cnf(c1115,plain,skolem0001!=X923|unisex(X923,skolem0005),inference(resolution,[status(thm)],[c415, reflexivity])).
% 1.54/1.75  cnf(c405,plain,general(skolem0001,skolem0003),inference(resolution,[status(thm)],[c267, c384])).
% 1.54/1.75  cnf(c411,plain,skolem0001!=X881|skolem0003!=X882|general(X881,X882),inference(resolution,[status(thm)],[c405, c9])).
% 1.54/1.75  cnf(c1112,plain,skolem0001!=X922|general(X922,skolem0003),inference(resolution,[status(thm)],[c411, reflexivity])).
% 1.54/1.75  cnf(c409,plain,skolem0001!=X871|skolem0008!=X870|entity(X871,X870),inference(resolution,[status(thm)],[c21, c318])).
% 1.54/1.75  cnf(c1105,plain,skolem0001!=X917|entity(X917,skolem0008),inference(resolution,[status(thm)],[c409, reflexivity])).
% 1.54/1.75  cnf(c1104,plain,skolem0001!=X916|entity(X916,skolem0002),inference(resolution,[status(thm)],[c409, c449])).
% 1.54/1.75  cnf(c408,plain,skolem0001!=X866|skolem0004!=X865|entity(X866,X865),inference(resolution,[status(thm)],[c21, c317])).
% 1.54/1.75  cnf(c1102,plain,skolem0001!=X913|entity(X913,skolem0004),inference(resolution,[status(thm)],[c408, reflexivity])).
% 1.54/1.75  cnf(c404,plain,general(skolem0001,skolem0005),inference(resolution,[status(thm)],[c267, c385])).
% 1.54/1.75  cnf(c406,plain,skolem0001!=X859|skolem0005!=X860|general(X859,X860),inference(resolution,[status(thm)],[c404, c9])).
% 1.54/1.75  cnf(c1100,plain,skolem0001!=X912|general(X912,skolem0005),inference(resolution,[status(thm)],[c406, reflexivity])).
% 1.54/1.75  cnf(c401,plain,nonhuman(skolem0001,skolem0003),inference(resolution,[status(thm)],[c264, c384])).
% 1.54/1.75  cnf(c403,plain,skolem0001!=X855|skolem0003!=X854|nonhuman(X855,X854),inference(resolution,[status(thm)],[c401, c10])).
% 1.54/1.75  cnf(c1097,plain,skolem0001!=X909|nonhuman(X909,skolem0003),inference(resolution,[status(thm)],[c403, reflexivity])).
% 1.54/1.75  cnf(c400,plain,nonhuman(skolem0001,skolem0005),inference(resolution,[status(thm)],[c264, c385])).
% 1.54/1.75  cnf(c402,plain,skolem0001!=X849|skolem0005!=X848|nonhuman(X849,X848),inference(resolution,[status(thm)],[c400, c10])).
% 1.54/1.75  cnf(c1094,plain,skolem0001!=X908|nonhuman(X908,skolem0005),inference(resolution,[status(thm)],[c402, reflexivity])).
% 1.54/1.75  cnf(c339,plain,impartial(skolem0001,skolem0002),inference(resolution,[status(thm)],[c237, c313])).
% 1.54/1.75  cnf(c398,plain,skolem0001!=X838|skolem0002!=X839|impartial(X838,X839),inference(resolution,[status(thm)],[c20, c339])).
% 1.54/1.75  cnf(c1087,plain,skolem0001!=X903|impartial(X903,skolem0002),inference(resolution,[status(thm)],[c398, reflexivity])).
% 1.54/1.75  cnf(c1086,plain,skolem0001!=X902|impartial(X902,skolem0008),inference(resolution,[status(thm)],[c398, c447])).
% 1.54/1.75  cnf(c336,plain,existent(skolem0001,skolem0002),inference(resolution,[status(thm)],[c234, c319])).
% 1.54/1.75  cnf(c418,plain,skolem0001!=X901|skolem0002!=X900|existent(X901,X900),inference(resolution,[status(thm)],[c22, c336])).
% 1.54/1.75  cnf(c337,plain,impartial(skolem0001,skolem0004),inference(resolution,[status(thm)],[c237, c312])).
% 1.54/1.75  cnf(c397,plain,skolem0001!=X832|skolem0004!=X833|impartial(X832,X833),inference(resolution,[status(thm)],[c20, c337])).
% 1.54/1.75  cnf(c1084,plain,skolem0001!=X899|impartial(X899,skolem0004),inference(resolution,[status(thm)],[c397, reflexivity])).
% 1.54/1.75  cnf(c395,plain,skolem0001!=X826|skolem0003!=X827|thing(X826,X827),inference(resolution,[status(thm)],[c392, c11])).
% 1.54/1.75  cnf(c1082,plain,skolem0001!=X898|thing(X898,skolem0003),inference(resolution,[status(thm)],[c395, reflexivity])).
% 1.54/1.75  cnf(c393,plain,skolem0001!=X822|skolem0005!=X823|thing(X822,X823),inference(resolution,[status(thm)],[c391, c11])).
% 1.54/1.75  cnf(c1079,plain,skolem0001!=X897|thing(X897,skolem0005),inference(resolution,[status(thm)],[c393, reflexivity])).
% 1.54/1.75  cnf(c341,plain,living(skolem0001,skolem0008),inference(resolution,[status(thm)],[c240, c314])).
% 1.54/1.75  cnf(c389,plain,skolem0001!=X809|skolem0008!=X810|living(X809,X810),inference(resolution,[status(thm)],[c19, c341])).
% 1.54/1.75  cnf(c1075,plain,skolem0001!=X892|living(X892,skolem0008),inference(resolution,[status(thm)],[c389, reflexivity])).
% 1.54/1.75  cnf(c1074,plain,skolem0001!=X889|living(X889,skolem0002),inference(resolution,[status(thm)],[c389, c449])).
% 1.54/1.75  cnf(c340,plain,living(skolem0001,skolem0004),inference(resolution,[status(thm)],[c240, c312])).
% 1.54/1.75  cnf(c388,plain,skolem0001!=X803|skolem0004!=X804|living(X803,X804),inference(resolution,[status(thm)],[c19, c340])).
% 1.54/1.75  cnf(c1071,plain,skolem0001!=X888|living(X888,skolem0004),inference(resolution,[status(thm)],[c388, reflexivity])).
% 1.54/1.75  cnf(c387,plain,skolem0001!=X798|skolem0005!=X797|abstraction(X798,X797),inference(resolution,[status(thm)],[c385, c7])).
% 1.54/1.75  cnf(c1069,plain,skolem0001!=X887|abstraction(X887,skolem0005),inference(resolution,[status(thm)],[c387, reflexivity])).
% 1.54/1.75  cnf(c386,plain,skolem0001!=X793|skolem0003!=X792|abstraction(X793,X792),inference(resolution,[status(thm)],[c384, c7])).
% 1.54/1.75  cnf(c1066,plain,skolem0001!=X884|abstraction(X884,skolem0003),inference(resolution,[status(thm)],[c386, reflexivity])).
% 1.54/1.75  cnf(c383,plain,skolem0001!=X788|skolem0005!=X787|relation(X788,X787),inference(resolution,[status(thm)],[c378, c3])).
% 1.54/1.75  cnf(c1064,plain,skolem0001!=X883|relation(X883,skolem0005),inference(resolution,[status(thm)],[c383, reflexivity])).
% 1.54/1.75  cnf(c382,plain,skolem0001!=X783|skolem0003!=X782|relation(X783,X782),inference(resolution,[status(thm)],[c377, c3])).
% 1.54/1.75  cnf(c1060,plain,skolem0001!=X880|relation(X880,skolem0003),inference(resolution,[status(thm)],[c382, reflexivity])).
% 1.54/1.75  cnf(c380,plain,skolem0001!=X773|skolem0008!=X774|organism(X773,X774),inference(resolution,[status(thm)],[c18, c314])).
% 1.54/1.75  cnf(c1052,plain,skolem0001!=X877|organism(X877,skolem0008),inference(resolution,[status(thm)],[c380, reflexivity])).
% 1.54/1.75  cnf(c410,plain,skolem0001!=X876|skolem0002!=X875|entity(X876,X875),inference(resolution,[status(thm)],[c21, c319])).
% 1.54/1.75  cnf(c1051,plain,skolem0001!=X874|organism(X874,skolem0002),inference(resolution,[status(thm)],[c380, c449])).
% 1.54/1.75  cnf(c379,plain,skolem0001!=X769|skolem0004!=X770|organism(X769,X770),inference(resolution,[status(thm)],[c18, c312])).
% 1.54/1.75  cnf(c1048,plain,skolem0001!=X873|organism(X873,skolem0004),inference(resolution,[status(thm)],[c379, reflexivity])).
% 1.54/1.75  cnf(c1047,plain,~accessible_world(skolem0007,X872)|vincent_forename(X872,skolem0005),inference(resolution,[status(thm)],[c1044, c176])).
% 1.54/1.75  cnf(c1041,plain,~accessible_world(skolem0007,X869)|proposition(X869,skolem0007),inference(resolution,[status(thm)],[c1040, c173])).
% 1.54/1.75  cnf(c376,plain,skolem0001!=X765|skolem0005!=X766|relname(X765,X766),inference(resolution,[status(thm)],[c374, c12])).
% 1.54/1.75  cnf(c1039,plain,skolem0001!=X868|relname(X868,skolem0005),inference(resolution,[status(thm)],[c376, reflexivity])).
% 1.54/1.75  cnf(c1038,plain,~accessible_world(skolem0007,X867)|think_believe_consider(X867,skolem0006),inference(resolution,[status(thm)],[c1036, c167])).
% 1.54/1.75  cnf(c375,plain,skolem0001!=X759|skolem0003!=X760|relname(X759,X760),inference(resolution,[status(thm)],[c373, c12])).
% 1.54/1.75  cnf(c1035,plain,skolem0001!=X864|relname(X864,skolem0003),inference(resolution,[status(thm)],[c375, reflexivity])).
% 1.54/1.75  cnf(c1029,plain,~accessible_world(skolem0007,X861)|present(X861,skolem0006),inference(resolution,[status(thm)],[c1027, c161])).
% 1.54/1.75  cnf(c346,plain,human(skolem0001,skolem0004),inference(resolution,[status(thm)],[c243, c311])).
% 1.54/1.75  cnf(c371,plain,skolem0001!=X747|skolem0004!=X748|human(X747,X748),inference(resolution,[status(thm)],[c17, c346])).
% 1.54/1.75  cnf(c1026,plain,skolem0001!=X858|human(X858,skolem0004),inference(resolution,[status(thm)],[c371, reflexivity])).
% 1.54/1.75  cnf(c1025,plain,~accessible_world(skolem0007,X857)|jules_forename(X857,skolem0003),inference(resolution,[status(thm)],[c1022, c152])).
% 1.54/1.75  cnf(c347,plain,human(skolem0001,skolem0002),inference(resolution,[status(thm)],[c243, c309])).
% 1.54/1.75  cnf(c370,plain,skolem0001!=X742|skolem0002!=X743|human(X742,X743),inference(resolution,[status(thm)],[c17, c347])).
% 1.54/1.75  cnf(c1021,plain,skolem0001!=X856|human(X856,skolem0002),inference(resolution,[status(thm)],[c370, reflexivity])).
% 1.54/1.75  cnf(c1020,plain,skolem0001!=X853|human(X853,skolem0008),inference(resolution,[status(thm)],[c370, c447])).
% 1.54/1.75  cnf(c360,plain,male(skolem0001,skolem0004),inference(resolution,[status(thm)],[c249, c48])).
% 1.54/1.75  cnf(c368,plain,skolem0001!=X737|skolem0004!=X736|male(X737,X736),inference(resolution,[status(thm)],[c360, c14])).
% 1.54/1.75  cnf(c1018,plain,skolem0001!=X852|male(X852,skolem0004),inference(resolution,[status(thm)],[c368, reflexivity])).
% 1.54/1.75  cnf(c358,plain,male(skolem0001,skolem0002),inference(resolution,[status(thm)],[c249, c44])).
% 1.54/1.75  cnf(c364,plain,skolem0001!=X726|skolem0002!=X725|male(X726,X725),inference(resolution,[status(thm)],[c358, c14])).
% 1.54/1.75  cnf(c1012,plain,skolem0001!=X847|male(X847,skolem0002),inference(resolution,[status(thm)],[c364, reflexivity])).
% 1.54/1.75  cnf(c1011,plain,skolem0001!=X846|male(X846,skolem0008),inference(resolution,[status(thm)],[c364, c447])).
% 1.54/1.75  cnf(c338,plain,impartial(skolem0001,skolem0008),inference(resolution,[status(thm)],[c237, c314])).
% 1.54/1.75  cnf(c399,plain,skolem0001!=X844|skolem0008!=X845|impartial(X844,X845),inference(resolution,[status(thm)],[c20, c338])).
% 1.54/1.75  cnf(c355,plain,animate(skolem0001,skolem0004),inference(resolution,[status(thm)],[c246, c311])).
% 1.54/1.75  cnf(c363,plain,skolem0001!=X722|skolem0004!=X721|animate(X722,X721),inference(resolution,[status(thm)],[c16, c355])).
% 1.54/1.75  cnf(c1005,plain,skolem0001!=X843|animate(X843,skolem0004),inference(resolution,[status(thm)],[c363, reflexivity])).
% 1.54/1.75  cnf(c356,plain,animate(skolem0001,skolem0002),inference(resolution,[status(thm)],[c246, c309])).
% 1.54/1.75  cnf(c361,plain,skolem0001!=X713|skolem0002!=X712|animate(X713,X712),inference(resolution,[status(thm)],[c16, c356])).
% 1.54/1.75  cnf(c998,plain,skolem0001!=X840|animate(X840,skolem0002),inference(resolution,[status(thm)],[c361, reflexivity])).
% 1.54/1.75  cnf(c997,plain,skolem0001!=X837|animate(X837,skolem0008),inference(resolution,[status(thm)],[c361, c447])).
% 1.54/1.75  fof(ax45,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&nonhuman(V,U))=>nonhuman(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax45)).
% 1.54/1.75  fof(c144,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~nonhuman(V,U))|nonhuman(W,U))))),inference(fof_nnf,[status(thm)],[ax45])).
% 1.54/1.75  fof(c145,plain,(![X98]:(![X99]:(![X100]:((~accessible_world(X99,X100)|~nonhuman(X99,X98))|nonhuman(X100,X98))))),inference(variable_rename,[status(thm)],[c144])).
% 1.54/1.75  cnf(c146,plain,~accessible_world(X587,X585)|~nonhuman(X587,X586)|nonhuman(X585,X586),inference(split_conjunct,[status(thm)],[c145])).
% 1.54/1.75  cnf(c994,plain,~accessible_world(skolem0007,X836)|nonhuman(X836,skolem0007),inference(resolution,[status(thm)],[c985, c146])).
% 1.54/1.75  fof(ax44,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&general(V,U))=>general(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax44)).
% 1.54/1.75  fof(c147,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~general(V,U))|general(W,U))))),inference(fof_nnf,[status(thm)],[ax44])).
% 1.54/1.75  fof(c148,plain,(![X101]:(![X102]:(![X103]:((~accessible_world(X102,X103)|~general(X102,X101))|general(X103,X101))))),inference(variable_rename,[status(thm)],[c147])).
% 1.54/1.75  cnf(c149,plain,~accessible_world(X589,X588)|~general(X589,X590)|general(X588,X590),inference(split_conjunct,[status(thm)],[c148])).
% 1.54/1.75  cnf(c989,plain,~accessible_world(skolem0007,X831)|general(X831,skolem0007),inference(resolution,[status(thm)],[c984, c149])).
% 1.54/1.75  fof(ax46,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&abstraction(V,U))=>abstraction(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax46)).
% 1.54/1.75  fof(c141,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~abstraction(V,U))|abstraction(W,U))))),inference(fof_nnf,[status(thm)],[ax46])).
% 1.54/1.75  fof(c142,plain,(![X95]:(![X96]:(![X97]:((~accessible_world(X96,X97)|~abstraction(X96,X95))|abstraction(X97,X95))))),inference(variable_rename,[status(thm)],[c141])).
% 1.54/1.75  cnf(c143,plain,~accessible_world(X583,X582)|~abstraction(X583,X581)|abstraction(X582,X581),inference(split_conjunct,[status(thm)],[c142])).
% 1.54/1.76  cnf(c983,plain,~accessible_world(skolem0007,X830)|abstraction(X830,skolem0007),inference(resolution,[status(thm)],[c982, c143])).
% 1.54/1.76  cnf(c980,plain,~accessible_world(skolem0007,X829)|relation(X829,skolem0007),inference(resolution,[status(thm)],[c979, c140])).
% 1.54/1.76  cnf(c353,plain,skolem0001!=X706|skolem0002!=X705|human_person(X706,X705),inference(resolution,[status(thm)],[c15, c309])).
% 1.54/1.76  cnf(c978,plain,skolem0001!=X828|human_person(X828,skolem0002),inference(resolution,[status(thm)],[c353, reflexivity])).
% 1.54/1.76  cnf(c977,plain,skolem0001!=X825|human_person(X825,skolem0008),inference(resolution,[status(thm)],[c353, c447])).
% 1.54/1.76  cnf(c352,plain,skolem0001!=X701|skolem0004!=X700|human_person(X701,X700),inference(resolution,[status(thm)],[c15, c311])).
% 1.54/1.76  cnf(c974,plain,skolem0001!=X824|human_person(X824,skolem0004),inference(resolution,[status(thm)],[c352, reflexivity])).
% 1.54/1.76  cnf(c345,plain,skolem0001!=X696|skolem0004!=X697|man(X696,X697),inference(resolution,[status(thm)],[c13, c48])).
% 1.54/1.76  cnf(c973,plain,skolem0001!=X821|man(X821,skolem0004),inference(resolution,[status(thm)],[c345, reflexivity])).
% 1.54/1.76  cnf(c971,plain,~accessible_world(skolem0007,X820)|nonhuman(X820,skolem0005),inference(resolution,[status(thm)],[c964, c146])).
% 1.54/1.76  cnf(c968,plain,~accessible_world(skolem0007,X819)|general(X819,skolem0005),inference(resolution,[status(thm)],[c963, c149])).
% 1.54/1.76  cnf(c962,plain,~accessible_world(skolem0007,X818)|abstraction(X818,skolem0005),inference(resolution,[status(thm)],[c961, c143])).
% 1.54/1.76  cnf(c959,plain,~accessible_world(skolem0007,X817)|relation(X817,skolem0005),inference(resolution,[status(thm)],[c958, c140])).
% 1.54/1.76  cnf(c342,plain,living(skolem0001,skolem0002),inference(resolution,[status(thm)],[c240, c313])).
% 1.54/1.76  cnf(c390,plain,skolem0001!=X815|skolem0002!=X816|living(X815,X816),inference(resolution,[status(thm)],[c19, c342])).
% 1.54/1.76  fof(ax48,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&relname(V,U))=>relname(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax48)).
% 1.54/1.76  fof(c135,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~relname(V,U))|relname(W,U))))),inference(fof_nnf,[status(thm)],[ax48])).
% 1.54/1.76  fof(c136,plain,(![X89]:(![X90]:(![X91]:((~accessible_world(X90,X91)|~relname(X90,X89))|relname(X91,X89))))),inference(variable_rename,[status(thm)],[c135])).
% 1.54/1.76  cnf(c137,plain,~accessible_world(X577,X576)|~relname(X577,X575)|relname(X576,X575),inference(split_conjunct,[status(thm)],[c136])).
% 1.54/1.76  cnf(c956,plain,~accessible_world(skolem0007,X814)|relname(X814,skolem0005),inference(resolution,[status(thm)],[c951, c137])).
% 1.54/1.76  cnf(c952,plain,~accessible_world(skolem0007,X811)|forename(X811,skolem0005),inference(resolution,[status(thm)],[c950, c134])).
% 1.54/1.76  cnf(c343,plain,skolem0001!=X691|skolem0002!=X692|man(X691,X692),inference(resolution,[status(thm)],[c13, c44])).
% 1.54/1.76  cnf(c949,plain,skolem0001!=X808|man(X808,skolem0002),inference(resolution,[status(thm)],[c343, reflexivity])).
% 1.54/1.76  cnf(c948,plain,skolem0001!=X807|man(X807,skolem0008),inference(resolution,[status(thm)],[c343, c447])).
% 1.54/1.76  cnf(c946,plain,~accessible_world(skolem0007,X806)|nonhuman(X806,skolem0003),inference(resolution,[status(thm)],[c939, c146])).
% 1.54/1.76  cnf(c943,plain,~accessible_world(skolem0007,X805)|general(X805,skolem0003),inference(resolution,[status(thm)],[c938, c149])).
% 1.54/1.76  cnf(c937,plain,~accessible_world(skolem0007,X802)|abstraction(X802,skolem0003),inference(resolution,[status(thm)],[c936, c143])).
% 1.54/1.76  cnf(c934,plain,~accessible_world(skolem0007,X801)|relation(X801,skolem0003),inference(resolution,[status(thm)],[c933, c140])).
% 1.54/1.76  cnf(c931,plain,~accessible_world(skolem0007,X800)|relname(X800,skolem0003),inference(resolution,[status(thm)],[c927, c137])).
% 1.54/1.76  cnf(c333,plain,skolem0001!=X689|skolem0004!=X690|thing(X689,X690),inference(resolution,[status(thm)],[c11, c320])).
% 1.54/1.76  cnf(c930,plain,skolem0001!=X799|thing(X799,skolem0004),inference(resolution,[status(thm)],[c333, reflexivity])).
% 1.54/1.76  cnf(c928,plain,~accessible_world(skolem0007,X796)|forename(X796,skolem0003),inference(resolution,[status(thm)],[c926, c134])).
% 1.54/1.76  cnf(c332,plain,skolem0001!=X683|skolem0009!=X684|thing(X683,X684),inference(resolution,[status(thm)],[c11, c291])).
% 1.54/1.76  cnf(c925,plain,skolem0001!=X795|thing(X795,skolem0009),inference(resolution,[status(thm)],[c332, reflexivity])).
% 1.54/1.76  cnf(c331,plain,skolem0001!=X678|skolem0006!=X679|thing(X678,X679),inference(resolution,[status(thm)],[c11, c304])).
% 1.54/1.76  cnf(c923,plain,skolem0001!=X794|thing(X794,skolem0006),inference(resolution,[status(thm)],[c331, reflexivity])).
% 1.54/1.76  cnf(c329,plain,skolem0001!=X669|skolem0008!=X670|thing(X669,X670),inference(resolution,[status(thm)],[c11, c321])).
% 1.54/1.76  cnf(c913,plain,skolem0001!=X789|thing(X789,skolem0008),inference(resolution,[status(thm)],[c329, reflexivity])).
% 1.54/1.76  cnf(c912,plain,skolem0001!=X786|thing(X786,skolem0002),inference(resolution,[status(thm)],[c329, c449])).
% 1.54/1.76  cnf(c302,plain,unisex(skolem0001,skolem0006),inference(resolution,[status(thm)],[c298, c210])).
% 1.54/1.76  cnf(c316,plain,skolem0001!=X664|skolem0006!=X665|unisex(X664,X665),inference(resolution,[status(thm)],[c8, c302])).
% 1.54/1.76  cnf(c909,plain,skolem0001!=X785|unisex(X785,skolem0006),inference(resolution,[status(thm)],[c316, reflexivity])).
% 1.54/1.76  cnf(c296,plain,unisex(skolem0001,skolem0009),inference(resolution,[status(thm)],[c210, c289])).
% 1.54/1.76  cnf(c315,plain,skolem0001!=X658|skolem0009!=X659|unisex(X658,X659),inference(resolution,[status(thm)],[c8, c296])).
% 1.54/1.76  cnf(c906,plain,skolem0001!=X784|unisex(X784,skolem0009),inference(resolution,[status(thm)],[c315, reflexivity])).
% 1.54/1.76  cnf(c308,plain,skolem0001!=X654|skolem0003!=X655|jules_forename(X654,X655),inference(resolution,[status(thm)],[c6, c45])).
% 1.54/1.76  cnf(c903,plain,skolem0001!=X781|jules_forename(X781,skolem0003),inference(resolution,[status(thm)],[c308, reflexivity])).
% 1.54/1.76  cnf(c297,plain,event(skolem0001,skolem0009),inference(resolution,[status(thm)],[c213, c63])).
% 1.54/1.76  cnf(c301,plain,skolem0001!=X650|skolem0009!=X649|event(X650,X649),inference(resolution,[status(thm)],[c5, c297])).
% 1.54/1.76  cnf(c900,plain,skolem0001!=X780|event(X780,skolem0009),inference(resolution,[status(thm)],[c301, reflexivity])).
% 1.54/1.76  cnf(c381,plain,skolem0001!=X778|skolem0002!=X779|organism(X778,X779),inference(resolution,[status(thm)],[c18, c313])).
% 1.54/1.76  cnf(c300,plain,skolem0001!=X645|skolem0006!=X644|event(X645,X644),inference(resolution,[status(thm)],[c5, c54])).
% 1.54/1.76  cnf(c896,plain,skolem0001!=X777|event(X777,skolem0006),inference(resolution,[status(thm)],[c300, reflexivity])).
% 1.54/1.76  cnf(c290,plain,skolem0001!=X640|skolem0007!=X639|proposition(X640,X639),inference(resolution,[status(thm)],[c2, c51])).
% 1.54/1.76  cnf(c893,plain,skolem0001!=X776|proposition(X776,skolem0007),inference(resolution,[status(thm)],[c290, reflexivity])).
% 1.54/1.76  cnf(c288,plain,skolem0001!=X634|skolem0005!=X635|forename(X634,X635),inference(resolution,[status(thm)],[c1, c50])).
% 1.54/1.76  cnf(c890,plain,skolem0001!=X775|forename(X775,skolem0005),inference(resolution,[status(thm)],[c288, reflexivity])).
% 1.54/1.76  cnf(c287,plain,skolem0001!=X630|skolem0003!=X631|forename(X630,X631),inference(resolution,[status(thm)],[c1, c46])).
% 1.54/1.76  cnf(c887,plain,skolem0001!=X772|forename(X772,skolem0003),inference(resolution,[status(thm)],[c287, reflexivity])).
% 1.54/1.76  cnf(c286,plain,skolem0001!=X625|skolem0005!=X626|vincent_forename(X625,X626),inference(resolution,[status(thm)],[c0, c49])).
% 1.54/1.76  cnf(c884,plain,skolem0001!=X771|vincent_forename(X771,skolem0005),inference(resolution,[status(thm)],[c286, reflexivity])).
% 1.54/1.76  fof(ax55,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&existent(V,U))=>existent(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax55)).
% 1.54/1.76  fof(c114,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~existent(V,U))|existent(W,U))))),inference(fof_nnf,[status(thm)],[ax55])).
% 1.54/1.76  fof(c115,plain,(![X68]:(![X69]:(![X70]:((~accessible_world(X69,X70)|~existent(X69,X68))|existent(X70,X68))))),inference(variable_rename,[status(thm)],[c114])).
% 1.54/1.76  cnf(c116,plain,~accessible_world(X541,X540)|~existent(X541,X542)|existent(X540,X542),inference(split_conjunct,[status(thm)],[c115])).
% 1.54/1.76  cnf(c851,plain,~accessible_world(skolem0007,X764)|existent(X764,skolem0004),inference(resolution,[status(thm)],[c844, c116])).
% 1.54/1.76  fof(ax54,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&impartial(V,U))=>impartial(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax54)).
% 1.54/1.76  fof(c117,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~impartial(V,U))|impartial(W,U))))),inference(fof_nnf,[status(thm)],[ax54])).
% 1.54/1.76  fof(c118,plain,(![X71]:(![X72]:(![X73]:((~accessible_world(X72,X73)|~impartial(X72,X71))|impartial(X73,X71))))),inference(variable_rename,[status(thm)],[c117])).
% 1.54/1.76  cnf(c119,plain,~accessible_world(X548,X547)|~impartial(X548,X549)|impartial(X547,X549),inference(split_conjunct,[status(thm)],[c118])).
% 1.54/1.76  cnf(c848,plain,~accessible_world(skolem0007,X762)|impartial(X762,skolem0004),inference(resolution,[status(thm)],[c836, c119])).
% 1.54/1.76  fof(ax53,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&living(V,U))=>living(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax53)).
% 1.54/1.76  fof(c120,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~living(V,U))|living(W,U))))),inference(fof_nnf,[status(thm)],[ax53])).
% 1.54/1.76  fof(c121,plain,(![X74]:(![X75]:(![X76]:((~accessible_world(X75,X76)|~living(X75,X74))|living(X76,X74))))),inference(variable_rename,[status(thm)],[c120])).
% 1.54/1.76  cnf(c122,plain,~accessible_world(X553,X555)|~living(X553,X554)|living(X555,X554),inference(split_conjunct,[status(thm)],[c121])).
% 1.54/1.76  cnf(c845,plain,~accessible_world(skolem0007,X761)|living(X761,skolem0004),inference(resolution,[status(thm)],[c834, c122])).
% 1.54/1.76  fof(ax56,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&entity(V,U))=>entity(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax56)).
% 1.54/1.76  fof(c111,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~entity(V,U))|entity(W,U))))),inference(fof_nnf,[status(thm)],[ax56])).
% 1.54/1.76  fof(c112,plain,(![X65]:(![X66]:(![X67]:((~accessible_world(X66,X67)|~entity(X66,X65))|entity(X67,X65))))),inference(variable_rename,[status(thm)],[c111])).
% 1.54/1.76  cnf(c113,plain,~accessible_world(X536,X537)|~entity(X536,X535)|entity(X537,X535),inference(split_conjunct,[status(thm)],[c112])).
% 1.54/1.76  cnf(c842,plain,~accessible_world(skolem0007,X758)|entity(X758,skolem0004),inference(resolution,[status(thm)],[c832, c113])).
% 1.54/1.76  fof(ax52,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&human(V,U))=>human(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax52)).
% 1.54/1.76  fof(c123,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~human(V,U))|human(W,U))))),inference(fof_nnf,[status(thm)],[ax52])).
% 1.54/1.76  fof(c124,plain,(![X77]:(![X78]:(![X79]:((~accessible_world(X78,X79)|~human(X78,X77))|human(X79,X77))))),inference(variable_rename,[status(thm)],[c123])).
% 1.54/1.76  cnf(c125,plain,~accessible_world(X560,X559)|~human(X560,X561)|human(X559,X561),inference(split_conjunct,[status(thm)],[c124])).
% 1.54/1.76  cnf(c837,plain,~accessible_world(skolem0007,X757)|human(X757,skolem0004),inference(resolution,[status(thm)],[c828, c125])).
% 1.54/1.76  fof(ax57,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&organism(V,U))=>organism(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax57)).
% 1.54/1.76  fof(c108,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~organism(V,U))|organism(W,U))))),inference(fof_nnf,[status(thm)],[ax57])).
% 1.54/1.76  fof(c109,plain,(![X62]:(![X63]:(![X64]:((~accessible_world(X63,X64)|~organism(X63,X62))|organism(X64,X62))))),inference(variable_rename,[status(thm)],[c108])).
% 1.54/1.76  cnf(c110,plain,~accessible_world(X531,X530)|~organism(X531,X529)|organism(X530,X529),inference(split_conjunct,[status(thm)],[c109])).
% 1.54/1.76  cnf(c833,plain,~accessible_world(skolem0007,X756)|organism(X756,skolem0004),inference(resolution,[status(thm)],[c826, c110])).
% 1.54/1.76  fof(ax51,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&animate(V,U))=>animate(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax51)).
% 1.54/1.76  fof(c126,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~animate(V,U))|animate(W,U))))),inference(fof_nnf,[status(thm)],[ax51])).
% 1.54/1.76  fof(c127,plain,(![X80]:(![X81]:(![X82]:((~accessible_world(X81,X82)|~animate(X81,X80))|animate(X82,X80))))),inference(variable_rename,[status(thm)],[c126])).
% 1.54/1.76  cnf(c128,plain,~accessible_world(X566,X564)|~animate(X566,X565)|animate(X564,X565),inference(split_conjunct,[status(thm)],[c127])).
% 1.54/1.76  cnf(c830,plain,~accessible_world(skolem0007,X755)|animate(X755,skolem0004),inference(resolution,[status(thm)],[c825, c128])).
% 1.54/1.76  fof(ax58,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&human_person(V,U))=>human_person(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax58)).
% 1.54/1.76  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.54/1.76  fof(c106,plain,(![X59]:(![X60]:(![X61]:((~accessible_world(X60,X61)|~human_person(X60,X59))|human_person(X61,X59))))),inference(variable_rename,[status(thm)],[c105])).
% 1.54/1.76  cnf(c107,plain,~accessible_world(X522,X523)|~human_person(X522,X524)|human_person(X523,X524),inference(split_conjunct,[status(thm)],[c106])).
% 1.54/1.76  cnf(c827,plain,~accessible_world(skolem0007,X754)|human_person(X754,skolem0004),inference(resolution,[status(thm)],[c820, c107])).
% 1.54/1.76  cnf(c348,plain,human(skolem0001,skolem0008),inference(resolution,[status(thm)],[c243, c310])).
% 1.54/1.76  cnf(c372,plain,skolem0001!=X752|skolem0008!=X753|human(X752,X753),inference(resolution,[status(thm)],[c17, c348])).
% 1.54/1.76  fof(ax50,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&male(V,U))=>male(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax50)).
% 1.54/1.76  fof(c129,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~male(V,U))|male(W,U))))),inference(fof_nnf,[status(thm)],[ax50])).
% 1.54/1.76  fof(c130,plain,(![X83]:(![X84]:(![X85]:((~accessible_world(X84,X85)|~male(X84,X83))|male(X85,X83))))),inference(variable_rename,[status(thm)],[c129])).
% 1.54/1.76  cnf(c131,plain,~accessible_world(X570,X571)|~male(X570,X569)|male(X571,X569),inference(split_conjunct,[status(thm)],[c130])).
% 1.54/1.76  cnf(c823,plain,~accessible_world(skolem0007,X751)|male(X751,skolem0004),inference(resolution,[status(thm)],[c816, c131])).
% 1.54/1.76  cnf(c814,plain,~accessible_world(skolem0007,X750)|man(X750,skolem0004),inference(resolution,[status(thm)],[c809, c104])).
% 1.54/1.76  cnf(c780,plain,~accessible_world(skolem0007,X746)|existent(X746,skolem0008),inference(resolution,[status(thm)],[c773, c116])).
% 1.54/1.76  cnf(c777,plain,~accessible_world(skolem0007,X744)|impartial(X744,skolem0008),inference(resolution,[status(thm)],[c762, c119])).
% 1.54/1.76  cnf(c774,plain,~accessible_world(skolem0007,X741)|living(X741,skolem0008),inference(resolution,[status(thm)],[c760, c122])).
% 1.54/1.76  cnf(c771,plain,~accessible_world(skolem0007,X740)|entity(X740,skolem0008),inference(resolution,[status(thm)],[c758, c113])).
% 1.54/1.76  cnf(c766,plain,~accessible_world(skolem0007,X739)|human(X739,skolem0008),inference(resolution,[status(thm)],[c755, c125])).
% 1.54/1.76  cnf(c765,plain,~accessible_world(skolem0001,X738)|general(X738,skolem0005),inference(resolution,[status(thm)],[c149, c404])).
% 1.54/1.76  cnf(c764,plain,~accessible_world(skolem0001,X735)|general(X735,skolem0007),inference(resolution,[status(thm)],[c149, c429])).
% 1.54/1.76  cnf(c763,plain,~accessible_world(skolem0001,X734)|general(X734,skolem0003),inference(resolution,[status(thm)],[c149, c405])).
% 1.54/1.76  cnf(c759,plain,~accessible_world(skolem0007,X733)|organism(X733,skolem0008),inference(resolution,[status(thm)],[c753, c110])).
% 1.54/1.76  cnf(c359,plain,male(skolem0001,skolem0008),inference(resolution,[status(thm)],[c249, c62])).
% 1.54/1.76  cnf(c366,plain,skolem0001!=X732|skolem0008!=X731|male(X732,X731),inference(resolution,[status(thm)],[c359, c14])).
% 1.54/1.76  cnf(c757,plain,~accessible_world(skolem0007,X730)|animate(X730,skolem0008),inference(resolution,[status(thm)],[c752, c128])).
% 1.54/1.76  cnf(c754,plain,~accessible_world(skolem0007,X729)|human_person(X729,skolem0008),inference(resolution,[status(thm)],[c744, c107])).
% 1.54/1.76  cnf(c750,plain,~accessible_world(skolem0007,X728)|male(X728,skolem0008),inference(resolution,[status(thm)],[c740, c131])).
% 1.54/1.76  cnf(c747,plain,~accessible_world(skolem0001,X727)|nonhuman(X727,skolem0007),inference(resolution,[status(thm)],[c146, c430])).
% 1.54/1.76  cnf(c746,plain,~accessible_world(skolem0001,X724)|nonhuman(X724,skolem0003),inference(resolution,[status(thm)],[c146, c401])).
% 1.54/1.76  cnf(c745,plain,~accessible_world(skolem0001,X723)|nonhuman(X723,skolem0005),inference(resolution,[status(thm)],[c146, c400])).
% 1.54/1.76  cnf(c738,plain,~accessible_world(skolem0007,X720)|man(X720,skolem0008),inference(resolution,[status(thm)],[c736, c104])).
% 1.54/1.76  cnf(c731,plain,~accessible_world(skolem0001,X719)|abstraction(X719,skolem0003),inference(resolution,[status(thm)],[c143, c384])).
% 1.54/1.76  cnf(c730,plain,~accessible_world(skolem0001,X718)|abstraction(X718,skolem0007),inference(resolution,[status(thm)],[c143, c428])).
% 1.54/1.76  cnf(c357,plain,animate(skolem0001,skolem0008),inference(resolution,[status(thm)],[c246, c310])).
% 1.54/1.76  cnf(c362,plain,skolem0001!=X717|skolem0008!=X716|animate(X717,X716),inference(resolution,[status(thm)],[c16, c357])).
% 1.54/1.76  cnf(c729,plain,~accessible_world(skolem0001,X715)|abstraction(X715,skolem0005),inference(resolution,[status(thm)],[c143, c385])).
% 1.54/1.76  cnf(c714,plain,~accessible_world(skolem0001,X714)|relation(X714,skolem0005),inference(resolution,[status(thm)],[c140, c378])).
% 1.54/1.76  cnf(c713,plain,~accessible_world(skolem0001,X711)|relation(X711,skolem0003),inference(resolution,[status(thm)],[c140, c377])).
% 1.54/1.76  fof(ax33,axiom,(![U]:(![V]:(specific(U,V)=>(~general(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax33)).
% 1.54/1.76  fof(c181,plain,(![U]:(![V]:(specific(U,V)=>~general(U,V)))),inference(fof_simplification,[status(thm)],[ax33])).
% 1.54/1.76  fof(c182,plain,(![U]:(![V]:(~specific(U,V)|~general(U,V)))),inference(fof_nnf,[status(thm)],[c181])).
% 1.54/1.76  fof(c183,plain,(![X136]:(![X137]:(~specific(X136,X137)|~general(X136,X137)))),inference(variable_rename,[status(thm)],[c182])).
% 1.54/1.76  cnf(c184,plain,~specific(X220,X219)|~general(X220,X219),inference(split_conjunct,[status(thm)],[c183])).
% 1.54/1.76  cnf(c991,plain,~specific(skolem0007,skolem0007),inference(resolution,[status(thm)],[c984, c184])).
% 1.54/1.76  cnf(c354,plain,skolem0001!=X710|skolem0008!=X709|human_person(X710,X709),inference(resolution,[status(thm)],[c15, c310])).
% 1.54/1.76  cnf(c705,plain,~accessible_world(skolem0007,X707)|existent(X707,skolem0002),inference(resolution,[status(thm)],[c697, c116])).
% 1.54/1.76  cnf(c703,plain,~accessible_world(skolem0001,X704)|relname(X704,skolem0005),inference(resolution,[status(thm)],[c137, c374])).
% 1.54/1.76  cnf(c702,plain,~accessible_world(skolem0001,X703)|relname(X703,skolem0003),inference(resolution,[status(thm)],[c137, c373])).
% 1.54/1.76  cnf(c701,plain,~accessible_world(skolem0007,X702)|impartial(X702,skolem0002),inference(resolution,[status(thm)],[c687, c119])).
% 1.54/1.76  cnf(c698,plain,~accessible_world(skolem0007,X699)|living(X699,skolem0002),inference(resolution,[status(thm)],[c685, c122])).
% 1.54/1.76  cnf(c695,plain,~accessible_world(skolem0007,X698)|entity(X698,skolem0002),inference(resolution,[status(thm)],[c683, c113])).
% 1.54/1.76  cnf(c970,plain,~specific(skolem0007,skolem0005),inference(resolution,[status(thm)],[c963, c184])).
% 1.54/1.76  cnf(c344,plain,skolem0001!=X694|skolem0008!=X695|man(X694,X695),inference(resolution,[status(thm)],[c13, c62])).
% 1.54/1.76  cnf(c945,plain,~specific(skolem0007,skolem0003),inference(resolution,[status(thm)],[c938, c184])).
% 1.54/1.76  cnf(c688,plain,~accessible_world(skolem0007,X687)|human(X687,skolem0002),inference(resolution,[status(thm)],[c680, c125])).
% 1.54/1.76  cnf(c684,plain,~accessible_world(skolem0007,X686)|organism(X686,skolem0002),inference(resolution,[status(thm)],[c678, c110])).
% 1.54/1.76  cnf(c682,plain,~accessible_world(skolem0007,X685)|animate(X685,skolem0002),inference(resolution,[status(thm)],[c677, c128])).
% 1.54/1.76  cnf(c679,plain,~accessible_world(skolem0007,X682)|human_person(X682,skolem0002),inference(resolution,[status(thm)],[c669, c107])).
% 1.54/1.76  cnf(c675,plain,~accessible_world(skolem0001,X681)|male(X681,skolem0008),inference(resolution,[status(thm)],[c131, c359])).
% 1.54/1.76  cnf(c674,plain,~accessible_world(skolem0007,X680)|male(X680,skolem0002),inference(resolution,[status(thm)],[c131, c665])).
% 1.54/1.76  cnf(c673,plain,~accessible_world(skolem0001,X677)|male(X677,skolem0002),inference(resolution,[status(thm)],[c131, c358])).
% 1.54/1.76  cnf(c672,plain,~accessible_world(skolem0001,X676)|male(X676,skolem0004),inference(resolution,[status(thm)],[c131, c360])).
% 1.54/1.76  cnf(c663,plain,~accessible_world(skolem0007,X675)|man(X675,skolem0002),inference(resolution,[status(thm)],[c661, c104])).
% 1.54/1.76  cnf(c330,plain,skolem0001!=X673|skolem0002!=X674|thing(X673,X674),inference(resolution,[status(thm)],[c11, c322])).
% 1.54/1.76  cnf(c659,plain,~accessible_world(skolem0001,X672)|animate(X672,skolem0004),inference(resolution,[status(thm)],[c128, c355])).
% 1.54/1.76  cnf(c658,plain,~accessible_world(skolem0001,X671)|animate(X671,skolem0008),inference(resolution,[status(thm)],[c128, c357])).
% 1.54/1.76  cnf(c657,plain,~accessible_world(skolem0001,X668)|animate(X668,skolem0002),inference(resolution,[status(thm)],[c128, c356])).
% 1.54/1.76  cnf(c654,plain,~accessible_world(skolem0007,X667)|event(X667,skolem0006),inference(resolution,[status(thm)],[c653, c101])).
% 1.54/1.76  cnf(c652,plain,~accessible_world(skolem0001,X666)|human(X666,skolem0008),inference(resolution,[status(thm)],[c125, c348])).
% 1.54/1.76  cnf(c651,plain,~accessible_world(skolem0001,X663)|human(X663,skolem0004),inference(resolution,[status(thm)],[c125, c346])).
% 1.54/1.76  cnf(c650,plain,~accessible_world(skolem0001,X662)|human(X662,skolem0002),inference(resolution,[status(thm)],[c125, c347])).
% 1.54/1.76  cnf(c648,plain,~accessible_world(skolem0007,X661)|unisex(X661,skolem0007),inference(resolution,[status(thm)],[c646, c98])).
% 1.54/1.76  cnf(c645,plain,~accessible_world(skolem0007,X660)|unisex(X660,skolem0005),inference(resolution,[status(thm)],[c643, c98])).
% 1.54/1.76  cnf(c642,plain,~accessible_world(skolem0001,X657)|living(X657,skolem0002),inference(resolution,[status(thm)],[c122, c342])).
% 1.54/1.76  cnf(c641,plain,~accessible_world(skolem0001,X656)|living(X656,skolem0008),inference(resolution,[status(thm)],[c122, c341])).
% 1.54/1.76  cnf(c640,plain,~accessible_world(skolem0001,X653)|living(X653,skolem0004),inference(resolution,[status(thm)],[c122, c340])).
% 1.54/1.76  cnf(c639,plain,~accessible_world(skolem0007,X652)|unisex(X652,skolem0003),inference(resolution,[status(thm)],[c637, c98])).
% 1.54/1.76  cnf(c636,plain,~accessible_world(skolem0001,X651)|impartial(X651,skolem0008),inference(resolution,[status(thm)],[c119, c338])).
% 1.54/1.76  cnf(c635,plain,~accessible_world(skolem0001,X648)|impartial(X648,skolem0002),inference(resolution,[status(thm)],[c119, c339])).
% 1.54/1.76  cnf(c634,plain,~accessible_world(skolem0001,X647)|impartial(X647,skolem0004),inference(resolution,[status(thm)],[c119, c337])).
% 1.54/1.76  cnf(c631,plain,~accessible_world(skolem0001,X646)|existent(X646,skolem0002),inference(resolution,[status(thm)],[c116, c336])).
% 1.54/1.76  cnf(c630,plain,~accessible_world(skolem0001,X643)|existent(X643,skolem0008),inference(resolution,[status(thm)],[c116, c335])).
% 1.54/1.76  cnf(c629,plain,~accessible_world(skolem0001,X642)|existent(X642,skolem0004),inference(resolution,[status(thm)],[c116, c334])).
% 1.54/1.76  cnf(c627,plain,~accessible_world(skolem0007,X641)|specific(X641,skolem0002),inference(resolution,[status(thm)],[c625, c92])).
% 1.54/1.76  cnf(c624,plain,~accessible_world(skolem0007,X638)|specific(X638,skolem0004),inference(resolution,[status(thm)],[c619, c92])).
% 1.54/1.76  cnf(c622,plain,~accessible_world(skolem0001,X637)|entity(X637,skolem0002),inference(resolution,[status(thm)],[c113, c319])).
% 1.54/1.76  cnf(c621,plain,~accessible_world(skolem0001,X636)|entity(X636,skolem0008),inference(resolution,[status(thm)],[c113, c318])).
% 1.54/1.76  cnf(c620,plain,~accessible_world(skolem0001,X633)|entity(X633,skolem0004),inference(resolution,[status(thm)],[c113, c317])).
% 1.54/1.76  cnf(c617,plain,~accessible_world(skolem0001,X632)|organism(X632,skolem0002),inference(resolution,[status(thm)],[c110, c313])).
% 1.54/1.76  cnf(c616,plain,~accessible_world(skolem0001,X629)|organism(X629,skolem0008),inference(resolution,[status(thm)],[c110, c314])).
% 1.54/1.76  cnf(c615,plain,~accessible_world(skolem0001,X628)|organism(X628,skolem0004),inference(resolution,[status(thm)],[c110, c312])).
% 1.54/1.76  cnf(c613,plain,~accessible_world(skolem0007,X627)|specific(X627,skolem0008),inference(resolution,[status(thm)],[c611, c92])).
% 1.54/1.76  cnf(c610,plain,~accessible_world(skolem0001,X624)|human_person(X624,skolem0008),inference(resolution,[status(thm)],[c107, c310])).
% 1.54/1.76  cnf(c609,plain,~accessible_world(skolem0001,X623)|human_person(X623,skolem0002),inference(resolution,[status(thm)],[c107, c309])).
% 1.54/1.76  cnf(c608,plain,~accessible_world(skolem0001,X622)|human_person(X622,skolem0004),inference(resolution,[status(thm)],[c107, c311])).
% 1.54/1.76  fof(ax31,axiom,(![U]:(![V]:(existent(U,V)=>(~nonexistent(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax31)).
% 1.54/1.76  fof(c189,plain,(![U]:(![V]:(existent(U,V)=>~nonexistent(U,V)))),inference(fof_simplification,[status(thm)],[ax31])).
% 1.54/1.76  fof(c190,plain,(![U]:(![V]:(~existent(U,V)|~nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[c189])).
% 1.54/1.76  fof(c191,plain,(![X140]:(![X141]:(~existent(X140,X141)|~nonexistent(X140,X141)))),inference(variable_rename,[status(thm)],[c190])).
% 1.54/1.76  cnf(c192,plain,~existent(X224,X223)|~nonexistent(X224,X223),inference(split_conjunct,[status(thm)],[c191])).
% 1.54/1.76  cnf(c871,plain,~existent(skolem0007,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c864, c192])).
% 1.54/1.76  fof(ax32,axiom,(![U]:(![V]:(nonhuman(U,V)=>(~human(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax32)).
% 1.54/1.76  fof(c185,plain,(![U]:(![V]:(nonhuman(U,V)=>~human(U,V)))),inference(fof_simplification,[status(thm)],[ax32])).
% 1.54/1.76  fof(c186,plain,(![U]:(![V]:(~nonhuman(U,V)|~human(U,V)))),inference(fof_nnf,[status(thm)],[c185])).
% 1.54/1.76  fof(c187,plain,(![X138]:(![X139]:(~nonhuman(X138,X139)|~human(X138,X139)))),inference(variable_rename,[status(thm)],[c186])).
% 1.54/1.76  cnf(c188,plain,~nonhuman(X221,X222)|~human(X221,X222),inference(split_conjunct,[status(thm)],[c187])).
% 1.54/1.76  cnf(c838,plain,~nonhuman(skolem0007,skolem0004),inference(resolution,[status(thm)],[c828, c188])).
% 1.54/1.76  fof(ax34,axiom,(![U]:(![V]:(unisex(U,V)=>(~male(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax34)).
% 1.54/1.76  fof(c177,plain,(![U]:(![V]:(unisex(U,V)=>~male(U,V)))),inference(fof_simplification,[status(thm)],[ax34])).
% 1.54/1.76  fof(c178,plain,(![U]:(![V]:(~unisex(U,V)|~male(U,V)))),inference(fof_nnf,[status(thm)],[c177])).
% 1.54/1.76  fof(c179,plain,(![X134]:(![X135]:(~unisex(X134,X135)|~male(X134,X135)))),inference(variable_rename,[status(thm)],[c178])).
% 1.54/1.76  cnf(c180,plain,~unisex(X217,X218)|~male(X217,X218),inference(split_conjunct,[status(thm)],[c179])).
% 1.54/1.76  cnf(c822,plain,~unisex(skolem0007,skolem0004),inference(resolution,[status(thm)],[c816, c180])).
% 1.54/1.76  cnf(c798,plain,~existent(skolem0007,skolem0010(skolem0008)),inference(resolution,[status(thm)],[c792, c192])).
% 1.54/1.76  cnf(c767,plain,~nonhuman(skolem0007,skolem0008),inference(resolution,[status(thm)],[c755, c188])).
% 1.54/1.76  cnf(c749,plain,~unisex(skolem0007,skolem0008),inference(resolution,[status(thm)],[c740, c180])).
% 1.54/1.76  cnf(c724,plain,~existent(skolem0007,skolem0010(skolem0002)),inference(resolution,[status(thm)],[c718, c192])).
% 1.54/1.76  cnf(c689,plain,~nonhuman(skolem0007,skolem0002),inference(resolution,[status(thm)],[c680, c188])).
% 1.54/1.76  cnf(c671,plain,~unisex(skolem0007,skolem0002),inference(resolution,[status(thm)],[c665, c180])).
% 1.54/1.76  cnf(c600,plain,~accessible_world(skolem0001,X567)|event(X567,skolem0009),inference(resolution,[status(thm)],[c101, c297])).
% 1.54/1.76  cnf(c598,plain,~accessible_world(skolem0007,X562)|event(X562,skolem0009),inference(resolution,[status(thm)],[c101, c470])).
% 1.54/1.76  cnf(c594,plain,~accessible_world(skolem0001,X558)|unisex(X558,skolem0006),inference(resolution,[status(thm)],[c98, c302])).
% 1.54/1.76  cnf(c591,plain,~accessible_world(skolem0007,X552)|unisex(X552,skolem0009),inference(resolution,[status(thm)],[c98, c477])).
% 1.54/1.76  cnf(c589,plain,~accessible_world(skolem0007,X550)|unisex(X550,skolem0006),inference(resolution,[status(thm)],[c98, c498])).
% 1.54/1.76  cnf(c588,plain,~accessible_world(skolem0001,X546)|unisex(X546,skolem0009),inference(resolution,[status(thm)],[c98, c296])).
% 1.54/1.76  cnf(c587,plain,~accessible_world(skolem0007,X545)|nonexistent(X545,skolem0006),inference(resolution,[status(thm)],[c95, c499])).
% 1.54/1.76  cnf(c586,plain,~accessible_world(skolem0007,X544)|nonexistent(X544,skolem0009),inference(resolution,[status(thm)],[c95, c478])).
% 1.54/1.76  cnf(c585,plain,~accessible_world(skolem0001,X543)|nonexistent(X543,skolem0006),inference(resolution,[status(thm)],[c95, c303])).
% 1.54/1.76  cnf(c584,plain,~accessible_world(skolem0001,X539)|nonexistent(X539,skolem0009),inference(resolution,[status(thm)],[c95, c294])).
% 1.54/1.76  cnf(c580,plain,~accessible_world(skolem0001,X533)|specific(X533,skolem0006),inference(resolution,[status(thm)],[c92, c305])).
% 1.54/1.76  cnf(c579,plain,~accessible_world(skolem0007,X532)|specific(X532,skolem0006),inference(resolution,[status(thm)],[c92, c501])).
% 1.54/1.76  cnf(c578,plain,~accessible_world(skolem0001,X528)|specific(X528,skolem0009),inference(resolution,[status(thm)],[c92, c293])).
% 1.54/1.76  cnf(c577,plain,~accessible_world(skolem0007,X527)|specific(X527,skolem0009),inference(resolution,[status(thm)],[c92, c480])).
% 1.54/1.76  cnf(c574,plain,~accessible_world(skolem0007,X525)|singleton(X525,skolem0003),inference(resolution,[status(thm)],[c557, c89])).
% 1.54/1.76  cnf(c573,plain,~accessible_world(skolem0001,X521)|singleton(X521,skolem0002),inference(resolution,[status(thm)],[c89, c325])).
% 1.54/1.76  cnf(c572,plain,~accessible_world(skolem0001,X520)|singleton(X520,skolem0005),inference(resolution,[status(thm)],[c89, c394])).
% 1.54/1.76  cnf(c571,plain,~accessible_world(skolem0001,X516)|singleton(X516,skolem0009),inference(resolution,[status(thm)],[c89, c292])).
% 1.54/1.76  cnf(c570,plain,~accessible_world(skolem0001,X515)|singleton(X515,skolem0006),inference(resolution,[status(thm)],[c89, c307])).
% 1.54/1.76  cnf(c569,plain,~accessible_world(skolem0007,X514)|singleton(X514,skolem0009),inference(resolution,[status(thm)],[c89, c486])).
% 1.54/1.76  cnf(c568,plain,~accessible_world(skolem0001,X510)|singleton(X510,skolem0007),inference(resolution,[status(thm)],[c89, c438])).
% 1.54/1.76  cnf(c567,plain,~accessible_world(skolem0001,X509)|singleton(X509,skolem0008),inference(resolution,[status(thm)],[c89, c324])).
% 1.54/1.76  cnf(c566,plain,~accessible_world(skolem0001,X508)|singleton(X508,skolem0003),inference(resolution,[status(thm)],[c89, c396])).
% 1.54/1.76  cnf(c565,plain,~accessible_world(skolem0007,X504)|singleton(X504,skolem0008),inference(resolution,[status(thm)],[c89, c529])).
% 1.54/1.76  cnf(c564,plain,~accessible_world(skolem0007,X503)|singleton(X503,skolem0002),inference(resolution,[status(thm)],[c89, c542])).
% 1.54/1.76  cnf(c563,plain,~accessible_world(skolem0007,X502)|singleton(X502,skolem0005),inference(resolution,[status(thm)],[c89, c524])).
% 1.54/1.76  cnf(c562,plain,~accessible_world(skolem0007,X501)|singleton(X501,skolem0006),inference(resolution,[status(thm)],[c89, c508])).
% 1.54/1.76  cnf(c561,plain,~accessible_world(skolem0007,X500)|singleton(X500,skolem0004),inference(resolution,[status(thm)],[c89, c552])).
% 1.54/1.76  cnf(c560,plain,~accessible_world(skolem0007,X496)|singleton(X496,skolem0007),inference(resolution,[status(thm)],[c89, c537])).
% 1.54/1.76  cnf(c559,plain,~accessible_world(skolem0001,X495)|singleton(X495,skolem0004),inference(resolution,[status(thm)],[c89, c323])).
% 1.54/1.76  cnf(c558,plain,~accessible_world(skolem0007,X494)|thing(X494,skolem0003),inference(resolution,[status(thm)],[c555, c86])).
% 1.54/1.76  cnf(c553,plain,~accessible_world(skolem0007,X493)|thing(X493,skolem0004),inference(resolution,[status(thm)],[c550, c86])).
% 1.54/1.76  cnf(c543,plain,~accessible_world(skolem0007,X489)|thing(X489,skolem0002),inference(resolution,[status(thm)],[c540, c86])).
% 1.54/1.76  cnf(c538,plain,~accessible_world(skolem0007,X488)|thing(X488,skolem0007),inference(resolution,[status(thm)],[c532, c86])).
% 1.54/1.76  cnf(c530,plain,~accessible_world(skolem0007,X487)|thing(X487,skolem0008),inference(resolution,[status(thm)],[c527, c86])).
% 1.54/1.76  cnf(c525,plain,~accessible_world(skolem0007,X486)|thing(X486,skolem0005),inference(resolution,[status(thm)],[c522, c86])).
% 1.54/1.76  cnf(c519,plain,~accessible_world(skolem0001,X475)|thing(X475,skolem0009),inference(resolution,[status(thm)],[c86, c291])).
% 1.54/1.76  cnf(c518,plain,~accessible_world(skolem0007,X474)|thing(X474,skolem0009),inference(resolution,[status(thm)],[c86, c479])).
% 1.54/1.76  cnf(c517,plain,~accessible_world(skolem0001,X473)|thing(X473,skolem0006),inference(resolution,[status(thm)],[c86, c304])).
% 1.54/1.76  cnf(c513,plain,~accessible_world(skolem0007,X459)|thing(X459,skolem0006),inference(resolution,[status(thm)],[c86, c500])).
% 1.54/1.76  cnf(c496,plain,~accessible_world(skolem0007,X453)|eventuality(X453,skolem0006),inference(resolution,[status(thm)],[c495, c83])).
% 1.54/1.76  cnf(c505,plain,~existent(skolem0007,skolem0006),inference(resolution,[status(thm)],[c499, c192])).
% 1.54/1.76  cnf(c491,plain,~accessible_world(skolem0001,X437)|eventuality(X437,skolem0009),inference(resolution,[status(thm)],[c83, c289])).
% 1.54/1.76  cnf(c490,plain,~accessible_world(skolem0007,X432)|eventuality(X432,skolem0009),inference(resolution,[status(thm)],[c83, c472])).
% 1.54/1.76  cnf(c473,plain,~accessible_world(skolem0007,X428)|state(X428,skolem0009),inference(resolution,[status(thm)],[c469, c80])).
% 1.54/1.76  cnf(c483,plain,~existent(skolem0007,skolem0009),inference(resolution,[status(thm)],[c478, c192])).
% 1.54/1.76  cnf(transitivity,axiom,X206!=X207|X207!=X208|X206=X208,theory(equality)).
% 1.54/1.76  cnf(c451,plain,X400!=skolem0008|X400=skolem0002,inference(resolution,[status(thm)],[c449, transitivity])).
% 1.54/1.76  cnf(c448,plain,X399!=skolem0002|X399=skolem0008,inference(resolution,[status(thm)],[c447, transitivity])).
% 1.54/1.76  cnf(c35,axiom,X384!=X385|~actual_world(X384)|actual_world(X385),theory(equality)).
% 1.54/1.76  cnf(c453,plain,~actual_world(skolem0008)|actual_world(skolem0002),inference(resolution,[status(thm)],[c449, c35])).
% 1.54/1.76  cnf(c450,plain,~actual_world(skolem0002)|actual_world(skolem0008),inference(resolution,[status(thm)],[c447, c35])).
% 1.54/1.76  fof(ax1,axiom,(![U]:(![V]:(vincent_forename(U,V)=>forename(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax1)).
% 1.54/1.76  fof(c280,plain,(![U]:(![V]:(~vincent_forename(U,V)|forename(U,V)))),inference(fof_nnf,[status(thm)],[ax1])).
% 1.54/1.76  fof(c281,plain,(![X200]:(![X201]:(~vincent_forename(X200,X201)|forename(X200,X201)))),inference(variable_rename,[status(thm)],[c280])).
% 1.54/1.76  cnf(c282,plain,~vincent_forename(X375,X376)|forename(X375,X376),inference(split_conjunct,[status(thm)],[c281])).
% 1.54/1.76  cnf(c435,plain,~specific(skolem0001,skolem0007),inference(resolution,[status(thm)],[c429, c184])).
% 1.54/1.76  fof(ax3,axiom,(![U]:(![V]:(smoke(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax3)).
% 1.54/1.76  fof(c274,plain,(![U]:(![V]:(~smoke(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax3])).
% 1.54/1.76  fof(c275,plain,(![X196]:(![X197]:(~smoke(X196,X197)|event(X196,X197)))),inference(variable_rename,[status(thm)],[c274])).
% 1.54/1.76  cnf(c276,plain,~smoke(X363,X364)|event(X363,X364),inference(split_conjunct,[status(thm)],[c275])).
% 1.54/1.76  fof(ax4,axiom,(![U]:(![V]:(jules_forename(U,V)=>forename(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax4)).
% 1.54/1.76  fof(c271,plain,(![U]:(![V]:(~jules_forename(U,V)|forename(U,V)))),inference(fof_nnf,[status(thm)],[ax4])).
% 1.54/1.76  fof(c272,plain,(![X194]:(![X195]:(~jules_forename(X194,X195)|forename(X194,X195)))),inference(variable_rename,[status(thm)],[c271])).
% 1.54/1.76  cnf(c273,plain,~jules_forename(X361,X362)|forename(X361,X362),inference(split_conjunct,[status(thm)],[c272])).
% 1.54/1.76  cnf(c412,plain,~specific(skolem0001,skolem0003),inference(resolution,[status(thm)],[c405, c184])).
% 1.54/1.76  cnf(c407,plain,~specific(skolem0001,skolem0005),inference(resolution,[status(thm)],[c404, c184])).
% 1.54/1.76  cnf(c369,plain,~unisex(skolem0001,skolem0004),inference(resolution,[status(thm)],[c360, c180])).
% 1.54/1.76  cnf(c367,plain,~unisex(skolem0001,skolem0008),inference(resolution,[status(thm)],[c359, c180])).
% 1.54/1.76  cnf(c365,plain,~unisex(skolem0001,skolem0002),inference(resolution,[status(thm)],[c358, c180])).
% 1.54/1.76  cnf(c351,plain,~nonhuman(skolem0001,skolem0008),inference(resolution,[status(thm)],[c348, c188])).
% 1.54/1.76  cnf(c350,plain,~nonhuman(skolem0001,skolem0002),inference(resolution,[status(thm)],[c347, c188])).
% 1.54/1.76  cnf(c349,plain,~nonhuman(skolem0001,skolem0004),inference(resolution,[status(thm)],[c346, c188])).
% 1.54/1.76  cnf(c306,plain,~existent(skolem0001,skolem0006),inference(resolution,[status(thm)],[c303, c192])).
% 1.54/1.76  cnf(c295,plain,~existent(skolem0001,skolem0009),inference(resolution,[status(thm)],[c294, c192])).
% 1.54/1.76  cnf(c42,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c41])).
% 1.54/1.76  % SZS output end Saturation
% 1.54/1.76  
% 1.54/1.76  % Initial clauses    : 133
% 1.54/1.76  % Processed clauses  : 1087
% 1.54/1.76  % Factors computed   : 24
% 1.54/1.76  % Resolvents computed: 1352
% 1.54/1.76  % Tautologies deleted: 3
% 1.54/1.76  % Forward subsumed   : 419
% 1.54/1.76  % Backward subsumed  : 2
% 1.54/1.76  % -------- CPU Time ---------
% 1.54/1.76  % User time          : 1.405 s
% 1.54/1.76  % System time        : 0.016 s
% 1.54/1.76  % Total time         : 1.421 s
%------------------------------------------------------------------------------