%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NLP252+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:39 PM UTC 2026
% Result : Theorem 0.12s 5.56s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 5
% Syntax : Number of formulae : 121 ( 27 unt; 0 def)
% Number of atoms : 1880 ( 0 equ)
% Maximal formula atoms : 66 ( 15 avg)
% Number of connectives : 3355 (1596 ~;1552 |; 199 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 57 ( 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-8 aty)
% Number of variables : 506 ( 438 !; 68 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [U,V] :
( jules_forename(U,V)
=> forename(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [U,V] :
( vincent_forename(U,V)
=> forename(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [U,V] :
( smoke(U,V)
=> event(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [U,V,W] :
( ( man(V,U)
& accessible_world(V,W) )
=> man(W,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,conjecture,
~ ( ~ ? [X5] :
( ? [X6,X7,X8,V,W,X,Y,Z,X1,X2,X9,X10] :
( ? [X11] :
( smoke(X10,X11)
& present(X10,X11)
& agent(X10,X11,X1)
& event(X10,X11) )
& accessible_world(X5,X10)
& think_believe_consider(X5,X9)
& present(X5,X9)
& event(X5,X9)
& theme(X5,X9,X10)
& agent(X5,X9,X6)
& proposition(X5,X10)
& 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,X8)
& jules_forename(X5,X8)
& of(X5,X8,X1)
& 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/sandbox/benchmark/theBenchmark.p') ).
fof(f73,negated_conjecture,
~ ~ ( ~ ? [X5] :
( ? [X6,X7,X8,V,W,X,Y,Z,X1,X2,X9,X10] :
( ? [X11] :
( smoke(X10,X11)
& present(X10,X11)
& agent(X10,X11,X1)
& event(X10,X11) )
& accessible_world(X5,X10)
& think_believe_consider(X5,X9)
& present(X5,X9)
& event(X5,X9)
& theme(X5,X9,X10)
& agent(X5,X9,X6)
& proposition(X5,X10)
& 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,X8)
& jules_forename(X5,X8)
& of(X5,X8,X1)
& 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,V,W,X,Y,Z,X1,X2,X9,X10] :
( ! [X11] :
( ~ smoke(X10,X11)
| ~ present(X10,X11)
| ~ agent(X10,X11,X1)
| ~ event(X10,X11) )
| ~ accessible_world(X5,X10)
| ~ think_believe_consider(X5,X9)
| ~ present(X5,X9)
| ~ event(X5,X9)
| ~ theme(X5,X9,X10)
| ~ agent(X5,X9,X6)
| ~ proposition(X5,X10)
| ~ 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,X8)
| ~ jules_forename(X5,X8)
| ~ of(X5,X8,X1)
| ~ 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] :
( ! [X1,X10] :
( ! [X11] :
( ~ smoke(X10,X11)
| ~ present(X10,X11)
| ~ agent(X10,X11,X1)
| ~ event(X10,X11) )
| ~ accessible_world(X5,X10)
| ! [X9] :
( ~ think_believe_consider(X5,X9)
| ~ present(X5,X9)
| ~ event(X5,X9)
| ~ theme(X5,X9,X10)
| ! [X6] :
( ~ agent(X5,X9,X6)
| ~ proposition(X5,X10)
| ! [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)
| ! [X8] :
( ~ forename(X5,X8)
| ~ jules_forename(X5,X8)
| ~ of(X5,X8,X1)
| ! [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] :
( ! [X1,X10] :
( ! [X11] :
( ~ smoke(X10,X11)
| ~ present(X10,X11)
| ~ agent(X10,X11,X1)
| ~ event(X10,X11) )
| ~ accessible_world(X5,X10)
| ! [X9] :
( ~ think_believe_consider(X5,X9)
| ~ present(X5,X9)
| ~ event(X5,X9)
| ~ theme(X5,X9,X10)
| ! [X6] :
( ~ agent(X5,X9,X6)
| ~ proposition(X5,X10)
| ! [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,X6,X9,X10,X1,X5))
| ~ event(Y,X4) )
& man(Y,sK9_skl(Y,Z,X2,X6,X9,X10,X1,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)
| ! [X8] :
( ~ forename(X5,X8)
| ~ jules_forename(X5,X8)
| ~ of(X5,X8,X1)
| ! [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,X6,X9,X10,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,X13] :
( ~ smoke(X12,X13)
| ~ present(X12,X13)
| ~ agent(X12,X13,X4)
| ~ 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,X2)
| ~ proposition(X0,X12)
| ~ be(X0,X10,X4,X4)
| ~ state(X0,X10)
| ~ man(X0,X4)
| ~ forename(X0,X9)
| ~ jules_forename(X0,X9)
| ~ man(X0,X4)
| ~ of(X0,X9,X4)
| man(X7,sK9_skl(X7,X9,X10,X2,X11,X12,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)
| ~ 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] :
( ~ 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,X11,X4,X4)
| ~ state(X0,X11)
| ~ man(X0,X4)
| ~ forename(X0,X10)
| ~ jules_forename(X0,X10)
| ~ man(X0,X4)
| ~ of(X0,X10,X4)
| ~ smoke(X7,X9)
| ~ present(X7,X9)
| ~ agent(X7,X9,sK9_skl(X7,X10,X11,X2,X12,X13,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)
| ~ 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] :
( ~ smoke(X12,X13)
| ~ present(X12,X13)
| ~ agent(X12,X13,X4)
| ~ 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,X2)
| ~ proposition(X0,X12)
| ~ be(X0,X10,X4,X4)
| ~ state(X0,X10)
| ~ forename(X0,X9)
| ~ jules_forename(X0,X9)
| ~ man(X0,X4)
| ~ of(X0,X9,X4)
| man(X7,sK9_skl(X7,X9,X10,X2,X11,X12,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)
| ~ 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] :
( ~ 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,X11,X4,X4)
| ~ state(X0,X11)
| ~ forename(X0,X10)
| ~ jules_forename(X0,X10)
| ~ man(X0,X4)
| ~ of(X0,X10,X4)
| ~ smoke(X7,X9)
| ~ present(X7,X9)
| ~ agent(X7,X9,sK9_skl(X7,X10,X11,X2,X12,X13,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)
| ~ 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(f295,plain,
! [X0] :
( man(sK4_skl,X0)
| ~ man(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f186,f266]) ).
fof(f339,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13] :
( ~ smoke(X12,X13)
| ~ present(X12,X13)
| ~ agent(X12,X13,X4)
| ~ 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,X2)
| ~ proposition(X0,X12)
| ~ be(X0,X10,X4,X4)
| ~ state(X0,X10)
| ~ forename(X0,X9)
| ~ jules_forename(X0,X9)
| ~ man(X0,X4)
| ~ of(X0,X9,X4)
| man(X7,sK9_skl(X7,X9,X10,X2,X11,X12,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)
| ~ 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(f341,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( ~ smoke(X9,X10)
| ~ present(X9,X10)
| ~ agent(X9,X10,X1)
| ~ 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,X7,X1,X1)
| ~ state(sK0_skl,X7)
| ~ forename(sK0_skl,X6)
| ~ jules_forename(sK0_skl,X6)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X6,X1)
| man(X4,sK9_skl(X4,X6,X7,sK6_skl,X8,X9,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)
| ~ of(sK0_skl,X0,X1)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ actual_world(sK0_skl) ),
inference(resolution,[status(thm)],[f339,f256]) ).
fof(f343,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( ~ smoke(X9,X10)
| ~ present(X9,X10)
| ~ agent(X9,X10,X1)
| ~ 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,X7,X1,X1)
| ~ state(sK0_skl,X7)
| ~ forename(sK0_skl,X6)
| ~ jules_forename(sK0_skl,X6)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X6,X1)
| man(X4,sK9_skl(X4,X6,X7,sK6_skl,X8,X9,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)
| ~ of(sK0_skl,X0,X1)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f341,f255]) ).
fof(f344,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,X11,X4,X4)
| ~ state(X0,X11)
| ~ forename(X0,X10)
| ~ jules_forename(X0,X10)
| ~ man(X0,X4)
| ~ of(X0,X10,X4)
| ~ smoke(X7,X9)
| ~ present(X7,X9)
| ~ agent(X7,X9,sK9_skl(X7,X10,X11,X2,X12,X13,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)
| ~ 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(f346,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,X8,X1,X1)
| ~ state(sK0_skl,X8)
| ~ forename(sK0_skl,X7)
| ~ jules_forename(sK0_skl,X7)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X7,X1)
| ~ smoke(X4,X6)
| ~ present(X4,X6)
| ~ agent(X4,X6,sK9_skl(X4,X7,X8,sK6_skl,X9,X10,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)
| ~ of(sK0_skl,X0,X1)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ actual_world(sK0_skl) ),
inference(resolution,[status(thm)],[f344,f256]) ).
fof(f348,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,X8,X1,X1)
| ~ state(sK0_skl,X8)
| ~ forename(sK0_skl,X7)
| ~ jules_forename(sK0_skl,X7)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X7,X1)
| ~ smoke(X4,X6)
| ~ present(X4,X6)
| ~ agent(X4,X6,sK9_skl(X4,X7,X8,sK6_skl,X9,X10,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)
| ~ of(sK0_skl,X0,X1)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f346,f255]) ).
fof(f367,plain,
man(sK4_skl,sK1_skl),
inference(resolution,[status(thm)],[f295,f272]) ).
fof(f415,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( ~ smoke(X9,X10)
| ~ present(X9,X10)
| ~ agent(X9,X10,X1)
| ~ 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,X7,X1,X1)
| ~ state(sK0_skl,X7)
| ~ forename(sK0_skl,X6)
| ~ jules_forename(sK0_skl,X6)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X6,X1)
| man(X4,sK9_skl(X4,X6,X7,sK6_skl,X8,X9,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)
| ~ of(sK0_skl,X0,X1)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f343,f257]) ).
fof(f416,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)
| man(X2,sK9_skl(X2,X4,X5,sK6_skl,X6,X7,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)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(resolution,[status(thm)],[f415,f271]) ).
fof(f418,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)
| man(X2,sK9_skl(X2,X4,X5,sK6_skl,X6,X7,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)],[f416,f258]) ).
fof(f425,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,X8,X1,X1)
| ~ state(sK0_skl,X8)
| ~ forename(sK0_skl,X7)
| ~ jules_forename(sK0_skl,X7)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X7,X1)
| ~ smoke(X4,X6)
| ~ present(X4,X6)
| ~ agent(X4,X6,sK9_skl(X4,X7,X8,sK6_skl,X9,X10,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)
| ~ of(sK0_skl,X0,X1)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f348,f257]) ).
fof(f426,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,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)
| ~ smoke(X2,X4)
| ~ present(X2,X4)
| ~ agent(X2,X4,sK9_skl(X2,X5,X6,sK6_skl,X7,X8,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)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(resolution,[status(thm)],[f425,f271]) ).
fof(f428,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,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)
| ~ smoke(X2,X4)
| ~ present(X2,X4)
| ~ agent(X2,X4,sK9_skl(X2,X5,X6,sK6_skl,X7,X8,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)],[f426,f258]) ).
fof(f463,plain,
smoke(sK4_skl,sK8_skl(sK1_skl)),
inference(resolution,[status(thm)],[f367,f270]) ).
fof(f464,plain,
present(sK4_skl,sK8_skl(sK1_skl)),
inference(resolution,[status(thm)],[f367,f269]) ).
fof(f465,plain,
agent(sK4_skl,sK8_skl(sK1_skl),sK1_skl),
inference(resolution,[status(thm)],[f367,f268]) ).
fof(f544,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)
| man(X2,sK9_skl(X2,X4,X5,sK6_skl,X6,X7,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) ),
inference(forward_subsumption_resolution,[status(thm)],[f418,f273]) ).
fof(f546,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)
| ~ forename(sK0_skl,X2)
| ~ 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)
| ~ forename(sK0_skl,sK7_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f544,f256]) ).
fof(f549,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)
| ~ forename(sK0_skl,X2)
| ~ 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)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f546,f77]) ).
fof(f573,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,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)
| ~ smoke(X2,X4)
| ~ present(X2,X4)
| ~ agent(X2,X4,sK9_skl(X2,X5,X6,sK6_skl,X7,X8,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) ),
inference(forward_subsumption_resolution,[status(thm)],[f428,f273]) ).
fof(f575,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)
| ~ 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)
| ~ forename(sK0_skl,sK7_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f573,f256]) ).
fof(f578,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)
| ~ 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)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f575,f77]) ).
fof(f693,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)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f549,f75]) ).
fof(f694,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)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f693,f261]) ).
fof(f695,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)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f694,f274]) ).
fof(f711,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)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f578,f75]) ).
fof(f712,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)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f711,f261]) ).
fof(f713,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)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ man(sK0_skl,sK6_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f712,f274]) ).
fof(f788,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)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f695,f257]) ).
fof(f789,plain,
! [X0,X1,X2,X3,X4] :
( ~ smoke(X3,X4)
| ~ present(X3,X4)
| ~ agent(X3,X4,sK1_skl)
| ~ event(X3,X4)
| ~ 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)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(resolution,[status(thm)],[f788,f262]) ).
fof(f790,plain,
! [X0,X1,X2,X3,X4] :
( ~ smoke(X3,X4)
| ~ present(X3,X4)
| ~ agent(X3,X4,sK1_skl)
| ~ event(X3,X4)
| ~ 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(forward_subsumption_resolution,[status(thm)],[f789,f258]) ).
fof(f796,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)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f713,f257]) ).
fof(f875,plain,
! [X0,X1,X2,X3,X4] :
( ~ smoke(X3,X4)
| ~ present(X3,X4)
| ~ agent(X3,X4,sK1_skl)
| ~ event(X3,X4)
| ~ 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)],[f790,f260]) ).
fof(f876,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,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(resolution,[status(thm)],[f875,f271]) ).
fof(f877,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)
| ~ event(sK0_skl,sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f876,f133]) ).
fof(f893,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(forward_subsumption_resolution,[status(thm)],[f877,f263]) ).
fof(f894,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)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f893,f277]) ).
fof(f895,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)
| ~ think_believe_consider(sK0_skl,sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f894,f264]) ).
fof(f896,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(forward_subsumption_resolution,[status(thm)],[f895,f265]) ).
fof(f897,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,sK6_skl,sK5_skl,X0,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f896,f261]) ).
fof(f898,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,sK6_skl,sK5_skl,X0,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f897,f266]) ).
fof(f909,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(forward_subsumption_resolution,[status(thm)],[f898,f272]) ).
fof(f910,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)
| ~ 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,sK4_skl,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f909,f465]) ).
fof(f911,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)
| ~ state(sK0_skl,sK2_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)],[f910,f273]) ).
fof(f914,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(forward_subsumption_resolution,[status(thm)],[f911,f276]) ).
fof(f915,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)
| ~ 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)],[f914,f464]) ).
fof(f916,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)
| ~ 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)],[f915,f260]) ).
fof(f917,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(forward_subsumption_resolution,[status(thm)],[f916,f262]) ).
fof(f918,plain,
( ~ 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)],[f917,f463]) ).
fof(f919,plain,
( ~ 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)],[f918,f263]) ).
fof(f924,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(forward_subsumption_resolution,[status(thm)],[f919,f264]) ).
fof(f925,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(resolution,[status(thm)],[f924,f265]) ).
fof(f926,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)],[f925,f266]) ).
fof(f927,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)],[f926,f270]) ).
fof(f928,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)],[f926,f269]) ).
fof(f929,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)],[f926,f268]) ).
fof(f997,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)))
| ~ event(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)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(resolution,[status(thm)],[f929,f796]) ).
fof(f998,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)))
| ~ event(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)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f997]) ).
fof(f999,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)))
| ~ event(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(forward_subsumption_resolution,[status(thm)],[f998,f258]) ).
fof(f1004,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)))
| ~ event(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)],[f999,f260]) ).
fof(f1005,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)))
| ~ event(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(resolution,[status(thm)],[f1004,f928]) ).
fof(f1006,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)))
| ~ event(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)],[f1005,f262]) ).
fof(f1010,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(forward_subsumption_resolution,[status(thm)],[f1006,f133]) ).
fof(f1011,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)
| ~ 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)],[f1010,f927]) ).
fof(f1012,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)
| ~ event(sK0_skl,sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1011,f133]) ).
fof(f1013,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(forward_subsumption_resolution,[status(thm)],[f1012,f263]) ).
fof(f1014,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)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f1013,f277]) ).
fof(f1015,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)
| ~ think_believe_consider(sK0_skl,sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1014,f264]) ).
fof(f1016,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(forward_subsumption_resolution,[status(thm)],[f1015,f265]) ).
fof(f1017,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ present(sK4_skl,sK8_skl(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)],[f1016,f465]) ).
fof(f1018,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ present(sK4_skl,sK8_skl(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)],[f1017,f266]) ).
fof(f1019,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ present(sK4_skl,sK8_skl(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)],[f1018,f271]) ).
fof(f1020,plain,
( ~ smoke(sK4_skl,sK8_skl(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(resolution,[status(thm)],[f1019,f464]) ).
fof(f1021,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ agent(sK0_skl,sK5_skl,sK6_skl)
| ~ state(sK0_skl,sK2_skl)
| ~ jules_forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1020,f272]) ).
fof(f1022,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ agent(sK0_skl,sK5_skl,sK6_skl)
| ~ state(sK0_skl,sK2_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1021,f273]) ).
fof(f1023,plain,
( ~ agent(sK0_skl,sK5_skl,sK6_skl)
| ~ state(sK0_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f1022,f463]) ).
fof(f1024,plain,
~ agent(sK0_skl,sK5_skl,sK6_skl),
inference(forward_subsumption_resolution,[status(thm)],[f1023,f276]) ).
fof(f1025,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1024,f261]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP252+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.35 % Computer : n012.cluster.edu
% 0.09/5.35 % Model : x86_64 x86_64
% 0.09/5.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.35 % Memory : 8046.5625MB
% 0.09/5.35 % OS : Linux 6.8.0-71-generic
% 0.09/5.35 % CPULimit : 300
% 0.09/5.35 % WCLimit : 300
% 0.09/5.35 % DateTime : Mon Sep 21 01:55:12 UTC 2026
% 0.09/5.36 % CPUTime :
% 0.09/5.37 % Drodi V4.1.1
% 0.12/5.56 % Refutation found
% 0.12/5.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/5.56 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/5.59 % Elapsed time: 0.220995 seconds
% 0.12/5.59 % CPU time: 1.479084 seconds
% 0.12/5.59 % Total memory used: 69.456 MB
% 0.12/5.59 % Net memory used: 67.098 MB
%------------------------------------------------------------------------------