%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NLP257-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 : n003.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:38 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP257-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.34 % Computer : n003.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 01:57:30 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.13/0.43 % Refutation found
% 0.13/0.43 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.43 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.43 fof(f1,axiom,(
% 0.13/0.43 (![U,V]: (( ~ smoke(U,V)| event(U,V) ) ))),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f29,axiom,(
% 0.13/0.43 (![U,V]: (( ~ vincent_forename(U,V)| forename(U,V) ) ))),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f30,axiom,(
% 0.13/0.43 (![U,V]: (( ~ jules_forename(U,V)| forename(U,V) ) ))),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f52,axiom,(
% 0.13/0.43 (![U,V,W]: (( ~ accessible_world(U,V)| ~ man(U,W)| man(V,W) ) ))),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f72,negated_conjecture,(
% 0.13/0.43 actual_world(skc8) ),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f73,negated_conjecture,(
% 0.13/0.43 man(skc8,skc15) ),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f74,negated_conjecture,(
% 0.13/0.43 forename(skc8,skc14) ),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f75,negated_conjecture,(
% 0.13/0.43 vincent_forename(skc8,skc14) ),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f76,negated_conjecture,(
% 0.13/0.43 event(skc8,skc13) ),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f77,negated_conjecture,(
% 0.13/0.43 present(skc8,skc13) ),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f78,negated_conjecture,(
% 0.13/0.43 think_believe_consider(skc8,skc13) ),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f79,negated_conjecture,(
% 0.13/0.43 jules_forename(skc8,skc11) ),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f81,negated_conjecture,(
% 0.13/0.43 man(skc8,skc10) ),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f82,negated_conjecture,(
% 0.13/0.43 state(skc8,skc9) ),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f83,negated_conjecture,(
% 0.13/0.43 accessible_world(skc8,skc12) ),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f84,negated_conjecture,(
% 0.13/0.43 proposition(skc8,skc12) ),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f85,negated_conjecture,(
% 0.13/0.43 of(skc8,skc14,skc15) ),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f86,negated_conjecture,(
% 0.13/0.43 agent(skc8,skc13,skc15) ),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f87,negated_conjecture,(
% 0.13/0.43 theme(skc8,skc13,skc12) ),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f88,negated_conjecture,(
% 0.13/0.43 of(skc8,skc11,skc10) ),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f89,negated_conjecture,(
% 0.13/0.43 be(skc8,skc9,skc10,skc10) ),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f90,negated_conjecture,(
% 0.13/0.43 (![U,V]: (( ~ man(skc12,U)| smoke(skc12,skf2(V)) ) ))),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f91,negated_conjecture,(
% 0.13/0.43 (![U,V]: (( ~ man(skc12,U)| present(skc12,skf2(V)) ) ))),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f92,negated_conjecture,(
% 0.13/0.43 (![U,V]: (( ~ man(skc12,U)| event(skc12,skf2(V)) ) ))),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f93,negated_conjecture,(
% 0.13/0.43 (![U]: (( ~ man(skc12,U)| agent(skc12,skf2(U),U) ) ))),
% 0.13/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f94,negated_conjecture,(
% 0.13/0.43 (![U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7]: (( ~ state(U,V)| ~ be(U,V,W,W)| ~ man(U,W)| ~ of(U,X,W)| ~ jules_forename(U,X)| ~ forename(U,X)| ~ jules_forename(U,Y)| ~ forename(U,Y)| ~ smoke(Z,X1)| ~ present(Z,X1)| ~ agent(Z,X1,X2)| ~ event(Z,X1)| ~ man(U,X2)| ~ of(U,Y,X2)| ~ proposition(U,Z)| ~ accessible_world(U,Z)| ~ accessible_world(U,X3)| ~ proposition(U,X3)| ~ theme(U,X4,X3)| ~ event(U,X4)| ~ present(U,X4)| ~ think_believe_consider(U,X4)| ~ man(U,X5)| ~ agent(U,X4,X5)| ~ agent(U,X6,X5)| ~ forename(U,X7)| ~ vincent_forename(U,X7)| ~ of(U,X7,X5)| ~ think_believe_consider(U,X6)| ~ present(U,X6)| ~ event(U,X6)| ~ theme(U,X6,Z)| ~ actual_world(U)| man(X3,skf4(X3)) ) ))),
% 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]: (( ~ state(U,V)| ~ be(U,V,W,W)| ~ man(U,W)| ~ of(U,X,W)| ~ jules_forename(U,X)| ~ forename(U,X)| ~ jules_forename(U,Y)| ~ forename(U,Y)| ~ smoke(Z,X1)| ~ present(Z,X1)| ~ agent(Z,X1,X2)| ~ event(Z,X1)| ~ man(U,X2)| ~ of(U,Y,X2)| ~ proposition(U,Z)| ~ accessible_world(U,Z)| ~ smoke(X3,X4)| ~ present(X3,X4)| ~ agent(X3,X4,skf4(X3))| ~ event(X3,X4)| ~ accessible_world(U,X3)| ~ proposition(U,X3)| ~ theme(U,X5,X3)| ~ event(U,X5)| ~ present(U,X5)| ~ think_believe_consider(U,X5)| ~ man(U,X6)| ~ agent(U,X5,X6)| ~ agent(U,X7,X6)| ~ forename(U,X8)| ~ vincent_forename(U,X8)| ~ of(U,X8,X6)| ~ think_believe_consider(U,X7)| ~ present(U,X7)| ~ event(U,X7)| ~ theme(U,X7,Z)| ~ actual_world(U) ) ))),
% 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(f206,plain,(
% 0.13/0.43 forename(skc8,skc14)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f74])).
% 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(f226,plain,(
% 0.13/0.43 (![U]: ~man(skc12,U))|(![V]: event(skc12,skf2(V)))),
% 0.13/0.43 inference(miniscoping,[status(thm)],[f92])).
% 0.13/0.43 fof(f227,plain,(
% 0.13/0.43 ![X0,X1]: (~man(skc12,X0)|event(skc12,skf2(X1)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f226])).
% 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 ![X3]: ((![U]: ((![Z,X6]: (((((![X5,X7]: (((((![X4]: (((((((((((![Y,X2]: (((![X1]: (((((((![X]: (((![W]: (((![V]: (~state(U,V)|~be(U,V,W,W)))|~man(U,W))|~of(U,X,W)))|~jules_forename(U,X))|~forename(U,X)))|~jules_forename(U,Y))|~forename(U,Y))|~smoke(Z,X1))|~present(Z,X1))|~agent(Z,X1,X2))|~event(Z,X1)))|~man(U,X2))|~of(U,Y,X2)))|~proposition(U,Z))|~accessible_world(U,Z))|~accessible_world(U,X3))|~proposition(U,X3))|~theme(U,X4,X3))|~event(U,X4))|~present(U,X4))|~think_believe_consider(U,X4))|~man(U,X5))|~agent(U,X4,X5)))|~agent(U,X6,X5))|~forename(U,X7))|~vincent_forename(U,X7))|~of(U,X7,X5)))|~think_believe_consider(U,X6))|~present(U,X6))|~event(U,X6))|~theme(U,X6,Z)))|~actual_world(U)))|man(X3,skf4(X3)))),
% 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]: (~state(X0,X1)|~be(X0,X1,X2,X2)|~man(X0,X2)|~of(X0,X3,X2)|~jules_forename(X0,X3)|~forename(X0,X3)|~jules_forename(X0,X4)|~forename(X0,X4)|~smoke(X5,X6)|~present(X5,X6)|~agent(X5,X6,X7)|~event(X5,X6)|~man(X0,X7)|~of(X0,X4,X7)|~proposition(X0,X5)|~accessible_world(X0,X5)|~accessible_world(X0,X8)|~proposition(X0,X8)|~theme(X0,X9,X8)|~event(X0,X9)|~present(X0,X9)|~think_believe_consider(X0,X9)|~man(X0,X10)|~agent(X0,X9,X10)|~agent(X0,X11,X10)|~forename(X0,X12)|~vincent_forename(X0,X12)|~of(X0,X12,X10)|~think_believe_consider(X0,X11)|~present(X0,X11)|~event(X0,X11)|~theme(X0,X11,X5)|~actual_world(X0)|man(X8,skf4(X8)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f229])).
% 0.13/0.43 fof(f231,plain,(
% 0.13/0.43 ![U]: ((![Z,X7]: (((((![X6,X8]: (((((![X5]: ((((((![X3]: ((((![X4]: (((((((![Y,X2]: (((![X1]: (((((((![X]: (((![W]: (((![V]: (~state(U,V)|~be(U,V,W,W)))|~man(U,W))|~of(U,X,W)))|~jules_forename(U,X))|~forename(U,X)))|~jules_forename(U,Y))|~forename(U,Y))|~smoke(Z,X1))|~present(Z,X1))|~agent(Z,X1,X2))|~event(Z,X1)))|~man(U,X2))|~of(U,Y,X2)))|~proposition(U,Z))|~accessible_world(U,Z))|~smoke(X3,X4))|~present(X3,X4))|~agent(X3,X4,skf4(X3)))|~event(X3,X4)))|~accessible_world(U,X3))|~proposition(U,X3))|~theme(U,X5,X3)))|~event(U,X5))|~present(U,X5))|~think_believe_consider(U,X5))|~man(U,X6))|~agent(U,X5,X6)))|~agent(U,X7,X6))|~forename(U,X8))|~vincent_forename(U,X8))|~of(U,X8,X6)))|~think_believe_consider(U,X7))|~present(U,X7))|~event(U,X7))|~theme(U,X7,Z)))|~actual_world(U))),
% 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]: (~state(X0,X1)|~be(X0,X1,X2,X2)|~man(X0,X2)|~of(X0,X3,X2)|~jules_forename(X0,X3)|~forename(X0,X3)|~jules_forename(X0,X4)|~forename(X0,X4)|~smoke(X5,X6)|~present(X5,X6)|~agent(X5,X6,X7)|~event(X5,X6)|~man(X0,X7)|~of(X0,X4,X7)|~proposition(X0,X5)|~accessible_world(X0,X5)|~smoke(X8,X9)|~present(X8,X9)|~agent(X8,X9,skf4(X8))|~event(X8,X9)|~accessible_world(X0,X8)|~proposition(X0,X8)|~theme(X0,X10,X8)|~event(X0,X10)|~present(X0,X10)|~think_believe_consider(X0,X10)|~man(X0,X11)|~agent(X0,X10,X11)|~agent(X0,X12,X11)|~forename(X0,X13)|~vincent_forename(X0,X13)|~of(X0,X13,X11)|~think_believe_consider(X0,X12)|~present(X0,X12)|~event(X0,X12)|~theme(X0,X12,X5)|~actual_world(X0))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f231])).
% 0.13/0.43 fof(f289,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(f358,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~state(X0,X1)|~be(X0,X1,X2,X2)|~man(X0,X2)|~of(X0,X3,X2)|~jules_forename(X0,X3)|~jules_forename(X0,X4)|~forename(X0,X4)|~smoke(X5,X6)|~present(X5,X6)|~agent(X5,X6,X7)|~event(X5,X6)|~man(X0,X7)|~of(X0,X4,X7)|~proposition(X0,X5)|~accessible_world(X0,X5)|~accessible_world(X0,X8)|~proposition(X0,X8)|~theme(X0,X9,X8)|~event(X0,X9)|~present(X0,X9)|~think_believe_consider(X0,X9)|~man(X0,X10)|~agent(X0,X9,X10)|~agent(X0,X11,X10)|~forename(X0,X12)|~vincent_forename(X0,X12)|~of(X0,X12,X10)|~think_believe_consider(X0,X11)|~present(X0,X11)|~event(X0,X11)|~theme(X0,X11,X5)|~actual_world(X0)|man(X8,skf4(X8)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f230,f125])).
% 0.13/0.43 fof(f359,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~state(skc8,skc9)|~man(skc8,skc10)|~of(skc8,X0,skc10)|~jules_forename(skc8,X0)|~jules_forename(skc8,X1)|~forename(skc8,X1)|~smoke(X2,X3)|~present(X2,X3)|~agent(X2,X3,X4)|~event(X2,X3)|~man(skc8,X4)|~of(skc8,X1,X4)|~proposition(skc8,X2)|~accessible_world(skc8,X2)|~accessible_world(skc8,X5)|~proposition(skc8,X5)|~theme(skc8,X6,X5)|~event(skc8,X6)|~present(skc8,X6)|~think_believe_consider(skc8,X6)|~man(skc8,X7)|~agent(skc8,X6,X7)|~agent(skc8,X8,X7)|~forename(skc8,X9)|~vincent_forename(skc8,X9)|~of(skc8,X9,X7)|~think_believe_consider(skc8,X8)|~present(skc8,X8)|~event(skc8,X8)|~theme(skc8,X8,X2)|~actual_world(skc8)|man(X5,skf4(X5)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f358,f221])).
% 0.13/0.43 fof(f360,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~man(skc8,skc10)|~of(skc8,X0,skc10)|~jules_forename(skc8,X0)|~jules_forename(skc8,X1)|~forename(skc8,X1)|~smoke(X2,X3)|~present(X2,X3)|~agent(X2,X3,X4)|~event(X2,X3)|~man(skc8,X4)|~of(skc8,X1,X4)|~proposition(skc8,X2)|~accessible_world(skc8,X2)|~accessible_world(skc8,X5)|~proposition(skc8,X5)|~theme(skc8,X6,X5)|~event(skc8,X6)|~present(skc8,X6)|~think_believe_consider(skc8,X6)|~man(skc8,X7)|~agent(skc8,X6,X7)|~agent(skc8,X8,X7)|~forename(skc8,X9)|~vincent_forename(skc8,X9)|~of(skc8,X9,X7)|~think_believe_consider(skc8,X8)|~present(skc8,X8)|~event(skc8,X8)|~theme(skc8,X8,X2)|~actual_world(skc8)|man(X5,skf4(X5)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f359,f214])).
% 0.13/0.43 fof(f364,plain,(
% 0.13/0.43 man(skc12,skc10)),
% 0.13/0.43 inference(resolution,[status(thm)],[f289,f213])).
% 0.13/0.43 fof(f366,plain,(
% 0.13/0.43 agent(skc12,skf2(skc10),skc10)),
% 0.13/0.43 inference(resolution,[status(thm)],[f364,f228])).
% 0.13/0.43 fof(f367,plain,(
% 0.13/0.43 ![X0]: (event(skc12,skf2(X0)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f364,f227])).
% 0.13/0.43 fof(f368,plain,(
% 0.13/0.43 ![X0]: (present(skc12,skf2(X0)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f364,f225])).
% 0.13/0.43 fof(f369,plain,(
% 0.13/0.43 ![X0]: (smoke(skc12,skf2(X0)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f364,f223])).
% 0.13/0.43 fof(f372,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~state(X0,X1)|~be(X0,X1,X2,X2)|~man(X0,X2)|~of(X0,X3,X2)|~jules_forename(X0,X3)|~jules_forename(X0,X4)|~forename(X0,X4)|~smoke(X5,X6)|~present(X5,X6)|~agent(X5,X6,X7)|~event(X5,X6)|~man(X0,X7)|~of(X0,X4,X7)|~proposition(X0,X5)|~accessible_world(X0,X5)|~smoke(X8,X9)|~present(X8,X9)|~agent(X8,X9,skf4(X8))|~event(X8,X9)|~accessible_world(X0,X8)|~proposition(X0,X8)|~theme(X0,X10,X8)|~event(X0,X10)|~present(X0,X10)|~think_believe_consider(X0,X10)|~man(X0,X11)|~agent(X0,X10,X11)|~agent(X0,X12,X11)|~forename(X0,X13)|~vincent_forename(X0,X13)|~of(X0,X13,X11)|~think_believe_consider(X0,X12)|~present(X0,X12)|~event(X0,X12)|~theme(X0,X12,X5)|~actual_world(X0))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f232,f125])).
% 0.13/0.43 fof(f373,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~state(skc8,skc9)|~man(skc8,skc10)|~of(skc8,X0,skc10)|~jules_forename(skc8,X0)|~jules_forename(skc8,X1)|~forename(skc8,X1)|~smoke(X2,X3)|~present(X2,X3)|~agent(X2,X3,X4)|~event(X2,X3)|~man(skc8,X4)|~of(skc8,X1,X4)|~proposition(skc8,X2)|~accessible_world(skc8,X2)|~smoke(X5,X6)|~present(X5,X6)|~agent(X5,X6,skf4(X5))|~event(X5,X6)|~accessible_world(skc8,X5)|~proposition(skc8,X5)|~theme(skc8,X7,X5)|~event(skc8,X7)|~present(skc8,X7)|~think_believe_consider(skc8,X7)|~man(skc8,X8)|~agent(skc8,X7,X8)|~agent(skc8,X9,X8)|~forename(skc8,X10)|~vincent_forename(skc8,X10)|~of(skc8,X10,X8)|~think_believe_consider(skc8,X9)|~present(skc8,X9)|~event(skc8,X9)|~theme(skc8,X9,X2)|~actual_world(skc8))),
% 0.13/0.43 inference(resolution,[status(thm)],[f372,f221])).
% 0.13/0.43 fof(f374,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~man(skc8,skc10)|~of(skc8,X0,skc10)|~jules_forename(skc8,X0)|~jules_forename(skc8,X1)|~forename(skc8,X1)|~smoke(X2,X3)|~present(X2,X3)|~agent(X2,X3,X4)|~event(X2,X3)|~man(skc8,X4)|~of(skc8,X1,X4)|~proposition(skc8,X2)|~accessible_world(skc8,X2)|~smoke(X5,X6)|~present(X5,X6)|~agent(X5,X6,skf4(X5))|~event(X5,X6)|~accessible_world(skc8,X5)|~proposition(skc8,X5)|~theme(skc8,X7,X5)|~event(skc8,X7)|~present(skc8,X7)|~think_believe_consider(skc8,X7)|~man(skc8,X8)|~agent(skc8,X7,X8)|~agent(skc8,X9,X8)|~forename(skc8,X10)|~vincent_forename(skc8,X10)|~of(skc8,X10,X8)|~think_believe_consider(skc8,X9)|~present(skc8,X9)|~event(skc8,X9)|~theme(skc8,X9,X2)|~actual_world(skc8))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f373,f214])).
% 0.13/0.43 fof(f492,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~of(skc8,X0,skc10)|~jules_forename(skc8,X0)|~jules_forename(skc8,X1)|~forename(skc8,X1)|~smoke(X2,X3)|~present(X2,X3)|~agent(X2,X3,X4)|~event(X2,X3)|~man(skc8,X4)|~of(skc8,X1,X4)|~proposition(skc8,X2)|~accessible_world(skc8,X2)|~accessible_world(skc8,X5)|~proposition(skc8,X5)|~theme(skc8,X6,X5)|~event(skc8,X6)|~present(skc8,X6)|~think_believe_consider(skc8,X6)|~man(skc8,X7)|~agent(skc8,X6,X7)|~agent(skc8,X8,X7)|~forename(skc8,X9)|~vincent_forename(skc8,X9)|~of(skc8,X9,X7)|~think_believe_consider(skc8,X8)|~present(skc8,X8)|~event(skc8,X8)|~theme(skc8,X8,X2)|~actual_world(skc8)|man(X5,skf4(X5)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f360,f213])).
% 0.13/0.43 fof(f493,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~jules_forename(skc8,skc11)|~jules_forename(skc8,X0)|~forename(skc8,X0)|~smoke(X1,X2)|~present(X1,X2)|~agent(X1,X2,X3)|~event(X1,X2)|~man(skc8,X3)|~of(skc8,X0,X3)|~proposition(skc8,X1)|~accessible_world(skc8,X1)|~accessible_world(skc8,X4)|~proposition(skc8,X4)|~theme(skc8,X5,X4)|~event(skc8,X5)|~present(skc8,X5)|~think_believe_consider(skc8,X5)|~man(skc8,X6)|~agent(skc8,X5,X6)|~agent(skc8,X7,X6)|~forename(skc8,X8)|~vincent_forename(skc8,X8)|~of(skc8,X8,X6)|~think_believe_consider(skc8,X7)|~present(skc8,X7)|~event(skc8,X7)|~theme(skc8,X7,X1)|~actual_world(skc8)|man(X4,skf4(X4)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f492,f220])).
% 0.13/0.43 fof(f494,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~jules_forename(skc8,X0)|~forename(skc8,X0)|~smoke(X1,X2)|~present(X1,X2)|~agent(X1,X2,X3)|~event(X1,X2)|~man(skc8,X3)|~of(skc8,X0,X3)|~proposition(skc8,X1)|~accessible_world(skc8,X1)|~accessible_world(skc8,X4)|~proposition(skc8,X4)|~theme(skc8,X5,X4)|~event(skc8,X5)|~present(skc8,X5)|~think_believe_consider(skc8,X5)|~man(skc8,X6)|~agent(skc8,X5,X6)|~agent(skc8,X7,X6)|~forename(skc8,X8)|~vincent_forename(skc8,X8)|~of(skc8,X8,X6)|~think_believe_consider(skc8,X7)|~present(skc8,X7)|~event(skc8,X7)|~theme(skc8,X7,X1)|~actual_world(skc8)|man(X4,skf4(X4)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f493,f211])).
% 0.13/0.43 fof(f495,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~of(skc8,X0,skc10)|~jules_forename(skc8,X0)|~jules_forename(skc8,X1)|~forename(skc8,X1)|~smoke(X2,X3)|~present(X2,X3)|~agent(X2,X3,X4)|~event(X2,X3)|~man(skc8,X4)|~of(skc8,X1,X4)|~proposition(skc8,X2)|~accessible_world(skc8,X2)|~smoke(X5,X6)|~present(X5,X6)|~agent(X5,X6,skf4(X5))|~event(X5,X6)|~accessible_world(skc8,X5)|~proposition(skc8,X5)|~theme(skc8,X7,X5)|~event(skc8,X7)|~present(skc8,X7)|~think_believe_consider(skc8,X7)|~man(skc8,X8)|~agent(skc8,X7,X8)|~agent(skc8,X9,X8)|~forename(skc8,X10)|~vincent_forename(skc8,X10)|~of(skc8,X10,X8)|~think_believe_consider(skc8,X9)|~present(skc8,X9)|~event(skc8,X9)|~theme(skc8,X9,X2)|~actual_world(skc8))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f374,f213])).
% 0.13/0.43 fof(f496,plain,(
% 0.13/0.43 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~jules_forename(skc8,skc11)|~jules_forename(skc8,X0)|~forename(skc8,X0)|~smoke(X1,X2)|~present(X1,X2)|~agent(X1,X2,X3)|~event(X1,X2)|~man(skc8,X3)|~of(skc8,X0,X3)|~proposition(skc8,X1)|~accessible_world(skc8,X1)|~smoke(X4,X5)|~present(X4,X5)|~agent(X4,X5,skf4(X4))|~event(X4,X5)|~accessible_world(skc8,X4)|~proposition(skc8,X4)|~theme(skc8,X6,X4)|~event(skc8,X6)|~present(skc8,X6)|~think_believe_consider(skc8,X6)|~man(skc8,X7)|~agent(skc8,X6,X7)|~agent(skc8,X8,X7)|~forename(skc8,X9)|~vincent_forename(skc8,X9)|~of(skc8,X9,X7)|~think_believe_consider(skc8,X8)|~present(skc8,X8)|~event(skc8,X8)|~theme(skc8,X8,X1)|~actual_world(skc8))),
% 0.13/0.44 inference(resolution,[status(thm)],[f495,f220])).
% 0.13/0.44 fof(f497,plain,(
% 0.13/0.44 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~jules_forename(skc8,X0)|~forename(skc8,X0)|~smoke(X1,X2)|~present(X1,X2)|~agent(X1,X2,X3)|~event(X1,X2)|~man(skc8,X3)|~of(skc8,X0,X3)|~proposition(skc8,X1)|~accessible_world(skc8,X1)|~smoke(X4,X5)|~present(X4,X5)|~agent(X4,X5,skf4(X4))|~event(X4,X5)|~accessible_world(skc8,X4)|~proposition(skc8,X4)|~theme(skc8,X6,X4)|~event(skc8,X6)|~present(skc8,X6)|~think_believe_consider(skc8,X6)|~man(skc8,X7)|~agent(skc8,X6,X7)|~agent(skc8,X8,X7)|~forename(skc8,X9)|~vincent_forename(skc8,X9)|~of(skc8,X9,X7)|~think_believe_consider(skc8,X8)|~present(skc8,X8)|~event(skc8,X8)|~theme(skc8,X8,X1)|~actual_world(skc8))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f496,f211])).
% 0.13/0.44 fof(f538,plain,(
% 0.13/0.44 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~jules_forename(skc8,X0)|~smoke(X1,X2)|~present(X1,X2)|~agent(X1,X2,X3)|~event(X1,X2)|~man(skc8,X3)|~of(skc8,X0,X3)|~proposition(skc8,X1)|~accessible_world(skc8,X1)|~accessible_world(skc8,X4)|~proposition(skc8,X4)|~theme(skc8,X5,X4)|~event(skc8,X5)|~present(skc8,X5)|~think_believe_consider(skc8,X5)|~man(skc8,X6)|~agent(skc8,X5,X6)|~agent(skc8,X7,X6)|~forename(skc8,X8)|~vincent_forename(skc8,X8)|~of(skc8,X8,X6)|~think_believe_consider(skc8,X7)|~present(skc8,X7)|~event(skc8,X7)|~theme(skc8,X7,X1)|~actual_world(skc8)|man(X4,skf4(X4)))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f494,f125])).
% 0.13/0.44 fof(f540,plain,(
% 0.13/0.44 ![X0,X1,X2,X3,X4,X5]: (~jules_forename(skc8,X0)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~event(skc12,skf2(skc10))|~man(skc8,skc10)|~of(skc8,X0,skc10)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~accessible_world(skc8,X1)|~proposition(skc8,X1)|~theme(skc8,X2,X1)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~man(skc8,X3)|~agent(skc8,X2,X3)|~agent(skc8,X4,X3)|~forename(skc8,X5)|~vincent_forename(skc8,X5)|~of(skc8,X5,X3)|~think_believe_consider(skc8,X4)|~present(skc8,X4)|~event(skc8,X4)|~theme(skc8,X4,skc12)|~actual_world(skc8)|man(X1,skf4(X1)))),
% 0.13/0.44 inference(resolution,[status(thm)],[f538,f366])).
% 0.13/0.44 fof(f544,plain,(
% 0.13/0.44 ![X0,X1,X2,X3,X4,X5]: (~jules_forename(skc8,X0)|~present(skc12,skf2(skc10))|~event(skc12,skf2(skc10))|~man(skc8,skc10)|~of(skc8,X0,skc10)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~accessible_world(skc8,X1)|~proposition(skc8,X1)|~theme(skc8,X2,X1)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~man(skc8,X3)|~agent(skc8,X2,X3)|~agent(skc8,X4,X3)|~forename(skc8,X5)|~vincent_forename(skc8,X5)|~of(skc8,X5,X3)|~think_believe_consider(skc8,X4)|~present(skc8,X4)|~event(skc8,X4)|~theme(skc8,X4,skc12)|~actual_world(skc8)|man(X1,skf4(X1)))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f540,f369])).
% 0.13/0.44 fof(f547,plain,(
% 0.13/0.44 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~jules_forename(skc8,X0)|~smoke(X1,X2)|~present(X1,X2)|~agent(X1,X2,X3)|~event(X1,X2)|~man(skc8,X3)|~of(skc8,X0,X3)|~proposition(skc8,X1)|~accessible_world(skc8,X1)|~smoke(X4,X5)|~present(X4,X5)|~agent(X4,X5,skf4(X4))|~event(X4,X5)|~accessible_world(skc8,X4)|~proposition(skc8,X4)|~theme(skc8,X6,X4)|~event(skc8,X6)|~present(skc8,X6)|~think_believe_consider(skc8,X6)|~man(skc8,X7)|~agent(skc8,X6,X7)|~agent(skc8,X8,X7)|~forename(skc8,X9)|~vincent_forename(skc8,X9)|~of(skc8,X9,X7)|~think_believe_consider(skc8,X8)|~present(skc8,X8)|~event(skc8,X8)|~theme(skc8,X8,X1)|~actual_world(skc8))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f497,f125])).
% 0.13/0.44 fof(f549,plain,(
% 0.13/0.44 ![X0,X1,X2,X3,X4,X5,X6]: (~jules_forename(skc8,X0)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~event(skc12,skf2(skc10))|~man(skc8,skc10)|~of(skc8,X0,skc10)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~smoke(X1,X2)|~present(X1,X2)|~agent(X1,X2,skf4(X1))|~event(X1,X2)|~accessible_world(skc8,X1)|~proposition(skc8,X1)|~theme(skc8,X3,X1)|~event(skc8,X3)|~present(skc8,X3)|~think_believe_consider(skc8,X3)|~man(skc8,X4)|~agent(skc8,X3,X4)|~agent(skc8,X5,X4)|~forename(skc8,X6)|~vincent_forename(skc8,X6)|~of(skc8,X6,X4)|~think_believe_consider(skc8,X5)|~present(skc8,X5)|~event(skc8,X5)|~theme(skc8,X5,skc12)|~actual_world(skc8))),
% 0.13/0.44 inference(resolution,[status(thm)],[f547,f366])).
% 0.13/0.44 fof(f553,plain,(
% 0.13/0.44 ![X0,X1,X2,X3,X4,X5,X6]: (~jules_forename(skc8,X0)|~present(skc12,skf2(skc10))|~event(skc12,skf2(skc10))|~man(skc8,skc10)|~of(skc8,X0,skc10)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~smoke(X1,X2)|~present(X1,X2)|~agent(X1,X2,skf4(X1))|~event(X1,X2)|~accessible_world(skc8,X1)|~proposition(skc8,X1)|~theme(skc8,X3,X1)|~event(skc8,X3)|~present(skc8,X3)|~think_believe_consider(skc8,X3)|~man(skc8,X4)|~agent(skc8,X3,X4)|~agent(skc8,X5,X4)|~forename(skc8,X6)|~vincent_forename(skc8,X6)|~of(skc8,X6,X4)|~think_believe_consider(skc8,X5)|~present(skc8,X5)|~event(skc8,X5)|~theme(skc8,X5,skc12)|~actual_world(skc8))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f549,f369])).
% 0.13/0.44 fof(f624,plain,(
% 0.13/0.44 ![X0,X1,X2,X3,X4,X5]: (~jules_forename(skc8,X0)|~event(skc12,skf2(skc10))|~man(skc8,skc10)|~of(skc8,X0,skc10)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~accessible_world(skc8,X1)|~proposition(skc8,X1)|~theme(skc8,X2,X1)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~man(skc8,X3)|~agent(skc8,X2,X3)|~agent(skc8,X4,X3)|~forename(skc8,X5)|~vincent_forename(skc8,X5)|~of(skc8,X5,X3)|~think_believe_consider(skc8,X4)|~present(skc8,X4)|~event(skc8,X4)|~theme(skc8,X4,skc12)|~actual_world(skc8)|man(X1,skf4(X1)))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f544,f368])).
% 0.13/0.44 fof(f625,plain,(
% 0.13/0.44 ![X0,X1,X2,X3,X4]: (~jules_forename(skc8,skc11)|~event(skc12,skf2(skc10))|~man(skc8,skc10)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X1,X0)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~man(skc8,X2)|~agent(skc8,X1,X2)|~agent(skc8,X3,X2)|~forename(skc8,X4)|~vincent_forename(skc8,X4)|~of(skc8,X4,X2)|~think_believe_consider(skc8,X3)|~present(skc8,X3)|~event(skc8,X3)|~theme(skc8,X3,skc12)|~actual_world(skc8)|man(X0,skf4(X0)))),
% 0.13/0.44 inference(resolution,[status(thm)],[f624,f220])).
% 0.13/0.44 fof(f626,plain,(
% 0.13/0.44 ![X0,X1,X2,X3,X4]: (~event(skc12,skf2(skc10))|~man(skc8,skc10)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X1,X0)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~man(skc8,X2)|~agent(skc8,X1,X2)|~agent(skc8,X3,X2)|~forename(skc8,X4)|~vincent_forename(skc8,X4)|~of(skc8,X4,X2)|~think_believe_consider(skc8,X3)|~present(skc8,X3)|~event(skc8,X3)|~theme(skc8,X3,skc12)|~actual_world(skc8)|man(X0,skf4(X0)))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f625,f211])).
% 0.13/0.44 fof(f630,plain,(
% 0.13/0.44 ![X0,X1,X2,X3,X4,X5,X6]: (~jules_forename(skc8,X0)|~event(skc12,skf2(skc10))|~man(skc8,skc10)|~of(skc8,X0,skc10)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~smoke(X1,X2)|~present(X1,X2)|~agent(X1,X2,skf4(X1))|~event(X1,X2)|~accessible_world(skc8,X1)|~proposition(skc8,X1)|~theme(skc8,X3,X1)|~event(skc8,X3)|~present(skc8,X3)|~think_believe_consider(skc8,X3)|~man(skc8,X4)|~agent(skc8,X3,X4)|~agent(skc8,X5,X4)|~forename(skc8,X6)|~vincent_forename(skc8,X6)|~of(skc8,X6,X4)|~think_believe_consider(skc8,X5)|~present(skc8,X5)|~event(skc8,X5)|~theme(skc8,X5,skc12)|~actual_world(skc8))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f553,f368])).
% 0.13/0.44 fof(f631,plain,(
% 0.13/0.44 ![X0,X1,X2,X3,X4,X5]: (~jules_forename(skc8,skc11)|~event(skc12,skf2(skc10))|~man(skc8,skc10)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~event(X0,X1)|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X2,X0)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~man(skc8,X3)|~agent(skc8,X2,X3)|~agent(skc8,X4,X3)|~forename(skc8,X5)|~vincent_forename(skc8,X5)|~of(skc8,X5,X3)|~think_believe_consider(skc8,X4)|~present(skc8,X4)|~event(skc8,X4)|~theme(skc8,X4,skc12)|~actual_world(skc8))),
% 0.13/0.44 inference(resolution,[status(thm)],[f630,f220])).
% 0.13/0.44 fof(f632,plain,(
% 0.13/0.44 ![X0,X1,X2,X3,X4,X5]: (~event(skc12,skf2(skc10))|~man(skc8,skc10)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~event(X0,X1)|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X2,X0)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~man(skc8,X3)|~agent(skc8,X2,X3)|~agent(skc8,X4,X3)|~forename(skc8,X5)|~vincent_forename(skc8,X5)|~of(skc8,X5,X3)|~think_believe_consider(skc8,X4)|~present(skc8,X4)|~event(skc8,X4)|~theme(skc8,X4,skc12)|~actual_world(skc8))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f631,f211])).
% 0.13/0.44 fof(f633,plain,(
% 0.13/0.44 ![X0,X1,X2,X3,X4]: (~man(skc8,skc10)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~theme(skc8,X1,X0)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~man(skc8,X2)|~agent(skc8,X1,X2)|~agent(skc8,X3,X2)|~forename(skc8,X4)|~vincent_forename(skc8,X4)|~of(skc8,X4,X2)|~think_believe_consider(skc8,X3)|~present(skc8,X3)|~event(skc8,X3)|~theme(skc8,X3,skc12)|~actual_world(skc8)|man(X0,skf4(X0)))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f626,f367])).
% 0.13/0.44 fof(f634,plain,(
% 0.13/0.44 ![X0,X1,X2]: (~man(skc8,skc10)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~man(skc8,X0)|~agent(skc8,skc13,X0)|~agent(skc8,X1,X0)|~forename(skc8,X2)|~vincent_forename(skc8,X2)|~of(skc8,X2,X0)|~think_believe_consider(skc8,X1)|~present(skc8,X1)|~event(skc8,X1)|~theme(skc8,X1,skc12)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.44 inference(resolution,[status(thm)],[f633,f219])).
% 0.13/0.44 fof(f635,plain,(
% 0.13/0.44 ![X0,X1,X2]: (~man(skc8,skc10)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~man(skc8,X0)|~agent(skc8,skc13,X0)|~agent(skc8,X1,X0)|~forename(skc8,X2)|~vincent_forename(skc8,X2)|~of(skc8,X2,X0)|~think_believe_consider(skc8,X1)|~present(skc8,X1)|~event(skc8,X1)|~theme(skc8,X1,skc12)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.44 inference(duplicate_literals_removal,[status(thm)],[f634])).
% 0.13/0.44 fof(f636,plain,(
% 0.13/0.44 ![X0,X1,X2]: (~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~man(skc8,X0)|~agent(skc8,skc13,X0)|~agent(skc8,X1,X0)|~forename(skc8,X2)|~vincent_forename(skc8,X2)|~of(skc8,X2,X0)|~think_believe_consider(skc8,X1)|~present(skc8,X1)|~event(skc8,X1)|~theme(skc8,X1,skc12)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f635,f213])).
% 0.13/0.44 fof(f637,plain,(
% 0.13/0.44 ![X0,X1,X2]: (~accessible_world(skc8,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~man(skc8,X0)|~agent(skc8,skc13,X0)|~agent(skc8,X1,X0)|~forename(skc8,X2)|~vincent_forename(skc8,X2)|~of(skc8,X2,X0)|~think_believe_consider(skc8,X1)|~present(skc8,X1)|~event(skc8,X1)|~theme(skc8,X1,skc12)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f636,f216])).
% 0.13/0.44 fof(f638,plain,(
% 0.13/0.44 ![X0]: (~accessible_world(skc8,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~man(skc8,skc15)|~agent(skc8,skc13,skc15)|~forename(skc8,X0)|~vincent_forename(skc8,X0)|~of(skc8,X0,skc15)|~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~theme(skc8,skc13,skc12)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.44 inference(resolution,[status(thm)],[f637,f218])).
% 0.13/0.44 fof(f639,plain,(
% 0.13/0.44 ![X0]: (~accessible_world(skc8,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~man(skc8,skc15)|~agent(skc8,skc13,skc15)|~forename(skc8,X0)|~vincent_forename(skc8,X0)|~of(skc8,X0,skc15)|~theme(skc8,skc13,skc12)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.44 inference(duplicate_literals_removal,[status(thm)],[f638])).
% 0.13/0.44 fof(f640,plain,(
% 0.13/0.44 ![X0]: (~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~man(skc8,skc15)|~agent(skc8,skc13,skc15)|~forename(skc8,X0)|~vincent_forename(skc8,X0)|~of(skc8,X0,skc15)|~theme(skc8,skc13,skc12)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f639,f215])).
% 0.13/0.44 fof(f650,plain,(
% 0.13/0.44 ![X0]: (~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~man(skc8,skc15)|~agent(skc8,skc13,skc15)|~forename(skc8,X0)|~vincent_forename(skc8,X0)|~of(skc8,X0,skc15)|~theme(skc8,skc13,skc12)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f640,f208])).
% 0.13/0.44 fof(f651,plain,(
% 0.13/0.44 ~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~man(skc8,skc15)|~agent(skc8,skc13,skc15)|~forename(skc8,skc14)|~vincent_forename(skc8,skc14)|~theme(skc8,skc13,skc12)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.44 inference(resolution,[status(thm)],[f650,f217])).
% 0.13/0.44 fof(f652,plain,(
% 0.13/0.44 ~think_believe_consider(skc8,skc13)|~man(skc8,skc15)|~agent(skc8,skc13,skc15)|~forename(skc8,skc14)|~vincent_forename(skc8,skc14)|~theme(skc8,skc13,skc12)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f651,f209])).
% 0.13/0.44 fof(f653,plain,(
% 0.13/0.44 ~man(skc8,skc15)|~agent(skc8,skc13,skc15)|~forename(skc8,skc14)|~vincent_forename(skc8,skc14)|~theme(skc8,skc13,skc12)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f652,f210])).
% 0.13/0.44 fof(f654,plain,(
% 0.13/0.44 ~man(skc8,skc15)|~agent(skc8,skc13,skc15)|~forename(skc8,skc14)|~vincent_forename(skc8,skc14)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.44 inference(resolution,[status(thm)],[f653,f219])).
% 0.13/0.44 fof(f655,plain,(
% 0.13/0.44 ~agent(skc8,skc13,skc15)|~forename(skc8,skc14)|~vincent_forename(skc8,skc14)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f654,f205])).
% 0.13/0.44 fof(f656,plain,(
% 0.13/0.44 ~forename(skc8,skc14)|~vincent_forename(skc8,skc14)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f655,f218])).
% 0.13/0.44 fof(f657,plain,(
% 0.13/0.44 ~forename(skc8,skc14)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.44 inference(resolution,[status(thm)],[f656,f207])).
% 0.13/0.44 fof(f658,plain,(
% 0.13/0.44 ~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f657,f206])).
% 0.13/0.44 fof(f659,plain,(
% 0.13/0.44 man(skc12,skf4(skc12))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f658,f204])).
% 0.13/0.44 fof(f660,plain,(
% 0.13/0.44 agent(skc12,skf2(skf4(skc12)),skf4(skc12))),
% 0.13/0.44 inference(resolution,[status(thm)],[f659,f228])).
% 0.13/0.44 fof(f683,plain,(
% 0.13/0.44 ![X0,X1,X2,X3,X4,X5]: (~event(skc12,skf2(skc10))|~man(skc8,skc10)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~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)|~man(skc8,X3)|~agent(skc8,X2,X3)|~agent(skc8,X4,X3)|~forename(skc8,X5)|~vincent_forename(skc8,X5)|~of(skc8,X5,X3)|~think_believe_consider(skc8,X4)|~present(skc8,X4)|~event(skc8,X4)|~theme(skc8,X4,skc12)|~actual_world(skc8))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f632,f96])).
% 0.13/0.44 fof(f698,plain,(
% 0.13/0.44 ![X0,X1,X2,X3]: (~event(skc12,skf2(skc10))|~man(skc8,skc10)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~smoke(skc12,skf2(skf4(skc12)))|~present(skc12,skf2(skf4(skc12)))|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~man(skc8,X1)|~agent(skc8,X0,X1)|~agent(skc8,X2,X1)|~forename(skc8,X3)|~vincent_forename(skc8,X3)|~of(skc8,X3,X1)|~think_believe_consider(skc8,X2)|~present(skc8,X2)|~event(skc8,X2)|~theme(skc8,X2,skc12)|~actual_world(skc8))),
% 0.13/0.44 inference(resolution,[status(thm)],[f660,f683])).
% 0.13/0.44 fof(f706,plain,(
% 0.13/0.44 ![X0,X1,X2,X3]: (~event(skc12,skf2(skc10))|~man(skc8,skc10)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~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)|~man(skc8,X1)|~agent(skc8,X0,X1)|~agent(skc8,X2,X1)|~forename(skc8,X3)|~vincent_forename(skc8,X3)|~of(skc8,X3,X1)|~think_believe_consider(skc8,X2)|~present(skc8,X2)|~event(skc8,X2)|~theme(skc8,X2,skc12)|~actual_world(skc8))),
% 0.13/0.44 inference(duplicate_literals_removal,[status(thm)],[f698])).
% 0.13/0.44 fof(f707,plain,(
% 0.13/0.44 ![X0,X1,X2,X3]: (~man(skc8,skc10)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~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)|~man(skc8,X1)|~agent(skc8,X0,X1)|~agent(skc8,X2,X1)|~forename(skc8,X3)|~vincent_forename(skc8,X3)|~of(skc8,X3,X1)|~think_believe_consider(skc8,X2)|~present(skc8,X2)|~event(skc8,X2)|~theme(skc8,X2,skc12)|~actual_world(skc8))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f706,f367])).
% 0.13/0.44 fof(f717,plain,(
% 0.13/0.44 ![X0,X1,X2,X3]: (~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~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)|~man(skc8,X1)|~agent(skc8,X0,X1)|~agent(skc8,X2,X1)|~forename(skc8,X3)|~vincent_forename(skc8,X3)|~of(skc8,X3,X1)|~think_believe_consider(skc8,X2)|~present(skc8,X2)|~event(skc8,X2)|~theme(skc8,X2,skc12)|~actual_world(skc8))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f707,f213])).
% 0.13/0.44 fof(f718,plain,(
% 0.13/0.44 ![X0,X1,X2,X3]: (~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~smoke(skc12,skf2(skf4(skc12)))|~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~man(skc8,X1)|~agent(skc8,X0,X1)|~agent(skc8,X2,X1)|~forename(skc8,X3)|~vincent_forename(skc8,X3)|~of(skc8,X3,X1)|~think_believe_consider(skc8,X2)|~present(skc8,X2)|~event(skc8,X2)|~theme(skc8,X2,skc12)|~actual_world(skc8))),
% 0.13/0.44 inference(resolution,[status(thm)],[f717,f368])).
% 0.13/0.44 fof(f719,plain,(
% 0.13/0.44 ![X0,X1,X2,X3]: (~accessible_world(skc8,skc12)|~smoke(skc12,skf2(skf4(skc12)))|~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~man(skc8,X1)|~agent(skc8,X0,X1)|~agent(skc8,X2,X1)|~forename(skc8,X3)|~vincent_forename(skc8,X3)|~of(skc8,X3,X1)|~think_believe_consider(skc8,X2)|~present(skc8,X2)|~event(skc8,X2)|~theme(skc8,X2,skc12)|~actual_world(skc8))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f718,f216])).
% 0.13/0.44 fof(f720,plain,(
% 0.13/0.44 ![X0,X1,X2,X3]: (~smoke(skc12,skf2(skf4(skc12)))|~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~man(skc8,X1)|~agent(skc8,X0,X1)|~agent(skc8,X2,X1)|~forename(skc8,X3)|~vincent_forename(skc8,X3)|~of(skc8,X3,X1)|~think_believe_consider(skc8,X2)|~present(skc8,X2)|~event(skc8,X2)|~theme(skc8,X2,skc12)|~actual_world(skc8))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f719,f215])).
% 0.13/0.44 fof(f721,plain,(
% 0.13/0.44 ![X0,X1,X2,X3]: (~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~man(skc8,X1)|~agent(skc8,X0,X1)|~agent(skc8,X2,X1)|~forename(skc8,X3)|~vincent_forename(skc8,X3)|~of(skc8,X3,X1)|~think_believe_consider(skc8,X2)|~present(skc8,X2)|~event(skc8,X2)|~theme(skc8,X2,skc12)|~actual_world(skc8))),
% 0.13/0.44 inference(resolution,[status(thm)],[f720,f369])).
% 0.13/0.44 fof(f722,plain,(
% 0.13/0.44 ![X0,X1,X2,X3]: (~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~man(skc8,X1)|~agent(skc8,X0,X1)|~agent(skc8,X2,X1)|~vincent_forename(skc8,X3)|~of(skc8,X3,X1)|~think_believe_consider(skc8,X2)|~present(skc8,X2)|~event(skc8,X2)|~theme(skc8,X2,skc12)|~actual_world(skc8))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f721,f124])).
% 0.13/0.44 fof(f732,plain,(
% 0.13/0.44 ![X0,X1,X2,X3]: (~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~man(skc8,X1)|~agent(skc8,X0,X1)|~agent(skc8,X2,X1)|~vincent_forename(skc8,X3)|~of(skc8,X3,X1)|~think_believe_consider(skc8,X2)|~present(skc8,X2)|~event(skc8,X2)|~theme(skc8,X2,skc12))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f722,f204])).
% 0.13/0.44 fof(f733,plain,(
% 0.13/0.44 ![X0,X1,X2]: (~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~man(skc8,X0)|~agent(skc8,skc13,X0)|~agent(skc8,X1,X0)|~vincent_forename(skc8,X2)|~of(skc8,X2,X0)|~think_believe_consider(skc8,X1)|~present(skc8,X1)|~event(skc8,X1)|~theme(skc8,X1,skc12))),
% 0.13/0.44 inference(resolution,[status(thm)],[f732,f219])).
% 0.13/0.44 fof(f734,plain,(
% 0.13/0.44 ![X0,X1,X2]: (~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~man(skc8,X0)|~agent(skc8,skc13,X0)|~agent(skc8,X1,X0)|~vincent_forename(skc8,X2)|~of(skc8,X2,X0)|~think_believe_consider(skc8,X1)|~present(skc8,X1)|~event(skc8,X1)|~theme(skc8,X1,skc12))),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f733,f208])).
% 0.13/0.45 fof(f735,plain,(
% 0.13/0.45 ![X0,X1,X2]: (~think_believe_consider(skc8,skc13)|~man(skc8,X0)|~agent(skc8,skc13,X0)|~agent(skc8,X1,X0)|~vincent_forename(skc8,X2)|~of(skc8,X2,X0)|~think_believe_consider(skc8,X1)|~present(skc8,X1)|~event(skc8,X1)|~theme(skc8,X1,skc12))),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f734,f209])).
% 0.13/0.45 fof(f736,plain,(
% 0.13/0.45 ![X0]: (~think_believe_consider(skc8,skc13)|~man(skc8,skc15)|~agent(skc8,skc13,skc15)|~vincent_forename(skc8,X0)|~of(skc8,X0,skc15)|~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~theme(skc8,skc13,skc12))),
% 0.13/0.45 inference(resolution,[status(thm)],[f735,f218])).
% 0.13/0.45 fof(f737,plain,(
% 0.13/0.45 ![X0]: (~think_believe_consider(skc8,skc13)|~man(skc8,skc15)|~agent(skc8,skc13,skc15)|~vincent_forename(skc8,X0)|~of(skc8,X0,skc15)|~present(skc8,skc13)|~event(skc8,skc13)|~theme(skc8,skc13,skc12))),
% 0.13/0.45 inference(duplicate_literals_removal,[status(thm)],[f736])).
% 0.13/0.45 fof(f738,plain,(
% 0.13/0.45 ![X0]: (~man(skc8,skc15)|~agent(skc8,skc13,skc15)|~vincent_forename(skc8,X0)|~of(skc8,X0,skc15)|~present(skc8,skc13)|~event(skc8,skc13)|~theme(skc8,skc13,skc12))),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f737,f210])).
% 0.13/0.45 fof(f742,plain,(
% 0.13/0.45 ![X0]: (~agent(skc8,skc13,skc15)|~vincent_forename(skc8,X0)|~of(skc8,X0,skc15)|~present(skc8,skc13)|~event(skc8,skc13)|~theme(skc8,skc13,skc12))),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f738,f205])).
% 0.13/0.45 fof(f743,plain,(
% 0.13/0.45 ~agent(skc8,skc13,skc15)|~vincent_forename(skc8,skc14)|~present(skc8,skc13)|~event(skc8,skc13)|~theme(skc8,skc13,skc12)),
% 0.13/0.45 inference(resolution,[status(thm)],[f742,f217])).
% 0.13/0.45 fof(f744,plain,(
% 0.13/0.45 ~vincent_forename(skc8,skc14)|~present(skc8,skc13)|~event(skc8,skc13)|~theme(skc8,skc13,skc12)),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f743,f218])).
% 0.13/0.45 fof(f745,plain,(
% 0.13/0.45 ~present(skc8,skc13)|~event(skc8,skc13)|~theme(skc8,skc13,skc12)),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f744,f207])).
% 0.13/0.45 fof(f746,plain,(
% 0.13/0.45 ~present(skc8,skc13)|~event(skc8,skc13)),
% 0.13/0.45 inference(resolution,[status(thm)],[f745,f219])).
% 0.13/0.45 fof(f747,plain,(
% 0.13/0.45 ~event(skc8,skc13)),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f746,f209])).
% 0.13/0.45 fof(f748,plain,(
% 0.13/0.45 $false),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f747,f208])).
% 0.13/0.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.46 % Elapsed time: 0.103113 seconds
% 0.13/0.46 % CPU time: 0.484523 seconds
% 0.13/0.46 % Total memory used: 54.747 MB
% 0.13/0.46 % Net memory used: 54.199 MB
%------------------------------------------------------------------------------