%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NLP251+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:33:36 PM UTC 2026
% Result : Theorem 2.14s 0.99s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP251+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n026.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 01:58:07 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 2.14/0.99 % Refutation found
% 2.14/0.99 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.14/0.99 % SZS output start CNFRefutation for theBenchmark
% 2.14/0.99 fof(f1,axiom,(
% 2.14/0.99 (! [U,V] :( jules_forename(U,V)=> forename(U,V) ) )),
% 2.14/0.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.14/0.99 fof(f2,axiom,(
% 2.14/0.99 (! [U,V] :( vincent_forename(U,V)=> forename(U,V) ) )),
% 2.14/0.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.14/0.99 fof(f30,axiom,(
% 2.14/0.99 (! [U,V] :( smoke(U,V)=> event(U,V) ) )),
% 2.14/0.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.14/0.99 fof(f49,axiom,(
% 2.14/0.99 (! [U,V,W] :( ( accessible_world(V,W)& man(V,U) )=> man(W,U) ) )),
% 2.14/0.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.14/0.99 fof(f72,conjecture,(
% 2.14/0.99 ~ ( (? [U] :( actual_world(U)& (? [V,W,X,Y,Z,X1,X2] :( of(U,W,V)& man(U,V)& vincent_forename(U,W)& forename(U,W)& proposition(U,Y)& agent(U,X,V)& theme(U,X,Y)& event(U,X)& present(U,X)& think_believe_consider(U,X)& accessible_world(U,Y)& (! [X3] :( man(Y,X3)=> (? [X4] :( event(Y,X4)& agent(Y,X4,X3)& present(Y,X4)& smoke(Y,X4) ) )))& of(U,Z,X1)& man(U,X1)& jules_forename(U,Z)& forename(U,Z)& man(U,X1)& state(U,X2)& be(U,X2,X1,X1) ) )))& ~ (? [X5] :( actual_world(X5)& (? [X6,X7,X8,X9,V,W,X,Y,Z,X1,X2,X10,X11] :( of(X5,X7,X6)& man(X5,X6)& vincent_forename(X5,X7)& forename(X5,X7)& of(X5,X9,X8)& man(X5,X8)& jules_forename(X5,X9)& forename(X5,X9)& of(X5,W,V)& man(X5,V)& vincent_forename(X5,W)& forename(X5,W)& proposition(X5,Y)& agent(X5,X,V)& theme(X5,X,Y)& event(X5,X)& present(X5,X)& think_believe_consider(X5,X)& accessible_world(X5,Y)& (! [X3] :( man(Y,X3)=> (? [X4] :( event(Y,X4)& agent(Y,X4,X3)& present(Y,X4)& smoke(Y,X4) ) )))& of(X5,Z,X1)& man(X5,X1)& jules_forename(X5,Z)& forename(X5,Z)& man(X5,X1)& state(X5,X2)& be(X5,X2,X1,X1)& proposition(X5,X11)& agent(X5,X10,X6)& theme(X5,X10,X11)& event(X5,X10)& present(X5,X10)& think_believe_consider(X5,X10)& accessible_world(X5,X11)& (? [X12] :( event(X11,X12)& agent(X11,X12,X8)& present(X11,X12)& smoke(X11,X12) ) )) )) )) ),
% 2.14/0.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.14/0.99 fof(f73,negated_conjecture,(
% 2.14/0.99 ~(~ ( (? [U] :( actual_world(U)& (? [V,W,X,Y,Z,X1,X2] :( of(U,W,V)& man(U,V)& vincent_forename(U,W)& forename(U,W)& proposition(U,Y)& agent(U,X,V)& theme(U,X,Y)& event(U,X)& present(U,X)& think_believe_consider(U,X)& accessible_world(U,Y)& (! [X3] :( man(Y,X3)=> (? [X4] :( event(Y,X4)& agent(Y,X4,X3)& present(Y,X4)& smoke(Y,X4) ) )))& of(U,Z,X1)& man(U,X1)& jules_forename(U,Z)& forename(U,Z)& man(U,X1)& state(U,X2)& be(U,X2,X1,X1) ) )))& ~ (? [X5] :( actual_world(X5)& (? [X6,X7,X8,X9,V,W,X,Y,Z,X1,X2,X10,X11] :( of(X5,X7,X6)& man(X5,X6)& vincent_forename(X5,X7)& forename(X5,X7)& of(X5,X9,X8)& man(X5,X8)& jules_forename(X5,X9)& forename(X5,X9)& of(X5,W,V)& man(X5,V)& vincent_forename(X5,W)& forename(X5,W)& proposition(X5,Y)& agent(X5,X,V)& theme(X5,X,Y)& event(X5,X)& present(X5,X)& think_believe_consider(X5,X)& accessible_world(X5,Y)& (! [X3] :( man(Y,X3)=> (? [X4] :( event(Y,X4)& agent(Y,X4,X3)& present(Y,X4)& smoke(Y,X4) ) )))& of(X5,Z,X1)& man(X5,X1)& jules_forename(X5,Z)& forename(X5,Z)& man(X5,X1)& state(X5,X2)& be(X5,X2,X1,X1)& proposition(X5,X11)& agent(X5,X10,X6)& theme(X5,X10,X11)& event(X5,X10)& present(X5,X10)& think_believe_consider(X5,X10)& accessible_world(X5,X11)& (? [X12] :( event(X11,X12)& agent(X11,X12,X8)& present(X11,X12)& smoke(X11,X12) ) )) )) )) )),
% 2.14/0.99 inference(negated_conjecture,[status(cth)],[f72])).
% 2.14/0.99 fof(f74,plain,(
% 2.14/0.99 ![U,V]: (~jules_forename(U,V)|forename(U,V))),
% 2.14/0.99 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 2.14/0.99 fof(f75,plain,(
% 2.14/0.99 ![X0,X1]: (~jules_forename(X0,X1)|forename(X0,X1))),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f74])).
% 2.14/0.99 fof(f76,plain,(
% 2.14/0.99 ![U,V]: (~vincent_forename(U,V)|forename(U,V))),
% 2.14/0.99 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 2.14/0.99 fof(f77,plain,(
% 2.14/0.99 ![X0,X1]: (~vincent_forename(X0,X1)|forename(X0,X1))),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f76])).
% 2.14/0.99 fof(f132,plain,(
% 2.14/0.99 ![U,V]: (~smoke(U,V)|event(U,V))),
% 2.14/0.99 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 2.14/0.99 fof(f133,plain,(
% 2.14/0.99 ![X0,X1]: (~smoke(X0,X1)|event(X0,X1))),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f132])).
% 2.14/0.99 fof(f184,plain,(
% 2.14/0.99 ![U,V,W]: ((~accessible_world(V,W)|~man(V,U))|man(W,U))),
% 2.14/0.99 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 2.14/0.99 fof(f185,plain,(
% 2.14/0.99 ![U,W]: ((![V]: (~accessible_world(V,W)|~man(V,U)))|man(W,U))),
% 2.14/0.99 inference(miniscoping,[status(thm)],[f184])).
% 2.14/0.99 fof(f186,plain,(
% 2.14/0.99 ![X0,X1,X2]: (~accessible_world(X0,X1)|~man(X0,X2)|man(X1,X2))),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f185])).
% 2.14/0.99 fof(f252,plain,(
% 2.14/0.99 (?[U]: (actual_world(U)&(?[V,W,X,Y,Z,X1,X2]: ((((((((((((((((((of(U,W,V)&man(U,V))&vincent_forename(U,W))&forename(U,W))&proposition(U,Y))&agent(U,X,V))&theme(U,X,Y))&event(U,X))&present(U,X))&think_believe_consider(U,X))&accessible_world(U,Y))&(![X3]: (~man(Y,X3)|(?[X4]: (((event(Y,X4)&agent(Y,X4,X3))&present(Y,X4))&smoke(Y,X4))))))&of(U,Z,X1))&man(U,X1))&jules_forename(U,Z))&forename(U,Z))&man(U,X1))&state(U,X2))&be(U,X2,X1,X1)))))&(![X5]: (~actual_world(X5)|(![X6,X7,X8,X9,V,W,X,Y,Z,X1,X2,X10,X11]: ((((((((((((((((((((((((((((((((((~of(X5,X7,X6)|~man(X5,X6))|~vincent_forename(X5,X7))|~forename(X5,X7))|~of(X5,X9,X8))|~man(X5,X8))|~jules_forename(X5,X9))|~forename(X5,X9))|~of(X5,W,V))|~man(X5,V))|~vincent_forename(X5,W))|~forename(X5,W))|~proposition(X5,Y))|~agent(X5,X,V))|~theme(X5,X,Y))|~event(X5,X))|~present(X5,X))|~think_believe_consider(X5,X))|~accessible_world(X5,Y))|(?[X3]: (man(Y,X3)&(![X4]: (((~event(Y,X4)|~agent(Y,X4,X3))|~present(Y,X4))|~smoke(Y,X4))))))|~of(X5,Z,X1))|~man(X5,X1))|~jules_forename(X5,Z))|~forename(X5,Z))|~man(X5,X1))|~state(X5,X2))|~be(X5,X2,X1,X1))|~proposition(X5,X11))|~agent(X5,X10,X6))|~theme(X5,X10,X11))|~event(X5,X10))|~present(X5,X10))|~think_believe_consider(X5,X10))|~accessible_world(X5,X11))|(![X12]: (((~event(X11,X12)|~agent(X11,X12,X8))|~present(X11,X12))|~smoke(X11,X12)))))))),
% 2.14/0.99 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 2.14/0.99 fof(f253,plain,(
% 2.14/0.99 (?[U]: (actual_world(U)&(?[X1,X2]: ((((?[Z]: (((((?[Y]: (((?[X]: (((((?[V]: (((?[W]: (((of(U,W,V)&man(U,V))&vincent_forename(U,W))&forename(U,W)))&proposition(U,Y))&agent(U,X,V)))&theme(U,X,Y))&event(U,X))&present(U,X))&think_believe_consider(U,X)))&accessible_world(U,Y))&(![X3]: (~man(Y,X3)|(?[X4]: (((event(Y,X4)&agent(Y,X4,X3))&present(Y,X4))&smoke(Y,X4)))))))&of(U,Z,X1))&man(U,X1))&jules_forename(U,Z))&forename(U,Z)))&man(U,X1))&state(U,X2))&be(U,X2,X1,X1)))))&(![X5]: (~actual_world(X5)|(![X8,X11]: (((![X10]: (((((![X6]: (((![X1,X2]: ((((![Z]: (((((![Y]: (((![X]: (((((![V]: (((![W]: (((((![X9]: (((((![X7]: (((~of(X5,X7,X6)|~man(X5,X6))|~vincent_forename(X5,X7))|~forename(X5,X7)))|~of(X5,X9,X8))|~man(X5,X8))|~jules_forename(X5,X9))|~forename(X5,X9)))|~of(X5,W,V))|~man(X5,V))|~vincent_forename(X5,W))|~forename(X5,W)))|~proposition(X5,Y))|~agent(X5,X,V)))|~theme(X5,X,Y))|~event(X5,X))|~present(X5,X))|~think_believe_consider(X5,X)))|~accessible_world(X5,Y))|(?[X3]: (man(Y,X3)&(![X4]: (((~event(Y,X4)|~agent(Y,X4,X3))|~present(Y,X4))|~smoke(Y,X4)))))))|~of(X5,Z,X1))|~man(X5,X1))|~jules_forename(X5,Z))|~forename(X5,Z)))|~man(X5,X1))|~state(X5,X2))|~be(X5,X2,X1,X1)))|~proposition(X5,X11))|~agent(X5,X10,X6)))|~theme(X5,X10,X11))|~event(X5,X10))|~present(X5,X10))|~think_believe_consider(X5,X10)))|~accessible_world(X5,X11))|(![X12]: (((~event(X11,X12)|~agent(X11,X12,X8))|~present(X11,X12))|~smoke(X11,X12)))))))),
% 2.14/0.99 inference(miniscoping,[status(thm)],[f252])).
% 2.14/0.99 fof(f254,plain,(
% 2.14/0.99 (actual_world(sK0_skl)&((((((((((((((((((of(sK0_skl,sK7_skl,sK6_skl)&man(sK0_skl,sK6_skl))&vincent_forename(sK0_skl,sK7_skl))&forename(sK0_skl,sK7_skl))&proposition(sK0_skl,sK4_skl))&agent(sK0_skl,sK5_skl,sK6_skl))&theme(sK0_skl,sK5_skl,sK4_skl))&event(sK0_skl,sK5_skl))&present(sK0_skl,sK5_skl))&think_believe_consider(sK0_skl,sK5_skl))&accessible_world(sK0_skl,sK4_skl))&(![X3]: (~man(sK4_skl,X3)|(((event(sK4_skl,sK8_skl(X3))&agent(sK4_skl,sK8_skl(X3),X3))&present(sK4_skl,sK8_skl(X3)))&smoke(sK4_skl,sK8_skl(X3))))))&of(sK0_skl,sK3_skl,sK1_skl))&man(sK0_skl,sK1_skl))&jules_forename(sK0_skl,sK3_skl))&forename(sK0_skl,sK3_skl))&man(sK0_skl,sK1_skl))&state(sK0_skl,sK2_skl))&be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)))&(![X5]: (~actual_world(X5)|(![X8,X11]: (((![X10]: (((((![X6]: (((![X1,X2]: ((((![Z]: (((((![Y]: (((![X]: (((((![V]: (((![W]: (((((![X9]: (((((![X7]: (((~of(X5,X7,X6)|~man(X5,X6))|~vincent_forename(X5,X7))|~forename(X5,X7)))|~of(X5,X9,X8))|~man(X5,X8))|~jules_forename(X5,X9))|~forename(X5,X9)))|~of(X5,W,V))|~man(X5,V))|~vincent_forename(X5,W))|~forename(X5,W)))|~proposition(X5,Y))|~agent(X5,X,V)))|~theme(X5,X,Y))|~event(X5,X))|~present(X5,X))|~think_believe_consider(X5,X)))|~accessible_world(X5,Y))|(man(Y,sK9_skl(Y,Z,X2,X1,X6,X10,X11,X8,X5))&(![X4]: (((~event(Y,X4)|~agent(Y,X4,sK9_skl(Y,Z,X2,X1,X6,X10,X11,X8,X5)))|~present(Y,X4))|~smoke(Y,X4))))))|~of(X5,Z,X1))|~man(X5,X1))|~jules_forename(X5,Z))|~forename(X5,Z)))|~man(X5,X1))|~state(X5,X2))|~be(X5,X2,X1,X1)))|~proposition(X5,X11))|~agent(X5,X10,X6)))|~theme(X5,X10,X11))|~event(X5,X10))|~present(X5,X10))|~think_believe_consider(X5,X10)))|~accessible_world(X5,X11))|(![X12]: (((~event(X11,X12)|~agent(X11,X12,X8))|~present(X11,X12))|~smoke(X11,X12)))))))),
% 2.14/0.99 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl]),skolemize(U,sK0_skl),skolemize(X1,sK1_skl),skolemize(X2,sK2_skl),skolemize(Z,sK3_skl),skolemize(Y,sK4_skl),skolemize(X,sK5_skl),skolemize(V,sK6_skl),skolemize(W,sK7_skl),skolemize(X4,sK8_skl(X3)),skolemize(X3,sK9_skl(Y,Z,X2,X1,X6,X10,X11,X8,X5))],[f253])).
% 2.14/0.99 fof(f255,plain,(
% 2.14/0.99 actual_world(sK0_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f256,plain,(
% 2.14/0.99 of(sK0_skl,sK7_skl,sK6_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f257,plain,(
% 2.14/0.99 man(sK0_skl,sK6_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f258,plain,(
% 2.14/0.99 vincent_forename(sK0_skl,sK7_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f260,plain,(
% 2.14/0.99 proposition(sK0_skl,sK4_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f261,plain,(
% 2.14/0.99 agent(sK0_skl,sK5_skl,sK6_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f262,plain,(
% 2.14/0.99 theme(sK0_skl,sK5_skl,sK4_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f263,plain,(
% 2.14/0.99 event(sK0_skl,sK5_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f264,plain,(
% 2.14/0.99 present(sK0_skl,sK5_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f265,plain,(
% 2.14/0.99 think_believe_consider(sK0_skl,sK5_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f266,plain,(
% 2.14/0.99 accessible_world(sK0_skl,sK4_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f267,plain,(
% 2.14/0.99 ![X0]: (~man(sK4_skl,X0)|event(sK4_skl,sK8_skl(X0)))),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f268,plain,(
% 2.14/0.99 ![X0]: (~man(sK4_skl,X0)|agent(sK4_skl,sK8_skl(X0),X0))),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f269,plain,(
% 2.14/0.99 ![X0]: (~man(sK4_skl,X0)|present(sK4_skl,sK8_skl(X0)))),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f270,plain,(
% 2.14/0.99 ![X0]: (~man(sK4_skl,X0)|smoke(sK4_skl,sK8_skl(X0)))),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f271,plain,(
% 2.14/0.99 of(sK0_skl,sK3_skl,sK1_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f272,plain,(
% 2.14/0.99 man(sK0_skl,sK1_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f273,plain,(
% 2.14/0.99 jules_forename(sK0_skl,sK3_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f274,plain,(
% 2.14/0.99 forename(sK0_skl,sK3_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f276,plain,(
% 2.14/0.99 state(sK0_skl,sK2_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f277,plain,(
% 2.14/0.99 be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f278,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~actual_world(X0)|~of(X0,X1,X2)|~man(X0,X2)|~vincent_forename(X0,X1)|~forename(X0,X1)|~of(X0,X3,X4)|~man(X0,X4)|~jules_forename(X0,X3)|~forename(X0,X3)|~of(X0,X5,X6)|~man(X0,X6)|~vincent_forename(X0,X5)|~forename(X0,X5)|~proposition(X0,X7)|~agent(X0,X8,X6)|~theme(X0,X8,X7)|~event(X0,X8)|~present(X0,X8)|~think_believe_consider(X0,X8)|~accessible_world(X0,X7)|man(X7,sK9_skl(X7,X9,X10,X11,X2,X12,X13,X4,X0))|~of(X0,X9,X11)|~man(X0,X11)|~jules_forename(X0,X9)|~forename(X0,X9)|~man(X0,X11)|~state(X0,X10)|~be(X0,X10,X11,X11)|~proposition(X0,X13)|~agent(X0,X12,X2)|~theme(X0,X12,X13)|~event(X0,X12)|~present(X0,X12)|~think_believe_consider(X0,X12)|~accessible_world(X0,X13)|~event(X13,X14)|~agent(X13,X14,X4)|~present(X13,X14)|~smoke(X13,X14))),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f279,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~actual_world(X0)|~of(X0,X1,X2)|~man(X0,X2)|~vincent_forename(X0,X1)|~forename(X0,X1)|~of(X0,X3,X4)|~man(X0,X4)|~jules_forename(X0,X3)|~forename(X0,X3)|~of(X0,X5,X6)|~man(X0,X6)|~vincent_forename(X0,X5)|~forename(X0,X5)|~proposition(X0,X7)|~agent(X0,X8,X6)|~theme(X0,X8,X7)|~event(X0,X8)|~present(X0,X8)|~think_believe_consider(X0,X8)|~accessible_world(X0,X7)|~event(X7,X9)|~agent(X7,X9,sK9_skl(X7,X10,X11,X12,X2,X13,X14,X4,X0))|~present(X7,X9)|~smoke(X7,X9)|~of(X0,X10,X12)|~man(X0,X12)|~jules_forename(X0,X10)|~forename(X0,X10)|~man(X0,X12)|~state(X0,X11)|~be(X0,X11,X12,X12)|~proposition(X0,X14)|~agent(X0,X13,X2)|~theme(X0,X13,X14)|~event(X0,X13)|~present(X0,X13)|~think_believe_consider(X0,X13)|~accessible_world(X0,X14)|~event(X14,X15)|~agent(X14,X15,X4)|~present(X14,X15)|~smoke(X14,X15))),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f254])).
% 2.14/0.99 fof(f280,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~actual_world(X0)|~of(X0,X1,X2)|~man(X0,X2)|~vincent_forename(X0,X1)|~forename(X0,X1)|~of(X0,X3,X4)|~man(X0,X4)|~jules_forename(X0,X3)|~forename(X0,X3)|~of(X0,X5,X6)|~man(X0,X6)|~vincent_forename(X0,X5)|~forename(X0,X5)|~proposition(X0,X7)|~agent(X0,X8,X6)|~theme(X0,X8,X7)|~event(X0,X8)|~present(X0,X8)|~think_believe_consider(X0,X8)|~accessible_world(X0,X7)|man(X7,sK9_skl(X7,X9,X10,X11,X2,X12,X13,X4,X0))|~of(X0,X9,X11)|~man(X0,X11)|~jules_forename(X0,X9)|~forename(X0,X9)|~state(X0,X10)|~be(X0,X10,X11,X11)|~proposition(X0,X13)|~agent(X0,X12,X2)|~theme(X0,X12,X13)|~event(X0,X12)|~present(X0,X12)|~think_believe_consider(X0,X12)|~accessible_world(X0,X13)|~event(X13,X14)|~agent(X13,X14,X4)|~present(X13,X14)|~smoke(X13,X14))),
% 2.14/0.99 inference(duplicate_literals_removal,[status(thm)],[f278])).
% 2.14/0.99 fof(f281,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~actual_world(X0)|~of(X0,X1,X2)|~man(X0,X2)|~vincent_forename(X0,X1)|~forename(X0,X1)|~of(X0,X3,X4)|~man(X0,X4)|~jules_forename(X0,X3)|~forename(X0,X3)|~of(X0,X5,X6)|~man(X0,X6)|~vincent_forename(X0,X5)|~forename(X0,X5)|~proposition(X0,X7)|~agent(X0,X8,X6)|~theme(X0,X8,X7)|~event(X0,X8)|~present(X0,X8)|~think_believe_consider(X0,X8)|~accessible_world(X0,X7)|~event(X7,X9)|~agent(X7,X9,sK9_skl(X7,X10,X11,X12,X2,X13,X14,X4,X0))|~present(X7,X9)|~smoke(X7,X9)|~of(X0,X10,X12)|~man(X0,X12)|~jules_forename(X0,X10)|~forename(X0,X10)|~state(X0,X11)|~be(X0,X11,X12,X12)|~proposition(X0,X14)|~agent(X0,X13,X2)|~theme(X0,X13,X14)|~event(X0,X13)|~present(X0,X13)|~think_believe_consider(X0,X13)|~accessible_world(X0,X14)|~event(X14,X15)|~agent(X14,X15,X4)|~present(X14,X15)|~smoke(X14,X15))),
% 2.14/0.99 inference(duplicate_literals_removal,[status(thm)],[f279])).
% 2.14/0.99 fof(f311,plain,(
% 2.14/0.99 ![X0]: (~man(sK0_skl,X0)|man(sK4_skl,X0))),
% 2.14/0.99 inference(resolution,[status(thm)],[f186,f266])).
% 2.14/0.99 fof(f349,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~actual_world(X0)|~of(X0,X1,X2)|~man(X0,X2)|~vincent_forename(X0,X1)|~of(X0,X3,X4)|~man(X0,X4)|~jules_forename(X0,X3)|~forename(X0,X3)|~of(X0,X5,X6)|~man(X0,X6)|~vincent_forename(X0,X5)|~forename(X0,X5)|~proposition(X0,X7)|~agent(X0,X8,X6)|~theme(X0,X8,X7)|~event(X0,X8)|~present(X0,X8)|~think_believe_consider(X0,X8)|~accessible_world(X0,X7)|man(X7,sK9_skl(X7,X9,X10,X11,X2,X12,X13,X4,X0))|~of(X0,X9,X11)|~man(X0,X11)|~jules_forename(X0,X9)|~forename(X0,X9)|~state(X0,X10)|~be(X0,X10,X11,X11)|~proposition(X0,X13)|~agent(X0,X12,X2)|~theme(X0,X12,X13)|~event(X0,X12)|~present(X0,X12)|~think_believe_consider(X0,X12)|~accessible_world(X0,X13)|~event(X13,X14)|~agent(X13,X14,X4)|~present(X13,X14)|~smoke(X13,X14))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f280,f77])).
% 2.14/0.99 fof(f351,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~actual_world(sK0_skl)|~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~of(sK0_skl,X0,X1)|~man(sK0_skl,X1)|~jules_forename(sK0_skl,X0)|~forename(sK0_skl,X0)|~of(sK0_skl,X2,X3)|~man(sK0_skl,X3)|~vincent_forename(sK0_skl,X2)|~forename(sK0_skl,X2)|~proposition(sK0_skl,X4)|~agent(sK0_skl,X5,X3)|~theme(sK0_skl,X5,X4)|~event(sK0_skl,X5)|~present(sK0_skl,X5)|~think_believe_consider(sK0_skl,X5)|~accessible_world(sK0_skl,X4)|man(X4,sK9_skl(X4,X6,X7,X8,sK6_skl,X9,X10,X1,sK0_skl))|~of(sK0_skl,X6,X8)|~man(sK0_skl,X8)|~jules_forename(sK0_skl,X6)|~forename(sK0_skl,X6)|~state(sK0_skl,X7)|~be(sK0_skl,X7,X8,X8)|~proposition(sK0_skl,X10)|~agent(sK0_skl,X9,sK6_skl)|~theme(sK0_skl,X9,X10)|~event(sK0_skl,X9)|~present(sK0_skl,X9)|~think_believe_consider(sK0_skl,X9)|~accessible_world(sK0_skl,X10)|~event(X10,X11)|~agent(X10,X11,X1)|~present(X10,X11)|~smoke(X10,X11))),
% 2.14/0.99 inference(resolution,[status(thm)],[f349,f256])).
% 2.14/0.99 fof(f353,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~of(sK0_skl,X0,X1)|~man(sK0_skl,X1)|~jules_forename(sK0_skl,X0)|~forename(sK0_skl,X0)|~of(sK0_skl,X2,X3)|~man(sK0_skl,X3)|~vincent_forename(sK0_skl,X2)|~forename(sK0_skl,X2)|~proposition(sK0_skl,X4)|~agent(sK0_skl,X5,X3)|~theme(sK0_skl,X5,X4)|~event(sK0_skl,X5)|~present(sK0_skl,X5)|~think_believe_consider(sK0_skl,X5)|~accessible_world(sK0_skl,X4)|man(X4,sK9_skl(X4,X6,X7,X8,sK6_skl,X9,X10,X1,sK0_skl))|~of(sK0_skl,X6,X8)|~man(sK0_skl,X8)|~jules_forename(sK0_skl,X6)|~forename(sK0_skl,X6)|~state(sK0_skl,X7)|~be(sK0_skl,X7,X8,X8)|~proposition(sK0_skl,X10)|~agent(sK0_skl,X9,sK6_skl)|~theme(sK0_skl,X9,X10)|~event(sK0_skl,X9)|~present(sK0_skl,X9)|~think_believe_consider(sK0_skl,X9)|~accessible_world(sK0_skl,X10)|~event(X10,X11)|~agent(X10,X11,X1)|~present(X10,X11)|~smoke(X10,X11))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f351,f255])).
% 2.14/0.99 fof(f370,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~actual_world(X0)|~of(X0,X1,X2)|~man(X0,X2)|~vincent_forename(X0,X1)|~of(X0,X3,X4)|~man(X0,X4)|~jules_forename(X0,X3)|~forename(X0,X3)|~of(X0,X5,X6)|~man(X0,X6)|~vincent_forename(X0,X5)|~forename(X0,X5)|~proposition(X0,X7)|~agent(X0,X8,X6)|~theme(X0,X8,X7)|~event(X0,X8)|~present(X0,X8)|~think_believe_consider(X0,X8)|~accessible_world(X0,X7)|~event(X7,X9)|~agent(X7,X9,sK9_skl(X7,X10,X11,X12,X2,X13,X14,X4,X0))|~present(X7,X9)|~smoke(X7,X9)|~of(X0,X10,X12)|~man(X0,X12)|~jules_forename(X0,X10)|~forename(X0,X10)|~state(X0,X11)|~be(X0,X11,X12,X12)|~proposition(X0,X14)|~agent(X0,X13,X2)|~theme(X0,X13,X14)|~event(X0,X13)|~present(X0,X13)|~think_believe_consider(X0,X13)|~accessible_world(X0,X14)|~event(X14,X15)|~agent(X14,X15,X4)|~present(X14,X15)|~smoke(X14,X15))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f281,f77])).
% 2.14/0.99 fof(f372,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~actual_world(sK0_skl)|~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~of(sK0_skl,X0,X1)|~man(sK0_skl,X1)|~jules_forename(sK0_skl,X0)|~forename(sK0_skl,X0)|~of(sK0_skl,X2,X3)|~man(sK0_skl,X3)|~vincent_forename(sK0_skl,X2)|~forename(sK0_skl,X2)|~proposition(sK0_skl,X4)|~agent(sK0_skl,X5,X3)|~theme(sK0_skl,X5,X4)|~event(sK0_skl,X5)|~present(sK0_skl,X5)|~think_believe_consider(sK0_skl,X5)|~accessible_world(sK0_skl,X4)|~event(X4,X6)|~agent(X4,X6,sK9_skl(X4,X7,X8,X9,sK6_skl,X10,X11,X1,sK0_skl))|~present(X4,X6)|~smoke(X4,X6)|~of(sK0_skl,X7,X9)|~man(sK0_skl,X9)|~jules_forename(sK0_skl,X7)|~forename(sK0_skl,X7)|~state(sK0_skl,X8)|~be(sK0_skl,X8,X9,X9)|~proposition(sK0_skl,X11)|~agent(sK0_skl,X10,sK6_skl)|~theme(sK0_skl,X10,X11)|~event(sK0_skl,X10)|~present(sK0_skl,X10)|~think_believe_consider(sK0_skl,X10)|~accessible_world(sK0_skl,X11)|~event(X11,X12)|~agent(X11,X12,X1)|~present(X11,X12)|~smoke(X11,X12))),
% 2.14/0.99 inference(resolution,[status(thm)],[f370,f256])).
% 2.14/0.99 fof(f374,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~of(sK0_skl,X0,X1)|~man(sK0_skl,X1)|~jules_forename(sK0_skl,X0)|~forename(sK0_skl,X0)|~of(sK0_skl,X2,X3)|~man(sK0_skl,X3)|~vincent_forename(sK0_skl,X2)|~forename(sK0_skl,X2)|~proposition(sK0_skl,X4)|~agent(sK0_skl,X5,X3)|~theme(sK0_skl,X5,X4)|~event(sK0_skl,X5)|~present(sK0_skl,X5)|~think_believe_consider(sK0_skl,X5)|~accessible_world(sK0_skl,X4)|~event(X4,X6)|~agent(X4,X6,sK9_skl(X4,X7,X8,X9,sK6_skl,X10,X11,X1,sK0_skl))|~present(X4,X6)|~smoke(X4,X6)|~of(sK0_skl,X7,X9)|~man(sK0_skl,X9)|~jules_forename(sK0_skl,X7)|~forename(sK0_skl,X7)|~state(sK0_skl,X8)|~be(sK0_skl,X8,X9,X9)|~proposition(sK0_skl,X11)|~agent(sK0_skl,X10,sK6_skl)|~theme(sK0_skl,X10,X11)|~event(sK0_skl,X10)|~present(sK0_skl,X10)|~think_believe_consider(sK0_skl,X10)|~accessible_world(sK0_skl,X11)|~event(X11,X12)|~agent(X11,X12,X1)|~present(X11,X12)|~smoke(X11,X12))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f372,f255])).
% 2.14/0.99 fof(f421,plain,(
% 2.14/0.99 man(sK4_skl,sK1_skl)),
% 2.14/0.99 inference(resolution,[status(thm)],[f311,f272])).
% 2.14/0.99 fof(f427,plain,(
% 2.14/0.99 smoke(sK4_skl,sK8_skl(sK1_skl))),
% 2.14/0.99 inference(resolution,[status(thm)],[f421,f270])).
% 2.14/0.99 fof(f428,plain,(
% 2.14/0.99 present(sK4_skl,sK8_skl(sK1_skl))),
% 2.14/0.99 inference(resolution,[status(thm)],[f421,f269])).
% 2.14/0.99 fof(f429,plain,(
% 2.14/0.99 agent(sK4_skl,sK8_skl(sK1_skl),sK1_skl)),
% 2.14/0.99 inference(resolution,[status(thm)],[f421,f268])).
% 2.14/0.99 fof(f473,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~vincent_forename(sK0_skl,sK7_skl)|~of(sK0_skl,X0,X1)|~man(sK0_skl,X1)|~jules_forename(sK0_skl,X0)|~forename(sK0_skl,X0)|~of(sK0_skl,X2,X3)|~man(sK0_skl,X3)|~vincent_forename(sK0_skl,X2)|~forename(sK0_skl,X2)|~proposition(sK0_skl,X4)|~agent(sK0_skl,X5,X3)|~theme(sK0_skl,X5,X4)|~event(sK0_skl,X5)|~present(sK0_skl,X5)|~think_believe_consider(sK0_skl,X5)|~accessible_world(sK0_skl,X4)|man(X4,sK9_skl(X4,X6,X7,X8,sK6_skl,X9,X10,X1,sK0_skl))|~of(sK0_skl,X6,X8)|~man(sK0_skl,X8)|~jules_forename(sK0_skl,X6)|~forename(sK0_skl,X6)|~state(sK0_skl,X7)|~be(sK0_skl,X7,X8,X8)|~proposition(sK0_skl,X10)|~agent(sK0_skl,X9,sK6_skl)|~theme(sK0_skl,X9,X10)|~event(sK0_skl,X9)|~present(sK0_skl,X9)|~think_believe_consider(sK0_skl,X9)|~accessible_world(sK0_skl,X10)|~event(X10,X11)|~agent(X10,X11,X1)|~present(X10,X11)|~smoke(X10,X11))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f353,f257])).
% 2.14/0.99 fof(f474,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~vincent_forename(sK0_skl,sK7_skl)|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~forename(sK0_skl,sK3_skl)|~of(sK0_skl,X0,X1)|~man(sK0_skl,X1)|~vincent_forename(sK0_skl,X0)|~forename(sK0_skl,X0)|~proposition(sK0_skl,X2)|~agent(sK0_skl,X3,X1)|~theme(sK0_skl,X3,X2)|~event(sK0_skl,X3)|~present(sK0_skl,X3)|~think_believe_consider(sK0_skl,X3)|~accessible_world(sK0_skl,X2)|man(X2,sK9_skl(X2,X4,X5,X6,sK6_skl,X7,X8,sK1_skl,sK0_skl))|~of(sK0_skl,X4,X6)|~man(sK0_skl,X6)|~jules_forename(sK0_skl,X4)|~forename(sK0_skl,X4)|~state(sK0_skl,X5)|~be(sK0_skl,X5,X6,X6)|~proposition(sK0_skl,X8)|~agent(sK0_skl,X7,sK6_skl)|~theme(sK0_skl,X7,X8)|~event(sK0_skl,X7)|~present(sK0_skl,X7)|~think_believe_consider(sK0_skl,X7)|~accessible_world(sK0_skl,X8)|~event(X8,X9)|~agent(X8,X9,sK1_skl)|~present(X8,X9)|~smoke(X8,X9))),
% 2.14/0.99 inference(resolution,[status(thm)],[f473,f271])).
% 2.14/0.99 fof(f476,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~forename(sK0_skl,sK3_skl)|~of(sK0_skl,X0,X1)|~man(sK0_skl,X1)|~vincent_forename(sK0_skl,X0)|~forename(sK0_skl,X0)|~proposition(sK0_skl,X2)|~agent(sK0_skl,X3,X1)|~theme(sK0_skl,X3,X2)|~event(sK0_skl,X3)|~present(sK0_skl,X3)|~think_believe_consider(sK0_skl,X3)|~accessible_world(sK0_skl,X2)|man(X2,sK9_skl(X2,X4,X5,X6,sK6_skl,X7,X8,sK1_skl,sK0_skl))|~of(sK0_skl,X4,X6)|~man(sK0_skl,X6)|~jules_forename(sK0_skl,X4)|~forename(sK0_skl,X4)|~state(sK0_skl,X5)|~be(sK0_skl,X5,X6,X6)|~proposition(sK0_skl,X8)|~agent(sK0_skl,X7,sK6_skl)|~theme(sK0_skl,X7,X8)|~event(sK0_skl,X7)|~present(sK0_skl,X7)|~think_believe_consider(sK0_skl,X7)|~accessible_world(sK0_skl,X8)|~event(X8,X9)|~agent(X8,X9,sK1_skl)|~present(X8,X9)|~smoke(X8,X9))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f474,f258])).
% 2.14/0.99 fof(f498,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~vincent_forename(sK0_skl,sK7_skl)|~of(sK0_skl,X0,X1)|~man(sK0_skl,X1)|~jules_forename(sK0_skl,X0)|~forename(sK0_skl,X0)|~of(sK0_skl,X2,X3)|~man(sK0_skl,X3)|~vincent_forename(sK0_skl,X2)|~forename(sK0_skl,X2)|~proposition(sK0_skl,X4)|~agent(sK0_skl,X5,X3)|~theme(sK0_skl,X5,X4)|~event(sK0_skl,X5)|~present(sK0_skl,X5)|~think_believe_consider(sK0_skl,X5)|~accessible_world(sK0_skl,X4)|~event(X4,X6)|~agent(X4,X6,sK9_skl(X4,X7,X8,X9,sK6_skl,X10,X11,X1,sK0_skl))|~present(X4,X6)|~smoke(X4,X6)|~of(sK0_skl,X7,X9)|~man(sK0_skl,X9)|~jules_forename(sK0_skl,X7)|~forename(sK0_skl,X7)|~state(sK0_skl,X8)|~be(sK0_skl,X8,X9,X9)|~proposition(sK0_skl,X11)|~agent(sK0_skl,X10,sK6_skl)|~theme(sK0_skl,X10,X11)|~event(sK0_skl,X10)|~present(sK0_skl,X10)|~think_believe_consider(sK0_skl,X10)|~accessible_world(sK0_skl,X11)|~event(X11,X12)|~agent(X11,X12,X1)|~present(X11,X12)|~smoke(X11,X12))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f374,f257])).
% 2.14/0.99 fof(f499,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~vincent_forename(sK0_skl,sK7_skl)|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~forename(sK0_skl,sK3_skl)|~of(sK0_skl,X0,X1)|~man(sK0_skl,X1)|~vincent_forename(sK0_skl,X0)|~forename(sK0_skl,X0)|~proposition(sK0_skl,X2)|~agent(sK0_skl,X3,X1)|~theme(sK0_skl,X3,X2)|~event(sK0_skl,X3)|~present(sK0_skl,X3)|~think_believe_consider(sK0_skl,X3)|~accessible_world(sK0_skl,X2)|~event(X2,X4)|~agent(X2,X4,sK9_skl(X2,X5,X6,X7,sK6_skl,X8,X9,sK1_skl,sK0_skl))|~present(X2,X4)|~smoke(X2,X4)|~of(sK0_skl,X5,X7)|~man(sK0_skl,X7)|~jules_forename(sK0_skl,X5)|~forename(sK0_skl,X5)|~state(sK0_skl,X6)|~be(sK0_skl,X6,X7,X7)|~proposition(sK0_skl,X9)|~agent(sK0_skl,X8,sK6_skl)|~theme(sK0_skl,X8,X9)|~event(sK0_skl,X8)|~present(sK0_skl,X8)|~think_believe_consider(sK0_skl,X8)|~accessible_world(sK0_skl,X9)|~event(X9,X10)|~agent(X9,X10,sK1_skl)|~present(X9,X10)|~smoke(X9,X10))),
% 2.14/0.99 inference(resolution,[status(thm)],[f498,f271])).
% 2.14/0.99 fof(f501,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~forename(sK0_skl,sK3_skl)|~of(sK0_skl,X0,X1)|~man(sK0_skl,X1)|~vincent_forename(sK0_skl,X0)|~forename(sK0_skl,X0)|~proposition(sK0_skl,X2)|~agent(sK0_skl,X3,X1)|~theme(sK0_skl,X3,X2)|~event(sK0_skl,X3)|~present(sK0_skl,X3)|~think_believe_consider(sK0_skl,X3)|~accessible_world(sK0_skl,X2)|~event(X2,X4)|~agent(X2,X4,sK9_skl(X2,X5,X6,X7,sK6_skl,X8,X9,sK1_skl,sK0_skl))|~present(X2,X4)|~smoke(X2,X4)|~of(sK0_skl,X5,X7)|~man(sK0_skl,X7)|~jules_forename(sK0_skl,X5)|~forename(sK0_skl,X5)|~state(sK0_skl,X6)|~be(sK0_skl,X6,X7,X7)|~proposition(sK0_skl,X9)|~agent(sK0_skl,X8,sK6_skl)|~theme(sK0_skl,X8,X9)|~event(sK0_skl,X8)|~present(sK0_skl,X8)|~think_believe_consider(sK0_skl,X8)|~accessible_world(sK0_skl,X9)|~event(X9,X10)|~agent(X9,X10,sK1_skl)|~present(X9,X10)|~smoke(X9,X10))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f499,f258])).
% 2.14/0.99 fof(f661,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~jules_forename(sK0_skl,sK3_skl)|~forename(sK0_skl,sK3_skl)|~of(sK0_skl,X0,X1)|~man(sK0_skl,X1)|~vincent_forename(sK0_skl,X0)|~forename(sK0_skl,X0)|~proposition(sK0_skl,X2)|~agent(sK0_skl,X3,X1)|~theme(sK0_skl,X3,X2)|~event(sK0_skl,X3)|~present(sK0_skl,X3)|~think_believe_consider(sK0_skl,X3)|~accessible_world(sK0_skl,X2)|man(X2,sK9_skl(X2,X4,X5,X6,sK6_skl,X7,X8,sK1_skl,sK0_skl))|~of(sK0_skl,X4,X6)|~man(sK0_skl,X6)|~jules_forename(sK0_skl,X4)|~forename(sK0_skl,X4)|~state(sK0_skl,X5)|~be(sK0_skl,X5,X6,X6)|~proposition(sK0_skl,X8)|~agent(sK0_skl,X7,sK6_skl)|~theme(sK0_skl,X7,X8)|~event(sK0_skl,X7)|~present(sK0_skl,X7)|~think_believe_consider(sK0_skl,X7)|~accessible_world(sK0_skl,X8)|~event(X8,X9)|~agent(X8,X9,sK1_skl)|~present(X8,X9)|~smoke(X8,X9))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f476,f272])).
% 2.14/0.99 fof(f663,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~jules_forename(sK0_skl,sK3_skl)|~forename(sK0_skl,sK3_skl)|~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~forename(sK0_skl,sK7_skl)|~proposition(sK0_skl,X0)|~agent(sK0_skl,X1,sK6_skl)|~theme(sK0_skl,X1,X0)|~event(sK0_skl,X1)|~present(sK0_skl,X1)|~think_believe_consider(sK0_skl,X1)|~accessible_world(sK0_skl,X0)|man(X0,sK9_skl(X0,X2,X3,X4,sK6_skl,X5,X6,sK1_skl,sK0_skl))|~of(sK0_skl,X2,X4)|~man(sK0_skl,X4)|~jules_forename(sK0_skl,X2)|~forename(sK0_skl,X2)|~state(sK0_skl,X3)|~be(sK0_skl,X3,X4,X4)|~proposition(sK0_skl,X6)|~agent(sK0_skl,X5,sK6_skl)|~theme(sK0_skl,X5,X6)|~event(sK0_skl,X5)|~present(sK0_skl,X5)|~think_believe_consider(sK0_skl,X5)|~accessible_world(sK0_skl,X6)|~event(X6,X7)|~agent(X6,X7,sK1_skl)|~present(X6,X7)|~smoke(X6,X7))),
% 2.14/0.99 inference(resolution,[status(thm)],[f661,f256])).
% 2.14/0.99 fof(f666,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~forename(sK0_skl,sK3_skl)|~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~forename(sK0_skl,sK7_skl)|~proposition(sK0_skl,X0)|~agent(sK0_skl,X1,sK6_skl)|~theme(sK0_skl,X1,X0)|~event(sK0_skl,X1)|~present(sK0_skl,X1)|~think_believe_consider(sK0_skl,X1)|~accessible_world(sK0_skl,X0)|man(X0,sK9_skl(X0,X2,X3,X4,sK6_skl,X5,X6,sK1_skl,sK0_skl))|~of(sK0_skl,X2,X4)|~man(sK0_skl,X4)|~jules_forename(sK0_skl,X2)|~forename(sK0_skl,X2)|~state(sK0_skl,X3)|~be(sK0_skl,X3,X4,X4)|~proposition(sK0_skl,X6)|~agent(sK0_skl,X5,sK6_skl)|~theme(sK0_skl,X5,X6)|~event(sK0_skl,X5)|~present(sK0_skl,X5)|~think_believe_consider(sK0_skl,X5)|~accessible_world(sK0_skl,X6)|~event(X6,X7)|~agent(X6,X7,sK1_skl)|~present(X6,X7)|~smoke(X6,X7))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f663,f273])).
% 2.14/0.99 fof(f697,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~jules_forename(sK0_skl,sK3_skl)|~forename(sK0_skl,sK3_skl)|~of(sK0_skl,X0,X1)|~man(sK0_skl,X1)|~vincent_forename(sK0_skl,X0)|~forename(sK0_skl,X0)|~proposition(sK0_skl,X2)|~agent(sK0_skl,X3,X1)|~theme(sK0_skl,X3,X2)|~event(sK0_skl,X3)|~present(sK0_skl,X3)|~think_believe_consider(sK0_skl,X3)|~accessible_world(sK0_skl,X2)|~event(X2,X4)|~agent(X2,X4,sK9_skl(X2,X5,X6,X7,sK6_skl,X8,X9,sK1_skl,sK0_skl))|~present(X2,X4)|~smoke(X2,X4)|~of(sK0_skl,X5,X7)|~man(sK0_skl,X7)|~jules_forename(sK0_skl,X5)|~forename(sK0_skl,X5)|~state(sK0_skl,X6)|~be(sK0_skl,X6,X7,X7)|~proposition(sK0_skl,X9)|~agent(sK0_skl,X8,sK6_skl)|~theme(sK0_skl,X8,X9)|~event(sK0_skl,X8)|~present(sK0_skl,X8)|~think_believe_consider(sK0_skl,X8)|~accessible_world(sK0_skl,X9)|~event(X9,X10)|~agent(X9,X10,sK1_skl)|~present(X9,X10)|~smoke(X9,X10))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f501,f272])).
% 2.14/0.99 fof(f699,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~jules_forename(sK0_skl,sK3_skl)|~forename(sK0_skl,sK3_skl)|~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~forename(sK0_skl,sK7_skl)|~proposition(sK0_skl,X0)|~agent(sK0_skl,X1,sK6_skl)|~theme(sK0_skl,X1,X0)|~event(sK0_skl,X1)|~present(sK0_skl,X1)|~think_believe_consider(sK0_skl,X1)|~accessible_world(sK0_skl,X0)|~event(X0,X2)|~agent(X0,X2,sK9_skl(X0,X3,X4,X5,sK6_skl,X6,X7,sK1_skl,sK0_skl))|~present(X0,X2)|~smoke(X0,X2)|~of(sK0_skl,X3,X5)|~man(sK0_skl,X5)|~jules_forename(sK0_skl,X3)|~forename(sK0_skl,X3)|~state(sK0_skl,X4)|~be(sK0_skl,X4,X5,X5)|~proposition(sK0_skl,X7)|~agent(sK0_skl,X6,sK6_skl)|~theme(sK0_skl,X6,X7)|~event(sK0_skl,X6)|~present(sK0_skl,X6)|~think_believe_consider(sK0_skl,X6)|~accessible_world(sK0_skl,X7)|~event(X7,X8)|~agent(X7,X8,sK1_skl)|~present(X7,X8)|~smoke(X7,X8))),
% 2.14/0.99 inference(resolution,[status(thm)],[f697,f256])).
% 2.14/0.99 fof(f702,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~forename(sK0_skl,sK3_skl)|~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~forename(sK0_skl,sK7_skl)|~proposition(sK0_skl,X0)|~agent(sK0_skl,X1,sK6_skl)|~theme(sK0_skl,X1,X0)|~event(sK0_skl,X1)|~present(sK0_skl,X1)|~think_believe_consider(sK0_skl,X1)|~accessible_world(sK0_skl,X0)|~event(X0,X2)|~agent(X0,X2,sK9_skl(X0,X3,X4,X5,sK6_skl,X6,X7,sK1_skl,sK0_skl))|~present(X0,X2)|~smoke(X0,X2)|~of(sK0_skl,X3,X5)|~man(sK0_skl,X5)|~jules_forename(sK0_skl,X3)|~forename(sK0_skl,X3)|~state(sK0_skl,X4)|~be(sK0_skl,X4,X5,X5)|~proposition(sK0_skl,X7)|~agent(sK0_skl,X6,sK6_skl)|~theme(sK0_skl,X6,X7)|~event(sK0_skl,X6)|~present(sK0_skl,X6)|~think_believe_consider(sK0_skl,X6)|~accessible_world(sK0_skl,X7)|~event(X7,X8)|~agent(X7,X8,sK1_skl)|~present(X7,X8)|~smoke(X7,X8))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f699,f273])).
% 2.14/0.99 fof(f769,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~forename(sK0_skl,sK3_skl)|~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~proposition(sK0_skl,X0)|~agent(sK0_skl,X1,sK6_skl)|~theme(sK0_skl,X1,X0)|~event(sK0_skl,X1)|~present(sK0_skl,X1)|~think_believe_consider(sK0_skl,X1)|~accessible_world(sK0_skl,X0)|man(X0,sK9_skl(X0,X2,X3,X4,sK6_skl,X5,X6,sK1_skl,sK0_skl))|~of(sK0_skl,X2,X4)|~man(sK0_skl,X4)|~jules_forename(sK0_skl,X2)|~forename(sK0_skl,X2)|~state(sK0_skl,X3)|~be(sK0_skl,X3,X4,X4)|~proposition(sK0_skl,X6)|~agent(sK0_skl,X5,sK6_skl)|~theme(sK0_skl,X5,X6)|~event(sK0_skl,X5)|~present(sK0_skl,X5)|~think_believe_consider(sK0_skl,X5)|~accessible_world(sK0_skl,X6)|~event(X6,X7)|~agent(X6,X7,sK1_skl)|~present(X6,X7)|~smoke(X6,X7))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f666,f77])).
% 2.14/0.99 fof(f770,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6]: (~forename(sK0_skl,sK3_skl)|~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~proposition(sK0_skl,X0)|~theme(sK0_skl,sK5_skl,X0)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,X0)|man(X0,sK9_skl(X0,X1,X2,X3,sK6_skl,X4,X5,sK1_skl,sK0_skl))|~of(sK0_skl,X1,X3)|~man(sK0_skl,X3)|~jules_forename(sK0_skl,X1)|~forename(sK0_skl,X1)|~state(sK0_skl,X2)|~be(sK0_skl,X2,X3,X3)|~proposition(sK0_skl,X5)|~agent(sK0_skl,X4,sK6_skl)|~theme(sK0_skl,X4,X5)|~event(sK0_skl,X4)|~present(sK0_skl,X4)|~think_believe_consider(sK0_skl,X4)|~accessible_world(sK0_skl,X5)|~event(X5,X6)|~agent(X5,X6,sK1_skl)|~present(X5,X6)|~smoke(X5,X6))),
% 2.14/0.99 inference(resolution,[status(thm)],[f769,f261])).
% 2.14/0.99 fof(f771,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6]: (~forename(sK0_skl,sK3_skl)|~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~proposition(sK0_skl,X0)|~theme(sK0_skl,sK5_skl,X0)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,X0)|man(X0,sK9_skl(X0,X1,X2,X3,sK6_skl,X4,X5,sK1_skl,sK0_skl))|~of(sK0_skl,X1,X3)|~man(sK0_skl,X3)|~jules_forename(sK0_skl,X1)|~state(sK0_skl,X2)|~be(sK0_skl,X2,X3,X3)|~proposition(sK0_skl,X5)|~agent(sK0_skl,X4,sK6_skl)|~theme(sK0_skl,X4,X5)|~event(sK0_skl,X4)|~present(sK0_skl,X4)|~think_believe_consider(sK0_skl,X4)|~accessible_world(sK0_skl,X5)|~event(X5,X6)|~agent(X5,X6,sK1_skl)|~present(X5,X6)|~smoke(X5,X6))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f770,f75])).
% 2.14/0.99 fof(f791,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6]: (~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~proposition(sK0_skl,X0)|~theme(sK0_skl,sK5_skl,X0)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,X0)|man(X0,sK9_skl(X0,X1,X2,X3,sK6_skl,X4,X5,sK1_skl,sK0_skl))|~of(sK0_skl,X1,X3)|~man(sK0_skl,X3)|~jules_forename(sK0_skl,X1)|~state(sK0_skl,X2)|~be(sK0_skl,X2,X3,X3)|~proposition(sK0_skl,X5)|~agent(sK0_skl,X4,sK6_skl)|~theme(sK0_skl,X4,X5)|~event(sK0_skl,X4)|~present(sK0_skl,X4)|~think_believe_consider(sK0_skl,X4)|~accessible_world(sK0_skl,X5)|~event(X5,X6)|~agent(X5,X6,sK1_skl)|~present(X5,X6)|~smoke(X5,X6))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f771,f274])).
% 2.14/0.99 fof(f792,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5]: (~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~proposition(sK0_skl,sK4_skl)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|man(sK4_skl,sK9_skl(sK4_skl,X0,X1,X2,sK6_skl,X3,X4,sK1_skl,sK0_skl))|~of(sK0_skl,X0,X2)|~man(sK0_skl,X2)|~jules_forename(sK0_skl,X0)|~state(sK0_skl,X1)|~be(sK0_skl,X1,X2,X2)|~proposition(sK0_skl,X4)|~agent(sK0_skl,X3,sK6_skl)|~theme(sK0_skl,X3,X4)|~event(sK0_skl,X3)|~present(sK0_skl,X3)|~think_believe_consider(sK0_skl,X3)|~accessible_world(sK0_skl,X4)|~event(X4,X5)|~agent(X4,X5,sK1_skl)|~present(X4,X5)|~smoke(X4,X5))),
% 2.14/0.99 inference(resolution,[status(thm)],[f791,f262])).
% 2.14/0.99 fof(f793,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5]: (~vincent_forename(sK0_skl,sK7_skl)|~proposition(sK0_skl,sK4_skl)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|man(sK4_skl,sK9_skl(sK4_skl,X0,X1,X2,sK6_skl,X3,X4,sK1_skl,sK0_skl))|~of(sK0_skl,X0,X2)|~man(sK0_skl,X2)|~jules_forename(sK0_skl,X0)|~state(sK0_skl,X1)|~be(sK0_skl,X1,X2,X2)|~proposition(sK0_skl,X4)|~agent(sK0_skl,X3,sK6_skl)|~theme(sK0_skl,X3,X4)|~event(sK0_skl,X3)|~present(sK0_skl,X3)|~think_believe_consider(sK0_skl,X3)|~accessible_world(sK0_skl,X4)|~event(X4,X5)|~agent(X4,X5,sK1_skl)|~present(X4,X5)|~smoke(X4,X5))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f792,f257])).
% 2.14/0.99 fof(f794,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5]: (~proposition(sK0_skl,sK4_skl)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|man(sK4_skl,sK9_skl(sK4_skl,X0,X1,X2,sK6_skl,X3,X4,sK1_skl,sK0_skl))|~of(sK0_skl,X0,X2)|~man(sK0_skl,X2)|~jules_forename(sK0_skl,X0)|~state(sK0_skl,X1)|~be(sK0_skl,X1,X2,X2)|~proposition(sK0_skl,X4)|~agent(sK0_skl,X3,sK6_skl)|~theme(sK0_skl,X3,X4)|~event(sK0_skl,X3)|~present(sK0_skl,X3)|~think_believe_consider(sK0_skl,X3)|~accessible_world(sK0_skl,X4)|~event(X4,X5)|~agent(X4,X5,sK1_skl)|~present(X4,X5)|~smoke(X4,X5))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f793,f258])).
% 2.14/0.99 fof(f795,plain,(
% 2.14/0.99 ![X0,X1,X2,X3]: (~proposition(sK0_skl,sK4_skl)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,X0,sK1_skl,sK6_skl,X1,X2,sK1_skl,sK0_skl))|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,X0)|~be(sK0_skl,X0,sK1_skl,sK1_skl)|~proposition(sK0_skl,X2)|~agent(sK0_skl,X1,sK6_skl)|~theme(sK0_skl,X1,X2)|~event(sK0_skl,X1)|~present(sK0_skl,X1)|~think_believe_consider(sK0_skl,X1)|~accessible_world(sK0_skl,X2)|~event(X2,X3)|~agent(X2,X3,sK1_skl)|~present(X2,X3)|~smoke(X2,X3))),
% 2.14/0.99 inference(resolution,[status(thm)],[f794,f271])).
% 2.14/0.99 fof(f797,plain,(
% 2.14/0.99 ![X0,X1,X2,X3]: (~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,X0,sK1_skl,sK6_skl,X1,X2,sK1_skl,sK0_skl))|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,X0)|~be(sK0_skl,X0,sK1_skl,sK1_skl)|~proposition(sK0_skl,X2)|~agent(sK0_skl,X1,sK6_skl)|~theme(sK0_skl,X1,X2)|~event(sK0_skl,X1)|~present(sK0_skl,X1)|~think_believe_consider(sK0_skl,X1)|~accessible_world(sK0_skl,X2)|~event(X2,X3)|~agent(X2,X3,sK1_skl)|~present(X2,X3)|~smoke(X2,X3))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f795,f260])).
% 2.14/0.99 fof(f800,plain,(
% 2.14/0.99 ![X0,X1,X2,X3]: (~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,X0,sK1_skl,sK6_skl,X1,X2,sK1_skl,sK0_skl))|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,X0)|~be(sK0_skl,X0,sK1_skl,sK1_skl)|~proposition(sK0_skl,X2)|~agent(sK0_skl,X1,sK6_skl)|~theme(sK0_skl,X1,X2)|~event(sK0_skl,X1)|~present(sK0_skl,X1)|~think_believe_consider(sK0_skl,X1)|~accessible_world(sK0_skl,X2)|~agent(X2,X3,sK1_skl)|~present(X2,X3)|~smoke(X2,X3))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f797,f133])).
% 2.14/0.99 fof(f801,plain,(
% 2.14/0.99 ![X0,X1,X2]: (~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,X0,X1,sK1_skl,sK0_skl))|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~proposition(sK0_skl,X1)|~agent(sK0_skl,X0,sK6_skl)|~theme(sK0_skl,X0,X1)|~event(sK0_skl,X0)|~present(sK0_skl,X0)|~think_believe_consider(sK0_skl,X0)|~accessible_world(sK0_skl,X1)|~agent(X1,X2,sK1_skl)|~present(X1,X2)|~smoke(X1,X2))),
% 2.14/0.99 inference(resolution,[status(thm)],[f800,f277])).
% 2.14/0.99 fof(f802,plain,(
% 2.14/0.99 ![X0,X1,X2]: (~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,X0,X1,sK1_skl,sK0_skl))|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~proposition(sK0_skl,X1)|~agent(sK0_skl,X0,sK6_skl)|~theme(sK0_skl,X0,X1)|~event(sK0_skl,X0)|~present(sK0_skl,X0)|~think_believe_consider(sK0_skl,X0)|~accessible_world(sK0_skl,X1)|~agent(X1,X2,sK1_skl)|~present(X1,X2)|~smoke(X1,X2))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f801,f263])).
% 2.14/0.99 fof(f803,plain,(
% 2.14/0.99 ![X0,X1,X2]: (~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,X0,X1,sK1_skl,sK0_skl))|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~proposition(sK0_skl,X1)|~agent(sK0_skl,X0,sK6_skl)|~theme(sK0_skl,X0,X1)|~event(sK0_skl,X0)|~present(sK0_skl,X0)|~think_believe_consider(sK0_skl,X0)|~accessible_world(sK0_skl,X1)|~agent(X1,X2,sK1_skl)|~present(X1,X2)|~smoke(X1,X2))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f802,f264])).
% 2.14/0.99 fof(f804,plain,(
% 2.14/0.99 ![X0,X1]: (~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,X0,sK1_skl,sK0_skl))|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~proposition(sK0_skl,X0)|~theme(sK0_skl,sK5_skl,X0)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,X0)|~agent(X0,X1,sK1_skl)|~present(X0,X1)|~smoke(X0,X1))),
% 2.14/0.99 inference(resolution,[status(thm)],[f803,f261])).
% 2.14/0.99 fof(f805,plain,(
% 2.14/0.99 ![X0,X1]: (~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,X0,sK1_skl,sK0_skl))|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~proposition(sK0_skl,X0)|~theme(sK0_skl,sK5_skl,X0)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,X0)|~agent(X0,X1,sK1_skl)|~present(X0,X1)|~smoke(X0,X1))),
% 2.14/0.99 inference(duplicate_literals_removal,[status(thm)],[f804])).
% 2.14/0.99 fof(f806,plain,(
% 2.14/0.99 ![X0,X1]: (~accessible_world(sK0_skl,sK4_skl)|man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,X0,sK1_skl,sK0_skl))|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~proposition(sK0_skl,X0)|~theme(sK0_skl,sK5_skl,X0)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,X0)|~agent(X0,X1,sK1_skl)|~present(X0,X1)|~smoke(X0,X1))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f805,f265])).
% 2.14/0.99 fof(f807,plain,(
% 2.14/0.99 ![X0,X1]: (man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,X0,sK1_skl,sK0_skl))|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~proposition(sK0_skl,X0)|~theme(sK0_skl,sK5_skl,X0)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,X0)|~agent(X0,X1,sK1_skl)|~present(X0,X1)|~smoke(X0,X1))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f806,f266])).
% 2.14/0.99 fof(f808,plain,(
% 2.14/0.99 man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl))|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~proposition(sK0_skl,sK4_skl)|~theme(sK0_skl,sK5_skl,sK4_skl)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~present(sK4_skl,sK8_skl(sK1_skl))|~smoke(sK4_skl,sK8_skl(sK1_skl))),
% 2.14/0.99 inference(resolution,[status(thm)],[f807,f429])).
% 2.14/0.99 fof(f809,plain,(
% 2.14/0.99 man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl))|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~proposition(sK0_skl,sK4_skl)|~theme(sK0_skl,sK5_skl,sK4_skl)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~present(sK4_skl,sK8_skl(sK1_skl))|~smoke(sK4_skl,sK8_skl(sK1_skl))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f808,f272])).
% 2.14/0.99 fof(f810,plain,(
% 2.14/0.99 man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl))|~state(sK0_skl,sK2_skl)|~proposition(sK0_skl,sK4_skl)|~theme(sK0_skl,sK5_skl,sK4_skl)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~present(sK4_skl,sK8_skl(sK1_skl))|~smoke(sK4_skl,sK8_skl(sK1_skl))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f809,f273])).
% 2.14/0.99 fof(f811,plain,(
% 2.14/0.99 man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl))|~state(sK0_skl,sK2_skl)|~proposition(sK0_skl,sK4_skl)|~theme(sK0_skl,sK5_skl,sK4_skl)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~smoke(sK4_skl,sK8_skl(sK1_skl))),
% 2.14/0.99 inference(resolution,[status(thm)],[f810,f428])).
% 2.14/0.99 fof(f812,plain,(
% 2.14/0.99 man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl))|~proposition(sK0_skl,sK4_skl)|~theme(sK0_skl,sK5_skl,sK4_skl)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~smoke(sK4_skl,sK8_skl(sK1_skl))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f811,f276])).
% 2.14/0.99 fof(f817,plain,(
% 2.14/0.99 man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl))|~theme(sK0_skl,sK5_skl,sK4_skl)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~smoke(sK4_skl,sK8_skl(sK1_skl))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f812,f260])).
% 2.14/0.99 fof(f818,plain,(
% 2.14/0.99 man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl))|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~smoke(sK4_skl,sK8_skl(sK1_skl))),
% 2.14/0.99 inference(resolution,[status(thm)],[f817,f262])).
% 2.14/0.99 fof(f819,plain,(
% 2.14/0.99 man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl))|~present(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~smoke(sK4_skl,sK8_skl(sK1_skl))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f818,f263])).
% 2.14/0.99 fof(f820,plain,(
% 2.14/0.99 man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl))|~accessible_world(sK0_skl,sK4_skl)|~smoke(sK4_skl,sK8_skl(sK1_skl))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f819,f264])).
% 2.14/0.99 fof(f821,plain,(
% 2.14/0.99 man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl))|~accessible_world(sK0_skl,sK4_skl)),
% 2.14/0.99 inference(resolution,[status(thm)],[f820,f427])).
% 2.14/0.99 fof(f822,plain,(
% 2.14/0.99 man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f821,f266])).
% 2.14/0.99 fof(f823,plain,(
% 2.14/0.99 smoke(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))),
% 2.14/0.99 inference(resolution,[status(thm)],[f822,f270])).
% 2.14/0.99 fof(f824,plain,(
% 2.14/0.99 present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))),
% 2.14/0.99 inference(resolution,[status(thm)],[f822,f269])).
% 2.14/0.99 fof(f825,plain,(
% 2.14/0.99 agent(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)),sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl))),
% 2.14/0.99 inference(resolution,[status(thm)],[f822,f268])).
% 2.14/0.99 fof(f826,plain,(
% 2.14/0.99 event(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))),
% 2.14/0.99 inference(resolution,[status(thm)],[f822,f267])).
% 2.14/0.99 fof(f835,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~forename(sK0_skl,sK3_skl)|~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~proposition(sK0_skl,X0)|~agent(sK0_skl,X1,sK6_skl)|~theme(sK0_skl,X1,X0)|~event(sK0_skl,X1)|~present(sK0_skl,X1)|~think_believe_consider(sK0_skl,X1)|~accessible_world(sK0_skl,X0)|~event(X0,X2)|~agent(X0,X2,sK9_skl(X0,X3,X4,X5,sK6_skl,X6,X7,sK1_skl,sK0_skl))|~present(X0,X2)|~smoke(X0,X2)|~of(sK0_skl,X3,X5)|~man(sK0_skl,X5)|~jules_forename(sK0_skl,X3)|~forename(sK0_skl,X3)|~state(sK0_skl,X4)|~be(sK0_skl,X4,X5,X5)|~proposition(sK0_skl,X7)|~agent(sK0_skl,X6,sK6_skl)|~theme(sK0_skl,X6,X7)|~event(sK0_skl,X6)|~present(sK0_skl,X6)|~think_believe_consider(sK0_skl,X6)|~accessible_world(sK0_skl,X7)|~event(X7,X8)|~agent(X7,X8,sK1_skl)|~present(X7,X8)|~smoke(X7,X8))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f702,f77])).
% 2.14/0.99 fof(f836,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~forename(sK0_skl,sK3_skl)|~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~proposition(sK0_skl,X0)|~theme(sK0_skl,sK5_skl,X0)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,X0)|~event(X0,X1)|~agent(X0,X1,sK9_skl(X0,X2,X3,X4,sK6_skl,X5,X6,sK1_skl,sK0_skl))|~present(X0,X1)|~smoke(X0,X1)|~of(sK0_skl,X2,X4)|~man(sK0_skl,X4)|~jules_forename(sK0_skl,X2)|~forename(sK0_skl,X2)|~state(sK0_skl,X3)|~be(sK0_skl,X3,X4,X4)|~proposition(sK0_skl,X6)|~agent(sK0_skl,X5,sK6_skl)|~theme(sK0_skl,X5,X6)|~event(sK0_skl,X5)|~present(sK0_skl,X5)|~think_believe_consider(sK0_skl,X5)|~accessible_world(sK0_skl,X6)|~event(X6,X7)|~agent(X6,X7,sK1_skl)|~present(X6,X7)|~smoke(X6,X7))),
% 2.14/0.99 inference(resolution,[status(thm)],[f835,f261])).
% 2.14/0.99 fof(f837,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~forename(sK0_skl,sK3_skl)|~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~proposition(sK0_skl,X0)|~theme(sK0_skl,sK5_skl,X0)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,X0)|~event(X0,X1)|~agent(X0,X1,sK9_skl(X0,X2,X3,X4,sK6_skl,X5,X6,sK1_skl,sK0_skl))|~present(X0,X1)|~smoke(X0,X1)|~of(sK0_skl,X2,X4)|~man(sK0_skl,X4)|~jules_forename(sK0_skl,X2)|~state(sK0_skl,X3)|~be(sK0_skl,X3,X4,X4)|~proposition(sK0_skl,X6)|~agent(sK0_skl,X5,sK6_skl)|~theme(sK0_skl,X5,X6)|~event(sK0_skl,X5)|~present(sK0_skl,X5)|~think_believe_consider(sK0_skl,X5)|~accessible_world(sK0_skl,X6)|~event(X6,X7)|~agent(X6,X7,sK1_skl)|~present(X6,X7)|~smoke(X6,X7))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f836,f75])).
% 2.14/0.99 fof(f905,plain,(
% 2.14/0.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~proposition(sK0_skl,X0)|~theme(sK0_skl,sK5_skl,X0)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,X0)|~event(X0,X1)|~agent(X0,X1,sK9_skl(X0,X2,X3,X4,sK6_skl,X5,X6,sK1_skl,sK0_skl))|~present(X0,X1)|~smoke(X0,X1)|~of(sK0_skl,X2,X4)|~man(sK0_skl,X4)|~jules_forename(sK0_skl,X2)|~state(sK0_skl,X3)|~be(sK0_skl,X3,X4,X4)|~proposition(sK0_skl,X6)|~agent(sK0_skl,X5,sK6_skl)|~theme(sK0_skl,X5,X6)|~event(sK0_skl,X5)|~present(sK0_skl,X5)|~think_believe_consider(sK0_skl,X5)|~accessible_world(sK0_skl,X6)|~event(X6,X7)|~agent(X6,X7,sK1_skl)|~present(X6,X7)|~smoke(X6,X7))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f837,f274])).
% 2.14/0.99 fof(f906,plain,(
% 2.14/0.99 ![X0]: (~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~proposition(sK0_skl,sK4_skl)|~theme(sK0_skl,sK5_skl,sK4_skl)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~event(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~smoke(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~of(sK0_skl,sK3_skl,sK1_skl)|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)|~proposition(sK0_skl,sK4_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~theme(sK0_skl,sK5_skl,sK4_skl)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~event(sK4_skl,X0)|~agent(sK4_skl,X0,sK1_skl)|~present(sK4_skl,X0)|~smoke(sK4_skl,X0))),
% 2.14/0.99 inference(resolution,[status(thm)],[f905,f825])).
% 2.14/0.99 fof(f907,plain,(
% 2.14/0.99 ![X0]: (~man(sK0_skl,sK6_skl)|~vincent_forename(sK0_skl,sK7_skl)|~proposition(sK0_skl,sK4_skl)|~theme(sK0_skl,sK5_skl,sK4_skl)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~event(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~smoke(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~of(sK0_skl,sK3_skl,sK1_skl)|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~event(sK4_skl,X0)|~agent(sK4_skl,X0,sK1_skl)|~present(sK4_skl,X0)|~smoke(sK4_skl,X0))),
% 2.14/0.99 inference(duplicate_literals_removal,[status(thm)],[f906])).
% 2.14/0.99 fof(f908,plain,(
% 2.14/0.99 ![X0]: (~vincent_forename(sK0_skl,sK7_skl)|~proposition(sK0_skl,sK4_skl)|~theme(sK0_skl,sK5_skl,sK4_skl)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~event(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~smoke(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~of(sK0_skl,sK3_skl,sK1_skl)|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~event(sK4_skl,X0)|~agent(sK4_skl,X0,sK1_skl)|~present(sK4_skl,X0)|~smoke(sK4_skl,X0))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f907,f257])).
% 2.14/0.99 fof(f1094,plain,(
% 2.14/0.99 ![X0]: (~proposition(sK0_skl,sK4_skl)|~theme(sK0_skl,sK5_skl,sK4_skl)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~event(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~smoke(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~of(sK0_skl,sK3_skl,sK1_skl)|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~event(sK4_skl,X0)|~agent(sK4_skl,X0,sK1_skl)|~present(sK4_skl,X0)|~smoke(sK4_skl,X0))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f908,f258])).
% 2.14/0.99 fof(f1095,plain,(
% 2.14/0.99 ![X0]: (~proposition(sK0_skl,sK4_skl)|~theme(sK0_skl,sK5_skl,sK4_skl)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~event(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~smoke(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~of(sK0_skl,sK3_skl,sK1_skl)|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~event(sK4_skl,X0)|~agent(sK4_skl,X0,sK1_skl)|~present(sK4_skl,X0)|~smoke(sK4_skl,X0))),
% 2.14/0.99 inference(resolution,[status(thm)],[f1094,f824])).
% 2.14/0.99 fof(f1096,plain,(
% 2.14/0.99 ![X0]: (~theme(sK0_skl,sK5_skl,sK4_skl)|~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~event(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~smoke(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~of(sK0_skl,sK3_skl,sK1_skl)|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~event(sK4_skl,X0)|~agent(sK4_skl,X0,sK1_skl)|~present(sK4_skl,X0)|~smoke(sK4_skl,X0))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f1095,f260])).
% 2.14/0.99 fof(f1097,plain,(
% 2.14/0.99 ![X0]: (~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~event(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~smoke(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~of(sK0_skl,sK3_skl,sK1_skl)|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~event(sK4_skl,X0)|~agent(sK4_skl,X0,sK1_skl)|~present(sK4_skl,X0)|~smoke(sK4_skl,X0))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f1096,f262])).
% 2.14/0.99 fof(f1098,plain,(
% 2.14/0.99 ![X0]: (~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~event(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~of(sK0_skl,sK3_skl,sK1_skl)|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~event(sK4_skl,X0)|~agent(sK4_skl,X0,sK1_skl)|~present(sK4_skl,X0)|~smoke(sK4_skl,X0))),
% 2.14/0.99 inference(resolution,[status(thm)],[f1097,f823])).
% 2.14/0.99 fof(f1099,plain,(
% 2.14/0.99 ![X0]: (~event(sK0_skl,sK5_skl)|~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~event(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~of(sK0_skl,sK3_skl,sK1_skl)|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~agent(sK4_skl,X0,sK1_skl)|~present(sK4_skl,X0)|~smoke(sK4_skl,X0))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f1098,f133])).
% 2.14/0.99 fof(f1100,plain,(
% 2.14/0.99 ![X0]: (~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~event(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))|~of(sK0_skl,sK3_skl,sK1_skl)|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~agent(sK4_skl,X0,sK1_skl)|~present(sK4_skl,X0)|~smoke(sK4_skl,X0))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f1099,f263])).
% 2.14/0.99 fof(f1101,plain,(
% 2.14/0.99 ![X0]: (~present(sK0_skl,sK5_skl)|~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~of(sK0_skl,sK3_skl,sK1_skl)|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~agent(sK4_skl,X0,sK1_skl)|~present(sK4_skl,X0)|~smoke(sK4_skl,X0))),
% 2.14/0.99 inference(resolution,[status(thm)],[f1100,f826])).
% 2.14/0.99 fof(f1102,plain,(
% 2.14/0.99 ![X0]: (~think_believe_consider(sK0_skl,sK5_skl)|~accessible_world(sK0_skl,sK4_skl)|~of(sK0_skl,sK3_skl,sK1_skl)|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~agent(sK4_skl,X0,sK1_skl)|~present(sK4_skl,X0)|~smoke(sK4_skl,X0))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f1101,f264])).
% 2.14/0.99 fof(f1103,plain,(
% 2.14/0.99 ![X0]: (~accessible_world(sK0_skl,sK4_skl)|~of(sK0_skl,sK3_skl,sK1_skl)|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~agent(sK4_skl,X0,sK1_skl)|~present(sK4_skl,X0)|~smoke(sK4_skl,X0))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f1102,f265])).
% 2.14/0.99 fof(f1104,plain,(
% 2.14/0.99 ![X0]: (~accessible_world(sK0_skl,sK4_skl)|~of(sK0_skl,sK3_skl,sK1_skl)|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~agent(sK4_skl,X0,sK1_skl)|~present(sK4_skl,X0)|~smoke(sK4_skl,X0))),
% 2.14/0.99 inference(resolution,[status(thm)],[f1103,f277])).
% 2.14/0.99 fof(f1105,plain,(
% 2.14/0.99 ![X0]: (~of(sK0_skl,sK3_skl,sK1_skl)|~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~agent(sK4_skl,X0,sK1_skl)|~present(sK4_skl,X0)|~smoke(sK4_skl,X0))),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f1104,f266])).
% 2.14/0.99 fof(f1106,plain,(
% 2.14/0.99 ![X0]: (~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~agent(sK4_skl,X0,sK1_skl)|~present(sK4_skl,X0)|~smoke(sK4_skl,X0))),
% 2.14/1.02 inference(forward_subsumption_resolution,[status(thm)],[f1105,f271])).
% 2.14/1.02 fof(f1107,plain,(
% 2.14/1.02 ~man(sK0_skl,sK1_skl)|~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~present(sK4_skl,sK8_skl(sK1_skl))|~smoke(sK4_skl,sK8_skl(sK1_skl))),
% 2.14/1.02 inference(resolution,[status(thm)],[f1106,f429])).
% 2.14/1.02 fof(f1108,plain,(
% 2.14/1.02 ~jules_forename(sK0_skl,sK3_skl)|~state(sK0_skl,sK2_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~present(sK4_skl,sK8_skl(sK1_skl))|~smoke(sK4_skl,sK8_skl(sK1_skl))),
% 2.14/1.02 inference(forward_subsumption_resolution,[status(thm)],[f1107,f272])).
% 2.14/1.02 fof(f1109,plain,(
% 2.14/1.02 ~state(sK0_skl,sK2_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~present(sK4_skl,sK8_skl(sK1_skl))|~smoke(sK4_skl,sK8_skl(sK1_skl))),
% 2.14/1.02 inference(forward_subsumption_resolution,[status(thm)],[f1108,f273])).
% 2.14/1.02 fof(f1110,plain,(
% 2.14/1.02 ~state(sK0_skl,sK2_skl)|~agent(sK0_skl,sK5_skl,sK6_skl)|~smoke(sK4_skl,sK8_skl(sK1_skl))),
% 2.14/1.02 inference(resolution,[status(thm)],[f1109,f428])).
% 2.14/1.02 fof(f1111,plain,(
% 2.14/1.02 ~agent(sK0_skl,sK5_skl,sK6_skl)|~smoke(sK4_skl,sK8_skl(sK1_skl))),
% 2.14/1.02 inference(forward_subsumption_resolution,[status(thm)],[f1110,f276])).
% 2.14/1.02 fof(f1113,plain,(
% 2.14/1.02 ~smoke(sK4_skl,sK8_skl(sK1_skl))),
% 2.14/1.02 inference(forward_subsumption_resolution,[status(thm)],[f1111,f261])).
% 2.14/1.02 fof(f1114,plain,(
% 2.14/1.02 $false),
% 2.14/1.02 inference(backward_subsumption_resolution,[status(thm)],[f427,f1113])).
% 2.14/1.02 % SZS output end CNFRefutation for theBenchmark.p
% 2.14/1.03 % Elapsed time: 0.645863 seconds
% 2.14/1.03 % CPU time: 4.678678 seconds
% 2.14/1.03 % Total memory used: 83.581 MB
% 2.14/1.03 % Net memory used: 79.305 MB
%------------------------------------------------------------------------------