%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NLP251+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 : n010.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:38 PM UTC 2026
% Result : Theorem 0.54s 0.60s
% Output : CNFRefutation 0.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 67
% Number of leaves : 5
% Syntax : Number of formulae : 125 ( 28 unt; 0 def)
% Number of atoms : 1964 ( 0 equ)
% Maximal formula atoms : 67 ( 15 avg)
% Number of connectives : 3514 (1675 ~;1630 |; 201 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 59 ( 19 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-9 aty)
% Number of variables : 553 ( 483 !; 70 ?)
% 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,X8,X9,V,W,X,Y,Z,X1,X2,X10,X11] :
( ? [X12] :
( smoke(X11,X12)
& present(X11,X12)
& agent(X11,X12,X8)
& event(X11,X12) )
& accessible_world(X5,X11)
& think_believe_consider(X5,X10)
& present(X5,X10)
& event(X5,X10)
& theme(X5,X10,X11)
& agent(X5,X10,X6)
& proposition(X5,X11)
& 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,X9)
& jules_forename(X5,X9)
& man(X5,X8)
& of(X5,X9,X8)
& forename(X5,X7)
& vincent_forename(X5,X7)
& man(X5,X6)
& of(X5,X7,X6) )
& 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,X8,X9,V,W,X,Y,Z,X1,X2,X10,X11] :
( ? [X12] :
( smoke(X11,X12)
& present(X11,X12)
& agent(X11,X12,X8)
& event(X11,X12) )
& accessible_world(X5,X11)
& think_believe_consider(X5,X10)
& present(X5,X10)
& event(X5,X10)
& theme(X5,X10,X11)
& agent(X5,X10,X6)
& proposition(X5,X11)
& 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,X9)
& jules_forename(X5,X9)
& man(X5,X8)
& of(X5,X9,X8)
& forename(X5,X7)
& vincent_forename(X5,X7)
& man(X5,X6)
& of(X5,X7,X6) )
& 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,X8,X9,V,W,X,Y,Z,X1,X2,X10,X11] :
( ! [X12] :
( ~ smoke(X11,X12)
| ~ present(X11,X12)
| ~ agent(X11,X12,X8)
| ~ event(X11,X12) )
| ~ accessible_world(X5,X11)
| ~ think_believe_consider(X5,X10)
| ~ present(X5,X10)
| ~ event(X5,X10)
| ~ theme(X5,X10,X11)
| ~ agent(X5,X10,X6)
| ~ proposition(X5,X11)
| ~ 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,X9)
| ~ jules_forename(X5,X9)
| ~ man(X5,X8)
| ~ of(X5,X9,X8)
| ~ forename(X5,X7)
| ~ vincent_forename(X5,X7)
| ~ man(X5,X6)
| ~ of(X5,X7,X6) )
| ~ 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] :
( ! [X8,X11] :
( ! [X12] :
( ~ smoke(X11,X12)
| ~ present(X11,X12)
| ~ agent(X11,X12,X8)
| ~ event(X11,X12) )
| ~ accessible_world(X5,X11)
| ! [X10] :
( ~ think_believe_consider(X5,X10)
| ~ present(X5,X10)
| ~ event(X5,X10)
| ~ theme(X5,X10,X11)
| ! [X6] :
( ~ agent(X5,X10,X6)
| ~ proposition(X5,X11)
| ! [X1,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)
| ! [V] :
( ~ agent(X5,X,V)
| ~ proposition(X5,Y)
| ! [W] :
( ~ forename(X5,W)
| ~ vincent_forename(X5,W)
| ~ man(X5,V)
| ~ of(X5,W,V)
| ! [X9] :
( ~ forename(X5,X9)
| ~ jules_forename(X5,X9)
| ~ man(X5,X8)
| ~ of(X5,X9,X8)
| ! [X7] :
( ~ forename(X5,X7)
| ~ vincent_forename(X5,X7)
| ~ man(X5,X6)
| ~ of(X5,X7,X6) ) ) ) ) ) ) ) ) ) ) )
| ~ 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] :
( ! [X8,X11] :
( ! [X12] :
( ~ smoke(X11,X12)
| ~ present(X11,X12)
| ~ agent(X11,X12,X8)
| ~ event(X11,X12) )
| ~ accessible_world(X5,X11)
| ! [X10] :
( ~ think_believe_consider(X5,X10)
| ~ present(X5,X10)
| ~ event(X5,X10)
| ~ theme(X5,X10,X11)
| ! [X6] :
( ~ agent(X5,X10,X6)
| ~ proposition(X5,X11)
| ! [X1,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,X1,X6,X10,X11,X8,X5))
| ~ event(Y,X4) )
& man(Y,sK9_skl(Y,Z,X2,X1,X6,X10,X11,X8,X5)) )
| ~ accessible_world(X5,Y)
| ! [X] :
( ~ think_believe_consider(X5,X)
| ~ present(X5,X)
| ~ event(X5,X)
| ~ theme(X5,X,Y)
| ! [V] :
( ~ agent(X5,X,V)
| ~ proposition(X5,Y)
| ! [W] :
( ~ forename(X5,W)
| ~ vincent_forename(X5,W)
| ~ man(X5,V)
| ~ of(X5,W,V)
| ! [X9] :
( ~ forename(X5,X9)
| ~ jules_forename(X5,X9)
| ~ man(X5,X8)
| ~ of(X5,X9,X8)
| ! [X7] :
( ~ forename(X5,X7)
| ~ vincent_forename(X5,X7)
| ~ man(X5,X6)
| ~ of(X5,X7,X6) ) ) ) ) ) ) ) ) ) ) )
| ~ 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,X1,X6,X10,X11,X8,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(f267,plain,
! [X0] :
( event(sK4_skl,sK8_skl(X0))
| ~ man(sK4_skl,X0) ),
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,X13,X14] :
( ~ smoke(X13,X14)
| ~ present(X13,X14)
| ~ agent(X13,X14,X4)
| ~ event(X13,X14)
| ~ accessible_world(X0,X13)
| ~ think_believe_consider(X0,X12)
| ~ present(X0,X12)
| ~ event(X0,X12)
| ~ theme(X0,X12,X13)
| ~ agent(X0,X12,X2)
| ~ proposition(X0,X13)
| ~ be(X0,X10,X11,X11)
| ~ state(X0,X10)
| ~ man(X0,X11)
| ~ forename(X0,X9)
| ~ jules_forename(X0,X9)
| ~ man(X0,X11)
| ~ of(X0,X9,X11)
| man(X7,sK9_skl(X7,X9,X10,X11,X2,X12,X13,X4,X0))
| ~ accessible_world(X0,X7)
| ~ think_believe_consider(X0,X8)
| ~ present(X0,X8)
| ~ event(X0,X8)
| ~ theme(X0,X8,X7)
| ~ agent(X0,X8,X6)
| ~ proposition(X0,X7)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X6)
| ~ of(X0,X5,X6)
| ~ forename(X0,X3)
| ~ jules_forename(X0,X3)
| ~ man(X0,X4)
| ~ of(X0,X3,X4)
| ~ forename(X0,X1)
| ~ vincent_forename(X0,X1)
| ~ man(X0,X2)
| ~ 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,X14,X15] :
( ~ smoke(X14,X15)
| ~ present(X14,X15)
| ~ agent(X14,X15,X4)
| ~ event(X14,X15)
| ~ accessible_world(X0,X14)
| ~ think_believe_consider(X0,X13)
| ~ present(X0,X13)
| ~ event(X0,X13)
| ~ theme(X0,X13,X14)
| ~ agent(X0,X13,X2)
| ~ proposition(X0,X14)
| ~ be(X0,X11,X12,X12)
| ~ state(X0,X11)
| ~ man(X0,X12)
| ~ forename(X0,X10)
| ~ jules_forename(X0,X10)
| ~ man(X0,X12)
| ~ of(X0,X10,X12)
| ~ smoke(X7,X9)
| ~ present(X7,X9)
| ~ agent(X7,X9,sK9_skl(X7,X10,X11,X12,X2,X13,X14,X4,X0))
| ~ event(X7,X9)
| ~ accessible_world(X0,X7)
| ~ think_believe_consider(X0,X8)
| ~ present(X0,X8)
| ~ event(X0,X8)
| ~ theme(X0,X8,X7)
| ~ agent(X0,X8,X6)
| ~ proposition(X0,X7)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X6)
| ~ of(X0,X5,X6)
| ~ forename(X0,X3)
| ~ jules_forename(X0,X3)
| ~ man(X0,X4)
| ~ of(X0,X3,X4)
| ~ forename(X0,X1)
| ~ vincent_forename(X0,X1)
| ~ man(X0,X2)
| ~ 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,X13,X14] :
( ~ smoke(X13,X14)
| ~ present(X13,X14)
| ~ agent(X13,X14,X4)
| ~ event(X13,X14)
| ~ accessible_world(X0,X13)
| ~ think_believe_consider(X0,X12)
| ~ present(X0,X12)
| ~ event(X0,X12)
| ~ theme(X0,X12,X13)
| ~ agent(X0,X12,X2)
| ~ proposition(X0,X13)
| ~ be(X0,X10,X11,X11)
| ~ state(X0,X10)
| ~ forename(X0,X9)
| ~ jules_forename(X0,X9)
| ~ man(X0,X11)
| ~ of(X0,X9,X11)
| man(X7,sK9_skl(X7,X9,X10,X11,X2,X12,X13,X4,X0))
| ~ accessible_world(X0,X7)
| ~ think_believe_consider(X0,X8)
| ~ present(X0,X8)
| ~ event(X0,X8)
| ~ theme(X0,X8,X7)
| ~ agent(X0,X8,X6)
| ~ proposition(X0,X7)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X6)
| ~ of(X0,X5,X6)
| ~ forename(X0,X3)
| ~ jules_forename(X0,X3)
| ~ man(X0,X4)
| ~ of(X0,X3,X4)
| ~ forename(X0,X1)
| ~ vincent_forename(X0,X1)
| ~ man(X0,X2)
| ~ 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,X14,X15] :
( ~ smoke(X14,X15)
| ~ present(X14,X15)
| ~ agent(X14,X15,X4)
| ~ event(X14,X15)
| ~ accessible_world(X0,X14)
| ~ think_believe_consider(X0,X13)
| ~ present(X0,X13)
| ~ event(X0,X13)
| ~ theme(X0,X13,X14)
| ~ agent(X0,X13,X2)
| ~ proposition(X0,X14)
| ~ be(X0,X11,X12,X12)
| ~ state(X0,X11)
| ~ forename(X0,X10)
| ~ jules_forename(X0,X10)
| ~ man(X0,X12)
| ~ of(X0,X10,X12)
| ~ smoke(X7,X9)
| ~ present(X7,X9)
| ~ agent(X7,X9,sK9_skl(X7,X10,X11,X12,X2,X13,X14,X4,X0))
| ~ event(X7,X9)
| ~ accessible_world(X0,X7)
| ~ think_believe_consider(X0,X8)
| ~ present(X0,X8)
| ~ event(X0,X8)
| ~ theme(X0,X8,X7)
| ~ agent(X0,X8,X6)
| ~ proposition(X0,X7)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X6)
| ~ of(X0,X5,X6)
| ~ forename(X0,X3)
| ~ jules_forename(X0,X3)
| ~ man(X0,X4)
| ~ of(X0,X3,X4)
| ~ forename(X0,X1)
| ~ vincent_forename(X0,X1)
| ~ man(X0,X2)
| ~ of(X0,X1,X2)
| ~ actual_world(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f279]) ).
fof(f373,plain,
! [X0] :
( man(sK4_skl,X0)
| ~ man(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f186,f266]) ).
fof(f440,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14] :
( ~ smoke(X13,X14)
| ~ present(X13,X14)
| ~ agent(X13,X14,X4)
| ~ event(X13,X14)
| ~ accessible_world(X0,X13)
| ~ think_believe_consider(X0,X12)
| ~ present(X0,X12)
| ~ event(X0,X12)
| ~ theme(X0,X12,X13)
| ~ agent(X0,X12,X2)
| ~ proposition(X0,X13)
| ~ be(X0,X10,X11,X11)
| ~ state(X0,X10)
| ~ forename(X0,X9)
| ~ jules_forename(X0,X9)
| ~ man(X0,X11)
| ~ of(X0,X9,X11)
| man(X7,sK9_skl(X7,X9,X10,X11,X2,X12,X13,X4,X0))
| ~ accessible_world(X0,X7)
| ~ think_believe_consider(X0,X8)
| ~ present(X0,X8)
| ~ event(X0,X8)
| ~ theme(X0,X8,X7)
| ~ agent(X0,X8,X6)
| ~ proposition(X0,X7)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X6)
| ~ of(X0,X5,X6)
| ~ forename(X0,X3)
| ~ jules_forename(X0,X3)
| ~ man(X0,X4)
| ~ of(X0,X3,X4)
| ~ vincent_forename(X0,X1)
| ~ man(X0,X2)
| ~ of(X0,X1,X2)
| ~ actual_world(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f280,f77]) ).
fof(f442,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ~ smoke(X10,X11)
| ~ present(X10,X11)
| ~ agent(X10,X11,X1)
| ~ event(X10,X11)
| ~ accessible_world(sK0_skl,X10)
| ~ think_believe_consider(sK0_skl,X9)
| ~ present(sK0_skl,X9)
| ~ event(sK0_skl,X9)
| ~ theme(sK0_skl,X9,X10)
| ~ agent(sK0_skl,X9,sK6_skl)
| ~ proposition(sK0_skl,X10)
| ~ be(sK0_skl,X7,X8,X8)
| ~ state(sK0_skl,X7)
| ~ forename(sK0_skl,X6)
| ~ jules_forename(sK0_skl,X6)
| ~ man(sK0_skl,X8)
| ~ of(sK0_skl,X6,X8)
| man(X4,sK9_skl(X4,X6,X7,X8,sK6_skl,X9,X10,X1,sK0_skl))
| ~ accessible_world(sK0_skl,X4)
| ~ think_believe_consider(sK0_skl,X5)
| ~ present(sK0_skl,X5)
| ~ event(sK0_skl,X5)
| ~ theme(sK0_skl,X5,X4)
| ~ agent(sK0_skl,X5,X3)
| ~ proposition(sK0_skl,X4)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X3)
| ~ of(sK0_skl,X2,X3)
| ~ forename(sK0_skl,X0)
| ~ jules_forename(sK0_skl,X0)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X0,X1)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ actual_world(sK0_skl) ),
inference(resolution,[status(thm)],[f440,f256]) ).
fof(f444,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ~ smoke(X10,X11)
| ~ present(X10,X11)
| ~ agent(X10,X11,X1)
| ~ event(X10,X11)
| ~ accessible_world(sK0_skl,X10)
| ~ think_believe_consider(sK0_skl,X9)
| ~ present(sK0_skl,X9)
| ~ event(sK0_skl,X9)
| ~ theme(sK0_skl,X9,X10)
| ~ agent(sK0_skl,X9,sK6_skl)
| ~ proposition(sK0_skl,X10)
| ~ be(sK0_skl,X7,X8,X8)
| ~ state(sK0_skl,X7)
| ~ forename(sK0_skl,X6)
| ~ jules_forename(sK0_skl,X6)
| ~ man(sK0_skl,X8)
| ~ of(sK0_skl,X6,X8)
| man(X4,sK9_skl(X4,X6,X7,X8,sK6_skl,X9,X10,X1,sK0_skl))
| ~ accessible_world(sK0_skl,X4)
| ~ think_believe_consider(sK0_skl,X5)
| ~ present(sK0_skl,X5)
| ~ event(sK0_skl,X5)
| ~ theme(sK0_skl,X5,X4)
| ~ agent(sK0_skl,X5,X3)
| ~ proposition(sK0_skl,X4)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X3)
| ~ of(sK0_skl,X2,X3)
| ~ forename(sK0_skl,X0)
| ~ jules_forename(sK0_skl,X0)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X0,X1)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f442,f255]) ).
fof(f450,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
( ~ smoke(X14,X15)
| ~ present(X14,X15)
| ~ agent(X14,X15,X4)
| ~ event(X14,X15)
| ~ accessible_world(X0,X14)
| ~ think_believe_consider(X0,X13)
| ~ present(X0,X13)
| ~ event(X0,X13)
| ~ theme(X0,X13,X14)
| ~ agent(X0,X13,X2)
| ~ proposition(X0,X14)
| ~ be(X0,X11,X12,X12)
| ~ state(X0,X11)
| ~ forename(X0,X10)
| ~ jules_forename(X0,X10)
| ~ man(X0,X12)
| ~ of(X0,X10,X12)
| ~ smoke(X7,X9)
| ~ present(X7,X9)
| ~ agent(X7,X9,sK9_skl(X7,X10,X11,X12,X2,X13,X14,X4,X0))
| ~ event(X7,X9)
| ~ accessible_world(X0,X7)
| ~ think_believe_consider(X0,X8)
| ~ present(X0,X8)
| ~ event(X0,X8)
| ~ theme(X0,X8,X7)
| ~ agent(X0,X8,X6)
| ~ proposition(X0,X7)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X6)
| ~ of(X0,X5,X6)
| ~ forename(X0,X3)
| ~ jules_forename(X0,X3)
| ~ man(X0,X4)
| ~ of(X0,X3,X4)
| ~ vincent_forename(X0,X1)
| ~ man(X0,X2)
| ~ of(X0,X1,X2)
| ~ actual_world(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f281,f77]) ).
fof(f452,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( ~ smoke(X11,X12)
| ~ present(X11,X12)
| ~ agent(X11,X12,X1)
| ~ event(X11,X12)
| ~ accessible_world(sK0_skl,X11)
| ~ think_believe_consider(sK0_skl,X10)
| ~ present(sK0_skl,X10)
| ~ event(sK0_skl,X10)
| ~ theme(sK0_skl,X10,X11)
| ~ agent(sK0_skl,X10,sK6_skl)
| ~ proposition(sK0_skl,X11)
| ~ be(sK0_skl,X8,X9,X9)
| ~ state(sK0_skl,X8)
| ~ forename(sK0_skl,X7)
| ~ jules_forename(sK0_skl,X7)
| ~ man(sK0_skl,X9)
| ~ of(sK0_skl,X7,X9)
| ~ smoke(X4,X6)
| ~ present(X4,X6)
| ~ agent(X4,X6,sK9_skl(X4,X7,X8,X9,sK6_skl,X10,X11,X1,sK0_skl))
| ~ event(X4,X6)
| ~ accessible_world(sK0_skl,X4)
| ~ think_believe_consider(sK0_skl,X5)
| ~ present(sK0_skl,X5)
| ~ event(sK0_skl,X5)
| ~ theme(sK0_skl,X5,X4)
| ~ agent(sK0_skl,X5,X3)
| ~ proposition(sK0_skl,X4)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X3)
| ~ of(sK0_skl,X2,X3)
| ~ forename(sK0_skl,X0)
| ~ jules_forename(sK0_skl,X0)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X0,X1)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ actual_world(sK0_skl) ),
inference(resolution,[status(thm)],[f450,f256]) ).
fof(f454,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( ~ smoke(X11,X12)
| ~ present(X11,X12)
| ~ agent(X11,X12,X1)
| ~ event(X11,X12)
| ~ accessible_world(sK0_skl,X11)
| ~ think_believe_consider(sK0_skl,X10)
| ~ present(sK0_skl,X10)
| ~ event(sK0_skl,X10)
| ~ theme(sK0_skl,X10,X11)
| ~ agent(sK0_skl,X10,sK6_skl)
| ~ proposition(sK0_skl,X11)
| ~ be(sK0_skl,X8,X9,X9)
| ~ state(sK0_skl,X8)
| ~ forename(sK0_skl,X7)
| ~ jules_forename(sK0_skl,X7)
| ~ man(sK0_skl,X9)
| ~ of(sK0_skl,X7,X9)
| ~ smoke(X4,X6)
| ~ present(X4,X6)
| ~ agent(X4,X6,sK9_skl(X4,X7,X8,X9,sK6_skl,X10,X11,X1,sK0_skl))
| ~ event(X4,X6)
| ~ accessible_world(sK0_skl,X4)
| ~ think_believe_consider(sK0_skl,X5)
| ~ present(sK0_skl,X5)
| ~ event(sK0_skl,X5)
| ~ theme(sK0_skl,X5,X4)
| ~ agent(sK0_skl,X5,X3)
| ~ proposition(sK0_skl,X4)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X3)
| ~ of(sK0_skl,X2,X3)
| ~ forename(sK0_skl,X0)
| ~ jules_forename(sK0_skl,X0)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X0,X1)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f452,f255]) ).
fof(f468,plain,
man(sK4_skl,sK1_skl),
inference(resolution,[status(thm)],[f373,f272]) ).
fof(f484,plain,
smoke(sK4_skl,sK8_skl(sK1_skl)),
inference(resolution,[status(thm)],[f468,f270]) ).
fof(f485,plain,
present(sK4_skl,sK8_skl(sK1_skl)),
inference(resolution,[status(thm)],[f468,f269]) ).
fof(f486,plain,
agent(sK4_skl,sK8_skl(sK1_skl),sK1_skl),
inference(resolution,[status(thm)],[f468,f268]) ).
fof(f597,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ~ smoke(X10,X11)
| ~ present(X10,X11)
| ~ agent(X10,X11,X1)
| ~ event(X10,X11)
| ~ accessible_world(sK0_skl,X10)
| ~ think_believe_consider(sK0_skl,X9)
| ~ present(sK0_skl,X9)
| ~ event(sK0_skl,X9)
| ~ theme(sK0_skl,X9,X10)
| ~ agent(sK0_skl,X9,sK6_skl)
| ~ proposition(sK0_skl,X10)
| ~ be(sK0_skl,X7,X8,X8)
| ~ state(sK0_skl,X7)
| ~ forename(sK0_skl,X6)
| ~ jules_forename(sK0_skl,X6)
| ~ man(sK0_skl,X8)
| ~ of(sK0_skl,X6,X8)
| man(X4,sK9_skl(X4,X6,X7,X8,sK6_skl,X9,X10,X1,sK0_skl))
| ~ accessible_world(sK0_skl,X4)
| ~ think_believe_consider(sK0_skl,X5)
| ~ present(sK0_skl,X5)
| ~ event(sK0_skl,X5)
| ~ theme(sK0_skl,X5,X4)
| ~ agent(sK0_skl,X5,X3)
| ~ proposition(sK0_skl,X4)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X3)
| ~ of(sK0_skl,X2,X3)
| ~ forename(sK0_skl,X0)
| ~ jules_forename(sK0_skl,X0)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X0,X1)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f444,f257]) ).
fof(f598,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,sK6_skl)
| ~ proposition(sK0_skl,X8)
| ~ be(sK0_skl,X5,X6,X6)
| ~ state(sK0_skl,X5)
| ~ forename(sK0_skl,X4)
| ~ jules_forename(sK0_skl,X4)
| ~ man(sK0_skl,X6)
| ~ of(sK0_skl,X4,X6)
| man(X2,sK9_skl(X2,X4,X5,X6,sK6_skl,X7,X8,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X2)
| ~ think_believe_consider(sK0_skl,X3)
| ~ present(sK0_skl,X3)
| ~ event(sK0_skl,X3)
| ~ theme(sK0_skl,X3,X2)
| ~ agent(sK0_skl,X3,X1)
| ~ proposition(sK0_skl,X2)
| ~ forename(sK0_skl,X0)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(resolution,[status(thm)],[f597,f271]) ).
fof(f600,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,sK6_skl)
| ~ proposition(sK0_skl,X8)
| ~ be(sK0_skl,X5,X6,X6)
| ~ state(sK0_skl,X5)
| ~ forename(sK0_skl,X4)
| ~ jules_forename(sK0_skl,X4)
| ~ man(sK0_skl,X6)
| ~ of(sK0_skl,X4,X6)
| man(X2,sK9_skl(X2,X4,X5,X6,sK6_skl,X7,X8,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X2)
| ~ think_believe_consider(sK0_skl,X3)
| ~ present(sK0_skl,X3)
| ~ event(sK0_skl,X3)
| ~ theme(sK0_skl,X3,X2)
| ~ agent(sK0_skl,X3,X1)
| ~ proposition(sK0_skl,X2)
| ~ forename(sK0_skl,X0)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f598,f258]) ).
fof(f610,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( ~ smoke(X11,X12)
| ~ present(X11,X12)
| ~ agent(X11,X12,X1)
| ~ event(X11,X12)
| ~ accessible_world(sK0_skl,X11)
| ~ think_believe_consider(sK0_skl,X10)
| ~ present(sK0_skl,X10)
| ~ event(sK0_skl,X10)
| ~ theme(sK0_skl,X10,X11)
| ~ agent(sK0_skl,X10,sK6_skl)
| ~ proposition(sK0_skl,X11)
| ~ be(sK0_skl,X8,X9,X9)
| ~ state(sK0_skl,X8)
| ~ forename(sK0_skl,X7)
| ~ jules_forename(sK0_skl,X7)
| ~ man(sK0_skl,X9)
| ~ of(sK0_skl,X7,X9)
| ~ smoke(X4,X6)
| ~ present(X4,X6)
| ~ agent(X4,X6,sK9_skl(X4,X7,X8,X9,sK6_skl,X10,X11,X1,sK0_skl))
| ~ event(X4,X6)
| ~ accessible_world(sK0_skl,X4)
| ~ think_believe_consider(sK0_skl,X5)
| ~ present(sK0_skl,X5)
| ~ event(sK0_skl,X5)
| ~ theme(sK0_skl,X5,X4)
| ~ agent(sK0_skl,X5,X3)
| ~ proposition(sK0_skl,X4)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X3)
| ~ of(sK0_skl,X2,X3)
| ~ forename(sK0_skl,X0)
| ~ jules_forename(sK0_skl,X0)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X0,X1)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f454,f257]) ).
fof(f611,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,sK6_skl)
| ~ proposition(sK0_skl,X9)
| ~ be(sK0_skl,X6,X7,X7)
| ~ state(sK0_skl,X6)
| ~ forename(sK0_skl,X5)
| ~ jules_forename(sK0_skl,X5)
| ~ man(sK0_skl,X7)
| ~ of(sK0_skl,X5,X7)
| ~ smoke(X2,X4)
| ~ present(X2,X4)
| ~ agent(X2,X4,sK9_skl(X2,X5,X6,X7,sK6_skl,X8,X9,sK1_skl,sK0_skl))
| ~ event(X2,X4)
| ~ accessible_world(sK0_skl,X2)
| ~ think_believe_consider(sK0_skl,X3)
| ~ present(sK0_skl,X3)
| ~ event(sK0_skl,X3)
| ~ theme(sK0_skl,X3,X2)
| ~ agent(sK0_skl,X3,X1)
| ~ proposition(sK0_skl,X2)
| ~ forename(sK0_skl,X0)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(resolution,[status(thm)],[f610,f271]) ).
fof(f613,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,sK6_skl)
| ~ proposition(sK0_skl,X9)
| ~ be(sK0_skl,X6,X7,X7)
| ~ state(sK0_skl,X6)
| ~ forename(sK0_skl,X5)
| ~ jules_forename(sK0_skl,X5)
| ~ man(sK0_skl,X7)
| ~ of(sK0_skl,X5,X7)
| ~ smoke(X2,X4)
| ~ present(X2,X4)
| ~ agent(X2,X4,sK9_skl(X2,X5,X6,X7,sK6_skl,X8,X9,sK1_skl,sK0_skl))
| ~ event(X2,X4)
| ~ accessible_world(sK0_skl,X2)
| ~ think_believe_consider(sK0_skl,X3)
| ~ present(sK0_skl,X3)
| ~ event(sK0_skl,X3)
| ~ theme(sK0_skl,X3,X2)
| ~ agent(sK0_skl,X3,X1)
| ~ proposition(sK0_skl,X2)
| ~ forename(sK0_skl,X0)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f611,f258]) ).
fof(f643,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,sK6_skl)
| ~ proposition(sK0_skl,X8)
| ~ be(sK0_skl,X5,X6,X6)
| ~ state(sK0_skl,X5)
| ~ forename(sK0_skl,X4)
| ~ jules_forename(sK0_skl,X4)
| ~ man(sK0_skl,X6)
| ~ of(sK0_skl,X4,X6)
| man(X2,sK9_skl(X2,X4,X5,X6,sK6_skl,X7,X8,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X2)
| ~ think_believe_consider(sK0_skl,X3)
| ~ present(sK0_skl,X3)
| ~ event(sK0_skl,X3)
| ~ theme(sK0_skl,X3,X2)
| ~ agent(sK0_skl,X3,X1)
| ~ proposition(sK0_skl,X2)
| ~ forename(sK0_skl,X0)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f600,f272]) ).
fof(f645,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,X3,X4,X4)
| ~ state(sK0_skl,X3)
| ~ forename(sK0_skl,X2)
| ~ jules_forename(sK0_skl,X2)
| ~ man(sK0_skl,X4)
| ~ of(sK0_skl,X2,X4)
| man(X0,sK9_skl(X0,X2,X3,X4,sK6_skl,X5,X6,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)
| ~ forename(sK0_skl,sK7_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f643,f256]) ).
fof(f648,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,X3,X4,X4)
| ~ state(sK0_skl,X3)
| ~ forename(sK0_skl,X2)
| ~ jules_forename(sK0_skl,X2)
| ~ man(sK0_skl,X4)
| ~ of(sK0_skl,X2,X4)
| man(X0,sK9_skl(X0,X2,X3,X4,sK6_skl,X5,X6,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)
| ~ forename(sK0_skl,sK7_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f645,f273]) ).
fof(f669,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,sK6_skl)
| ~ proposition(sK0_skl,X9)
| ~ be(sK0_skl,X6,X7,X7)
| ~ state(sK0_skl,X6)
| ~ forename(sK0_skl,X5)
| ~ jules_forename(sK0_skl,X5)
| ~ man(sK0_skl,X7)
| ~ of(sK0_skl,X5,X7)
| ~ smoke(X2,X4)
| ~ present(X2,X4)
| ~ agent(X2,X4,sK9_skl(X2,X5,X6,X7,sK6_skl,X8,X9,sK1_skl,sK0_skl))
| ~ event(X2,X4)
| ~ accessible_world(sK0_skl,X2)
| ~ think_believe_consider(sK0_skl,X3)
| ~ present(sK0_skl,X3)
| ~ event(sK0_skl,X3)
| ~ theme(sK0_skl,X3,X2)
| ~ agent(sK0_skl,X3,X1)
| ~ proposition(sK0_skl,X2)
| ~ forename(sK0_skl,X0)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f613,f272]) ).
fof(f671,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,X4,X5,X5)
| ~ state(sK0_skl,X4)
| ~ forename(sK0_skl,X3)
| ~ jules_forename(sK0_skl,X3)
| ~ man(sK0_skl,X5)
| ~ of(sK0_skl,X3,X5)
| ~ smoke(X0,X2)
| ~ present(X0,X2)
| ~ agent(X0,X2,sK9_skl(X0,X3,X4,X5,sK6_skl,X6,X7,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)
| ~ forename(sK0_skl,sK7_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f669,f256]) ).
fof(f674,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,X4,X5,X5)
| ~ state(sK0_skl,X4)
| ~ forename(sK0_skl,X3)
| ~ jules_forename(sK0_skl,X3)
| ~ man(sK0_skl,X5)
| ~ of(sK0_skl,X3,X5)
| ~ smoke(X0,X2)
| ~ present(X0,X2)
| ~ agent(X0,X2,sK9_skl(X0,X3,X4,X5,sK6_skl,X6,X7,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)
| ~ forename(sK0_skl,sK7_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f671,f273]) ).
fof(f733,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,X3,X4,X4)
| ~ state(sK0_skl,X3)
| ~ forename(sK0_skl,X2)
| ~ jules_forename(sK0_skl,X2)
| ~ man(sK0_skl,X4)
| ~ of(sK0_skl,X2,X4)
| man(X0,sK9_skl(X0,X2,X3,X4,sK6_skl,X5,X6,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)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f648,f77]) ).
fof(f734,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,X2,X3,X3)
| ~ state(sK0_skl,X2)
| ~ forename(sK0_skl,X1)
| ~ jules_forename(sK0_skl,X1)
| ~ man(sK0_skl,X3)
| ~ of(sK0_skl,X1,X3)
| man(X0,sK9_skl(X0,X1,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)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f733,f261]) ).
fof(f735,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,X2,X3,X3)
| ~ state(sK0_skl,X2)
| ~ jules_forename(sK0_skl,X1)
| ~ man(sK0_skl,X3)
| ~ of(sK0_skl,X1,X3)
| man(X0,sK9_skl(X0,X1,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)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f734,f75]) ).
fof(f785,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,X4,X5,X5)
| ~ state(sK0_skl,X4)
| ~ forename(sK0_skl,X3)
| ~ jules_forename(sK0_skl,X3)
| ~ man(sK0_skl,X5)
| ~ of(sK0_skl,X3,X5)
| ~ smoke(X0,X2)
| ~ present(X0,X2)
| ~ agent(X0,X2,sK9_skl(X0,X3,X4,X5,sK6_skl,X6,X7,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)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f674,f77]) ).
fof(f786,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,X3,X4,X4)
| ~ state(sK0_skl,X3)
| ~ forename(sK0_skl,X2)
| ~ jules_forename(sK0_skl,X2)
| ~ man(sK0_skl,X4)
| ~ of(sK0_skl,X2,X4)
| ~ smoke(X0,X1)
| ~ present(X0,X1)
| ~ agent(X0,X1,sK9_skl(X0,X2,X3,X4,sK6_skl,X5,X6,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)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f785,f261]) ).
fof(f787,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,X3,X4,X4)
| ~ state(sK0_skl,X3)
| ~ jules_forename(sK0_skl,X2)
| ~ man(sK0_skl,X4)
| ~ of(sK0_skl,X2,X4)
| ~ smoke(X0,X1)
| ~ present(X0,X1)
| ~ agent(X0,X1,sK9_skl(X0,X2,X3,X4,sK6_skl,X5,X6,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)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f786,f75]) ).
fof(f813,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,X2,X3,X3)
| ~ state(sK0_skl,X2)
| ~ jules_forename(sK0_skl,X1)
| ~ man(sK0_skl,X3)
| ~ of(sK0_skl,X1,X3)
| man(X0,sK9_skl(X0,X1,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)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f735,f274]) ).
fof(f814,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,X1,X2,X2)
| ~ state(sK0_skl,X1)
| ~ jules_forename(sK0_skl,X0)
| ~ man(sK0_skl,X2)
| ~ of(sK0_skl,X0,X2)
| man(sK4_skl,sK9_skl(sK4_skl,X0,X1,X2,sK6_skl,X3,X4,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)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl) ),
inference(resolution,[status(thm)],[f813,f262]) ).
fof(f815,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,X1,X2,X2)
| ~ state(sK0_skl,X1)
| ~ jules_forename(sK0_skl,X0)
| ~ man(sK0_skl,X2)
| ~ of(sK0_skl,X0,X2)
| man(sK4_skl,sK9_skl(sK4_skl,X0,X1,X2,sK6_skl,X3,X4,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)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f814,f257]) ).
fof(f816,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,X1,X2,X2)
| ~ state(sK0_skl,X1)
| ~ jules_forename(sK0_skl,X0)
| ~ man(sK0_skl,X2)
| ~ of(sK0_skl,X0,X2)
| man(sK4_skl,sK9_skl(sK4_skl,X0,X1,X2,sK6_skl,X3,X4,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(forward_subsumption_resolution,[status(thm)],[f815,f258]) ).
fof(f817,plain,
! [X0,X1,X2,X3] :
( ~ smoke(X2,X3)
| ~ present(X2,X3)
| ~ agent(X2,X3,sK1_skl)
| ~ event(X2,X3)
| ~ 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,sK1_skl,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)
| ~ event(sK0_skl,sK5_skl)
| ~ proposition(sK0_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f816,f271]) ).
fof(f819,plain,
! [X0,X1,X2,X3] :
( ~ smoke(X2,X3)
| ~ present(X2,X3)
| ~ agent(X2,X3,sK1_skl)
| ~ event(X2,X3)
| ~ 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,sK1_skl,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)
| ~ event(sK0_skl,sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f817,f260]) ).
fof(f827,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,sK1_skl,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)
| ~ event(sK0_skl,sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f819,f133]) ).
fof(f828,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,sK1_skl,sK6_skl,X0,X1,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)],[f827,f277]) ).
fof(f829,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,sK1_skl,sK6_skl,X0,X1,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)],[f828,f263]) ).
fof(f830,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,sK1_skl,sK6_skl,X0,X1,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f829,f264]) ).
fof(f831,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(sK0_skl,sK1_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,X0,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f830,f261]) ).
fof(f832,plain,
! [X0,X1] :
( ~ smoke(X0,X1)
| ~ present(X0,X1)
| ~ agent(X0,X1,sK1_skl)
| ~ accessible_world(sK0_skl,X0)
| ~ 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(sK0_skl,sK1_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,X0,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f831]) ).
fof(f833,plain,
! [X0,X1] :
( ~ smoke(X0,X1)
| ~ present(X0,X1)
| ~ agent(X0,X1,sK1_skl)
| ~ accessible_world(sK0_skl,X0)
| ~ 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(sK0_skl,sK1_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,X0,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,sK4_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f832,f265]) ).
fof(f840,plain,
! [X0,X1] :
( ~ smoke(X0,X1)
| ~ present(X0,X1)
| ~ agent(X0,X1,sK1_skl)
| ~ accessible_world(sK0_skl,X0)
| ~ 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(sK0_skl,sK1_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,X0,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f833,f266]) ).
fof(f841,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ present(sK4_skl,sK8_skl(sK1_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,sK4_skl)
| ~ proposition(sK0_skl,sK4_skl)
| ~ 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,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f840,f486]) ).
fof(f842,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ present(sK4_skl,sK8_skl(sK1_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,sK4_skl)
| ~ proposition(sK0_skl,sK4_skl)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f841,f272]) ).
fof(f843,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ present(sK4_skl,sK8_skl(sK1_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,sK4_skl)
| ~ proposition(sK0_skl,sK4_skl)
| ~ state(sK0_skl,sK2_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f842,f273]) ).
fof(f844,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,sK4_skl)
| ~ proposition(sK0_skl,sK4_skl)
| ~ state(sK0_skl,sK2_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f843,f485]) ).
fof(f845,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ accessible_world(sK0_skl,sK4_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,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f844,f276]) ).
fof(f852,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ accessible_world(sK0_skl,sK4_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,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f845,f260]) ).
fof(f853,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f852,f262]) ).
fof(f854,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ present(sK0_skl,sK5_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f853,f263]) ).
fof(f855,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f854,f264]) ).
fof(f856,plain,
( ~ accessible_world(sK0_skl,sK4_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f855,f484]) ).
fof(f857,plain,
man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f856,f266]) ).
fof(f863,plain,
smoke(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl))),
inference(resolution,[status(thm)],[f857,f270]) ).
fof(f864,plain,
present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl))),
inference(resolution,[status(thm)],[f857,f269]) ).
fof(f865,plain,
agent(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)),sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)),
inference(resolution,[status(thm)],[f857,f268]) ).
fof(f866,plain,
event(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl))),
inference(resolution,[status(thm)],[f857,f267]) ).
fof(f899,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,X3,X4,X4)
| ~ state(sK0_skl,X3)
| ~ jules_forename(sK0_skl,X2)
| ~ man(sK0_skl,X4)
| ~ of(sK0_skl,X2,X4)
| ~ smoke(X0,X1)
| ~ present(X0,X1)
| ~ agent(X0,X1,sK9_skl(X0,X2,X3,X4,sK6_skl,X5,X6,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)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f787,f274]) ).
fof(f935,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,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ event(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_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)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl) ),
inference(resolution,[status(thm)],[f865,f899]) ).
fof(f936,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,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ event(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_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)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f935]) ).
fof(f937,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,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ event(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_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)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f936,f257]) ).
fof(f1097,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,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ event(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_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(forward_subsumption_resolution,[status(thm)],[f937,f258]) ).
fof(f1098,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,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_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)],[f1097,f866]) ).
fof(f1099,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,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_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)],[f1098,f260]) ).
fof(f1100,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,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)))
| ~ present(sK4_skl,sK8_skl(sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_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)],[f1099,f262]) ).
fof(f1101,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,sK1_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)],[f1100,f864]) ).
fof(f1102,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,sK1_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)],[f1101,f133]) ).
fof(f1103,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,sK1_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)],[f1102,f263]) ).
fof(f1104,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)],[f1103,f863]) ).
fof(f1105,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)],[f1104,f264]) ).
fof(f1106,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)],[f1105,f265]) ).
fof(f1107,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)],[f1106,f277]) ).
fof(f1108,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)],[f1107,f266]) ).
fof(f1109,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)],[f1108,f271]) ).
fof(f1110,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)],[f1109,f261]) ).
fof(f1111,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)],[f1110,f272]) ).
fof(f1112,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)],[f1111,f273]) ).
fof(f1113,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ present(sK4_skl,sK8_skl(sK1_skl))
| ~ state(sK0_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f1112,f486]) ).
fof(f1114,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ present(sK4_skl,sK8_skl(sK1_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1113,f276]) ).
fof(f1116,plain,
~ smoke(sK4_skl,sK8_skl(sK1_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f1114,f485]) ).
fof(f1117,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f484,f1116]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP251+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 01:55:40 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.54/0.60 % Refutation found
% 0.54/0.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.54/0.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.54/0.61 % Elapsed time: 0.241677 seconds
% 0.54/0.61 % CPU time: 1.615279 seconds
% 0.54/0.61 % Total memory used: 69.819 MB
% 0.54/0.61 % Net memory used: 67.577 MB
%------------------------------------------------------------------------------