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