%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NLP252-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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 : Unsatisfiable 0.13s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP252-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n007.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 01:53:05 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.42 % Refutation found
% 0.13/0.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.42 fof(f1,axiom,(
% 0.13/0.42 (![U,V]: (( ~ smoke(U,V)| event(U,V) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f29,axiom,(
% 0.13/0.42 (![U,V]: (( ~ vincent_forename(U,V)| forename(U,V) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f30,axiom,(
% 0.13/0.42 (![U,V]: (( ~ jules_forename(U,V)| forename(U,V) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f52,axiom,(
% 0.13/0.42 (![U,V,W]: (( ~ accessible_world(U,V)| ~ man(U,W)| man(V,W) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f72,negated_conjecture,(
% 0.13/0.42 actual_world(skc8) ),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f73,negated_conjecture,(
% 0.13/0.42 man(skc8,skc15) ),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f75,negated_conjecture,(
% 0.13/0.42 vincent_forename(skc8,skc14) ),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f76,negated_conjecture,(
% 0.13/0.42 event(skc8,skc13) ),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f77,negated_conjecture,(
% 0.13/0.42 present(skc8,skc13) ),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f78,negated_conjecture,(
% 0.13/0.42 think_believe_consider(skc8,skc13) ),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f79,negated_conjecture,(
% 0.13/0.42 jules_forename(skc8,skc11) ),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f81,negated_conjecture,(
% 0.13/0.42 man(skc8,skc10) ),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f82,negated_conjecture,(
% 0.13/0.42 state(skc8,skc9) ),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f83,negated_conjecture,(
% 0.13/0.42 accessible_world(skc8,skc12) ),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f84,negated_conjecture,(
% 0.13/0.42 proposition(skc8,skc12) ),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f85,negated_conjecture,(
% 0.13/0.42 of(skc8,skc14,skc15) ),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f86,negated_conjecture,(
% 0.13/0.42 agent(skc8,skc13,skc15) ),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f87,negated_conjecture,(
% 0.13/0.42 theme(skc8,skc13,skc12) ),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f88,negated_conjecture,(
% 0.13/0.42 of(skc8,skc11,skc10) ),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f89,negated_conjecture,(
% 0.13/0.42 be(skc8,skc9,skc10,skc10) ),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f90,negated_conjecture,(
% 0.13/0.42 (![U,V]: (( ~ man(skc12,U)| smoke(skc12,skf2(V)) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f91,negated_conjecture,(
% 0.13/0.42 (![U,V]: (( ~ man(skc12,U)| present(skc12,skf2(V)) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f93,negated_conjecture,(
% 0.13/0.42 (![U]: (( ~ man(skc12,U)| agent(skc12,skf2(U),U) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f94,negated_conjecture,(
% 0.13/0.43 (![U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7]: (( ~ accessible_world(U,V)| ~ proposition(U,V)| ~ theme(U,W,V)| ~ event(U,W)| ~ present(U,W)| ~ think_believe_consider(U,W)| ~ forename(U,X)| ~ vincent_forename(U,X)| ~ of(U,X,Y)| ~ man(U,Y)| ~ agent(U,W,Y)| ~ state(U,Z)| ~ smoke(X1,X2)| ~ present(X1,X2)| ~ agent(X1,X2,X3)| ~ event(X1,X2)| ~ be(U,Z,X3,X3)| ~ man(U,X3)| ~ of(U,X4,X3)| ~ jules_forename(U,X4)| ~ forename(U,X4)| ~ proposition(U,X1)| ~ accessible_world(U,X1)| ~ think_believe_consider(U,X5)| ~ present(U,X5)| ~ event(U,X5)| ~ theme(U,X5,X1)| ~ vincent_forename(U,X6)| ~ forename(U,X6)| ~ agent(U,X5,X7)| ~ man(U,X7)| ~ of(U,X6,X7)| ~ actual_world(U)| man(V,skf4(V)) ) ))),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f95,negated_conjecture,(
% 0.13/0.43 (![U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8]: (( ~ smoke(U,V)| ~ present(U,V)| ~ agent(U,V,skf4(U))| ~ event(U,V)| ~ accessible_world(W,U)| ~ proposition(W,U)| ~ theme(W,X,U)| ~ event(W,X)| ~ present(W,X)| ~ think_believe_consider(W,X)| ~ forename(W,Y)| ~ vincent_forename(W,Y)| ~ of(W,Y,Z)| ~ man(W,Z)| ~ agent(W,X,Z)| ~ state(W,X1)| ~ smoke(X2,X3)| ~ present(X2,X3)| ~ agent(X2,X3,X4)| ~ event(X2,X3)| ~ be(W,X1,X4,X4)| ~ man(W,X4)| ~ of(W,X5,X4)| ~ jules_forename(W,X5)| ~ forename(W,X5)| ~ proposition(W,X2)| ~ accessible_world(W,X2)| ~ think_believe_consider(W,X6)| ~ present(W,X6)| ~ event(W,X6)| ~ theme(W,X6,X2)| ~ vincent_forename(W,X7)| ~ forename(W,X7)| ~ agent(W,X6,X8)| ~ man(W,X8)| ~ of(W,X7,X8)| ~ actual_world(W) ) ))),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f96,plain,(
% 0.13/0.43 ![X0,X1]: (~smoke(X0,X1)|event(X0,X1))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.43 fof(f124,plain,(
% 0.13/0.43 ![X0,X1]: (~vincent_forename(X0,X1)|forename(X0,X1))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f29])).
% 0.13/0.43 fof(f125,plain,(
% 0.13/0.43 ![X0,X1]: (~jules_forename(X0,X1)|forename(X0,X1))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f30])).
% 0.13/0.43 fof(f164,plain,(
% 0.13/0.43 ![V,W]: ((![U]: (~accessible_world(U,V)|~man(U,W)))|man(V,W))),
% 0.13/0.43 inference(miniscoping,[status(thm)],[f52])).
% 0.13/0.43 fof(f165,plain,(
% 0.13/0.43 ![X0,X1,X2]: (~accessible_world(X0,X1)|~man(X0,X2)|man(X1,X2))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f164])).
% 0.13/0.43 fof(f204,plain,(
% 0.13/0.43 actual_world(skc8)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f72])).
% 0.13/0.43 fof(f205,plain,(
% 0.13/0.43 man(skc8,skc15)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f73])).
% 0.13/0.43 fof(f207,plain,(
% 0.13/0.43 vincent_forename(skc8,skc14)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f75])).
% 0.13/0.43 fof(f208,plain,(
% 0.13/0.43 event(skc8,skc13)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f76])).
% 0.13/0.43 fof(f209,plain,(
% 0.13/0.43 present(skc8,skc13)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f77])).
% 0.13/0.43 fof(f210,plain,(
% 0.13/0.43 think_believe_consider(skc8,skc13)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f78])).
% 0.13/0.43 fof(f211,plain,(
% 0.13/0.43 jules_forename(skc8,skc11)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f79])).
% 0.13/0.43 fof(f213,plain,(
% 0.13/0.43 man(skc8,skc10)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f81])).
% 0.13/0.43 fof(f214,plain,(
% 0.13/0.43 state(skc8,skc9)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f82])).
% 0.13/0.43 fof(f215,plain,(
% 0.13/0.43 accessible_world(skc8,skc12)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f83])).
% 0.13/0.43 fof(f216,plain,(
% 0.13/0.43 proposition(skc8,skc12)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f84])).
% 0.13/0.43 fof(f217,plain,(
% 0.13/0.43 of(skc8,skc14,skc15)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f85])).
% 0.13/0.43 fof(f218,plain,(
% 0.13/0.43 agent(skc8,skc13,skc15)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f86])).
% 0.13/0.43 fof(f219,plain,(
% 0.13/0.43 theme(skc8,skc13,skc12)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f87])).
% 0.13/0.43 fof(f220,plain,(
% 0.13/0.43 of(skc8,skc11,skc10)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f88])).
% 0.13/0.43 fof(f221,plain,(
% 0.13/0.43 be(skc8,skc9,skc10,skc10)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f89])).
% 0.13/0.43 fof(f222,plain,(
% 0.13/0.43 (![U]: ~man(skc12,U))|(![V]: smoke(skc12,skf2(V)))),
% 0.13/0.43 inference(miniscoping,[status(thm)],[f90])).
% 0.13/0.43 fof(f223,plain,(
% 0.13/0.43 ![X0,X1]: (~man(skc12,X0)|smoke(skc12,skf2(X1)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f222])).
% 0.13/0.43 fof(f224,plain,(
% 0.13/0.43 (![U]: ~man(skc12,U))|(![V]: present(skc12,skf2(V)))),
% 0.13/0.43 inference(miniscoping,[status(thm)],[f91])).
% 0.13/0.43 fof(f225,plain,(
% 0.13/0.43 ![X0,X1]: (~man(skc12,X0)|present(skc12,skf2(X1)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f224])).
% 0.13/0.43 fof(f228,plain,(
% 0.13/0.43 ![X0]: (~man(skc12,X0)|agent(skc12,skf2(X0),X0))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f93])).
% 0.13/0.43 fof(f229,plain,(
% 0.13/0.43 ![V]: ((![U]: ((![X6,X7]: (((![X5]: ((((![X1]: (((((((![X4]: (((![X3]: (((![Z]: ((![X2]: ((((((![W,Y]: (((![X]: ((((((((~accessible_world(U,V)|~proposition(U,V))|~theme(U,W,V))|~event(U,W))|~present(U,W))|~think_believe_consider(U,W))|~forename(U,X))|~vincent_forename(U,X))|~of(U,X,Y)))|~man(U,Y))|~agent(U,W,Y)))|~state(U,Z))|~smoke(X1,X2))|~present(X1,X2))|~agent(X1,X2,X3))|~event(X1,X2)))|~be(U,Z,X3,X3)))|~man(U,X3))|~of(U,X4,X3)))|~jules_forename(U,X4))|~forename(U,X4)))|~proposition(U,X1))|~accessible_world(U,X1))|~think_believe_consider(U,X5))|~present(U,X5))|~event(U,X5))|~theme(U,X5,X1)))|~vincent_forename(U,X6))|~forename(U,X6))|~agent(U,X5,X7)))|~man(U,X7))|~of(U,X6,X7)))|~actual_world(U)))|man(V,skf4(V)))),
% 0.13/0.43 inference(miniscoping,[status(thm)],[f94])).
% 0.13/0.43 fof(f230,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~accessible_world(X0,X1)|~proposition(X0,X1)|~theme(X0,X2,X1)|~event(X0,X2)|~present(X0,X2)|~think_believe_consider(X0,X2)|~forename(X0,X3)|~vincent_forename(X0,X3)|~of(X0,X3,X4)|~man(X0,X4)|~agent(X0,X2,X4)|~state(X0,X5)|~smoke(X6,X7)|~present(X6,X7)|~agent(X6,X7,X8)|~event(X6,X7)|~be(X0,X5,X8,X8)|~man(X0,X8)|~of(X0,X9,X8)|~jules_forename(X0,X9)|~forename(X0,X9)|~proposition(X0,X6)|~accessible_world(X0,X6)|~think_believe_consider(X0,X10)|~present(X0,X10)|~event(X0,X10)|~theme(X0,X10,X6)|~vincent_forename(X0,X11)|~forename(X0,X11)|~agent(X0,X10,X12)|~man(X0,X12)|~of(X0,X11,X12)|~actual_world(X0)|man(X1,skf4(X1)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f229])).
% 0.13/0.43 fof(f231,plain,(
% 0.13/0.43 ![W]: ((![X7,X8]: (((![X6]: ((((![X2]: (((((((![X5]: (((![X4]: (((![X1]: ((![X3]: ((((((![X,Z]: (((![Y]: (((((((![U]: ((((![V]: (((~smoke(U,V)|~present(U,V))|~agent(U,V,skf4(U)))|~event(U,V)))|~accessible_world(W,U))|~proposition(W,U))|~theme(W,X,U)))|~event(W,X))|~present(W,X))|~think_believe_consider(W,X))|~forename(W,Y))|~vincent_forename(W,Y))|~of(W,Y,Z)))|~man(W,Z))|~agent(W,X,Z)))|~state(W,X1))|~smoke(X2,X3))|~present(X2,X3))|~agent(X2,X3,X4))|~event(X2,X3)))|~be(W,X1,X4,X4)))|~man(W,X4))|~of(W,X5,X4)))|~jules_forename(W,X5))|~forename(W,X5)))|~proposition(W,X2))|~accessible_world(W,X2))|~think_believe_consider(W,X6))|~present(W,X6))|~event(W,X6))|~theme(W,X6,X2)))|~vincent_forename(W,X7))|~forename(W,X7))|~agent(W,X6,X8)))|~man(W,X8))|~of(W,X7,X8)))|~actual_world(W))),
% 0.13/0.43 inference(miniscoping,[status(thm)],[f95])).
% 0.13/0.43 fof(f232,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~event(X0,X1)|~accessible_world(X2,X0)|~proposition(X2,X0)|~theme(X2,X3,X0)|~event(X2,X3)|~present(X2,X3)|~think_believe_consider(X2,X3)|~forename(X2,X4)|~vincent_forename(X2,X4)|~of(X2,X4,X5)|~man(X2,X5)|~agent(X2,X3,X5)|~state(X2,X6)|~smoke(X7,X8)|~present(X7,X8)|~agent(X7,X8,X9)|~event(X7,X8)|~be(X2,X6,X9,X9)|~man(X2,X9)|~of(X2,X10,X9)|~jules_forename(X2,X10)|~forename(X2,X10)|~proposition(X2,X7)|~accessible_world(X2,X7)|~think_believe_consider(X2,X11)|~present(X2,X11)|~event(X2,X11)|~theme(X2,X11,X7)|~vincent_forename(X2,X12)|~forename(X2,X12)|~agent(X2,X11,X13)|~man(X2,X13)|~of(X2,X12,X13)|~actual_world(X2))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f231])).
% 0.13/0.43 fof(f286,plain,(
% 0.13/0.43 ![X0]: (~man(skc8,X0)|man(skc12,X0))),
% 0.13/0.43 inference(resolution,[status(thm)],[f165,f215])).
% 0.13/0.43 fof(f307,plain,(
% 0.13/0.43 man(skc12,skc10)),
% 0.13/0.43 inference(resolution,[status(thm)],[f286,f213])).
% 0.13/0.43 fof(f309,plain,(
% 0.13/0.43 ![X0]: (present(skc12,skf2(X0)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f307,f225])).
% 0.13/0.43 fof(f310,plain,(
% 0.13/0.43 ![X0]: (smoke(skc12,skf2(X0)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f307,f223])).
% 0.13/0.43 fof(f379,plain,(
% 0.13/0.43 agent(skc12,skf2(skc10),skc10)),
% 0.13/0.43 inference(resolution,[status(thm)],[f228,f307])).
% 0.13/0.43 fof(f405,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~accessible_world(X0,X1)|~proposition(X0,X1)|~theme(X0,X2,X1)|~event(X0,X2)|~present(X0,X2)|~think_believe_consider(X0,X2)|~forename(X0,X3)|~vincent_forename(X0,X3)|~of(X0,X3,X4)|~man(X0,X4)|~agent(X0,X2,X4)|~state(X0,X5)|~smoke(X6,X7)|~present(X6,X7)|~agent(X6,X7,X8)|~be(X0,X5,X8,X8)|~man(X0,X8)|~of(X0,X9,X8)|~jules_forename(X0,X9)|~forename(X0,X9)|~proposition(X0,X6)|~accessible_world(X0,X6)|~think_believe_consider(X0,X10)|~present(X0,X10)|~event(X0,X10)|~theme(X0,X10,X6)|~vincent_forename(X0,X11)|~forename(X0,X11)|~agent(X0,X10,X12)|~man(X0,X12)|~of(X0,X11,X12)|~actual_world(X0)|man(X1,skf4(X1)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f230,f96])).
% 0.13/0.43 fof(f406,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X1,X0)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~forename(skc8,X2)|~vincent_forename(skc8,X2)|~of(skc8,X2,X3)|~man(skc8,X3)|~agent(skc8,X1,X3)|~state(skc8,X4)|~smoke(X5,X6)|~present(X5,X6)|~agent(X5,X6,X7)|~be(skc8,X4,X7,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~jules_forename(skc8,X8)|~forename(skc8,X8)|~proposition(skc8,X5)|~accessible_world(skc8,X5)|~think_believe_consider(skc8,X9)|~present(skc8,X9)|~event(skc8,X9)|~theme(skc8,X9,X5)|~vincent_forename(skc8,X10)|~forename(skc8,X10)|~agent(skc8,X9,X11)|~man(skc8,X11)|~of(skc8,X10,X11)|man(X0,skf4(X0)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f405,f204])).
% 0.13/0.43 fof(f407,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X1,X0)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~forename(skc8,X2)|~vincent_forename(skc8,X2)|~of(skc8,X2,X3)|~man(skc8,X3)|~agent(skc8,X1,X3)|~state(skc8,X4)|~smoke(X5,X6)|~present(X5,X6)|~agent(X5,X6,X7)|~be(skc8,X4,X7,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~jules_forename(skc8,X8)|~proposition(skc8,X5)|~accessible_world(skc8,X5)|~think_believe_consider(skc8,X9)|~present(skc8,X9)|~event(skc8,X9)|~theme(skc8,X9,X5)|~vincent_forename(skc8,X10)|~forename(skc8,X10)|~agent(skc8,X9,X11)|~man(skc8,X11)|~of(skc8,X10,X11)|man(X0,skf4(X0)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f406,f125])).
% 0.13/0.43 fof(f436,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~accessible_world(X2,X0)|~proposition(X2,X0)|~theme(X2,X3,X0)|~event(X2,X3)|~present(X2,X3)|~think_believe_consider(X2,X3)|~forename(X2,X4)|~vincent_forename(X2,X4)|~of(X2,X4,X5)|~man(X2,X5)|~agent(X2,X3,X5)|~state(X2,X6)|~smoke(X7,X8)|~present(X7,X8)|~agent(X7,X8,X9)|~event(X7,X8)|~be(X2,X6,X9,X9)|~man(X2,X9)|~of(X2,X10,X9)|~jules_forename(X2,X10)|~forename(X2,X10)|~proposition(X2,X7)|~accessible_world(X2,X7)|~think_believe_consider(X2,X11)|~present(X2,X11)|~event(X2,X11)|~theme(X2,X11,X7)|~vincent_forename(X2,X12)|~forename(X2,X12)|~agent(X2,X11,X13)|~man(X2,X13)|~of(X2,X12,X13)|~actual_world(X2))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f232,f96])).
% 0.13/0.43 fof(f437,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X2,X0)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~forename(skc8,X3)|~vincent_forename(skc8,X3)|~of(skc8,X3,X4)|~man(skc8,X4)|~agent(skc8,X2,X4)|~state(skc8,X5)|~smoke(X6,X7)|~present(X6,X7)|~agent(X6,X7,X8)|~event(X6,X7)|~be(skc8,X5,X8,X8)|~man(skc8,X8)|~of(skc8,X9,X8)|~jules_forename(skc8,X9)|~forename(skc8,X9)|~proposition(skc8,X6)|~accessible_world(skc8,X6)|~think_believe_consider(skc8,X10)|~present(skc8,X10)|~event(skc8,X10)|~theme(skc8,X10,X6)|~vincent_forename(skc8,X11)|~forename(skc8,X11)|~agent(skc8,X10,X12)|~man(skc8,X12)|~of(skc8,X11,X12))),
% 0.13/0.43 inference(resolution,[status(thm)],[f436,f204])).
% 0.13/0.43 fof(f438,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X2,X0)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~forename(skc8,X3)|~vincent_forename(skc8,X3)|~of(skc8,X3,X4)|~man(skc8,X4)|~agent(skc8,X2,X4)|~state(skc8,X5)|~smoke(X6,X7)|~present(X6,X7)|~agent(X6,X7,X8)|~be(skc8,X5,X8,X8)|~man(skc8,X8)|~of(skc8,X9,X8)|~jules_forename(skc8,X9)|~forename(skc8,X9)|~proposition(skc8,X6)|~accessible_world(skc8,X6)|~think_believe_consider(skc8,X10)|~present(skc8,X10)|~event(skc8,X10)|~theme(skc8,X10,X6)|~vincent_forename(skc8,X11)|~forename(skc8,X11)|~agent(skc8,X10,X12)|~man(skc8,X12)|~of(skc8,X11,X12))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f437,f96])).
% 0.13/0.43 fof(f501,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X1,X0)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~vincent_forename(skc8,X2)|~of(skc8,X2,X3)|~man(skc8,X3)|~agent(skc8,X1,X3)|~state(skc8,X4)|~smoke(X5,X6)|~present(X5,X6)|~agent(X5,X6,X7)|~be(skc8,X4,X7,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~jules_forename(skc8,X8)|~proposition(skc8,X5)|~accessible_world(skc8,X5)|~think_believe_consider(skc8,X9)|~present(skc8,X9)|~event(skc8,X9)|~theme(skc8,X9,X5)|~vincent_forename(skc8,X10)|~forename(skc8,X10)|~agent(skc8,X9,X11)|~man(skc8,X11)|~of(skc8,X10,X11)|man(X0,skf4(X0)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f407,f124])).
% 0.13/0.43 fof(f502,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X1,X0)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~vincent_forename(skc8,X2)|~of(skc8,X2,X3)|~man(skc8,X3)|~agent(skc8,X1,X3)|~state(skc8,X4)|~smoke(skc12,X5)|~present(skc12,X5)|~agent(skc12,X5,X6)|~be(skc8,X4,X6,X6)|~man(skc8,X6)|~of(skc8,X7,X6)|~jules_forename(skc8,X7)|~proposition(skc8,skc12)|~think_believe_consider(skc8,X8)|~present(skc8,X8)|~event(skc8,X8)|~theme(skc8,X8,skc12)|~vincent_forename(skc8,X9)|~forename(skc8,X9)|~agent(skc8,X8,X10)|~man(skc8,X10)|~of(skc8,X9,X10)|man(X0,skf4(X0)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f501,f215])).
% 0.13/0.43 fof(f503,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X1,X0)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~vincent_forename(skc8,X2)|~of(skc8,X2,X3)|~man(skc8,X3)|~agent(skc8,X1,X3)|~state(skc8,X4)|~smoke(skc12,X5)|~present(skc12,X5)|~agent(skc12,X5,X6)|~be(skc8,X4,X6,X6)|~man(skc8,X6)|~of(skc8,X7,X6)|~jules_forename(skc8,X7)|~think_believe_consider(skc8,X8)|~present(skc8,X8)|~event(skc8,X8)|~theme(skc8,X8,skc12)|~vincent_forename(skc8,X9)|~forename(skc8,X9)|~agent(skc8,X8,X10)|~man(skc8,X10)|~of(skc8,X9,X10)|man(X0,skf4(X0)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f502,f216])).
% 0.13/0.43 fof(f517,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X1,X0)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~vincent_forename(skc8,X2)|~of(skc8,X2,X3)|~man(skc8,X3)|~agent(skc8,X1,X3)|~state(skc8,X4)|~smoke(skc12,X5)|~present(skc12,X5)|~agent(skc12,X5,X6)|~be(skc8,X4,X6,X6)|~man(skc8,X6)|~of(skc8,X7,X6)|~jules_forename(skc8,X7)|~think_believe_consider(skc8,X8)|~present(skc8,X8)|~event(skc8,X8)|~theme(skc8,X8,skc12)|~vincent_forename(skc8,X9)|~agent(skc8,X8,X10)|~man(skc8,X10)|~of(skc8,X9,X10)|man(X0,skf4(X0)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f503,f124])).
% 0.13/0.43 fof(f518,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X1,X0)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~vincent_forename(skc8,X2)|~of(skc8,X2,X3)|~man(skc8,X3)|~agent(skc8,X1,X3)|~state(skc8,X4)|~smoke(skc12,X5)|~present(skc12,X5)|~agent(skc12,X5,X6)|~be(skc8,X4,X6,X6)|~man(skc8,X6)|~of(skc8,X7,X6)|~jules_forename(skc8,X7)|~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~vincent_forename(skc8,X8)|~agent(skc8,skc13,X9)|~man(skc8,X9)|~of(skc8,X8,X9)|man(X0,skf4(X0)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f517,f219])).
% 0.13/0.43 fof(f519,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X1,X0)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~vincent_forename(skc8,X2)|~of(skc8,X2,X3)|~man(skc8,X3)|~agent(skc8,X1,X3)|~state(skc8,X4)|~smoke(skc12,X5)|~present(skc12,X5)|~agent(skc12,X5,X6)|~be(skc8,X4,X6,X6)|~man(skc8,X6)|~of(skc8,X7,X6)|~jules_forename(skc8,X7)|~present(skc8,skc13)|~event(skc8,skc13)|~vincent_forename(skc8,X8)|~agent(skc8,skc13,X9)|~man(skc8,X9)|~of(skc8,X8,X9)|man(X0,skf4(X0)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f518,f210])).
% 0.13/0.43 fof(f520,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X2,X0)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~forename(skc8,X3)|~vincent_forename(skc8,X3)|~of(skc8,X3,X4)|~man(skc8,X4)|~agent(skc8,X2,X4)|~state(skc8,X5)|~smoke(X6,X7)|~present(X6,X7)|~agent(X6,X7,X8)|~be(skc8,X5,X8,X8)|~man(skc8,X8)|~of(skc8,X9,X8)|~jules_forename(skc8,X9)|~proposition(skc8,X6)|~accessible_world(skc8,X6)|~think_believe_consider(skc8,X10)|~present(skc8,X10)|~event(skc8,X10)|~theme(skc8,X10,X6)|~vincent_forename(skc8,X11)|~forename(skc8,X11)|~agent(skc8,X10,X12)|~man(skc8,X12)|~of(skc8,X11,X12))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f438,f125])).
% 0.13/0.43 fof(f521,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X2,X0)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~forename(skc8,X3)|~vincent_forename(skc8,X3)|~of(skc8,X3,X4)|~man(skc8,X4)|~agent(skc8,X2,X4)|~state(skc8,X5)|~smoke(skc12,X6)|~present(skc12,X6)|~agent(skc12,X6,X7)|~be(skc8,X5,X7,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~jules_forename(skc8,X8)|~proposition(skc8,skc12)|~think_believe_consider(skc8,X9)|~present(skc8,X9)|~event(skc8,X9)|~theme(skc8,X9,skc12)|~vincent_forename(skc8,X10)|~forename(skc8,X10)|~agent(skc8,X9,X11)|~man(skc8,X11)|~of(skc8,X10,X11))),
% 0.13/0.43 inference(resolution,[status(thm)],[f520,f215])).
% 0.13/0.43 fof(f522,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X2,X0)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~vincent_forename(skc8,X3)|~of(skc8,X3,X4)|~man(skc8,X4)|~agent(skc8,X2,X4)|~state(skc8,X5)|~smoke(skc12,X6)|~present(skc12,X6)|~agent(skc12,X6,X7)|~be(skc8,X5,X7,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~jules_forename(skc8,X8)|~proposition(skc8,skc12)|~think_believe_consider(skc8,X9)|~present(skc8,X9)|~event(skc8,X9)|~theme(skc8,X9,skc12)|~vincent_forename(skc8,X10)|~forename(skc8,X10)|~agent(skc8,X9,X11)|~man(skc8,X11)|~of(skc8,X10,X11))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f521,f124])).
% 0.13/0.43 fof(f523,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X2,X0)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~vincent_forename(skc8,X3)|~of(skc8,X3,X4)|~man(skc8,X4)|~agent(skc8,X2,X4)|~state(skc8,X5)|~smoke(skc12,X6)|~present(skc12,X6)|~agent(skc12,X6,X7)|~be(skc8,X5,X7,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~jules_forename(skc8,X8)|~think_believe_consider(skc8,X9)|~present(skc8,X9)|~event(skc8,X9)|~theme(skc8,X9,skc12)|~vincent_forename(skc8,X10)|~forename(skc8,X10)|~agent(skc8,X9,X11)|~man(skc8,X11)|~of(skc8,X10,X11))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f522,f216])).
% 0.13/0.43 fof(f524,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X2,X0)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~vincent_forename(skc8,X3)|~of(skc8,X3,X4)|~man(skc8,X4)|~agent(skc8,X2,X4)|~state(skc8,X5)|~smoke(skc12,X6)|~present(skc12,X6)|~agent(skc12,X6,X7)|~be(skc8,X5,X7,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~jules_forename(skc8,X8)|~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~vincent_forename(skc8,X9)|~forename(skc8,X9)|~agent(skc8,skc13,X10)|~man(skc8,X10)|~of(skc8,X9,X10))),
% 0.13/0.43 inference(resolution,[status(thm)],[f523,f219])).
% 0.13/0.43 fof(f525,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X2,X0)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~vincent_forename(skc8,X3)|~of(skc8,X3,X4)|~man(skc8,X4)|~agent(skc8,X2,X4)|~state(skc8,X5)|~smoke(skc12,X6)|~present(skc12,X6)|~agent(skc12,X6,X7)|~be(skc8,X5,X7,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~jules_forename(skc8,X8)|~present(skc8,skc13)|~event(skc8,skc13)|~vincent_forename(skc8,X9)|~forename(skc8,X9)|~agent(skc8,skc13,X10)|~man(skc8,X10)|~of(skc8,X9,X10))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f524,f210])).
% 0.13/0.43 fof(f563,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X1,X0)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~vincent_forename(skc8,X2)|~of(skc8,X2,X3)|~man(skc8,X3)|~agent(skc8,X1,X3)|~state(skc8,X4)|~smoke(skc12,X5)|~present(skc12,X5)|~agent(skc12,X5,X6)|~be(skc8,X4,X6,X6)|~man(skc8,X6)|~of(skc8,X7,X6)|~jules_forename(skc8,X7)|~event(skc8,skc13)|~vincent_forename(skc8,X8)|~agent(skc8,skc13,X9)|~man(skc8,X9)|~of(skc8,X8,X9)|man(X0,skf4(X0)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f519,f209])).
% 0.13/0.43 fof(f564,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X1,X0)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~vincent_forename(skc8,X2)|~of(skc8,X2,X3)|~man(skc8,X3)|~agent(skc8,X1,X3)|~state(skc8,X4)|~smoke(skc12,X5)|~present(skc12,X5)|~agent(skc12,X5,X6)|~be(skc8,X4,X6,X6)|~man(skc8,X6)|~of(skc8,X7,X6)|~jules_forename(skc8,X7)|~vincent_forename(skc8,X8)|~agent(skc8,skc13,X9)|~man(skc8,X9)|~of(skc8,X8,X9)|man(X0,skf4(X0)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f563,f208])).
% 0.13/0.43 fof(f565,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X1,X0)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~vincent_forename(skc8,X2)|~of(skc8,X2,X3)|~man(skc8,X3)|~agent(skc8,X1,X3)|~state(skc8,X4)|~smoke(skc12,X5)|~present(skc12,X5)|~agent(skc12,X5,X6)|~be(skc8,X4,X6,X6)|~man(skc8,X6)|~of(skc8,X7,X6)|~jules_forename(skc8,X7)|~vincent_forename(skc8,X8)|~man(skc8,skc15)|~of(skc8,X8,skc15)|man(X0,skf4(X0)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f564,f218])).
% 0.13/0.43 fof(f566,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X1,X0)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~vincent_forename(skc8,X2)|~of(skc8,X2,X3)|~man(skc8,X3)|~agent(skc8,X1,X3)|~state(skc8,X4)|~smoke(skc12,X5)|~present(skc12,X5)|~agent(skc12,X5,X6)|~be(skc8,X4,X6,X6)|~man(skc8,X6)|~of(skc8,X7,X6)|~jules_forename(skc8,X7)|~vincent_forename(skc8,X8)|~of(skc8,X8,skc15)|man(X0,skf4(X0)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f565,f205])).
% 0.13/0.43 fof(f567,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X1,X0)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~vincent_forename(skc8,X2)|~of(skc8,X2,X3)|~man(skc8,X3)|~agent(skc8,X1,X3)|~state(skc8,X4)|~smoke(skc12,X5)|~present(skc12,X5)|~agent(skc12,X5,X6)|~be(skc8,X4,X6,X6)|~man(skc8,X6)|~of(skc8,X7,X6)|~jules_forename(skc8,X7)|~vincent_forename(skc8,skc14)|man(X0,skf4(X0)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f566,f217])).
% 0.13/0.43 fof(f568,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X1,X0)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~vincent_forename(skc8,X2)|~of(skc8,X2,X3)|~man(skc8,X3)|~agent(skc8,X1,X3)|~state(skc8,X4)|~smoke(skc12,X5)|~present(skc12,X5)|~agent(skc12,X5,X6)|~be(skc8,X4,X6,X6)|~man(skc8,X6)|~of(skc8,X7,X6)|~jules_forename(skc8,X7)|man(X0,skf4(X0)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f567,f207])).
% 0.13/0.43 fof(f569,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6]: (~proposition(skc8,skc12)|~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~vincent_forename(skc8,X1)|~of(skc8,X1,X2)|~man(skc8,X2)|~agent(skc8,X0,X2)|~state(skc8,X3)|~smoke(skc12,X4)|~present(skc12,X4)|~agent(skc12,X4,X5)|~be(skc8,X3,X5,X5)|~man(skc8,X5)|~of(skc8,X6,X5)|~jules_forename(skc8,X6)|man(skc12,skf4(skc12)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f568,f215])).
% 0.13/0.43 fof(f570,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6]: (~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~vincent_forename(skc8,X1)|~of(skc8,X1,X2)|~man(skc8,X2)|~agent(skc8,X0,X2)|~state(skc8,X3)|~smoke(skc12,X4)|~present(skc12,X4)|~agent(skc12,X4,X5)|~be(skc8,X3,X5,X5)|~man(skc8,X5)|~of(skc8,X6,X5)|~jules_forename(skc8,X6)|man(skc12,skf4(skc12)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f569,f216])).
% 0.13/0.43 fof(f571,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4]: (~theme(skc8,skc13,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~vincent_forename(skc8,X0)|~of(skc8,X0,skc15)|~man(skc8,skc15)|~state(skc8,X1)|~smoke(skc12,X2)|~present(skc12,X2)|~agent(skc12,X2,X3)|~be(skc8,X1,X3,X3)|~man(skc8,X3)|~of(skc8,X4,X3)|~jules_forename(skc8,X4)|man(skc12,skf4(skc12)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f570,f218])).
% 0.13/0.43 fof(f577,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4]: (~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~vincent_forename(skc8,X0)|~of(skc8,X0,skc15)|~man(skc8,skc15)|~state(skc8,X1)|~smoke(skc12,X2)|~present(skc12,X2)|~agent(skc12,X2,X3)|~be(skc8,X1,X3,X3)|~man(skc8,X3)|~of(skc8,X4,X3)|~jules_forename(skc8,X4)|man(skc12,skf4(skc12)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f571,f219])).
% 0.13/0.43 fof(f583,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4]: (~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~vincent_forename(skc8,X0)|~of(skc8,X0,skc15)|~man(skc8,skc15)|~state(skc8,X1)|~smoke(skc12,X2)|~present(skc12,X2)|~agent(skc12,X2,X3)|~be(skc8,X1,X3,X3)|~man(skc8,X3)|~of(skc8,X4,X3)|~jules_forename(skc8,X4)|man(skc12,skf4(skc12)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f577,f208])).
% 0.13/0.43 fof(f584,plain,(
% 0.13/0.43 ![X0,X1,X2,X3]: (~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~vincent_forename(skc8,skc14)|~man(skc8,skc15)|~state(skc8,X0)|~smoke(skc12,X1)|~present(skc12,X1)|~agent(skc12,X1,X2)|~be(skc8,X0,X2,X2)|~man(skc8,X2)|~of(skc8,X3,X2)|~jules_forename(skc8,X3)|man(skc12,skf4(skc12)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f583,f217])).
% 0.13/0.43 fof(f585,plain,(
% 0.13/0.43 ![X0,X1,X2,X3]: (~think_believe_consider(skc8,skc13)|~vincent_forename(skc8,skc14)|~man(skc8,skc15)|~state(skc8,X0)|~smoke(skc12,X1)|~present(skc12,X1)|~agent(skc12,X1,X2)|~be(skc8,X0,X2,X2)|~man(skc8,X2)|~of(skc8,X3,X2)|~jules_forename(skc8,X3)|man(skc12,skf4(skc12)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f584,f209])).
% 0.13/0.43 fof(f586,plain,(
% 0.13/0.43 ![X0,X1,X2,X3]: (~vincent_forename(skc8,skc14)|~man(skc8,skc15)|~state(skc8,X0)|~smoke(skc12,X1)|~present(skc12,X1)|~agent(skc12,X1,X2)|~be(skc8,X0,X2,X2)|~man(skc8,X2)|~of(skc8,X3,X2)|~jules_forename(skc8,X3)|man(skc12,skf4(skc12)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f585,f210])).
% 0.13/0.43 fof(f588,plain,(
% 0.13/0.43 ![X0,X1]: (~vincent_forename(skc8,skc14)|~man(skc8,skc15)|~state(skc8,X0)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~be(skc8,X0,skc10,skc10)|~man(skc8,skc10)|~of(skc8,X1,skc10)|~jules_forename(skc8,X1)|man(skc12,skf4(skc12)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f586,f379])).
% 0.13/0.43 fof(f592,plain,(
% 0.13/0.43 ![X0,X1]: (~man(skc8,skc15)|~state(skc8,X0)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~be(skc8,X0,skc10,skc10)|~man(skc8,skc10)|~of(skc8,X1,skc10)|~jules_forename(skc8,X1)|man(skc12,skf4(skc12)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f588,f207])).
% 0.13/0.43 fof(f606,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X2,X0)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~vincent_forename(skc8,X3)|~of(skc8,X3,X4)|~man(skc8,X4)|~agent(skc8,X2,X4)|~state(skc8,X5)|~smoke(skc12,X6)|~present(skc12,X6)|~agent(skc12,X6,X7)|~be(skc8,X5,X7,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~jules_forename(skc8,X8)|~event(skc8,skc13)|~vincent_forename(skc8,X9)|~forename(skc8,X9)|~agent(skc8,skc13,X10)|~man(skc8,X10)|~of(skc8,X9,X10))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f525,f209])).
% 0.13/0.43 fof(f607,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X2,X0)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~vincent_forename(skc8,X3)|~of(skc8,X3,X4)|~man(skc8,X4)|~agent(skc8,X2,X4)|~state(skc8,X5)|~smoke(skc12,X6)|~present(skc12,X6)|~agent(skc12,X6,X7)|~be(skc8,X5,X7,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~jules_forename(skc8,X8)|~vincent_forename(skc8,X9)|~forename(skc8,X9)|~agent(skc8,skc13,X10)|~man(skc8,X10)|~of(skc8,X9,X10))),
% 0.13/0.43 inference(resolution,[status(thm)],[f606,f208])).
% 0.13/0.43 fof(f608,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X2,X0)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~vincent_forename(skc8,X3)|~of(skc8,X3,X4)|~man(skc8,X4)|~agent(skc8,X2,X4)|~state(skc8,X5)|~smoke(skc12,X6)|~present(skc12,X6)|~agent(skc12,X6,X7)|~be(skc8,X5,X7,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~jules_forename(skc8,X8)|~vincent_forename(skc8,X9)|~agent(skc8,skc13,X10)|~man(skc8,X10)|~of(skc8,X9,X10))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f607,f124])).
% 0.13/0.43 fof(f609,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X2,X0)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~vincent_forename(skc8,X3)|~of(skc8,X3,X4)|~man(skc8,X4)|~agent(skc8,X2,X4)|~state(skc8,X5)|~smoke(skc12,X6)|~present(skc12,X6)|~agent(skc12,X6,X7)|~be(skc8,X5,X7,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~jules_forename(skc8,X8)|~vincent_forename(skc8,X9)|~man(skc8,skc15)|~of(skc8,X9,skc15))),
% 0.13/0.43 inference(resolution,[status(thm)],[f608,f218])).
% 0.13/0.43 fof(f610,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X2,X0)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~vincent_forename(skc8,X3)|~of(skc8,X3,X4)|~man(skc8,X4)|~agent(skc8,X2,X4)|~state(skc8,X5)|~smoke(skc12,X6)|~present(skc12,X6)|~agent(skc12,X6,X7)|~be(skc8,X5,X7,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~jules_forename(skc8,X8)|~vincent_forename(skc8,X9)|~of(skc8,X9,skc15))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f609,f205])).
% 0.13/0.43 fof(f613,plain,(
% 0.13/0.43 ![X0,X1]: (~state(skc8,X0)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~be(skc8,X0,skc10,skc10)|~man(skc8,skc10)|~of(skc8,X1,skc10)|~jules_forename(skc8,X1)|man(skc12,skf4(skc12)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f592,f205])).
% 0.13/0.43 fof(f614,plain,(
% 0.13/0.43 ![X0,X1]: (~state(skc8,X0)|~smoke(skc12,skf2(skc10))|~be(skc8,X0,skc10,skc10)|~man(skc8,skc10)|~of(skc8,X1,skc10)|~jules_forename(skc8,X1)|man(skc12,skf4(skc12)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f613,f309])).
% 0.13/0.43 fof(f618,plain,(
% 0.13/0.43 ![X0,X1]: (~state(skc8,X0)|~be(skc8,X0,skc10,skc10)|~man(skc8,skc10)|~of(skc8,X1,skc10)|~jules_forename(skc8,X1)|man(skc12,skf4(skc12)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f614,f310])).
% 0.13/0.43 fof(f622,plain,(
% 0.13/0.43 ![X0,X1]: (~state(skc8,X0)|~be(skc8,X0,skc10,skc10)|~of(skc8,X1,skc10)|~jules_forename(skc8,X1)|man(skc12,skf4(skc12)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f618,f213])).
% 0.13/0.43 fof(f623,plain,(
% 0.13/0.43 ![X0]: (~state(skc8,skc9)|~of(skc8,X0,skc10)|~jules_forename(skc8,X0)|man(skc12,skf4(skc12)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f622,f221])).
% 0.13/0.43 fof(f624,plain,(
% 0.13/0.43 ![X0]: (~of(skc8,X0,skc10)|~jules_forename(skc8,X0)|man(skc12,skf4(skc12)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f623,f214])).
% 0.13/0.43 fof(f625,plain,(
% 0.13/0.43 ~jules_forename(skc8,skc11)|man(skc12,skf4(skc12))),
% 0.13/0.43 inference(resolution,[status(thm)],[f624,f220])).
% 0.13/0.43 fof(f626,plain,(
% 0.13/0.43 man(skc12,skf4(skc12))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f625,f211])).
% 0.13/0.43 fof(f627,plain,(
% 0.13/0.43 agent(skc12,skf2(skf4(skc12)),skf4(skc12))),
% 0.13/0.43 inference(resolution,[status(thm)],[f626,f228])).
% 0.13/0.43 fof(f640,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X2,X0)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~vincent_forename(skc8,X3)|~of(skc8,X3,X4)|~man(skc8,X4)|~agent(skc8,X2,X4)|~state(skc8,X5)|~smoke(skc12,X6)|~present(skc12,X6)|~agent(skc12,X6,X7)|~be(skc8,X5,X7,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~jules_forename(skc8,X8)|~vincent_forename(skc8,skc14))),
% 0.13/0.43 inference(resolution,[status(thm)],[f610,f217])).
% 0.13/0.43 fof(f641,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X2,X0)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~vincent_forename(skc8,X3)|~of(skc8,X3,X4)|~man(skc8,X4)|~agent(skc8,X2,X4)|~state(skc8,X5)|~smoke(skc12,X6)|~present(skc12,X6)|~agent(skc12,X6,X7)|~be(skc8,X5,X7,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~jules_forename(skc8,X8))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f640,f207])).
% 0.13/0.43 fof(f642,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~smoke(skc12,X0)|~present(skc12,X0)|~agent(skc12,X0,skf4(skc12))|~proposition(skc8,skc12)|~theme(skc8,X1,skc12)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~vincent_forename(skc8,X2)|~of(skc8,X2,X3)|~man(skc8,X3)|~agent(skc8,X1,X3)|~state(skc8,X4)|~smoke(skc12,X5)|~present(skc12,X5)|~agent(skc12,X5,X6)|~be(skc8,X4,X6,X6)|~man(skc8,X6)|~of(skc8,X7,X6)|~jules_forename(skc8,X7))),
% 0.13/0.43 inference(resolution,[status(thm)],[f641,f215])).
% 0.13/0.43 fof(f643,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~smoke(skc12,X0)|~present(skc12,X0)|~agent(skc12,X0,skf4(skc12))|~theme(skc8,X1,skc12)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~vincent_forename(skc8,X2)|~of(skc8,X2,X3)|~man(skc8,X3)|~agent(skc8,X1,X3)|~state(skc8,X4)|~smoke(skc12,X5)|~present(skc12,X5)|~agent(skc12,X5,X6)|~be(skc8,X4,X6,X6)|~man(skc8,X6)|~of(skc8,X7,X6)|~jules_forename(skc8,X7))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f642,f216])).
% 0.13/0.43 fof(f647,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6]: (~smoke(skc12,skf2(skf4(skc12)))|~present(skc12,skf2(skf4(skc12)))|~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~vincent_forename(skc8,X1)|~of(skc8,X1,X2)|~man(skc8,X2)|~agent(skc8,X0,X2)|~state(skc8,X3)|~smoke(skc12,X4)|~present(skc12,X4)|~agent(skc12,X4,X5)|~be(skc8,X3,X5,X5)|~man(skc8,X5)|~of(skc8,X6,X5)|~jules_forename(skc8,X6))),
% 0.13/0.43 inference(resolution,[status(thm)],[f627,f643])).
% 0.13/0.43 fof(f648,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6]: (~present(skc12,skf2(skf4(skc12)))|~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~vincent_forename(skc8,X1)|~of(skc8,X1,X2)|~man(skc8,X2)|~agent(skc8,X0,X2)|~state(skc8,X3)|~smoke(skc12,X4)|~present(skc12,X4)|~agent(skc12,X4,X5)|~be(skc8,X3,X5,X5)|~man(skc8,X5)|~of(skc8,X6,X5)|~jules_forename(skc8,X6))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f647,f310])).
% 0.13/0.43 fof(f649,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6]: (~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~vincent_forename(skc8,X1)|~of(skc8,X1,X2)|~man(skc8,X2)|~agent(skc8,X0,X2)|~state(skc8,X3)|~smoke(skc12,X4)|~present(skc12,X4)|~agent(skc12,X4,X5)|~be(skc8,X3,X5,X5)|~man(skc8,X5)|~of(skc8,X6,X5)|~jules_forename(skc8,X6))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f648,f309])).
% 0.13/0.43 fof(f650,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5]: (~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~vincent_forename(skc8,X0)|~of(skc8,X0,X1)|~man(skc8,X1)|~agent(skc8,skc13,X1)|~state(skc8,X2)|~smoke(skc12,X3)|~present(skc12,X3)|~agent(skc12,X3,X4)|~be(skc8,X2,X4,X4)|~man(skc8,X4)|~of(skc8,X5,X4)|~jules_forename(skc8,X5))),
% 0.13/0.43 inference(resolution,[status(thm)],[f649,f219])).
% 0.13/0.43 fof(f651,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5]: (~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~vincent_forename(skc8,X0)|~of(skc8,X0,X1)|~man(skc8,X1)|~agent(skc8,skc13,X1)|~state(skc8,X2)|~smoke(skc12,X3)|~present(skc12,X3)|~agent(skc12,X3,X4)|~be(skc8,X2,X4,X4)|~man(skc8,X4)|~of(skc8,X5,X4)|~jules_forename(skc8,X5))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f650,f208])).
% 0.13/0.43 fof(f652,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5]: (~think_believe_consider(skc8,skc13)|~vincent_forename(skc8,X0)|~of(skc8,X0,X1)|~man(skc8,X1)|~agent(skc8,skc13,X1)|~state(skc8,X2)|~smoke(skc12,X3)|~present(skc12,X3)|~agent(skc12,X3,X4)|~be(skc8,X2,X4,X4)|~man(skc8,X4)|~of(skc8,X5,X4)|~jules_forename(skc8,X5))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f651,f209])).
% 0.13/0.43 fof(f653,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5]: (~vincent_forename(skc8,X0)|~of(skc8,X0,X1)|~man(skc8,X1)|~agent(skc8,skc13,X1)|~state(skc8,X2)|~smoke(skc12,X3)|~present(skc12,X3)|~agent(skc12,X3,X4)|~be(skc8,X2,X4,X4)|~man(skc8,X4)|~of(skc8,X5,X4)|~jules_forename(skc8,X5))),
% 0.13/0.43 inference(resolution,[status(thm)],[f652,f210])).
% 0.13/0.43 fof(f654,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4]: (~vincent_forename(skc8,X0)|~of(skc8,X0,skc15)|~man(skc8,skc15)|~state(skc8,X1)|~smoke(skc12,X2)|~present(skc12,X2)|~agent(skc12,X2,X3)|~be(skc8,X1,X3,X3)|~man(skc8,X3)|~of(skc8,X4,X3)|~jules_forename(skc8,X4))),
% 0.13/0.43 inference(resolution,[status(thm)],[f653,f218])).
% 0.13/0.43 fof(f655,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4]: (~vincent_forename(skc8,X0)|~of(skc8,X0,skc15)|~state(skc8,X1)|~smoke(skc12,X2)|~present(skc12,X2)|~agent(skc12,X2,X3)|~be(skc8,X1,X3,X3)|~man(skc8,X3)|~of(skc8,X4,X3)|~jules_forename(skc8,X4))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f654,f205])).
% 0.13/0.43 fof(f656,plain,(
% 0.13/0.43 ![X0,X1,X2,X3]: (~vincent_forename(skc8,skc14)|~state(skc8,X0)|~smoke(skc12,X1)|~present(skc12,X1)|~agent(skc12,X1,X2)|~be(skc8,X0,X2,X2)|~man(skc8,X2)|~of(skc8,X3,X2)|~jules_forename(skc8,X3))),
% 0.13/0.43 inference(resolution,[status(thm)],[f655,f217])).
% 0.13/0.43 fof(f657,plain,(
% 0.13/0.43 ![X0,X1,X2,X3]: (~state(skc8,X0)|~smoke(skc12,X1)|~present(skc12,X1)|~agent(skc12,X1,X2)|~be(skc8,X0,X2,X2)|~man(skc8,X2)|~of(skc8,X3,X2)|~jules_forename(skc8,X3))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f656,f207])).
% 0.13/0.43 fof(f658,plain,(
% 0.13/0.43 ![X0,X1,X2,X3]: (~state(skc8,X0)|~smoke(skc12,skf2(X1))|~agent(skc12,skf2(X1),X2)|~be(skc8,X0,X2,X2)|~man(skc8,X2)|~of(skc8,X3,X2)|~jules_forename(skc8,X3))),
% 0.13/0.43 inference(resolution,[status(thm)],[f657,f309])).
% 0.13/0.43 fof(f662,plain,(
% 0.13/0.43 ![X0,X1,X2,X3]: (~state(skc8,X0)|~agent(skc12,skf2(X1),X2)|~be(skc8,X0,X2,X2)|~man(skc8,X2)|~of(skc8,X3,X2)|~jules_forename(skc8,X3))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f658,f310])).
% 0.13/0.43 fof(f663,plain,(
% 0.13/0.43 ![X0,X1,X2]: (~state(skc8,X0)|~agent(skc12,skf2(X1),skc10)|~be(skc8,X0,skc10,skc10)|~of(skc8,X2,skc10)|~jules_forename(skc8,X2))),
% 0.13/0.43 inference(resolution,[status(thm)],[f662,f213])).
% 0.13/0.43 fof(f665,plain,(
% 0.13/0.43 ![X0,X1]: (~state(skc8,X0)|~be(skc8,X0,skc10,skc10)|~of(skc8,X1,skc10)|~jules_forename(skc8,X1))),
% 0.13/0.43 inference(resolution,[status(thm)],[f663,f379])).
% 0.13/0.43 fof(f666,plain,(
% 0.13/0.43 ![X0]: (~state(skc8,skc9)|~of(skc8,X0,skc10)|~jules_forename(skc8,X0))),
% 0.13/0.43 inference(resolution,[status(thm)],[f665,f221])).
% 0.13/0.43 fof(f667,plain,(
% 0.13/0.43 ![X0]: (~of(skc8,X0,skc10)|~jules_forename(skc8,X0))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f666,f214])).
% 0.13/0.43 fof(f668,plain,(
% 0.13/0.43 ~jules_forename(skc8,skc11)),
% 0.13/0.43 inference(resolution,[status(thm)],[f667,f220])).
% 0.13/0.43 fof(f669,plain,(
% 0.13/0.43 $false),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f668,f211])).
% 0.13/0.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.45 % Elapsed time: 0.083334 seconds
% 0.13/0.45 % CPU time: 0.358220 seconds
% 0.13/0.45 % Total memory used: 54.409 MB
% 0.13/0.45 % Net memory used: 53.987 MB
%------------------------------------------------------------------------------