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