%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NLP257+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/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:08:01 AM UTC 2026
% Result : Theorem 0.11s 0.49s
% Output : CNFRefutation 0.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 2
% Syntax : Number of formulae : 117 ( 30 unt; 0 def)
% Number of atoms : 1934 ( 0 equ)
% Maximal formula atoms : 103 ( 16 avg)
% Number of connectives : 3479 (1662 ~;1614 |; 198 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 79 ( 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-13 aty)
% Number of variables : 555 ( 0 sgn 72 !; 58 ?)
% 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,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('theBenchmark.p',co1) ).
fof(co1_neg,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(assume_negation,[status(cth)],[co1]) ).
fof(nnf_72,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] :
( ? [X0,X12,X13,X14,X15,X16,X17] :
( be(U,X17,X16,X16)
& state(U,X17)
& man(U,X16)
& forename(U,X15)
& jules_forename(U,X15)
& man(U,X16)
& of(U,X15,X16)
& ! [X18] :
( ? [X19] :
( smoke(X14,X19)
& present(X14,X19)
& agent(X14,X19,X18)
& event(X14,X19) )
| ~ man(X14,X18) )
& accessible_world(U,X14)
& think_believe_consider(U,X13)
& present(U,X13)
& event(U,X13)
& theme(U,X13,X14)
& agent(U,X13,X0)
& proposition(U,X14)
& forename(U,X12)
& vincent_forename(U,X12)
& man(U,X0)
& of(U,X12,X0) )
& actual_world(U) ) ),
inference(fof_nnf,[status(thm)],[co1_neg]) ).
fof(sk_co1_neg_sk,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)
| ( ! [X4] :
( ~ smoke(Y,X4)
| ~ present(Y,X4)
| ~ agent(Y,X4,sK0(X5,X6,X7,X8,V,W,X,Y,Z,X1,X2,X9,X10))
| ~ event(Y,X4) )
& man(Y,sK0(X5,X6,X7,X8,V,W,X,Y,Z,X1,X2,X9,X10)) )
| ~ 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) )
& 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)
& ! [X18] :
( ( smoke(sK5,sK6(X18))
& present(sK5,sK6(X18))
& agent(sK5,sK6(X18),X18)
& event(sK5,sK6(X18)) )
| ~ man(sK5,X18) )
& 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(X12,sK9),skolemize(X13,sK7),skolemize(X14,sK5),skolemize(X15,sK4),skolemize(X16,sK3),skolemize(X17,sK2),skolemize(X19,sK6(X18)),skolemize(X3,sK0(X5,X6,X7,X8,V,W,X,Y,Z,X1,X2,X9,X10))],[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] :
( ~ smoke(VAR_13,VAR_14)
| ~ present(VAR_13,VAR_14)
| ~ agent(VAR_13,VAR_14,VAR_2)
| ~ 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_4)
| ~ 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)
| ~ smoke(VAR_6,VAR_8)
| ~ present(VAR_6,VAR_8)
| ~ agent(VAR_6,VAR_8,sK0(VAR_0,VAR_2,VAR_1,VAR_3,VAR_4,VAR_5,VAR_7,VAR_6,VAR_9,VAR_10,VAR_11,VAR_12,VAR_13))
| ~ event(VAR_6,VAR_8)
| ~ accessible_world(VAR_0,VAR_6)
| ~ think_believe_consider(VAR_0,VAR_7)
| ~ present(VAR_0,VAR_7)
| ~ event(VAR_0,VAR_7)
| ~ theme(VAR_0,VAR_7,VAR_6)
| ~ agent(VAR_0,VAR_7,VAR_4)
| ~ proposition(VAR_0,VAR_6)
| ~ forename(VAR_0,VAR_5)
| ~ vincent_forename(VAR_0,VAR_5)
| ~ man(VAR_0,VAR_4)
| ~ of(VAR_0,VAR_5,VAR_4)
| ~ forename(VAR_0,VAR_3)
| ~ vincent_forename(VAR_0,VAR_3)
| ~ of(VAR_0,VAR_3,VAR_4)
| ~ forename(VAR_0,VAR_1)
| ~ jules_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] :
( ~ smoke(VAR_12,VAR_13)
| ~ present(VAR_12,VAR_13)
| ~ agent(VAR_12,VAR_13,VAR_2)
| ~ event(VAR_12,VAR_13)
| ~ accessible_world(VAR_0,VAR_12)
| ~ think_believe_consider(VAR_0,VAR_11)
| ~ present(VAR_0,VAR_11)
| ~ event(VAR_0,VAR_11)
| ~ theme(VAR_0,VAR_11,VAR_12)
| ~ agent(VAR_0,VAR_11,VAR_4)
| ~ proposition(VAR_0,VAR_12)
| ~ be(VAR_0,VAR_10,VAR_9,VAR_9)
| ~ state(VAR_0,VAR_10)
| ~ forename(VAR_0,VAR_8)
| ~ jules_forename(VAR_0,VAR_8)
| ~ man(VAR_0,VAR_9)
| ~ of(VAR_0,VAR_8,VAR_9)
| man(VAR_6,sK0(VAR_0,VAR_2,VAR_1,VAR_3,VAR_4,VAR_5,VAR_7,VAR_6,VAR_8,VAR_9,VAR_10,VAR_11,VAR_12))
| ~ accessible_world(VAR_0,VAR_6)
| ~ think_believe_consider(VAR_0,VAR_7)
| ~ present(VAR_0,VAR_7)
| ~ event(VAR_0,VAR_7)
| ~ theme(VAR_0,VAR_7,VAR_6)
| ~ agent(VAR_0,VAR_7,VAR_4)
| ~ proposition(VAR_0,VAR_6)
| ~ forename(VAR_0,VAR_5)
| ~ vincent_forename(VAR_0,VAR_5)
| ~ man(VAR_0,VAR_4)
| ~ of(VAR_0,VAR_5,VAR_4)
| ~ forename(VAR_0,VAR_3)
| ~ vincent_forename(VAR_0,VAR_3)
| ~ of(VAR_0,VAR_3,VAR_4)
| ~ forename(VAR_0,VAR_1)
| ~ jules_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(V12,V13)
| ~ present(V12,V13)
| ~ agent(V12,V13,C)
| ~ event(V12,V13)
| ~ accessible_world(A,V12)
| ~ think_believe_consider(A,V11)
| ~ present(A,V11)
| ~ event(A,V11)
| ~ theme(A,V11,V12)
| ~ agent(A,V11,E)
| ~ proposition(A,V12)
| ~ be(A,V10,V9,V9)
| ~ state(A,V10)
| ~ forename(A,V8)
| ~ jules_forename(A,V8)
| ~ man(A,V9)
| ~ of(A,V8,V9)
| man(V6,sK0(A,C,B,D,E,F,V7,V6,V8,V9,V10,V11,V12))
| ~ accessible_world(A,V6)
| ~ think_believe_consider(A,V7)
| ~ present(A,V7)
| ~ event(A,V7)
| ~ theme(A,V7,V6)
| ~ agent(A,V7,E)
| ~ proposition(A,V6)
| ~ forename(A,F)
| ~ vincent_forename(A,F)
| ~ man(A,E)
| ~ of(A,F,E)
| ~ forename(A,D)
| ~ vincent_forename(A,D)
| ~ of(A,D,E)
| ~ forename(A,B)
| ~ jules_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(V13,V14)
| ~ present(V13,V14)
| ~ agent(V13,V14,C)
| ~ 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,E)
| ~ 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)
| ~ smoke(V6,V8)
| ~ present(V6,V8)
| ~ agent(V6,V8,sK0(A,C,B,D,E,F,V7,V6,V9,V10,V11,V12,V13))
| ~ event(V6,V8)
| ~ accessible_world(A,V6)
| ~ think_believe_consider(A,V7)
| ~ present(A,V7)
| ~ event(A,V7)
| ~ theme(A,V7,V6)
| ~ agent(A,V7,E)
| ~ proposition(A,V6)
| ~ forename(A,F)
| ~ vincent_forename(A,F)
| ~ man(A,E)
| ~ of(A,F,E)
| ~ forename(A,D)
| ~ vincent_forename(A,D)
| ~ of(A,D,E)
| ~ forename(A,B)
| ~ jules_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(V12,V13)
| ~ present(V12,V13)
| ~ agent(V12,V13,B)
| ~ 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,D)
| ~ 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)
| ~ smoke(F,V7)
| ~ present(F,V7)
| ~ agent(F,V7,sK0(sK1,B,A,C,D,E,V6,F,V8,V9,V10,V11,V12))
| ~ event(F,V7)
| ~ accessible_world(sK1,F)
| ~ think_believe_consider(sK1,V6)
| ~ present(sK1,V6)
| ~ event(sK1,V6)
| ~ theme(sK1,V6,F)
| ~ agent(sK1,V6,D)
| ~ proposition(sK1,F)
| ~ forename(sK1,E)
| ~ vincent_forename(sK1,E)
| ~ man(sK1,D)
| ~ of(sK1,E,D)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ of(sK1,C,D)
| ~ forename(sK1,A)
| ~ jules_forename(sK1,A)
| ~ man(sK1,B)
| ~ of(sK1,A,B) ),
inference(resolve,[status(thm)],[c_75,c_74]) ).
cnf(c_77,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,D)
| ~ 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)
| man(F,sK0(sK1,B,A,C,D,E,V6,F,V7,V8,V9,V10,V11))
| ~ accessible_world(sK1,F)
| ~ think_believe_consider(sK1,V6)
| ~ present(sK1,V6)
| ~ event(sK1,V6)
| ~ theme(sK1,V6,F)
| ~ agent(sK1,V6,D)
| ~ proposition(sK1,F)
| ~ forename(sK1,E)
| ~ vincent_forename(sK1,E)
| ~ man(sK1,D)
| ~ of(sK1,E,D)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ of(sK1,C,D)
| ~ forename(sK1,A)
| ~ jules_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_460,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_460,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_461,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,B)
| ~ 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)
| man(D,sK0(sK1,sK3,sK4,A,B,C,E,D,F,V6,V7,V8,V9))
| ~ accessible_world(sK1,D)
| ~ think_believe_consider(sK1,E)
| ~ present(sK1,E)
| ~ event(sK1,E)
| ~ theme(sK1,E,D)
| ~ agent(sK1,E,B)
| ~ proposition(sK1,D)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ man(sK1,B)
| ~ of(sK1,C,B)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK4)
| ~ jules_forename(sK1,sK4)
| ~ man(sK1,sK3) ),
inference(resolve,[status(thm)],[c_77,c_83]) ).
cnf(c_462,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,B)
| ~ 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)
| man(D,sK0(sK1,sK3,sK4,A,B,C,E,D,F,V6,V7,V8,V9))
| ~ accessible_world(sK1,D)
| ~ think_believe_consider(sK1,E)
| ~ present(sK1,E)
| ~ event(sK1,E)
| ~ theme(sK1,E,D)
| ~ agent(sK1,E,B)
| ~ proposition(sK1,D)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ man(sK1,B)
| ~ of(sK1,C,B)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK4)
| ~ jules_forename(sK1,sK4) ),
inference(resolve,[status(thm)],[c_461,c_82]) ).
cnf(c_463,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,B)
| ~ 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)
| man(D,sK0(sK1,sK3,sK4,A,B,C,E,D,F,V6,V7,V8,V9))
| ~ accessible_world(sK1,D)
| ~ think_believe_consider(sK1,E)
| ~ present(sK1,E)
| ~ event(sK1,E)
| ~ theme(sK1,E,D)
| ~ agent(sK1,E,B)
| ~ proposition(sK1,D)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ man(sK1,B)
| ~ of(sK1,C,B)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK4) ),
inference(resolve,[status(thm)],[c_462,c_81]) ).
cnf(c_464,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,B)
| ~ 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)
| man(D,sK0(sK1,sK3,sK4,A,B,C,E,D,F,V6,V7,V8,V9))
| ~ accessible_world(sK1,D)
| ~ think_believe_consider(sK1,E)
| ~ present(sK1,E)
| ~ event(sK1,E)
| ~ theme(sK1,E,D)
| ~ agent(sK1,E,B)
| ~ proposition(sK1,D)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ man(sK1,B)
| ~ of(sK1,C,B)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ of(sK1,A,B) ),
inference(resolve,[status(thm)],[c_463,c_80]) ).
cnf(c_465,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)
| man(B,sK0(sK1,sK3,sK4,sK9,sK8,A,C,B,D,E,F,V6,V7))
| ~ accessible_world(sK1,B)
| ~ think_believe_consider(sK1,C)
| ~ present(sK1,C)
| ~ event(sK1,C)
| ~ theme(sK1,C,B)
| ~ agent(sK1,C,sK8)
| ~ proposition(sK1,B)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ man(sK1,sK8)
| ~ of(sK1,A,sK8)
| ~ forename(sK1,sK9)
| ~ vincent_forename(sK1,sK9) ),
inference(resolve,[status(thm)],[c_464,c_98]) ).
cnf(c_466,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)
| man(B,sK0(sK1,sK3,sK4,sK9,sK8,A,C,B,D,E,F,V6,V7))
| ~ accessible_world(sK1,B)
| ~ think_believe_consider(sK1,C)
| ~ present(sK1,C)
| ~ event(sK1,C)
| ~ theme(sK1,C,B)
| ~ agent(sK1,C,sK8)
| ~ proposition(sK1,B)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ man(sK1,sK8)
| ~ of(sK1,A,sK8)
| ~ forename(sK1,sK9) ),
inference(resolve,[status(thm)],[c_465,c_96]) ).
cnf(c_467,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)
| man(B,sK0(sK1,sK3,sK4,sK9,sK8,A,C,B,D,E,F,V6,V7))
| ~ accessible_world(sK1,B)
| ~ think_believe_consider(sK1,C)
| ~ present(sK1,C)
| ~ event(sK1,C)
| ~ theme(sK1,C,B)
| ~ agent(sK1,C,sK8)
| ~ proposition(sK1,B)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ man(sK1,sK8)
| ~ of(sK1,A,sK8) ),
inference(resolve,[status(thm)],[c_466,c_95]) ).
cnf(c_468,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,sK3,sK4,sK9,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_467,c_98]) ).
cnf(c_469,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,sK3,sK4,sK9,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_468,c_97]) ).
cnf(c_470,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,sK3,sK4,sK9,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_469,c_96]) ).
cnf(c_471,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,sK3,sK4,sK9,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_470,c_95]) ).
cnf(c_472,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,sK3,sK4,sK9,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_471,c_94]) ).
cnf(c_473,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,sK3,sK4,sK9,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_472,c_93]) ).
cnf(c_474,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,sK3,sK4,sK9,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_473,c_92]) ).
cnf(c_475,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,sK3,sK4,sK9,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_474,c_91]) ).
cnf(c_476,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,A,B,C,D,E))
| ~ accessible_world(sK1,sK5)
| ~ think_believe_consider(sK1,sK7) ),
inference(resolve,[status(thm)],[c_475,c_90]) ).
cnf(c_477,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,A,B,C,D,E))
| ~ accessible_world(sK1,sK5) ),
inference(resolve,[status(thm)],[c_476,c_89]) ).
cnf(c_478,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,A,B,C,D,E)) ),
inference(resolve,[status(thm)],[c_477,c_88]) ).
cnf(c_479,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,A,B,C)) ),
inference(resolve,[status(thm)],[c_478,c_83]) ).
cnf(c_480,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,A,B,C)) ),
inference(resolve,[status(thm)],[c_479,c_82]) ).
cnf(c_481,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,A,B,C)) ),
inference(resolve,[status(thm)],[c_480,c_81]) ).
cnf(c_482,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,A,B,C)) ),
inference(resolve,[status(thm)],[c_481,c_80]) ).
cnf(c_483,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,A,B)) ),
inference(resolve,[status(thm)],[c_482,c_79]) ).
cnf(c_484,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,A,B)) ),
inference(resolve,[status(thm)],[c_483,c_78]) ).
cnf(c_485,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,A,sK5)) ),
inference(resolve,[status(thm)],[c_484,c_94]) ).
cnf(c_486,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_485,c_93]) ).
cnf(c_487,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_486,c_92]) ).
cnf(c_488,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_487,c_91]) ).
cnf(c_489,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_488,c_90]) ).
cnf(c_490,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| man(sK5,sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_489,c_89]) ).
cnf(c_491,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| man(sK5,sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_490,c_88]) ).
cnf(c_492,negated_conjecture,
( ~ smoke(sK5,sK6(sK3))
| ~ present(sK5,sK6(sK3))
| ~ agent(sK5,sK6(sK3),sK3)
| man(sK5,sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_491,c_208]) ).
cnf(c_493,negated_conjecture,
( ~ smoke(sK5,sK6(sK3))
| ~ present(sK5,sK6(sK3))
| man(sK5,sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_492,c_209]) ).
cnf(c_494,negated_conjecture,
( ~ smoke(sK5,sK6(sK3))
| man(sK5,sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_493,c_210]) ).
cnf(c_289,negated_conjecture,
man(sK5,sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)),
inference(resolve,[status(thm)],[c_494,c_211]) ).
cnf(c_352,negated_conjecture,
event(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))),
inference(resolve,[status(thm)],[c_87,c_289]) ).
cnf(c_353,negated_conjecture,
agent(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)),sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)),
inference(resolve,[status(thm)],[c_86,c_289]) ).
cnf(c_354,negated_conjecture,
present(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))),
inference(resolve,[status(thm)],[c_85,c_289]) ).
cnf(c_355,negated_conjecture,
smoke(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))),
inference(resolve,[status(thm)],[c_84,c_289]) ).
cnf(c_495,negated_conjecture,
( ~ smoke(V10,V11)
| ~ present(V10,V11)
| ~ agent(V10,V11,sK3)
| ~ 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,B)
| ~ 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)
| ~ smoke(D,F)
| ~ present(D,F)
| ~ agent(D,F,sK0(sK1,sK3,sK4,A,B,C,E,D,V6,V7,V8,V9,V10))
| ~ event(D,F)
| ~ accessible_world(sK1,D)
| ~ think_believe_consider(sK1,E)
| ~ present(sK1,E)
| ~ event(sK1,E)
| ~ theme(sK1,E,D)
| ~ agent(sK1,E,B)
| ~ proposition(sK1,D)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ man(sK1,B)
| ~ of(sK1,C,B)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK4)
| ~ jules_forename(sK1,sK4)
| ~ man(sK1,sK3) ),
inference(resolve,[status(thm)],[c_76,c_83]) ).
cnf(c_496,negated_conjecture,
( ~ smoke(V10,V11)
| ~ present(V10,V11)
| ~ agent(V10,V11,sK3)
| ~ 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,B)
| ~ 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)
| ~ smoke(D,F)
| ~ present(D,F)
| ~ agent(D,F,sK0(sK1,sK3,sK4,A,B,C,E,D,V6,V7,V8,V9,V10))
| ~ event(D,F)
| ~ accessible_world(sK1,D)
| ~ think_believe_consider(sK1,E)
| ~ present(sK1,E)
| ~ event(sK1,E)
| ~ theme(sK1,E,D)
| ~ agent(sK1,E,B)
| ~ proposition(sK1,D)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ man(sK1,B)
| ~ of(sK1,C,B)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK4)
| ~ jules_forename(sK1,sK4) ),
inference(resolve,[status(thm)],[c_495,c_82]) ).
cnf(c_497,negated_conjecture,
( ~ smoke(V10,V11)
| ~ present(V10,V11)
| ~ agent(V10,V11,sK3)
| ~ 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,B)
| ~ 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)
| ~ smoke(D,F)
| ~ present(D,F)
| ~ agent(D,F,sK0(sK1,sK3,sK4,A,B,C,E,D,V6,V7,V8,V9,V10))
| ~ event(D,F)
| ~ accessible_world(sK1,D)
| ~ think_believe_consider(sK1,E)
| ~ present(sK1,E)
| ~ event(sK1,E)
| ~ theme(sK1,E,D)
| ~ agent(sK1,E,B)
| ~ proposition(sK1,D)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ man(sK1,B)
| ~ of(sK1,C,B)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ of(sK1,A,B)
| ~ forename(sK1,sK4) ),
inference(resolve,[status(thm)],[c_496,c_81]) ).
cnf(c_498,negated_conjecture,
( ~ smoke(V10,V11)
| ~ present(V10,V11)
| ~ agent(V10,V11,sK3)
| ~ 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,B)
| ~ 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)
| ~ smoke(D,F)
| ~ present(D,F)
| ~ agent(D,F,sK0(sK1,sK3,sK4,A,B,C,E,D,V6,V7,V8,V9,V10))
| ~ event(D,F)
| ~ accessible_world(sK1,D)
| ~ think_believe_consider(sK1,E)
| ~ present(sK1,E)
| ~ event(sK1,E)
| ~ theme(sK1,E,D)
| ~ agent(sK1,E,B)
| ~ proposition(sK1,D)
| ~ forename(sK1,C)
| ~ vincent_forename(sK1,C)
| ~ man(sK1,B)
| ~ of(sK1,C,B)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ of(sK1,A,B) ),
inference(resolve,[status(thm)],[c_497,c_80]) ).
cnf(c_499,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)
| ~ smoke(B,D)
| ~ present(B,D)
| ~ agent(B,D,sK0(sK1,sK3,sK4,sK9,sK8,A,C,B,E,F,V6,V7,V8))
| ~ event(B,D)
| ~ accessible_world(sK1,B)
| ~ think_believe_consider(sK1,C)
| ~ present(sK1,C)
| ~ event(sK1,C)
| ~ theme(sK1,C,B)
| ~ agent(sK1,C,sK8)
| ~ proposition(sK1,B)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ man(sK1,sK8)
| ~ of(sK1,A,sK8)
| ~ forename(sK1,sK9)
| ~ vincent_forename(sK1,sK9) ),
inference(resolve,[status(thm)],[c_498,c_98]) ).
cnf(c_500,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)
| ~ smoke(B,D)
| ~ present(B,D)
| ~ agent(B,D,sK0(sK1,sK3,sK4,sK9,sK8,A,C,B,E,F,V6,V7,V8))
| ~ event(B,D)
| ~ accessible_world(sK1,B)
| ~ think_believe_consider(sK1,C)
| ~ present(sK1,C)
| ~ event(sK1,C)
| ~ theme(sK1,C,B)
| ~ agent(sK1,C,sK8)
| ~ proposition(sK1,B)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ man(sK1,sK8)
| ~ of(sK1,A,sK8)
| ~ forename(sK1,sK9) ),
inference(resolve,[status(thm)],[c_499,c_96]) ).
cnf(c_501,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)
| ~ smoke(B,D)
| ~ present(B,D)
| ~ agent(B,D,sK0(sK1,sK3,sK4,sK9,sK8,A,C,B,E,F,V6,V7,V8))
| ~ event(B,D)
| ~ accessible_world(sK1,B)
| ~ think_believe_consider(sK1,C)
| ~ present(sK1,C)
| ~ event(sK1,C)
| ~ theme(sK1,C,B)
| ~ agent(sK1,C,sK8)
| ~ proposition(sK1,B)
| ~ forename(sK1,A)
| ~ vincent_forename(sK1,A)
| ~ man(sK1,sK8)
| ~ of(sK1,A,sK8) ),
inference(resolve,[status(thm)],[c_500,c_95]) ).
cnf(c_502,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,sK3,sK4,sK9,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_501,c_98]) ).
cnf(c_503,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,sK3,sK4,sK9,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_502,c_97]) ).
cnf(c_504,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,sK3,sK4,sK9,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_503,c_96]) ).
cnf(c_505,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,sK3,sK4,sK9,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_504,c_95]) ).
cnf(c_506,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,sK3,sK4,sK9,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_505,c_94]) ).
cnf(c_507,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,sK3,sK4,sK9,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_506,c_93]) ).
cnf(c_508,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,sK3,sK4,sK9,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_507,c_92]) ).
cnf(c_509,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,sK3,sK4,sK9,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_508,c_91]) ).
cnf(c_510,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,sK3,sK4,sK9,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_509,c_90]) ).
cnf(c_511,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,B,C,D,E,F))
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5) ),
inference(resolve,[status(thm)],[c_510,c_89]) ).
cnf(c_512,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,B,C,D,E,F))
| ~ event(sK5,A) ),
inference(resolve,[status(thm)],[c_511,c_88]) ).
cnf(c_513,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)))
| ~ present(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)))
| ~ agent(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)),sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,A,B,C,D,E)) ),
inference(resolve,[status(thm)],[c_512,c_352]) ).
cnf(c_514,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5)))
| ~ present(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_513,c_353]) ).
cnf(c_515,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_514,c_354]) ).
cnf(c_516,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_515,c_83]) ).
cnf(c_517,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_516,c_82]) ).
cnf(c_518,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_517,c_81]) ).
cnf(c_519,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_518,c_80]) ).
cnf(c_520,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_519,c_79]) ).
cnf(c_521,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,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_520,c_78]) ).
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)
| ~ smoke(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_521,c_94]) ).
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)
| ~ smoke(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_522,c_93]) ).
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)
| ~ smoke(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_523,c_92]) ).
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)
| ~ smoke(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_524,c_91]) ).
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)
| ~ smoke(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_525,c_90]) ).
cnf(c_527,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ accessible_world(sK1,sK5)
| ~ smoke(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_526,c_89]) ).
cnf(c_528,negated_conjecture,
( ~ smoke(sK5,A)
| ~ present(sK5,A)
| ~ agent(sK5,A,sK3)
| ~ event(sK5,A)
| ~ smoke(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_527,c_88]) ).
cnf(c_529,negated_conjecture,
( ~ smoke(sK5,sK6(sK3))
| ~ present(sK5,sK6(sK3))
| ~ agent(sK5,sK6(sK3),sK3)
| ~ smoke(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_528,c_208]) ).
cnf(c_530,negated_conjecture,
( ~ smoke(sK5,sK6(sK3))
| ~ present(sK5,sK6(sK3))
| ~ smoke(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_529,c_209]) ).
cnf(c_531,negated_conjecture,
( ~ smoke(sK5,sK6(sK3))
| ~ smoke(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))) ),
inference(resolve,[status(thm)],[c_530,c_210]) ).
cnf(c_532,negated_conjecture,
~ smoke(sK5,sK6(sK0(sK1,sK3,sK4,sK9,sK8,sK9,sK7,sK5,sK4,sK3,sK2,sK7,sK5))),
inference(resolve,[status(thm)],[c_531,c_211]) ).
cnf(c_459,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_355,c_532]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP257+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n010.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 : Sat Sep 26 01:49:01 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.36 % Process 2207161 was started by sandbox on n010,
% 0.07/0.36 % Sat Sep 26 01:49:01 2026
% 0.07/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.11/0.38
% 0.11/0.38 % From the command line: assign(max_seconds, 300).
% 0.11/0.49
% 0.11/0.49 % SZS status Theorem for theBenchmark
% 0.11/0.49
% 0.11/0.49 % Proof 1 at 0.09 (+ 0.01) seconds.
% 0.11/0.49 % Length of proof is 40.
% 0.11/0.49 % Level of proof is 6.
% 0.11/0.49 % Maximum clause weight is 152.000.
% 0.11/0.49 % Given clauses 317.
% 0.11/0.49
% 0.11/0.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------