%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NLP257+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 : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:31:40 PM UTC 2026
% Result : Theorem 0.12s 0.40s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 5
% Syntax : Number of formulae : 123 ( 28 unt; 0 def)
% Number of atoms : 1888 ( 0 equ)
% Maximal formula atoms : 66 ( 15 avg)
% Number of connectives : 3367 (1602 ~;1558 |; 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-9 aty)
% Number of variables : 544 ( 476 !; 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,X6)
& 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,V)
& 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)
& vincent_forename(X5,X8)
& of(X5,X8,V)
& forename(X5,X7)
& jules_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,X6)
& 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,V)
& 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)
& vincent_forename(X5,X8)
& of(X5,X8,V)
& forename(X5,X7)
& jules_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,X6)
| ~ 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,V)
| ~ 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)
| ~ vincent_forename(X5,X8)
| ~ of(X5,X8,V)
| ~ forename(X5,X7)
| ~ jules_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] :
( ! [X6,X10] :
( ! [X11] :
( ~ smoke(X10,X11)
| ~ present(X10,X11)
| ~ agent(X10,X11,X6)
| ~ event(X10,X11) )
| ~ accessible_world(X5,X10)
| ! [X9] :
( ~ think_believe_consider(X5,X9)
| ~ present(X5,X9)
| ~ event(X5,X9)
| ~ theme(X5,X9,X10)
| ! [V] :
( ~ agent(X5,X9,V)
| ~ proposition(X5,X10)
| ! [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)
| ~ 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)
| ~ vincent_forename(X5,X8)
| ~ of(X5,X8,V)
| ! [X7] :
( ~ forename(X5,X7)
| ~ jules_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] :
( ! [X6,X10] :
( ! [X11] :
( ~ smoke(X10,X11)
| ~ present(X10,X11)
| ~ agent(X10,X11,X6)
| ~ event(X10,X11) )
| ~ accessible_world(X5,X10)
| ! [X9] :
( ~ think_believe_consider(X5,X9)
| ~ present(X5,X9)
| ~ event(X5,X9)
| ~ theme(X5,X9,X10)
| ! [V] :
( ~ agent(X5,X9,V)
| ~ proposition(X5,X10)
| ! [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,V,X9,X10,X6,X5))
| ~ event(Y,X4) )
& man(Y,sK9_skl(Y,Z,X2,X1,V,X9,X10,X6,X5)) )
| ~ accessible_world(X5,Y)
| ! [X] :
( ~ think_believe_consider(X5,X)
| ~ present(X5,X)
| ~ event(X5,X)
| ~ theme(X5,X,Y)
| ~ agent(X5,X,V)
| ~ proposition(X5,Y)
| ! [W] :
( ~ forename(X5,W)
| ~ vincent_forename(X5,W)
| ~ man(X5,V)
| ~ of(X5,W,V)
| ! [X8] :
( ~ forename(X5,X8)
| ~ vincent_forename(X5,X8)
| ~ of(X5,X8,V)
| ! [X7] :
( ~ forename(X5,X7)
| ~ jules_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,V,X9,X10,X6,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] :
( ~ smoke(X12,X13)
| ~ present(X12,X13)
| ~ agent(X12,X13,X2)
| ~ event(X12,X13)
| ~ accessible_world(X0,X12)
| ~ think_believe_consider(X0,X11)
| ~ present(X0,X11)
| ~ event(X0,X11)
| ~ theme(X0,X11,X12)
| ~ agent(X0,X11,X4)
| ~ proposition(X0,X12)
| ~ be(X0,X9,X10,X10)
| ~ state(X0,X9)
| ~ man(X0,X10)
| ~ forename(X0,X8)
| ~ jules_forename(X0,X8)
| ~ man(X0,X10)
| ~ of(X0,X8,X10)
| man(X6,sK9_skl(X6,X8,X9,X10,X4,X11,X12,X2,X0))
| ~ accessible_world(X0,X6)
| ~ think_believe_consider(X0,X7)
| ~ present(X0,X7)
| ~ event(X0,X7)
| ~ theme(X0,X7,X6)
| ~ agent(X0,X7,X4)
| ~ proposition(X0,X6)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X4)
| ~ of(X0,X5,X4)
| ~ forename(X0,X3)
| ~ vincent_forename(X0,X3)
| ~ of(X0,X3,X4)
| ~ forename(X0,X1)
| ~ jules_forename(X0,X1)
| ~ 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,X2)
| ~ 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,X4)
| ~ 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)
| ~ smoke(X6,X8)
| ~ present(X6,X8)
| ~ agent(X6,X8,sK9_skl(X6,X9,X10,X11,X4,X12,X13,X2,X0))
| ~ event(X6,X8)
| ~ accessible_world(X0,X6)
| ~ think_believe_consider(X0,X7)
| ~ present(X0,X7)
| ~ event(X0,X7)
| ~ theme(X0,X7,X6)
| ~ agent(X0,X7,X4)
| ~ proposition(X0,X6)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X4)
| ~ of(X0,X5,X4)
| ~ forename(X0,X3)
| ~ vincent_forename(X0,X3)
| ~ of(X0,X3,X4)
| ~ forename(X0,X1)
| ~ jules_forename(X0,X1)
| ~ 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,X2)
| ~ event(X12,X13)
| ~ accessible_world(X0,X12)
| ~ think_believe_consider(X0,X11)
| ~ present(X0,X11)
| ~ event(X0,X11)
| ~ theme(X0,X11,X12)
| ~ agent(X0,X11,X4)
| ~ proposition(X0,X12)
| ~ be(X0,X9,X10,X10)
| ~ state(X0,X9)
| ~ forename(X0,X8)
| ~ jules_forename(X0,X8)
| ~ man(X0,X10)
| ~ of(X0,X8,X10)
| man(X6,sK9_skl(X6,X8,X9,X10,X4,X11,X12,X2,X0))
| ~ accessible_world(X0,X6)
| ~ think_believe_consider(X0,X7)
| ~ present(X0,X7)
| ~ event(X0,X7)
| ~ theme(X0,X7,X6)
| ~ agent(X0,X7,X4)
| ~ proposition(X0,X6)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X4)
| ~ of(X0,X5,X4)
| ~ forename(X0,X3)
| ~ vincent_forename(X0,X3)
| ~ of(X0,X3,X4)
| ~ forename(X0,X1)
| ~ jules_forename(X0,X1)
| ~ 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,X2)
| ~ 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,X4)
| ~ 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)
| ~ smoke(X6,X8)
| ~ present(X6,X8)
| ~ agent(X6,X8,sK9_skl(X6,X9,X10,X11,X4,X12,X13,X2,X0))
| ~ event(X6,X8)
| ~ accessible_world(X0,X6)
| ~ think_believe_consider(X0,X7)
| ~ present(X0,X7)
| ~ event(X0,X7)
| ~ theme(X0,X7,X6)
| ~ agent(X0,X7,X4)
| ~ proposition(X0,X6)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X4)
| ~ of(X0,X5,X4)
| ~ forename(X0,X3)
| ~ vincent_forename(X0,X3)
| ~ of(X0,X3,X4)
| ~ forename(X0,X1)
| ~ jules_forename(X0,X1)
| ~ man(X0,X2)
| ~ of(X0,X1,X2)
| ~ actual_world(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f279]) ).
fof(f321,plain,
! [X0] :
( man(sK4_skl,X0)
| ~ man(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f186,f266]) ).
fof(f383,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13] :
( ~ smoke(X12,X13)
| ~ present(X12,X13)
| ~ agent(X12,X13,X2)
| ~ event(X12,X13)
| ~ accessible_world(X0,X12)
| ~ think_believe_consider(X0,X11)
| ~ present(X0,X11)
| ~ event(X0,X11)
| ~ theme(X0,X11,X12)
| ~ agent(X0,X11,X4)
| ~ proposition(X0,X12)
| ~ be(X0,X9,X10,X10)
| ~ state(X0,X9)
| ~ forename(X0,X8)
| ~ jules_forename(X0,X8)
| ~ man(X0,X10)
| ~ of(X0,X8,X10)
| man(X6,sK9_skl(X6,X8,X9,X10,X4,X11,X12,X2,X0))
| ~ accessible_world(X0,X6)
| ~ think_believe_consider(X0,X7)
| ~ present(X0,X7)
| ~ event(X0,X7)
| ~ theme(X0,X7,X6)
| ~ agent(X0,X7,X4)
| ~ proposition(X0,X6)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X4)
| ~ of(X0,X5,X4)
| ~ vincent_forename(X0,X3)
| ~ of(X0,X3,X4)
| ~ forename(X0,X1)
| ~ jules_forename(X0,X1)
| ~ man(X0,X2)
| ~ of(X0,X1,X2)
| ~ actual_world(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f280,f77]) ).
fof(f384,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( ~ smoke(X9,X10)
| ~ present(X9,X10)
| ~ agent(X9,X10,sK1_skl)
| ~ event(X9,X10)
| ~ accessible_world(sK0_skl,X9)
| ~ think_believe_consider(sK0_skl,X8)
| ~ present(sK0_skl,X8)
| ~ event(sK0_skl,X8)
| ~ theme(sK0_skl,X8,X9)
| ~ agent(sK0_skl,X8,X1)
| ~ proposition(sK0_skl,X9)
| ~ be(sK0_skl,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)
| man(X3,sK9_skl(X3,X5,X6,X7,X1,X8,X9,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X3)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X3)
| ~ agent(sK0_skl,X4,X1)
| ~ proposition(sK0_skl,X3)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X2,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl) ),
inference(resolution,[status(thm)],[f383,f271]) ).
fof(f386,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( ~ smoke(X9,X10)
| ~ present(X9,X10)
| ~ agent(X9,X10,sK1_skl)
| ~ event(X9,X10)
| ~ accessible_world(sK0_skl,X9)
| ~ think_believe_consider(sK0_skl,X8)
| ~ present(sK0_skl,X8)
| ~ event(sK0_skl,X8)
| ~ theme(sK0_skl,X8,X9)
| ~ agent(sK0_skl,X8,X1)
| ~ proposition(sK0_skl,X9)
| ~ be(sK0_skl,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)
| man(X3,sK9_skl(X3,X5,X6,X7,X1,X8,X9,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X3)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X3)
| ~ agent(sK0_skl,X4,X1)
| ~ proposition(sK0_skl,X3)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X2,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f384,f255]) ).
fof(f404,plain,
man(sK4_skl,sK1_skl),
inference(resolution,[status(thm)],[f321,f272]) ).
fof(f406,plain,
smoke(sK4_skl,sK8_skl(sK1_skl)),
inference(resolution,[status(thm)],[f404,f270]) ).
fof(f407,plain,
present(sK4_skl,sK8_skl(sK1_skl)),
inference(resolution,[status(thm)],[f404,f269]) ).
fof(f408,plain,
agent(sK4_skl,sK8_skl(sK1_skl),sK1_skl),
inference(resolution,[status(thm)],[f404,f268]) ).
fof(f430,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14] :
( ~ smoke(X13,X14)
| ~ present(X13,X14)
| ~ agent(X13,X14,X2)
| ~ 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,X4)
| ~ 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)
| ~ smoke(X6,X8)
| ~ present(X6,X8)
| ~ agent(X6,X8,sK9_skl(X6,X9,X10,X11,X4,X12,X13,X2,X0))
| ~ event(X6,X8)
| ~ accessible_world(X0,X6)
| ~ think_believe_consider(X0,X7)
| ~ present(X0,X7)
| ~ event(X0,X7)
| ~ theme(X0,X7,X6)
| ~ agent(X0,X7,X4)
| ~ proposition(X0,X6)
| ~ forename(X0,X5)
| ~ vincent_forename(X0,X5)
| ~ man(X0,X4)
| ~ of(X0,X5,X4)
| ~ vincent_forename(X0,X3)
| ~ of(X0,X3,X4)
| ~ forename(X0,X1)
| ~ jules_forename(X0,X1)
| ~ man(X0,X2)
| ~ of(X0,X1,X2)
| ~ actual_world(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f281,f77]) ).
fof(f431,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ~ smoke(X10,X11)
| ~ present(X10,X11)
| ~ agent(X10,X11,sK1_skl)
| ~ 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,X1)
| ~ 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)
| ~ smoke(X3,X5)
| ~ present(X3,X5)
| ~ agent(X3,X5,sK9_skl(X3,X6,X7,X8,X1,X9,X10,sK1_skl,sK0_skl))
| ~ event(X3,X5)
| ~ accessible_world(sK0_skl,X3)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X3)
| ~ agent(sK0_skl,X4,X1)
| ~ proposition(sK0_skl,X3)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X2,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl) ),
inference(resolution,[status(thm)],[f430,f271]) ).
fof(f433,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ~ smoke(X10,X11)
| ~ present(X10,X11)
| ~ agent(X10,X11,sK1_skl)
| ~ 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,X1)
| ~ 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)
| ~ smoke(X3,X5)
| ~ present(X3,X5)
| ~ agent(X3,X5,sK9_skl(X3,X6,X7,X8,X1,X9,X10,sK1_skl,sK0_skl))
| ~ event(X3,X5)
| ~ accessible_world(sK0_skl,X3)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X3)
| ~ agent(sK0_skl,X4,X1)
| ~ proposition(sK0_skl,X3)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X2,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl)
| ~ man(sK0_skl,sK1_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f431,f255]) ).
fof(f529,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( ~ smoke(X9,X10)
| ~ present(X9,X10)
| ~ agent(X9,X10,sK1_skl)
| ~ event(X9,X10)
| ~ accessible_world(sK0_skl,X9)
| ~ think_believe_consider(sK0_skl,X8)
| ~ present(sK0_skl,X8)
| ~ event(sK0_skl,X8)
| ~ theme(sK0_skl,X8,X9)
| ~ agent(sK0_skl,X8,X1)
| ~ proposition(sK0_skl,X9)
| ~ be(sK0_skl,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)
| man(X3,sK9_skl(X3,X5,X6,X7,X1,X8,X9,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X3)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X3)
| ~ agent(sK0_skl,X4,X1)
| ~ proposition(sK0_skl,X3)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X2,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f386,f272]) ).
fof(f531,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)
| man(X1,sK9_skl(X1,X3,X4,X5,sK6_skl,X6,X7,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X1)
| ~ think_believe_consider(sK0_skl,X2)
| ~ present(sK0_skl,X2)
| ~ event(sK0_skl,X2)
| ~ theme(sK0_skl,X2,X1)
| ~ agent(sK0_skl,X2,sK6_skl)
| ~ proposition(sK0_skl,X1)
| ~ forename(sK0_skl,X0)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl)
| ~ of(sK0_skl,X0,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f529,f256]) ).
fof(f533,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)
| man(X1,sK9_skl(X1,X3,X4,X5,sK6_skl,X6,X7,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X1)
| ~ think_believe_consider(sK0_skl,X2)
| ~ present(sK0_skl,X2)
| ~ event(sK0_skl,X2)
| ~ theme(sK0_skl,X2,X1)
| ~ agent(sK0_skl,X2,sK6_skl)
| ~ proposition(sK0_skl,X1)
| ~ forename(sK0_skl,X0)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl)
| ~ of(sK0_skl,X0,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f531,f273]) ).
fof(f575,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ~ smoke(X10,X11)
| ~ present(X10,X11)
| ~ agent(X10,X11,sK1_skl)
| ~ 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,X1)
| ~ 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)
| ~ smoke(X3,X5)
| ~ present(X3,X5)
| ~ agent(X3,X5,sK9_skl(X3,X6,X7,X8,X1,X9,X10,sK1_skl,sK0_skl))
| ~ event(X3,X5)
| ~ accessible_world(sK0_skl,X3)
| ~ think_believe_consider(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ event(sK0_skl,X4)
| ~ theme(sK0_skl,X4,X3)
| ~ agent(sK0_skl,X4,X1)
| ~ proposition(sK0_skl,X3)
| ~ forename(sK0_skl,X2)
| ~ vincent_forename(sK0_skl,X2)
| ~ man(sK0_skl,X1)
| ~ of(sK0_skl,X2,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ of(sK0_skl,X0,X1)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f433,f272]) ).
fof(f577,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)
| ~ smoke(X1,X3)
| ~ present(X1,X3)
| ~ agent(X1,X3,sK9_skl(X1,X4,X5,X6,sK6_skl,X7,X8,sK1_skl,sK0_skl))
| ~ event(X1,X3)
| ~ accessible_world(sK0_skl,X1)
| ~ think_believe_consider(sK0_skl,X2)
| ~ present(sK0_skl,X2)
| ~ event(sK0_skl,X2)
| ~ theme(sK0_skl,X2,X1)
| ~ agent(sK0_skl,X2,sK6_skl)
| ~ proposition(sK0_skl,X1)
| ~ forename(sK0_skl,X0)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl)
| ~ of(sK0_skl,X0,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl)
| ~ jules_forename(sK0_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f575,f256]) ).
fof(f579,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)
| ~ smoke(X1,X3)
| ~ present(X1,X3)
| ~ agent(X1,X3,sK9_skl(X1,X4,X5,X6,sK6_skl,X7,X8,sK1_skl,sK0_skl))
| ~ event(X1,X3)
| ~ accessible_world(sK0_skl,X1)
| ~ think_believe_consider(sK0_skl,X2)
| ~ present(sK0_skl,X2)
| ~ event(sK0_skl,X2)
| ~ theme(sK0_skl,X2,X1)
| ~ agent(sK0_skl,X2,sK6_skl)
| ~ proposition(sK0_skl,X1)
| ~ forename(sK0_skl,X0)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl)
| ~ of(sK0_skl,X0,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f577,f273]) ).
fof(f645,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)
| man(X1,sK9_skl(X1,X3,X4,X5,sK6_skl,X6,X7,sK1_skl,sK0_skl))
| ~ accessible_world(sK0_skl,X1)
| ~ think_believe_consider(sK0_skl,X2)
| ~ present(sK0_skl,X2)
| ~ event(sK0_skl,X2)
| ~ theme(sK0_skl,X2,X1)
| ~ agent(sK0_skl,X2,sK6_skl)
| ~ proposition(sK0_skl,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl)
| ~ of(sK0_skl,X0,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f533,f77]) ).
fof(f646,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)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f645,f256]) ).
fof(f647,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)
| ~ man(sK0_skl,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f646]) ).
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)
| ~ 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)
| ~ man(sK0_skl,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f647,f75]) ).
fof(f649,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)
| 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)
| ~ man(sK0_skl,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f648,f274]) ).
fof(f650,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)
| ~ man(sK0_skl,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(resolution,[status(thm)],[f649,f261]) ).
fof(f651,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)
| ~ man(sK0_skl,sK6_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f650,f258]) ).
fof(f652,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) ),
inference(forward_subsumption_resolution,[status(thm)],[f651,f257]) ).
fof(f653,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(resolution,[status(thm)],[f652,f262]) ).
fof(f654,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) ),
inference(forward_subsumption_resolution,[status(thm)],[f653,f260]) ).
fof(f655,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ smoke(X4,X5)
| ~ present(X4,X5)
| ~ agent(X4,X5,sK1_skl)
| ~ accessible_world(sK0_skl,X4)
| ~ think_believe_consider(sK0_skl,X3)
| ~ present(sK0_skl,X3)
| ~ event(sK0_skl,X3)
| ~ theme(sK0_skl,X3,X4)
| ~ agent(sK0_skl,X3,sK6_skl)
| ~ proposition(sK0_skl,X4)
| ~ be(sK0_skl,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) ),
inference(forward_subsumption_resolution,[status(thm)],[f654,f133]) ).
fof(f656,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(resolution,[status(thm)],[f655,f271]) ).
fof(f658,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) ),
inference(forward_subsumption_resolution,[status(thm)],[f656,f263]) ).
fof(f660,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) ),
inference(forward_subsumption_resolution,[status(thm)],[f658,f264]) ).
fof(f661,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(resolution,[status(thm)],[f660,f277]) ).
fof(f662,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) ),
inference(forward_subsumption_resolution,[status(thm)],[f661,f265]) ).
fof(f663,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)) ),
inference(forward_subsumption_resolution,[status(thm)],[f662,f266]) ).
fof(f664,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)) ),
inference(resolution,[status(thm)],[f663,f261]) ).
fof(f665,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,sK1_skl,sK6_skl,sK5_skl,X0,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f664,f272]) ).
fof(f666,plain,
! [X0,X1] :
( ~ smoke(X0,X1)
| ~ present(X0,X1)
| ~ agent(X0,X1,sK1_skl)
| ~ accessible_world(sK0_skl,X0)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,X0)
| ~ proposition(sK0_skl,X0)
| ~ state(sK0_skl,sK2_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,X0,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f665,f273]) ).
fof(f667,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,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f666,f408]) ).
fof(f668,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,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f667,f276]) ).
fof(f676,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ present(sK4_skl,sK8_skl(sK1_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| ~ event(sK0_skl,sK5_skl)
| ~ theme(sK0_skl,sK5_skl,sK4_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f668,f260]) ).
fof(f677,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,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f676,f407]) ).
fof(f678,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,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f677,f262]) ).
fof(f679,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ accessible_world(sK0_skl,sK4_skl)
| ~ think_believe_consider(sK0_skl,sK5_skl)
| ~ present(sK0_skl,sK5_skl)
| man(sK4_skl,sK9_skl(sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f678,f263]) ).
fof(f680,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,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f679,f406]) ).
fof(f681,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,sK1_skl,sK6_skl,sK5_skl,sK4_skl,sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f680,f264]) ).
fof(f682,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(forward_subsumption_resolution,[status(thm)],[f681,f265]) ).
fof(f683,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(resolution,[status(thm)],[f682,f266]) ).
fof(f684,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)],[f683,f270]) ).
fof(f685,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)],[f683,f269]) ).
fof(f686,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)],[f683,f268]) ).
fof(f687,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)],[f683,f267]) ).
fof(f703,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)
| ~ smoke(X1,X3)
| ~ present(X1,X3)
| ~ agent(X1,X3,sK9_skl(X1,X4,X5,X6,sK6_skl,X7,X8,sK1_skl,sK0_skl))
| ~ event(X1,X3)
| ~ accessible_world(sK0_skl,X1)
| ~ think_believe_consider(sK0_skl,X2)
| ~ present(sK0_skl,X2)
| ~ event(sK0_skl,X2)
| ~ theme(sK0_skl,X2,X1)
| ~ agent(sK0_skl,X2,sK6_skl)
| ~ proposition(sK0_skl,X1)
| ~ vincent_forename(sK0_skl,X0)
| ~ man(sK0_skl,sK6_skl)
| ~ of(sK0_skl,X0,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f579,f77]) ).
fof(f704,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)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f703,f256]) ).
fof(f705,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)
| ~ man(sK0_skl,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f704]) ).
fof(f706,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)
| ~ 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)
| ~ man(sK0_skl,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl)
| ~ forename(sK0_skl,sK3_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f705,f75]) ).
fof(f776,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)
| ~ 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)
| ~ man(sK0_skl,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f706,f274]) ).
fof(f777,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)
| ~ man(sK0_skl,sK6_skl)
| ~ vincent_forename(sK0_skl,sK7_skl) ),
inference(resolution,[status(thm)],[f776,f261]) ).
fof(f778,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)
| ~ man(sK0_skl,sK6_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f777,f258]) ).
fof(f799,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) ),
inference(forward_subsumption_resolution,[status(thm)],[f778,f257]) ).
fof(f800,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) ),
inference(resolution,[status(thm)],[f799,f686]) ).
fof(f801,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(duplicate_literals_removal,[status(thm)],[f800]) ).
fof(f802,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) ),
inference(forward_subsumption_resolution,[status(thm)],[f801,f260]) ).
fof(f804,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) ),
inference(forward_subsumption_resolution,[status(thm)],[f802,f262]) ).
fof(f805,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(resolution,[status(thm)],[f804,f687]) ).
fof(f806,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)))
| ~ 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)],[f805,f133]) ).
fof(f807,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)))
| ~ 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) ),
inference(forward_subsumption_resolution,[status(thm)],[f806,f263]) ).
fof(f808,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(resolution,[status(thm)],[f807,f685]) ).
fof(f809,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) ),
inference(forward_subsumption_resolution,[status(thm)],[f808,f264]) ).
fof(f810,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) ),
inference(forward_subsumption_resolution,[status(thm)],[f809,f265]) ).
fof(f811,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(resolution,[status(thm)],[f810,f684]) ).
fof(f812,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) ),
inference(forward_subsumption_resolution,[status(thm)],[f811,f266]) ).
fof(f813,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) ),
inference(forward_subsumption_resolution,[status(thm)],[f812,f271]) ).
fof(f814,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(resolution,[status(thm)],[f813,f277]) ).
fof(f815,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) ),
inference(forward_subsumption_resolution,[status(thm)],[f814,f272]) ).
fof(f816,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) ),
inference(forward_subsumption_resolution,[status(thm)],[f815,f273]) ).
fof(f817,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl)
| ~ state(sK0_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f816,f261]) ).
fof(f818,plain,
! [X0] :
( ~ smoke(sK4_skl,X0)
| ~ present(sK4_skl,X0)
| ~ agent(sK4_skl,X0,sK1_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f817,f276]) ).
fof(f819,plain,
( ~ smoke(sK4_skl,sK8_skl(sK1_skl))
| ~ present(sK4_skl,sK8_skl(sK1_skl)) ),
inference(resolution,[status(thm)],[f818,f408]) ).
fof(f820,plain,
~ smoke(sK4_skl,sK8_skl(sK1_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f819,f407]) ).
fof(f821,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f820,f406]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP257+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n005.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 01:55:33 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.40 % Refutation found
% 0.12/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.45 % Elapsed time: 0.082000 seconds
% 0.12/0.45 % CPU time: 0.289317 seconds
% 0.12/0.45 % Total memory used: 50.562 MB
% 0.12/0.45 % Net memory used: 50.411 MB
%------------------------------------------------------------------------------