%------------------------------------------------------------------------------
% 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 : n009.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:00 AM UTC 2026
% Result : Unsatisfiable 0.15s 5.44s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 25
% Syntax : Number of formulae : 137 ( 46 unt; 0 def)
% Number of atoms : 1751 ( 0 equ)
% Maximal formula atoms : 41 ( 12 avg)
% Number of connectives : 3270 (1656 ~;1614 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 58 ( 14 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-1 aty)
% Number of variables : 634 ( 44 sgn 41 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(clause94,axiom,
! [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] :
( man(VAR_1,skf4(VAR_1))
| ~ actual_world(VAR_0)
| ~ think_believe_consider(VAR_0,VAR_13)
| ~ present(VAR_0,VAR_13)
| ~ event(VAR_0,VAR_13)
| ~ theme(VAR_0,VAR_13,VAR_8)
| ~ of(VAR_0,VAR_12,VAR_14)
| ~ man(VAR_0,VAR_14)
| ~ agent(VAR_0,VAR_13,VAR_14)
| ~ forename(VAR_0,VAR_12)
| ~ vincent_forename(VAR_0,VAR_12)
| ~ of(VAR_0,VAR_9,VAR_11)
| ~ man(VAR_0,VAR_11)
| ~ event(VAR_8,VAR_10)
| ~ agent(VAR_8,VAR_10,VAR_11)
| ~ present(VAR_8,VAR_10)
| ~ smoke(VAR_8,VAR_10)
| ~ forename(VAR_0,VAR_9)
| ~ jules_forename(VAR_0,VAR_9)
| ~ proposition(VAR_0,VAR_8)
| ~ accessible_world(VAR_0,VAR_8)
| ~ of(VAR_0,VAR_7,VAR_6)
| ~ jules_forename(VAR_0,VAR_7)
| ~ forename(VAR_0,VAR_7)
| ~ be(VAR_0,VAR_5,VAR_6,VAR_6)
| ~ man(VAR_0,VAR_6)
| ~ state(VAR_0,VAR_5)
| ~ of(VAR_0,VAR_3,VAR_4)
| ~ man(VAR_0,VAR_4)
| ~ agent(VAR_0,VAR_2,VAR_4)
| ~ forename(VAR_0,VAR_3)
| ~ vincent_forename(VAR_0,VAR_3)
| ~ theme(VAR_0,VAR_2,VAR_1)
| ~ event(VAR_0,VAR_2)
| ~ present(VAR_0,VAR_2)
| ~ think_believe_consider(VAR_0,VAR_2)
| ~ accessible_world(VAR_0,VAR_1)
| ~ proposition(VAR_0,VAR_1) ),
file('theBenchmark.p',clause94) ).
cnf(c_1,plain,
( man(B,skf4(B))
| ~ actual_world(A)
| ~ think_believe_consider(A,V13)
| ~ present(A,V13)
| ~ event(A,V13)
| ~ theme(A,V13,V8)
| ~ of(A,V12,V14)
| ~ man(A,V14)
| ~ agent(A,V13,V14)
| ~ forename(A,V12)
| ~ vincent_forename(A,V12)
| ~ of(A,V9,V11)
| ~ man(A,V11)
| ~ event(V8,V10)
| ~ agent(V8,V10,V11)
| ~ present(V8,V10)
| ~ smoke(V8,V10)
| ~ forename(A,V9)
| ~ jules_forename(A,V9)
| ~ proposition(A,V8)
| ~ accessible_world(A,V8)
| ~ of(A,V7,V6)
| ~ jules_forename(A,V7)
| ~ forename(A,V7)
| ~ be(A,F,V6,V6)
| ~ man(A,V6)
| ~ state(A,F)
| ~ of(A,D,E)
| ~ man(A,E)
| ~ agent(A,C,E)
| ~ forename(A,D)
| ~ vincent_forename(A,D)
| ~ theme(A,C,B)
| ~ event(A,C)
| ~ present(A,C)
| ~ think_believe_consider(A,C)
| ~ accessible_world(A,B)
| ~ proposition(A,B) ),
inference(clausify,[status(thm)],[clause94]) ).
fof(clause72,axiom,
actual_world(skc8),
file('theBenchmark.p',clause72) ).
cnf(c_2,plain,
actual_world(skc8),
inference(clausify,[status(thm)],[clause72]) ).
fof(clause95,axiom,
! [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] :
( ~ actual_world(VAR_0)
| ~ think_believe_consider(VAR_0,VAR_14)
| ~ present(VAR_0,VAR_14)
| ~ event(VAR_0,VAR_14)
| ~ theme(VAR_0,VAR_14,VAR_9)
| ~ of(VAR_0,VAR_13,VAR_15)
| ~ man(VAR_0,VAR_15)
| ~ agent(VAR_0,VAR_14,VAR_15)
| ~ forename(VAR_0,VAR_13)
| ~ vincent_forename(VAR_0,VAR_13)
| ~ of(VAR_0,VAR_10,VAR_12)
| ~ man(VAR_0,VAR_12)
| ~ event(VAR_9,VAR_11)
| ~ agent(VAR_9,VAR_11,VAR_12)
| ~ present(VAR_9,VAR_11)
| ~ smoke(VAR_9,VAR_11)
| ~ forename(VAR_0,VAR_10)
| ~ jules_forename(VAR_0,VAR_10)
| ~ proposition(VAR_0,VAR_9)
| ~ accessible_world(VAR_0,VAR_9)
| ~ of(VAR_0,VAR_8,VAR_7)
| ~ jules_forename(VAR_0,VAR_8)
| ~ forename(VAR_0,VAR_8)
| ~ be(VAR_0,VAR_6,VAR_7,VAR_7)
| ~ man(VAR_0,VAR_7)
| ~ state(VAR_0,VAR_6)
| ~ of(VAR_0,VAR_4,VAR_5)
| ~ man(VAR_0,VAR_5)
| ~ agent(VAR_0,VAR_3,VAR_5)
| ~ forename(VAR_0,VAR_4)
| ~ vincent_forename(VAR_0,VAR_4)
| ~ theme(VAR_0,VAR_3,VAR_1)
| ~ event(VAR_0,VAR_3)
| ~ present(VAR_0,VAR_3)
| ~ think_believe_consider(VAR_0,VAR_3)
| ~ event(VAR_1,VAR_2)
| ~ agent(VAR_1,VAR_2,skf4(VAR_1))
| ~ present(VAR_1,VAR_2)
| ~ smoke(VAR_1,VAR_2)
| ~ accessible_world(VAR_0,VAR_1)
| ~ proposition(VAR_0,VAR_1) ),
file('theBenchmark.p',clause95) ).
cnf(c_3,plain,
( ~ actual_world(A)
| ~ think_believe_consider(A,V14)
| ~ present(A,V14)
| ~ event(A,V14)
| ~ theme(A,V14,V9)
| ~ of(A,V13,V15)
| ~ man(A,V15)
| ~ agent(A,V14,V15)
| ~ forename(A,V13)
| ~ vincent_forename(A,V13)
| ~ of(A,V10,V12)
| ~ man(A,V12)
| ~ event(V9,V11)
| ~ agent(V9,V11,V12)
| ~ present(V9,V11)
| ~ smoke(V9,V11)
| ~ forename(A,V10)
| ~ jules_forename(A,V10)
| ~ proposition(A,V9)
| ~ accessible_world(A,V9)
| ~ of(A,V8,V7)
| ~ jules_forename(A,V8)
| ~ forename(A,V8)
| ~ be(A,V6,V7,V7)
| ~ man(A,V7)
| ~ state(A,V6)
| ~ of(A,E,F)
| ~ man(A,F)
| ~ agent(A,D,F)
| ~ forename(A,E)
| ~ vincent_forename(A,E)
| ~ theme(A,D,B)
| ~ event(A,D)
| ~ present(A,D)
| ~ think_believe_consider(A,D)
| ~ event(B,C)
| ~ agent(B,C,skf4(B))
| ~ present(B,C)
| ~ smoke(B,C)
| ~ accessible_world(A,B)
| ~ proposition(A,B) ),
inference(clausify,[status(thm)],[clause95]) ).
cnf(c_4,plain,
( ~ think_believe_consider(skc8,V13)
| ~ present(skc8,V13)
| ~ event(skc8,V13)
| ~ theme(skc8,V13,V8)
| ~ of(skc8,V12,V14)
| ~ man(skc8,V14)
| ~ agent(skc8,V13,V14)
| ~ forename(skc8,V12)
| ~ vincent_forename(skc8,V12)
| ~ of(skc8,V9,V11)
| ~ man(skc8,V11)
| ~ event(V8,V10)
| ~ agent(V8,V10,V11)
| ~ present(V8,V10)
| ~ smoke(V8,V10)
| ~ forename(skc8,V9)
| ~ jules_forename(skc8,V9)
| ~ proposition(skc8,V8)
| ~ accessible_world(skc8,V8)
| ~ of(skc8,V7,V6)
| ~ jules_forename(skc8,V7)
| ~ forename(skc8,V7)
| ~ be(skc8,F,V6,V6)
| ~ man(skc8,V6)
| ~ state(skc8,F)
| ~ of(skc8,D,E)
| ~ man(skc8,E)
| ~ agent(skc8,C,E)
| ~ forename(skc8,D)
| ~ vincent_forename(skc8,D)
| ~ theme(skc8,C,A)
| ~ event(skc8,C)
| ~ present(skc8,C)
| ~ think_believe_consider(skc8,C)
| ~ event(A,B)
| ~ agent(A,B,skf4(A))
| ~ present(A,B)
| ~ smoke(A,B)
| ~ accessible_world(skc8,A)
| ~ proposition(skc8,A) ),
inference(resolve,[status(thm)],[c_3,c_2]) ).
cnf(c_5,plain,
( man(A,skf4(A))
| ~ think_believe_consider(skc8,V12)
| ~ present(skc8,V12)
| ~ event(skc8,V12)
| ~ theme(skc8,V12,V7)
| ~ of(skc8,V11,V13)
| ~ man(skc8,V13)
| ~ agent(skc8,V12,V13)
| ~ forename(skc8,V11)
| ~ vincent_forename(skc8,V11)
| ~ of(skc8,V8,V10)
| ~ man(skc8,V10)
| ~ event(V7,V9)
| ~ agent(V7,V9,V10)
| ~ present(V7,V9)
| ~ smoke(V7,V9)
| ~ forename(skc8,V8)
| ~ jules_forename(skc8,V8)
| ~ proposition(skc8,V7)
| ~ accessible_world(skc8,V7)
| ~ of(skc8,V6,F)
| ~ jules_forename(skc8,V6)
| ~ forename(skc8,V6)
| ~ be(skc8,E,F,F)
| ~ man(skc8,F)
| ~ state(skc8,E)
| ~ of(skc8,C,D)
| ~ man(skc8,D)
| ~ agent(skc8,B,D)
| ~ forename(skc8,C)
| ~ vincent_forename(skc8,C)
| ~ theme(skc8,B,A)
| ~ event(skc8,B)
| ~ present(skc8,B)
| ~ think_believe_consider(skc8,B)
| ~ accessible_world(skc8,A)
| ~ proposition(skc8,A) ),
inference(resolve,[status(thm)],[c_1,c_2]) ).
fof(clause93,axiom,
! [VAR_0] :
( agent(skc12,skf2(VAR_0),VAR_0)
| ~ man(skc12,VAR_0) ),
file('theBenchmark.p',clause93) ).
cnf(c_6,plain,
( agent(skc12,skf2(A),A)
| ~ man(skc12,A) ),
inference(clausify,[status(thm)],[clause93]) ).
fof(clause92,axiom,
! [VAR_0,VAR_1] :
( event(skc12,skf2(VAR_1))
| ~ man(skc12,VAR_0) ),
file('theBenchmark.p',clause92) ).
cnf(c_7,plain,
( event(skc12,skf2(B))
| ~ man(skc12,A) ),
inference(clausify,[status(thm)],[clause92]) ).
fof(clause91,axiom,
! [VAR_0,VAR_1] :
( present(skc12,skf2(VAR_1))
| ~ man(skc12,VAR_0) ),
file('theBenchmark.p',clause91) ).
cnf(c_8,plain,
( present(skc12,skf2(B))
| ~ man(skc12,A) ),
inference(clausify,[status(thm)],[clause91]) ).
fof(clause90,axiom,
! [VAR_0,VAR_1] :
( smoke(skc12,skf2(VAR_1))
| ~ man(skc12,VAR_0) ),
file('theBenchmark.p',clause90) ).
cnf(c_9,plain,
( smoke(skc12,skf2(B))
| ~ man(skc12,A) ),
inference(clausify,[status(thm)],[clause90]) ).
fof(clause89,axiom,
be(skc8,skc9,skc10,skc10),
file('theBenchmark.p',clause89) ).
cnf(c_10,plain,
be(skc8,skc9,skc10,skc10),
inference(clausify,[status(thm)],[clause89]) ).
fof(clause88,axiom,
of(skc8,skc11,skc10),
file('theBenchmark.p',clause88) ).
cnf(c_11,plain,
of(skc8,skc11,skc10),
inference(clausify,[status(thm)],[clause88]) ).
fof(clause87,axiom,
theme(skc8,skc13,skc12),
file('theBenchmark.p',clause87) ).
cnf(c_12,plain,
theme(skc8,skc13,skc12),
inference(clausify,[status(thm)],[clause87]) ).
fof(clause86,axiom,
agent(skc8,skc13,skc15),
file('theBenchmark.p',clause86) ).
cnf(c_13,plain,
agent(skc8,skc13,skc15),
inference(clausify,[status(thm)],[clause86]) ).
fof(clause85,axiom,
of(skc8,skc14,skc15),
file('theBenchmark.p',clause85) ).
cnf(c_14,plain,
of(skc8,skc14,skc15),
inference(clausify,[status(thm)],[clause85]) ).
fof(clause84,axiom,
proposition(skc8,skc12),
file('theBenchmark.p',clause84) ).
cnf(c_15,plain,
proposition(skc8,skc12),
inference(clausify,[status(thm)],[clause84]) ).
fof(clause83,axiom,
accessible_world(skc8,skc12),
file('theBenchmark.p',clause83) ).
cnf(c_16,plain,
accessible_world(skc8,skc12),
inference(clausify,[status(thm)],[clause83]) ).
fof(clause82,axiom,
state(skc8,skc9),
file('theBenchmark.p',clause82) ).
cnf(c_17,plain,
state(skc8,skc9),
inference(clausify,[status(thm)],[clause82]) ).
fof(clause81,axiom,
man(skc8,skc10),
file('theBenchmark.p',clause81) ).
cnf(c_18,plain,
man(skc8,skc10),
inference(clausify,[status(thm)],[clause81]) ).
fof(clause80,axiom,
forename(skc8,skc11),
file('theBenchmark.p',clause80) ).
cnf(c_19,plain,
forename(skc8,skc11),
inference(clausify,[status(thm)],[clause80]) ).
fof(clause79,axiom,
jules_forename(skc8,skc11),
file('theBenchmark.p',clause79) ).
cnf(c_20,plain,
jules_forename(skc8,skc11),
inference(clausify,[status(thm)],[clause79]) ).
fof(clause78,axiom,
think_believe_consider(skc8,skc13),
file('theBenchmark.p',clause78) ).
cnf(c_21,plain,
think_believe_consider(skc8,skc13),
inference(clausify,[status(thm)],[clause78]) ).
fof(clause77,axiom,
present(skc8,skc13),
file('theBenchmark.p',clause77) ).
cnf(c_22,plain,
present(skc8,skc13),
inference(clausify,[status(thm)],[clause77]) ).
fof(clause76,axiom,
event(skc8,skc13),
file('theBenchmark.p',clause76) ).
cnf(c_23,plain,
event(skc8,skc13),
inference(clausify,[status(thm)],[clause76]) ).
fof(clause75,axiom,
vincent_forename(skc8,skc14),
file('theBenchmark.p',clause75) ).
cnf(c_24,plain,
vincent_forename(skc8,skc14),
inference(clausify,[status(thm)],[clause75]) ).
fof(clause74,axiom,
forename(skc8,skc14),
file('theBenchmark.p',clause74) ).
cnf(c_25,plain,
forename(skc8,skc14),
inference(clausify,[status(thm)],[clause74]) ).
fof(clause73,axiom,
man(skc8,skc15),
file('theBenchmark.p',clause73) ).
cnf(c_26,plain,
man(skc8,skc15),
inference(clausify,[status(thm)],[clause73]) ).
fof(clause52,axiom,
! [VAR_0,VAR_1,VAR_2] :
( man(VAR_1,VAR_2)
| ~ man(VAR_0,VAR_2)
| ~ accessible_world(VAR_0,VAR_1) ),
file('theBenchmark.p',clause52) ).
cnf(c_46,plain,
( man(B,C)
| ~ man(A,C)
| ~ accessible_world(A,B) ),
inference(clausify,[status(thm)],[clause52]) ).
cnf(c_291,plain,
( man(skc12,A)
| ~ man(skc8,A) ),
inference(resolve,[status(thm)],[c_46,c_16]) ).
cnf(c_107,plain,
man(skc12,skc15),
inference(resolve,[status(thm)],[c_291,c_26]) ).
cnf(c_292,plain,
( man(skc12,A)
| ~ man(skc8,A) ),
inference(resolve,[status(thm)],[c_46,c_16]) ).
cnf(c_108,plain,
man(skc12,skc10),
inference(resolve,[status(thm)],[c_292,c_18]) ).
cnf(c_128,plain,
smoke(skc12,skf2(A)),
inference(resolve,[status(thm)],[c_9,c_107]) ).
cnf(c_129,plain,
present(skc12,skf2(A)),
inference(resolve,[status(thm)],[c_8,c_107]) ).
cnf(c_130,plain,
event(skc12,skf2(A)),
inference(resolve,[status(thm)],[c_7,c_107]) ).
cnf(c_134,plain,
agent(skc12,skf2(skc10),skc10),
inference(resolve,[status(thm)],[c_6,c_108]) ).
cnf(c_293,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,V11)
| ~ present(skc8,V11)
| ~ event(skc8,V11)
| ~ theme(skc8,V11,V6)
| ~ of(skc8,V10,V12)
| ~ man(skc8,V12)
| ~ agent(skc8,V11,V12)
| ~ forename(skc8,V10)
| ~ vincent_forename(skc8,V10)
| ~ of(skc8,V7,V9)
| ~ man(skc8,V9)
| ~ event(V6,V8)
| ~ agent(V6,V8,V9)
| ~ present(V6,V8)
| ~ smoke(V6,V8)
| ~ forename(skc8,V7)
| ~ jules_forename(skc8,V7)
| ~ proposition(skc8,V6)
| ~ accessible_world(skc8,V6)
| ~ of(skc8,F,E)
| ~ jules_forename(skc8,F)
| ~ forename(skc8,F)
| ~ be(skc8,D,E,E)
| ~ man(skc8,E)
| ~ state(skc8,D)
| ~ of(skc8,B,C)
| ~ man(skc8,C)
| ~ agent(skc8,A,C)
| ~ forename(skc8,B)
| ~ vincent_forename(skc8,B)
| ~ theme(skc8,A,skc12)
| ~ event(skc8,A)
| ~ present(skc8,A)
| ~ think_believe_consider(skc8,A)
| ~ accessible_world(skc8,skc12) ),
inference(resolve,[status(thm)],[c_5,c_15]) ).
cnf(c_294,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,V11)
| ~ present(skc8,V11)
| ~ event(skc8,V11)
| ~ theme(skc8,V11,V6)
| ~ of(skc8,V10,V12)
| ~ man(skc8,V12)
| ~ agent(skc8,V11,V12)
| ~ forename(skc8,V10)
| ~ vincent_forename(skc8,V10)
| ~ of(skc8,V7,V9)
| ~ man(skc8,V9)
| ~ event(V6,V8)
| ~ agent(V6,V8,V9)
| ~ present(V6,V8)
| ~ smoke(V6,V8)
| ~ forename(skc8,V7)
| ~ jules_forename(skc8,V7)
| ~ proposition(skc8,V6)
| ~ accessible_world(skc8,V6)
| ~ of(skc8,F,E)
| ~ jules_forename(skc8,F)
| ~ forename(skc8,F)
| ~ be(skc8,D,E,E)
| ~ man(skc8,E)
| ~ state(skc8,D)
| ~ of(skc8,B,C)
| ~ man(skc8,C)
| ~ agent(skc8,A,C)
| ~ forename(skc8,B)
| ~ vincent_forename(skc8,B)
| ~ theme(skc8,A,skc12)
| ~ event(skc8,A)
| ~ present(skc8,A)
| ~ think_believe_consider(skc8,A) ),
inference(resolve,[status(thm)],[c_293,c_16]) ).
cnf(c_295,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,V10)
| ~ present(skc8,V10)
| ~ event(skc8,V10)
| ~ theme(skc8,V10,F)
| ~ of(skc8,V9,V11)
| ~ man(skc8,V11)
| ~ agent(skc8,V10,V11)
| ~ forename(skc8,V9)
| ~ vincent_forename(skc8,V9)
| ~ of(skc8,V6,V8)
| ~ man(skc8,V8)
| ~ event(F,V7)
| ~ agent(F,V7,V8)
| ~ present(F,V7)
| ~ smoke(F,V7)
| ~ forename(skc8,V6)
| ~ jules_forename(skc8,V6)
| ~ proposition(skc8,F)
| ~ accessible_world(skc8,F)
| ~ of(skc8,E,D)
| ~ jules_forename(skc8,E)
| ~ forename(skc8,E)
| ~ be(skc8,C,D,D)
| ~ man(skc8,D)
| ~ state(skc8,C)
| ~ of(skc8,A,B)
| ~ man(skc8,B)
| ~ agent(skc8,skc13,B)
| ~ forename(skc8,A)
| ~ vincent_forename(skc8,A)
| ~ theme(skc8,skc13,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13) ),
inference(resolve,[status(thm)],[c_294,c_21]) ).
cnf(c_296,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,V10)
| ~ present(skc8,V10)
| ~ event(skc8,V10)
| ~ theme(skc8,V10,F)
| ~ of(skc8,V9,V11)
| ~ man(skc8,V11)
| ~ agent(skc8,V10,V11)
| ~ forename(skc8,V9)
| ~ vincent_forename(skc8,V9)
| ~ of(skc8,V6,V8)
| ~ man(skc8,V8)
| ~ event(F,V7)
| ~ agent(F,V7,V8)
| ~ present(F,V7)
| ~ smoke(F,V7)
| ~ forename(skc8,V6)
| ~ jules_forename(skc8,V6)
| ~ proposition(skc8,F)
| ~ accessible_world(skc8,F)
| ~ of(skc8,E,D)
| ~ jules_forename(skc8,E)
| ~ forename(skc8,E)
| ~ be(skc8,C,D,D)
| ~ man(skc8,D)
| ~ state(skc8,C)
| ~ of(skc8,A,B)
| ~ man(skc8,B)
| ~ agent(skc8,skc13,B)
| ~ forename(skc8,A)
| ~ vincent_forename(skc8,A)
| ~ theme(skc8,skc13,skc12)
| ~ event(skc8,skc13) ),
inference(resolve,[status(thm)],[c_295,c_22]) ).
cnf(c_297,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,V10)
| ~ present(skc8,V10)
| ~ event(skc8,V10)
| ~ theme(skc8,V10,F)
| ~ of(skc8,V9,V11)
| ~ man(skc8,V11)
| ~ agent(skc8,V10,V11)
| ~ forename(skc8,V9)
| ~ vincent_forename(skc8,V9)
| ~ of(skc8,V6,V8)
| ~ man(skc8,V8)
| ~ event(F,V7)
| ~ agent(F,V7,V8)
| ~ present(F,V7)
| ~ smoke(F,V7)
| ~ forename(skc8,V6)
| ~ jules_forename(skc8,V6)
| ~ proposition(skc8,F)
| ~ accessible_world(skc8,F)
| ~ of(skc8,E,D)
| ~ jules_forename(skc8,E)
| ~ forename(skc8,E)
| ~ be(skc8,C,D,D)
| ~ man(skc8,D)
| ~ state(skc8,C)
| ~ of(skc8,A,B)
| ~ man(skc8,B)
| ~ agent(skc8,skc13,B)
| ~ forename(skc8,A)
| ~ vincent_forename(skc8,A)
| ~ theme(skc8,skc13,skc12) ),
inference(resolve,[status(thm)],[c_296,c_23]) ).
cnf(c_298,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,V10)
| ~ present(skc8,V10)
| ~ event(skc8,V10)
| ~ theme(skc8,V10,F)
| ~ of(skc8,V9,V11)
| ~ man(skc8,V11)
| ~ agent(skc8,V10,V11)
| ~ forename(skc8,V9)
| ~ vincent_forename(skc8,V9)
| ~ of(skc8,V6,V8)
| ~ man(skc8,V8)
| ~ event(F,V7)
| ~ agent(F,V7,V8)
| ~ present(F,V7)
| ~ smoke(F,V7)
| ~ forename(skc8,V6)
| ~ jules_forename(skc8,V6)
| ~ proposition(skc8,F)
| ~ accessible_world(skc8,F)
| ~ of(skc8,E,D)
| ~ jules_forename(skc8,E)
| ~ forename(skc8,E)
| ~ be(skc8,C,D,D)
| ~ man(skc8,D)
| ~ state(skc8,C)
| ~ of(skc8,A,B)
| ~ man(skc8,B)
| ~ agent(skc8,skc13,B)
| ~ forename(skc8,A)
| ~ vincent_forename(skc8,A) ),
inference(resolve,[status(thm)],[c_297,c_12]) ).
cnf(c_299,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,V9)
| ~ present(skc8,V9)
| ~ event(skc8,V9)
| ~ theme(skc8,V9,E)
| ~ of(skc8,V8,V10)
| ~ man(skc8,V10)
| ~ agent(skc8,V9,V10)
| ~ forename(skc8,V8)
| ~ vincent_forename(skc8,V8)
| ~ of(skc8,F,V7)
| ~ man(skc8,V7)
| ~ event(E,V6)
| ~ agent(E,V6,V7)
| ~ present(E,V6)
| ~ smoke(E,V6)
| ~ forename(skc8,F)
| ~ jules_forename(skc8,F)
| ~ proposition(skc8,E)
| ~ accessible_world(skc8,E)
| ~ of(skc8,D,C)
| ~ jules_forename(skc8,D)
| ~ forename(skc8,D)
| ~ be(skc8,B,C,C)
| ~ man(skc8,C)
| ~ state(skc8,B)
| ~ of(skc8,skc14,A)
| ~ man(skc8,A)
| ~ agent(skc8,skc13,A)
| ~ forename(skc8,skc14) ),
inference(resolve,[status(thm)],[c_298,c_24]) ).
cnf(c_300,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,V9)
| ~ present(skc8,V9)
| ~ event(skc8,V9)
| ~ theme(skc8,V9,E)
| ~ of(skc8,V8,V10)
| ~ man(skc8,V10)
| ~ agent(skc8,V9,V10)
| ~ forename(skc8,V8)
| ~ vincent_forename(skc8,V8)
| ~ of(skc8,F,V7)
| ~ man(skc8,V7)
| ~ event(E,V6)
| ~ agent(E,V6,V7)
| ~ present(E,V6)
| ~ smoke(E,V6)
| ~ forename(skc8,F)
| ~ jules_forename(skc8,F)
| ~ proposition(skc8,E)
| ~ accessible_world(skc8,E)
| ~ of(skc8,D,C)
| ~ jules_forename(skc8,D)
| ~ forename(skc8,D)
| ~ be(skc8,B,C,C)
| ~ man(skc8,C)
| ~ state(skc8,B)
| ~ of(skc8,skc14,A)
| ~ man(skc8,A)
| ~ agent(skc8,skc13,A) ),
inference(resolve,[status(thm)],[c_299,c_25]) ).
cnf(c_301,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,V8)
| ~ present(skc8,V8)
| ~ event(skc8,V8)
| ~ theme(skc8,V8,D)
| ~ of(skc8,V7,V9)
| ~ man(skc8,V9)
| ~ agent(skc8,V8,V9)
| ~ forename(skc8,V7)
| ~ vincent_forename(skc8,V7)
| ~ of(skc8,E,V6)
| ~ man(skc8,V6)
| ~ event(D,F)
| ~ agent(D,F,V6)
| ~ present(D,F)
| ~ smoke(D,F)
| ~ forename(skc8,E)
| ~ jules_forename(skc8,E)
| ~ proposition(skc8,D)
| ~ accessible_world(skc8,D)
| ~ of(skc8,C,B)
| ~ jules_forename(skc8,C)
| ~ forename(skc8,C)
| ~ be(skc8,A,B,B)
| ~ man(skc8,B)
| ~ state(skc8,A)
| ~ of(skc8,skc14,skc15)
| ~ man(skc8,skc15) ),
inference(resolve,[status(thm)],[c_300,c_13]) ).
cnf(c_302,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,V8)
| ~ present(skc8,V8)
| ~ event(skc8,V8)
| ~ theme(skc8,V8,D)
| ~ of(skc8,V7,V9)
| ~ man(skc8,V9)
| ~ agent(skc8,V8,V9)
| ~ forename(skc8,V7)
| ~ vincent_forename(skc8,V7)
| ~ of(skc8,E,V6)
| ~ man(skc8,V6)
| ~ event(D,F)
| ~ agent(D,F,V6)
| ~ present(D,F)
| ~ smoke(D,F)
| ~ forename(skc8,E)
| ~ jules_forename(skc8,E)
| ~ proposition(skc8,D)
| ~ accessible_world(skc8,D)
| ~ of(skc8,C,B)
| ~ jules_forename(skc8,C)
| ~ forename(skc8,C)
| ~ be(skc8,A,B,B)
| ~ man(skc8,B)
| ~ state(skc8,A)
| ~ of(skc8,skc14,skc15) ),
inference(resolve,[status(thm)],[c_301,c_26]) ).
cnf(c_303,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,V8)
| ~ present(skc8,V8)
| ~ event(skc8,V8)
| ~ theme(skc8,V8,D)
| ~ of(skc8,V7,V9)
| ~ man(skc8,V9)
| ~ agent(skc8,V8,V9)
| ~ forename(skc8,V7)
| ~ vincent_forename(skc8,V7)
| ~ of(skc8,E,V6)
| ~ man(skc8,V6)
| ~ event(D,F)
| ~ agent(D,F,V6)
| ~ present(D,F)
| ~ smoke(D,F)
| ~ forename(skc8,E)
| ~ jules_forename(skc8,E)
| ~ proposition(skc8,D)
| ~ accessible_world(skc8,D)
| ~ of(skc8,C,B)
| ~ jules_forename(skc8,C)
| ~ forename(skc8,C)
| ~ be(skc8,A,B,B)
| ~ man(skc8,B)
| ~ state(skc8,A) ),
inference(resolve,[status(thm)],[c_302,c_14]) ).
cnf(c_304,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,V7)
| ~ present(skc8,V7)
| ~ event(skc8,V7)
| ~ theme(skc8,V7,C)
| ~ of(skc8,V6,V8)
| ~ man(skc8,V8)
| ~ agent(skc8,V7,V8)
| ~ forename(skc8,V6)
| ~ vincent_forename(skc8,V6)
| ~ of(skc8,D,F)
| ~ man(skc8,F)
| ~ event(C,E)
| ~ agent(C,E,F)
| ~ present(C,E)
| ~ smoke(C,E)
| ~ forename(skc8,D)
| ~ jules_forename(skc8,D)
| ~ proposition(skc8,C)
| ~ accessible_world(skc8,C)
| ~ of(skc8,B,A)
| ~ jules_forename(skc8,B)
| ~ forename(skc8,B)
| ~ be(skc8,skc9,A,A)
| ~ man(skc8,A) ),
inference(resolve,[status(thm)],[c_303,c_17]) ).
cnf(c_305,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,V6)
| ~ present(skc8,V6)
| ~ event(skc8,V6)
| ~ theme(skc8,V6,B)
| ~ of(skc8,F,V7)
| ~ man(skc8,V7)
| ~ agent(skc8,V6,V7)
| ~ forename(skc8,F)
| ~ vincent_forename(skc8,F)
| ~ of(skc8,C,E)
| ~ man(skc8,E)
| ~ event(B,D)
| ~ agent(B,D,E)
| ~ present(B,D)
| ~ smoke(B,D)
| ~ forename(skc8,C)
| ~ jules_forename(skc8,C)
| ~ proposition(skc8,B)
| ~ accessible_world(skc8,B)
| ~ of(skc8,A,skc10)
| ~ jules_forename(skc8,A)
| ~ forename(skc8,A)
| ~ be(skc8,skc9,skc10,skc10) ),
inference(resolve,[status(thm)],[c_304,c_18]) ).
cnf(c_306,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,V6)
| ~ present(skc8,V6)
| ~ event(skc8,V6)
| ~ theme(skc8,V6,B)
| ~ of(skc8,F,V7)
| ~ man(skc8,V7)
| ~ agent(skc8,V6,V7)
| ~ forename(skc8,F)
| ~ vincent_forename(skc8,F)
| ~ of(skc8,C,E)
| ~ man(skc8,E)
| ~ event(B,D)
| ~ agent(B,D,E)
| ~ present(B,D)
| ~ smoke(B,D)
| ~ forename(skc8,C)
| ~ jules_forename(skc8,C)
| ~ proposition(skc8,B)
| ~ accessible_world(skc8,B)
| ~ of(skc8,A,skc10)
| ~ jules_forename(skc8,A)
| ~ forename(skc8,A) ),
inference(resolve,[status(thm)],[c_305,c_10]) ).
cnf(c_307,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,F)
| ~ present(skc8,F)
| ~ event(skc8,F)
| ~ theme(skc8,F,A)
| ~ of(skc8,E,V6)
| ~ man(skc8,V6)
| ~ agent(skc8,F,V6)
| ~ forename(skc8,E)
| ~ vincent_forename(skc8,E)
| ~ of(skc8,B,D)
| ~ man(skc8,D)
| ~ event(A,C)
| ~ agent(A,C,D)
| ~ present(A,C)
| ~ smoke(A,C)
| ~ forename(skc8,B)
| ~ jules_forename(skc8,B)
| ~ proposition(skc8,A)
| ~ accessible_world(skc8,A)
| ~ of(skc8,skc11,skc10)
| ~ jules_forename(skc8,skc11) ),
inference(resolve,[status(thm)],[c_306,c_19]) ).
cnf(c_308,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,F)
| ~ present(skc8,F)
| ~ event(skc8,F)
| ~ theme(skc8,F,A)
| ~ of(skc8,E,V6)
| ~ man(skc8,V6)
| ~ agent(skc8,F,V6)
| ~ forename(skc8,E)
| ~ vincent_forename(skc8,E)
| ~ of(skc8,B,D)
| ~ man(skc8,D)
| ~ event(A,C)
| ~ agent(A,C,D)
| ~ present(A,C)
| ~ smoke(A,C)
| ~ forename(skc8,B)
| ~ jules_forename(skc8,B)
| ~ proposition(skc8,A)
| ~ accessible_world(skc8,A)
| ~ of(skc8,skc11,skc10) ),
inference(resolve,[status(thm)],[c_307,c_20]) ).
cnf(c_309,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,F)
| ~ present(skc8,F)
| ~ event(skc8,F)
| ~ theme(skc8,F,A)
| ~ of(skc8,E,V6)
| ~ man(skc8,V6)
| ~ agent(skc8,F,V6)
| ~ forename(skc8,E)
| ~ vincent_forename(skc8,E)
| ~ of(skc8,B,D)
| ~ man(skc8,D)
| ~ event(A,C)
| ~ agent(A,C,D)
| ~ present(A,C)
| ~ smoke(A,C)
| ~ forename(skc8,B)
| ~ jules_forename(skc8,B)
| ~ proposition(skc8,A)
| ~ accessible_world(skc8,A) ),
inference(resolve,[status(thm)],[c_308,c_11]) ).
cnf(c_310,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,E)
| ~ present(skc8,E)
| ~ event(skc8,E)
| ~ theme(skc8,E,skc12)
| ~ of(skc8,D,F)
| ~ man(skc8,F)
| ~ agent(skc8,E,F)
| ~ forename(skc8,D)
| ~ vincent_forename(skc8,D)
| ~ of(skc8,A,C)
| ~ man(skc8,C)
| ~ event(skc12,B)
| ~ agent(skc12,B,C)
| ~ present(skc12,B)
| ~ smoke(skc12,B)
| ~ forename(skc8,A)
| ~ jules_forename(skc8,A)
| ~ proposition(skc8,skc12) ),
inference(resolve,[status(thm)],[c_309,c_16]) ).
cnf(c_311,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,E)
| ~ present(skc8,E)
| ~ event(skc8,E)
| ~ theme(skc8,E,skc12)
| ~ of(skc8,D,F)
| ~ man(skc8,F)
| ~ agent(skc8,E,F)
| ~ forename(skc8,D)
| ~ vincent_forename(skc8,D)
| ~ of(skc8,A,C)
| ~ man(skc8,C)
| ~ event(skc12,B)
| ~ agent(skc12,B,C)
| ~ present(skc12,B)
| ~ smoke(skc12,B)
| ~ forename(skc8,A)
| ~ jules_forename(skc8,A) ),
inference(resolve,[status(thm)],[c_310,c_15]) ).
cnf(c_312,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,D)
| ~ present(skc8,D)
| ~ event(skc8,D)
| ~ theme(skc8,D,skc12)
| ~ of(skc8,C,E)
| ~ man(skc8,E)
| ~ agent(skc8,D,E)
| ~ forename(skc8,C)
| ~ vincent_forename(skc8,C)
| ~ of(skc8,skc11,B)
| ~ man(skc8,B)
| ~ event(skc12,A)
| ~ agent(skc12,A,B)
| ~ present(skc12,A)
| ~ smoke(skc12,A)
| ~ forename(skc8,skc11) ),
inference(resolve,[status(thm)],[c_311,c_20]) ).
cnf(c_313,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,D)
| ~ present(skc8,D)
| ~ event(skc8,D)
| ~ theme(skc8,D,skc12)
| ~ of(skc8,C,E)
| ~ man(skc8,E)
| ~ agent(skc8,D,E)
| ~ forename(skc8,C)
| ~ vincent_forename(skc8,C)
| ~ of(skc8,skc11,B)
| ~ man(skc8,B)
| ~ event(skc12,A)
| ~ agent(skc12,A,B)
| ~ present(skc12,A)
| ~ smoke(skc12,A) ),
inference(resolve,[status(thm)],[c_312,c_19]) ).
cnf(c_314,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,D)
| ~ present(skc8,D)
| ~ event(skc8,D)
| ~ theme(skc8,D,skc12)
| ~ of(skc8,C,E)
| ~ man(skc8,E)
| ~ agent(skc8,D,E)
| ~ forename(skc8,C)
| ~ vincent_forename(skc8,C)
| ~ of(skc8,skc11,B)
| ~ man(skc8,B)
| ~ event(skc12,skf2(A))
| ~ agent(skc12,skf2(A),B)
| ~ present(skc12,skf2(A)) ),
inference(resolve,[status(thm)],[c_313,c_128]) ).
cnf(c_315,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,D)
| ~ present(skc8,D)
| ~ event(skc8,D)
| ~ theme(skc8,D,skc12)
| ~ of(skc8,C,E)
| ~ man(skc8,E)
| ~ agent(skc8,D,E)
| ~ forename(skc8,C)
| ~ vincent_forename(skc8,C)
| ~ of(skc8,skc11,B)
| ~ man(skc8,B)
| ~ event(skc12,skf2(A))
| ~ agent(skc12,skf2(A),B) ),
inference(resolve,[status(thm)],[c_314,c_129]) ).
cnf(c_316,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,B)
| ~ present(skc8,B)
| ~ event(skc8,B)
| ~ theme(skc8,B,skc12)
| ~ of(skc8,A,C)
| ~ man(skc8,C)
| ~ agent(skc8,B,C)
| ~ forename(skc8,A)
| ~ vincent_forename(skc8,A)
| ~ of(skc8,skc11,skc10)
| ~ man(skc8,skc10)
| ~ event(skc12,skf2(skc10)) ),
inference(resolve,[status(thm)],[c_315,c_134]) ).
cnf(c_317,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,B)
| ~ present(skc8,B)
| ~ event(skc8,B)
| ~ theme(skc8,B,skc12)
| ~ of(skc8,A,C)
| ~ man(skc8,C)
| ~ agent(skc8,B,C)
| ~ forename(skc8,A)
| ~ vincent_forename(skc8,A)
| ~ of(skc8,skc11,skc10)
| ~ man(skc8,skc10) ),
inference(resolve,[status(thm)],[c_316,c_130]) ).
cnf(c_318,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,B)
| ~ present(skc8,B)
| ~ event(skc8,B)
| ~ theme(skc8,B,skc12)
| ~ of(skc8,A,C)
| ~ man(skc8,C)
| ~ agent(skc8,B,C)
| ~ forename(skc8,A)
| ~ vincent_forename(skc8,A)
| ~ of(skc8,skc11,skc10) ),
inference(resolve,[status(thm)],[c_317,c_18]) ).
cnf(c_319,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,B)
| ~ present(skc8,B)
| ~ event(skc8,B)
| ~ theme(skc8,B,skc12)
| ~ of(skc8,A,C)
| ~ man(skc8,C)
| ~ agent(skc8,B,C)
| ~ forename(skc8,A)
| ~ vincent_forename(skc8,A) ),
inference(resolve,[status(thm)],[c_318,c_11]) ).
cnf(c_320,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,A)
| ~ present(skc8,A)
| ~ event(skc8,A)
| ~ theme(skc8,A,skc12)
| ~ of(skc8,skc14,B)
| ~ man(skc8,B)
| ~ agent(skc8,A,B)
| ~ forename(skc8,skc14) ),
inference(resolve,[status(thm)],[c_319,c_24]) ).
cnf(c_321,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,A)
| ~ present(skc8,A)
| ~ event(skc8,A)
| ~ theme(skc8,A,skc12)
| ~ of(skc8,skc14,B)
| ~ man(skc8,B)
| ~ agent(skc8,A,B) ),
inference(resolve,[status(thm)],[c_320,c_25]) ).
cnf(c_322,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc12)
| ~ of(skc8,skc14,skc15)
| ~ man(skc8,skc15) ),
inference(resolve,[status(thm)],[c_321,c_13]) ).
cnf(c_323,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc12)
| ~ of(skc8,skc14,skc15) ),
inference(resolve,[status(thm)],[c_322,c_26]) ).
cnf(c_324,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc12) ),
inference(resolve,[status(thm)],[c_323,c_14]) ).
cnf(c_325,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13) ),
inference(resolve,[status(thm)],[c_324,c_12]) ).
cnf(c_326,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13) ),
inference(resolve,[status(thm)],[c_325,c_23]) ).
cnf(c_327,plain,
( man(skc12,skf4(skc12))
| ~ think_believe_consider(skc8,skc13) ),
inference(resolve,[status(thm)],[c_326,c_22]) ).
cnf(c_219,plain,
man(skc12,skf4(skc12)),
inference(resolve,[status(thm)],[c_327,c_21]) ).
cnf(c_328,plain,
( ~ think_believe_consider(skc8,V12)
| ~ present(skc8,V12)
| ~ event(skc8,V12)
| ~ theme(skc8,V12,V7)
| ~ of(skc8,V11,V13)
| ~ man(skc8,V13)
| ~ agent(skc8,V12,V13)
| ~ forename(skc8,V11)
| ~ vincent_forename(skc8,V11)
| ~ of(skc8,V8,V10)
| ~ man(skc8,V10)
| ~ event(V7,V9)
| ~ agent(V7,V9,V10)
| ~ present(V7,V9)
| ~ smoke(V7,V9)
| ~ forename(skc8,V8)
| ~ jules_forename(skc8,V8)
| ~ proposition(skc8,V7)
| ~ accessible_world(skc8,V7)
| ~ of(skc8,V6,F)
| ~ jules_forename(skc8,V6)
| ~ forename(skc8,V6)
| ~ be(skc8,E,F,F)
| ~ man(skc8,F)
| ~ state(skc8,E)
| ~ of(skc8,C,D)
| ~ man(skc8,D)
| ~ agent(skc8,B,D)
| ~ forename(skc8,C)
| ~ vincent_forename(skc8,C)
| ~ theme(skc8,B,skc12)
| ~ event(skc8,B)
| ~ present(skc8,B)
| ~ think_believe_consider(skc8,B)
| ~ event(skc12,A)
| ~ agent(skc12,A,skf4(skc12))
| ~ present(skc12,A)
| ~ smoke(skc12,A)
| ~ accessible_world(skc8,skc12) ),
inference(resolve,[status(thm)],[c_4,c_15]) ).
cnf(c_329,plain,
( ~ think_believe_consider(skc8,V12)
| ~ present(skc8,V12)
| ~ event(skc8,V12)
| ~ theme(skc8,V12,V7)
| ~ of(skc8,V11,V13)
| ~ man(skc8,V13)
| ~ agent(skc8,V12,V13)
| ~ forename(skc8,V11)
| ~ vincent_forename(skc8,V11)
| ~ of(skc8,V8,V10)
| ~ man(skc8,V10)
| ~ event(V7,V9)
| ~ agent(V7,V9,V10)
| ~ present(V7,V9)
| ~ smoke(V7,V9)
| ~ forename(skc8,V8)
| ~ jules_forename(skc8,V8)
| ~ proposition(skc8,V7)
| ~ accessible_world(skc8,V7)
| ~ of(skc8,V6,F)
| ~ jules_forename(skc8,V6)
| ~ forename(skc8,V6)
| ~ be(skc8,E,F,F)
| ~ man(skc8,F)
| ~ state(skc8,E)
| ~ of(skc8,C,D)
| ~ man(skc8,D)
| ~ agent(skc8,B,D)
| ~ forename(skc8,C)
| ~ vincent_forename(skc8,C)
| ~ theme(skc8,B,skc12)
| ~ event(skc8,B)
| ~ present(skc8,B)
| ~ think_believe_consider(skc8,B)
| ~ event(skc12,A)
| ~ agent(skc12,A,skf4(skc12))
| ~ present(skc12,A)
| ~ smoke(skc12,A) ),
inference(resolve,[status(thm)],[c_328,c_16]) ).
cnf(c_330,plain,
( ~ think_believe_consider(skc8,V12)
| ~ present(skc8,V12)
| ~ event(skc8,V12)
| ~ theme(skc8,V12,V7)
| ~ of(skc8,V11,V13)
| ~ man(skc8,V13)
| ~ agent(skc8,V12,V13)
| ~ forename(skc8,V11)
| ~ vincent_forename(skc8,V11)
| ~ of(skc8,V8,V10)
| ~ man(skc8,V10)
| ~ event(V7,V9)
| ~ agent(V7,V9,V10)
| ~ present(V7,V9)
| ~ smoke(V7,V9)
| ~ forename(skc8,V8)
| ~ jules_forename(skc8,V8)
| ~ proposition(skc8,V7)
| ~ accessible_world(skc8,V7)
| ~ of(skc8,V6,F)
| ~ jules_forename(skc8,V6)
| ~ forename(skc8,V6)
| ~ be(skc8,E,F,F)
| ~ man(skc8,F)
| ~ state(skc8,E)
| ~ of(skc8,C,D)
| ~ man(skc8,D)
| ~ agent(skc8,B,D)
| ~ forename(skc8,C)
| ~ vincent_forename(skc8,C)
| ~ theme(skc8,B,skc12)
| ~ event(skc8,B)
| ~ present(skc8,B)
| ~ think_believe_consider(skc8,B)
| ~ event(skc12,skf2(A))
| ~ agent(skc12,skf2(A),skf4(skc12))
| ~ present(skc12,skf2(A)) ),
inference(resolve,[status(thm)],[c_329,c_128]) ).
cnf(c_331,plain,
( ~ think_believe_consider(skc8,V12)
| ~ present(skc8,V12)
| ~ event(skc8,V12)
| ~ theme(skc8,V12,V7)
| ~ of(skc8,V11,V13)
| ~ man(skc8,V13)
| ~ agent(skc8,V12,V13)
| ~ forename(skc8,V11)
| ~ vincent_forename(skc8,V11)
| ~ of(skc8,V8,V10)
| ~ man(skc8,V10)
| ~ event(V7,V9)
| ~ agent(V7,V9,V10)
| ~ present(V7,V9)
| ~ smoke(V7,V9)
| ~ forename(skc8,V8)
| ~ jules_forename(skc8,V8)
| ~ proposition(skc8,V7)
| ~ accessible_world(skc8,V7)
| ~ of(skc8,V6,F)
| ~ jules_forename(skc8,V6)
| ~ forename(skc8,V6)
| ~ be(skc8,E,F,F)
| ~ man(skc8,F)
| ~ state(skc8,E)
| ~ of(skc8,C,D)
| ~ man(skc8,D)
| ~ agent(skc8,B,D)
| ~ forename(skc8,C)
| ~ vincent_forename(skc8,C)
| ~ theme(skc8,B,skc12)
| ~ event(skc8,B)
| ~ present(skc8,B)
| ~ think_believe_consider(skc8,B)
| ~ event(skc12,skf2(A))
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_330,c_129]) ).
cnf(c_332,plain,
( ~ think_believe_consider(skc8,V12)
| ~ present(skc8,V12)
| ~ event(skc8,V12)
| ~ theme(skc8,V12,V7)
| ~ of(skc8,V11,V13)
| ~ man(skc8,V13)
| ~ agent(skc8,V12,V13)
| ~ forename(skc8,V11)
| ~ vincent_forename(skc8,V11)
| ~ of(skc8,V8,V10)
| ~ man(skc8,V10)
| ~ event(V7,V9)
| ~ agent(V7,V9,V10)
| ~ present(V7,V9)
| ~ smoke(V7,V9)
| ~ forename(skc8,V8)
| ~ jules_forename(skc8,V8)
| ~ proposition(skc8,V7)
| ~ accessible_world(skc8,V7)
| ~ of(skc8,V6,F)
| ~ jules_forename(skc8,V6)
| ~ forename(skc8,V6)
| ~ be(skc8,E,F,F)
| ~ man(skc8,F)
| ~ state(skc8,E)
| ~ of(skc8,C,D)
| ~ man(skc8,D)
| ~ agent(skc8,B,D)
| ~ forename(skc8,C)
| ~ vincent_forename(skc8,C)
| ~ theme(skc8,B,skc12)
| ~ event(skc8,B)
| ~ present(skc8,B)
| ~ think_believe_consider(skc8,B)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_331,c_130]) ).
cnf(c_333,plain,
( ~ think_believe_consider(skc8,V11)
| ~ present(skc8,V11)
| ~ event(skc8,V11)
| ~ theme(skc8,V11,V6)
| ~ of(skc8,V10,V12)
| ~ man(skc8,V12)
| ~ agent(skc8,V11,V12)
| ~ forename(skc8,V10)
| ~ vincent_forename(skc8,V10)
| ~ of(skc8,V7,V9)
| ~ man(skc8,V9)
| ~ event(V6,V8)
| ~ agent(V6,V8,V9)
| ~ present(V6,V8)
| ~ smoke(V6,V8)
| ~ forename(skc8,V7)
| ~ jules_forename(skc8,V7)
| ~ proposition(skc8,V6)
| ~ accessible_world(skc8,V6)
| ~ of(skc8,F,E)
| ~ jules_forename(skc8,F)
| ~ forename(skc8,F)
| ~ be(skc8,D,E,E)
| ~ man(skc8,E)
| ~ state(skc8,D)
| ~ of(skc8,B,C)
| ~ man(skc8,C)
| ~ agent(skc8,skc13,C)
| ~ forename(skc8,B)
| ~ vincent_forename(skc8,B)
| ~ theme(skc8,skc13,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_332,c_21]) ).
cnf(c_334,plain,
( ~ think_believe_consider(skc8,V11)
| ~ present(skc8,V11)
| ~ event(skc8,V11)
| ~ theme(skc8,V11,V6)
| ~ of(skc8,V10,V12)
| ~ man(skc8,V12)
| ~ agent(skc8,V11,V12)
| ~ forename(skc8,V10)
| ~ vincent_forename(skc8,V10)
| ~ of(skc8,V7,V9)
| ~ man(skc8,V9)
| ~ event(V6,V8)
| ~ agent(V6,V8,V9)
| ~ present(V6,V8)
| ~ smoke(V6,V8)
| ~ forename(skc8,V7)
| ~ jules_forename(skc8,V7)
| ~ proposition(skc8,V6)
| ~ accessible_world(skc8,V6)
| ~ of(skc8,F,E)
| ~ jules_forename(skc8,F)
| ~ forename(skc8,F)
| ~ be(skc8,D,E,E)
| ~ man(skc8,E)
| ~ state(skc8,D)
| ~ of(skc8,B,C)
| ~ man(skc8,C)
| ~ agent(skc8,skc13,C)
| ~ forename(skc8,B)
| ~ vincent_forename(skc8,B)
| ~ theme(skc8,skc13,skc12)
| ~ event(skc8,skc13)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_333,c_22]) ).
cnf(c_335,plain,
( ~ think_believe_consider(skc8,V11)
| ~ present(skc8,V11)
| ~ event(skc8,V11)
| ~ theme(skc8,V11,V6)
| ~ of(skc8,V10,V12)
| ~ man(skc8,V12)
| ~ agent(skc8,V11,V12)
| ~ forename(skc8,V10)
| ~ vincent_forename(skc8,V10)
| ~ of(skc8,V7,V9)
| ~ man(skc8,V9)
| ~ event(V6,V8)
| ~ agent(V6,V8,V9)
| ~ present(V6,V8)
| ~ smoke(V6,V8)
| ~ forename(skc8,V7)
| ~ jules_forename(skc8,V7)
| ~ proposition(skc8,V6)
| ~ accessible_world(skc8,V6)
| ~ of(skc8,F,E)
| ~ jules_forename(skc8,F)
| ~ forename(skc8,F)
| ~ be(skc8,D,E,E)
| ~ man(skc8,E)
| ~ state(skc8,D)
| ~ of(skc8,B,C)
| ~ man(skc8,C)
| ~ agent(skc8,skc13,C)
| ~ forename(skc8,B)
| ~ vincent_forename(skc8,B)
| ~ theme(skc8,skc13,skc12)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_334,c_23]) ).
cnf(c_336,plain,
( ~ think_believe_consider(skc8,V11)
| ~ present(skc8,V11)
| ~ event(skc8,V11)
| ~ theme(skc8,V11,V6)
| ~ of(skc8,V10,V12)
| ~ man(skc8,V12)
| ~ agent(skc8,V11,V12)
| ~ forename(skc8,V10)
| ~ vincent_forename(skc8,V10)
| ~ of(skc8,V7,V9)
| ~ man(skc8,V9)
| ~ event(V6,V8)
| ~ agent(V6,V8,V9)
| ~ present(V6,V8)
| ~ smoke(V6,V8)
| ~ forename(skc8,V7)
| ~ jules_forename(skc8,V7)
| ~ proposition(skc8,V6)
| ~ accessible_world(skc8,V6)
| ~ of(skc8,F,E)
| ~ jules_forename(skc8,F)
| ~ forename(skc8,F)
| ~ be(skc8,D,E,E)
| ~ man(skc8,E)
| ~ state(skc8,D)
| ~ of(skc8,B,C)
| ~ man(skc8,C)
| ~ agent(skc8,skc13,C)
| ~ forename(skc8,B)
| ~ vincent_forename(skc8,B)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_335,c_12]) ).
cnf(c_337,plain,
( ~ think_believe_consider(skc8,V10)
| ~ present(skc8,V10)
| ~ event(skc8,V10)
| ~ theme(skc8,V10,F)
| ~ of(skc8,V9,V11)
| ~ man(skc8,V11)
| ~ agent(skc8,V10,V11)
| ~ forename(skc8,V9)
| ~ vincent_forename(skc8,V9)
| ~ of(skc8,V6,V8)
| ~ man(skc8,V8)
| ~ event(F,V7)
| ~ agent(F,V7,V8)
| ~ present(F,V7)
| ~ smoke(F,V7)
| ~ forename(skc8,V6)
| ~ jules_forename(skc8,V6)
| ~ proposition(skc8,F)
| ~ accessible_world(skc8,F)
| ~ of(skc8,E,D)
| ~ jules_forename(skc8,E)
| ~ forename(skc8,E)
| ~ be(skc8,C,D,D)
| ~ man(skc8,D)
| ~ state(skc8,C)
| ~ of(skc8,skc14,B)
| ~ man(skc8,B)
| ~ agent(skc8,skc13,B)
| ~ forename(skc8,skc14)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_336,c_24]) ).
cnf(c_338,plain,
( ~ think_believe_consider(skc8,V10)
| ~ present(skc8,V10)
| ~ event(skc8,V10)
| ~ theme(skc8,V10,F)
| ~ of(skc8,V9,V11)
| ~ man(skc8,V11)
| ~ agent(skc8,V10,V11)
| ~ forename(skc8,V9)
| ~ vincent_forename(skc8,V9)
| ~ of(skc8,V6,V8)
| ~ man(skc8,V8)
| ~ event(F,V7)
| ~ agent(F,V7,V8)
| ~ present(F,V7)
| ~ smoke(F,V7)
| ~ forename(skc8,V6)
| ~ jules_forename(skc8,V6)
| ~ proposition(skc8,F)
| ~ accessible_world(skc8,F)
| ~ of(skc8,E,D)
| ~ jules_forename(skc8,E)
| ~ forename(skc8,E)
| ~ be(skc8,C,D,D)
| ~ man(skc8,D)
| ~ state(skc8,C)
| ~ of(skc8,skc14,B)
| ~ man(skc8,B)
| ~ agent(skc8,skc13,B)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_337,c_25]) ).
cnf(c_339,plain,
( ~ think_believe_consider(skc8,V9)
| ~ present(skc8,V9)
| ~ event(skc8,V9)
| ~ theme(skc8,V9,E)
| ~ of(skc8,V8,V10)
| ~ man(skc8,V10)
| ~ agent(skc8,V9,V10)
| ~ forename(skc8,V8)
| ~ vincent_forename(skc8,V8)
| ~ of(skc8,F,V7)
| ~ man(skc8,V7)
| ~ event(E,V6)
| ~ agent(E,V6,V7)
| ~ present(E,V6)
| ~ smoke(E,V6)
| ~ forename(skc8,F)
| ~ jules_forename(skc8,F)
| ~ proposition(skc8,E)
| ~ accessible_world(skc8,E)
| ~ of(skc8,D,C)
| ~ jules_forename(skc8,D)
| ~ forename(skc8,D)
| ~ be(skc8,B,C,C)
| ~ man(skc8,C)
| ~ state(skc8,B)
| ~ of(skc8,skc14,skc15)
| ~ man(skc8,skc15)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_338,c_13]) ).
cnf(c_340,plain,
( ~ think_believe_consider(skc8,V9)
| ~ present(skc8,V9)
| ~ event(skc8,V9)
| ~ theme(skc8,V9,E)
| ~ of(skc8,V8,V10)
| ~ man(skc8,V10)
| ~ agent(skc8,V9,V10)
| ~ forename(skc8,V8)
| ~ vincent_forename(skc8,V8)
| ~ of(skc8,F,V7)
| ~ man(skc8,V7)
| ~ event(E,V6)
| ~ agent(E,V6,V7)
| ~ present(E,V6)
| ~ smoke(E,V6)
| ~ forename(skc8,F)
| ~ jules_forename(skc8,F)
| ~ proposition(skc8,E)
| ~ accessible_world(skc8,E)
| ~ of(skc8,D,C)
| ~ jules_forename(skc8,D)
| ~ forename(skc8,D)
| ~ be(skc8,B,C,C)
| ~ man(skc8,C)
| ~ state(skc8,B)
| ~ of(skc8,skc14,skc15)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_339,c_26]) ).
cnf(c_341,plain,
( ~ think_believe_consider(skc8,V9)
| ~ present(skc8,V9)
| ~ event(skc8,V9)
| ~ theme(skc8,V9,E)
| ~ of(skc8,V8,V10)
| ~ man(skc8,V10)
| ~ agent(skc8,V9,V10)
| ~ forename(skc8,V8)
| ~ vincent_forename(skc8,V8)
| ~ of(skc8,F,V7)
| ~ man(skc8,V7)
| ~ event(E,V6)
| ~ agent(E,V6,V7)
| ~ present(E,V6)
| ~ smoke(E,V6)
| ~ forename(skc8,F)
| ~ jules_forename(skc8,F)
| ~ proposition(skc8,E)
| ~ accessible_world(skc8,E)
| ~ of(skc8,D,C)
| ~ jules_forename(skc8,D)
| ~ forename(skc8,D)
| ~ be(skc8,B,C,C)
| ~ man(skc8,C)
| ~ state(skc8,B)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_340,c_14]) ).
cnf(c_342,plain,
( ~ think_believe_consider(skc8,V8)
| ~ present(skc8,V8)
| ~ event(skc8,V8)
| ~ theme(skc8,V8,D)
| ~ of(skc8,V7,V9)
| ~ man(skc8,V9)
| ~ agent(skc8,V8,V9)
| ~ forename(skc8,V7)
| ~ vincent_forename(skc8,V7)
| ~ of(skc8,E,V6)
| ~ man(skc8,V6)
| ~ event(D,F)
| ~ agent(D,F,V6)
| ~ present(D,F)
| ~ smoke(D,F)
| ~ forename(skc8,E)
| ~ jules_forename(skc8,E)
| ~ proposition(skc8,D)
| ~ accessible_world(skc8,D)
| ~ of(skc8,C,B)
| ~ jules_forename(skc8,C)
| ~ forename(skc8,C)
| ~ be(skc8,skc9,B,B)
| ~ man(skc8,B)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_341,c_17]) ).
cnf(c_343,plain,
( ~ think_believe_consider(skc8,V7)
| ~ present(skc8,V7)
| ~ event(skc8,V7)
| ~ theme(skc8,V7,C)
| ~ of(skc8,V6,V8)
| ~ man(skc8,V8)
| ~ agent(skc8,V7,V8)
| ~ forename(skc8,V6)
| ~ vincent_forename(skc8,V6)
| ~ of(skc8,D,F)
| ~ man(skc8,F)
| ~ event(C,E)
| ~ agent(C,E,F)
| ~ present(C,E)
| ~ smoke(C,E)
| ~ forename(skc8,D)
| ~ jules_forename(skc8,D)
| ~ proposition(skc8,C)
| ~ accessible_world(skc8,C)
| ~ of(skc8,B,skc10)
| ~ jules_forename(skc8,B)
| ~ forename(skc8,B)
| ~ be(skc8,skc9,skc10,skc10)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_342,c_18]) ).
cnf(c_344,plain,
( ~ think_believe_consider(skc8,V7)
| ~ present(skc8,V7)
| ~ event(skc8,V7)
| ~ theme(skc8,V7,C)
| ~ of(skc8,V6,V8)
| ~ man(skc8,V8)
| ~ agent(skc8,V7,V8)
| ~ forename(skc8,V6)
| ~ vincent_forename(skc8,V6)
| ~ of(skc8,D,F)
| ~ man(skc8,F)
| ~ event(C,E)
| ~ agent(C,E,F)
| ~ present(C,E)
| ~ smoke(C,E)
| ~ forename(skc8,D)
| ~ jules_forename(skc8,D)
| ~ proposition(skc8,C)
| ~ accessible_world(skc8,C)
| ~ of(skc8,B,skc10)
| ~ jules_forename(skc8,B)
| ~ forename(skc8,B)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_343,c_10]) ).
cnf(c_345,plain,
( ~ think_believe_consider(skc8,V6)
| ~ present(skc8,V6)
| ~ event(skc8,V6)
| ~ theme(skc8,V6,B)
| ~ of(skc8,F,V7)
| ~ man(skc8,V7)
| ~ agent(skc8,V6,V7)
| ~ forename(skc8,F)
| ~ vincent_forename(skc8,F)
| ~ of(skc8,C,E)
| ~ man(skc8,E)
| ~ event(B,D)
| ~ agent(B,D,E)
| ~ present(B,D)
| ~ smoke(B,D)
| ~ forename(skc8,C)
| ~ jules_forename(skc8,C)
| ~ proposition(skc8,B)
| ~ accessible_world(skc8,B)
| ~ of(skc8,skc11,skc10)
| ~ jules_forename(skc8,skc11)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_344,c_19]) ).
cnf(c_346,plain,
( ~ think_believe_consider(skc8,V6)
| ~ present(skc8,V6)
| ~ event(skc8,V6)
| ~ theme(skc8,V6,B)
| ~ of(skc8,F,V7)
| ~ man(skc8,V7)
| ~ agent(skc8,V6,V7)
| ~ forename(skc8,F)
| ~ vincent_forename(skc8,F)
| ~ of(skc8,C,E)
| ~ man(skc8,E)
| ~ event(B,D)
| ~ agent(B,D,E)
| ~ present(B,D)
| ~ smoke(B,D)
| ~ forename(skc8,C)
| ~ jules_forename(skc8,C)
| ~ proposition(skc8,B)
| ~ accessible_world(skc8,B)
| ~ of(skc8,skc11,skc10)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_345,c_20]) ).
cnf(c_347,plain,
( ~ think_believe_consider(skc8,V6)
| ~ present(skc8,V6)
| ~ event(skc8,V6)
| ~ theme(skc8,V6,B)
| ~ of(skc8,F,V7)
| ~ man(skc8,V7)
| ~ agent(skc8,V6,V7)
| ~ forename(skc8,F)
| ~ vincent_forename(skc8,F)
| ~ of(skc8,C,E)
| ~ man(skc8,E)
| ~ event(B,D)
| ~ agent(B,D,E)
| ~ present(B,D)
| ~ smoke(B,D)
| ~ forename(skc8,C)
| ~ jules_forename(skc8,C)
| ~ proposition(skc8,B)
| ~ accessible_world(skc8,B)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_346,c_11]) ).
cnf(c_348,plain,
( ~ think_believe_consider(skc8,F)
| ~ present(skc8,F)
| ~ event(skc8,F)
| ~ theme(skc8,F,skc12)
| ~ of(skc8,E,V6)
| ~ man(skc8,V6)
| ~ agent(skc8,F,V6)
| ~ forename(skc8,E)
| ~ vincent_forename(skc8,E)
| ~ of(skc8,B,D)
| ~ man(skc8,D)
| ~ event(skc12,C)
| ~ agent(skc12,C,D)
| ~ present(skc12,C)
| ~ smoke(skc12,C)
| ~ forename(skc8,B)
| ~ jules_forename(skc8,B)
| ~ proposition(skc8,skc12)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_347,c_16]) ).
cnf(c_349,plain,
( ~ think_believe_consider(skc8,F)
| ~ present(skc8,F)
| ~ event(skc8,F)
| ~ theme(skc8,F,skc12)
| ~ of(skc8,E,V6)
| ~ man(skc8,V6)
| ~ agent(skc8,F,V6)
| ~ forename(skc8,E)
| ~ vincent_forename(skc8,E)
| ~ of(skc8,B,D)
| ~ man(skc8,D)
| ~ event(skc12,C)
| ~ agent(skc12,C,D)
| ~ present(skc12,C)
| ~ smoke(skc12,C)
| ~ forename(skc8,B)
| ~ jules_forename(skc8,B)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_348,c_15]) ).
cnf(c_350,plain,
( ~ think_believe_consider(skc8,E)
| ~ present(skc8,E)
| ~ event(skc8,E)
| ~ theme(skc8,E,skc12)
| ~ of(skc8,D,F)
| ~ man(skc8,F)
| ~ agent(skc8,E,F)
| ~ forename(skc8,D)
| ~ vincent_forename(skc8,D)
| ~ of(skc8,skc11,C)
| ~ man(skc8,C)
| ~ event(skc12,B)
| ~ agent(skc12,B,C)
| ~ present(skc12,B)
| ~ smoke(skc12,B)
| ~ forename(skc8,skc11)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_349,c_20]) ).
cnf(c_351,plain,
( ~ think_believe_consider(skc8,E)
| ~ present(skc8,E)
| ~ event(skc8,E)
| ~ theme(skc8,E,skc12)
| ~ of(skc8,D,F)
| ~ man(skc8,F)
| ~ agent(skc8,E,F)
| ~ forename(skc8,D)
| ~ vincent_forename(skc8,D)
| ~ of(skc8,skc11,C)
| ~ man(skc8,C)
| ~ event(skc12,B)
| ~ agent(skc12,B,C)
| ~ present(skc12,B)
| ~ smoke(skc12,B)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_350,c_19]) ).
cnf(c_352,plain,
( ~ think_believe_consider(skc8,E)
| ~ present(skc8,E)
| ~ event(skc8,E)
| ~ theme(skc8,E,skc12)
| ~ of(skc8,D,F)
| ~ man(skc8,F)
| ~ agent(skc8,E,F)
| ~ forename(skc8,D)
| ~ vincent_forename(skc8,D)
| ~ of(skc8,skc11,C)
| ~ man(skc8,C)
| ~ event(skc12,skf2(B))
| ~ agent(skc12,skf2(B),C)
| ~ present(skc12,skf2(B))
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_351,c_128]) ).
cnf(c_353,plain,
( ~ think_believe_consider(skc8,E)
| ~ present(skc8,E)
| ~ event(skc8,E)
| ~ theme(skc8,E,skc12)
| ~ of(skc8,D,F)
| ~ man(skc8,F)
| ~ agent(skc8,E,F)
| ~ forename(skc8,D)
| ~ vincent_forename(skc8,D)
| ~ of(skc8,skc11,C)
| ~ man(skc8,C)
| ~ event(skc12,skf2(B))
| ~ agent(skc12,skf2(B),C)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_352,c_129]) ).
cnf(c_354,plain,
( ~ think_believe_consider(skc8,C)
| ~ present(skc8,C)
| ~ event(skc8,C)
| ~ theme(skc8,C,skc12)
| ~ of(skc8,B,D)
| ~ man(skc8,D)
| ~ agent(skc8,C,D)
| ~ forename(skc8,B)
| ~ vincent_forename(skc8,B)
| ~ of(skc8,skc11,skc10)
| ~ man(skc8,skc10)
| ~ event(skc12,skf2(skc10))
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_353,c_134]) ).
cnf(c_355,plain,
( ~ think_believe_consider(skc8,C)
| ~ present(skc8,C)
| ~ event(skc8,C)
| ~ theme(skc8,C,skc12)
| ~ of(skc8,B,D)
| ~ man(skc8,D)
| ~ agent(skc8,C,D)
| ~ forename(skc8,B)
| ~ vincent_forename(skc8,B)
| ~ of(skc8,skc11,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_354,c_130]) ).
cnf(c_356,plain,
( ~ think_believe_consider(skc8,C)
| ~ present(skc8,C)
| ~ event(skc8,C)
| ~ theme(skc8,C,skc12)
| ~ of(skc8,B,D)
| ~ man(skc8,D)
| ~ agent(skc8,C,D)
| ~ forename(skc8,B)
| ~ vincent_forename(skc8,B)
| ~ of(skc8,skc11,skc10)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_355,c_18]) ).
cnf(c_357,plain,
( ~ think_believe_consider(skc8,C)
| ~ present(skc8,C)
| ~ event(skc8,C)
| ~ theme(skc8,C,skc12)
| ~ of(skc8,B,D)
| ~ man(skc8,D)
| ~ agent(skc8,C,D)
| ~ forename(skc8,B)
| ~ vincent_forename(skc8,B)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_356,c_11]) ).
cnf(c_358,plain,
( ~ think_believe_consider(skc8,B)
| ~ present(skc8,B)
| ~ event(skc8,B)
| ~ theme(skc8,B,skc12)
| ~ of(skc8,skc14,C)
| ~ man(skc8,C)
| ~ agent(skc8,B,C)
| ~ forename(skc8,skc14)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_357,c_24]) ).
cnf(c_359,plain,
( ~ think_believe_consider(skc8,B)
| ~ present(skc8,B)
| ~ event(skc8,B)
| ~ theme(skc8,B,skc12)
| ~ of(skc8,skc14,C)
| ~ man(skc8,C)
| ~ agent(skc8,B,C)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_358,c_25]) ).
cnf(c_360,plain,
( ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc12)
| ~ of(skc8,skc14,skc15)
| ~ man(skc8,skc15)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_359,c_13]) ).
cnf(c_361,plain,
( ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc12)
| ~ of(skc8,skc14,skc15)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_360,c_26]) ).
cnf(c_362,plain,
( ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc12)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_361,c_14]) ).
cnf(c_363,plain,
( ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_362,c_12]) ).
cnf(c_364,plain,
( ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_363,c_23]) ).
cnf(c_365,plain,
( ~ think_believe_consider(skc8,skc13)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_364,c_22]) ).
cnf(c_220,plain,
~ agent(skc12,skf2(A),skf4(skc12)),
inference(resolve,[status(thm)],[c_365,c_21]) ).
cnf(c_366,plain,
agent(skc12,skf2(skf4(skc12)),skf4(skc12)),
inference(resolve,[status(thm)],[c_6,c_219]) ).
cnf(c_290,plain,
$false,
inference(resolve,[status(thm)],[c_220,c_366]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % 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.10/5.37 % Computer : n009.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Sat Sep 26 01:46:34 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/5.37 % Process 3100272 was started by sandbox2 on n009,
% 0.10/5.37 % Sat Sep 26 01:46:34 2026
% 0.10/5.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/5.38
% 0.10/5.38 % From the command line: assign(max_seconds, 300).
% 0.15/5.44
% 0.15/5.44 % SZS status Unsatisfiable for theBenchmark
% 0.15/5.44
% 0.15/5.44 % Proof 1 at 0.05 (+ 0.00) seconds.
% 0.15/5.44 % Length of proof is 36.
% 0.15/5.44 % Level of proof is 4.
% 0.15/5.44 % Maximum clause weight is 133.000.
% 0.15/5.44 % Given clauses 232.
% 0.15/5.44
% 0.15/5.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------