%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NLP252-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 : n007.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.10s 0.45s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 25
% Syntax : Number of formulae : 129 ( 46 unt; 0 def)
% Number of atoms : 1439 ( 0 equ)
% Maximal formula atoms : 37 ( 11 avg)
% Number of connectives : 2658 (1348 ~;1310 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 52 ( 12 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 : 500 ( 42 sgn 37 !; 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] :
( man(VAR_1,skf4(VAR_1))
| ~ actual_world(VAR_0)
| ~ of(VAR_0,VAR_11,VAR_12)
| ~ man(VAR_0,VAR_12)
| ~ agent(VAR_0,VAR_10,VAR_12)
| ~ forename(VAR_0,VAR_11)
| ~ vincent_forename(VAR_0,VAR_11)
| ~ theme(VAR_0,VAR_10,VAR_6)
| ~ event(VAR_0,VAR_10)
| ~ present(VAR_0,VAR_10)
| ~ think_believe_consider(VAR_0,VAR_10)
| ~ accessible_world(VAR_0,VAR_6)
| ~ proposition(VAR_0,VAR_6)
| ~ forename(VAR_0,VAR_9)
| ~ jules_forename(VAR_0,VAR_9)
| ~ of(VAR_0,VAR_9,VAR_8)
| ~ man(VAR_0,VAR_8)
| ~ be(VAR_0,VAR_5,VAR_8,VAR_8)
| ~ event(VAR_6,VAR_7)
| ~ agent(VAR_6,VAR_7,VAR_8)
| ~ present(VAR_6,VAR_7)
| ~ smoke(VAR_6,VAR_7)
| ~ state(VAR_0,VAR_5)
| ~ agent(VAR_0,VAR_2,VAR_4)
| ~ man(VAR_0,VAR_4)
| ~ of(VAR_0,VAR_3,VAR_4)
| ~ vincent_forename(VAR_0,VAR_3)
| ~ forename(VAR_0,VAR_3)
| ~ think_believe_consider(VAR_0,VAR_2)
| ~ present(VAR_0,VAR_2)
| ~ event(VAR_0,VAR_2)
| ~ theme(VAR_0,VAR_2,VAR_1)
| ~ proposition(VAR_0,VAR_1)
| ~ accessible_world(VAR_0,VAR_1) ),
file('theBenchmark.p',clause94) ).
cnf(c_1,plain,
( man(B,skf4(B))
| ~ actual_world(A)
| ~ of(A,V11,V12)
| ~ man(A,V12)
| ~ agent(A,V10,V12)
| ~ forename(A,V11)
| ~ vincent_forename(A,V11)
| ~ theme(A,V10,V6)
| ~ event(A,V10)
| ~ present(A,V10)
| ~ think_believe_consider(A,V10)
| ~ accessible_world(A,V6)
| ~ proposition(A,V6)
| ~ forename(A,V9)
| ~ jules_forename(A,V9)
| ~ of(A,V9,V8)
| ~ man(A,V8)
| ~ be(A,F,V8,V8)
| ~ event(V6,V7)
| ~ agent(V6,V7,V8)
| ~ present(V6,V7)
| ~ smoke(V6,V7)
| ~ state(A,F)
| ~ agent(A,C,E)
| ~ man(A,E)
| ~ of(A,D,E)
| ~ vincent_forename(A,D)
| ~ forename(A,D)
| ~ think_believe_consider(A,C)
| ~ present(A,C)
| ~ event(A,C)
| ~ theme(A,C,B)
| ~ proposition(A,B)
| ~ accessible_world(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] :
( ~ actual_world(VAR_2)
| ~ of(VAR_2,VAR_12,VAR_13)
| ~ man(VAR_2,VAR_13)
| ~ agent(VAR_2,VAR_11,VAR_13)
| ~ forename(VAR_2,VAR_12)
| ~ vincent_forename(VAR_2,VAR_12)
| ~ theme(VAR_2,VAR_11,VAR_7)
| ~ event(VAR_2,VAR_11)
| ~ present(VAR_2,VAR_11)
| ~ think_believe_consider(VAR_2,VAR_11)
| ~ accessible_world(VAR_2,VAR_7)
| ~ proposition(VAR_2,VAR_7)
| ~ forename(VAR_2,VAR_10)
| ~ jules_forename(VAR_2,VAR_10)
| ~ of(VAR_2,VAR_10,VAR_9)
| ~ man(VAR_2,VAR_9)
| ~ be(VAR_2,VAR_6,VAR_9,VAR_9)
| ~ event(VAR_7,VAR_8)
| ~ agent(VAR_7,VAR_8,VAR_9)
| ~ present(VAR_7,VAR_8)
| ~ smoke(VAR_7,VAR_8)
| ~ state(VAR_2,VAR_6)
| ~ agent(VAR_2,VAR_3,VAR_5)
| ~ man(VAR_2,VAR_5)
| ~ of(VAR_2,VAR_4,VAR_5)
| ~ vincent_forename(VAR_2,VAR_4)
| ~ forename(VAR_2,VAR_4)
| ~ think_believe_consider(VAR_2,VAR_3)
| ~ present(VAR_2,VAR_3)
| ~ event(VAR_2,VAR_3)
| ~ theme(VAR_2,VAR_3,VAR_0)
| ~ proposition(VAR_2,VAR_0)
| ~ accessible_world(VAR_2,VAR_0)
| ~ event(VAR_0,VAR_1)
| ~ agent(VAR_0,VAR_1,skf4(VAR_0))
| ~ present(VAR_0,VAR_1)
| ~ smoke(VAR_0,VAR_1) ),
file('theBenchmark.p',clause95) ).
cnf(c_3,plain,
( ~ actual_world(C)
| ~ of(C,V12,V13)
| ~ man(C,V13)
| ~ agent(C,V11,V13)
| ~ forename(C,V12)
| ~ vincent_forename(C,V12)
| ~ theme(C,V11,V7)
| ~ event(C,V11)
| ~ present(C,V11)
| ~ think_believe_consider(C,V11)
| ~ accessible_world(C,V7)
| ~ proposition(C,V7)
| ~ forename(C,V10)
| ~ jules_forename(C,V10)
| ~ of(C,V10,V9)
| ~ man(C,V9)
| ~ be(C,V6,V9,V9)
| ~ event(V7,V8)
| ~ agent(V7,V8,V9)
| ~ present(V7,V8)
| ~ smoke(V7,V8)
| ~ state(C,V6)
| ~ agent(C,D,F)
| ~ man(C,F)
| ~ of(C,E,F)
| ~ vincent_forename(C,E)
| ~ forename(C,E)
| ~ think_believe_consider(C,D)
| ~ present(C,D)
| ~ event(C,D)
| ~ theme(C,D,A)
| ~ proposition(C,A)
| ~ accessible_world(C,A)
| ~ event(A,B)
| ~ agent(A,B,skf4(A))
| ~ present(A,B)
| ~ smoke(A,B) ),
inference(clausify,[status(thm)],[clause95]) ).
cnf(c_4,plain,
( ~ of(skc8,V11,V12)
| ~ man(skc8,V12)
| ~ agent(skc8,V10,V12)
| ~ forename(skc8,V11)
| ~ vincent_forename(skc8,V11)
| ~ theme(skc8,V10,V6)
| ~ event(skc8,V10)
| ~ present(skc8,V10)
| ~ think_believe_consider(skc8,V10)
| ~ accessible_world(skc8,V6)
| ~ proposition(skc8,V6)
| ~ forename(skc8,V9)
| ~ jules_forename(skc8,V9)
| ~ of(skc8,V9,V8)
| ~ man(skc8,V8)
| ~ be(skc8,F,V8,V8)
| ~ event(V6,V7)
| ~ agent(V6,V7,V8)
| ~ present(V6,V7)
| ~ smoke(V6,V7)
| ~ state(skc8,F)
| ~ agent(skc8,C,E)
| ~ man(skc8,E)
| ~ of(skc8,D,E)
| ~ vincent_forename(skc8,D)
| ~ forename(skc8,D)
| ~ think_believe_consider(skc8,C)
| ~ present(skc8,C)
| ~ event(skc8,C)
| ~ theme(skc8,C,A)
| ~ proposition(skc8,A)
| ~ accessible_world(skc8,A)
| ~ event(A,B)
| ~ agent(A,B,skf4(A))
| ~ present(A,B)
| ~ smoke(A,B) ),
inference(resolve,[status(thm)],[c_3,c_2]) ).
cnf(c_5,plain,
( man(A,skf4(A))
| ~ of(skc8,V10,V11)
| ~ man(skc8,V11)
| ~ agent(skc8,V9,V11)
| ~ forename(skc8,V10)
| ~ vincent_forename(skc8,V10)
| ~ theme(skc8,V9,F)
| ~ event(skc8,V9)
| ~ present(skc8,V9)
| ~ think_believe_consider(skc8,V9)
| ~ accessible_world(skc8,F)
| ~ proposition(skc8,F)
| ~ forename(skc8,V8)
| ~ jules_forename(skc8,V8)
| ~ of(skc8,V8,V7)
| ~ man(skc8,V7)
| ~ be(skc8,E,V7,V7)
| ~ event(F,V6)
| ~ agent(F,V6,V7)
| ~ present(F,V6)
| ~ smoke(F,V6)
| ~ state(skc8,E)
| ~ agent(skc8,B,D)
| ~ man(skc8,D)
| ~ of(skc8,C,D)
| ~ vincent_forename(skc8,C)
| ~ forename(skc8,C)
| ~ think_believe_consider(skc8,B)
| ~ present(skc8,B)
| ~ event(skc8,B)
| ~ theme(skc8,B,A)
| ~ proposition(skc8,A)
| ~ accessible_world(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_282,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_282,c_26]) ).
cnf(c_283,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_283,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_284,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,V9,V10)
| ~ man(skc8,V10)
| ~ agent(skc8,V8,V10)
| ~ forename(skc8,V9)
| ~ vincent_forename(skc8,V9)
| ~ theme(skc8,V8,E)
| ~ event(skc8,V8)
| ~ present(skc8,V8)
| ~ think_believe_consider(skc8,V8)
| ~ accessible_world(skc8,E)
| ~ proposition(skc8,E)
| ~ forename(skc8,V7)
| ~ jules_forename(skc8,V7)
| ~ of(skc8,V7,V6)
| ~ man(skc8,V6)
| ~ be(skc8,D,V6,V6)
| ~ event(E,F)
| ~ agent(E,F,V6)
| ~ present(E,F)
| ~ smoke(E,F)
| ~ state(skc8,D)
| ~ agent(skc8,A,C)
| ~ man(skc8,C)
| ~ of(skc8,B,C)
| ~ vincent_forename(skc8,B)
| ~ forename(skc8,B)
| ~ think_believe_consider(skc8,A)
| ~ present(skc8,A)
| ~ event(skc8,A)
| ~ theme(skc8,A,skc12)
| ~ proposition(skc8,skc12) ),
inference(resolve,[status(thm)],[c_5,c_16]) ).
cnf(c_285,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,V9,V10)
| ~ man(skc8,V10)
| ~ agent(skc8,V8,V10)
| ~ forename(skc8,V9)
| ~ vincent_forename(skc8,V9)
| ~ theme(skc8,V8,E)
| ~ event(skc8,V8)
| ~ present(skc8,V8)
| ~ think_believe_consider(skc8,V8)
| ~ accessible_world(skc8,E)
| ~ proposition(skc8,E)
| ~ forename(skc8,V7)
| ~ jules_forename(skc8,V7)
| ~ of(skc8,V7,V6)
| ~ man(skc8,V6)
| ~ be(skc8,D,V6,V6)
| ~ event(E,F)
| ~ agent(E,F,V6)
| ~ present(E,F)
| ~ smoke(E,F)
| ~ state(skc8,D)
| ~ agent(skc8,A,C)
| ~ man(skc8,C)
| ~ of(skc8,B,C)
| ~ vincent_forename(skc8,B)
| ~ forename(skc8,B)
| ~ think_believe_consider(skc8,A)
| ~ present(skc8,A)
| ~ event(skc8,A)
| ~ theme(skc8,A,skc12) ),
inference(resolve,[status(thm)],[c_284,c_15]) ).
cnf(c_286,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,V8,V9)
| ~ man(skc8,V9)
| ~ agent(skc8,V7,V9)
| ~ forename(skc8,V8)
| ~ vincent_forename(skc8,V8)
| ~ theme(skc8,V7,D)
| ~ event(skc8,V7)
| ~ present(skc8,V7)
| ~ think_believe_consider(skc8,V7)
| ~ accessible_world(skc8,D)
| ~ proposition(skc8,D)
| ~ forename(skc8,V6)
| ~ jules_forename(skc8,V6)
| ~ of(skc8,V6,F)
| ~ man(skc8,F)
| ~ be(skc8,C,F,F)
| ~ event(D,E)
| ~ agent(D,E,F)
| ~ present(D,E)
| ~ smoke(D,E)
| ~ state(skc8,C)
| ~ agent(skc8,skc13,B)
| ~ man(skc8,B)
| ~ of(skc8,A,B)
| ~ vincent_forename(skc8,A)
| ~ forename(skc8,A)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13) ),
inference(resolve,[status(thm)],[c_285,c_12]) ).
cnf(c_287,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,V8,V9)
| ~ man(skc8,V9)
| ~ agent(skc8,V7,V9)
| ~ forename(skc8,V8)
| ~ vincent_forename(skc8,V8)
| ~ theme(skc8,V7,D)
| ~ event(skc8,V7)
| ~ present(skc8,V7)
| ~ think_believe_consider(skc8,V7)
| ~ accessible_world(skc8,D)
| ~ proposition(skc8,D)
| ~ forename(skc8,V6)
| ~ jules_forename(skc8,V6)
| ~ of(skc8,V6,F)
| ~ man(skc8,F)
| ~ be(skc8,C,F,F)
| ~ event(D,E)
| ~ agent(D,E,F)
| ~ present(D,E)
| ~ smoke(D,E)
| ~ state(skc8,C)
| ~ agent(skc8,skc13,B)
| ~ man(skc8,B)
| ~ of(skc8,A,B)
| ~ vincent_forename(skc8,A)
| ~ forename(skc8,A)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13) ),
inference(resolve,[status(thm)],[c_286,c_23]) ).
cnf(c_288,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,V8,V9)
| ~ man(skc8,V9)
| ~ agent(skc8,V7,V9)
| ~ forename(skc8,V8)
| ~ vincent_forename(skc8,V8)
| ~ theme(skc8,V7,D)
| ~ event(skc8,V7)
| ~ present(skc8,V7)
| ~ think_believe_consider(skc8,V7)
| ~ accessible_world(skc8,D)
| ~ proposition(skc8,D)
| ~ forename(skc8,V6)
| ~ jules_forename(skc8,V6)
| ~ of(skc8,V6,F)
| ~ man(skc8,F)
| ~ be(skc8,C,F,F)
| ~ event(D,E)
| ~ agent(D,E,F)
| ~ present(D,E)
| ~ smoke(D,E)
| ~ state(skc8,C)
| ~ agent(skc8,skc13,B)
| ~ man(skc8,B)
| ~ of(skc8,A,B)
| ~ vincent_forename(skc8,A)
| ~ forename(skc8,A)
| ~ think_believe_consider(skc8,skc13) ),
inference(resolve,[status(thm)],[c_287,c_22]) ).
cnf(c_289,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,V8,V9)
| ~ man(skc8,V9)
| ~ agent(skc8,V7,V9)
| ~ forename(skc8,V8)
| ~ vincent_forename(skc8,V8)
| ~ theme(skc8,V7,D)
| ~ event(skc8,V7)
| ~ present(skc8,V7)
| ~ think_believe_consider(skc8,V7)
| ~ accessible_world(skc8,D)
| ~ proposition(skc8,D)
| ~ forename(skc8,V6)
| ~ jules_forename(skc8,V6)
| ~ of(skc8,V6,F)
| ~ man(skc8,F)
| ~ be(skc8,C,F,F)
| ~ event(D,E)
| ~ agent(D,E,F)
| ~ present(D,E)
| ~ smoke(D,E)
| ~ state(skc8,C)
| ~ agent(skc8,skc13,B)
| ~ man(skc8,B)
| ~ of(skc8,A,B)
| ~ vincent_forename(skc8,A)
| ~ forename(skc8,A) ),
inference(resolve,[status(thm)],[c_288,c_21]) ).
cnf(c_290,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,V7,V8)
| ~ man(skc8,V8)
| ~ agent(skc8,V6,V8)
| ~ forename(skc8,V7)
| ~ vincent_forename(skc8,V7)
| ~ theme(skc8,V6,C)
| ~ event(skc8,V6)
| ~ present(skc8,V6)
| ~ think_believe_consider(skc8,V6)
| ~ accessible_world(skc8,C)
| ~ proposition(skc8,C)
| ~ forename(skc8,F)
| ~ jules_forename(skc8,F)
| ~ of(skc8,F,E)
| ~ man(skc8,E)
| ~ be(skc8,B,E,E)
| ~ event(C,D)
| ~ agent(C,D,E)
| ~ present(C,D)
| ~ smoke(C,D)
| ~ state(skc8,B)
| ~ agent(skc8,skc13,A)
| ~ man(skc8,A)
| ~ of(skc8,skc14,A)
| ~ vincent_forename(skc8,skc14) ),
inference(resolve,[status(thm)],[c_289,c_25]) ).
cnf(c_291,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,V7,V8)
| ~ man(skc8,V8)
| ~ agent(skc8,V6,V8)
| ~ forename(skc8,V7)
| ~ vincent_forename(skc8,V7)
| ~ theme(skc8,V6,C)
| ~ event(skc8,V6)
| ~ present(skc8,V6)
| ~ think_believe_consider(skc8,V6)
| ~ accessible_world(skc8,C)
| ~ proposition(skc8,C)
| ~ forename(skc8,F)
| ~ jules_forename(skc8,F)
| ~ of(skc8,F,E)
| ~ man(skc8,E)
| ~ be(skc8,B,E,E)
| ~ event(C,D)
| ~ agent(C,D,E)
| ~ present(C,D)
| ~ smoke(C,D)
| ~ state(skc8,B)
| ~ agent(skc8,skc13,A)
| ~ man(skc8,A)
| ~ of(skc8,skc14,A) ),
inference(resolve,[status(thm)],[c_290,c_24]) ).
cnf(c_292,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,V6,V7)
| ~ man(skc8,V7)
| ~ agent(skc8,F,V7)
| ~ forename(skc8,V6)
| ~ vincent_forename(skc8,V6)
| ~ theme(skc8,F,B)
| ~ event(skc8,F)
| ~ present(skc8,F)
| ~ think_believe_consider(skc8,F)
| ~ accessible_world(skc8,B)
| ~ proposition(skc8,B)
| ~ forename(skc8,E)
| ~ jules_forename(skc8,E)
| ~ of(skc8,E,D)
| ~ man(skc8,D)
| ~ be(skc8,A,D,D)
| ~ event(B,C)
| ~ agent(B,C,D)
| ~ present(B,C)
| ~ smoke(B,C)
| ~ state(skc8,A)
| ~ agent(skc8,skc13,skc15)
| ~ man(skc8,skc15) ),
inference(resolve,[status(thm)],[c_291,c_14]) ).
cnf(c_293,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,V6,V7)
| ~ man(skc8,V7)
| ~ agent(skc8,F,V7)
| ~ forename(skc8,V6)
| ~ vincent_forename(skc8,V6)
| ~ theme(skc8,F,B)
| ~ event(skc8,F)
| ~ present(skc8,F)
| ~ think_believe_consider(skc8,F)
| ~ accessible_world(skc8,B)
| ~ proposition(skc8,B)
| ~ forename(skc8,E)
| ~ jules_forename(skc8,E)
| ~ of(skc8,E,D)
| ~ man(skc8,D)
| ~ be(skc8,A,D,D)
| ~ event(B,C)
| ~ agent(B,C,D)
| ~ present(B,C)
| ~ smoke(B,C)
| ~ state(skc8,A)
| ~ agent(skc8,skc13,skc15) ),
inference(resolve,[status(thm)],[c_292,c_26]) ).
cnf(c_294,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,V6,V7)
| ~ man(skc8,V7)
| ~ agent(skc8,F,V7)
| ~ forename(skc8,V6)
| ~ vincent_forename(skc8,V6)
| ~ theme(skc8,F,B)
| ~ event(skc8,F)
| ~ present(skc8,F)
| ~ think_believe_consider(skc8,F)
| ~ accessible_world(skc8,B)
| ~ proposition(skc8,B)
| ~ forename(skc8,E)
| ~ jules_forename(skc8,E)
| ~ of(skc8,E,D)
| ~ man(skc8,D)
| ~ be(skc8,A,D,D)
| ~ event(B,C)
| ~ agent(B,C,D)
| ~ present(B,C)
| ~ smoke(B,C)
| ~ state(skc8,A) ),
inference(resolve,[status(thm)],[c_293,c_13]) ).
cnf(c_295,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,F,V6)
| ~ man(skc8,V6)
| ~ agent(skc8,E,V6)
| ~ forename(skc8,F)
| ~ vincent_forename(skc8,F)
| ~ theme(skc8,E,A)
| ~ event(skc8,E)
| ~ present(skc8,E)
| ~ think_believe_consider(skc8,E)
| ~ accessible_world(skc8,A)
| ~ proposition(skc8,A)
| ~ forename(skc8,D)
| ~ jules_forename(skc8,D)
| ~ of(skc8,D,C)
| ~ man(skc8,C)
| ~ be(skc8,skc9,C,C)
| ~ event(A,B)
| ~ agent(A,B,C)
| ~ present(A,B)
| ~ smoke(A,B) ),
inference(resolve,[status(thm)],[c_294,c_17]) ).
cnf(c_296,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,E,F)
| ~ man(skc8,F)
| ~ agent(skc8,D,F)
| ~ forename(skc8,E)
| ~ vincent_forename(skc8,E)
| ~ theme(skc8,D,skc12)
| ~ event(skc8,D)
| ~ present(skc8,D)
| ~ think_believe_consider(skc8,D)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ forename(skc8,C)
| ~ jules_forename(skc8,C)
| ~ of(skc8,C,B)
| ~ man(skc8,B)
| ~ be(skc8,skc9,B,B)
| ~ event(skc12,skf2(A))
| ~ agent(skc12,skf2(A),B)
| ~ present(skc12,skf2(A)) ),
inference(resolve,[status(thm)],[c_295,c_128]) ).
cnf(c_297,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,E,F)
| ~ man(skc8,F)
| ~ agent(skc8,D,F)
| ~ forename(skc8,E)
| ~ vincent_forename(skc8,E)
| ~ theme(skc8,D,skc12)
| ~ event(skc8,D)
| ~ present(skc8,D)
| ~ think_believe_consider(skc8,D)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ forename(skc8,C)
| ~ jules_forename(skc8,C)
| ~ of(skc8,C,B)
| ~ man(skc8,B)
| ~ be(skc8,skc9,B,B)
| ~ event(skc12,skf2(A))
| ~ agent(skc12,skf2(A),B) ),
inference(resolve,[status(thm)],[c_296,c_129]) ).
cnf(c_298,plain,
( man(skc12,skf4(skc12))
| ~ 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)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ forename(skc8,A)
| ~ jules_forename(skc8,A)
| ~ of(skc8,A,skc10)
| ~ man(skc8,skc10)
| ~ be(skc8,skc9,skc10,skc10)
| ~ event(skc12,skf2(skc10)) ),
inference(resolve,[status(thm)],[c_297,c_134]) ).
cnf(c_299,plain,
( man(skc12,skf4(skc12))
| ~ 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)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ forename(skc8,A)
| ~ jules_forename(skc8,A)
| ~ of(skc8,A,skc10)
| ~ man(skc8,skc10)
| ~ be(skc8,skc9,skc10,skc10) ),
inference(resolve,[status(thm)],[c_298,c_130]) ).
cnf(c_300,plain,
( man(skc12,skf4(skc12))
| ~ 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)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ forename(skc8,A)
| ~ jules_forename(skc8,A)
| ~ of(skc8,A,skc10)
| ~ man(skc8,skc10) ),
inference(resolve,[status(thm)],[c_299,c_10]) ).
cnf(c_301,plain,
( man(skc12,skf4(skc12))
| ~ 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)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ forename(skc8,A)
| ~ jules_forename(skc8,A)
| ~ of(skc8,A,skc10) ),
inference(resolve,[status(thm)],[c_300,c_18]) ).
cnf(c_302,plain,
( man(skc12,skf4(skc12))
| ~ 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)
| ~ proposition(skc8,skc12)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11) ),
inference(resolve,[status(thm)],[c_301,c_11]) ).
cnf(c_303,plain,
( man(skc12,skf4(skc12))
| ~ 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)
| ~ proposition(skc8,skc12)
| ~ forename(skc8,skc11) ),
inference(resolve,[status(thm)],[c_302,c_20]) ).
cnf(c_304,plain,
( man(skc12,skf4(skc12))
| ~ 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)
| ~ proposition(skc8,skc12) ),
inference(resolve,[status(thm)],[c_303,c_19]) ).
cnf(c_305,plain,
( man(skc12,skf4(skc12))
| ~ 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_304,c_15]) ).
cnf(c_306,plain,
( man(skc12,skf4(skc12))
| ~ 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_305,c_16]) ).
cnf(c_307,plain,
( man(skc12,skf4(skc12))
| ~ 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_306,c_21]) ).
cnf(c_308,plain,
( man(skc12,skf4(skc12))
| ~ 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_307,c_22]) ).
cnf(c_309,plain,
( man(skc12,skf4(skc12))
| ~ 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_308,c_23]) ).
cnf(c_310,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,A,B)
| ~ man(skc8,B)
| ~ agent(skc8,skc13,B)
| ~ forename(skc8,A)
| ~ vincent_forename(skc8,A) ),
inference(resolve,[status(thm)],[c_309,c_12]) ).
cnf(c_311,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,skc14,A)
| ~ man(skc8,A)
| ~ agent(skc8,skc13,A)
| ~ forename(skc8,skc14) ),
inference(resolve,[status(thm)],[c_310,c_24]) ).
cnf(c_312,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,skc14,A)
| ~ man(skc8,A)
| ~ agent(skc8,skc13,A) ),
inference(resolve,[status(thm)],[c_311,c_25]) ).
cnf(c_313,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,skc14,skc15)
| ~ man(skc8,skc15) ),
inference(resolve,[status(thm)],[c_312,c_13]) ).
cnf(c_314,plain,
( man(skc12,skf4(skc12))
| ~ of(skc8,skc14,skc15) ),
inference(resolve,[status(thm)],[c_313,c_26]) ).
cnf(c_206,plain,
man(skc12,skf4(skc12)),
inference(resolve,[status(thm)],[c_314,c_14]) ).
cnf(c_315,plain,
( ~ of(skc8,V10,V11)
| ~ man(skc8,V11)
| ~ agent(skc8,V9,V11)
| ~ forename(skc8,V10)
| ~ vincent_forename(skc8,V10)
| ~ theme(skc8,V9,F)
| ~ event(skc8,V9)
| ~ present(skc8,V9)
| ~ think_believe_consider(skc8,V9)
| ~ accessible_world(skc8,F)
| ~ proposition(skc8,F)
| ~ forename(skc8,V8)
| ~ jules_forename(skc8,V8)
| ~ of(skc8,V8,V7)
| ~ man(skc8,V7)
| ~ be(skc8,E,V7,V7)
| ~ event(F,V6)
| ~ agent(F,V6,V7)
| ~ present(F,V6)
| ~ smoke(F,V6)
| ~ state(skc8,E)
| ~ agent(skc8,B,D)
| ~ man(skc8,D)
| ~ of(skc8,C,D)
| ~ vincent_forename(skc8,C)
| ~ forename(skc8,C)
| ~ think_believe_consider(skc8,B)
| ~ present(skc8,B)
| ~ event(skc8,B)
| ~ theme(skc8,B,skc12)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc12,skf2(A))
| ~ agent(skc12,skf2(A),skf4(skc12))
| ~ present(skc12,skf2(A)) ),
inference(resolve,[status(thm)],[c_4,c_128]) ).
cnf(c_316,plain,
( ~ of(skc8,V10,V11)
| ~ man(skc8,V11)
| ~ agent(skc8,V9,V11)
| ~ forename(skc8,V10)
| ~ vincent_forename(skc8,V10)
| ~ theme(skc8,V9,F)
| ~ event(skc8,V9)
| ~ present(skc8,V9)
| ~ think_believe_consider(skc8,V9)
| ~ accessible_world(skc8,F)
| ~ proposition(skc8,F)
| ~ forename(skc8,V8)
| ~ jules_forename(skc8,V8)
| ~ of(skc8,V8,V7)
| ~ man(skc8,V7)
| ~ be(skc8,E,V7,V7)
| ~ event(F,V6)
| ~ agent(F,V6,V7)
| ~ present(F,V6)
| ~ smoke(F,V6)
| ~ state(skc8,E)
| ~ agent(skc8,B,D)
| ~ man(skc8,D)
| ~ of(skc8,C,D)
| ~ vincent_forename(skc8,C)
| ~ forename(skc8,C)
| ~ think_believe_consider(skc8,B)
| ~ present(skc8,B)
| ~ event(skc8,B)
| ~ theme(skc8,B,skc12)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc12,skf2(A))
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_315,c_129]) ).
cnf(c_317,plain,
( ~ of(skc8,V10,V11)
| ~ man(skc8,V11)
| ~ agent(skc8,V9,V11)
| ~ forename(skc8,V10)
| ~ vincent_forename(skc8,V10)
| ~ theme(skc8,V9,F)
| ~ event(skc8,V9)
| ~ present(skc8,V9)
| ~ think_believe_consider(skc8,V9)
| ~ accessible_world(skc8,F)
| ~ proposition(skc8,F)
| ~ forename(skc8,V8)
| ~ jules_forename(skc8,V8)
| ~ of(skc8,V8,V7)
| ~ man(skc8,V7)
| ~ be(skc8,E,V7,V7)
| ~ event(F,V6)
| ~ agent(F,V6,V7)
| ~ present(F,V6)
| ~ smoke(F,V6)
| ~ state(skc8,E)
| ~ agent(skc8,B,D)
| ~ man(skc8,D)
| ~ of(skc8,C,D)
| ~ vincent_forename(skc8,C)
| ~ forename(skc8,C)
| ~ think_believe_consider(skc8,B)
| ~ present(skc8,B)
| ~ event(skc8,B)
| ~ theme(skc8,B,skc12)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_316,c_130]) ).
cnf(c_318,plain,
( ~ of(skc8,V10,V11)
| ~ man(skc8,V11)
| ~ agent(skc8,V9,V11)
| ~ forename(skc8,V10)
| ~ vincent_forename(skc8,V10)
| ~ theme(skc8,V9,F)
| ~ event(skc8,V9)
| ~ present(skc8,V9)
| ~ think_believe_consider(skc8,V9)
| ~ accessible_world(skc8,F)
| ~ proposition(skc8,F)
| ~ forename(skc8,V8)
| ~ jules_forename(skc8,V8)
| ~ of(skc8,V8,V7)
| ~ man(skc8,V7)
| ~ be(skc8,E,V7,V7)
| ~ event(F,V6)
| ~ agent(F,V6,V7)
| ~ present(F,V6)
| ~ smoke(F,V6)
| ~ state(skc8,E)
| ~ agent(skc8,B,D)
| ~ man(skc8,D)
| ~ of(skc8,C,D)
| ~ vincent_forename(skc8,C)
| ~ forename(skc8,C)
| ~ think_believe_consider(skc8,B)
| ~ present(skc8,B)
| ~ event(skc8,B)
| ~ theme(skc8,B,skc12)
| ~ proposition(skc8,skc12)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_317,c_16]) ).
cnf(c_319,plain,
( ~ of(skc8,V10,V11)
| ~ man(skc8,V11)
| ~ agent(skc8,V9,V11)
| ~ forename(skc8,V10)
| ~ vincent_forename(skc8,V10)
| ~ theme(skc8,V9,F)
| ~ event(skc8,V9)
| ~ present(skc8,V9)
| ~ think_believe_consider(skc8,V9)
| ~ accessible_world(skc8,F)
| ~ proposition(skc8,F)
| ~ forename(skc8,V8)
| ~ jules_forename(skc8,V8)
| ~ of(skc8,V8,V7)
| ~ man(skc8,V7)
| ~ be(skc8,E,V7,V7)
| ~ event(F,V6)
| ~ agent(F,V6,V7)
| ~ present(F,V6)
| ~ smoke(F,V6)
| ~ state(skc8,E)
| ~ agent(skc8,B,D)
| ~ man(skc8,D)
| ~ of(skc8,C,D)
| ~ vincent_forename(skc8,C)
| ~ forename(skc8,C)
| ~ think_believe_consider(skc8,B)
| ~ present(skc8,B)
| ~ event(skc8,B)
| ~ theme(skc8,B,skc12)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_318,c_15]) ).
cnf(c_320,plain,
( ~ of(skc8,V9,V10)
| ~ man(skc8,V10)
| ~ agent(skc8,V8,V10)
| ~ forename(skc8,V9)
| ~ vincent_forename(skc8,V9)
| ~ theme(skc8,V8,E)
| ~ event(skc8,V8)
| ~ present(skc8,V8)
| ~ think_believe_consider(skc8,V8)
| ~ accessible_world(skc8,E)
| ~ proposition(skc8,E)
| ~ forename(skc8,V7)
| ~ jules_forename(skc8,V7)
| ~ of(skc8,V7,V6)
| ~ man(skc8,V6)
| ~ be(skc8,D,V6,V6)
| ~ event(E,F)
| ~ agent(E,F,V6)
| ~ present(E,F)
| ~ smoke(E,F)
| ~ state(skc8,D)
| ~ agent(skc8,skc13,C)
| ~ man(skc8,C)
| ~ of(skc8,B,C)
| ~ vincent_forename(skc8,B)
| ~ forename(skc8,B)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_319,c_12]) ).
cnf(c_321,plain,
( ~ of(skc8,V9,V10)
| ~ man(skc8,V10)
| ~ agent(skc8,V8,V10)
| ~ forename(skc8,V9)
| ~ vincent_forename(skc8,V9)
| ~ theme(skc8,V8,E)
| ~ event(skc8,V8)
| ~ present(skc8,V8)
| ~ think_believe_consider(skc8,V8)
| ~ accessible_world(skc8,E)
| ~ proposition(skc8,E)
| ~ forename(skc8,V7)
| ~ jules_forename(skc8,V7)
| ~ of(skc8,V7,V6)
| ~ man(skc8,V6)
| ~ be(skc8,D,V6,V6)
| ~ event(E,F)
| ~ agent(E,F,V6)
| ~ present(E,F)
| ~ smoke(E,F)
| ~ state(skc8,D)
| ~ agent(skc8,skc13,C)
| ~ man(skc8,C)
| ~ of(skc8,B,C)
| ~ vincent_forename(skc8,B)
| ~ forename(skc8,B)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_320,c_23]) ).
cnf(c_322,plain,
( ~ of(skc8,V9,V10)
| ~ man(skc8,V10)
| ~ agent(skc8,V8,V10)
| ~ forename(skc8,V9)
| ~ vincent_forename(skc8,V9)
| ~ theme(skc8,V8,E)
| ~ event(skc8,V8)
| ~ present(skc8,V8)
| ~ think_believe_consider(skc8,V8)
| ~ accessible_world(skc8,E)
| ~ proposition(skc8,E)
| ~ forename(skc8,V7)
| ~ jules_forename(skc8,V7)
| ~ of(skc8,V7,V6)
| ~ man(skc8,V6)
| ~ be(skc8,D,V6,V6)
| ~ event(E,F)
| ~ agent(E,F,V6)
| ~ present(E,F)
| ~ smoke(E,F)
| ~ state(skc8,D)
| ~ agent(skc8,skc13,C)
| ~ man(skc8,C)
| ~ of(skc8,B,C)
| ~ vincent_forename(skc8,B)
| ~ forename(skc8,B)
| ~ think_believe_consider(skc8,skc13)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_321,c_22]) ).
cnf(c_323,plain,
( ~ of(skc8,V9,V10)
| ~ man(skc8,V10)
| ~ agent(skc8,V8,V10)
| ~ forename(skc8,V9)
| ~ vincent_forename(skc8,V9)
| ~ theme(skc8,V8,E)
| ~ event(skc8,V8)
| ~ present(skc8,V8)
| ~ think_believe_consider(skc8,V8)
| ~ accessible_world(skc8,E)
| ~ proposition(skc8,E)
| ~ forename(skc8,V7)
| ~ jules_forename(skc8,V7)
| ~ of(skc8,V7,V6)
| ~ man(skc8,V6)
| ~ be(skc8,D,V6,V6)
| ~ event(E,F)
| ~ agent(E,F,V6)
| ~ present(E,F)
| ~ smoke(E,F)
| ~ state(skc8,D)
| ~ agent(skc8,skc13,C)
| ~ man(skc8,C)
| ~ of(skc8,B,C)
| ~ vincent_forename(skc8,B)
| ~ forename(skc8,B)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_322,c_21]) ).
cnf(c_324,plain,
( ~ of(skc8,V8,V9)
| ~ man(skc8,V9)
| ~ agent(skc8,V7,V9)
| ~ forename(skc8,V8)
| ~ vincent_forename(skc8,V8)
| ~ theme(skc8,V7,D)
| ~ event(skc8,V7)
| ~ present(skc8,V7)
| ~ think_believe_consider(skc8,V7)
| ~ accessible_world(skc8,D)
| ~ proposition(skc8,D)
| ~ forename(skc8,V6)
| ~ jules_forename(skc8,V6)
| ~ of(skc8,V6,F)
| ~ man(skc8,F)
| ~ be(skc8,C,F,F)
| ~ event(D,E)
| ~ agent(D,E,F)
| ~ present(D,E)
| ~ smoke(D,E)
| ~ state(skc8,C)
| ~ agent(skc8,skc13,B)
| ~ man(skc8,B)
| ~ of(skc8,skc14,B)
| ~ vincent_forename(skc8,skc14)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_323,c_25]) ).
cnf(c_325,plain,
( ~ of(skc8,V8,V9)
| ~ man(skc8,V9)
| ~ agent(skc8,V7,V9)
| ~ forename(skc8,V8)
| ~ vincent_forename(skc8,V8)
| ~ theme(skc8,V7,D)
| ~ event(skc8,V7)
| ~ present(skc8,V7)
| ~ think_believe_consider(skc8,V7)
| ~ accessible_world(skc8,D)
| ~ proposition(skc8,D)
| ~ forename(skc8,V6)
| ~ jules_forename(skc8,V6)
| ~ of(skc8,V6,F)
| ~ man(skc8,F)
| ~ be(skc8,C,F,F)
| ~ event(D,E)
| ~ agent(D,E,F)
| ~ present(D,E)
| ~ smoke(D,E)
| ~ state(skc8,C)
| ~ agent(skc8,skc13,B)
| ~ man(skc8,B)
| ~ of(skc8,skc14,B)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_324,c_24]) ).
cnf(c_326,plain,
( ~ of(skc8,V7,V8)
| ~ man(skc8,V8)
| ~ agent(skc8,V6,V8)
| ~ forename(skc8,V7)
| ~ vincent_forename(skc8,V7)
| ~ theme(skc8,V6,C)
| ~ event(skc8,V6)
| ~ present(skc8,V6)
| ~ think_believe_consider(skc8,V6)
| ~ accessible_world(skc8,C)
| ~ proposition(skc8,C)
| ~ forename(skc8,F)
| ~ jules_forename(skc8,F)
| ~ of(skc8,F,E)
| ~ man(skc8,E)
| ~ be(skc8,B,E,E)
| ~ event(C,D)
| ~ agent(C,D,E)
| ~ present(C,D)
| ~ smoke(C,D)
| ~ state(skc8,B)
| ~ agent(skc8,skc13,skc15)
| ~ man(skc8,skc15)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_325,c_14]) ).
cnf(c_327,plain,
( ~ of(skc8,V7,V8)
| ~ man(skc8,V8)
| ~ agent(skc8,V6,V8)
| ~ forename(skc8,V7)
| ~ vincent_forename(skc8,V7)
| ~ theme(skc8,V6,C)
| ~ event(skc8,V6)
| ~ present(skc8,V6)
| ~ think_believe_consider(skc8,V6)
| ~ accessible_world(skc8,C)
| ~ proposition(skc8,C)
| ~ forename(skc8,F)
| ~ jules_forename(skc8,F)
| ~ of(skc8,F,E)
| ~ man(skc8,E)
| ~ be(skc8,B,E,E)
| ~ event(C,D)
| ~ agent(C,D,E)
| ~ present(C,D)
| ~ smoke(C,D)
| ~ state(skc8,B)
| ~ agent(skc8,skc13,skc15)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_326,c_26]) ).
cnf(c_328,plain,
( ~ of(skc8,V7,V8)
| ~ man(skc8,V8)
| ~ agent(skc8,V6,V8)
| ~ forename(skc8,V7)
| ~ vincent_forename(skc8,V7)
| ~ theme(skc8,V6,C)
| ~ event(skc8,V6)
| ~ present(skc8,V6)
| ~ think_believe_consider(skc8,V6)
| ~ accessible_world(skc8,C)
| ~ proposition(skc8,C)
| ~ forename(skc8,F)
| ~ jules_forename(skc8,F)
| ~ of(skc8,F,E)
| ~ man(skc8,E)
| ~ be(skc8,B,E,E)
| ~ event(C,D)
| ~ agent(C,D,E)
| ~ present(C,D)
| ~ smoke(C,D)
| ~ state(skc8,B)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_327,c_13]) ).
cnf(c_329,plain,
( ~ of(skc8,V6,V7)
| ~ man(skc8,V7)
| ~ agent(skc8,F,V7)
| ~ forename(skc8,V6)
| ~ vincent_forename(skc8,V6)
| ~ theme(skc8,F,B)
| ~ event(skc8,F)
| ~ present(skc8,F)
| ~ think_believe_consider(skc8,F)
| ~ accessible_world(skc8,B)
| ~ proposition(skc8,B)
| ~ forename(skc8,E)
| ~ jules_forename(skc8,E)
| ~ of(skc8,E,D)
| ~ man(skc8,D)
| ~ be(skc8,skc9,D,D)
| ~ event(B,C)
| ~ agent(B,C,D)
| ~ present(B,C)
| ~ smoke(B,C)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_328,c_17]) ).
cnf(c_330,plain,
( ~ of(skc8,F,V6)
| ~ man(skc8,V6)
| ~ agent(skc8,E,V6)
| ~ forename(skc8,F)
| ~ vincent_forename(skc8,F)
| ~ theme(skc8,E,skc12)
| ~ event(skc8,E)
| ~ present(skc8,E)
| ~ think_believe_consider(skc8,E)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ forename(skc8,D)
| ~ jules_forename(skc8,D)
| ~ of(skc8,D,C)
| ~ man(skc8,C)
| ~ be(skc8,skc9,C,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_329,c_128]) ).
cnf(c_331,plain,
( ~ of(skc8,F,V6)
| ~ man(skc8,V6)
| ~ agent(skc8,E,V6)
| ~ forename(skc8,F)
| ~ vincent_forename(skc8,F)
| ~ theme(skc8,E,skc12)
| ~ event(skc8,E)
| ~ present(skc8,E)
| ~ think_believe_consider(skc8,E)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ forename(skc8,D)
| ~ jules_forename(skc8,D)
| ~ of(skc8,D,C)
| ~ man(skc8,C)
| ~ be(skc8,skc9,C,C)
| ~ event(skc12,skf2(B))
| ~ agent(skc12,skf2(B),C)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_330,c_129]) ).
cnf(c_332,plain,
( ~ of(skc8,D,E)
| ~ man(skc8,E)
| ~ agent(skc8,C,E)
| ~ forename(skc8,D)
| ~ vincent_forename(skc8,D)
| ~ theme(skc8,C,skc12)
| ~ event(skc8,C)
| ~ present(skc8,C)
| ~ think_believe_consider(skc8,C)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ forename(skc8,B)
| ~ jules_forename(skc8,B)
| ~ of(skc8,B,skc10)
| ~ man(skc8,skc10)
| ~ be(skc8,skc9,skc10,skc10)
| ~ event(skc12,skf2(skc10))
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_331,c_134]) ).
cnf(c_333,plain,
( ~ of(skc8,D,E)
| ~ man(skc8,E)
| ~ agent(skc8,C,E)
| ~ forename(skc8,D)
| ~ vincent_forename(skc8,D)
| ~ theme(skc8,C,skc12)
| ~ event(skc8,C)
| ~ present(skc8,C)
| ~ think_believe_consider(skc8,C)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ forename(skc8,B)
| ~ jules_forename(skc8,B)
| ~ of(skc8,B,skc10)
| ~ man(skc8,skc10)
| ~ be(skc8,skc9,skc10,skc10)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_332,c_130]) ).
cnf(c_334,plain,
( ~ of(skc8,D,E)
| ~ man(skc8,E)
| ~ agent(skc8,C,E)
| ~ forename(skc8,D)
| ~ vincent_forename(skc8,D)
| ~ theme(skc8,C,skc12)
| ~ event(skc8,C)
| ~ present(skc8,C)
| ~ think_believe_consider(skc8,C)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ forename(skc8,B)
| ~ jules_forename(skc8,B)
| ~ of(skc8,B,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_333,c_10]) ).
cnf(c_335,plain,
( ~ of(skc8,D,E)
| ~ man(skc8,E)
| ~ agent(skc8,C,E)
| ~ forename(skc8,D)
| ~ vincent_forename(skc8,D)
| ~ theme(skc8,C,skc12)
| ~ event(skc8,C)
| ~ present(skc8,C)
| ~ think_believe_consider(skc8,C)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ forename(skc8,B)
| ~ jules_forename(skc8,B)
| ~ of(skc8,B,skc10)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_334,c_18]) ).
cnf(c_336,plain,
( ~ 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)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_335,c_11]) ).
cnf(c_337,plain,
( ~ 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)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ forename(skc8,skc11)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_336,c_20]) ).
cnf(c_338,plain,
( ~ 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)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_337,c_19]) ).
cnf(c_339,plain,
( ~ 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)
| ~ accessible_world(skc8,skc12)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_338,c_15]) ).
cnf(c_340,plain,
( ~ 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_339,c_16]) ).
cnf(c_341,plain,
( ~ 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_340,c_21]) ).
cnf(c_342,plain,
( ~ 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_341,c_22]) ).
cnf(c_343,plain,
( ~ 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_342,c_23]) ).
cnf(c_344,plain,
( ~ 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_343,c_12]) ).
cnf(c_345,plain,
( ~ 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_344,c_24]) ).
cnf(c_346,plain,
( ~ of(skc8,skc14,B)
| ~ man(skc8,B)
| ~ agent(skc8,skc13,B)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_345,c_25]) ).
cnf(c_347,plain,
( ~ of(skc8,skc14,skc15)
| ~ man(skc8,skc15)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_346,c_13]) ).
cnf(c_348,plain,
( ~ of(skc8,skc14,skc15)
| ~ agent(skc12,skf2(A),skf4(skc12)) ),
inference(resolve,[status(thm)],[c_347,c_26]) ).
cnf(c_207,plain,
~ agent(skc12,skf2(A),skf4(skc12)),
inference(resolve,[status(thm)],[c_348,c_14]) ).
cnf(c_349,plain,
agent(skc12,skf2(skf4(skc12)),skf4(skc12)),
inference(resolve,[status(thm)],[c_6,c_206]) ).
cnf(c_281,plain,
$false,
inference(resolve,[status(thm)],[c_207,c_349]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP252-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.10/0.37 % Computer : n007.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 01:44:53 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 2501652 was started by sandbox on n007,
% 0.10/0.37 % Sat Sep 26 01:44:53 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.38
% 0.10/0.38 % From the command line: assign(max_seconds, 300).
% 0.10/0.45
% 0.10/0.45 % SZS status Unsatisfiable for theBenchmark
% 0.10/0.45
% 0.10/0.45 % Proof 1 at 0.06 (+ 0.01) seconds.
% 0.10/0.45 % Length of proof is 36.
% 0.10/0.45 % Level of proof is 4.
% 0.10/0.45 % Maximum clause weight is 130.000.
% 0.10/0.45 % Given clauses 215.
% 0.10/0.45
% 0.10/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------