%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NLP251-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP251-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n017.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 01:50:26 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.52 % Refutation found
% 0.13/0.52 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.52 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.52 fof(f1,axiom,(
% 0.13/0.52 (![U,V]: (( ~ smoke(U,V)| event(U,V) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f29,axiom,(
% 0.13/0.52 (![U,V]: (( ~ vincent_forename(U,V)| forename(U,V) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f30,axiom,(
% 0.13/0.52 (![U,V]: (( ~ jules_forename(U,V)| forename(U,V) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f52,axiom,(
% 0.13/0.52 (![U,V,W]: (( ~ accessible_world(U,V)| ~ man(U,W)| man(V,W) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f72,negated_conjecture,(
% 0.13/0.52 actual_world(skc8) ),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f73,negated_conjecture,(
% 0.13/0.52 man(skc8,skc15) ),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f74,negated_conjecture,(
% 0.13/0.52 forename(skc8,skc14) ),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f75,negated_conjecture,(
% 0.13/0.52 vincent_forename(skc8,skc14) ),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f76,negated_conjecture,(
% 0.13/0.52 event(skc8,skc13) ),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f77,negated_conjecture,(
% 0.13/0.52 present(skc8,skc13) ),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f78,negated_conjecture,(
% 0.13/0.52 think_believe_consider(skc8,skc13) ),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f79,negated_conjecture,(
% 0.13/0.52 jules_forename(skc8,skc11) ),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f81,negated_conjecture,(
% 0.13/0.52 man(skc8,skc10) ),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f82,negated_conjecture,(
% 0.13/0.52 state(skc8,skc9) ),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f83,negated_conjecture,(
% 0.13/0.52 accessible_world(skc8,skc12) ),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f84,negated_conjecture,(
% 0.13/0.52 proposition(skc8,skc12) ),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f85,negated_conjecture,(
% 0.13/0.52 of(skc8,skc14,skc15) ),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f86,negated_conjecture,(
% 0.13/0.52 agent(skc8,skc13,skc15) ),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f87,negated_conjecture,(
% 0.13/0.52 theme(skc8,skc13,skc12) ),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f88,negated_conjecture,(
% 0.13/0.52 of(skc8,skc11,skc10) ),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f89,negated_conjecture,(
% 0.13/0.52 be(skc8,skc9,skc10,skc10) ),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f90,negated_conjecture,(
% 0.13/0.52 (![U,V]: (( ~ man(skc12,U)| smoke(skc12,skf2(V)) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f91,negated_conjecture,(
% 0.13/0.52 (![U,V]: (( ~ man(skc12,U)| present(skc12,skf2(V)) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f93,negated_conjecture,(
% 0.13/0.52 (![U]: (( ~ man(skc12,U)| agent(skc12,skf2(U),U) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f94,negated_conjecture,(
% 0.13/0.52 (![U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (( ~ proposition(U,V)| ~ accessible_world(U,V)| ~ think_believe_consider(U,W)| ~ present(U,W)| ~ event(U,W)| ~ theme(U,W,V)| ~ vincent_forename(U,X)| ~ forename(U,X)| ~ agent(U,W,Y)| ~ man(U,Y)| ~ of(U,X,Y)| ~ state(U,Z)| ~ man(U,X1)| ~ be(U,Z,X1,X1)| ~ forename(U,X2)| ~ jules_forename(U,X2)| ~ of(U,X2,X1)| ~ accessible_world(U,X3)| ~ proposition(U,X3)| ~ jules_forename(U,X4)| ~ forename(U,X4)| ~ smoke(X3,X5)| ~ present(X3,X5)| ~ agent(X3,X5,X6)| ~ event(X3,X5)| ~ man(U,X6)| ~ of(U,X4,X6)| ~ vincent_forename(U,X7)| ~ forename(U,X7)| ~ agent(U,X8,X9)| ~ man(U,X9)| ~ of(U,X7,X9)| ~ theme(U,X8,X3)| ~ event(U,X8)| ~ present(U,X8)| ~ think_believe_consider(U,X8)| ~ actual_world(U)| man(V,skf4(V)) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f95,negated_conjecture,(
% 0.13/0.52 (![U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (( ~ proposition(U,V)| ~ accessible_world(U,V)| ~ smoke(V,W)| ~ present(V,W)| ~ agent(V,W,skf4(V))| ~ event(V,W)| ~ think_believe_consider(U,X)| ~ present(U,X)| ~ event(U,X)| ~ theme(U,X,V)| ~ vincent_forename(U,Y)| ~ forename(U,Y)| ~ agent(U,X,Z)| ~ man(U,Z)| ~ of(U,Y,Z)| ~ state(U,X1)| ~ man(U,X2)| ~ be(U,X1,X2,X2)| ~ forename(U,X3)| ~ jules_forename(U,X3)| ~ of(U,X3,X2)| ~ accessible_world(U,X4)| ~ proposition(U,X4)| ~ jules_forename(U,X5)| ~ forename(U,X5)| ~ smoke(X4,X6)| ~ present(X4,X6)| ~ agent(X4,X6,X7)| ~ event(X4,X6)| ~ man(U,X7)| ~ of(U,X5,X7)| ~ vincent_forename(U,X8)| ~ forename(U,X8)| ~ agent(U,X9,X10)| ~ man(U,X10)| ~ of(U,X8,X10)| ~ theme(U,X9,X4)| ~ event(U,X9)| ~ present(U,X9)| ~ think_believe_consider(U,X9)| ~ actual_world(U) ) ))),
% 0.13/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.52 fof(f96,plain,(
% 0.13/0.52 ![X0,X1]: (~smoke(X0,X1)|event(X0,X1))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.52 fof(f124,plain,(
% 0.13/0.52 ![X0,X1]: (~vincent_forename(X0,X1)|forename(X0,X1))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f29])).
% 0.13/0.52 fof(f125,plain,(
% 0.13/0.52 ![X0,X1]: (~jules_forename(X0,X1)|forename(X0,X1))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f30])).
% 0.13/0.52 fof(f164,plain,(
% 0.13/0.52 ![V,W]: ((![U]: (~accessible_world(U,V)|~man(U,W)))|man(V,W))),
% 0.13/0.52 inference(miniscoping,[status(thm)],[f52])).
% 0.13/0.52 fof(f165,plain,(
% 0.13/0.52 ![X0,X1,X2]: (~accessible_world(X0,X1)|~man(X0,X2)|man(X1,X2))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f164])).
% 0.13/0.52 fof(f204,plain,(
% 0.13/0.52 actual_world(skc8)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f72])).
% 0.13/0.52 fof(f205,plain,(
% 0.13/0.52 man(skc8,skc15)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f73])).
% 0.13/0.52 fof(f206,plain,(
% 0.13/0.52 forename(skc8,skc14)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f74])).
% 0.13/0.52 fof(f207,plain,(
% 0.13/0.52 vincent_forename(skc8,skc14)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f75])).
% 0.13/0.52 fof(f208,plain,(
% 0.13/0.52 event(skc8,skc13)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f76])).
% 0.13/0.52 fof(f209,plain,(
% 0.13/0.52 present(skc8,skc13)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f77])).
% 0.13/0.52 fof(f210,plain,(
% 0.13/0.52 think_believe_consider(skc8,skc13)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f78])).
% 0.13/0.52 fof(f211,plain,(
% 0.13/0.52 jules_forename(skc8,skc11)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f79])).
% 0.13/0.52 fof(f213,plain,(
% 0.13/0.52 man(skc8,skc10)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f81])).
% 0.13/0.52 fof(f214,plain,(
% 0.13/0.52 state(skc8,skc9)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f82])).
% 0.13/0.52 fof(f215,plain,(
% 0.13/0.52 accessible_world(skc8,skc12)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f83])).
% 0.13/0.52 fof(f216,plain,(
% 0.13/0.52 proposition(skc8,skc12)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f84])).
% 0.13/0.52 fof(f217,plain,(
% 0.13/0.52 of(skc8,skc14,skc15)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f85])).
% 0.13/0.52 fof(f218,plain,(
% 0.13/0.52 agent(skc8,skc13,skc15)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f86])).
% 0.13/0.52 fof(f219,plain,(
% 0.13/0.52 theme(skc8,skc13,skc12)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f87])).
% 0.13/0.52 fof(f220,plain,(
% 0.13/0.52 of(skc8,skc11,skc10)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f88])).
% 0.13/0.52 fof(f221,plain,(
% 0.13/0.52 be(skc8,skc9,skc10,skc10)),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f89])).
% 0.13/0.52 fof(f222,plain,(
% 0.13/0.52 (![U]: ~man(skc12,U))|(![V]: smoke(skc12,skf2(V)))),
% 0.13/0.52 inference(miniscoping,[status(thm)],[f90])).
% 0.13/0.52 fof(f223,plain,(
% 0.13/0.52 ![X0,X1]: (~man(skc12,X0)|smoke(skc12,skf2(X1)))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f222])).
% 0.13/0.52 fof(f224,plain,(
% 0.13/0.52 (![U]: ~man(skc12,U))|(![V]: present(skc12,skf2(V)))),
% 0.13/0.52 inference(miniscoping,[status(thm)],[f91])).
% 0.13/0.52 fof(f225,plain,(
% 0.13/0.52 ![X0,X1]: (~man(skc12,X0)|present(skc12,skf2(X1)))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f224])).
% 0.13/0.52 fof(f228,plain,(
% 0.13/0.52 ![X0]: (~man(skc12,X0)|agent(skc12,skf2(X0),X0))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f93])).
% 0.13/0.52 fof(f229,plain,(
% 0.13/0.52 ![V]: ((![U]: ((![X8]: ((((![X3]: ((![X7,X9]: ((((((![X4,X6]: (((![X5]: (((((((((![X1,X2]: ((((![Z]: ((((![X,Y]: (((![W]: ((((((((~proposition(U,V)|~accessible_world(U,V))|~think_believe_consider(U,W))|~present(U,W))|~event(U,W))|~theme(U,W,V))|~vincent_forename(U,X))|~forename(U,X))|~agent(U,W,Y)))|~man(U,Y))|~of(U,X,Y)))|~state(U,Z))|~man(U,X1))|~be(U,Z,X1,X1)))|~forename(U,X2))|~jules_forename(U,X2))|~of(U,X2,X1)))|~accessible_world(U,X3))|~proposition(U,X3))|~jules_forename(U,X4))|~forename(U,X4))|~smoke(X3,X5))|~present(X3,X5))|~agent(X3,X5,X6))|~event(X3,X5)))|~man(U,X6))|~of(U,X4,X6)))|~vincent_forename(U,X7))|~forename(U,X7))|~agent(U,X8,X9))|~man(U,X9))|~of(U,X7,X9)))|~theme(U,X8,X3)))|~event(U,X8))|~present(U,X8))|~think_believe_consider(U,X8)))|~actual_world(U)))|man(V,skf4(V)))),
% 0.13/0.52 inference(miniscoping,[status(thm)],[f94])).
% 0.13/0.52 fof(f230,plain,(
% 0.13/0.52 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~proposition(X0,X1)|~accessible_world(X0,X1)|~think_believe_consider(X0,X2)|~present(X0,X2)|~event(X0,X2)|~theme(X0,X2,X1)|~vincent_forename(X0,X3)|~forename(X0,X3)|~agent(X0,X2,X4)|~man(X0,X4)|~of(X0,X3,X4)|~state(X0,X5)|~man(X0,X6)|~be(X0,X5,X6,X6)|~forename(X0,X7)|~jules_forename(X0,X7)|~of(X0,X7,X6)|~accessible_world(X0,X8)|~proposition(X0,X8)|~jules_forename(X0,X9)|~forename(X0,X9)|~smoke(X8,X10)|~present(X8,X10)|~agent(X8,X10,X11)|~event(X8,X10)|~man(X0,X11)|~of(X0,X9,X11)|~vincent_forename(X0,X12)|~forename(X0,X12)|~agent(X0,X13,X14)|~man(X0,X14)|~of(X0,X12,X14)|~theme(X0,X13,X8)|~event(X0,X13)|~present(X0,X13)|~think_believe_consider(X0,X13)|~actual_world(X0)|man(X1,skf4(X1)))),
% 0.13/0.52 inference(cnf_transformation,[status(thm)],[f229])).
% 0.13/0.52 fof(f231,plain,(
% 0.13/0.52 ![U]: ((![X9]: ((((![X4]: ((![X8,X10]: ((((((![X5,X7]: (((![X6]: (((((((((![X2,X3]: ((((![X1]: ((((![Y,Z]: (((![X]: ((((![V]: (((((![W]: (((((~proposition(U,V)|~accessible_world(U,V))|~smoke(V,W))|~present(V,W))|~agent(V,W,skf4(V)))|~event(V,W)))|~think_believe_consider(U,X))|~present(U,X))|~event(U,X))|~theme(U,X,V)))|~vincent_forename(U,Y))|~forename(U,Y))|~agent(U,X,Z)))|~man(U,Z))|~of(U,Y,Z)))|~state(U,X1))|~man(U,X2))|~be(U,X1,X2,X2)))|~forename(U,X3))|~jules_forename(U,X3))|~of(U,X3,X2)))|~accessible_world(U,X4))|~proposition(U,X4))|~jules_forename(U,X5))|~forename(U,X5))|~smoke(X4,X6))|~present(X4,X6))|~agent(X4,X6,X7))|~event(X4,X6)))|~man(U,X7))|~of(U,X5,X7)))|~vincent_forename(U,X8))|~forename(U,X8))|~agent(U,X9,X10))|~man(U,X10))|~of(U,X8,X10)))|~theme(U,X9,X4)))|~event(U,X9))|~present(U,X9))|~think_believe_consider(U,X9)))|~actual_world(U))),
% 0.13/0.53 inference(miniscoping,[status(thm)],[f95])).
% 0.13/0.53 fof(f232,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~proposition(X0,X1)|~accessible_world(X0,X1)|~smoke(X1,X2)|~present(X1,X2)|~agent(X1,X2,skf4(X1))|~event(X1,X2)|~think_believe_consider(X0,X3)|~present(X0,X3)|~event(X0,X3)|~theme(X0,X3,X1)|~vincent_forename(X0,X4)|~forename(X0,X4)|~agent(X0,X3,X5)|~man(X0,X5)|~of(X0,X4,X5)|~state(X0,X6)|~man(X0,X7)|~be(X0,X6,X7,X7)|~forename(X0,X8)|~jules_forename(X0,X8)|~of(X0,X8,X7)|~accessible_world(X0,X9)|~proposition(X0,X9)|~jules_forename(X0,X10)|~forename(X0,X10)|~smoke(X9,X11)|~present(X9,X11)|~agent(X9,X11,X12)|~event(X9,X11)|~man(X0,X12)|~of(X0,X10,X12)|~vincent_forename(X0,X13)|~forename(X0,X13)|~agent(X0,X14,X15)|~man(X0,X15)|~of(X0,X13,X15)|~theme(X0,X14,X9)|~event(X0,X14)|~present(X0,X14)|~think_believe_consider(X0,X14)|~actual_world(X0))),
% 0.13/0.53 inference(cnf_transformation,[status(thm)],[f231])).
% 0.13/0.53 fof(f289,plain,(
% 0.13/0.53 ![X0]: (~man(skc8,X0)|man(skc12,X0))),
% 0.13/0.53 inference(resolution,[status(thm)],[f165,f215])).
% 0.13/0.53 fof(f358,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~proposition(X0,X1)|~accessible_world(X0,X1)|~think_believe_consider(X0,X2)|~present(X0,X2)|~event(X0,X2)|~theme(X0,X2,X1)|~vincent_forename(X0,X3)|~forename(X0,X3)|~agent(X0,X2,X4)|~man(X0,X4)|~of(X0,X3,X4)|~state(X0,X5)|~man(X0,X6)|~be(X0,X5,X6,X6)|~forename(X0,X7)|~jules_forename(X0,X7)|~of(X0,X7,X6)|~accessible_world(X0,X8)|~proposition(X0,X8)|~jules_forename(X0,X9)|~forename(X0,X9)|~smoke(X8,X10)|~present(X8,X10)|~agent(X8,X10,X11)|~man(X0,X11)|~of(X0,X9,X11)|~vincent_forename(X0,X12)|~forename(X0,X12)|~agent(X0,X13,X14)|~man(X0,X14)|~of(X0,X12,X14)|~theme(X0,X13,X8)|~event(X0,X13)|~present(X0,X13)|~think_believe_consider(X0,X13)|~actual_world(X0)|man(X1,skf4(X1)))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f230,f96])).
% 0.13/0.53 fof(f359,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~vincent_forename(skc8,X0)|~forename(skc8,X0)|~agent(skc8,skc13,X1)|~man(skc8,X1)|~of(skc8,X0,X1)|~state(skc8,X2)|~man(skc8,X3)|~be(skc8,X2,X3,X3)|~forename(skc8,X4)|~jules_forename(skc8,X4)|~of(skc8,X4,X3)|~accessible_world(skc8,X5)|~proposition(skc8,X5)|~jules_forename(skc8,X6)|~forename(skc8,X6)|~smoke(X5,X7)|~present(X5,X7)|~agent(X5,X7,X8)|~man(skc8,X8)|~of(skc8,X6,X8)|~vincent_forename(skc8,X9)|~forename(skc8,X9)|~agent(skc8,X10,X11)|~man(skc8,X11)|~of(skc8,X9,X11)|~theme(skc8,X10,X5)|~event(skc8,X10)|~present(skc8,X10)|~think_believe_consider(skc8,X10)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(resolution,[status(thm)],[f358,f219])).
% 0.13/0.53 fof(f360,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~accessible_world(skc8,skc12)|~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~vincent_forename(skc8,X0)|~forename(skc8,X0)|~agent(skc8,skc13,X1)|~man(skc8,X1)|~of(skc8,X0,X1)|~state(skc8,X2)|~man(skc8,X3)|~be(skc8,X2,X3,X3)|~forename(skc8,X4)|~jules_forename(skc8,X4)|~of(skc8,X4,X3)|~accessible_world(skc8,X5)|~proposition(skc8,X5)|~jules_forename(skc8,X6)|~forename(skc8,X6)|~smoke(X5,X7)|~present(X5,X7)|~agent(X5,X7,X8)|~man(skc8,X8)|~of(skc8,X6,X8)|~vincent_forename(skc8,X9)|~forename(skc8,X9)|~agent(skc8,X10,X11)|~man(skc8,X11)|~of(skc8,X9,X11)|~theme(skc8,X10,X5)|~event(skc8,X10)|~present(skc8,X10)|~think_believe_consider(skc8,X10)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f359,f216])).
% 0.13/0.53 fof(f364,plain,(
% 0.13/0.53 man(skc12,skc10)),
% 0.13/0.53 inference(resolution,[status(thm)],[f289,f213])).
% 0.13/0.53 fof(f366,plain,(
% 0.13/0.53 agent(skc12,skf2(skc10),skc10)),
% 0.13/0.53 inference(resolution,[status(thm)],[f364,f228])).
% 0.13/0.53 fof(f368,plain,(
% 0.13/0.53 ![X0]: (present(skc12,skf2(X0)))),
% 0.13/0.53 inference(resolution,[status(thm)],[f364,f225])).
% 0.13/0.53 fof(f369,plain,(
% 0.13/0.53 ![X0]: (smoke(skc12,skf2(X0)))),
% 0.13/0.53 inference(resolution,[status(thm)],[f364,f223])).
% 0.13/0.53 fof(f372,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~proposition(X0,X1)|~accessible_world(X0,X1)|~smoke(X1,X2)|~present(X1,X2)|~agent(X1,X2,skf4(X1))|~think_believe_consider(X0,X3)|~present(X0,X3)|~event(X0,X3)|~theme(X0,X3,X1)|~vincent_forename(X0,X4)|~forename(X0,X4)|~agent(X0,X3,X5)|~man(X0,X5)|~of(X0,X4,X5)|~state(X0,X6)|~man(X0,X7)|~be(X0,X6,X7,X7)|~forename(X0,X8)|~jules_forename(X0,X8)|~of(X0,X8,X7)|~accessible_world(X0,X9)|~proposition(X0,X9)|~jules_forename(X0,X10)|~forename(X0,X10)|~smoke(X9,X11)|~present(X9,X11)|~agent(X9,X11,X12)|~event(X9,X11)|~man(X0,X12)|~of(X0,X10,X12)|~vincent_forename(X0,X13)|~forename(X0,X13)|~agent(X0,X14,X15)|~man(X0,X15)|~of(X0,X13,X15)|~theme(X0,X14,X9)|~event(X0,X14)|~present(X0,X14)|~think_believe_consider(X0,X14)|~actual_world(X0))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f232,f96])).
% 0.13/0.53 fof(f490,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~vincent_forename(skc8,X0)|~forename(skc8,X0)|~agent(skc8,skc13,X1)|~man(skc8,X1)|~of(skc8,X0,X1)|~state(skc8,X2)|~man(skc8,X3)|~be(skc8,X2,X3,X3)|~forename(skc8,X4)|~jules_forename(skc8,X4)|~of(skc8,X4,X3)|~accessible_world(skc8,X5)|~proposition(skc8,X5)|~jules_forename(skc8,X6)|~forename(skc8,X6)|~smoke(X5,X7)|~present(X5,X7)|~agent(X5,X7,X8)|~man(skc8,X8)|~of(skc8,X6,X8)|~vincent_forename(skc8,X9)|~forename(skc8,X9)|~agent(skc8,X10,X11)|~man(skc8,X11)|~of(skc8,X9,X11)|~theme(skc8,X10,X5)|~event(skc8,X10)|~present(skc8,X10)|~think_believe_consider(skc8,X10)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f360,f215])).
% 0.13/0.53 fof(f492,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,X0)|~man(skc8,X1)|~be(skc8,X0,X1,X1)|~forename(skc8,X2)|~jules_forename(skc8,X2)|~of(skc8,X2,X1)|~accessible_world(skc8,X3)|~proposition(skc8,X3)|~jules_forename(skc8,X4)|~forename(skc8,X4)|~smoke(X3,X5)|~present(X3,X5)|~agent(X3,X5,X6)|~man(skc8,X6)|~of(skc8,X4,X6)|~vincent_forename(skc8,X7)|~forename(skc8,X7)|~agent(skc8,X8,X9)|~man(skc8,X9)|~of(skc8,X7,X9)|~theme(skc8,X8,X3)|~event(skc8,X8)|~present(skc8,X8)|~think_believe_consider(skc8,X8)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(resolution,[status(thm)],[f490,f217])).
% 0.13/0.53 fof(f494,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~present(skc8,skc13)|~event(skc8,skc13)|~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,X0)|~man(skc8,X1)|~be(skc8,X0,X1,X1)|~forename(skc8,X2)|~jules_forename(skc8,X2)|~of(skc8,X2,X1)|~accessible_world(skc8,X3)|~proposition(skc8,X3)|~jules_forename(skc8,X4)|~forename(skc8,X4)|~smoke(X3,X5)|~present(X3,X5)|~agent(X3,X5,X6)|~man(skc8,X6)|~of(skc8,X4,X6)|~vincent_forename(skc8,X7)|~forename(skc8,X7)|~agent(skc8,X8,X9)|~man(skc8,X9)|~of(skc8,X7,X9)|~theme(skc8,X8,X3)|~event(skc8,X8)|~present(skc8,X8)|~think_believe_consider(skc8,X8)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f492,f210])).
% 0.13/0.53 fof(f539,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~event(skc8,skc13)|~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,X0)|~man(skc8,X1)|~be(skc8,X0,X1,X1)|~forename(skc8,X2)|~jules_forename(skc8,X2)|~of(skc8,X2,X1)|~accessible_world(skc8,X3)|~proposition(skc8,X3)|~jules_forename(skc8,X4)|~forename(skc8,X4)|~smoke(X3,X5)|~present(X3,X5)|~agent(X3,X5,X6)|~man(skc8,X6)|~of(skc8,X4,X6)|~vincent_forename(skc8,X7)|~forename(skc8,X7)|~agent(skc8,X8,X9)|~man(skc8,X9)|~of(skc8,X7,X9)|~theme(skc8,X8,X3)|~event(skc8,X8)|~present(skc8,X8)|~think_believe_consider(skc8,X8)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f494,f209])).
% 0.13/0.53 fof(f540,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~event(skc8,skc13)|~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~forename(skc8,X0)|~jules_forename(skc8,X0)|~of(skc8,X0,skc10)|~accessible_world(skc8,X1)|~proposition(skc8,X1)|~jules_forename(skc8,X2)|~forename(skc8,X2)|~smoke(X1,X3)|~present(X1,X3)|~agent(X1,X3,X4)|~man(skc8,X4)|~of(skc8,X2,X4)|~vincent_forename(skc8,X5)|~forename(skc8,X5)|~agent(skc8,X6,X7)|~man(skc8,X7)|~of(skc8,X5,X7)|~theme(skc8,X6,X1)|~event(skc8,X6)|~present(skc8,X6)|~think_believe_consider(skc8,X6)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(resolution,[status(thm)],[f539,f221])).
% 0.13/0.53 fof(f541,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~forename(skc8,X0)|~jules_forename(skc8,X0)|~of(skc8,X0,skc10)|~accessible_world(skc8,X1)|~proposition(skc8,X1)|~jules_forename(skc8,X2)|~forename(skc8,X2)|~smoke(X1,X3)|~present(X1,X3)|~agent(X1,X3,X4)|~man(skc8,X4)|~of(skc8,X2,X4)|~vincent_forename(skc8,X5)|~forename(skc8,X5)|~agent(skc8,X6,X7)|~man(skc8,X7)|~of(skc8,X5,X7)|~theme(skc8,X6,X1)|~event(skc8,X6)|~present(skc8,X6)|~think_believe_consider(skc8,X6)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f540,f208])).
% 0.13/0.53 fof(f570,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~forename(skc8,X0)|~jules_forename(skc8,X0)|~of(skc8,X0,skc10)|~accessible_world(skc8,X1)|~proposition(skc8,X1)|~jules_forename(skc8,X2)|~forename(skc8,X2)|~smoke(X1,X3)|~present(X1,X3)|~agent(X1,X3,X4)|~man(skc8,X4)|~of(skc8,X2,X4)|~vincent_forename(skc8,X5)|~forename(skc8,X5)|~agent(skc8,X6,X7)|~man(skc8,X7)|~of(skc8,X5,X7)|~theme(skc8,X6,X1)|~event(skc8,X6)|~present(skc8,X6)|~think_believe_consider(skc8,X6)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f541,f207])).
% 0.13/0.53 fof(f571,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6]: (~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~forename(skc8,skc11)|~jules_forename(skc8,skc11)|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~jules_forename(skc8,X1)|~forename(skc8,X1)|~smoke(X0,X2)|~present(X0,X2)|~agent(X0,X2,X3)|~man(skc8,X3)|~of(skc8,X1,X3)|~vincent_forename(skc8,X4)|~forename(skc8,X4)|~agent(skc8,X5,X6)|~man(skc8,X6)|~of(skc8,X4,X6)|~theme(skc8,X5,X0)|~event(skc8,X5)|~present(skc8,X5)|~think_believe_consider(skc8,X5)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(resolution,[status(thm)],[f570,f220])).
% 0.13/0.53 fof(f572,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6]: (~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~jules_forename(skc8,X1)|~forename(skc8,X1)|~smoke(X0,X2)|~present(X0,X2)|~agent(X0,X2,X3)|~man(skc8,X3)|~of(skc8,X1,X3)|~vincent_forename(skc8,X4)|~forename(skc8,X4)|~agent(skc8,X5,X6)|~man(skc8,X6)|~of(skc8,X4,X6)|~theme(skc8,X5,X0)|~event(skc8,X5)|~present(skc8,X5)|~think_believe_consider(skc8,X5)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f571,f125])).
% 0.13/0.53 fof(f597,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6]: (~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~jules_forename(skc8,X1)|~smoke(X0,X2)|~present(X0,X2)|~agent(X0,X2,X3)|~man(skc8,X3)|~of(skc8,X1,X3)|~vincent_forename(skc8,X4)|~forename(skc8,X4)|~agent(skc8,X5,X6)|~man(skc8,X6)|~of(skc8,X4,X6)|~theme(skc8,X5,X0)|~event(skc8,X5)|~present(skc8,X5)|~think_believe_consider(skc8,X5)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f572,f125])).
% 0.13/0.53 fof(f599,plain,(
% 0.13/0.53 ![X0,X1,X2,X3]: (~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~jules_forename(skc8,X0)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~man(skc8,skc10)|~of(skc8,X0,skc10)|~vincent_forename(skc8,X1)|~forename(skc8,X1)|~agent(skc8,X2,X3)|~man(skc8,X3)|~of(skc8,X1,X3)|~theme(skc8,X2,skc12)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(resolution,[status(thm)],[f597,f366])).
% 0.13/0.53 fof(f604,plain,(
% 0.13/0.53 ![X0,X1,X2,X3]: (~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~jules_forename(skc8,X0)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~of(skc8,X0,skc10)|~vincent_forename(skc8,X1)|~forename(skc8,X1)|~agent(skc8,X2,X3)|~man(skc8,X3)|~of(skc8,X1,X3)|~theme(skc8,X2,skc12)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(duplicate_literals_removal,[status(thm)],[f599])).
% 0.13/0.53 fof(f605,plain,(
% 0.13/0.53 ![X0,X1,X2,X3]: (~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~jules_forename(skc8,X0)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~of(skc8,X0,skc10)|~vincent_forename(skc8,X1)|~agent(skc8,X2,X3)|~man(skc8,X3)|~of(skc8,X1,X3)|~theme(skc8,X2,skc12)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f604,f124])).
% 0.13/0.53 fof(f656,plain,(
% 0.13/0.53 ![X0,X1,X2,X3]: (~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~jules_forename(skc8,X0)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~of(skc8,X0,skc10)|~vincent_forename(skc8,X1)|~agent(skc8,X2,X3)|~man(skc8,X3)|~of(skc8,X1,X3)|~theme(skc8,X2,skc12)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f605,f206])).
% 0.13/0.53 fof(f657,plain,(
% 0.13/0.53 ![X0,X1,X2]: (~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~jules_forename(skc8,skc11)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,X0)|~agent(skc8,X1,X2)|~man(skc8,X2)|~of(skc8,X0,X2)|~theme(skc8,X1,skc12)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(resolution,[status(thm)],[f656,f220])).
% 0.13/0.53 fof(f658,plain,(
% 0.13/0.53 ![X0,X1,X2]: (~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,X0)|~agent(skc8,X1,X2)|~man(skc8,X2)|~of(skc8,X0,X2)|~theme(skc8,X1,skc12)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(duplicate_literals_removal,[status(thm)],[f657])).
% 0.13/0.53 fof(f659,plain,(
% 0.13/0.53 ![X0,X1,X2]: (~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,X0)|~agent(skc8,X1,X2)|~man(skc8,X2)|~of(skc8,X0,X2)|~theme(skc8,X1,skc12)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f658,f218])).
% 0.13/0.53 fof(f663,plain,(
% 0.13/0.53 ![X0,X1,X2]: (~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,X0)|~agent(skc8,X1,X2)|~man(skc8,X2)|~of(skc8,X0,X2)|~theme(skc8,X1,skc12)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f659,f205])).
% 0.13/0.53 fof(f664,plain,(
% 0.13/0.53 ![X0]: (~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,X0)|~man(skc8,skc15)|~of(skc8,X0,skc15)|~theme(skc8,skc13,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(resolution,[status(thm)],[f663,f218])).
% 0.13/0.53 fof(f665,plain,(
% 0.13/0.53 ![X0]: (~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,X0)|~man(skc8,skc15)|~of(skc8,X0,skc15)|~theme(skc8,skc13,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f664,f214])).
% 0.13/0.53 fof(f666,plain,(
% 0.13/0.53 ![X0]: (~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,X0)|~man(skc8,skc15)|~of(skc8,X0,skc15)|~theme(skc8,skc13,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f665,f213])).
% 0.13/0.53 fof(f667,plain,(
% 0.13/0.53 ~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,skc14)|~man(skc8,skc15)|~theme(skc8,skc13,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.53 inference(resolution,[status(thm)],[f666,f217])).
% 0.13/0.53 fof(f668,plain,(
% 0.13/0.53 ~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,skc14)|~man(skc8,skc15)|~theme(skc8,skc13,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f667,f211])).
% 0.13/0.53 fof(f669,plain,(
% 0.13/0.53 ~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,skc14)|~man(skc8,skc15)|~theme(skc8,skc13,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f668,f215])).
% 0.13/0.53 fof(f670,plain,(
% 0.13/0.53 ~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,skc14)|~man(skc8,skc15)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.53 inference(resolution,[status(thm)],[f669,f219])).
% 0.13/0.53 fof(f671,plain,(
% 0.13/0.53 ~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,skc14)|~man(skc8,skc15)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f670,f216])).
% 0.13/0.53 fof(f672,plain,(
% 0.13/0.53 ~present(skc12,skf2(skc10))|~vincent_forename(skc8,skc14)|~man(skc8,skc15)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f671,f369])).
% 0.13/0.53 fof(f673,plain,(
% 0.13/0.53 ~vincent_forename(skc8,skc14)|~man(skc8,skc15)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.53 inference(resolution,[status(thm)],[f672,f368])).
% 0.13/0.53 fof(f674,plain,(
% 0.13/0.53 ~man(skc8,skc15)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f673,f207])).
% 0.13/0.53 fof(f675,plain,(
% 0.13/0.53 ~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f674,f205])).
% 0.13/0.53 fof(f676,plain,(
% 0.13/0.53 ~event(skc8,skc13)|~present(skc8,skc13)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.53 inference(resolution,[status(thm)],[f675,f210])).
% 0.13/0.53 fof(f677,plain,(
% 0.13/0.53 ~present(skc8,skc13)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f676,f208])).
% 0.13/0.53 fof(f678,plain,(
% 0.13/0.53 ~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f677,f209])).
% 0.13/0.53 fof(f679,plain,(
% 0.13/0.53 man(skc12,skf4(skc12))),
% 0.13/0.53 inference(resolution,[status(thm)],[f678,f204])).
% 0.13/0.53 fof(f705,plain,(
% 0.13/0.53 agent(skc12,skf2(skf4(skc12)),skf4(skc12))),
% 0.13/0.53 inference(resolution,[status(thm)],[f679,f228])).
% 0.13/0.53 fof(f721,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~proposition(X0,skc12)|~accessible_world(X0,skc12)|~smoke(skc12,skf2(skf4(skc12)))|~present(skc12,skf2(skf4(skc12)))|~think_believe_consider(X0,X1)|~present(X0,X1)|~event(X0,X1)|~theme(X0,X1,skc12)|~vincent_forename(X0,X2)|~forename(X0,X2)|~agent(X0,X1,X3)|~man(X0,X3)|~of(X0,X2,X3)|~state(X0,X4)|~man(X0,X5)|~be(X0,X4,X5,X5)|~forename(X0,X6)|~jules_forename(X0,X6)|~of(X0,X6,X5)|~accessible_world(X0,X7)|~proposition(X0,X7)|~jules_forename(X0,X8)|~forename(X0,X8)|~smoke(X7,X9)|~present(X7,X9)|~agent(X7,X9,X10)|~event(X7,X9)|~man(X0,X10)|~of(X0,X8,X10)|~vincent_forename(X0,X11)|~forename(X0,X11)|~agent(X0,X12,X13)|~man(X0,X13)|~of(X0,X11,X13)|~theme(X0,X12,X7)|~event(X0,X12)|~present(X0,X12)|~think_believe_consider(X0,X12)|~actual_world(X0))),
% 0.13/0.53 inference(resolution,[status(thm)],[f705,f372])).
% 0.13/0.53 fof(f722,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~proposition(X0,skc12)|~accessible_world(X0,skc12)|~present(skc12,skf2(skf4(skc12)))|~think_believe_consider(X0,X1)|~present(X0,X1)|~event(X0,X1)|~theme(X0,X1,skc12)|~vincent_forename(X0,X2)|~forename(X0,X2)|~agent(X0,X1,X3)|~man(X0,X3)|~of(X0,X2,X3)|~state(X0,X4)|~man(X0,X5)|~be(X0,X4,X5,X5)|~forename(X0,X6)|~jules_forename(X0,X6)|~of(X0,X6,X5)|~accessible_world(X0,X7)|~proposition(X0,X7)|~jules_forename(X0,X8)|~forename(X0,X8)|~smoke(X7,X9)|~present(X7,X9)|~agent(X7,X9,X10)|~event(X7,X9)|~man(X0,X10)|~of(X0,X8,X10)|~vincent_forename(X0,X11)|~forename(X0,X11)|~agent(X0,X12,X13)|~man(X0,X13)|~of(X0,X11,X13)|~theme(X0,X12,X7)|~event(X0,X12)|~present(X0,X12)|~think_believe_consider(X0,X12)|~actual_world(X0))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f721,f369])).
% 0.13/0.53 fof(f723,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~proposition(X0,skc12)|~accessible_world(X0,skc12)|~think_believe_consider(X0,X1)|~present(X0,X1)|~event(X0,X1)|~theme(X0,X1,skc12)|~vincent_forename(X0,X2)|~forename(X0,X2)|~agent(X0,X1,X3)|~man(X0,X3)|~of(X0,X2,X3)|~state(X0,X4)|~man(X0,X5)|~be(X0,X4,X5,X5)|~forename(X0,X6)|~jules_forename(X0,X6)|~of(X0,X6,X5)|~accessible_world(X0,X7)|~proposition(X0,X7)|~jules_forename(X0,X8)|~forename(X0,X8)|~smoke(X7,X9)|~present(X7,X9)|~agent(X7,X9,X10)|~event(X7,X9)|~man(X0,X10)|~of(X0,X8,X10)|~vincent_forename(X0,X11)|~forename(X0,X11)|~agent(X0,X12,X13)|~man(X0,X13)|~of(X0,X11,X13)|~theme(X0,X12,X7)|~event(X0,X12)|~present(X0,X12)|~think_believe_consider(X0,X12)|~actual_world(X0))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f722,f368])).
% 0.13/0.53 fof(f725,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~vincent_forename(skc8,X0)|~forename(skc8,X0)|~agent(skc8,skc13,X1)|~man(skc8,X1)|~of(skc8,X0,X1)|~state(skc8,X2)|~man(skc8,X3)|~be(skc8,X2,X3,X3)|~forename(skc8,X4)|~jules_forename(skc8,X4)|~of(skc8,X4,X3)|~accessible_world(skc8,X5)|~proposition(skc8,X5)|~jules_forename(skc8,X6)|~forename(skc8,X6)|~smoke(X5,X7)|~present(X5,X7)|~agent(X5,X7,X8)|~event(X5,X7)|~man(skc8,X8)|~of(skc8,X6,X8)|~vincent_forename(skc8,X9)|~forename(skc8,X9)|~agent(skc8,X10,X11)|~man(skc8,X11)|~of(skc8,X9,X11)|~theme(skc8,X10,X5)|~event(skc8,X10)|~present(skc8,X10)|~think_believe_consider(skc8,X10)|~actual_world(skc8))),
% 0.13/0.53 inference(resolution,[status(thm)],[f723,f219])).
% 0.13/0.53 fof(f727,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~accessible_world(skc8,skc12)|~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~vincent_forename(skc8,X0)|~forename(skc8,X0)|~agent(skc8,skc13,X1)|~man(skc8,X1)|~of(skc8,X0,X1)|~state(skc8,X2)|~man(skc8,X3)|~be(skc8,X2,X3,X3)|~forename(skc8,X4)|~jules_forename(skc8,X4)|~of(skc8,X4,X3)|~accessible_world(skc8,X5)|~proposition(skc8,X5)|~jules_forename(skc8,X6)|~forename(skc8,X6)|~smoke(X5,X7)|~present(X5,X7)|~agent(X5,X7,X8)|~event(X5,X7)|~man(skc8,X8)|~of(skc8,X6,X8)|~vincent_forename(skc8,X9)|~forename(skc8,X9)|~agent(skc8,X10,X11)|~man(skc8,X11)|~of(skc8,X9,X11)|~theme(skc8,X10,X5)|~event(skc8,X10)|~present(skc8,X10)|~think_believe_consider(skc8,X10)|~actual_world(skc8))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f725,f216])).
% 0.13/0.53 fof(f758,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~vincent_forename(skc8,X0)|~forename(skc8,X0)|~agent(skc8,skc13,X1)|~man(skc8,X1)|~of(skc8,X0,X1)|~state(skc8,X2)|~man(skc8,X3)|~be(skc8,X2,X3,X3)|~forename(skc8,X4)|~jules_forename(skc8,X4)|~of(skc8,X4,X3)|~accessible_world(skc8,X5)|~proposition(skc8,X5)|~jules_forename(skc8,X6)|~forename(skc8,X6)|~smoke(X5,X7)|~present(X5,X7)|~agent(X5,X7,X8)|~event(X5,X7)|~man(skc8,X8)|~of(skc8,X6,X8)|~vincent_forename(skc8,X9)|~forename(skc8,X9)|~agent(skc8,X10,X11)|~man(skc8,X11)|~of(skc8,X9,X11)|~theme(skc8,X10,X5)|~event(skc8,X10)|~present(skc8,X10)|~think_believe_consider(skc8,X10)|~actual_world(skc8))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f727,f215])).
% 0.13/0.53 fof(f760,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,X0)|~man(skc8,X1)|~be(skc8,X0,X1,X1)|~forename(skc8,X2)|~jules_forename(skc8,X2)|~of(skc8,X2,X1)|~accessible_world(skc8,X3)|~proposition(skc8,X3)|~jules_forename(skc8,X4)|~forename(skc8,X4)|~smoke(X3,X5)|~present(X3,X5)|~agent(X3,X5,X6)|~event(X3,X5)|~man(skc8,X6)|~of(skc8,X4,X6)|~vincent_forename(skc8,X7)|~forename(skc8,X7)|~agent(skc8,X8,X9)|~man(skc8,X9)|~of(skc8,X7,X9)|~theme(skc8,X8,X3)|~event(skc8,X8)|~present(skc8,X8)|~think_believe_consider(skc8,X8)|~actual_world(skc8))),
% 0.13/0.53 inference(resolution,[status(thm)],[f758,f217])).
% 0.13/0.53 fof(f762,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~present(skc8,skc13)|~event(skc8,skc13)|~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,X0)|~man(skc8,X1)|~be(skc8,X0,X1,X1)|~forename(skc8,X2)|~jules_forename(skc8,X2)|~of(skc8,X2,X1)|~accessible_world(skc8,X3)|~proposition(skc8,X3)|~jules_forename(skc8,X4)|~forename(skc8,X4)|~smoke(X3,X5)|~present(X3,X5)|~agent(X3,X5,X6)|~event(X3,X5)|~man(skc8,X6)|~of(skc8,X4,X6)|~vincent_forename(skc8,X7)|~forename(skc8,X7)|~agent(skc8,X8,X9)|~man(skc8,X9)|~of(skc8,X7,X9)|~theme(skc8,X8,X3)|~event(skc8,X8)|~present(skc8,X8)|~think_believe_consider(skc8,X8)|~actual_world(skc8))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f760,f210])).
% 0.13/0.53 fof(f785,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~event(skc8,skc13)|~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,X0)|~man(skc8,X1)|~be(skc8,X0,X1,X1)|~forename(skc8,X2)|~jules_forename(skc8,X2)|~of(skc8,X2,X1)|~accessible_world(skc8,X3)|~proposition(skc8,X3)|~jules_forename(skc8,X4)|~forename(skc8,X4)|~smoke(X3,X5)|~present(X3,X5)|~agent(X3,X5,X6)|~event(X3,X5)|~man(skc8,X6)|~of(skc8,X4,X6)|~vincent_forename(skc8,X7)|~forename(skc8,X7)|~agent(skc8,X8,X9)|~man(skc8,X9)|~of(skc8,X7,X9)|~theme(skc8,X8,X3)|~event(skc8,X8)|~present(skc8,X8)|~think_believe_consider(skc8,X8)|~actual_world(skc8))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f762,f209])).
% 0.13/0.53 fof(f786,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~event(skc8,skc13)|~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~forename(skc8,X0)|~jules_forename(skc8,X0)|~of(skc8,X0,skc10)|~accessible_world(skc8,X1)|~proposition(skc8,X1)|~jules_forename(skc8,X2)|~forename(skc8,X2)|~smoke(X1,X3)|~present(X1,X3)|~agent(X1,X3,X4)|~event(X1,X3)|~man(skc8,X4)|~of(skc8,X2,X4)|~vincent_forename(skc8,X5)|~forename(skc8,X5)|~agent(skc8,X6,X7)|~man(skc8,X7)|~of(skc8,X5,X7)|~theme(skc8,X6,X1)|~event(skc8,X6)|~present(skc8,X6)|~think_believe_consider(skc8,X6)|~actual_world(skc8))),
% 0.13/0.53 inference(resolution,[status(thm)],[f785,f221])).
% 0.13/0.53 fof(f787,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~event(skc8,skc13)|~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~forename(skc8,X0)|~jules_forename(skc8,X0)|~of(skc8,X0,skc10)|~accessible_world(skc8,X1)|~proposition(skc8,X1)|~jules_forename(skc8,X2)|~forename(skc8,X2)|~smoke(X1,X3)|~present(X1,X3)|~agent(X1,X3,X4)|~man(skc8,X4)|~of(skc8,X2,X4)|~vincent_forename(skc8,X5)|~forename(skc8,X5)|~agent(skc8,X6,X7)|~man(skc8,X7)|~of(skc8,X5,X7)|~theme(skc8,X6,X1)|~event(skc8,X6)|~present(skc8,X6)|~think_believe_consider(skc8,X6)|~actual_world(skc8))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f786,f96])).
% 0.13/0.53 fof(f820,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~forename(skc8,X0)|~jules_forename(skc8,X0)|~of(skc8,X0,skc10)|~accessible_world(skc8,X1)|~proposition(skc8,X1)|~jules_forename(skc8,X2)|~forename(skc8,X2)|~smoke(X1,X3)|~present(X1,X3)|~agent(X1,X3,X4)|~man(skc8,X4)|~of(skc8,X2,X4)|~vincent_forename(skc8,X5)|~forename(skc8,X5)|~agent(skc8,X6,X7)|~man(skc8,X7)|~of(skc8,X5,X7)|~theme(skc8,X6,X1)|~event(skc8,X6)|~present(skc8,X6)|~think_believe_consider(skc8,X6)|~actual_world(skc8))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f787,f208])).
% 0.13/0.53 fof(f821,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6]: (~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~forename(skc8,skc11)|~jules_forename(skc8,skc11)|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~jules_forename(skc8,X1)|~forename(skc8,X1)|~smoke(X0,X2)|~present(X0,X2)|~agent(X0,X2,X3)|~man(skc8,X3)|~of(skc8,X1,X3)|~vincent_forename(skc8,X4)|~forename(skc8,X4)|~agent(skc8,X5,X6)|~man(skc8,X6)|~of(skc8,X4,X6)|~theme(skc8,X5,X0)|~event(skc8,X5)|~present(skc8,X5)|~think_believe_consider(skc8,X5)|~actual_world(skc8))),
% 0.13/0.53 inference(resolution,[status(thm)],[f820,f220])).
% 0.13/0.53 fof(f822,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6]: (~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~forename(skc8,skc11)|~jules_forename(skc8,skc11)|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~jules_forename(skc8,X1)|~forename(skc8,X1)|~smoke(X0,X2)|~present(X0,X2)|~agent(X0,X2,X3)|~man(skc8,X3)|~of(skc8,X1,X3)|~vincent_forename(skc8,X4)|~forename(skc8,X4)|~agent(skc8,X5,X6)|~man(skc8,X6)|~of(skc8,X4,X6)|~theme(skc8,X5,X0)|~event(skc8,X5)|~present(skc8,X5)|~think_believe_consider(skc8,X5)|~actual_world(skc8))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f821,f207])).
% 0.13/0.53 fof(f855,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6]: (~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~jules_forename(skc8,X1)|~forename(skc8,X1)|~smoke(X0,X2)|~present(X0,X2)|~agent(X0,X2,X3)|~man(skc8,X3)|~of(skc8,X1,X3)|~vincent_forename(skc8,X4)|~forename(skc8,X4)|~agent(skc8,X5,X6)|~man(skc8,X6)|~of(skc8,X4,X6)|~theme(skc8,X5,X0)|~event(skc8,X5)|~present(skc8,X5)|~think_believe_consider(skc8,X5)|~actual_world(skc8))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f822,f125])).
% 0.13/0.53 fof(f858,plain,(
% 0.13/0.53 ![X0,X1,X2,X3]: (~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~jules_forename(skc8,X0)|~forename(skc8,X0)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~man(skc8,skc10)|~of(skc8,X0,skc10)|~vincent_forename(skc8,X1)|~forename(skc8,X1)|~agent(skc8,X2,X3)|~man(skc8,X3)|~of(skc8,X1,X3)|~theme(skc8,X2,skc12)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~actual_world(skc8))),
% 0.13/0.53 inference(resolution,[status(thm)],[f855,f366])).
% 0.13/0.53 fof(f864,plain,(
% 0.13/0.53 ![X0,X1,X2,X3]: (~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~jules_forename(skc8,X0)|~forename(skc8,X0)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~of(skc8,X0,skc10)|~vincent_forename(skc8,X1)|~forename(skc8,X1)|~agent(skc8,X2,X3)|~man(skc8,X3)|~of(skc8,X1,X3)|~theme(skc8,X2,skc12)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~actual_world(skc8))),
% 0.13/0.53 inference(duplicate_literals_removal,[status(thm)],[f858])).
% 0.13/0.53 fof(f865,plain,(
% 0.13/0.53 ![X0,X1,X2,X3]: (~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~jules_forename(skc8,X0)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~of(skc8,X0,skc10)|~vincent_forename(skc8,X1)|~forename(skc8,X1)|~agent(skc8,X2,X3)|~man(skc8,X3)|~of(skc8,X1,X3)|~theme(skc8,X2,skc12)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~actual_world(skc8))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f864,f125])).
% 0.13/0.53 fof(f958,plain,(
% 0.13/0.53 ![X0,X1,X2,X3]: (~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~jules_forename(skc8,X0)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~of(skc8,X0,skc10)|~vincent_forename(skc8,X1)|~agent(skc8,X2,X3)|~man(skc8,X3)|~of(skc8,X1,X3)|~theme(skc8,X2,skc12)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~actual_world(skc8))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f865,f124])).
% 0.13/0.53 fof(f959,plain,(
% 0.13/0.53 ![X0,X1,X2]: (~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~jules_forename(skc8,skc11)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,X0)|~agent(skc8,X1,X2)|~man(skc8,X2)|~of(skc8,X0,X2)|~theme(skc8,X1,skc12)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~actual_world(skc8))),
% 0.13/0.53 inference(resolution,[status(thm)],[f958,f220])).
% 0.13/0.53 fof(f960,plain,(
% 0.13/0.53 ![X0,X1,X2]: (~forename(skc8,skc14)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,X0)|~agent(skc8,X1,X2)|~man(skc8,X2)|~of(skc8,X0,X2)|~theme(skc8,X1,skc12)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~actual_world(skc8))),
% 0.13/0.53 inference(duplicate_literals_removal,[status(thm)],[f959])).
% 0.13/0.53 fof(f961,plain,(
% 0.13/0.53 ![X0,X1,X2]: (~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,X0)|~agent(skc8,X1,X2)|~man(skc8,X2)|~of(skc8,X0,X2)|~theme(skc8,X1,skc12)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~actual_world(skc8))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f960,f206])).
% 0.13/0.53 fof(f976,plain,(
% 0.13/0.53 ![X0,X1,X2]: (~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,X0)|~agent(skc8,X1,X2)|~man(skc8,X2)|~of(skc8,X0,X2)|~theme(skc8,X1,skc12)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~actual_world(skc8))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f961,f218])).
% 0.13/0.53 fof(f977,plain,(
% 0.13/0.53 ![X0]: (~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,X0)|~man(skc8,skc15)|~of(skc8,X0,skc15)|~theme(skc8,skc13,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8))),
% 0.13/0.53 inference(resolution,[status(thm)],[f976,f218])).
% 0.13/0.53 fof(f978,plain,(
% 0.13/0.53 ![X0]: (~man(skc8,skc15)|~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,X0)|~of(skc8,X0,skc15)|~theme(skc8,skc13,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8))),
% 0.13/0.53 inference(duplicate_literals_removal,[status(thm)],[f977])).
% 0.13/0.53 fof(f979,plain,(
% 0.13/0.53 ![X0]: (~state(skc8,skc9)|~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,X0)|~of(skc8,X0,skc15)|~theme(skc8,skc13,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f978,f205])).
% 0.13/0.53 fof(f991,plain,(
% 0.13/0.53 ![X0]: (~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,X0)|~of(skc8,X0,skc15)|~theme(skc8,skc13,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8))),
% 0.13/0.53 inference(forward_subsumption_resolution,[status(thm)],[f979,f214])).
% 0.13/0.53 fof(f992,plain,(
% 0.64/0.53 ~man(skc8,skc10)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,skc14)|~theme(skc8,skc13,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)),
% 0.64/0.53 inference(resolution,[status(thm)],[f991,f217])).
% 0.64/0.53 fof(f993,plain,(
% 0.64/0.53 ~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,skc14)|~theme(skc8,skc13,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)),
% 0.64/0.53 inference(forward_subsumption_resolution,[status(thm)],[f992,f213])).
% 0.64/0.53 fof(f994,plain,(
% 0.64/0.53 ~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,skc14)|~theme(skc8,skc13,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)),
% 0.64/0.53 inference(forward_subsumption_resolution,[status(thm)],[f993,f211])).
% 0.64/0.53 fof(f995,plain,(
% 0.64/0.53 ~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,skc14)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)),
% 0.64/0.53 inference(resolution,[status(thm)],[f994,f219])).
% 0.64/0.53 fof(f996,plain,(
% 0.64/0.53 ~proposition(skc8,skc12)|~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,skc14)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)),
% 0.64/0.53 inference(forward_subsumption_resolution,[status(thm)],[f995,f215])).
% 0.64/0.53 fof(f1001,plain,(
% 0.64/0.53 ~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~vincent_forename(skc8,skc14)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)),
% 0.64/0.53 inference(forward_subsumption_resolution,[status(thm)],[f996,f216])).
% 0.64/0.53 fof(f1002,plain,(
% 0.64/0.53 ~smoke(skc12,skf2(skc10))|~vincent_forename(skc8,skc14)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)),
% 0.64/0.54 inference(resolution,[status(thm)],[f1001,f368])).
% 0.64/0.54 fof(f1003,plain,(
% 0.64/0.54 ~vincent_forename(skc8,skc14)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)),
% 0.64/0.54 inference(forward_subsumption_resolution,[status(thm)],[f1002,f369])).
% 0.64/0.54 fof(f1004,plain,(
% 0.64/0.54 ~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)),
% 0.64/0.54 inference(forward_subsumption_resolution,[status(thm)],[f1003,f207])).
% 0.64/0.54 fof(f1005,plain,(
% 0.64/0.54 ~event(skc8,skc13)|~present(skc8,skc13)|~actual_world(skc8)),
% 0.64/0.54 inference(resolution,[status(thm)],[f1004,f210])).
% 0.64/0.54 fof(f1006,plain,(
% 0.64/0.54 ~present(skc8,skc13)|~actual_world(skc8)),
% 0.64/0.54 inference(forward_subsumption_resolution,[status(thm)],[f1005,f208])).
% 0.64/0.54 fof(f1008,plain,(
% 0.64/0.54 ~actual_world(skc8)),
% 0.64/0.54 inference(forward_subsumption_resolution,[status(thm)],[f1006,f209])).
% 0.64/0.54 fof(f1009,plain,(
% 0.64/0.54 $false),
% 0.64/0.54 inference(backward_subsumption_resolution,[status(thm)],[f204,f1008])).
% 0.64/0.54 % SZS output end CNFRefutation for theBenchmark.p
% 0.64/0.54 % Elapsed time: 0.171891 seconds
% 0.64/0.54 % CPU time: 1.098977 seconds
% 0.64/0.54 % Total memory used: 65.298 MB
% 0.64/0.54 % Net memory used: 63.506 MB
%------------------------------------------------------------------------------