%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NLP258-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 : n011.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.12s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP258-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.10/0.35 % Computer : n011.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 01:56:26 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 0.12/0.40 % Refutation found
% 0.12/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.40 fof(f1,axiom,(
% 0.12/0.40 (![U,V]: (( ~ smoke(U,V)| event(U,V) ) ))),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f30,axiom,(
% 0.12/0.40 (![U,V]: (( ~ jules_forename(U,V)| forename(U,V) ) ))),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f52,axiom,(
% 0.12/0.40 (![U,V,W]: (( ~ accessible_world(U,V)| ~ man(U,W)| man(V,W) ) ))),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f72,negated_conjecture,(
% 0.12/0.40 actual_world(skc8) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f73,negated_conjecture,(
% 0.12/0.40 man(skc8,skc15) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f74,negated_conjecture,(
% 0.12/0.40 forename(skc8,skc14) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f75,negated_conjecture,(
% 0.12/0.40 vincent_forename(skc8,skc14) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f76,negated_conjecture,(
% 0.12/0.40 event(skc8,skc13) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f77,negated_conjecture,(
% 0.12/0.40 present(skc8,skc13) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f78,negated_conjecture,(
% 0.12/0.40 think_believe_consider(skc8,skc13) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f79,negated_conjecture,(
% 0.12/0.40 jules_forename(skc8,skc11) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f81,negated_conjecture,(
% 0.12/0.40 man(skc8,skc10) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f82,negated_conjecture,(
% 0.12/0.40 state(skc8,skc9) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f83,negated_conjecture,(
% 0.12/0.40 accessible_world(skc8,skc12) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f84,negated_conjecture,(
% 0.12/0.40 proposition(skc8,skc12) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f85,negated_conjecture,(
% 0.12/0.40 of(skc8,skc14,skc15) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f86,negated_conjecture,(
% 0.12/0.40 agent(skc8,skc13,skc15) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f87,negated_conjecture,(
% 0.12/0.40 theme(skc8,skc13,skc12) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f88,negated_conjecture,(
% 0.12/0.40 of(skc8,skc11,skc10) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f89,negated_conjecture,(
% 0.12/0.40 be(skc8,skc9,skc10,skc10) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f90,negated_conjecture,(
% 0.12/0.40 (![U,V]: (( ~ man(skc12,U)| smoke(skc12,skf2(V)) ) ))),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f91,negated_conjecture,(
% 0.12/0.40 (![U,V]: (( ~ man(skc12,U)| present(skc12,skf2(V)) ) ))),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f92,negated_conjecture,(
% 0.12/0.40 (![U,V]: (( ~ man(skc12,U)| event(skc12,skf2(V)) ) ))),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f93,negated_conjecture,(
% 0.12/0.40 (![U]: (( ~ man(skc12,U)| agent(skc12,skf2(U),U) ) ))),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f94,negated_conjecture,(
% 0.12/0.40 (![U,V,W,X,Y,Z,X1,X2,X3,X4,X5]: (( ~ state(U,V)| ~ man(U,W)| ~ be(U,V,W,W)| ~ smoke(X,Y)| ~ present(X,Y)| ~ agent(X,Y,W)| ~ event(X,Y)| ~ forename(U,Z)| ~ jules_forename(U,Z)| ~ of(U,Z,W)| ~ accessible_world(U,X)| ~ proposition(U,X)| ~ proposition(U,X1)| ~ accessible_world(U,X1)| ~ think_believe_consider(U,X2)| ~ present(U,X2)| ~ event(U,X2)| ~ theme(U,X2,X1)| ~ agent(U,X3,X4)| ~ agent(U,X2,X4)| ~ man(U,X4)| ~ of(U,X5,X4)| ~ vincent_forename(U,X5)| ~ forename(U,X5)| ~ theme(U,X3,X)| ~ event(U,X3)| ~ present(U,X3)| ~ think_believe_consider(U,X3)| ~ actual_world(U)| man(X1,skf4(X1)) ) ))),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f95,negated_conjecture,(
% 0.12/0.40 (![U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6]: (( ~ state(U,V)| ~ man(U,W)| ~ be(U,V,W,W)| ~ smoke(X,Y)| ~ present(X,Y)| ~ agent(X,Y,W)| ~ event(X,Y)| ~ forename(U,Z)| ~ jules_forename(U,Z)| ~ of(U,Z,W)| ~ accessible_world(U,X)| ~ proposition(U,X)| ~ proposition(U,X1)| ~ accessible_world(U,X1)| ~ smoke(X1,X2)| ~ present(X1,X2)| ~ agent(X1,X2,skf4(X1))| ~ event(X1,X2)| ~ think_believe_consider(U,X3)| ~ present(U,X3)| ~ event(U,X3)| ~ theme(U,X3,X1)| ~ agent(U,X4,X5)| ~ agent(U,X3,X5)| ~ man(U,X5)| ~ of(U,X6,X5)| ~ vincent_forename(U,X6)| ~ forename(U,X6)| ~ theme(U,X4,X)| ~ event(U,X4)| ~ present(U,X4)| ~ think_believe_consider(U,X4)| ~ actual_world(U) ) ))),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f96,plain,(
% 0.12/0.40 ![X0,X1]: (~smoke(X0,X1)|event(X0,X1))),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f1])).
% 0.12/0.40 fof(f125,plain,(
% 0.12/0.40 ![X0,X1]: (~jules_forename(X0,X1)|forename(X0,X1))),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f30])).
% 0.12/0.40 fof(f164,plain,(
% 0.12/0.40 ![V,W]: ((![U]: (~accessible_world(U,V)|~man(U,W)))|man(V,W))),
% 0.12/0.40 inference(miniscoping,[status(thm)],[f52])).
% 0.12/0.40 fof(f165,plain,(
% 0.12/0.40 ![X0,X1,X2]: (~accessible_world(X0,X1)|~man(X0,X2)|man(X1,X2))),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f164])).
% 0.12/0.40 fof(f204,plain,(
% 0.12/0.40 actual_world(skc8)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f72])).
% 0.12/0.40 fof(f205,plain,(
% 0.12/0.40 man(skc8,skc15)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f73])).
% 0.12/0.40 fof(f206,plain,(
% 0.12/0.40 forename(skc8,skc14)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f74])).
% 0.12/0.40 fof(f207,plain,(
% 0.12/0.40 vincent_forename(skc8,skc14)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f75])).
% 0.12/0.40 fof(f208,plain,(
% 0.12/0.40 event(skc8,skc13)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f76])).
% 0.12/0.40 fof(f209,plain,(
% 0.12/0.40 present(skc8,skc13)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f77])).
% 0.12/0.40 fof(f210,plain,(
% 0.12/0.40 think_believe_consider(skc8,skc13)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f78])).
% 0.12/0.40 fof(f211,plain,(
% 0.12/0.40 jules_forename(skc8,skc11)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f79])).
% 0.12/0.40 fof(f213,plain,(
% 0.12/0.40 man(skc8,skc10)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f81])).
% 0.12/0.40 fof(f214,plain,(
% 0.12/0.40 state(skc8,skc9)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f82])).
% 0.12/0.40 fof(f215,plain,(
% 0.12/0.40 accessible_world(skc8,skc12)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f83])).
% 0.12/0.40 fof(f216,plain,(
% 0.12/0.40 proposition(skc8,skc12)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f84])).
% 0.12/0.40 fof(f217,plain,(
% 0.12/0.40 of(skc8,skc14,skc15)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f85])).
% 0.12/0.40 fof(f218,plain,(
% 0.12/0.40 agent(skc8,skc13,skc15)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f86])).
% 0.12/0.40 fof(f219,plain,(
% 0.12/0.40 theme(skc8,skc13,skc12)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f87])).
% 0.12/0.40 fof(f220,plain,(
% 0.12/0.40 of(skc8,skc11,skc10)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f88])).
% 0.12/0.40 fof(f221,plain,(
% 0.12/0.40 be(skc8,skc9,skc10,skc10)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f89])).
% 0.12/0.40 fof(f222,plain,(
% 0.12/0.40 (![U]: ~man(skc12,U))|(![V]: smoke(skc12,skf2(V)))),
% 0.12/0.40 inference(miniscoping,[status(thm)],[f90])).
% 0.12/0.40 fof(f223,plain,(
% 0.12/0.40 ![X0,X1]: (~man(skc12,X0)|smoke(skc12,skf2(X1)))),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f222])).
% 0.12/0.40 fof(f224,plain,(
% 0.12/0.40 (![U]: ~man(skc12,U))|(![V]: present(skc12,skf2(V)))),
% 0.12/0.40 inference(miniscoping,[status(thm)],[f91])).
% 0.12/0.40 fof(f225,plain,(
% 0.12/0.40 ![X0,X1]: (~man(skc12,X0)|present(skc12,skf2(X1)))),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f224])).
% 0.12/0.40 fof(f226,plain,(
% 0.12/0.40 (![U]: ~man(skc12,U))|(![V]: event(skc12,skf2(V)))),
% 0.12/0.40 inference(miniscoping,[status(thm)],[f92])).
% 0.12/0.40 fof(f227,plain,(
% 0.12/0.40 ![X0,X1]: (~man(skc12,X0)|event(skc12,skf2(X1)))),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f226])).
% 0.12/0.40 fof(f228,plain,(
% 0.12/0.40 ![X0]: (~man(skc12,X0)|agent(skc12,skf2(X0),X0))),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f93])).
% 0.12/0.40 fof(f229,plain,(
% 0.12/0.40 ![X1]: ((![U]: ((![X3]: ((((![X]: ((![X5]: (((![X4]: (((![X2]: (((((((((((![W,Z]: ((((![Y]: (((((![V]: ((~state(U,V)|~man(U,W))|~be(U,V,W,W)))|~smoke(X,Y))|~present(X,Y))|~agent(X,Y,W))|~event(X,Y)))|~forename(U,Z))|~jules_forename(U,Z))|~of(U,Z,W)))|~accessible_world(U,X))|~proposition(U,X))|~proposition(U,X1))|~accessible_world(U,X1))|~think_believe_consider(U,X2))|~present(U,X2))|~event(U,X2))|~theme(U,X2,X1))|~agent(U,X3,X4))|~agent(U,X2,X4)))|~man(U,X4))|~of(U,X5,X4)))|~vincent_forename(U,X5))|~forename(U,X5)))|~theme(U,X3,X)))|~event(U,X3))|~present(U,X3))|~think_believe_consider(U,X3)))|~actual_world(U)))|man(X1,skf4(X1)))),
% 0.12/0.40 inference(miniscoping,[status(thm)],[f94])).
% 0.12/0.40 fof(f230,plain,(
% 0.12/0.40 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~state(X0,X1)|~man(X0,X2)|~be(X0,X1,X2,X2)|~smoke(X3,X4)|~present(X3,X4)|~agent(X3,X4,X2)|~event(X3,X4)|~forename(X0,X5)|~jules_forename(X0,X5)|~of(X0,X5,X2)|~accessible_world(X0,X3)|~proposition(X0,X3)|~proposition(X0,X6)|~accessible_world(X0,X6)|~think_believe_consider(X0,X7)|~present(X0,X7)|~event(X0,X7)|~theme(X0,X7,X6)|~agent(X0,X8,X9)|~agent(X0,X7,X9)|~man(X0,X9)|~of(X0,X10,X9)|~vincent_forename(X0,X10)|~forename(X0,X10)|~theme(X0,X8,X3)|~event(X0,X8)|~present(X0,X8)|~think_believe_consider(X0,X8)|~actual_world(X0)|man(X6,skf4(X6)))),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f229])).
% 0.12/0.40 fof(f231,plain,(
% 0.12/0.40 ![U]: ((![X4]: ((((![X]: ((![X6]: (((![X5]: (((![X3]: (((![X1]: (((((![X2]: (((((((((![W,Z]: ((((![Y]: (((((![V]: ((~state(U,V)|~man(U,W))|~be(U,V,W,W)))|~smoke(X,Y))|~present(X,Y))|~agent(X,Y,W))|~event(X,Y)))|~forename(U,Z))|~jules_forename(U,Z))|~of(U,Z,W)))|~accessible_world(U,X))|~proposition(U,X))|~proposition(U,X1))|~accessible_world(U,X1))|~smoke(X1,X2))|~present(X1,X2))|~agent(X1,X2,skf4(X1)))|~event(X1,X2)))|~think_believe_consider(U,X3))|~present(U,X3))|~event(U,X3))|~theme(U,X3,X1)))|~agent(U,X4,X5))|~agent(U,X3,X5)))|~man(U,X5))|~of(U,X6,X5)))|~vincent_forename(U,X6))|~forename(U,X6)))|~theme(U,X4,X)))|~event(U,X4))|~present(U,X4))|~think_believe_consider(U,X4)))|~actual_world(U))),
% 0.12/0.40 inference(miniscoping,[status(thm)],[f95])).
% 0.12/0.40 fof(f232,plain,(
% 0.12/0.40 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~state(X0,X1)|~man(X0,X2)|~be(X0,X1,X2,X2)|~smoke(X3,X4)|~present(X3,X4)|~agent(X3,X4,X2)|~event(X3,X4)|~forename(X0,X5)|~jules_forename(X0,X5)|~of(X0,X5,X2)|~accessible_world(X0,X3)|~proposition(X0,X3)|~proposition(X0,X6)|~accessible_world(X0,X6)|~smoke(X6,X7)|~present(X6,X7)|~agent(X6,X7,skf4(X6))|~event(X6,X7)|~think_believe_consider(X0,X8)|~present(X0,X8)|~event(X0,X8)|~theme(X0,X8,X6)|~agent(X0,X9,X10)|~agent(X0,X8,X10)|~man(X0,X10)|~of(X0,X11,X10)|~vincent_forename(X0,X11)|~forename(X0,X11)|~theme(X0,X9,X3)|~event(X0,X9)|~present(X0,X9)|~think_believe_consider(X0,X9)|~actual_world(X0))),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f231])).
% 0.12/0.40 fof(f289,plain,(
% 0.12/0.40 ![X0]: (~man(skc8,X0)|man(skc12,X0))),
% 0.12/0.40 inference(resolution,[status(thm)],[f165,f215])).
% 0.12/0.40 fof(f358,plain,(
% 0.12/0.40 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~state(X0,X1)|~man(X0,X2)|~be(X0,X1,X2,X2)|~smoke(X3,X4)|~present(X3,X4)|~agent(X3,X4,X2)|~forename(X0,X5)|~jules_forename(X0,X5)|~of(X0,X5,X2)|~accessible_world(X0,X3)|~proposition(X0,X3)|~proposition(X0,X6)|~accessible_world(X0,X6)|~think_believe_consider(X0,X7)|~present(X0,X7)|~event(X0,X7)|~theme(X0,X7,X6)|~agent(X0,X8,X9)|~agent(X0,X7,X9)|~man(X0,X9)|~of(X0,X10,X9)|~vincent_forename(X0,X10)|~forename(X0,X10)|~theme(X0,X8,X3)|~event(X0,X8)|~present(X0,X8)|~think_believe_consider(X0,X8)|~actual_world(X0)|man(X6,skf4(X6)))),
% 0.12/0.40 inference(forward_subsumption_resolution,[status(thm)],[f230,f96])).
% 0.12/0.40 fof(f359,plain,(
% 0.12/0.40 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~state(skc8,skc9)|~man(skc8,skc10)|~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skc10)|~forename(skc8,X2)|~jules_forename(skc8,X2)|~of(skc8,X2,skc10)|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~proposition(skc8,X3)|~accessible_world(skc8,X3)|~think_believe_consider(skc8,X4)|~present(skc8,X4)|~event(skc8,X4)|~theme(skc8,X4,X3)|~agent(skc8,X5,X6)|~agent(skc8,X4,X6)|~man(skc8,X6)|~of(skc8,X7,X6)|~vincent_forename(skc8,X7)|~forename(skc8,X7)|~theme(skc8,X5,X0)|~event(skc8,X5)|~present(skc8,X5)|~think_believe_consider(skc8,X5)|~actual_world(skc8)|man(X3,skf4(X3)))),
% 0.12/0.40 inference(resolution,[status(thm)],[f358,f221])).
% 0.12/0.40 fof(f360,plain,(
% 0.12/0.40 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~man(skc8,skc10)|~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skc10)|~forename(skc8,X2)|~jules_forename(skc8,X2)|~of(skc8,X2,skc10)|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~proposition(skc8,X3)|~accessible_world(skc8,X3)|~think_believe_consider(skc8,X4)|~present(skc8,X4)|~event(skc8,X4)|~theme(skc8,X4,X3)|~agent(skc8,X5,X6)|~agent(skc8,X4,X6)|~man(skc8,X6)|~of(skc8,X7,X6)|~vincent_forename(skc8,X7)|~forename(skc8,X7)|~theme(skc8,X5,X0)|~event(skc8,X5)|~present(skc8,X5)|~think_believe_consider(skc8,X5)|~actual_world(skc8)|man(X3,skf4(X3)))),
% 0.12/0.40 inference(forward_subsumption_resolution,[status(thm)],[f359,f214])).
% 0.12/0.40 fof(f364,plain,(
% 0.12/0.40 man(skc12,skc10)),
% 0.12/0.40 inference(resolution,[status(thm)],[f289,f213])).
% 0.12/0.40 fof(f366,plain,(
% 0.12/0.40 agent(skc12,skf2(skc10),skc10)),
% 0.12/0.40 inference(resolution,[status(thm)],[f364,f228])).
% 0.12/0.40 fof(f367,plain,(
% 0.12/0.40 ![X0]: (event(skc12,skf2(X0)))),
% 0.12/0.40 inference(resolution,[status(thm)],[f364,f227])).
% 0.12/0.40 fof(f368,plain,(
% 0.12/0.40 ![X0]: (present(skc12,skf2(X0)))),
% 0.12/0.40 inference(resolution,[status(thm)],[f364,f225])).
% 0.12/0.40 fof(f369,plain,(
% 0.12/0.40 ![X0]: (smoke(skc12,skf2(X0)))),
% 0.12/0.40 inference(resolution,[status(thm)],[f364,f223])).
% 0.12/0.40 fof(f372,plain,(
% 0.12/0.40 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~state(X0,X1)|~man(X0,X2)|~be(X0,X1,X2,X2)|~smoke(X3,X4)|~present(X3,X4)|~agent(X3,X4,X2)|~forename(X0,X5)|~jules_forename(X0,X5)|~of(X0,X5,X2)|~accessible_world(X0,X3)|~proposition(X0,X3)|~proposition(X0,X6)|~accessible_world(X0,X6)|~smoke(X6,X7)|~present(X6,X7)|~agent(X6,X7,skf4(X6))|~event(X6,X7)|~think_believe_consider(X0,X8)|~present(X0,X8)|~event(X0,X8)|~theme(X0,X8,X6)|~agent(X0,X9,X10)|~agent(X0,X8,X10)|~man(X0,X10)|~of(X0,X11,X10)|~vincent_forename(X0,X11)|~forename(X0,X11)|~theme(X0,X9,X3)|~event(X0,X9)|~present(X0,X9)|~think_believe_consider(X0,X9)|~actual_world(X0))),
% 0.12/0.40 inference(forward_subsumption_resolution,[status(thm)],[f232,f96])).
% 0.12/0.40 fof(f373,plain,(
% 0.12/0.40 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~state(skc8,skc9)|~man(skc8,skc10)|~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skc10)|~forename(skc8,X2)|~jules_forename(skc8,X2)|~of(skc8,X2,skc10)|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~proposition(skc8,X3)|~accessible_world(skc8,X3)|~smoke(X3,X4)|~present(X3,X4)|~agent(X3,X4,skf4(X3))|~event(X3,X4)|~think_believe_consider(skc8,X5)|~present(skc8,X5)|~event(skc8,X5)|~theme(skc8,X5,X3)|~agent(skc8,X6,X7)|~agent(skc8,X5,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~vincent_forename(skc8,X8)|~forename(skc8,X8)|~theme(skc8,X6,X0)|~event(skc8,X6)|~present(skc8,X6)|~think_believe_consider(skc8,X6)|~actual_world(skc8))),
% 0.12/0.40 inference(resolution,[status(thm)],[f372,f221])).
% 0.12/0.40 fof(f374,plain,(
% 0.12/0.40 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~man(skc8,skc10)|~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skc10)|~forename(skc8,X2)|~jules_forename(skc8,X2)|~of(skc8,X2,skc10)|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~proposition(skc8,X3)|~accessible_world(skc8,X3)|~smoke(X3,X4)|~present(X3,X4)|~agent(X3,X4,skf4(X3))|~event(X3,X4)|~think_believe_consider(skc8,X5)|~present(skc8,X5)|~event(skc8,X5)|~theme(skc8,X5,X3)|~agent(skc8,X6,X7)|~agent(skc8,X5,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~vincent_forename(skc8,X8)|~forename(skc8,X8)|~theme(skc8,X6,X0)|~event(skc8,X6)|~present(skc8,X6)|~think_believe_consider(skc8,X6)|~actual_world(skc8))),
% 0.12/0.40 inference(forward_subsumption_resolution,[status(thm)],[f373,f214])).
% 0.12/0.40 fof(f492,plain,(
% 0.12/0.40 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skc10)|~forename(skc8,X2)|~jules_forename(skc8,X2)|~of(skc8,X2,skc10)|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~proposition(skc8,X3)|~accessible_world(skc8,X3)|~think_believe_consider(skc8,X4)|~present(skc8,X4)|~event(skc8,X4)|~theme(skc8,X4,X3)|~agent(skc8,X5,X6)|~agent(skc8,X4,X6)|~man(skc8,X6)|~of(skc8,X7,X6)|~vincent_forename(skc8,X7)|~forename(skc8,X7)|~theme(skc8,X5,X0)|~event(skc8,X5)|~present(skc8,X5)|~think_believe_consider(skc8,X5)|~actual_world(skc8)|man(X3,skf4(X3)))),
% 0.12/0.40 inference(forward_subsumption_resolution,[status(thm)],[f360,f213])).
% 0.12/0.40 fof(f493,plain,(
% 0.12/0.40 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skc10)|~forename(skc8,X2)|~jules_forename(skc8,X2)|~of(skc8,X2,skc10)|~accessible_world(skc8,X0)|~proposition(skc8,X0)|~proposition(skc8,X3)|~accessible_world(skc8,X3)|~smoke(X3,X4)|~present(X3,X4)|~agent(X3,X4,skf4(X3))|~event(X3,X4)|~think_believe_consider(skc8,X5)|~present(skc8,X5)|~event(skc8,X5)|~theme(skc8,X5,X3)|~agent(skc8,X6,X7)|~agent(skc8,X5,X7)|~man(skc8,X7)|~of(skc8,X8,X7)|~vincent_forename(skc8,X8)|~forename(skc8,X8)|~theme(skc8,X6,X0)|~event(skc8,X6)|~present(skc8,X6)|~think_believe_consider(skc8,X6)|~actual_world(skc8))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f374,f213])).
% 0.12/0.41 fof(f527,plain,(
% 0.12/0.41 ![X0,X1,X2,X3,X4,X5,X6]: (~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~forename(skc8,X0)|~jules_forename(skc8,X0)|~of(skc8,X0,skc10)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~proposition(skc8,X1)|~accessible_world(skc8,X1)|~smoke(X1,X2)|~present(X1,X2)|~agent(X1,X2,skf4(X1))|~event(X1,X2)|~think_believe_consider(skc8,X3)|~present(skc8,X3)|~event(skc8,X3)|~theme(skc8,X3,X1)|~agent(skc8,X4,X5)|~agent(skc8,X3,X5)|~man(skc8,X5)|~of(skc8,X6,X5)|~vincent_forename(skc8,X6)|~forename(skc8,X6)|~theme(skc8,X4,skc12)|~event(skc8,X4)|~present(skc8,X4)|~think_believe_consider(skc8,X4)|~actual_world(skc8))),
% 0.12/0.41 inference(resolution,[status(thm)],[f366,f493])).
% 0.12/0.41 fof(f528,plain,(
% 0.12/0.41 ![X0,X1,X2,X3,X4,X5]: (~smoke(skc12,skf2(skc10))|~present(skc12,skf2(skc10))|~forename(skc8,X0)|~jules_forename(skc8,X0)|~of(skc8,X0,skc10)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~proposition(skc8,X1)|~accessible_world(skc8,X1)|~think_believe_consider(skc8,X2)|~present(skc8,X2)|~event(skc8,X2)|~theme(skc8,X2,X1)|~agent(skc8,X3,X4)|~agent(skc8,X2,X4)|~man(skc8,X4)|~of(skc8,X5,X4)|~vincent_forename(skc8,X5)|~forename(skc8,X5)|~theme(skc8,X3,skc12)|~event(skc8,X3)|~present(skc8,X3)|~think_believe_consider(skc8,X3)|~actual_world(skc8)|man(X1,skf4(X1)))),
% 0.12/0.41 inference(resolution,[status(thm)],[f366,f492])).
% 0.12/0.41 fof(f529,plain,(
% 0.12/0.41 ![X0,X1,X2,X3,X4,X5,X6]: (~present(skc12,skf2(skc10))|~forename(skc8,X0)|~jules_forename(skc8,X0)|~of(skc8,X0,skc10)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~proposition(skc8,X1)|~accessible_world(skc8,X1)|~smoke(X1,X2)|~present(X1,X2)|~agent(X1,X2,skf4(X1))|~event(X1,X2)|~think_believe_consider(skc8,X3)|~present(skc8,X3)|~event(skc8,X3)|~theme(skc8,X3,X1)|~agent(skc8,X4,X5)|~agent(skc8,X3,X5)|~man(skc8,X5)|~of(skc8,X6,X5)|~vincent_forename(skc8,X6)|~forename(skc8,X6)|~theme(skc8,X4,skc12)|~event(skc8,X4)|~present(skc8,X4)|~think_believe_consider(skc8,X4)|~actual_world(skc8))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f527,f369])).
% 0.12/0.41 fof(f530,plain,(
% 0.12/0.41 ![X0,X1,X2,X3,X4,X5]: (~present(skc12,skf2(skc10))|~forename(skc8,X0)|~jules_forename(skc8,X0)|~of(skc8,X0,skc10)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~proposition(skc8,X1)|~accessible_world(skc8,X1)|~think_believe_consider(skc8,X2)|~present(skc8,X2)|~event(skc8,X2)|~theme(skc8,X2,X1)|~agent(skc8,X3,X4)|~agent(skc8,X2,X4)|~man(skc8,X4)|~of(skc8,X5,X4)|~vincent_forename(skc8,X5)|~forename(skc8,X5)|~theme(skc8,X3,skc12)|~event(skc8,X3)|~present(skc8,X3)|~think_believe_consider(skc8,X3)|~actual_world(skc8)|man(X1,skf4(X1)))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f528,f369])).
% 0.12/0.41 fof(f544,plain,(
% 0.12/0.41 ![X0,X1,X2,X3,X4,X5]: (~forename(skc8,X0)|~jules_forename(skc8,X0)|~of(skc8,X0,skc10)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~proposition(skc8,X1)|~accessible_world(skc8,X1)|~think_believe_consider(skc8,X2)|~present(skc8,X2)|~event(skc8,X2)|~theme(skc8,X2,X1)|~agent(skc8,X3,X4)|~agent(skc8,X2,X4)|~man(skc8,X4)|~of(skc8,X5,X4)|~vincent_forename(skc8,X5)|~forename(skc8,X5)|~theme(skc8,X3,skc12)|~event(skc8,X3)|~present(skc8,X3)|~think_believe_consider(skc8,X3)|~actual_world(skc8)|man(X1,skf4(X1)))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f530,f368])).
% 0.12/0.41 fof(f545,plain,(
% 0.12/0.41 ![X0,X1,X2,X3,X4]: (~forename(skc8,skc11)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~proposition(skc8,X0)|~accessible_world(skc8,X0)|~think_believe_consider(skc8,X1)|~present(skc8,X1)|~event(skc8,X1)|~theme(skc8,X1,X0)|~agent(skc8,X2,X3)|~agent(skc8,X1,X3)|~man(skc8,X3)|~of(skc8,X4,X3)|~vincent_forename(skc8,X4)|~forename(skc8,X4)|~theme(skc8,X2,skc12)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~actual_world(skc8)|man(X0,skf4(X0)))),
% 0.12/0.41 inference(resolution,[status(thm)],[f544,f220])).
% 0.12/0.41 fof(f546,plain,(
% 0.12/0.41 ![X0,X1,X2,X3,X4]: (~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~proposition(skc8,X0)|~accessible_world(skc8,X0)|~think_believe_consider(skc8,X1)|~present(skc8,X1)|~event(skc8,X1)|~theme(skc8,X1,X0)|~agent(skc8,X2,X3)|~agent(skc8,X1,X3)|~man(skc8,X3)|~of(skc8,X4,X3)|~vincent_forename(skc8,X4)|~forename(skc8,X4)|~theme(skc8,X2,skc12)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~actual_world(skc8)|man(X0,skf4(X0)))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f545,f125])).
% 0.12/0.41 fof(f547,plain,(
% 0.12/0.41 ![X0,X1,X2,X3,X4]: (~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~proposition(skc8,X0)|~accessible_world(skc8,X0)|~think_believe_consider(skc8,X1)|~present(skc8,X1)|~event(skc8,X1)|~theme(skc8,X1,X0)|~agent(skc8,X2,X3)|~agent(skc8,X1,X3)|~man(skc8,X3)|~of(skc8,X4,X3)|~vincent_forename(skc8,X4)|~forename(skc8,X4)|~theme(skc8,X2,skc12)|~event(skc8,X2)|~present(skc8,X2)|~think_believe_consider(skc8,X2)|~actual_world(skc8)|man(X0,skf4(X0)))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f546,f211])).
% 0.12/0.41 fof(f548,plain,(
% 0.12/0.41 ![X0,X1,X2]: (~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~agent(skc8,X0,X1)|~agent(skc8,skc13,X1)|~man(skc8,X1)|~of(skc8,X2,X1)|~vincent_forename(skc8,X2)|~forename(skc8,X2)|~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.12/0.41 inference(resolution,[status(thm)],[f547,f219])).
% 0.12/0.41 fof(f549,plain,(
% 0.12/0.41 ![X0,X1,X2]: (~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~agent(skc8,X0,X1)|~agent(skc8,skc13,X1)|~man(skc8,X1)|~of(skc8,X2,X1)|~vincent_forename(skc8,X2)|~forename(skc8,X2)|~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.12/0.41 inference(duplicate_literals_removal,[status(thm)],[f548])).
% 0.12/0.41 fof(f550,plain,(
% 0.12/0.41 ![X0,X1,X2]: (~proposition(skc8,skc12)|~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~agent(skc8,X0,X1)|~agent(skc8,skc13,X1)|~man(skc8,X1)|~of(skc8,X2,X1)|~vincent_forename(skc8,X2)|~forename(skc8,X2)|~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f549,f215])).
% 0.12/0.41 fof(f551,plain,(
% 0.12/0.41 ![X0,X1,X2]: (~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~agent(skc8,X0,X1)|~agent(skc8,skc13,X1)|~man(skc8,X1)|~of(skc8,X2,X1)|~vincent_forename(skc8,X2)|~forename(skc8,X2)|~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f550,f216])).
% 0.12/0.41 fof(f552,plain,(
% 0.12/0.41 ![X0]: (~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~of(skc8,X0,skc15)|~vincent_forename(skc8,X0)|~forename(skc8,X0)|~theme(skc8,skc13,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.12/0.41 inference(resolution,[status(thm)],[f551,f218])).
% 0.12/0.41 fof(f553,plain,(
% 0.12/0.41 ![X0]: (~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~of(skc8,X0,skc15)|~vincent_forename(skc8,X0)|~forename(skc8,X0)|~theme(skc8,skc13,skc12)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.12/0.41 inference(duplicate_literals_removal,[status(thm)],[f552])).
% 0.12/0.41 fof(f554,plain,(
% 0.12/0.41 ![X0]: (~present(skc8,skc13)|~event(skc8,skc13)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~of(skc8,X0,skc15)|~vincent_forename(skc8,X0)|~forename(skc8,X0)|~theme(skc8,skc13,skc12)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f553,f210])).
% 0.12/0.41 fof(f555,plain,(
% 0.12/0.41 ![X0]: (~event(skc8,skc13)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~of(skc8,X0,skc15)|~vincent_forename(skc8,X0)|~forename(skc8,X0)|~theme(skc8,skc13,skc12)|~actual_world(skc8)|man(skc12,skf4(skc12)))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f554,f209])).
% 0.12/0.41 fof(f556,plain,(
% 0.12/0.41 ~event(skc8,skc13)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~theme(skc8,skc13,skc12)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.12/0.41 inference(resolution,[status(thm)],[f555,f217])).
% 0.12/0.41 fof(f557,plain,(
% 0.12/0.41 ~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~theme(skc8,skc13,skc12)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f556,f208])).
% 0.12/0.41 fof(f558,plain,(
% 0.12/0.41 ~man(skc8,skc15)|~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~theme(skc8,skc13,skc12)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f557,f218])).
% 0.12/0.41 fof(f559,plain,(
% 0.12/0.41 ~man(skc8,skc15)|~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.12/0.41 inference(resolution,[status(thm)],[f558,f219])).
% 0.12/0.41 fof(f560,plain,(
% 0.12/0.41 ~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f559,f205])).
% 0.12/0.41 fof(f567,plain,(
% 0.12/0.41 ![X0,X1,X2,X3,X4,X5,X6]: (~forename(skc8,X0)|~jules_forename(skc8,X0)|~of(skc8,X0,skc10)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~proposition(skc8,X1)|~accessible_world(skc8,X1)|~smoke(X1,X2)|~present(X1,X2)|~agent(X1,X2,skf4(X1))|~event(X1,X2)|~think_believe_consider(skc8,X3)|~present(skc8,X3)|~event(skc8,X3)|~theme(skc8,X3,X1)|~agent(skc8,X4,X5)|~agent(skc8,X3,X5)|~man(skc8,X5)|~of(skc8,X6,X5)|~vincent_forename(skc8,X6)|~forename(skc8,X6)|~theme(skc8,X4,skc12)|~event(skc8,X4)|~present(skc8,X4)|~think_believe_consider(skc8,X4)|~actual_world(skc8))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f529,f368])).
% 0.12/0.41 fof(f568,plain,(
% 0.12/0.41 ![X0,X1,X2,X3,X4,X5]: (~forename(skc8,skc11)|~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~proposition(skc8,X0)|~accessible_world(skc8,X0)|~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~event(X0,X1)|~think_believe_consider(skc8,X2)|~present(skc8,X2)|~event(skc8,X2)|~theme(skc8,X2,X0)|~agent(skc8,X3,X4)|~agent(skc8,X2,X4)|~man(skc8,X4)|~of(skc8,X5,X4)|~vincent_forename(skc8,X5)|~forename(skc8,X5)|~theme(skc8,X3,skc12)|~event(skc8,X3)|~present(skc8,X3)|~think_believe_consider(skc8,X3)|~actual_world(skc8))),
% 0.12/0.41 inference(resolution,[status(thm)],[f567,f220])).
% 0.12/0.41 fof(f569,plain,(
% 0.12/0.41 ![X0,X1,X2,X3,X4,X5]: (~jules_forename(skc8,skc11)|~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~proposition(skc8,X0)|~accessible_world(skc8,X0)|~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~event(X0,X1)|~think_believe_consider(skc8,X2)|~present(skc8,X2)|~event(skc8,X2)|~theme(skc8,X2,X0)|~agent(skc8,X3,X4)|~agent(skc8,X2,X4)|~man(skc8,X4)|~of(skc8,X5,X4)|~vincent_forename(skc8,X5)|~forename(skc8,X5)|~theme(skc8,X3,skc12)|~event(skc8,X3)|~present(skc8,X3)|~think_believe_consider(skc8,X3)|~actual_world(skc8))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f568,f125])).
% 0.12/0.41 fof(f570,plain,(
% 0.12/0.41 ~forename(skc8,skc14)|~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f560,f207])).
% 0.12/0.41 fof(f571,plain,(
% 0.12/0.41 ~actual_world(skc8)|man(skc12,skf4(skc12))),
% 0.12/0.41 inference(resolution,[status(thm)],[f570,f206])).
% 0.12/0.41 fof(f572,plain,(
% 0.12/0.41 man(skc12,skf4(skc12))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f571,f204])).
% 0.12/0.41 fof(f573,plain,(
% 0.12/0.41 agent(skc12,skf2(skf4(skc12)),skf4(skc12))),
% 0.12/0.41 inference(resolution,[status(thm)],[f572,f228])).
% 0.12/0.41 fof(f586,plain,(
% 0.12/0.41 ![X0,X1,X2,X3,X4,X5]: (~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~proposition(skc8,X0)|~accessible_world(skc8,X0)|~smoke(X0,X1)|~present(X0,X1)|~agent(X0,X1,skf4(X0))|~event(X0,X1)|~think_believe_consider(skc8,X2)|~present(skc8,X2)|~event(skc8,X2)|~theme(skc8,X2,X0)|~agent(skc8,X3,X4)|~agent(skc8,X2,X4)|~man(skc8,X4)|~of(skc8,X5,X4)|~vincent_forename(skc8,X5)|~forename(skc8,X5)|~theme(skc8,X3,skc12)|~event(skc8,X3)|~present(skc8,X3)|~think_believe_consider(skc8,X3)|~actual_world(skc8))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f569,f211])).
% 0.12/0.41 fof(f599,plain,(
% 0.12/0.41 ![X0,X1,X2,X3]: (~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~proposition(skc8,skc12)|~accessible_world(skc8,skc12)|~smoke(skc12,skf2(skf4(skc12)))|~present(skc12,skf2(skf4(skc12)))|~event(skc12,skf2(skf4(skc12)))|~think_believe_consider(skc8,X0)|~present(skc8,X0)|~event(skc8,X0)|~theme(skc8,X0,skc12)|~agent(skc8,X1,X2)|~agent(skc8,X0,X2)|~man(skc8,X2)|~of(skc8,X3,X2)|~vincent_forename(skc8,X3)|~forename(skc8,X3)|~theme(skc8,X1,skc12)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~actual_world(skc8))),
% 0.12/0.41 inference(resolution,[status(thm)],[f573,f586])).
% 0.12/0.41 fof(f602,plain,(
% 0.12/0.41 ![X0,X1,X2,X3]: (~accessible_world(skc8,skc12)|~proposition(skc8,skc12)|~smoke(skc12,skf2(skf4(skc12)))|~present(skc12,skf2(skf4(skc12)))|~event(skc12,skf2(skf4(skc12)))|~think_believe_consider(skc8,X0)|~present(skc8,X0)|~event(skc8,X0)|~theme(skc8,X0,skc12)|~agent(skc8,X1,X2)|~agent(skc8,X0,X2)|~man(skc8,X2)|~of(skc8,X3,X2)|~vincent_forename(skc8,X3)|~forename(skc8,X3)|~theme(skc8,X1,skc12)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~actual_world(skc8))),
% 0.12/0.41 inference(duplicate_literals_removal,[status(thm)],[f599])).
% 0.12/0.41 fof(f603,plain,(
% 0.12/0.41 ![X0,X1,X2,X3]: (~proposition(skc8,skc12)|~smoke(skc12,skf2(skf4(skc12)))|~present(skc12,skf2(skf4(skc12)))|~event(skc12,skf2(skf4(skc12)))|~think_believe_consider(skc8,X0)|~present(skc8,X0)|~event(skc8,X0)|~theme(skc8,X0,skc12)|~agent(skc8,X1,X2)|~agent(skc8,X0,X2)|~man(skc8,X2)|~of(skc8,X3,X2)|~vincent_forename(skc8,X3)|~forename(skc8,X3)|~theme(skc8,X1,skc12)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~actual_world(skc8))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f602,f215])).
% 0.12/0.41 fof(f612,plain,(
% 0.12/0.41 ![X0,X1,X2,X3]: (~smoke(skc12,skf2(skf4(skc12)))|~present(skc12,skf2(skf4(skc12)))|~event(skc12,skf2(skf4(skc12)))|~think_believe_consider(skc8,X0)|~present(skc8,X0)|~event(skc8,X0)|~theme(skc8,X0,skc12)|~agent(skc8,X1,X2)|~agent(skc8,X0,X2)|~man(skc8,X2)|~of(skc8,X3,X2)|~vincent_forename(skc8,X3)|~forename(skc8,X3)|~theme(skc8,X1,skc12)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~actual_world(skc8))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f603,f216])).
% 0.12/0.41 fof(f613,plain,(
% 0.12/0.41 ![X0,X1,X2,X3]: (~smoke(skc12,skf2(skf4(skc12)))|~event(skc12,skf2(skf4(skc12)))|~think_believe_consider(skc8,X0)|~present(skc8,X0)|~event(skc8,X0)|~theme(skc8,X0,skc12)|~agent(skc8,X1,X2)|~agent(skc8,X0,X2)|~man(skc8,X2)|~of(skc8,X3,X2)|~vincent_forename(skc8,X3)|~forename(skc8,X3)|~theme(skc8,X1,skc12)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~actual_world(skc8))),
% 0.12/0.41 inference(resolution,[status(thm)],[f612,f368])).
% 0.12/0.41 fof(f614,plain,(
% 0.12/0.41 ![X0,X1,X2,X3]: (~event(skc12,skf2(skf4(skc12)))|~think_believe_consider(skc8,X0)|~present(skc8,X0)|~event(skc8,X0)|~theme(skc8,X0,skc12)|~agent(skc8,X1,X2)|~agent(skc8,X0,X2)|~man(skc8,X2)|~of(skc8,X3,X2)|~vincent_forename(skc8,X3)|~forename(skc8,X3)|~theme(skc8,X1,skc12)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~actual_world(skc8))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f613,f369])).
% 0.12/0.41 fof(f615,plain,(
% 0.12/0.41 ![X0,X1,X2,X3]: (~think_believe_consider(skc8,X0)|~present(skc8,X0)|~event(skc8,X0)|~theme(skc8,X0,skc12)|~agent(skc8,X1,X2)|~agent(skc8,X0,X2)|~man(skc8,X2)|~of(skc8,X3,X2)|~vincent_forename(skc8,X3)|~forename(skc8,X3)|~theme(skc8,X1,skc12)|~event(skc8,X1)|~present(skc8,X1)|~think_believe_consider(skc8,X1)|~actual_world(skc8))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f614,f367])).
% 0.12/0.41 fof(f616,plain,(
% 0.12/0.41 ![X0,X1,X2]: (~think_believe_consider(skc8,skc13)|~present(skc8,skc13)|~event(skc8,skc13)|~agent(skc8,X0,X1)|~agent(skc8,skc13,X1)|~man(skc8,X1)|~of(skc8,X2,X1)|~vincent_forename(skc8,X2)|~forename(skc8,X2)|~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~actual_world(skc8))),
% 0.12/0.42 inference(resolution,[status(thm)],[f615,f219])).
% 0.12/0.42 fof(f617,plain,(
% 0.12/0.42 ![X0,X1,X2]: (~present(skc8,skc13)|~event(skc8,skc13)|~agent(skc8,X0,X1)|~agent(skc8,skc13,X1)|~man(skc8,X1)|~of(skc8,X2,X1)|~vincent_forename(skc8,X2)|~forename(skc8,X2)|~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~actual_world(skc8))),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f616,f210])).
% 0.12/0.42 fof(f618,plain,(
% 0.12/0.42 ![X0,X1,X2]: (~event(skc8,skc13)|~agent(skc8,X0,X1)|~agent(skc8,skc13,X1)|~man(skc8,X1)|~of(skc8,X2,X1)|~vincent_forename(skc8,X2)|~forename(skc8,X2)|~theme(skc8,X0,skc12)|~event(skc8,X0)|~present(skc8,X0)|~think_believe_consider(skc8,X0)|~actual_world(skc8))),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f617,f209])).
% 0.12/0.42 fof(f619,plain,(
% 0.12/0.42 ![X0]: (~event(skc8,skc13)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~of(skc8,X0,skc15)|~vincent_forename(skc8,X0)|~forename(skc8,X0)|~theme(skc8,skc13,skc12)|~event(skc8,skc13)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8))),
% 0.12/0.42 inference(resolution,[status(thm)],[f618,f218])).
% 0.12/0.42 fof(f620,plain,(
% 0.12/0.42 ![X0]: (~event(skc8,skc13)|~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~of(skc8,X0,skc15)|~vincent_forename(skc8,X0)|~forename(skc8,X0)|~theme(skc8,skc13,skc12)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8))),
% 0.12/0.42 inference(duplicate_literals_removal,[status(thm)],[f619])).
% 0.12/0.42 fof(f621,plain,(
% 0.12/0.42 ![X0]: (~agent(skc8,skc13,skc15)|~man(skc8,skc15)|~of(skc8,X0,skc15)|~vincent_forename(skc8,X0)|~forename(skc8,X0)|~theme(skc8,skc13,skc12)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8))),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f620,f208])).
% 0.12/0.42 fof(f622,plain,(
% 0.12/0.42 ![X0]: (~man(skc8,skc15)|~of(skc8,X0,skc15)|~vincent_forename(skc8,X0)|~forename(skc8,X0)|~theme(skc8,skc13,skc12)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8))),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f621,f218])).
% 0.12/0.42 fof(f623,plain,(
% 0.12/0.42 ~man(skc8,skc15)|~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~theme(skc8,skc13,skc12)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)),
% 0.12/0.42 inference(resolution,[status(thm)],[f622,f217])).
% 0.12/0.42 fof(f624,plain,(
% 0.12/0.42 ~vincent_forename(skc8,skc14)|~forename(skc8,skc14)|~theme(skc8,skc13,skc12)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f623,f205])).
% 0.12/0.42 fof(f625,plain,(
% 0.12/0.42 ~forename(skc8,skc14)|~theme(skc8,skc13,skc12)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f624,f207])).
% 0.12/0.42 fof(f626,plain,(
% 0.12/0.42 ~forename(skc8,skc14)|~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)),
% 0.12/0.42 inference(resolution,[status(thm)],[f625,f219])).
% 0.12/0.42 fof(f627,plain,(
% 0.12/0.42 ~present(skc8,skc13)|~think_believe_consider(skc8,skc13)|~actual_world(skc8)),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f626,f206])).
% 0.12/0.42 fof(f628,plain,(
% 0.12/0.42 ~think_believe_consider(skc8,skc13)|~actual_world(skc8)),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f627,f209])).
% 0.12/0.42 fof(f629,plain,(
% 0.12/0.42 ~actual_world(skc8)),
% 0.12/0.42 inference(resolution,[status(thm)],[f628,f210])).
% 0.12/0.42 fof(f630,plain,(
% 0.12/0.42 $false),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f629,f204])).
% 0.12/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.44 % Elapsed time: 0.067203 seconds
% 0.12/0.44 % CPU time: 0.283573 seconds
% 0.12/0.44 % Total memory used: 49.001 MB
% 0.12/0.44 % Net memory used: 48.797 MB
%------------------------------------------------------------------------------