%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NLP251+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:07:59 AM UTC 2026
% Result : Theorem 0.15s 5.74s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 2
% Syntax : Number of formulae : 119 ( 30 unt; 0 def)
% Number of atoms : 2019 ( 0 equ)
% Maximal formula atoms : 105 ( 16 avg)
% Number of connectives : 3644 (1744 ~;1695 |; 200 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 81 ( 17 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-14 aty)
% Number of variables : 600 ( 0 sgn 76 !; 60 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax49,axiom,
! [U,V,W] :
( ( man(V,U)
& accessible_world(V,W) )
=> man(W,U) ),
file('theBenchmark.p',ax49) ).
fof(co1,conjecture,
~ ( ~ ? [X5] :
( ? [X6,X7,X8,X9,V,W,X,Y,Z,X1,X2,X10,X11] :
( ? [X12] :
( smoke(X11,X12)
& present(X11,X12)
& agent(X11,X12,X8)
& event(X11,X12) )
& accessible_world(X5,X11)
& think_believe_consider(X5,X10)
& present(X5,X10)
& event(X5,X10)
& theme(X5,X10,X11)
& agent(X5,X10,X6)
& proposition(X5,X11)
& be(X5,X2,X1,X1)
& state(X5,X2)
& man(X5,X1)
& forename(X5,Z)
& jules_forename(X5,Z)
& man(X5,X1)
& of(X5,Z,X1)
& ! [X3] :
( man(Y,X3)
=> ? [X4] :
( smoke(Y,X4)
& present(Y,X4)
& agent(Y,X4,X3)
& event(Y,X4) ) )
& accessible_world(X5,Y)
& think_believe_consider(X5,X)
& present(X5,X)
& event(X5,X)
& theme(X5,X,Y)
& agent(X5,X,V)
& proposition(X5,Y)
& forename(X5,W)
& vincent_forename(X5,W)
& man(X5,V)
& of(X5,W,V)
& forename(X5,X9)
& jules_forename(X5,X9)
& man(X5,X8)
& of(X5,X9,X8)
& forename(X5,X7)
& vincent_forename(X5,X7)
& man(X5,X6)
& of(X5,X7,X6) )
& actual_world(X5) )
& ? [U] :
( ? [V,W,X,Y,Z,X1,X2] :
( be(U,X2,X1,X1)
& state(U,X2)
& man(U,X1)
& forename(U,Z)
& jules_forename(U,Z)
& man(U,X1)
& of(U,Z,X1)
& ! [X3] :
( man(Y,X3)
=> ? [X4] :
( smoke(Y,X4)
& present(Y,X4)
& agent(Y,X4,X3)
& event(Y,X4) ) )
& accessible_world(U,Y)
& think_believe_consider(U,X)
& present(U,X)
& event(U,X)
& theme(U,X,Y)
& agent(U,X,V)
& proposition(U,Y)
& forename(U,W)
& vincent_forename(U,W)
& man(U,V)
& of(U,W,V) )
& actual_world(U) ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ~ ( ~ ? [X5] :
( ? [X6,X7,X8,X9,V,W,X,Y,Z,X1,X2,X10,X11] :
( ? [X12] :
( smoke(X11,X12)
& present(X11,X12)
& agent(X11,X12,X8)
& event(X11,X12) )
& accessible_world(X5,X11)
& think_believe_consider(X5,X10)
& present(X5,X10)
& event(X5,X10)
& theme(X5,X10,X11)
& agent(X5,X10,X6)
& proposition(X5,X11)
& be(X5,X2,X1,X1)
& state(X5,X2)
& man(X5,X1)
& forename(X5,Z)
& jules_forename(X5,Z)
& man(X5,X1)
& of(X5,Z,X1)
& ! [X3] :
( man(Y,X3)
=> ? [X4] :
( smoke(Y,X4)
& present(Y,X4)
& agent(Y,X4,X3)
& event(Y,X4) ) )
& accessible_world(X5,Y)
& think_believe_consider(X5,X)
& present(X5,X)
& event(X5,X)
& theme(X5,X,Y)
& agent(X5,X,V)
& proposition(X5,Y)
& forename(X5,W)
& vincent_forename(X5,W)
& man(X5,V)
& of(X5,W,V)
& forename(X5,X9)
& jules_forename(X5,X9)
& man(X5,X8)
& of(X5,X9,X8)
& forename(X5,X7)
& vincent_forename(X5,X7)
& man(X5,X6)
& of(X5,X7,X6) )
& actual_world(X5) )
& ? [U] :
( ? [V,W,X,Y,Z,X1,X2] :
( be(U,X2,X1,X1)
& state(U,X2)
& man(U,X1)
& forename(U,Z)
& jules_forename(U,Z)
& man(U,X1)
& of(U,Z,X1)
& ! [X3] :
( man(Y,X3)
=> ? [X4] :
( smoke(Y,X4)
& present(Y,X4)
& agent(Y,X4,X3)
& event(Y,X4) ) )
& accessible_world(U,Y)
& think_believe_consider(U,X)
& present(U,X)
& event(U,X)
& theme(U,X,Y)
& agent(U,X,V)
& proposition(U,Y)
& forename(U,W)
& vincent_forename(U,W)
& man(U,V)
& of(U,W,V) )
& actual_world(U) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
fof(nnf_72,plain,
( ! [X5] :
( ! [X6,X7,X8,X9,V,W,X,Y,Z,X1,X2,X10,X11] :
( ! [X12] :
( ~ smoke(X11,X12)
| ~ present(X11,X12)
| ~ agent(X11,X12,X8)
| ~ event(X11,X12) )
| ~ accessible_world(X5,X11)
| ~ think_believe_consider(X5,X10)
| ~ present(X5,X10)
| ~ event(X5,X10)
| ~ theme(X5,X10,X11)
| ~ agent(X5,X10,X6)
| ~ proposition(X5,X11)
| ~ be(X5,X2,X1,X1)
| ~ state(X5,X2)
| ~ man(X5,X1)
| ~ forename(X5,Z)
| ~ jules_forename(X5,Z)
| ~ man(X5,X1)
| ~ of(X5,Z,X1)
| ? [X3] :
( ! [X4] :
( ~ smoke(Y,X4)
| ~ present(Y,X4)
| ~ agent(Y,X4,X3)
| ~ event(Y,X4) )
& man(Y,X3) )
| ~ accessible_world(X5,Y)
| ~ think_believe_consider(X5,X)
| ~ present(X5,X)
| ~ event(X5,X)
| ~ theme(X5,X,Y)
| ~ agent(X5,X,V)
| ~ proposition(X5,Y)
| ~ forename(X5,W)
| ~ vincent_forename(X5,W)
| ~ man(X5,V)
| ~ of(X5,W,V)
| ~ forename(X5,X9)
| ~ jules_forename(X5,X9)
| ~ man(X5,X8)
| ~ of(X5,X9,X8)
| ~ forename(X5,X7)
| ~ vincent_forename(X5,X7)
| ~ man(X5,X6)
| ~ of(X5,X7,X6) )
| ~ actual_world(X5) )
& ? [U] :
( ? [X0,X13,X14,X15,X16,X17,X18] :
( be(U,X18,X17,X17)
& state(U,X18)
& man(U,X17)
& forename(U,X16)
& jules_forename(U,X16)
& man(U,X17)
& of(U,X16,X17)
& ! [X19] :
( ? [X20] :
( smoke(X15,X20)
& present(X15,X20)
& agent(X15,X20,X19)
& event(X15,X20) )
| ~ man(X15,X19) )
& accessible_world(U,X15)
& think_believe_consider(U,X14)
& present(U,X14)
& event(U,X14)
& theme(U,X14,X15)
& agent(U,X14,X0)
& proposition(U,X15)
& forename(U,X13)
& vincent_forename(U,X13)
& man(U,X0)
& of(U,X13,X0) )
& actual_world(U) ) ),
inference(fof_nnf,[status(thm)],[co1_neg]) ).
fof(sk_co1_neg_sk,plain,
( ! [X5] :
( ! [X6,X7,X8,X9,V,W,X,Y,Z,X1,X2,X10,X11] :
( ! [X12] :
( ~ smoke(X11,X12)
| ~ present(X11,X12)
| ~ agent(X11,X12,X8)
| ~ event(X11,X12) )
| ~ accessible_world(X5,X11)
| ~ think_believe_consider(X5,X10)
| ~ present(X5,X10)
| ~ event(X5,X10)
| ~ theme(X5,X10,X11)
| ~ agent(X5,X10,X6)
| ~ proposition(X5,X11)
| ~ be(X5,X2,X1,X1)
| ~ state(X5,X2)
| ~ man(X5,X1)
| ~ forename(X5,Z)
| ~ jules_forename(X5,Z)
| ~ man(X5,X1)
| ~ of(X5,Z,X1)
| ( ! [X4] :
( ~ smoke(Y,X4)
| ~ present(Y,X4)
| ~ agent(Y,X4,sK0(X5,X6,X7,X8,X9,V,W,X,Y,Z,X1,X2,X10,X11))
| ~ event(Y,X4) )
& man(Y,sK0(X5,X6,X7,X8,X9,V,W,X,Y,Z,X1,X2,X10,X11)) )
| ~ accessible_world(X5,Y)
| ~ think_believe_consider(X5,X)
| ~ present(X5,X)
| ~ event(X5,X)
| ~ theme(X5,X,Y)
| ~ agent(X5,X,V)
| ~ proposition(X5,Y)
| ~ forename(X5,W)
| ~ vincent_forename(X5,W)
| ~ man(X5,V)
| ~ of(X5,W,V)
| ~ forename(X5,X9)
| ~ jules_forename(X5,X9)
| ~ man(X5,X8)
| ~ of(X5,X9,X8)
| ~ forename(X5,X7)
| ~ vincent_forename(X5,X7)
| ~ man(X5,X6)
| ~ of(X5,X7,X6) )
| ~ actual_world(X5) )
& be(sK1,sK2,sK3,sK3)
& state(sK1,sK2)
& man(sK1,sK3)
& forename(sK1,sK4)
& jules_forename(sK1,sK4)
& man(sK1,sK3)
& of(sK1,sK4,sK3)
& ! [X19] :
( ( smoke(sK5,sK6(X19))
& present(sK5,sK6(X19))
& agent(sK5,sK6(X19),X19)
& event(sK5,sK6(X19)) )
| ~ man(sK5,X19) )
& accessible_world(sK1,sK5)
& think_believe_consider(sK1,sK7)
& present(sK1,sK7)
& event(sK1,sK7)
& theme(sK1,sK7,sK5)
& agent(sK1,sK7,sK8)
& proposition(sK1,sK5)
& forename(sK1,sK9)
& vincent_forename(sK1,sK9)
& man(sK1,sK8)
& of(sK1,sK9,sK8)
& actual_world(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK9,sK8,sK5,sK7,sK6,sK4,sK3,sK2,sK0]),skolemize(U,sK1),skolemize(X0,sK8),skolemize(X13,sK9),skolemize(X14,sK7),skolemize(X15,sK5),skolemize(X16,sK4),skolemize(X17,sK3),skolemize(X18,sK2),skolemize(X20,sK6(X19)),skolemize(X3,sK0(X5,X6,X7,X8,X9,V,W,X,Y,Z,X1,X2,X10,X11))],[nnf_72]) ).
fof(sk_co1_neg,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_8,VAR_9,VAR_10,VAR_11,VAR_12,VAR_13,VAR_14,VAR_15] :
( ~ smoke(VAR_14,VAR_15)
| ~ present(VAR_14,VAR_15)
| ~ agent(VAR_14,VAR_15,VAR_4)
| ~ event(VAR_14,VAR_15)
| ~ accessible_world(VAR_0,VAR_14)
| ~ think_believe_consider(VAR_0,VAR_13)
| ~ present(VAR_0,VAR_13)
| ~ event(VAR_0,VAR_13)
| ~ theme(VAR_0,VAR_13,VAR_14)
| ~ agent(VAR_0,VAR_13,VAR_2)
| ~ proposition(VAR_0,VAR_14)
| ~ be(VAR_0,VAR_12,VAR_11,VAR_11)
| ~ state(VAR_0,VAR_12)
| ~ forename(VAR_0,VAR_10)
| ~ jules_forename(VAR_0,VAR_10)
| ~ man(VAR_0,VAR_11)
| ~ of(VAR_0,VAR_10,VAR_11)
| ~ smoke(VAR_7,VAR_9)
| ~ present(VAR_7,VAR_9)
| ~ agent(VAR_7,VAR_9,sK0(VAR_0,VAR_2,VAR_1,VAR_4,VAR_3,VAR_6,VAR_5,VAR_8,VAR_7,VAR_10,VAR_11,VAR_12,VAR_13,VAR_14))
| ~ event(VAR_7,VAR_9)
| ~ accessible_world(VAR_0,VAR_7)
| ~ think_believe_consider(VAR_0,VAR_8)
| ~ present(VAR_0,VAR_8)
| ~ event(VAR_0,VAR_8)
| ~ theme(VAR_0,VAR_8,VAR_7)
| ~ agent(VAR_0,VAR_8,VAR_6)
| ~ proposition(VAR_0,VAR_7)
| ~ forename(VAR_0,VAR_5)
| ~ vincent_forename(VAR_0,VAR_5)
| ~ man(VAR_0,VAR_6)
| ~ of(VAR_0,VAR_5,VAR_6)
| ~ forename(VAR_0,VAR_3)
| ~ jules_forename(VAR_0,VAR_3)
| ~ man(VAR_0,VAR_4)
| ~ of(VAR_0,VAR_3,VAR_4)
| ~ forename(VAR_0,VAR_1)
| ~ vincent_forename(VAR_0,VAR_1)
| ~ man(VAR_0,VAR_2)
| ~ of(VAR_0,VAR_1,VAR_2)
| ~ actual_world(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_8,VAR_9,VAR_10,VAR_11,VAR_12,VAR_13,VAR_14] :
( ~ smoke(VAR_13,VAR_14)
| ~ present(VAR_13,VAR_14)
| ~ agent(VAR_13,VAR_14,VAR_4)
| ~ event(VAR_13,VAR_14)
| ~ accessible_world(VAR_0,VAR_13)
| ~ think_believe_consider(VAR_0,VAR_12)
| ~ present(VAR_0,VAR_12)
| ~ event(VAR_0,VAR_12)
| ~ theme(VAR_0,VAR_12,VAR_13)
| ~ agent(VAR_0,VAR_12,VAR_2)
| ~ proposition(VAR_0,VAR_13)
| ~ be(VAR_0,VAR_11,VAR_10,VAR_10)
| ~ state(VAR_0,VAR_11)
| ~ forename(VAR_0,VAR_9)
| ~ jules_forename(VAR_0,VAR_9)
| ~ man(VAR_0,VAR_10)
| ~ of(VAR_0,VAR_9,VAR_10)
| man(VAR_7,sK0(VAR_0,VAR_2,VAR_1,VAR_4,VAR_3,VAR_6,VAR_5,VAR_8,VAR_7,VAR_9,VAR_10,VAR_11,VAR_12,VAR_13))
| ~ accessible_world(VAR_0,VAR_7)
| ~ think_believe_consider(VAR_0,VAR_8)
| ~ present(VAR_0,VAR_8)
| ~ event(VAR_0,VAR_8)
| ~ theme(VAR_0,VAR_8,VAR_7)
| ~ agent(VAR_0,VAR_8,VAR_6)
| ~ proposition(VAR_0,VAR_7)
| ~ forename(VAR_0,VAR_5)
| ~ vincent_forename(VAR_0,VAR_5)
| ~ man(VAR_0,VAR_6)
| ~ of(VAR_0,VAR_5,VAR_6)
| ~ forename(VAR_0,VAR_3)
| ~ jules_forename(VAR_0,VAR_3)
| ~ man(VAR_0,VAR_4)
| ~ of(VAR_0,VAR_3,VAR_4)
| ~ forename(VAR_0,VAR_1)
| ~ vincent_forename(VAR_0,VAR_1)
| ~ man(VAR_0,VAR_2)
| ~ of(VAR_0,VAR_1,VAR_2)
| ~ actual_world(VAR_0) )
& be(sK1,sK2,sK3,sK3)
& state(sK1,sK2)
& forename(sK1,sK4)
& jules_forename(sK1,sK4)
& man(sK1,sK3)
& of(sK1,sK4,sK3)
& ! [VAR_0] :
( smoke(sK5,sK6(VAR_0))
| ~ man(sK5,VAR_0) )
& ! [VAR_0] :
( present(sK5,sK6(VAR_0))
| ~ man(sK5,VAR_0) )
& ! [VAR_0] :
( agent(sK5,sK6(VAR_0),VAR_0)
| ~ man(sK5,VAR_0) )
& ! [VAR_0] :
( event(sK5,sK6(VAR_0))
| ~ man(sK5,VAR_0) )
& accessible_world(sK1,sK5)
& think_believe_consider(sK1,sK7)
& present(sK1,sK7)
& event(sK1,sK7)
& theme(sK1,sK7,sK5)
& agent(sK1,sK7,sK8)
& proposition(sK1,sK5)
& forename(sK1,sK9)
& vincent_forename(sK1,sK9)
& man(sK1,sK8)
& of(sK1,sK9,sK8)
& actual_world(sK1) ),
inference(cnf_transformation,[status(thm)],[sk_co1_neg_sk]) ).
cnf(c_73,negated_conjecture,
( ~ smoke(V13,V14)
| ~ present(V13,V14)
| ~ agent(V13,V14,E)
| ~ event(V13,V14)
| ~ accessible_world(A,V13)
| ~ think_believe_consider(A,V12)
| ~ present(A,V12)
| ~ event(A,V12)
| ~ theme(A,V12,V13)
| ~ agent(A,V12,C)
| ~ proposition(A,V13)
| ~ be(A,V11,V10,V10)
| ~ state(A,V11)
| ~ forename(A,V9)
| ~ jules_forename(A,V9)
| ~ man(A,V10)
| ~ of(A,V9,V10)
| man(V7,sK0(A,C,B,E,D,V6,F,V8,V7,V9,V10,V11,V12,V13))
| ~ accessible_world(A,V7)
| ~ think_believe_consider(A,V8)
| ~ present(A,V8)
| ~ event(A,V8)
| ~ theme(A,V8,V7)
| ~ agent(A,V8,V6)
| ~ proposition(A,V7)
| ~ forename(A,F)
| ~ vincent_forename(A,F)
| ~ man(A,V6)
| ~ of(A,F,V6)
| ~ forename(A,D)
| ~ jules_forename(A,D)
| ~ man(A,E)
| ~ of(A,D,E)
| ~ forename(A,B)
| ~ vincent_forename(A,B)
| ~ man(A,C)
| ~ of(A,B,C)
| ~ actual_world(A) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_74,negated_conjecture,
actual_world(sK1),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_75,negated_conjecture,
( ~ smoke(V14,V15)
| ~ present(V14,V15)
| ~ agent(V14,V15,E)
| ~ event(V14,V15)
| ~ accessible_world(A,V14)
| ~ think_believe_consider(A,V13)
| ~ present(A,V13)
| ~ event(A,V13)
| ~ theme(A,V13,V14)
| ~ agent(A,V13,C)
| ~ proposition(A,V14)
| ~ be(A,V12,V11,V11)
| ~ state(A,V12)
| ~ forename(A,V10)
| ~ jules_forename(A,V10)
| ~ man(A,V11)
| ~ of(A,V10,V11)
| ~ smoke(V7,V9)
| ~ present(V7,V9)
| ~ agent(V7,V9,sK0(A,C,B,E,D,V6,F,V8,V7,V10,V11,V12,V13,V14))
| ~ event(V7,V9)
| ~ accessible_world(A,V7)
| ~ think_believe_consider(A,V8)
| ~ present(A,V8)
| ~ event(A,V8)
| ~ theme(A,V8,V7)
| ~ agent(A,V8,V6)
| ~ proposition(A,V7)
| ~ forename(A,F)
| ~ vincent_forename(A,F)
| ~ man(A,V6)
| ~ of(A,F,V6)
| ~ forename(A,D)
| ~ jules_forename(A,D)
| ~ man(A,E)
| ~ of(A,D,E)
| ~ forename(A,B)
| ~ vincent_forename(A,B)
| ~ man(A,C)
| ~ of(A,B,C)
| ~ actual_world(A) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_76,negated_conjecture,
( ~ smoke(V13,V14)
| ~ present(V13,V14)
| ~ agent(V13,V14,D)
| ~ event(V13,V14)
| ~ accessible_world(sK1,V13)
| ~ think_believe_consider(sK1,V12)
| ~ present(sK1,V12)
| ~ event(sK1,V12)
| ~ theme(sK1,V12,V13)
| ~ agent(sK1,V12,B)
| ~ proposition(sK1,V13)
| ~ be(sK1,V11,V10,V10)
| ~ state(sK1,V11)
| ~ forename(sK1,V9)
| ~ jules_forename(sK1,V9)
| ~ man(sK1,V10)
| ~ of(sK1,V9,V10)
| ~ smoke(V6,V8)
| ~ present(V6,V8)
| ~ agent(V6,V8,sK0(sK1,B,A,D,C,F,E,V7,V6,V9,V10,V11,V12,V13))
| ~ event(V6,V8)
| ~ accessible_world(sK1,V6)
| ~ think_believe_consider(sK1,V7)
| ~ present(sK1,V7)
| ~ event(sK1,V7)
| ~ theme(sK1,V7,V6)
| ~ agent(sK1,V7,F)
| ~ proposition(sK1,V6)
| ~ forename(sK1,E)
| ~ vincent_forename(sK1,E)
| ~ man(sK1,F)
| ~ of(sK1,E,F)
| ~ forename(sK1,C)
| ~ jules_forename(sK1,C)
| ~ man(sK1,D)
| ~ of(sK1,C,D)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B) ),
inference(resolve,[status(thm)],[c_75,c_74]) ).
cnf(c_77,negated_conjecture,
( ~ smoke(V12,V13)
| ~ present(V12,V13)
| ~ agent(V12,V13,D)
| ~ event(V12,V13)
| ~ accessible_world(sK1,V12)
| ~ think_believe_consider(sK1,V11)
| ~ present(sK1,V11)
| ~ event(sK1,V11)
| ~ theme(sK1,V11,V12)
| ~ agent(sK1,V11,B)
| ~ proposition(sK1,V12)
| ~ be(sK1,V10,V9,V9)
| ~ state(sK1,V10)
| ~ forename(sK1,V8)
| ~ jules_forename(sK1,V8)
| ~ man(sK1,V9)
| ~ of(sK1,V8,V9)
| man(V6,sK0(sK1,B,A,D,C,F,E,V7,V6,V8,V9,V10,V11,V12))
| ~ accessible_world(sK1,V6)
| ~ think_believe_consider(sK1,V7)
| ~ present(sK1,V7)
| ~ event(sK1,V7)
| ~ theme(sK1,V7,V6)
| ~ agent(sK1,V7,F)
| ~ proposition(sK1,V6)
| ~ forename(sK1,E)
| ~ vincent_forename(sK1,E)
| ~ man(sK1,F)
| ~ of(sK1,E,F)
| ~ forename(sK1,C)
| ~ jules_forename(sK1,C)
| ~ man(sK1,D)
| ~ of(sK1,C,D)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B) ),
inference(resolve,[status(thm)],[c_73,c_74]) ).
cnf(c_78,negated_conjecture,
be(sK1,sK2,sK3,sK3),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_79,negated_conjecture,
state(sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_80,negated_conjecture,
forename(sK1,sK4),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_81,negated_conjecture,
jules_forename(sK1,sK4),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_82,negated_conjecture,
man(sK1,sK3),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_83,negated_conjecture,
of(sK1,sK4,sK3),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_84,negated_conjecture,
( smoke(sK5,sK6(A))
| ~ man(sK5,A) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_85,negated_conjecture,
( present(sK5,sK6(A))
| ~ man(sK5,A) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_86,negated_conjecture,
( agent(sK5,sK6(A),A)
| ~ man(sK5,A) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_87,negated_conjecture,
( event(sK5,sK6(A))
| ~ man(sK5,A) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_88,negated_conjecture,
accessible_world(sK1,sK5),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_89,negated_conjecture,
think_believe_consider(sK1,sK7),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_90,negated_conjecture,
present(sK1,sK7),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_91,negated_conjecture,
event(sK1,sK7),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_92,negated_conjecture,
theme(sK1,sK7,sK5),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_93,negated_conjecture,
agent(sK1,sK7,sK8),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_94,negated_conjecture,
proposition(sK1,sK5),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_95,negated_conjecture,
forename(sK1,sK9),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_96,negated_conjecture,
vincent_forename(sK1,sK9),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_97,negated_conjecture,
man(sK1,sK8),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_98,negated_conjecture,
of(sK1,sK9,sK8),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_121,plain,
( man(B,C)
| ~ man(A,C)
| ~ accessible_world(A,B) ),
inference(clausify,[status(thm)],[ax49]) ).
cnf(c_466,negated_conjecture,
( man(sK5,A)
| ~ man(sK1,A) ),
inference(resolve,[status(thm)],[c_121,c_88]) ).
cnf(c_179,negated_conjecture,
man(sK5,sK3),
inference(resolve,[status(thm)],[c_466,c_82]) ).
cnf(c_208,negated_conjecture,
event(sK5,sK6(sK3)),
inference(resolve,[status(thm)],[c_87,c_179]) ).
cnf(c_209,negated_conjecture,
agent(sK5,sK6(sK3),sK3),
inference(resolve,[status(thm)],[c_86,c_179]) ).
cnf(c_210,negated_conjecture,
present(sK5,sK6(sK3)),
inference(resolve,[status(thm)],[c_85,c_179]) ).
cnf(c_211,negated_conjecture,
smoke(sK5,sK6(sK3)),
inference(resolve,[status(thm)],[c_84,c_179]) ).
cnf(c_467,negated_conjecture,
( ~ smoke(V10,V11)
| ~ present(V10,V11)
| ~ agent(V10,V11,B)
| ~ event(V10,V11)
| ~ accessible_world(sK1,V10)
| ~ think_believe_consider(sK1,V9)
| ~ present(sK1,V9)
| ~ event(sK1,V9)
| ~ theme(sK1,V9,V10)
| ~ agent(sK1,V9,sK8)
| ~ proposition(sK1,V10)
| ~ be(sK1,V8,V7,V7)
| ~ state(sK1,V8)
| ~ forename(sK1,V6)
| ~ jules_forename(sK1,V6)
| ~ man(sK1,V7)
| ~ of(sK1,V6,V7)
| man(E,sK0(sK1,sK8,sK9,B,A,D,C,F,E,V6,V7,V8,V9,V10))
| ~ accessible_world(sK1,E)
| ~ think_believe_consider(sK1,F)
| ~ present(sK1,F)
| ~ event(sK1,F)
| ~ theme(sK1,F,E)
| ~ agent(sK1,F,D)
| ~ proposition(sK1,E)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ man(sK1,D)
| ~ of(sK1,C,D)
| ~ forename(sK1,A)
| ~ jules_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK9)
| ~ vincent_forename(sK1,sK9)
| ~ man(sK1,sK8) ),
inference(resolve,[status(thm)],[c_77,c_98]) ).
cnf(c_468,negated_conjecture,
( ~ smoke(V10,V11)
| ~ present(V10,V11)
| ~ agent(V10,V11,B)
| ~ event(V10,V11)
| ~ accessible_world(sK1,V10)
| ~ think_believe_consider(sK1,V9)
| ~ present(sK1,V9)
| ~ event(sK1,V9)
| ~ theme(sK1,V9,V10)
| ~ agent(sK1,V9,sK8)
| ~ proposition(sK1,V10)
| ~ be(sK1,V8,V7,V7)
| ~ state(sK1,V8)
| ~ forename(sK1,V6)
| ~ jules_forename(sK1,V6)
| ~ man(sK1,V7)
| ~ of(sK1,V6,V7)
| man(E,sK0(sK1,sK8,sK9,B,A,D,C,F,E,V6,V7,V8,V9,V10))
| ~ accessible_world(sK1,E)
| ~ think_believe_consider(sK1,F)
| ~ present(sK1,F)
| ~ event(sK1,F)
| ~ theme(sK1,F,E)
| ~ agent(sK1,F,D)
| ~ proposition(sK1,E)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ man(sK1,D)
| ~ of(sK1,C,D)
| ~ forename(sK1,A)
| ~ jules_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK9)
| ~ vincent_forename(sK1,sK9) ),
inference(resolve,[status(thm)],[c_467,c_97]) ).
cnf(c_469,negated_conjecture,
( ~ smoke(V10,V11)
| ~ present(V10,V11)
| ~ agent(V10,V11,B)
| ~ event(V10,V11)
| ~ accessible_world(sK1,V10)
| ~ think_believe_consider(sK1,V9)
| ~ present(sK1,V9)
| ~ event(sK1,V9)
| ~ theme(sK1,V9,V10)
| ~ agent(sK1,V9,sK8)
| ~ proposition(sK1,V10)
| ~ be(sK1,V8,V7,V7)
| ~ state(sK1,V8)
| ~ forename(sK1,V6)
| ~ jules_forename(sK1,V6)
| ~ man(sK1,V7)
| ~ of(sK1,V6,V7)
| man(E,sK0(sK1,sK8,sK9,B,A,D,C,F,E,V6,V7,V8,V9,V10))
| ~ accessible_world(sK1,E)
| ~ think_believe_consider(sK1,F)
| ~ present(sK1,F)
| ~ event(sK1,F)
| ~ theme(sK1,F,E)
| ~ agent(sK1,F,D)
| ~ proposition(sK1,E)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ man(sK1,D)
| ~ of(sK1,C,D)
| ~ forename(sK1,A)
| ~ jules_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK9) ),
inference(resolve,[status(thm)],[c_468,c_96]) ).
cnf(c_470,negated_conjecture,
( ~ smoke(V10,V11)
| ~ present(V10,V11)
| ~ agent(V10,V11,B)
| ~ event(V10,V11)
| ~ accessible_world(sK1,V10)
| ~ think_believe_consider(sK1,V9)
| ~ present(sK1,V9)
| ~ event(sK1,V9)
| ~ theme(sK1,V9,V10)
| ~ agent(sK1,V9,sK8)
| ~ proposition(sK1,V10)
| ~ be(sK1,V8,V7,V7)
| ~ state(sK1,V8)
| ~ forename(sK1,V6)
| ~ jules_forename(sK1,V6)
| ~ man(sK1,V7)
| ~ of(sK1,V6,V7)
| man(E,sK0(sK1,sK8,sK9,B,A,D,C,F,E,V6,V7,V8,V9,V10))
| ~ accessible_world(sK1,E)
| ~ think_believe_consider(sK1,F)
| ~ present(sK1,F)
| ~ event(sK1,F)
| ~ theme(sK1,F,E)
| ~ agent(sK1,F,D)
| ~ proposition(sK1,E)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ man(sK1,D)
| ~ of(sK1,C,D)
| ~ forename(sK1,A)
| ~ jules_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B) ),
inference(resolve,[status(thm)],[c_469,c_95]) ).
cnf(c_471,negated_conjecture,
( ~ smoke(V8,V9)
| ~ present(V8,V9)
| ~ agent(V8,V9,sK3)
| ~ event(V8,V9)
| ~ accessible_world(sK1,V8)
| ~ think_believe_consider(sK1,V7)
| ~ present(sK1,V7)
| ~ event(sK1,V7)
| ~ theme(sK1,V7,V8)
| ~ agent(sK1,V7,sK8)
| ~ proposition(sK1,V8)
| ~ be(sK1,V6,F,F)
| ~ state(sK1,V6)
| ~ forename(sK1,E)
| ~ jules_forename(sK1,E)
| ~ man(sK1,F)
| ~ of(sK1,E,F)
| man(C,sK0(sK1,sK8,sK9,sK3,sK4,B,A,D,C,E,F,V6,V7,V8))
| ~ accessible_world(sK1,C)
| ~ think_believe_consider(sK1,D)
| ~ present(sK1,D)
| ~ event(sK1,D)
| ~ theme(sK1,D,C)
| ~ agent(sK1,D,B)
| ~ proposition(sK1,C)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK4)
| ~ jules_forename(sK1,sK4)
| ~ man(sK1,sK3) ),
inference(resolve,[status(thm)],[c_470,c_83]) ).
cnf(c_472,negated_conjecture,
( ~ smoke(V8,V9)
| ~ present(V8,V9)
| ~ agent(V8,V9,sK3)
| ~ event(V8,V9)
| ~ accessible_world(sK1,V8)
| ~ think_believe_consider(sK1,V7)
| ~ present(sK1,V7)
| ~ event(sK1,V7)
| ~ theme(sK1,V7,V8)
| ~ agent(sK1,V7,sK8)
| ~ proposition(sK1,V8)
| ~ be(sK1,V6,F,F)
| ~ state(sK1,V6)
| ~ forename(sK1,E)
| ~ jules_forename(sK1,E)
| ~ man(sK1,F)
| ~ of(sK1,E,F)
| man(C,sK0(sK1,sK8,sK9,sK3,sK4,B,A,D,C,E,F,V6,V7,V8))
| ~ accessible_world(sK1,C)
| ~ think_believe_consider(sK1,D)
| ~ present(sK1,D)
| ~ event(sK1,D)
| ~ theme(sK1,D,C)
| ~ agent(sK1,D,B)
| ~ proposition(sK1,C)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK4)
| ~ jules_forename(sK1,sK4) ),
inference(resolve,[status(thm)],[c_471,c_82]) ).
cnf(c_473,negated_conjecture,
( ~ smoke(V8,V9)
| ~ present(V8,V9)
| ~ agent(V8,V9,sK3)
| ~ event(V8,V9)
| ~ accessible_world(sK1,V8)
| ~ think_believe_consider(sK1,V7)
| ~ present(sK1,V7)
| ~ event(sK1,V7)
| ~ theme(sK1,V7,V8)
| ~ agent(sK1,V7,sK8)
| ~ proposition(sK1,V8)
| ~ be(sK1,V6,F,F)
| ~ state(sK1,V6)
| ~ forename(sK1,E)
| ~ jules_forename(sK1,E)
| ~ man(sK1,F)
| ~ of(sK1,E,F)
| man(C,sK0(sK1,sK8,sK9,sK3,sK4,B,A,D,C,E,F,V6,V7,V8))
| ~ accessible_world(sK1,C)
| ~ think_believe_consider(sK1,D)
| ~ present(sK1,D)
| ~ event(sK1,D)
| ~ theme(sK1,D,C)
| ~ agent(sK1,D,B)
| ~ proposition(sK1,C)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK4) ),
inference(resolve,[status(thm)],[c_472,c_81]) ).
cnf(c_474,negated_conjecture,
( ~ smoke(V8,V9)
| ~ present(V8,V9)
| ~ agent(V8,V9,sK3)
| ~ event(V8,V9)
| ~ accessible_world(sK1,V8)
| ~ think_believe_consider(sK1,V7)
| ~ present(sK1,V7)
| ~ event(sK1,V7)
| ~ theme(sK1,V7,V8)
| ~ agent(sK1,V7,sK8)
| ~ proposition(sK1,V8)
| ~ be(sK1,V6,F,F)
| ~ state(sK1,V6)
| ~ forename(sK1,E)
| ~ jules_forename(sK1,E)
| ~ man(sK1,F)
| ~ of(sK1,E,F)
| man(C,sK0(sK1,sK8,sK9,sK3,sK4,B,A,D,C,E,F,V6,V7,V8))
| ~ accessible_world(sK1,C)
| ~ think_believe_consider(sK1,D)
| ~ present(sK1,D)
| ~ event(sK1,D)
| ~ theme(sK1,D,C)
| ~ agent(sK1,D,B)
| ~ proposition(sK1,C)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B) ),
inference(resolve,[status(thm)],[c_473,c_80]) ).
cnf(c_475,negated_conjecture,
( ~ smoke(V6,V7)
| ~ present(V6,V7)
| ~ agent(V6,V7,sK3)
| ~ event(V6,V7)
| ~ accessible_world(sK1,V6)
| ~ think_believe_consider(sK1,F)
| ~ present(sK1,F)
| ~ event(sK1,F)
| ~ theme(sK1,F,V6)
| ~ agent(sK1,F,sK8)
| ~ proposition(sK1,V6)
| ~ be(sK1,E,D,D)
| ~ state(sK1,E)
| ~ forename(sK1,C)
| ~ jules_forename(sK1,C)
| ~ man(sK1,D)
| ~ of(sK1,C,D)
| man(A,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,B,A,C,D,E,F,V6))
| ~ accessible_world(sK1,A)
| ~ think_believe_consider(sK1,B)
| ~ present(sK1,B)
| ~ event(sK1,B)
| ~ theme(sK1,B,A)
| ~ agent(sK1,B,sK8)
| ~ proposition(sK1,A)
| ~ forename(sK1,sK9)
| ~ vincent_forename(sK1,sK9)
| ~ man(sK1,sK8) ),
inference(resolve,[status(thm)],[c_474,c_98]) ).
cnf(c_476,negated_conjecture,
( ~ smoke(V6,V7)
| ~ present(V6,V7)
| ~ agent(V6,V7,sK3)
| ~ event(V6,V7)
| ~ accessible_world(sK1,V6)
| ~ think_believe_consider(sK1,F)
| ~ present(sK1,F)
| ~ event(sK1,F)
| ~ theme(sK1,F,V6)
| ~ agent(sK1,F,sK8)
| ~ proposition(sK1,V6)
| ~ be(sK1,E,D,D)
| ~ state(sK1,E)
| ~ forename(sK1,C)
| ~ jules_forename(sK1,C)
| ~ man(sK1,D)
| ~ of(sK1,C,D)
| man(A,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,B,A,C,D,E,F,V6))
| ~ accessible_world(sK1,A)
| ~ think_believe_consider(sK1,B)
| ~ present(sK1,B)
| ~ event(sK1,B)
| ~ theme(sK1,B,A)
| ~ agent(sK1,B,sK8)
| ~ proposition(sK1,A)
| ~ forename(sK1,sK9)
| ~ vincent_forename(sK1,sK9) ),
inference(resolve,[status(thm)],[c_475,c_97]) ).
cnf(c_477,negated_conjecture,
( ~ smoke(V6,V7)
| ~ present(V6,V7)
| ~ agent(V6,V7,sK3)
| ~ event(V6,V7)
| ~ accessible_world(sK1,V6)
| ~ think_believe_consider(sK1,F)
| ~ present(sK1,F)
| ~ event(sK1,F)
| ~ theme(sK1,F,V6)
| ~ agent(sK1,F,sK8)
| ~ proposition(sK1,V6)
| ~ be(sK1,E,D,D)
| ~ state(sK1,E)
| ~ forename(sK1,C)
| ~ jules_forename(sK1,C)
| ~ man(sK1,D)
| ~ of(sK1,C,D)
| man(A,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,B,A,C,D,E,F,V6))
| ~ accessible_world(sK1,A)
| ~ think_believe_consider(sK1,B)
| ~ present(sK1,B)
| ~ event(sK1,B)
| ~ theme(sK1,B,A)
| ~ agent(sK1,B,sK8)
| ~ proposition(sK1,A)
| ~ forename(sK1,sK9) ),
inference(resolve,[status(thm)],[c_476,c_96]) ).
cnf(c_478,negated_conjecture,
( ~ smoke(V6,V7)
| ~ present(V6,V7)
| ~ agent(V6,V7,sK3)
| ~ event(V6,V7)
| ~ accessible_world(sK1,V6)
| ~ think_believe_consider(sK1,F)
| ~ present(sK1,F)
| ~ event(sK1,F)
| ~ theme(sK1,F,V6)
| ~ agent(sK1,F,sK8)
| ~ proposition(sK1,V6)
| ~ be(sK1,E,D,D)
| ~ state(sK1,E)
| ~ forename(sK1,C)
| ~ jules_forename(sK1,C)
| ~ man(sK1,D)
| ~ of(sK1,C,D)
| man(A,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,B,A,C,D,E,F,V6))
| ~ accessible_world(sK1,A)
| ~ think_believe_consider(sK1,B)
| ~ present(sK1,B)
| ~ event(sK1,B)
| ~ theme(sK1,B,A)
| ~ agent(sK1,B,sK8)
| ~ proposition(sK1,A) ),
inference(resolve,[status(thm)],[c_477,c_95]) ).
cnf(c_479,negated_conjecture,
( ~ smoke(F,V6)
| ~ present(F,V6)
| ~ agent(F,V6,sK3)
| ~ event(F,V6)
| ~ accessible_world(sK1,F)
| ~ think_believe_consider(sK1,E)
| ~ present(sK1,E)
| ~ event(sK1,E)
| ~ theme(sK1,E,F)
| ~ agent(sK1,E,sK8)
| ~ proposition(sK1,F)
| ~ be(sK1,D,C,C)
| ~ state(sK1,D)
| ~ forename(sK1,B)
| ~ jules_forename(sK1,B)
| ~ man(sK1,C)
| ~ of(sK1,B,C)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,A,sK5,B,C,D,E,F))
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,A)
| ~ present(sK1,A)
| ~ event(sK1,A)
| ~ theme(sK1,A,sK5)
| ~ agent(sK1,A,sK8) ),
inference(resolve,[status(thm)],[c_478,c_94]) ).
cnf(c_480,negated_conjecture,
( ~ smoke(E,F)
| ~ present(E,F)
| ~ agent(E,F,sK3)
| ~ event(E,F)
| ~ accessible_world(sK1,E)
| ~ think_believe_consider(sK1,D)
| ~ present(sK1,D)
| ~ event(sK1,D)
| ~ theme(sK1,D,E)
| ~ agent(sK1,D,sK8)
| ~ proposition(sK1,E)
| ~ be(sK1,C,B,B)
| ~ state(sK1,C)
| ~ forename(sK1,A)
| ~ jules_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,A,B,C,D,E))
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ event(sK1,sK7)
| ~ theme(sK1,sK7,sK5) ),
inference(resolve,[status(thm)],[c_479,c_93]) ).
cnf(c_481,negated_conjecture,
( ~ smoke(E,F)
| ~ present(E,F)
| ~ agent(E,F,sK3)
| ~ event(E,F)
| ~ accessible_world(sK1,E)
| ~ think_believe_consider(sK1,D)
| ~ present(sK1,D)
| ~ event(sK1,D)
| ~ theme(sK1,D,E)
| ~ agent(sK1,D,sK8)
| ~ proposition(sK1,E)
| ~ be(sK1,C,B,B)
| ~ state(sK1,C)
| ~ forename(sK1,A)
| ~ jules_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,A,B,C,D,E))
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ event(sK1,sK7) ),
inference(resolve,[status(thm)],[c_480,c_92]) ).
cnf(c_482,negated_conjecture,
( ~ smoke(E,F)
| ~ present(E,F)
| ~ agent(E,F,sK3)
| ~ event(E,F)
| ~ accessible_world(sK1,E)
| ~ think_believe_consider(sK1,D)
| ~ present(sK1,D)
| ~ event(sK1,D)
| ~ theme(sK1,D,E)
| ~ agent(sK1,D,sK8)
| ~ proposition(sK1,E)
| ~ be(sK1,C,B,B)
| ~ state(sK1,C)
| ~ forename(sK1,A)
| ~ jules_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,A,B,C,D,E))
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7) ),
inference(resolve,[status(thm)],[c_481,c_91]) ).
cnf(c_483,negated_conjecture,
( ~ smoke(E,F)
| ~ present(E,F)
| ~ agent(E,F,sK3)
| ~ event(E,F)
| ~ accessible_world(sK1,E)
| ~ think_believe_consider(sK1,D)
| ~ present(sK1,D)
| ~ event(sK1,D)
| ~ theme(sK1,D,E)
| ~ agent(sK1,D,sK8)
| ~ proposition(sK1,E)
| ~ be(sK1,C,B,B)
| ~ state(sK1,C)
| ~ forename(sK1,A)
| ~ jules_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,A,B,C,D,E))
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7) ),
inference(resolve,[status(thm)],[c_482,c_90]) ).
cnf(c_484,negated_conjecture,
( ~ smoke(E,F)
| ~ present(E,F)
| ~ agent(E,F,sK3)
| ~ event(E,F)
| ~ accessible_world(sK1,E)
| ~ think_believe_consider(sK1,D)
| ~ present(sK1,D)
| ~ event(sK1,D)
| ~ theme(sK1,D,E)
| ~ agent(sK1,D,sK8)
| ~ proposition(sK1,E)
| ~ be(sK1,C,B,B)
| ~ state(sK1,C)
| ~ forename(sK1,A)
| ~ jules_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,A,B,C,D,E))
| ~ accessible_world(sK1,sK5) ),
inference(resolve,[status(thm)],[c_483,c_89]) ).
cnf(c_485,negated_conjecture,
( ~ smoke(E,F)
| ~ present(E,F)
| ~ agent(E,F,sK3)
| ~ event(E,F)
| ~ accessible_world(sK1,E)
| ~ think_believe_consider(sK1,D)
| ~ present(sK1,D)
| ~ event(sK1,D)
| ~ theme(sK1,D,E)
| ~ agent(sK1,D,sK8)
| ~ proposition(sK1,E)
| ~ be(sK1,C,B,B)
| ~ state(sK1,C)
| ~ forename(sK1,A)
| ~ jules_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,A,B,C,D,E)) ),
inference(resolve,[status(thm)],[c_484,c_88]) ).
cnf(c_486,negated_conjecture,
( ~ smoke(C,D)
| ~ present(C,D)
| ~ agent(C,D,sK3)
| ~ event(C,D)
| ~ accessible_world(sK1,C)
| ~ think_believe_consider(sK1,B)
| ~ present(sK1,B)
| ~ event(sK1,B)
| ~ theme(sK1,B,C)
| ~ agent(sK1,B,sK8)
| ~ proposition(sK1,C)
| ~ be(sK1,A,sK3,sK3)
| ~ state(sK1,A)
| ~ forename(sK1,sK4)
| ~ jules_forename(sK1,sK4)
| ~ man(sK1,sK3)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,A,B,C)) ),
inference(resolve,[status(thm)],[c_485,c_83]) ).
cnf(c_487,negated_conjecture,
( ~ smoke(C,D)
| ~ present(C,D)
| ~ agent(C,D,sK3)
| ~ event(C,D)
| ~ accessible_world(sK1,C)
| ~ think_believe_consider(sK1,B)
| ~ present(sK1,B)
| ~ event(sK1,B)
| ~ theme(sK1,B,C)
| ~ agent(sK1,B,sK8)
| ~ proposition(sK1,C)
| ~ be(sK1,A,sK3,sK3)
| ~ state(sK1,A)
| ~ forename(sK1,sK4)
| ~ jules_forename(sK1,sK4)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,A,B,C)) ),
inference(resolve,[status(thm)],[c_486,c_82]) ).
cnf(c_488,negated_conjecture,
( ~ smoke(C,D)
| ~ present(C,D)
| ~ agent(C,D,sK3)
| ~ event(C,D)
| ~ accessible_world(sK1,C)
| ~ think_believe_consider(sK1,B)
| ~ present(sK1,B)
| ~ event(sK1,B)
| ~ theme(sK1,B,C)
| ~ agent(sK1,B,sK8)
| ~ proposition(sK1,C)
| ~ be(sK1,A,sK3,sK3)
| ~ state(sK1,A)
| ~ forename(sK1,sK4)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,A,B,C)) ),
inference(resolve,[status(thm)],[c_487,c_81]) ).
cnf(c_489,negated_conjecture,
( ~ smoke(C,D)
| ~ present(C,D)
| ~ agent(C,D,sK3)
| ~ event(C,D)
| ~ accessible_world(sK1,C)
| ~ think_believe_consider(sK1,B)
| ~ present(sK1,B)
| ~ event(sK1,B)
| ~ theme(sK1,B,C)
| ~ agent(sK1,B,sK8)
| ~ proposition(sK1,C)
| ~ be(sK1,A,sK3,sK3)
| ~ state(sK1,A)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,A,B,C)) ),
inference(resolve,[status(thm)],[c_488,c_80]) ).
cnf(c_490,negated_conjecture,
( ~ smoke(B,C)
| ~ present(B,C)
| ~ agent(B,C,sK3)
| ~ event(B,C)
| ~ accessible_world(sK1,B)
| ~ think_believe_consider(sK1,A)
| ~ present(sK1,A)
| ~ event(sK1,A)
| ~ theme(sK1,A,B)
| ~ agent(sK1,A,sK8)
| ~ proposition(sK1,B)
| ~ be(sK1,sK2,sK3,sK3)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,A,B)) ),
inference(resolve,[status(thm)],[c_489,c_79]) ).
cnf(c_491,negated_conjecture,
( ~ smoke(B,C)
| ~ present(B,C)
| ~ agent(B,C,sK3)
| ~ event(B,C)
| ~ accessible_world(sK1,B)
| ~ think_believe_consider(sK1,A)
| ~ present(sK1,A)
| ~ event(sK1,A)
| ~ theme(sK1,A,B)
| ~ agent(sK1,A,sK8)
| ~ proposition(sK1,B)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,A,B)) ),
inference(resolve,[status(thm)],[c_490,c_78]) ).
cnf(c_492,negated_conjecture,
( ~ smoke(sK5,B)
| ~ present(sK5,B)
| ~ agent(sK5,B,sK3)
| ~ event(sK5,B)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,A)
| ~ present(sK1,A)
| ~ event(sK1,A)
| ~ theme(sK1,A,sK5)
| ~ agent(sK1,A,sK8)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,A,sK5)) ),
inference(resolve,[status(thm)],[c_491,c_94]) ).
cnf(c_493,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ event(sK1,sK7)
| ~ theme(sK1,sK7,sK5)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_492,c_93]) ).
cnf(c_494,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ event(sK1,sK7)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_493,c_92]) ).
cnf(c_495,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_494,c_91]) ).
cnf(c_496,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_495,c_90]) ).
cnf(c_497,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_496,c_89]) ).
cnf(c_498,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_497,c_88]) ).
cnf(c_499,negated_conjecture,
( ~ smoke(sK5,sK6(sK3))
| ~ present(sK5,sK6(sK3))
| ~ agent(sK5,sK6(sK3),sK3)
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_498,c_208]) ).
cnf(c_500,negated_conjecture,
( ~ smoke(sK5,sK6(sK3))
| ~ present(sK5,sK6(sK3))
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_499,c_209]) ).
cnf(c_501,negated_conjecture,
( ~ smoke(sK5,sK6(sK3))
| man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_500,c_210]) ).
cnf(c_292,negated_conjecture,
man(sK5,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)),
inference(resolve,[status(thm)],[c_501,c_211]) ).
cnf(c_370,negated_conjecture,
event(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))),
inference(resolve,[status(thm)],[c_87,c_292]) ).
cnf(c_371,negated_conjecture,
agent(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)),sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)),
inference(resolve,[status(thm)],[c_86,c_292]) ).
cnf(c_372,negated_conjecture,
present(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))),
inference(resolve,[status(thm)],[c_85,c_292]) ).
cnf(c_373,negated_conjecture,
smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))),
inference(resolve,[status(thm)],[c_84,c_292]) ).
cnf(c_502,negated_conjecture,
( ~ smoke(V11,V12)
| ~ present(V11,V12)
| ~ agent(V11,V12,B)
| ~ event(V11,V12)
| ~ accessible_world(sK1,V11)
| ~ think_believe_consider(sK1,V10)
| ~ present(sK1,V10)
| ~ event(sK1,V10)
| ~ theme(sK1,V10,V11)
| ~ agent(sK1,V10,sK8)
| ~ proposition(sK1,V11)
| ~ be(sK1,V9,V8,V8)
| ~ state(sK1,V9)
| ~ forename(sK1,V7)
| ~ jules_forename(sK1,V7)
| ~ man(sK1,V8)
| ~ of(sK1,V7,V8)
| ~ smoke(E,V6)
| ~ present(E,V6)
| ~ agent(E,V6,sK0(sK1,sK8,sK9,B,A,D,C,F,E,V7,V8,V9,V10,V11))
| ~ event(E,V6)
| ~ accessible_world(sK1,E)
| ~ think_believe_consider(sK1,F)
| ~ present(sK1,F)
| ~ event(sK1,F)
| ~ theme(sK1,F,E)
| ~ agent(sK1,F,D)
| ~ proposition(sK1,E)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ man(sK1,D)
| ~ of(sK1,C,D)
| ~ forename(sK1,A)
| ~ jules_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK9)
| ~ vincent_forename(sK1,sK9)
| ~ man(sK1,sK8) ),
inference(resolve,[status(thm)],[c_76,c_98]) ).
cnf(c_503,negated_conjecture,
( ~ smoke(V11,V12)
| ~ present(V11,V12)
| ~ agent(V11,V12,B)
| ~ event(V11,V12)
| ~ accessible_world(sK1,V11)
| ~ think_believe_consider(sK1,V10)
| ~ present(sK1,V10)
| ~ event(sK1,V10)
| ~ theme(sK1,V10,V11)
| ~ agent(sK1,V10,sK8)
| ~ proposition(sK1,V11)
| ~ be(sK1,V9,V8,V8)
| ~ state(sK1,V9)
| ~ forename(sK1,V7)
| ~ jules_forename(sK1,V7)
| ~ man(sK1,V8)
| ~ of(sK1,V7,V8)
| ~ smoke(E,V6)
| ~ present(E,V6)
| ~ agent(E,V6,sK0(sK1,sK8,sK9,B,A,D,C,F,E,V7,V8,V9,V10,V11))
| ~ event(E,V6)
| ~ accessible_world(sK1,E)
| ~ think_believe_consider(sK1,F)
| ~ present(sK1,F)
| ~ event(sK1,F)
| ~ theme(sK1,F,E)
| ~ agent(sK1,F,D)
| ~ proposition(sK1,E)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ man(sK1,D)
| ~ of(sK1,C,D)
| ~ forename(sK1,A)
| ~ jules_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK9)
| ~ vincent_forename(sK1,sK9) ),
inference(resolve,[status(thm)],[c_502,c_97]) ).
cnf(c_504,negated_conjecture,
( ~ smoke(V11,V12)
| ~ present(V11,V12)
| ~ agent(V11,V12,B)
| ~ event(V11,V12)
| ~ accessible_world(sK1,V11)
| ~ think_believe_consider(sK1,V10)
| ~ present(sK1,V10)
| ~ event(sK1,V10)
| ~ theme(sK1,V10,V11)
| ~ agent(sK1,V10,sK8)
| ~ proposition(sK1,V11)
| ~ be(sK1,V9,V8,V8)
| ~ state(sK1,V9)
| ~ forename(sK1,V7)
| ~ jules_forename(sK1,V7)
| ~ man(sK1,V8)
| ~ of(sK1,V7,V8)
| ~ smoke(E,V6)
| ~ present(E,V6)
| ~ agent(E,V6,sK0(sK1,sK8,sK9,B,A,D,C,F,E,V7,V8,V9,V10,V11))
| ~ event(E,V6)
| ~ accessible_world(sK1,E)
| ~ think_believe_consider(sK1,F)
| ~ present(sK1,F)
| ~ event(sK1,F)
| ~ theme(sK1,F,E)
| ~ agent(sK1,F,D)
| ~ proposition(sK1,E)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ man(sK1,D)
| ~ of(sK1,C,D)
| ~ forename(sK1,A)
| ~ jules_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK9) ),
inference(resolve,[status(thm)],[c_503,c_96]) ).
cnf(c_505,negated_conjecture,
( ~ smoke(V11,V12)
| ~ present(V11,V12)
| ~ agent(V11,V12,B)
| ~ event(V11,V12)
| ~ accessible_world(sK1,V11)
| ~ think_believe_consider(sK1,V10)
| ~ present(sK1,V10)
| ~ event(sK1,V10)
| ~ theme(sK1,V10,V11)
| ~ agent(sK1,V10,sK8)
| ~ proposition(sK1,V11)
| ~ be(sK1,V9,V8,V8)
| ~ state(sK1,V9)
| ~ forename(sK1,V7)
| ~ jules_forename(sK1,V7)
| ~ man(sK1,V8)
| ~ of(sK1,V7,V8)
| ~ smoke(E,V6)
| ~ present(E,V6)
| ~ agent(E,V6,sK0(sK1,sK8,sK9,B,A,D,C,F,E,V7,V8,V9,V10,V11))
| ~ event(E,V6)
| ~ accessible_world(sK1,E)
| ~ think_believe_consider(sK1,F)
| ~ present(sK1,F)
| ~ event(sK1,F)
| ~ theme(sK1,F,E)
| ~ agent(sK1,F,D)
| ~ proposition(sK1,E)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ man(sK1,D)
| ~ of(sK1,C,D)
| ~ forename(sK1,A)
| ~ jules_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B) ),
inference(resolve,[status(thm)],[c_504,c_95]) ).
cnf(c_506,negated_conjecture,
( ~ smoke(V9,V10)
| ~ present(V9,V10)
| ~ agent(V9,V10,sK3)
| ~ event(V9,V10)
| ~ accessible_world(sK1,V9)
| ~ think_believe_consider(sK1,V8)
| ~ present(sK1,V8)
| ~ event(sK1,V8)
| ~ theme(sK1,V8,V9)
| ~ agent(sK1,V8,sK8)
| ~ proposition(sK1,V9)
| ~ be(sK1,V7,V6,V6)
| ~ state(sK1,V7)
| ~ forename(sK1,F)
| ~ jules_forename(sK1,F)
| ~ man(sK1,V6)
| ~ of(sK1,F,V6)
| ~ smoke(C,E)
| ~ present(C,E)
| ~ agent(C,E,sK0(sK1,sK8,sK9,sK3,sK4,B,A,D,C,F,V6,V7,V8,V9))
| ~ event(C,E)
| ~ accessible_world(sK1,C)
| ~ think_believe_consider(sK1,D)
| ~ present(sK1,D)
| ~ event(sK1,D)
| ~ theme(sK1,D,C)
| ~ agent(sK1,D,B)
| ~ proposition(sK1,C)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK4)
| ~ jules_forename(sK1,sK4)
| ~ man(sK1,sK3) ),
inference(resolve,[status(thm)],[c_505,c_83]) ).
cnf(c_507,negated_conjecture,
( ~ smoke(V9,V10)
| ~ present(V9,V10)
| ~ agent(V9,V10,sK3)
| ~ event(V9,V10)
| ~ accessible_world(sK1,V9)
| ~ think_believe_consider(sK1,V8)
| ~ present(sK1,V8)
| ~ event(sK1,V8)
| ~ theme(sK1,V8,V9)
| ~ agent(sK1,V8,sK8)
| ~ proposition(sK1,V9)
| ~ be(sK1,V7,V6,V6)
| ~ state(sK1,V7)
| ~ forename(sK1,F)
| ~ jules_forename(sK1,F)
| ~ man(sK1,V6)
| ~ of(sK1,F,V6)
| ~ smoke(C,E)
| ~ present(C,E)
| ~ agent(C,E,sK0(sK1,sK8,sK9,sK3,sK4,B,A,D,C,F,V6,V7,V8,V9))
| ~ event(C,E)
| ~ accessible_world(sK1,C)
| ~ think_believe_consider(sK1,D)
| ~ present(sK1,D)
| ~ event(sK1,D)
| ~ theme(sK1,D,C)
| ~ agent(sK1,D,B)
| ~ proposition(sK1,C)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK4)
| ~ jules_forename(sK1,sK4) ),
inference(resolve,[status(thm)],[c_506,c_82]) ).
cnf(c_508,negated_conjecture,
( ~ smoke(V9,V10)
| ~ present(V9,V10)
| ~ agent(V9,V10,sK3)
| ~ event(V9,V10)
| ~ accessible_world(sK1,V9)
| ~ think_believe_consider(sK1,V8)
| ~ present(sK1,V8)
| ~ event(sK1,V8)
| ~ theme(sK1,V8,V9)
| ~ agent(sK1,V8,sK8)
| ~ proposition(sK1,V9)
| ~ be(sK1,V7,V6,V6)
| ~ state(sK1,V7)
| ~ forename(sK1,F)
| ~ jules_forename(sK1,F)
| ~ man(sK1,V6)
| ~ of(sK1,F,V6)
| ~ smoke(C,E)
| ~ present(C,E)
| ~ agent(C,E,sK0(sK1,sK8,sK9,sK3,sK4,B,A,D,C,F,V6,V7,V8,V9))
| ~ event(C,E)
| ~ accessible_world(sK1,C)
| ~ think_believe_consider(sK1,D)
| ~ present(sK1,D)
| ~ event(sK1,D)
| ~ theme(sK1,D,C)
| ~ agent(sK1,D,B)
| ~ proposition(sK1,C)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK4) ),
inference(resolve,[status(thm)],[c_507,c_81]) ).
cnf(c_509,negated_conjecture,
( ~ smoke(V9,V10)
| ~ present(V9,V10)
| ~ agent(V9,V10,sK3)
| ~ event(V9,V10)
| ~ accessible_world(sK1,V9)
| ~ think_believe_consider(sK1,V8)
| ~ present(sK1,V8)
| ~ event(sK1,V8)
| ~ theme(sK1,V8,V9)
| ~ agent(sK1,V8,sK8)
| ~ proposition(sK1,V9)
| ~ be(sK1,V7,V6,V6)
| ~ state(sK1,V7)
| ~ forename(sK1,F)
| ~ jules_forename(sK1,F)
| ~ man(sK1,V6)
| ~ of(sK1,F,V6)
| ~ smoke(C,E)
| ~ present(C,E)
| ~ agent(C,E,sK0(sK1,sK8,sK9,sK3,sK4,B,A,D,C,F,V6,V7,V8,V9))
| ~ event(C,E)
| ~ accessible_world(sK1,C)
| ~ think_believe_consider(sK1,D)
| ~ present(sK1,D)
| ~ event(sK1,D)
| ~ theme(sK1,D,C)
| ~ agent(sK1,D,B)
| ~ proposition(sK1,C)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B) ),
inference(resolve,[status(thm)],[c_508,c_80]) ).
cnf(c_510,negated_conjecture,
( ~ smoke(V7,V8)
| ~ present(V7,V8)
| ~ agent(V7,V8,sK3)
| ~ event(V7,V8)
| ~ accessible_world(sK1,V7)
| ~ think_believe_consider(sK1,V6)
| ~ present(sK1,V6)
| ~ event(sK1,V6)
| ~ theme(sK1,V6,V7)
| ~ agent(sK1,V6,sK8)
| ~ proposition(sK1,V7)
| ~ be(sK1,F,E,E)
| ~ state(sK1,F)
| ~ forename(sK1,D)
| ~ jules_forename(sK1,D)
| ~ man(sK1,E)
| ~ of(sK1,D,E)
| ~ smoke(A,C)
| ~ present(A,C)
| ~ agent(A,C,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,B,A,D,E,F,V6,V7))
| ~ event(A,C)
| ~ accessible_world(sK1,A)
| ~ think_believe_consider(sK1,B)
| ~ present(sK1,B)
| ~ event(sK1,B)
| ~ theme(sK1,B,A)
| ~ agent(sK1,B,sK8)
| ~ proposition(sK1,A)
| ~ forename(sK1,sK9)
| ~ vincent_forename(sK1,sK9)
| ~ man(sK1,sK8) ),
inference(resolve,[status(thm)],[c_509,c_98]) ).
cnf(c_511,negated_conjecture,
( ~ smoke(V7,V8)
| ~ present(V7,V8)
| ~ agent(V7,V8,sK3)
| ~ event(V7,V8)
| ~ accessible_world(sK1,V7)
| ~ think_believe_consider(sK1,V6)
| ~ present(sK1,V6)
| ~ event(sK1,V6)
| ~ theme(sK1,V6,V7)
| ~ agent(sK1,V6,sK8)
| ~ proposition(sK1,V7)
| ~ be(sK1,F,E,E)
| ~ state(sK1,F)
| ~ forename(sK1,D)
| ~ jules_forename(sK1,D)
| ~ man(sK1,E)
| ~ of(sK1,D,E)
| ~ smoke(A,C)
| ~ present(A,C)
| ~ agent(A,C,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,B,A,D,E,F,V6,V7))
| ~ event(A,C)
| ~ accessible_world(sK1,A)
| ~ think_believe_consider(sK1,B)
| ~ present(sK1,B)
| ~ event(sK1,B)
| ~ theme(sK1,B,A)
| ~ agent(sK1,B,sK8)
| ~ proposition(sK1,A)
| ~ forename(sK1,sK9)
| ~ vincent_forename(sK1,sK9) ),
inference(resolve,[status(thm)],[c_510,c_97]) ).
cnf(c_512,negated_conjecture,
( ~ smoke(V7,V8)
| ~ present(V7,V8)
| ~ agent(V7,V8,sK3)
| ~ event(V7,V8)
| ~ accessible_world(sK1,V7)
| ~ think_believe_consider(sK1,V6)
| ~ present(sK1,V6)
| ~ event(sK1,V6)
| ~ theme(sK1,V6,V7)
| ~ agent(sK1,V6,sK8)
| ~ proposition(sK1,V7)
| ~ be(sK1,F,E,E)
| ~ state(sK1,F)
| ~ forename(sK1,D)
| ~ jules_forename(sK1,D)
| ~ man(sK1,E)
| ~ of(sK1,D,E)
| ~ smoke(A,C)
| ~ present(A,C)
| ~ agent(A,C,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,B,A,D,E,F,V6,V7))
| ~ event(A,C)
| ~ accessible_world(sK1,A)
| ~ think_believe_consider(sK1,B)
| ~ present(sK1,B)
| ~ event(sK1,B)
| ~ theme(sK1,B,A)
| ~ agent(sK1,B,sK8)
| ~ proposition(sK1,A)
| ~ forename(sK1,sK9) ),
inference(resolve,[status(thm)],[c_511,c_96]) ).
cnf(c_513,negated_conjecture,
( ~ smoke(V7,V8)
| ~ present(V7,V8)
| ~ agent(V7,V8,sK3)
| ~ event(V7,V8)
| ~ accessible_world(sK1,V7)
| ~ think_believe_consider(sK1,V6)
| ~ present(sK1,V6)
| ~ event(sK1,V6)
| ~ theme(sK1,V6,V7)
| ~ agent(sK1,V6,sK8)
| ~ proposition(sK1,V7)
| ~ be(sK1,F,E,E)
| ~ state(sK1,F)
| ~ forename(sK1,D)
| ~ jules_forename(sK1,D)
| ~ man(sK1,E)
| ~ of(sK1,D,E)
| ~ smoke(A,C)
| ~ present(A,C)
| ~ agent(A,C,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,B,A,D,E,F,V6,V7))
| ~ event(A,C)
| ~ accessible_world(sK1,A)
| ~ think_believe_consider(sK1,B)
| ~ present(sK1,B)
| ~ event(sK1,B)
| ~ theme(sK1,B,A)
| ~ agent(sK1,B,sK8)
| ~ proposition(sK1,A) ),
inference(resolve,[status(thm)],[c_512,c_95]) ).
cnf(c_514,negated_conjecture,
( ~ smoke(V6,V7)
| ~ present(V6,V7)
| ~ agent(V6,V7,sK3)
| ~ event(V6,V7)
| ~ accessible_world(sK1,V6)
| ~ think_believe_consider(sK1,F)
| ~ present(sK1,F)
| ~ event(sK1,F)
| ~ theme(sK1,F,V6)
| ~ agent(sK1,F,sK8)
| ~ proposition(sK1,V6)
| ~ be(sK1,E,D,D)
| ~ state(sK1,E)
| ~ forename(sK1,C)
| ~ jules_forename(sK1,C)
| ~ man(sK1,D)
| ~ of(sK1,C,D)
| ~ smoke(sK5,B)
| ~ present(sK5,B)
| ~ agent(sK5,B,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,A,sK5,C,D,E,F,V6))
| ~ event(sK5,B)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,A)
| ~ present(sK1,A)
| ~ event(sK1,A)
| ~ theme(sK1,A,sK5)
| ~ agent(sK1,A,sK8) ),
inference(resolve,[status(thm)],[c_513,c_94]) ).
cnf(c_515,negated_conjecture,
( ~ smoke(F,V6)
| ~ present(F,V6)
| ~ agent(F,V6,sK3)
| ~ event(F,V6)
| ~ accessible_world(sK1,F)
| ~ think_believe_consider(sK1,E)
| ~ present(sK1,E)
| ~ event(sK1,E)
| ~ theme(sK1,E,F)
| ~ agent(sK1,E,sK8)
| ~ proposition(sK1,F)
| ~ be(sK1,D,C,C)
| ~ state(sK1,D)
| ~ forename(sK1,B)
| ~ jules_forename(sK1,B)
| ~ man(sK1,C)
| ~ of(sK1,B,C)
| ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,B,C,D,E,F))
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ event(sK1,sK7)
| ~ theme(sK1,sK7,sK5) ),
inference(resolve,[status(thm)],[c_514,c_93]) ).
cnf(c_516,negated_conjecture,
( ~ smoke(F,V6)
| ~ present(F,V6)
| ~ agent(F,V6,sK3)
| ~ event(F,V6)
| ~ accessible_world(sK1,F)
| ~ think_believe_consider(sK1,E)
| ~ present(sK1,E)
| ~ event(sK1,E)
| ~ theme(sK1,E,F)
| ~ agent(sK1,E,sK8)
| ~ proposition(sK1,F)
| ~ be(sK1,D,C,C)
| ~ state(sK1,D)
| ~ forename(sK1,B)
| ~ jules_forename(sK1,B)
| ~ man(sK1,C)
| ~ of(sK1,B,C)
| ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,B,C,D,E,F))
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ event(sK1,sK7) ),
inference(resolve,[status(thm)],[c_515,c_92]) ).
cnf(c_517,negated_conjecture,
( ~ smoke(F,V6)
| ~ present(F,V6)
| ~ agent(F,V6,sK3)
| ~ event(F,V6)
| ~ accessible_world(sK1,F)
| ~ think_believe_consider(sK1,E)
| ~ present(sK1,E)
| ~ event(sK1,E)
| ~ theme(sK1,E,F)
| ~ agent(sK1,E,sK8)
| ~ proposition(sK1,F)
| ~ be(sK1,D,C,C)
| ~ state(sK1,D)
| ~ forename(sK1,B)
| ~ jules_forename(sK1,B)
| ~ man(sK1,C)
| ~ of(sK1,B,C)
| ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,B,C,D,E,F))
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7) ),
inference(resolve,[status(thm)],[c_516,c_91]) ).
cnf(c_518,negated_conjecture,
( ~ smoke(F,V6)
| ~ present(F,V6)
| ~ agent(F,V6,sK3)
| ~ event(F,V6)
| ~ accessible_world(sK1,F)
| ~ think_believe_consider(sK1,E)
| ~ present(sK1,E)
| ~ event(sK1,E)
| ~ theme(sK1,E,F)
| ~ agent(sK1,E,sK8)
| ~ proposition(sK1,F)
| ~ be(sK1,D,C,C)
| ~ state(sK1,D)
| ~ forename(sK1,B)
| ~ jules_forename(sK1,B)
| ~ man(sK1,C)
| ~ of(sK1,B,C)
| ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,B,C,D,E,F))
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7) ),
inference(resolve,[status(thm)],[c_517,c_90]) ).
cnf(c_519,negated_conjecture,
( ~ smoke(F,V6)
| ~ present(F,V6)
| ~ agent(F,V6,sK3)
| ~ event(F,V6)
| ~ accessible_world(sK1,F)
| ~ think_believe_consider(sK1,E)
| ~ present(sK1,E)
| ~ event(sK1,E)
| ~ theme(sK1,E,F)
| ~ agent(sK1,E,sK8)
| ~ proposition(sK1,F)
| ~ be(sK1,D,C,C)
| ~ state(sK1,D)
| ~ forename(sK1,B)
| ~ jules_forename(sK1,B)
| ~ man(sK1,C)
| ~ of(sK1,B,C)
| ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,B,C,D,E,F))
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5) ),
inference(resolve,[status(thm)],[c_518,c_89]) ).
cnf(c_520,negated_conjecture,
( ~ smoke(F,V6)
| ~ present(F,V6)
| ~ agent(F,V6,sK3)
| ~ event(F,V6)
| ~ accessible_world(sK1,F)
| ~ think_believe_consider(sK1,E)
| ~ present(sK1,E)
| ~ event(sK1,E)
| ~ theme(sK1,E,F)
| ~ agent(sK1,E,sK8)
| ~ proposition(sK1,F)
| ~ be(sK1,D,C,C)
| ~ state(sK1,D)
| ~ forename(sK1,B)
| ~ jules_forename(sK1,B)
| ~ man(sK1,C)
| ~ of(sK1,B,C)
| ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,B,C,D,E,F))
| ~ event(sK5,A) ),
inference(resolve,[status(thm)],[c_519,c_88]) ).
cnf(c_521,negated_conjecture,
( ~ smoke(E,F)
| ~ present(E,F)
| ~ agent(E,F,sK3)
| ~ event(E,F)
| ~ accessible_world(sK1,E)
| ~ think_believe_consider(sK1,D)
| ~ present(sK1,D)
| ~ event(sK1,D)
| ~ theme(sK1,D,E)
| ~ agent(sK1,D,sK8)
| ~ proposition(sK1,E)
| ~ be(sK1,C,B,B)
| ~ state(sK1,C)
| ~ forename(sK1,A)
| ~ jules_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B)
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)))
| ~ present(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)))
| ~ agent(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)),sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,A,B,C,D,E)) ),
inference(resolve,[status(thm)],[c_520,c_370]) ).
cnf(c_522,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ event(sK1,sK7)
| ~ theme(sK1,sK7,sK5)
| ~ agent(sK1,sK7,sK8)
| ~ proposition(sK1,sK5)
| ~ be(sK1,sK2,sK3,sK3)
| ~ state(sK1,sK2)
| ~ forename(sK1,sK4)
| ~ jules_forename(sK1,sK4)
| ~ man(sK1,sK3)
| ~ of(sK1,sK4,sK3)
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)))
| ~ present(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_521,c_371]) ).
cnf(c_523,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ event(sK1,sK7)
| ~ theme(sK1,sK7,sK5)
| ~ agent(sK1,sK7,sK8)
| ~ proposition(sK1,sK5)
| ~ be(sK1,sK2,sK3,sK3)
| ~ state(sK1,sK2)
| ~ forename(sK1,sK4)
| ~ jules_forename(sK1,sK4)
| ~ man(sK1,sK3)
| ~ of(sK1,sK4,sK3)
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_522,c_372]) ).
cnf(c_524,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ event(sK1,sK7)
| ~ theme(sK1,sK7,sK5)
| ~ agent(sK1,sK7,sK8)
| ~ proposition(sK1,sK5)
| ~ be(sK1,sK2,sK3,sK3)
| ~ state(sK1,sK2)
| ~ forename(sK1,sK4)
| ~ jules_forename(sK1,sK4)
| ~ man(sK1,sK3)
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_523,c_83]) ).
cnf(c_525,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ event(sK1,sK7)
| ~ theme(sK1,sK7,sK5)
| ~ agent(sK1,sK7,sK8)
| ~ proposition(sK1,sK5)
| ~ be(sK1,sK2,sK3,sK3)
| ~ state(sK1,sK2)
| ~ forename(sK1,sK4)
| ~ jules_forename(sK1,sK4)
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_524,c_82]) ).
cnf(c_526,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ event(sK1,sK7)
| ~ theme(sK1,sK7,sK5)
| ~ agent(sK1,sK7,sK8)
| ~ proposition(sK1,sK5)
| ~ be(sK1,sK2,sK3,sK3)
| ~ state(sK1,sK2)
| ~ forename(sK1,sK4)
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_525,c_81]) ).
cnf(c_527,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ event(sK1,sK7)
| ~ theme(sK1,sK7,sK5)
| ~ agent(sK1,sK7,sK8)
| ~ proposition(sK1,sK5)
| ~ be(sK1,sK2,sK3,sK3)
| ~ state(sK1,sK2)
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_526,c_80]) ).
cnf(c_528,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ event(sK1,sK7)
| ~ theme(sK1,sK7,sK5)
| ~ agent(sK1,sK7,sK8)
| ~ proposition(sK1,sK5)
| ~ be(sK1,sK2,sK3,sK3)
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_527,c_79]) ).
cnf(c_529,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ event(sK1,sK7)
| ~ theme(sK1,sK7,sK5)
| ~ agent(sK1,sK7,sK8)
| ~ proposition(sK1,sK5)
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_528,c_78]) ).
cnf(c_530,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ event(sK1,sK7)
| ~ theme(sK1,sK7,sK5)
| ~ agent(sK1,sK7,sK8)
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_529,c_94]) ).
cnf(c_531,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ event(sK1,sK7)
| ~ theme(sK1,sK7,sK5)
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_530,c_93]) ).
cnf(c_532,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ event(sK1,sK7)
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_531,c_92]) ).
cnf(c_533,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ present(sK1,sK7)
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_532,c_91]) ).
cnf(c_534,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7)
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_533,c_90]) ).
cnf(c_535,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_534,c_89]) ).
cnf(c_536,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_535,c_88]) ).
cnf(c_537,negated_conjecture,
( ~ smoke(sK5,sK6(sK3))
| ~ present(sK5,sK6(sK3))
| ~ agent(sK5,sK6(sK3),sK3)
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_536,c_208]) ).
cnf(c_538,negated_conjecture,
( ~ smoke(sK5,sK6(sK3))
| ~ present(sK5,sK6(sK3))
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_537,c_209]) ).
cnf(c_539,negated_conjecture,
( ~ smoke(sK5,sK6(sK3))
| ~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_538,c_210]) ).
cnf(c_540,negated_conjecture,
~ smoke(sK5,sK6(sK0(sK1,sK8,sK9,sK3,sK4,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))),
inference(resolve,[status(thm)],[c_539,c_211]) ).
cnf(c_465,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_373,c_540]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP251+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/5.60 % Computer : n010.cluster.edu
% 0.12/5.60 % Model : x86_64 x86_64
% 0.12/5.60 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.60 % Memory : 8046.5625MB
% 0.12/5.60 % OS : Linux 6.8.0-71-generic
% 0.12/5.60 % CPULimit : 300
% 0.12/5.60 % WCLimit : 300
% 0.12/5.60 % DateTime : Sat Sep 26 01:46:53 UTC 2026
% 0.12/5.60 % CPUTime :
% 0.12/5.60 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/5.60 % Process 2205730 was started by sandbox2 on n010,
% 0.12/5.60 % Sat Sep 26 01:46:53 2026
% 0.12/5.60 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/5.62
% 0.12/5.62 % From the command line: assign(max_seconds, 300).
% 0.15/5.74
% 0.15/5.74 % SZS status Theorem for theBenchmark
% 0.15/5.74
% 0.15/5.74 % Proof 1 at 0.10 (+ 0.01) seconds.
% 0.15/5.74 % Length of proof is 40.
% 0.15/5.74 % Level of proof is 6.
% 0.15/5.74 % Maximum clause weight is 156.000.
% 0.15/5.74 % Given clauses 323.
% 0.15/5.74
% 0.15/5.74 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------