%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NLP258+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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:31:40 PM UTC 2026
% Result : Theorem 0.12s 0.42s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 5
% Syntax : Number of formulae : 119 ( 27 unt; 0 def)
% Number of atoms : 1806 ( 0 equ)
% Maximal formula atoms : 65 ( 15 avg)
% Number of connectives : 3212 (1525 ~;1482 |; 197 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 55 ( 18 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 17 ( 16 usr; 1 prp; 0-4 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-8 aty)
% Number of variables : 501 ( 435 !; 66 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [U,V] :
( jules_forename(U,V)
=> forename(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [U,V] :
( vincent_forename(U,V)
=> forename(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [U,V] :
( smoke(U,V)
=> event(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [U,V,W] :
( ( man(V,U)
& accessible_world(V,W) )
=> man(W,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,conjecture,
~ ( ~ ? [X5] :
( ? [X6,X7,V,W,X,Y,Z,X1,X2,X8,X9] :
( ? [X10] :
( smoke(X9,X10)
& present(X9,X10)
& agent(X9,X10,X1)
& event(X9,X10) )
& accessible_world(X5,X9)
& think_believe_consider(X5,X8)
& present(X5,X8)
& event(X5,X8)
& theme(X5,X8,X9)
& agent(X5,X8,V)
& proposition(X5,X9)
& be(X5,X2,X1,X1)
& state(X5,X2)
& man(X5,X1)
& forename(X5,Z)
& jules_forename(X5,Z)
& man(X5,X1)
& of(X5,Z,X1)
& ! [X3] :
( man(Y,X3)
=> ? [X4] :
( smoke(Y,X4)
& present(Y,X4)
& agent(Y,X4,X3)
& event(Y,X4) ) )
& accessible_world(X5,Y)
& think_believe_consider(X5,X)
& present(X5,X)
& event(X5,X)
& theme(X5,X,Y)
& agent(X5,X,V)
& proposition(X5,Y)
& forename(X5,W)
& vincent_forename(X5,W)
& man(X5,V)
& of(X5,W,V)
& forename(X5,X7)
& vincent_forename(X5,X7)
& of(X5,X7,V)
& forename(X5,X6)
& jules_forename(X5,X6)
& of(X5,X6,X1) )
& actual_world(X5) )
& ? [U] :
( ? [V,W,X,Y,Z,X1,X2] :
( be(U,X2,X1,X1)
& state(U,X2)
& man(U,X1)
& forename(U,Z)
& jules_forename(U,Z)
& man(U,X1)
& of(U,Z,X1)
& ! [X3] :
( man(Y,X3)
=> ? [X4] :
( smoke(Y,X4)
& present(Y,X4)
& agent(Y,X4,X3)
& event(Y,X4) ) )
& accessible_world(U,Y)
& think_believe_consider(U,X)
& present(U,X)
& event(U,X)
& theme(U,X,Y)
& agent(U,X,V)
& proposition(U,Y)
& forename(U,W)
& vincent_forename(U,W)
& man(U,V)
& of(U,W,V) )
& actual_world(U) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,negated_conjecture,
~ ~ ( ~ ? [X5] :
( ? [X6,X7,V,W,X,Y,Z,X1,X2,X8,X9] :
( ? [X10] :
( smoke(X9,X10)
& present(X9,X10)
& agent(X9,X10,X1)
& event(X9,X10) )
& accessible_world(X5,X9)
& think_believe_consider(X5,X8)
& present(X5,X8)
& event(X5,X8)
& theme(X5,X8,X9)
& agent(X5,X8,V)
& proposition(X5,X9)
& be(X5,X2,X1,X1)
& state(X5,X2)
& man(X5,X1)
& forename(X5,Z)
& jules_forename(X5,Z)
& man(X5,X1)
& of(X5,Z,X1)
& ! [X3] :
( man(Y,X3)
=> ? [X4] :
( smoke(Y,X4)
& present(Y,X4)
& agent(Y,X4,X3)
& event(Y,X4) ) )
& accessible_world(X5,Y)
& think_believe_consider(X5,X)
& present(X5,X)
& event(X5,X)
& theme(X5,X,Y)
& agent(X5,X,V)
& proposition(X5,Y)
& forename(X5,W)
& vincent_forename(X5,W)
& man(X5,V)
& of(X5,W,V)
& forename(X5,X7)
& vincent_forename(X5,X7)
& of(X5,X7,V)
& forename(X5,X6)
& jules_forename(X5,X6)
& of(X5,X6,X1) )
& actual_world(X5) )
& ? [U] :
( ? [V,W,X,Y,Z,X1,X2] :
( be(U,X2,X1,X1)
& state(U,X2)
& man(U,X1)
& forename(U,Z)
& jules_forename(U,Z)
& man(U,X1)
& of(U,Z,X1)
& ! [X3] :
( man(Y,X3)
=> ? [X4] :
( smoke(Y,X4)
& present(Y,X4)
& agent(Y,X4,X3)
& event(Y,X4) ) )
& accessible_world(U,Y)
& think_believe_consider(U,X)
& present(U,X)
& event(U,X)
& theme(U,X,Y)
& agent(U,X,V)
& proposition(U,Y)
& forename(U,W)
& vincent_forename(U,W)
& man(U,V)
& of(U,W,V) )
& actual_world(U) ) ),
inference(negated_conjecture,[status(cth)],[f72]) ).
fof(f74,plain,
! [U,V] :
( forename(U,V)
| ~ jules_forename(U,V) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f75,plain,
! [X0,X1] :
( forename(X0,X1)
| ~ jules_forename(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f76,plain,
! [U,V] :
( forename(U,V)
| ~ vincent_forename(U,V) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f77,plain,
! [X0,X1] :
( forename(X0,X1)
| ~ vincent_forename(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f132,plain,
! [U,V] :
( event(U,V)
| ~ smoke(U,V) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f133,plain,
! [X0,X1] :
( event(X0,X1)
| ~ smoke(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f184,plain,
! [U,V,W] :
( man(W,U)
| ~ man(V,U)
| ~ accessible_world(V,W) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f185,plain,
! [U,W] :
( man(W,U)
| ! [V] :
( ~ man(V,U)
| ~ accessible_world(V,W) ) ),
inference(miniscoping,[status(thm)],[f184]) ).
fof(f186,plain,
! [X0,X1,X2] :
( man(X1,X2)
| ~ man(X0,X2)
| ~ accessible_world(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f252,plain,
( ! [X5] :
( ! [X6,X7,V,W,X,Y,Z,X1,X2,X8,X9] :
( ! [X10] :
( ~ smoke(X9,X10)
| ~ present(X9,X10)
| ~ agent(X9,X10,X1)
| ~ event(X9,X10) )
| ~ accessible_world(X5,X9)
| ~ think_believe_consider(X5,X8)
| ~ present(X5,X8)
| ~ event(X5,X8)
| ~ theme(X5,X8,X9)
| ~ agent(X5,X8,V)
| ~ proposition(X5,X9)
| ~ be(X5,X2,X1,X1)
| ~ state(X5,X2)
| ~ man(X5,X1)
| ~ forename(X5,Z)
| ~ jules_forename(X5,Z)
| ~ man(X5,X1)
| ~ of(X5,Z,X1)
| ? [X3] :
( ! [X4] :
( ~ smoke(Y,X4)
| ~ present(Y,X4)
| ~ agent(Y,X4,X3)
| ~ event(Y,X4) )
& man(Y,X3) )
| ~ accessible_world(X5,Y)
| ~ think_believe_consider(X5,X)
| ~ present(X5,X)
| ~ event(X5,X)
| ~ theme(X5,X,Y)
| ~ agent(X5,X,V)
| ~ proposition(X5,Y)
| ~ forename(X5,W)
| ~ vincent_forename(X5,W)
| ~ man(X5,V)
| ~ of(X5,W,V)
| ~ forename(X5,X7)
| ~ vincent_forename(X5,X7)
| ~ of(X5,X7,V)
| ~ forename(X5,X6)
| ~ jules_forename(X5,X6)
| ~ of(X5,X6,X1) )
| ~ actual_world(X5) )
& ? [U] :
( ? [V,W,X,Y,Z,X1,X2] :
( be(U,X2,X1,X1)
& state(U,X2)
& man(U,X1)
& forename(U,Z)
& jules_forename(U,Z)
& man(U,X1)
& of(U,Z,X1)
& ! [X3] :
( ? [X4] :
( smoke(Y,X4)
& present(Y,X4)
& agent(Y,X4,X3)
& event(Y,X4) )
| ~ man(Y,X3) )
& accessible_world(U,Y)
& think_believe_consider(U,X)
& present(U,X)
& event(U,X)
& theme(U,X,Y)
& agent(U,X,V)
& proposition(U,Y)
& forename(U,W)
& vincent_forename(U,W)
& man(U,V)
& of(U,W,V) )
& actual_world(U) ) ),
inference(pre_NNF_transformation,[status(thm)],[f73]) ).
fof(f253,plain,
( ! [X5] :
( ! [X1,X9] :
( ! [X10] :
( ~ smoke(X9,X10)
| ~ present(X9,X10)
| ~ agent(X9,X10,X1)
| ~ event(X9,X10) )
| ~ accessible_world(X5,X9)
| ! [X8] :
( ~ think_believe_consider(X5,X8)
| ~ present(X5,X8)
| ~ event(X5,X8)
| ~ theme(X5,X8,X9)
| ! [V] :
( ~ agent(X5,X8,V)
| ~ proposition(X5,X9)
| ! [X2] :
( ~ be(X5,X2,X1,X1)
| ~ state(X5,X2)
| ~ man(X5,X1)
| ! [Z] :
( ~ forename(X5,Z)
| ~ jules_forename(X5,Z)
| ~ man(X5,X1)
| ~ of(X5,Z,X1)
| ! [Y] :
( ? [X3] :
( ! [X4] :
( ~ smoke(Y,X4)
| ~ present(Y,X4)
| ~ agent(Y,X4,X3)
| ~ event(Y,X4) )
& man(Y,X3) )
| ~ accessible_world(X5,Y)
| ! [X] :
( ~ think_believe_consider(X5,X)
| ~ present(X5,X)
| ~ event(X5,X)
| ~ theme(X5,X,Y)
| ~ agent(X5,X,V)
| ~ proposition(X5,Y)
| ! [W] :
( ~ forename(X5,W)
| ~ vincent_forename(X5,W)
| ~ man(X5,V)
| ~ of(X5,W,V)
| ! [X7] :
( ~ forename(X5,X7)
| ~ vincent_forename(X5,X7)
| ~ of(X5,X7,V)
| ! [X6] :
( ~ forename(X5,X6)
| ~ jules_forename(X5,X6)
| ~ of(X5,X6,X1) ) ) ) ) ) ) ) ) ) )
| ~ actual_world(X5) )
& ? [U] :
( ? [X1,X2] :
( be(U,X2,X1,X1)
& state(U,X2)
& man(U,X1)
& ? [Z] :
( forename(U,Z)
& jules_forename(U,Z)
& man(U,X1)
& of(U,Z,X1)
& ? [Y] :
( ! [X3] :
( ? [X4] :
( smoke(Y,X4)
& present(Y,X4)
& agent(Y,X4,X3)
& event(Y,X4) )
| ~ man(Y,X3) )
& accessible_world(U,Y)
& ? [X] :
( think_believe_consider(U,X)
& present(U,X)
& event(U,X)
& theme(U,X,Y)
& ? [V] :
( agent(U,X,V)
& proposition(U,Y)
& ? [W] :
( forename(U,W)
& vincent_forename(U,W)
& man(U,V)
& of(U,W,V) ) ) ) ) ) )
& actual_world(U) ) ),
inference(miniscoping,[status(thm)],[f252]) ).
fof(f254,plain,
( ! [X5] :
( ! [X1,X9] :
( ! [X10] :
( ~ smoke(X9,X10)
| ~ present(X9,X10)
| ~ agent(X9,X10,X1)
| ~ event(X9,X10) )
| ~ accessible_world(X5,X9)
| ! [X8] :
( ~ think_believe_consider(X5,X8)
| ~ present(X5,X8)
| ~ event(X5,X8)
| ~ theme(X5,X8,X9)
| ! [V] :
( ~ agent(X5,X8,V)
| ~ proposition(X5,X9)
| ! [X2] :
( ~ be(X5,X2,X1,X1)
| ~ state(X5,X2)
| ~ man(X5,X1)
| ! [Z] :
( ~ forename(X5,Z)
| ~ jules_forename(X5,Z)
| ~ man(X5,X1)
| ~ of(X5,Z,X1)
| ! [Y] :
( ( ! [X4] :
( ~ smoke(Y,X4)
| ~ present(Y,X4)
| ~ agent(Y,X4,sK9_skl(Y,Z,X2,V,X8,X9,X1,X5))
| ~ event(Y,X4) )
& man(Y,sK9_skl(Y,Z,X2,V,X8,X9,X1,X5)) )
| ~ accessible_world(X5,Y)
| ! [X] :
( ~ think_believe_consider(X5,X)
| ~ present(X5,X)
| ~ event(X5,X)
| ~ theme(X5,X,Y)
| ~ agent(X5,X,V)
| ~ proposition(X5,Y)
| ! [W] :
( ~ forename(X5,W)
| ~ vincent_forename(X5,W)
| ~ man(X5,V)
| ~ of(X5,W,V)
| ! [X7] :
( ~ forename(X5,X7)
| ~ vincent_forename(X5,X7)
| ~ of(X5,X7,V)
| ! [X6] :
( ~ forename(X5,X6)
| ~ jules_forename(X5,X6)
| ~ of(X5,X6,X1) ) ) ) ) ) ) ) ) ) )
| ~ actual_world(X5) )
& be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)
& state(sK0_skl,sK2_skl)
& man(sK0_skl,sK1_skl)
& forename(sK0_skl,sK3_skl)
& jules_forename(sK0_skl,sK3_skl)
& man(sK0_skl,sK1_skl)
& of(sK0_skl,sK3_skl,sK1_skl)
& ! [X3] :
( ( smoke(sK4_skl,sK8_skl(X3))
& present(sK4_skl,sK8_skl(X3))
& agent(sK4_skl,sK8_skl(X3),X3)
& event(sK4_skl,sK8_skl(X3)) )
| ~ man(sK4_skl,X3) )
& accessible_world(sK0_skl,sK4_skl)
& think_believe_consider(sK0_skl,sK5_skl)
& present(sK0_skl,sK5_skl)
& event(sK0_skl,sK5_skl)
& theme(sK0_skl,sK5_skl,sK4_skl)
& agent(sK0_skl,sK5_skl,sK6_skl)
& proposition(sK0_skl,sK4_skl)
& forename(sK0_skl,sK7_skl)
& vincent_forename(sK0_skl,sK7_skl)
& man(sK0_skl,sK6_skl)
& of(sK0_skl,sK7_skl,sK6_skl)
& actual_world(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl]),skolemize(U,sK0_skl),skolemize(X1,sK1_skl),skolemize(X2,sK2_skl),skolemize(Z,sK3_skl),skolemize(Y,sK4_skl),skolemize(X,sK5_skl),skolemize(V,sK6_skl),skolemize(W,sK7_skl),skolemize(X4,sK8_skl(X3)),skolemize(X3,sK9_skl(Y,Z,X2,V,X8,X9,X1,X5))],[f253]) ).
fof(f255,plain,
actual_world(sK0_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f256,plain,
of(sK0_skl,sK7_skl,sK6_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f257,plain,
man(sK0_skl,sK6_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f258,plain,
vincent_forename(sK0_skl,sK7_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f260,plain,
proposition(sK0_skl,sK4_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f261,plain,
agent(sK0_skl,sK5_skl,sK6_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f262,plain,
theme(sK0_skl,sK5_skl,sK4_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f263,plain,
event(sK0_skl,sK5_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f264,plain,
present(sK0_skl,sK5_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f265,plain,
think_believe_consider(sK0_skl,sK5_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f266,plain,
accessible_world(sK0_skl,sK4_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f268,plain,
! [X0] :
( agent(sK4_skl,sK8_skl(X0),X0)
| ~ man(sK4_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f269,plain,
! [X0] :
( present(sK4_skl,sK8_skl(X0))
| ~ man(sK4_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f270,plain,
! [X0] :
( smoke(sK4_skl,sK8_skl(X0))
| ~ man(sK4_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f271,plain,
of(sK0_skl,sK3_skl,sK1_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f272,plain,
man(sK0_skl,sK1_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f273,plain,
jules_forename(sK0_skl,sK3_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f274,plain,
forename(sK0_skl,sK3_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f276,plain,
state(sK0_skl,sK2_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f277,plain,
be(sK0_skl,sK2_skl,sK1_skl,sK1_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f278,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( ~ smoke(X11,X12)
| ~ present(X11,X12)
| ~ agent(X11,X12,X2)
| ~ event(X11,X12)
| ~ accessible_world(X0,X11)
| ~ think_believe_consider(X0,X10)
| ~ present(X0,X10)
| ~ event(X0,X10)
| ~ theme(X0,X10,X11)
| ~ agent(X0,X10,X4)
| ~ proposition(X0,X11)
| ~ be(X0,X9,X2,X2)
| ~ state(X0,X9)
| ~ man(X0,X2)
| ~ forename(X0,X8)
| ~ jules_forename(X0,X8)
| ~ man(X0,X2)
| ~ of(X0,X8,X2)
| man(X6,sK9_skl(X6,X8,X9,X4,X10,X11,X2,X0))
| ~ accessible_world(X0,X6)
| ~ think_believe_consider(X0,X7)
| ~ present(X0,X7)
| ~ event(X0,X7)
| ~ theme(X0,X7,X6)
| ~ agent(X0,X7,X4)
| ~ proposition(X0,X6)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X4)
| ~ of(X0,X5,X4)
| ~ forename(X0,X3)
| ~ vincent_forename(X0,X3)
| ~ of(X0,X3,X4)
| ~ forename(X0,X1)
| ~ jules_forename(X0,X1)
| ~ of(X0,X1,X2)
| ~ actual_world(X0) ),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f279,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13] :
( ~ smoke(X12,X13)
| ~ present(X12,X13)
| ~ agent(X12,X13,X2)
| ~ event(X12,X13)
| ~ accessible_world(X0,X12)
| ~ think_believe_consider(X0,X11)
| ~ present(X0,X11)
| ~ event(X0,X11)
| ~ theme(X0,X11,X12)
| ~ agent(X0,X11,X4)
| ~ proposition(X0,X12)
| ~ be(X0,X10,X2,X2)
| ~ state(X0,X10)
| ~ man(X0,X2)
| ~ forename(X0,X9)
| ~ jules_forename(X0,X9)
| ~ man(X0,X2)
| ~ of(X0,X9,X2)
| ~ smoke(X6,X8)
| ~ present(X6,X8)
| ~ agent(X6,X8,sK9_skl(X6,X9,X10,X4,X11,X12,X2,X0))
| ~ event(X6,X8)
| ~ accessible_world(X0,X6)
| ~ think_believe_consider(X0,X7)
| ~ present(X0,X7)
| ~ event(X0,X7)
| ~ theme(X0,X7,X6)
| ~ agent(X0,X7,X4)
| ~ proposition(X0,X6)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X4)
| ~ of(X0,X5,X4)
| ~ forename(X0,X3)
| ~ vincent_forename(X0,X3)
| ~ of(X0,X3,X4)
| ~ forename(X0,X1)
| ~ jules_forename(X0,X1)
| ~ of(X0,X1,X2)
| ~ actual_world(X0) ),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f280,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( ~ smoke(X11,X12)
| ~ present(X11,X12)
| ~ agent(X11,X12,X2)
| ~ event(X11,X12)
| ~ accessible_world(X0,X11)
| ~ think_believe_consider(X0,X10)
| ~ present(X0,X10)
| ~ event(X0,X10)
| ~ theme(X0,X10,X11)
| ~ agent(X0,X10,X4)
| ~ proposition(X0,X11)
| ~ be(X0,X9,X2,X2)
| ~ state(X0,X9)
| ~ forename(X0,X8)
| ~ jules_forename(X0,X8)
| ~ man(X0,X2)
| ~ of(X0,X8,X2)
| man(X6,sK9_skl(X6,X8,X9,X4,X10,X11,X2,X0))
| ~ accessible_world(X0,X6)
| ~ think_believe_consider(X0,X7)
| ~ present(X0,X7)
| ~ event(X0,X7)
| ~ theme(X0,X7,X6)
| ~ agent(X0,X7,X4)
| ~ proposition(X0,X6)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X4)
| ~ of(X0,X5,X4)
| ~ forename(X0,X3)
| ~ vincent_forename(X0,X3)
| ~ of(X0,X3,X4)
| ~ forename(X0,X1)
| ~ jules_forename(X0,X1)
| ~ of(X0,X1,X2)
| ~ actual_world(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f278]) ).
fof(f281,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13] :
( ~ smoke(X12,X13)
| ~ present(X12,X13)
| ~ agent(X12,X13,X2)
| ~ event(X12,X13)
| ~ accessible_world(X0,X12)
| ~ think_believe_consider(X0,X11)
| ~ present(X0,X11)
| ~ event(X0,X11)
| ~ theme(X0,X11,X12)
| ~ agent(X0,X11,X4)
| ~ proposition(X0,X12)
| ~ be(X0,X10,X2,X2)
| ~ state(X0,X10)
| ~ forename(X0,X9)
| ~ jules_forename(X0,X9)
| ~ man(X0,X2)
| ~ of(X0,X9,X2)
| ~ smoke(X6,X8)
| ~ present(X6,X8)
| ~ agent(X6,X8,sK9_skl(X6,X9,X10,X4,X11,X12,X2,X0))
| ~ event(X6,X8)
| ~ accessible_world(X0,X6)
| ~ think_believe_consider(X0,X7)
| ~ present(X0,X7)
| ~ event(X0,X7)
| ~ theme(X0,X7,X6)
| ~ agent(X0,X7,X4)
| ~ proposition(X0,X6)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X4)
| ~ of(X0,X5,X4)
| ~ forename(X0,X3)
| ~ vincent_forename(X0,X3)
| ~ of(X0,X3,X4)
| ~ forename(X0,X1)
| ~ jules_forename(X0,X1)
| ~ of(X0,X1,X2)
| ~ actual_world(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f279]) ).
fof(f321,plain,
! [X0] :
( man(sK4_skl,X0)
| ~ man(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f186,f266]) ).
fof(f383,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( ~ smoke(X11,X12)
| ~ present(X11,X12)
| ~ agent(X11,X12,X2)
| ~ event(X11,X12)
| ~ accessible_world(X0,X11)
| ~ think_believe_consider(X0,X10)
| ~ present(X0,X10)
| ~ event(X0,X10)
| ~ theme(X0,X10,X11)
| ~ agent(X0,X10,X4)
| ~ proposition(X0,X11)
| ~ be(X0,X9,X2,X2)
| ~ state(X0,X9)
| ~ forename(X0,X8)
| ~ jules_forename(X0,X8)
| ~ man(X0,X2)
| ~ of(X0,X8,X2)
| man(X6,sK9_skl(X6,X8,X9,X4,X10,X11,X2,X0))
| ~ accessible_world(X0,X6)
| ~ think_believe_consider(X0,X7)
| ~ present(X0,X7)
| ~ event(X0,X7)
| ~ theme(X0,X7,X6)
| ~ agent(X0,X7,X4)
| ~ proposition(X0,X6)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X4)
| ~ of(X0,X5,X4)
| ~ vincent_forename(X0,X3)
| ~ of(X0,X3,X4)
| ~ forename(X0,X1)
| ~ jules_forename(X0,X1)
| ~ of(X0,X1,X2)
| ~ actual_world(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f280,f77]) ).
fof(f384,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ smoke(X8,X9)
| ~ present(X8,X9)
| ~ agent(X8,X9,sK1_skl)
| ~ event(X8,X9)
| ~ accessible_world(sK0_skl,X8)
| ~ think_believe_consider(sK0_skl,X7)
| ~ present(sK0_skl,X7)
| ~ event(sK0_skl,X7)
| ~ theme(sK0_skl,X7,X8)
| ~ agent(sK0_skl,X7,X1)
| ~ proposition(sK0_skl,X8)
| ~ be(sK0_skl,X6,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X6)
| ~ forename(sK0_skl,X5)
| ~ jules_forename(sK0_skl,X5)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X5,sK1_skl)
| man(X3,sK9_skl(X3,X5,X6,X1,X7,X8,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X3)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X3)
| ~ agent(sK0_skl,X4,X1)
| ~ proposition(sK0_skl,X3)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X2,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ actual_world(sK0_skl) ),
inference(resolution,[status(thm)],[f383,f271]) ).
fof(f386,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ smoke(X8,X9)
| ~ present(X8,X9)
| ~ agent(X8,X9,sK1_skl)
| ~ event(X8,X9)
| ~ accessible_world(sK0_skl,X8)
| ~ think_believe_consider(sK0_skl,X7)
| ~ present(sK0_skl,X7)
| ~ event(sK0_skl,X7)
| ~ theme(sK0_skl,X7,X8)
| ~ agent(sK0_skl,X7,X1)
| ~ proposition(sK0_skl,X8)
| ~ be(sK0_skl,X6,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X6)
| ~ forename(sK0_skl,X5)
| ~ jules_forename(sK0_skl,X5)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X5,sK1_skl)
| man(X3,sK9_skl(X3,X5,X6,X1,X7,X8,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X3)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X3)
| ~ agent(sK0_skl,X4,X1)
| ~ proposition(sK0_skl,X3)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X2,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f384,f255]) ).
fof(f404,plain,
man(sK4_skl,sK1_skl),
inference(resolution,[status(thm)],[f321,f272]) ).
fof(f406,plain,
smoke(sK4_skl,sK8_skl(sK1_skl)),
inference(resolution,[status(thm)],[f404,f270]) ).
fof(f407,plain,
present(sK4_skl,sK8_skl(sK1_skl)),
inference(resolution,[status(thm)],[f404,f269]) ).
fof(f408,plain,
agent(sK4_skl,sK8_skl(sK1_skl),sK1_skl),
inference(resolution,[status(thm)],[f404,f268]) ).
fof(f430,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13] :
( ~ smoke(X12,X13)
| ~ present(X12,X13)
| ~ agent(X12,X13,X2)
| ~ event(X12,X13)
| ~ accessible_world(X0,X12)
| ~ think_believe_consider(X0,X11)
| ~ present(X0,X11)
| ~ event(X0,X11)
| ~ theme(X0,X11,X12)
| ~ agent(X0,X11,X4)
| ~ proposition(X0,X12)
| ~ be(X0,X10,X2,X2)
| ~ state(X0,X10)
| ~ forename(X0,X9)
| ~ jules_forename(X0,X9)
| ~ man(X0,X2)
| ~ of(X0,X9,X2)
| ~ smoke(X6,X8)
| ~ present(X6,X8)
| ~ agent(X6,X8,sK9_skl(X6,X9,X10,X4,X11,X12,X2,X0))
| ~ event(X6,X8)
| ~ accessible_world(X0,X6)
| ~ think_believe_consider(X0,X7)
| ~ present(X0,X7)
| ~ event(X0,X7)
| ~ theme(X0,X7,X6)
| ~ agent(X0,X7,X4)
| ~ proposition(X0,X6)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X4)
| ~ of(X0,X5,X4)
| ~ vincent_forename(X0,X3)
| ~ of(X0,X3,X4)
| ~ forename(X0,X1)
| ~ jules_forename(X0,X1)
| ~ of(X0,X1,X2)
| ~ actual_world(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f281,f77]) ).
fof(f431,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( ~ smoke(X9,X10)
| ~ present(X9,X10)
| ~ agent(X9,X10,sK1_skl)
| ~ event(X9,X10)
| ~ accessible_world(sK0_skl,X9)
| ~ think_believe_consider(sK0_skl,X8)
| ~ present(sK0_skl,X8)
| ~ event(sK0_skl,X8)
| ~ theme(sK0_skl,X8,X9)
| ~ agent(sK0_skl,X8,X1)
| ~ proposition(sK0_skl,X9)
| ~ be(sK0_skl,X7,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X7)
| ~ forename(sK0_skl,X6)
| ~ jules_forename(sK0_skl,X6)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X6,sK1_skl)
| ~ smoke(X3,X5)
| ~ present(X3,X5)
| ~ agent(X3,X5,sK9_skl(X3,X6,X7,X1,X8,X9,sK1_skl,sK0_skl))
| ~ event(X3,X5)
| ~ accessible_world(sK0_skl,X3)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X3)
| ~ agent(sK0_skl,X4,X1)
| ~ proposition(sK0_skl,X3)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X2,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ actual_world(sK0_skl) ),
inference(resolution,[status(thm)],[f430,f271]) ).
fof(f433,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( ~ smoke(X9,X10)
| ~ present(X9,X10)
| ~ agent(X9,X10,sK1_skl)
| ~ event(X9,X10)
| ~ accessible_world(sK0_skl,X9)
| ~ think_believe_consider(sK0_skl,X8)
| ~ present(sK0_skl,X8)
| ~ event(sK0_skl,X8)
| ~ theme(sK0_skl,X8,X9)
| ~ agent(sK0_skl,X8,X1)
| ~ proposition(sK0_skl,X9)
| ~ be(sK0_skl,X7,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X7)
| ~ forename(sK0_skl,X6)
| ~ jules_forename(sK0_skl,X6)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X6,sK1_skl)
| ~ smoke(X3,X5)
| ~ present(X3,X5)
| ~ agent(X3,X5,sK9_skl(X3,X6,X7,X1,X8,X9,sK1_skl,sK0_skl))
| ~ event(X3,X5)
| ~ accessible_world(sK0_skl,X3)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X3)
| ~ agent(sK0_skl,X4,X1)
| ~ proposition(sK0_skl,X3)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X2,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f431,f255]) ).
fof(f529,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ smoke(X8,X9)
| ~ present(X8,X9)
| ~ agent(X8,X9,sK1_skl)
| ~ event(X8,X9)
| ~ accessible_world(sK0_skl,X8)
| ~ think_believe_consider(sK0_skl,X7)
| ~ present(sK0_skl,X7)
| ~ event(sK0_skl,X7)
| ~ theme(sK0_skl,X7,X8)
| ~ agent(sK0_skl,X7,X1)
| ~ proposition(sK0_skl,X8)
| ~ be(sK0_skl,X6,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X6)
| ~ forename(sK0_skl,X5)
| ~ jules_forename(sK0_skl,X5)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X5,sK1_skl)
| man(X3,sK9_skl(X3,X5,X6,X1,X7,X8,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X3)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X3)
| ~ agent(sK0_skl,X4,X1)
| ~ proposition(sK0_skl,X3)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X2,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f386,f273]) ).
fof(f531,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ smoke(X6,X7)
| ~ present(X6,X7)
| ~ agent(X6,X7,sK1_skl)
| ~ event(X6,X7)
| ~ accessible_world(sK0_skl,X6)
| ~ think_believe_consider(sK0_skl,X5)
| ~ present(sK0_skl,X5)
| ~ event(sK0_skl,X5)
| ~ theme(sK0_skl,X5,X6)
| ~ agent(sK0_skl,X5,sK6_skl)
| ~ proposition(sK0_skl,X6)
| ~ be(sK0_skl,X4,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X4)
| ~ forename(sK0_skl,X3)
| ~ jules_forename(sK0_skl,X3)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X3,sK1_skl)
| man(X1,sK9_skl(X1,X3,X4,sK6_skl,X5,X6,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X1)
| ~ think_believe_consider(sK0_skl,X2)
| ~ present(sK0_skl,X2)
| ~ event(sK0_skl,X2)
| ~ theme(sK0_skl,X2,X1)
| ~ agent(sK0_skl,X2,sK6_skl)
| ~ proposition(sK0_skl,X1)
| ~ forename(sK0_skl,X0)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl)
| ~ of(sK0_skl,X0,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f529,f256]) ).
fof(f534,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ smoke(X6,X7)
| ~ present(X6,X7)
| ~ agent(X6,X7,sK1_skl)
| ~ event(X6,X7)
| ~ accessible_world(sK0_skl,X6)
| ~ think_believe_consider(sK0_skl,X5)
| ~ present(sK0_skl,X5)
| ~ event(sK0_skl,X5)
| ~ theme(sK0_skl,X5,X6)
| ~ agent(sK0_skl,X5,sK6_skl)
| ~ proposition(sK0_skl,X6)
| ~ be(sK0_skl,X4,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X4)
| ~ forename(sK0_skl,X3)
| ~ jules_forename(sK0_skl,X3)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X3,sK1_skl)
| man(X1,sK9_skl(X1,X3,X4,sK6_skl,X5,X6,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X1)
| ~ think_believe_consider(sK0_skl,X2)
| ~ present(sK0_skl,X2)
| ~ event(sK0_skl,X2)
| ~ theme(sK0_skl,X2,X1)
| ~ agent(sK0_skl,X2,sK6_skl)
| ~ proposition(sK0_skl,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl)
| ~ of(sK0_skl,X0,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f531,f77]) ).
fof(f577,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( ~ smoke(X9,X10)
| ~ present(X9,X10)
| ~ agent(X9,X10,sK1_skl)
| ~ event(X9,X10)
| ~ accessible_world(sK0_skl,X9)
| ~ think_believe_consider(sK0_skl,X8)
| ~ present(sK0_skl,X8)
| ~ event(sK0_skl,X8)
| ~ theme(sK0_skl,X8,X9)
| ~ agent(sK0_skl,X8,X1)
| ~ proposition(sK0_skl,X9)
| ~ be(sK0_skl,X7,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X7)
| ~ forename(sK0_skl,X6)
| ~ jules_forename(sK0_skl,X6)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X6,sK1_skl)
| ~ smoke(X3,X5)
| ~ present(X3,X5)
| ~ agent(X3,X5,sK9_skl(X3,X6,X7,X1,X8,X9,sK1_skl,sK0_skl))
| ~ event(X3,X5)
| ~ accessible_world(sK0_skl,X3)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X3)
| ~ agent(sK0_skl,X4,X1)
| ~ proposition(sK0_skl,X3)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X2,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f433,f273]) ).
fof(f579,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ smoke(X7,X8)
| ~ present(X7,X8)
| ~ agent(X7,X8,sK1_skl)
| ~ event(X7,X8)
| ~ accessible_world(sK0_skl,X7)
| ~ think_believe_consider(sK0_skl,X6)
| ~ present(sK0_skl,X6)
| ~ event(sK0_skl,X6)
| ~ theme(sK0_skl,X6,X7)
| ~ agent(sK0_skl,X6,sK6_skl)
| ~ proposition(sK0_skl,X7)
| ~ be(sK0_skl,X5,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X5)
| ~ forename(sK0_skl,X4)
| ~ jules_forename(sK0_skl,X4)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X4,sK1_skl)
| ~ smoke(X1,X3)
| ~ present(X1,X3)
| ~ agent(X1,X3,sK9_skl(X1,X4,X5,sK6_skl,X6,X7,sK1_skl,sK0_skl))
| ~ event(X1,X3)
| ~ accessible_world(sK0_skl,X1)
| ~ think_believe_consider(sK0_skl,X2)
| ~ present(sK0_skl,X2)
| ~ event(sK0_skl,X2)
| ~ theme(sK0_skl,X2,X1)
| ~ agent(sK0_skl,X2,sK6_skl)
| ~ proposition(sK0_skl,X1)
| ~ forename(sK0_skl,X0)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl)
| ~ of(sK0_skl,X0,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f577,f256]) ).
fof(f582,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ smoke(X7,X8)
| ~ present(X7,X8)
| ~ agent(X7,X8,sK1_skl)
| ~ event(X7,X8)
| ~ accessible_world(sK0_skl,X7)
| ~ think_believe_consider(sK0_skl,X6)
| ~ present(sK0_skl,X6)
| ~ event(sK0_skl,X6)
| ~ theme(sK0_skl,X6,X7)
| ~ agent(sK0_skl,X6,sK6_skl)
| ~ proposition(sK0_skl,X7)
| ~ be(sK0_skl,X5,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X5)
| ~ forename(sK0_skl,X4)
| ~ jules_forename(sK0_skl,X4)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X4,sK1_skl)
| ~ smoke(X1,X3)
| ~ present(X1,X3)
| ~ agent(X1,X3,sK9_skl(X1,X4,X5,sK6_skl,X6,X7,sK1_skl,sK0_skl))
| ~ event(X1,X3)
| ~ accessible_world(sK0_skl,X1)
| ~ think_believe_consider(sK0_skl,X2)
| ~ present(sK0_skl,X2)
| ~ event(sK0_skl,X2)
| ~ theme(sK0_skl,X2,X1)
| ~ agent(sK0_skl,X2,sK6_skl)
| ~ proposition(sK0_skl,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl)
| ~ of(sK0_skl,X0,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f579,f77]) ).
fof(f663,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ smoke(X6,X7)
| ~ present(X6,X7)
| ~ agent(X6,X7,sK1_skl)
| ~ event(X6,X7)
| ~ accessible_world(sK0_skl,X6)
| ~ think_believe_consider(sK0_skl,X5)
| ~ present(sK0_skl,X5)
| ~ event(sK0_skl,X5)
| ~ theme(sK0_skl,X5,X6)
| ~ agent(sK0_skl,X5,sK6_skl)
| ~ proposition(sK0_skl,X6)
| ~ be(sK0_skl,X4,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X4)
| ~ jules_forename(sK0_skl,X3)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X3,sK1_skl)
| man(X1,sK9_skl(X1,X3,X4,sK6_skl,X5,X6,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X1)
| ~ think_believe_consider(sK0_skl,X2)
| ~ present(sK0_skl,X2)
| ~ event(sK0_skl,X2)
| ~ theme(sK0_skl,X2,X1)
| ~ agent(sK0_skl,X2,sK6_skl)
| ~ proposition(sK0_skl,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl)
| ~ of(sK0_skl,X0,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f534,f75]) ).
fof(f664,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ smoke(X5,X6)
| ~ present(X5,X6)
| ~ agent(X5,X6,sK1_skl)
| ~ event(X5,X6)
| ~ accessible_world(sK0_skl,X5)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X5)
| ~ agent(sK0_skl,X4,sK6_skl)
| ~ proposition(sK0_skl,X5)
| ~ be(sK0_skl,X3,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X3)
| ~ jules_forename(sK0_skl,X2)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X2,sK1_skl)
| man(X0,sK9_skl(X0,X2,X3,sK6_skl,X4,X5,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,X1)
| ~ present(sK0_skl,X1)
| ~ event(sK0_skl,X1)
| ~ theme(sK0_skl,X1,X0)
| ~ agent(sK0_skl,X1,sK6_skl)
| ~ proposition(sK0_skl,X0)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f663,f256]) ).
fof(f665,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ smoke(X5,X6)
| ~ present(X5,X6)
| ~ agent(X5,X6,sK1_skl)
| ~ event(X5,X6)
| ~ accessible_world(sK0_skl,X5)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X5)
| ~ agent(sK0_skl,X4,sK6_skl)
| ~ proposition(sK0_skl,X5)
| ~ be(sK0_skl,X3,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X3)
| ~ jules_forename(sK0_skl,X2)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X2,sK1_skl)
| man(X0,sK9_skl(X0,X2,X3,sK6_skl,X4,X5,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,X1)
| ~ present(sK0_skl,X1)
| ~ event(sK0_skl,X1)
| ~ theme(sK0_skl,X1,X0)
| ~ agent(sK0_skl,X1,sK6_skl)
| ~ proposition(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f664]) ).
fof(f666,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ smoke(X5,X6)
| ~ present(X5,X6)
| ~ agent(X5,X6,sK1_skl)
| ~ event(X5,X6)
| ~ accessible_world(sK0_skl,X5)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X5)
| ~ agent(sK0_skl,X4,sK6_skl)
| ~ proposition(sK0_skl,X5)
| ~ be(sK0_skl,X3,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X3)
| ~ jules_forename(sK0_skl,X2)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X2,sK1_skl)
| man(X0,sK9_skl(X0,X2,X3,sK6_skl,X4,X5,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,X1)
| ~ present(sK0_skl,X1)
| ~ event(sK0_skl,X1)
| ~ theme(sK0_skl,X1,X0)
| ~ agent(sK0_skl,X1,sK6_skl)
| ~ proposition(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f665,f274]) ).
fof(f667,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ smoke(X5,X6)
| ~ present(X5,X6)
| ~ agent(X5,X6,sK1_skl)
| ~ event(X5,X6)
| ~ accessible_world(sK0_skl,X5)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X5)
| ~ agent(sK0_skl,X4,sK6_skl)
| ~ proposition(sK0_skl,X5)
| ~ be(sK0_skl,X3,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X3)
| ~ jules_forename(sK0_skl,X2)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X2,sK1_skl)
| man(X0,sK9_skl(X0,X2,X3,sK6_skl,X4,X5,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,X1)
| ~ present(sK0_skl,X1)
| ~ event(sK0_skl,X1)
| ~ theme(sK0_skl,X1,X0)
| ~ agent(sK0_skl,X1,sK6_skl)
| ~ proposition(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f666,f258]) ).
fof(f668,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ smoke(X4,X5)
| ~ present(X4,X5)
| ~ agent(X4,X5,sK1_skl)
| ~ event(X4,X5)
| ~ accessible_world(sK0_skl,X4)
| ~ think_believe_consider(sK0_skl,X3)
| ~ present(sK0_skl,X3)
| ~ event(sK0_skl,X3)
| ~ theme(sK0_skl,X3,X4)
| ~ agent(sK0_skl,X3,sK6_skl)
| ~ proposition(sK0_skl,X4)
| ~ be(sK0_skl,X2,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X2)
| ~ jules_forename(sK0_skl,X1)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X1,sK1_skl)
| man(X0,sK9_skl(X0,X1,X2,sK6_skl,X3,X4,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,X0)
| ~ proposition(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl) ),
inference(resolution,[status(thm)],[f667,f261]) ).
fof(f669,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ smoke(X4,X5)
| ~ present(X4,X5)
| ~ agent(X4,X5,sK1_skl)
| ~ event(X4,X5)
| ~ accessible_world(sK0_skl,X4)
| ~ think_believe_consider(sK0_skl,X3)
| ~ present(sK0_skl,X3)
| ~ event(sK0_skl,X3)
| ~ theme(sK0_skl,X3,X4)
| ~ agent(sK0_skl,X3,sK6_skl)
| ~ proposition(sK0_skl,X4)
| ~ be(sK0_skl,X2,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X2)
| ~ jules_forename(sK0_skl,X1)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X1,sK1_skl)
| man(X0,sK9_skl(X0,X1,X2,sK6_skl,X3,X4,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,X0)
| ~ proposition(sK0_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f668,f257]) ).
fof(f678,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ smoke(X4,X5)
| ~ present(X4,X5)
| ~ agent(X4,X5,sK1_skl)
| ~ accessible_world(sK0_skl,X4)
| ~ think_believe_consider(sK0_skl,X3)
| ~ present(sK0_skl,X3)
| ~ event(sK0_skl,X3)
| ~ theme(sK0_skl,X3,X4)
| ~ agent(sK0_skl,X3,sK6_skl)
| ~ proposition(sK0_skl,X4)
| ~ be(sK0_skl,X2,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X2)
| ~ jules_forename(sK0_skl,X1)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X1,sK1_skl)
| man(X0,sK9_skl(X0,X1,X2,sK6_skl,X3,X4,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,X0)
| ~ proposition(sK0_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f669,f133]) ).
fof(f679,plain,
! [X0,X1,X2,X3,X4] :
( ~ smoke(X3,X4)
| ~ present(X3,X4)
| ~ agent(X3,X4,sK1_skl)
| ~ accessible_world(sK0_skl,X3)
| ~ think_believe_consider(sK0_skl,X2)
| ~ present(sK0_skl,X2)
| ~ event(sK0_skl,X2)
| ~ theme(sK0_skl,X2,X3)
| ~ agent(sK0_skl,X2,sK6_skl)
| ~ proposition(sK0_skl,X3)
| ~ be(sK0_skl,X1,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X1)
| ~ jules_forename(sK0_skl,X0)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X0,sK1_skl)
| man(sK4_skl,sK9_skl(sK4_skl,X0,X1,sK6_skl,X2,X3,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ proposition(sK0_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f678,f262]) ).
fof(f680,plain,
! [X0,X1,X2,X3,X4] :
( ~ smoke(X3,X4)
| ~ present(X3,X4)
| ~ agent(X3,X4,sK1_skl)
| ~ accessible_world(sK0_skl,X3)
| ~ think_believe_consider(sK0_skl,X2)
| ~ present(sK0_skl,X2)
| ~ event(sK0_skl,X2)
| ~ theme(sK0_skl,X2,X3)
| ~ agent(sK0_skl,X2,sK6_skl)
| ~ proposition(sK0_skl,X3)
| ~ be(sK0_skl,X1,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X1)
| ~ jules_forename(sK0_skl,X0)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X0,sK1_skl)
| man(sK4_skl,sK9_skl(sK4_skl,X0,X1,sK6_skl,X2,X3,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f679,f260]) ).
fof(f681,plain,
! [X0,X1,X2,X3,X4] :
( ~ smoke(X3,X4)
| ~ present(X3,X4)
| ~ agent(X3,X4,sK1_skl)
| ~ accessible_world(sK0_skl,X3)
| ~ think_believe_consider(sK0_skl,X2)
| ~ present(sK0_skl,X2)
| ~ event(sK0_skl,X2)
| ~ theme(sK0_skl,X2,X3)
| ~ agent(sK0_skl,X2,sK6_skl)
| ~ proposition(sK0_skl,X3)
| ~ be(sK0_skl,X1,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X1)
| ~ jules_forename(sK0_skl,X0)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X0,sK1_skl)
| man(sK4_skl,sK9_skl(sK4_skl,X0,X1,sK6_skl,X2,X3,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f680,f263]) ).
fof(f682,plain,
! [X0,X1,X2,X3] :
( ~ smoke(X2,X3)
| ~ present(X2,X3)
| ~ agent(X2,X3,sK1_skl)
| ~ accessible_world(sK0_skl,X2)
| ~ think_believe_consider(sK0_skl,X1)
| ~ present(sK0_skl,X1)
| ~ event(sK0_skl,X1)
| ~ theme(sK0_skl,X1,X2)
| ~ agent(sK0_skl,X1,sK6_skl)
| ~ proposition(sK0_skl,X2)
| ~ be(sK0_skl,X0,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X0)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,X0,sK6_skl,X1,X2,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f681,f271]) ).
fof(f683,plain,
! [X0,X1,X2,X3] :
( ~ smoke(X2,X3)
| ~ present(X2,X3)
| ~ agent(X2,X3,sK1_skl)
| ~ accessible_world(sK0_skl,X2)
| ~ think_believe_consider(sK0_skl,X1)
| ~ present(sK0_skl,X1)
| ~ event(sK0_skl,X1)
| ~ theme(sK0_skl,X1,X2)
| ~ agent(sK0_skl,X1,sK6_skl)
| ~ proposition(sK0_skl,X2)
| ~ be(sK0_skl,X0,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X0)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,X0,sK6_skl,X1,X2,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f682,f264]) ).
fof(f684,plain,
! [X0,X1,X2,X3] :
( ~ smoke(X2,X3)
| ~ present(X2,X3)
| ~ agent(X2,X3,sK1_skl)
| ~ accessible_world(sK0_skl,X2)
| ~ think_believe_consider(sK0_skl,X1)
| ~ present(sK0_skl,X1)
| ~ event(sK0_skl,X1)
| ~ theme(sK0_skl,X1,X2)
| ~ agent(sK0_skl,X1,sK6_skl)
| ~ proposition(sK0_skl,X2)
| ~ be(sK0_skl,X0,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X0)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,X0,sK6_skl,X1,X2,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,sK4_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f683,f265]) ).
fof(f685,plain,
! [X0,X1,X2] :
( ~ smoke(X1,X2)
| ~ present(X1,X2)
| ~ agent(X1,X2,sK1_skl)
| ~ accessible_world(sK0_skl,X1)
| ~ think_believe_consider(sK0_skl,X0)
| ~ present(sK0_skl,X0)
| ~ event(sK0_skl,X0)
| ~ theme(sK0_skl,X0,X1)
| ~ agent(sK0_skl,X0,sK6_skl)
| ~ proposition(sK0_skl,X1)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,X0,X1,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f684,f277]) ).
fof(f686,plain,
! [X0,X1,X2] :
( ~ smoke(X1,X2)
| ~ present(X1,X2)
| ~ agent(X1,X2,sK1_skl)
| ~ accessible_world(sK0_skl,X1)
| ~ think_believe_consider(sK0_skl,X0)
| ~ present(sK0_skl,X0)
| ~ event(sK0_skl,X0)
| ~ theme(sK0_skl,X0,X1)
| ~ agent(sK0_skl,X0,sK6_skl)
| ~ proposition(sK0_skl,X1)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,X0,X1,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f685,f266]) ).
fof(f687,plain,
! [X0,X1,X2] :
( ~ smoke(X1,X2)
| ~ present(X1,X2)
| ~ agent(X1,X2,sK1_skl)
| ~ accessible_world(sK0_skl,X1)
| ~ think_believe_consider(sK0_skl,X0)
| ~ present(sK0_skl,X0)
| ~ event(sK0_skl,X0)
| ~ theme(sK0_skl,X0,X1)
| ~ agent(sK0_skl,X0,sK6_skl)
| ~ proposition(sK0_skl,X1)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,X0,X1,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f686,f272]) ).
fof(f688,plain,
! [X0,X1] :
( ~ smoke(X0,X1)
| ~ present(X0,X1)
| ~ agent(X0,X1,sK1_skl)
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,X0)
| ~ proposition(sK0_skl,X0)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,X0,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f687,f261]) ).
fof(f689,plain,
! [X0,X1] :
( ~ smoke(X0,X1)
| ~ present(X0,X1)
| ~ agent(X0,X1,sK1_skl)
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,X0)
| ~ proposition(sK0_skl,X0)
| ~ state(sK0_skl,sK2_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,X0,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f688,f273]) ).
fof(f690,plain,
! [X0,X1] :
( ~ smoke(X0,X1)
| ~ present(X0,X1)
| ~ agent(X0,X1,sK1_skl)
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,X0)
| ~ proposition(sK0_skl,X0)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,X0,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f689,f276]) ).
fof(f691,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ present(sK4_skl,sK8_skl(sK1_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,sK4_skl)
| ~ proposition(sK0_skl,sK4_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f690,f408]) ).
fof(f692,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ present(sK4_skl,sK8_skl(sK1_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,sK4_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f691,f260]) ).
fof(f693,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ present(sK4_skl,sK8_skl(sK1_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f692,f262]) ).
fof(f694,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f693,f407]) ).
fof(f695,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f694,f263]) ).
fof(f696,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f695,f264]) ).
fof(f697,plain,
( ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f696,f406]) ).
fof(f698,plain,
( ~ accessible_world(sK0_skl,sK4_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f697,f265]) ).
fof(f699,plain,
man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f698,f266]) ).
fof(f700,plain,
smoke(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl))),
inference(resolution,[status(thm)],[f699,f270]) ).
fof(f701,plain,
present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl))),
inference(resolution,[status(thm)],[f699,f269]) ).
fof(f702,plain,
agent(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)),sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)),
inference(resolution,[status(thm)],[f699,f268]) ).
fof(f712,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ smoke(X7,X8)
| ~ present(X7,X8)
| ~ agent(X7,X8,sK1_skl)
| ~ event(X7,X8)
| ~ accessible_world(sK0_skl,X7)
| ~ think_believe_consider(sK0_skl,X6)
| ~ present(sK0_skl,X6)
| ~ event(sK0_skl,X6)
| ~ theme(sK0_skl,X6,X7)
| ~ agent(sK0_skl,X6,sK6_skl)
| ~ proposition(sK0_skl,X7)
| ~ be(sK0_skl,X5,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X5)
| ~ jules_forename(sK0_skl,X4)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X4,sK1_skl)
| ~ smoke(X1,X3)
| ~ present(X1,X3)
| ~ agent(X1,X3,sK9_skl(X1,X4,X5,sK6_skl,X6,X7,sK1_skl,sK0_skl))
| ~ event(X1,X3)
| ~ accessible_world(sK0_skl,X1)
| ~ think_believe_consider(sK0_skl,X2)
| ~ present(sK0_skl,X2)
| ~ event(sK0_skl,X2)
| ~ theme(sK0_skl,X2,X1)
| ~ agent(sK0_skl,X2,sK6_skl)
| ~ proposition(sK0_skl,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl)
| ~ of(sK0_skl,X0,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f582,f75]) ).
fof(f713,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ smoke(X6,X7)
| ~ present(X6,X7)
| ~ agent(X6,X7,sK1_skl)
| ~ event(X6,X7)
| ~ accessible_world(sK0_skl,X6)
| ~ think_believe_consider(sK0_skl,X5)
| ~ present(sK0_skl,X5)
| ~ event(sK0_skl,X5)
| ~ theme(sK0_skl,X5,X6)
| ~ agent(sK0_skl,X5,sK6_skl)
| ~ proposition(sK0_skl,X6)
| ~ be(sK0_skl,X4,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X4)
| ~ jules_forename(sK0_skl,X3)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X3,sK1_skl)
| ~ smoke(X0,X2)
| ~ present(X0,X2)
| ~ agent(X0,X2,sK9_skl(X0,X3,X4,sK6_skl,X5,X6,sK1_skl,sK0_skl))
| ~ event(X0,X2)
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,X1)
| ~ present(sK0_skl,X1)
| ~ event(sK0_skl,X1)
| ~ theme(sK0_skl,X1,X0)
| ~ agent(sK0_skl,X1,sK6_skl)
| ~ proposition(sK0_skl,X0)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f712,f256]) ).
fof(f714,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ smoke(X6,X7)
| ~ present(X6,X7)
| ~ agent(X6,X7,sK1_skl)
| ~ event(X6,X7)
| ~ accessible_world(sK0_skl,X6)
| ~ think_believe_consider(sK0_skl,X5)
| ~ present(sK0_skl,X5)
| ~ event(sK0_skl,X5)
| ~ theme(sK0_skl,X5,X6)
| ~ agent(sK0_skl,X5,sK6_skl)
| ~ proposition(sK0_skl,X6)
| ~ be(sK0_skl,X4,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X4)
| ~ jules_forename(sK0_skl,X3)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X3,sK1_skl)
| ~ smoke(X0,X2)
| ~ present(X0,X2)
| ~ agent(X0,X2,sK9_skl(X0,X3,X4,sK6_skl,X5,X6,sK1_skl,sK0_skl))
| ~ event(X0,X2)
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,X1)
| ~ present(sK0_skl,X1)
| ~ event(sK0_skl,X1)
| ~ theme(sK0_skl,X1,X0)
| ~ agent(sK0_skl,X1,sK6_skl)
| ~ proposition(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f713]) ).
fof(f715,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ smoke(X6,X7)
| ~ present(X6,X7)
| ~ agent(X6,X7,sK1_skl)
| ~ event(X6,X7)
| ~ accessible_world(sK0_skl,X6)
| ~ think_believe_consider(sK0_skl,X5)
| ~ present(sK0_skl,X5)
| ~ event(sK0_skl,X5)
| ~ theme(sK0_skl,X5,X6)
| ~ agent(sK0_skl,X5,sK6_skl)
| ~ proposition(sK0_skl,X6)
| ~ be(sK0_skl,X4,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X4)
| ~ jules_forename(sK0_skl,X3)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X3,sK1_skl)
| ~ smoke(X0,X2)
| ~ present(X0,X2)
| ~ agent(X0,X2,sK9_skl(X0,X3,X4,sK6_skl,X5,X6,sK1_skl,sK0_skl))
| ~ event(X0,X2)
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,X1)
| ~ present(sK0_skl,X1)
| ~ event(sK0_skl,X1)
| ~ theme(sK0_skl,X1,X0)
| ~ agent(sK0_skl,X1,sK6_skl)
| ~ proposition(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f714,f274]) ).
fof(f764,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ smoke(X6,X7)
| ~ present(X6,X7)
| ~ agent(X6,X7,sK1_skl)
| ~ event(X6,X7)
| ~ accessible_world(sK0_skl,X6)
| ~ think_believe_consider(sK0_skl,X5)
| ~ present(sK0_skl,X5)
| ~ event(sK0_skl,X5)
| ~ theme(sK0_skl,X5,X6)
| ~ agent(sK0_skl,X5,sK6_skl)
| ~ proposition(sK0_skl,X6)
| ~ be(sK0_skl,X4,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X4)
| ~ jules_forename(sK0_skl,X3)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X3,sK1_skl)
| ~ smoke(X0,X2)
| ~ present(X0,X2)
| ~ agent(X0,X2,sK9_skl(X0,X3,X4,sK6_skl,X5,X6,sK1_skl,sK0_skl))
| ~ event(X0,X2)
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,X1)
| ~ present(sK0_skl,X1)
| ~ event(sK0_skl,X1)
| ~ theme(sK0_skl,X1,X0)
| ~ agent(sK0_skl,X1,sK6_skl)
| ~ proposition(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f715,f258]) ).
fof(f765,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ smoke(X5,X6)
| ~ present(X5,X6)
| ~ agent(X5,X6,sK1_skl)
| ~ event(X5,X6)
| ~ accessible_world(sK0_skl,X5)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X5)
| ~ agent(sK0_skl,X4,sK6_skl)
| ~ proposition(sK0_skl,X5)
| ~ be(sK0_skl,X3,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X3)
| ~ jules_forename(sK0_skl,X2)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X2,sK1_skl)
| ~ smoke(X0,X1)
| ~ present(X0,X1)
| ~ agent(X0,X1,sK9_skl(X0,X2,X3,sK6_skl,X4,X5,sK1_skl,sK0_skl))
| ~ event(X0,X1)
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,X0)
| ~ proposition(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl) ),
inference(resolution,[status(thm)],[f764,f261]) ).
fof(f766,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ smoke(X5,X6)
| ~ present(X5,X6)
| ~ agent(X5,X6,sK1_skl)
| ~ event(X5,X6)
| ~ accessible_world(sK0_skl,X5)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X5)
| ~ agent(sK0_skl,X4,sK6_skl)
| ~ proposition(sK0_skl,X5)
| ~ be(sK0_skl,X3,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X3)
| ~ jules_forename(sK0_skl,X2)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X2,sK1_skl)
| ~ smoke(X0,X1)
| ~ present(X0,X1)
| ~ agent(X0,X1,sK9_skl(X0,X2,X3,sK6_skl,X4,X5,sK1_skl,sK0_skl))
| ~ event(X0,X1)
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,X0)
| ~ proposition(sK0_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f765,f257]) ).
fof(f767,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ smoke(X5,X6)
| ~ present(X5,X6)
| ~ agent(X5,X6,sK1_skl)
| ~ event(X5,X6)
| ~ accessible_world(sK0_skl,X5)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X5)
| ~ agent(sK0_skl,X4,sK6_skl)
| ~ proposition(sK0_skl,X5)
| ~ be(sK0_skl,X3,sK1_skl,sK1_skl)
| ~ state(sK0_skl,X3)
| ~ jules_forename(sK0_skl,X2)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,X2,sK1_skl)
| ~ smoke(X0,X1)
| ~ present(X0,X1)
| ~ agent(X0,X1,sK9_skl(X0,X2,X3,sK6_skl,X4,X5,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,X0)
| ~ proposition(sK0_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f766,f133]) ).
fof(f768,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl)
| ~ event(sK4_skl,X0)
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,sK4_skl)
| ~ agent(sK0_skl,sK5_skl,sK6_skl)
| ~ proposition(sK0_skl,sK4_skl)
| ~ be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,sK3_skl,sK1_skl)
| ~ smoke(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,sK4_skl)
| ~ proposition(sK0_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f767,f702]) ).
fof(f769,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl)
| ~ event(sK4_skl,X0)
| ~ agent(sK0_skl,sK5_skl,sK6_skl)
| ~ be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,sK3_skl,sK1_skl)
| ~ smoke(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,sK4_skl)
| ~ proposition(sK0_skl,sK4_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f768]) ).
fof(f770,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl)
| ~ event(sK4_skl,X0)
| ~ agent(sK0_skl,sK5_skl,sK6_skl)
| ~ be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,sK3_skl,sK1_skl)
| ~ smoke(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,sK4_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f769,f260]) ).
fof(f771,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl)
| ~ event(sK4_skl,X0)
| ~ agent(sK0_skl,sK5_skl,sK6_skl)
| ~ be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,sK3_skl,sK1_skl)
| ~ smoke(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f770,f262]) ).
fof(f772,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl)
| ~ event(sK4_skl,X0)
| ~ agent(sK0_skl,sK5_skl,sK6_skl)
| ~ be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,sK3_skl,sK1_skl)
| ~ smoke(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f771,f701]) ).
fof(f773,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl)
| ~ agent(sK0_skl,sK5_skl,sK6_skl)
| ~ be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,sK3_skl,sK1_skl)
| ~ smoke(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f772,f133]) ).
fof(f774,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl)
| ~ agent(sK0_skl,sK5_skl,sK6_skl)
| ~ be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,sK3_skl,sK1_skl)
| ~ smoke(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f773,f263]) ).
fof(f775,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl)
| ~ agent(sK0_skl,sK5_skl,sK6_skl)
| ~ be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,sK3_skl,sK1_skl)
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f774,f700]) ).
fof(f776,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl)
| ~ agent(sK0_skl,sK5_skl,sK6_skl)
| ~ be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,sK3_skl,sK1_skl)
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f775,f264]) ).
fof(f777,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl)
| ~ agent(sK0_skl,sK5_skl,sK6_skl)
| ~ be(sK0_skl,sK2_skl,sK1_skl,sK1_skl)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,sK3_skl,sK1_skl)
| ~ accessible_world(sK0_skl,sK4_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f776,f265]) ).
fof(f778,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl)
| ~ agent(sK0_skl,sK5_skl,sK6_skl)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,sK3_skl,sK1_skl)
| ~ accessible_world(sK0_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f777,f277]) ).
fof(f779,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl)
| ~ agent(sK0_skl,sK5_skl,sK6_skl)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| ~ of(sK0_skl,sK3_skl,sK1_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f778,f266]) ).
fof(f781,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl)
| ~ agent(sK0_skl,sK5_skl,sK6_skl)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f779,f271]) ).
fof(f782,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f781,f261]) ).
fof(f783,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f782,f272]) ).
fof(f784,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl)
| ~ state(sK0_skl,sK2_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f783,f273]) ).
fof(f785,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ present(sK4_skl,sK8_skl(sK1_skl))
| ~ state(sK0_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f784,f408]) ).
fof(f786,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ present(sK4_skl,sK8_skl(sK1_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f785,f276]) ).
fof(f788,plain,
~ smoke(sK4_skl,sK8_skl(sK1_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f786,f407]) ).
fof(f789,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f406,f788]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP258+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n020.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 01:56:47 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.42 % Refutation found
% 0.12/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.46 % Elapsed time: 0.086208 seconds
% 0.12/0.46 % CPU time: 0.443391 seconds
% 0.12/0.46 % Total memory used: 53.936 MB
% 0.12/0.46 % Net memory used: 53.658 MB
%------------------------------------------------------------------------------