Vampire---5.0.1.CSA-Sat.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : NLP233+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n016.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 : Tue Sep 29 12:08:04 PM UTC 2026

% Result   : CounterSatisfiable 4.22s 1.24s
% Output   : Saturation 4.86s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u134,negated_conjecture,
    ~ sP6 ).

cnf(u139,negated_conjecture,
    sP5(sK38) ).

cnf(u144,negated_conjecture,
    actual_world(sK38) ).

cnf(u148,negated_conjecture,
    ( ~ be(X0,X10,X9,X9)
    | ~ smoke(X12,X15)
    | ~ present(X12,X15)
    | ~ agent(X12,X15,X2)
    | ~ event(X12,X15)
    | ~ accessible_world(X0,X12)
    | ~ think_believe_consider(X0,X11)
    | ~ present(X0,X11)
    | ~ event(X0,X11)
    | ~ theme(X0,X11,X12)
    | ~ agent(X0,X11,X2)
    | ~ proposition(X0,X12)
    | ~ actual_world(X0)
    | ~ state(X0,X10)
    | ~ forename(X0,X8)
    | ~ jules_forename(X0,X8)
    | ~ man(X0,X9)
    | ~ of(X0,X8,X9)
    | man(X7,sK37(X7))
    | ~ accessible_world(X0,X7)
    | ~ think_believe_consider(X0,X6)
    | ~ present(X0,X6)
    | ~ event(X0,X6)
    | ~ theme(X0,X6,X7)
    | ~ agent(X0,X6,X4)
    | ~ proposition(X0,X7)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ man(X0,X4)
    | ~ of(X0,X5,X4)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X2)
    | ~ of(X0,X3,X2)
    | ~ forename(X0,X1)
    | ~ jules_forename(X0,X1)
    | ~ of(X0,X1,X2) ) ).

cnf(u152,negated_conjecture,
    ( ~ be(X0,X10,X9,X9)
    | ~ smoke(X12,X15)
    | ~ present(X12,X15)
    | ~ agent(X12,X15,X2)
    | ~ event(X12,X15)
    | ~ accessible_world(X0,X12)
    | ~ think_believe_consider(X0,X11)
    | ~ present(X0,X11)
    | ~ event(X0,X11)
    | ~ theme(X0,X11,X12)
    | ~ agent(X0,X11,X2)
    | ~ proposition(X0,X12)
    | ~ actual_world(X0)
    | ~ state(X0,X10)
    | ~ forename(X0,X8)
    | ~ jules_forename(X0,X8)
    | ~ man(X0,X9)
    | ~ of(X0,X8,X9)
    | ~ smoke(X7,X14)
    | ~ present(X7,X14)
    | ~ agent(X7,X14,sK37(X7))
    | ~ event(X7,X14)
    | ~ accessible_world(X0,X7)
    | ~ think_believe_consider(X0,X6)
    | ~ present(X0,X6)
    | ~ event(X0,X6)
    | ~ theme(X0,X6,X7)
    | ~ agent(X0,X6,X4)
    | ~ proposition(X0,X7)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ man(X0,X4)
    | ~ of(X0,X5,X4)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X2)
    | ~ of(X0,X3,X2)
    | ~ forename(X0,X1)
    | ~ jules_forename(X0,X1)
    | ~ of(X0,X1,X2) ) ).

cnf(u344,negated_conjecture,
    ( ~ of(X0,X1,sK24(X0))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ actual_world(X0)
    | ~ jules_forename(X0,sK25(X0))
    | man(sK34(X0),sK37(sK34(X0)))
    | ~ sP2(X0) ) ).

cnf(u824,negated_conjecture,
    ( ~ agent(X0,sK14(X0),sK12(sK15(X0)))
    | ~ smoke(sK15(X0),sK14(sK15(X0)))
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK12(sK15(X0)))
    | ~ of(X0,X1,sK12(sK15(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(sK15(X0)))
    | ~ sP5(X0)
    | ~ sP5(sK15(X0)) ) ).

cnf(u339,negated_conjecture,
    ( ~ theme(X3,X6,X5)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ accessible_world(X3,X5)
    | ~ think_believe_consider(X3,X6)
    | ~ present(X3,X6)
    | ~ event(X3,X6)
    | ~ agent(X0,X1,X2)
    | ~ agent(X3,X6,X7)
    | ~ proposition(X3,X5)
    | ~ forename(X3,X8)
    | ~ vincent_forename(X3,X8)
    | ~ man(X3,X7)
    | ~ of(X3,X8,X7)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X2)
    | ~ of(X3,X9,X2)
    | ~ forename(X3,X10)
    | ~ jules_forename(X3,X10)
    | ~ of(X3,X10,X2)
    | ~ sP2(X3)
    | ~ sP4(X5) ) ).

cnf(u1310,negated_conjecture,
    ( ~ agent(X0,sK19(X0),sK24(sK20(X0)))
    | ~ actual_world(X0)
    | ~ smoke(sK20(X0),sK33(sK20(X0)))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK24(sK20(X0)))
    | ~ of(X0,X1,sK24(sK20(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK24(sK20(X0)))
    | ~ sP5(X0)
    | ~ sP2(sK20(X0)) ) ).

cnf(u798,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X1)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ man(sK20(X0),X1)
    | ~ sP1(sK20(X0)) ) ).

cnf(u75,axiom,
    ( present(X0,sK21(X0,X1))
    | ~ man(X0,X1)
    | ~ sP4(X0) ) ).

cnf(u534,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK12(sK34(X0)))
    | ~ smoke(sK34(X0),sK14(sK34(X0)))
    | man(sK29(X0),sK37(sK29(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK12(sK34(X0)))
    | ~ of(X0,X1,sK12(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(sK34(X0)))
    | ~ sP2(X0)
    | ~ sP5(sK34(X0)) ) ).

cnf(u870,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK24(sK34(X0)))
    | ~ smoke(sK34(X0),sK33(sK34(X0)))
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK24(sK34(X0)))
    | ~ of(X0,X1,sK24(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK24(sK34(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP2(sK34(X0)) ) ).

cnf(u825,negated_conjecture,
    ( ~ agent(X0,sK14(X0),X1)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP0(sK15(X0),X1) ) ).

cnf(u995,negated_conjecture,
    ( ~ agent(sK29(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ present(sK29(X0),X2)
    | ~ smoke(sK29(X0),X2)
    | ~ agent(X0,sK28(X0),X1)
    | ~ event(sK29(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP2(X0) ) ).

cnf(u66,axiom,
    ( of(X0,sK13(X0),sK12(X0))
    | ~ sP5(X0) ) ).

cnf(u94,axiom,
    ( jules_forename(X0,sK30(X0))
    | ~ sP2(X0) ) ).

cnf(u549,negated_conjecture,
    ( ~ theme(X0,X2,X1)
    | ~ think_believe_consider(X0,X2)
    | ~ present(X0,X2)
    | ~ event(X0,X2)
    | ~ accessible_world(X0,X1)
    | ~ agent(X0,X2,X3)
    | ~ proposition(X0,X1)
    | ~ actual_world(X0)
    | ~ smoke(X1,X4)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ present(X1,X4)
    | ~ agent(X1,X4,X3)
    | ~ event(X1,X4)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ man(X0,X3)
    | ~ of(X0,X5,X3)
    | ~ forename(X0,X6)
    | ~ jules_forename(X0,X6)
    | ~ of(X0,X6,X3)
    | ~ sP5(X0) ) ).

cnf(u710,negated_conjecture,
    ( ~ sP3(sK20(X0),sK9(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK9(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(X0))
    | ~ sP5(X0)
    | man(sK20(X0),sK37(sK20(X0))) ) ).

cnf(u257,negated_conjecture,
    ( ~ of(X3,X5,sK17(X3))
    | ~ agent(X0,X1,X2)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ forename(X3,X5)
    | ~ jules_forename(X3,X5)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ accessible_world(X3,X6)
    | ~ think_believe_consider(X3,X7)
    | ~ present(X3,X7)
    | ~ event(X3,X7)
    | ~ theme(X3,X7,X6)
    | ~ agent(X3,X7,X8)
    | ~ proposition(X3,X6)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X8)
    | ~ of(X3,X9,X8)
    | ~ forename(X3,X10)
    | ~ vincent_forename(X3,X10)
    | ~ man(X3,X2)
    | ~ of(X3,X10,X2)
    | ~ forename(X3,X11)
    | ~ jules_forename(X3,X11)
    | ~ of(X3,X11,X2)
    | ~ sP5(X3)
    | ~ sP3(X6,sK37(X6)) ) ).

cnf(u49,axiom,
    ( state(X0,sK18(X0))
    | ~ sP5(X0) ) ).

cnf(u877,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ man(sK34(X0),X1)
    | ~ sP1(sK34(X0)) ) ).

cnf(u81,axiom,
    ( event(X0,sK22(X0,X1))
    | ~ sP3(X0,X1) ) ).

cnf(u109,axiom,
    ( forename(X0,sK25(X0))
    | ~ sP2(X0) ) ).

cnf(u1357,negated_conjecture,
    ( ~ agent(X0,sK14(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP3(sK15(X0),X1) ) ).

cnf(u40,axiom,
    ( sP3(sK20(X0),sK12(X0))
    | ~ sP5(X0) ) ).

cnf(u213,negated_conjecture,
    ( ~ agent(X3,sK14(X3),X5)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ smoke(X0,X1)
    | man(sK15(X3),sK37(sK15(X3)))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X2)
    | ~ forename(X3,X6)
    | ~ vincent_forename(X3,X6)
    | ~ man(X3,X5)
    | ~ of(X3,X6,X5)
    | ~ forename(X3,X7)
    | ~ vincent_forename(X3,X7)
    | ~ man(X3,X2)
    | ~ of(X3,X7,X2)
    | ~ forename(X3,X8)
    | ~ jules_forename(X3,X8)
    | ~ of(X3,X8,X2)
    | ~ sP2(X3)
    | ~ sP5(X3) ) ).

cnf(u1353,negated_conjecture,
    ( ~ agent(X0,sK14(X0),sK9(sK15(X0)))
    | ~ actual_world(X0)
    | ~ smoke(sK15(X0),sK19(sK15(X0)))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK9(sK15(X0)))
    | ~ of(X0,X1,sK9(sK15(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(sK15(X0)))
    | ~ sP5(X0)
    | ~ sP5(sK15(X0)) ) ).

cnf(u112,axiom,
    ( of(X0,sK25(X0),sK24(X0))
    | ~ sP2(X0) ) ).

cnf(u1050,negated_conjecture,
    ( ~ of(X0,X1,sK24(X0))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ actual_world(X0)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0) ) ).

cnf(u63,axiom,
    ( forename(X0,sK13(X0))
    | ~ sP5(X0) ) ).

cnf(u795,negated_conjecture,
    ( ~ agent(X0,sK19(X0),sK9(sK20(X0)))
    | ~ smoke(sK20(X0),sK19(sK20(X0)))
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK9(sK20(X0)))
    | ~ of(X0,X1,sK9(sK20(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(sK20(X0)))
    | ~ sP5(X0)
    | ~ sP5(sK20(X0)) ) ).

cnf(u452,negated_conjecture,
    ( ~ agent(X2,sK33(X2),X5)
    | ~ accessible_world(X2,X0)
    | ~ think_believe_consider(X2,X3)
    | ~ present(X2,X3)
    | ~ event(X2,X3)
    | ~ theme(X2,X3,X0)
    | ~ agent(X2,X3,X4)
    | ~ proposition(X2,X0)
    | ~ actual_world(X2)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ agent(X0,X1,X4)
    | ~ event(X0,X1)
    | ~ forename(X2,X6)
    | ~ vincent_forename(X2,X6)
    | ~ man(X2,X5)
    | ~ of(X2,X6,X5)
    | ~ forename(X2,X7)
    | ~ vincent_forename(X2,X7)
    | ~ man(X2,X4)
    | ~ of(X2,X7,X4)
    | ~ forename(X2,X8)
    | ~ jules_forename(X2,X8)
    | ~ of(X2,X8,X4)
    | ~ sP2(X2)
    | ~ sP4(sK34(X2)) ) ).

cnf(u904,negated_conjecture,
    ( ~ agent(X0,sK28(X0),X1)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP0(sK29(X0),X1) ) ).

cnf(u1208,negated_conjecture,
    ( ~ agent(X0,sK19(X0),sK24(sK20(X0)))
    | ~ smoke(sK20(X0),sK33(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK24(sK20(X0)))
    | ~ of(X0,X1,sK24(sK20(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK24(sK20(X0)))
    | ~ sP2(X0)
    | ~ sP5(X0)
    | ~ sP2(sK20(X0)) ) ).

cnf(u638,negated_conjecture,
    ( ~ agent(sK29(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ smoke(sK29(X0),X2)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ present(sK29(X0),X2)
    | ~ agent(X0,sK28(X0),X1)
    | ~ event(sK29(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP5(X0)
    | ~ sP2(X0) ) ).

cnf(u251,negated_conjecture,
    ( ~ smoke(X6,sK35(X6,sK37(X6)))
    | ~ agent(X0,X1,X2)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ forename(X3,X5)
    | ~ jules_forename(X3,X5)
    | ~ of(X3,X5,sK17(X3))
    | ~ present(X0,X1)
    | ~ present(X6,sK35(X6,sK37(X6)))
    | ~ smoke(X0,X1)
    | ~ event(X6,sK35(X6,sK37(X6)))
    | ~ accessible_world(X3,X6)
    | ~ think_believe_consider(X3,X7)
    | ~ present(X3,X7)
    | ~ event(X3,X7)
    | ~ theme(X3,X7,X6)
    | ~ agent(X3,X7,X8)
    | ~ proposition(X3,X6)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X8)
    | ~ of(X3,X9,X8)
    | ~ forename(X3,X10)
    | ~ vincent_forename(X3,X10)
    | ~ man(X3,X2)
    | ~ of(X3,X10,X2)
    | ~ forename(X3,X11)
    | ~ jules_forename(X3,X11)
    | ~ of(X3,X11,X2)
    | ~ sP5(X3)
    | ~ sP1(X6) ) ).

cnf(u591,negated_conjecture,
    ( ~ of(X0,X5,sK9(X0))
    | ~ think_believe_consider(X0,X2)
    | ~ present(X0,X2)
    | ~ event(X0,X2)
    | ~ theme(X0,X2,X1)
    | ~ agent(X0,X2,X3)
    | ~ proposition(X0,X1)
    | ~ actual_world(X0)
    | ~ present(X1,X4)
    | ~ smoke(X1,X4)
    | ~ agent(X1,X4,X3)
    | ~ event(X1,X4)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ accessible_world(X0,X1)
    | ~ forename(X0,X6)
    | ~ vincent_forename(X0,X6)
    | ~ man(X0,X3)
    | ~ of(X0,X6,X3)
    | ~ forename(X0,X7)
    | ~ jules_forename(X0,X7)
    | ~ of(X0,X7,X3)
    | ~ sP2(X0)
    | ~ sP1(sK20(X0))
    | ~ sP5(X0) ) ).

cnf(u971,negated_conjecture,
    ( ~ sP3(sK20(X0),sK9(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK9(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(X0))
    | ~ sP5(X0)
    | man(sK15(X0),sK37(sK15(X0))) ) ).

cnf(u763,negated_conjecture,
    ( ~ agent(X0,sK14(X0),X1)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP3(sK15(X0),X1) ) ).

cnf(u70,axiom,
    ( forename(X0,sK10(X0))
    | ~ sP5(X0) ) ).

cnf(u697,negated_conjecture,
    ( ~ sP0(sK20(X0),sK9(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK9(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(X0))
    | ~ sP5(X0)
    | man(sK20(X0),sK37(sK20(X0))) ) ).

cnf(u361,negated_conjecture,
    ( ~ sP3(X5,sK37(X5))
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ accessible_world(X3,X5)
    | ~ think_believe_consider(X3,X6)
    | ~ present(X3,X6)
    | ~ event(X3,X6)
    | ~ theme(X3,X6,X5)
    | ~ agent(X3,X6,X7)
    | ~ proposition(X3,X5)
    | ~ forename(X3,X8)
    | ~ vincent_forename(X3,X8)
    | ~ man(X3,X7)
    | ~ of(X3,X8,X7)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X2)
    | ~ of(X3,X9,X2)
    | ~ forename(X3,X10)
    | ~ jules_forename(X3,X10)
    | ~ of(X3,X10,X2)
    | ~ sP2(X3)
    | ~ agent(X0,X1,X2) ) ).

cnf(u1319,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ man(sK20(X0),X1)
    | ~ sP4(sK20(X0)) ) ).

cnf(u792,negated_conjecture,
    ( ~ agent(X0,sK19(X0),sK26(sK20(X0)))
    | ~ smoke(sK20(X0),sK28(sK20(X0)))
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK26(sK20(X0)))
    | ~ of(X0,X1,sK26(sK20(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK26(sK20(X0)))
    | ~ sP5(X0)
    | ~ sP2(sK20(X0)) ) ).

cnf(u433,negated_conjecture,
    ( ~ agent(X2,sK28(X2),X5)
    | ~ accessible_world(X2,X0)
    | ~ think_believe_consider(X2,X3)
    | ~ present(X2,X3)
    | ~ event(X2,X3)
    | ~ theme(X2,X3,X0)
    | ~ agent(X2,X3,X4)
    | ~ proposition(X2,X0)
    | ~ actual_world(X2)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ agent(X0,X1,X4)
    | ~ event(X0,X1)
    | ~ forename(X2,X6)
    | ~ vincent_forename(X2,X6)
    | ~ man(X2,X5)
    | ~ of(X2,X6,X5)
    | ~ forename(X2,X7)
    | ~ vincent_forename(X2,X7)
    | ~ man(X2,X4)
    | ~ of(X2,X7,X4)
    | ~ forename(X2,X8)
    | ~ jules_forename(X2,X8)
    | ~ of(X2,X8,X4)
    | ~ sP2(X2) ) ).

cnf(u1178,negated_conjecture,
    ( ~ agent(X0,sK28(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ sP0(sK29(X0),X1) ) ).

cnf(u911,negated_conjecture,
    ( ~ sP0(sK20(X0),sK9(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK9(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(X0))
    | ~ sP5(X0)
    | man(sK15(X0),sK37(sK15(X0))) ) ).

cnf(u44,axiom,
    ( event(X0,sK19(X0))
    | ~ sP5(X0) ) ).

cnf(u88,axiom,
    ( agent(X0,sK33(X0),sK24(X0))
    | ~ sP2(X0) ) ).

cnf(u116,axiom,
    ( smoke(X0,sK35(X0,X1))
    | ~ man(X0,X1)
    | ~ sP1(X0) ) ).

cnf(u324,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | man(sK34(X0),sK37(sK34(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ sP0(sK34(X0),X1) ) ).

cnf(u51,axiom,
    ( forename(X0,sK16(X0))
    | ~ sP5(X0) ) ).

cnf(u220,negated_conjecture,
    ( ~ of(X2,X5,sK24(X2))
    | ~ accessible_world(X2,X0)
    | ~ think_believe_consider(X2,X3)
    | ~ present(X2,X3)
    | ~ event(X2,X3)
    | ~ theme(X2,X3,X0)
    | ~ agent(X2,X3,X4)
    | ~ proposition(X2,X0)
    | ~ actual_world(X2)
    | ~ smoke(X0,X1)
    | man(sK34(X2),sK37(sK34(X2)))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X4)
    | ~ forename(X2,X5)
    | ~ vincent_forename(X2,X5)
    | ~ event(X0,X1)
    | ~ forename(X2,X6)
    | ~ vincent_forename(X2,X6)
    | ~ man(X2,X4)
    | ~ of(X2,X6,X4)
    | ~ forename(X2,X7)
    | ~ jules_forename(X2,X7)
    | ~ of(X2,X7,X4)
    | ~ sP2(X2) ) ).

cnf(u1209,negated_conjecture,
    ( ~ agent(X0,sK19(X0),sK26(sK20(X0)))
    | ~ smoke(sK20(X0),sK28(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK26(sK20(X0)))
    | ~ of(X0,X1,sK26(sK20(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK26(sK20(X0)))
    | ~ sP2(X0)
    | ~ sP5(X0)
    | ~ sP2(sK20(X0)) ) ).

cnf(u331,negated_conjecture,
    ( ~ theme(X3,X6,X5)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ accessible_world(X3,X5)
    | ~ think_believe_consider(X3,X6)
    | ~ present(X3,X6)
    | ~ event(X3,X6)
    | ~ agent(X0,X1,X2)
    | ~ agent(X3,X6,X7)
    | ~ proposition(X3,X5)
    | ~ forename(X3,X8)
    | ~ vincent_forename(X3,X8)
    | ~ man(X3,X7)
    | ~ of(X3,X8,X7)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X2)
    | ~ of(X3,X9,X2)
    | ~ forename(X3,X10)
    | ~ jules_forename(X3,X10)
    | ~ of(X3,X10,X2)
    | ~ sP2(X3)
    | ~ sP1(X5) ) ).

cnf(u554,negated_conjecture,
    ( ~ of(X0,X1,sK24(X0))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ actual_world(X0)
    | ~ jules_forename(X0,sK25(X0))
    | man(sK29(X0),sK37(sK29(X0)))
    | ~ sP2(X0) ) ).

cnf(u391,negated_conjecture,
    ( ~ of(X2,X5,sK9(X2))
    | ~ accessible_world(X2,X0)
    | ~ think_believe_consider(X2,X3)
    | ~ present(X2,X3)
    | ~ event(X2,X3)
    | ~ theme(X2,X3,X0)
    | ~ agent(X2,X3,X4)
    | ~ proposition(X2,X0)
    | ~ actual_world(X2)
    | ~ smoke(X0,X1)
    | man(sK20(X2),sK37(sK20(X2)))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X4)
    | ~ forename(X2,X5)
    | ~ vincent_forename(X2,X5)
    | ~ event(X0,X1)
    | ~ forename(X2,X6)
    | ~ vincent_forename(X2,X6)
    | ~ man(X2,X4)
    | ~ of(X2,X6,X4)
    | ~ forename(X2,X7)
    | ~ jules_forename(X2,X7)
    | ~ of(X2,X7,X4)
    | ~ sP5(X2) ) ).

cnf(u871,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK26(sK34(X0)))
    | ~ smoke(sK34(X0),sK28(sK34(X0)))
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK26(sK34(X0)))
    | ~ of(X0,X1,sK26(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK26(sK34(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP2(sK34(X0)) ) ).

cnf(u1216,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ sP5(X0)
    | ~ sP3(sK20(X0),X1) ) ).

cnf(u579,negated_conjecture,
    ( ~ of(X0,X5,sK24(X0))
    | ~ think_believe_consider(X0,X2)
    | ~ present(X0,X2)
    | ~ event(X0,X2)
    | ~ theme(X0,X2,X1)
    | ~ agent(X0,X2,X3)
    | ~ proposition(X0,X1)
    | ~ actual_world(X0)
    | ~ present(X1,X4)
    | ~ smoke(X1,X4)
    | ~ agent(X1,X4,X3)
    | ~ event(X1,X4)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ accessible_world(X0,X1)
    | ~ forename(X0,X6)
    | ~ vincent_forename(X0,X6)
    | ~ man(X0,X3)
    | ~ of(X0,X6,X3)
    | ~ forename(X0,X7)
    | ~ jules_forename(X0,X7)
    | ~ of(X0,X7,X3)
    | ~ sP2(X0)
    | ~ sP1(sK34(X0)) ) ).

cnf(u736,negated_conjecture,
    ( ~ theme(X0,X6,X5)
    | ~ present(X0,X1)
    | ~ event(X0,X1)
    | ~ theme(X0,X1,X2)
    | ~ agent(X0,X1,X3)
    | ~ proposition(X0,X2)
    | ~ actual_world(X0)
    | ~ accessible_world(X0,X2)
    | ~ present(X2,X4)
    | ~ agent(X2,X4,X3)
    | ~ smoke(X2,X4)
    | ~ event(X2,X4)
    | ~ accessible_world(X0,X5)
    | ~ think_believe_consider(X0,X6)
    | ~ present(X0,X6)
    | ~ event(X0,X6)
    | ~ think_believe_consider(X0,X1)
    | ~ agent(X0,X6,X7)
    | ~ proposition(X0,X5)
    | ~ forename(X0,X8)
    | ~ vincent_forename(X0,X8)
    | ~ man(X0,X7)
    | ~ of(X0,X8,X7)
    | ~ forename(X0,X9)
    | ~ vincent_forename(X0,X9)
    | ~ man(X0,X3)
    | ~ of(X0,X9,X3)
    | ~ forename(X0,X10)
    | ~ jules_forename(X0,X10)
    | ~ of(X0,X10,X3)
    | ~ sP5(X0)
    | ~ sP1(X5) ) ).

cnf(u730,negated_conjecture,
    ( ~ man(sK20(X0),sK9(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK9(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(X0))
    | ~ sP5(X0)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ sP4(sK20(X0)) ) ).

cnf(u906,negated_conjecture,
    ( ~ agent(X0,sK28(X0),X1)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP3(sK29(X0),X1) ) ).

cnf(u350,negated_conjecture,
    ( ~ sP0(X5,sK37(X5))
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ accessible_world(X3,X5)
    | ~ think_believe_consider(X3,X6)
    | ~ present(X3,X6)
    | ~ event(X3,X6)
    | ~ theme(X3,X6,X5)
    | ~ agent(X3,X6,X7)
    | ~ proposition(X3,X5)
    | ~ forename(X3,X8)
    | ~ vincent_forename(X3,X8)
    | ~ man(X3,X7)
    | ~ of(X3,X8,X7)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X2)
    | ~ of(X3,X9,X2)
    | ~ forename(X3,X10)
    | ~ jules_forename(X3,X10)
    | ~ of(X3,X10,X2)
    | ~ sP2(X3)
    | ~ agent(X0,X1,X2) ) ).

cnf(u966,negated_conjecture,
    ( ~ agent(X0,sK28(X0),X1)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP3(sK29(X0),X1) ) ).

cnf(u1140,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK24(sK34(X0)))
    | ~ smoke(sK34(X0),sK33(sK34(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK24(sK34(X0)))
    | ~ of(X0,X1,sK24(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK24(sK34(X0)))
    | ~ sP2(X0)
    | ~ sP2(sK34(X0)) ) ).

cnf(u365,negated_conjecture,
    ( ~ sP0(X5,sK37(X5))
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ accessible_world(X3,X5)
    | ~ think_believe_consider(X3,X6)
    | ~ present(X3,X6)
    | ~ event(X3,X6)
    | ~ theme(X3,X6,X5)
    | ~ agent(X3,X6,X7)
    | ~ proposition(X3,X5)
    | ~ forename(X3,X8)
    | ~ vincent_forename(X3,X8)
    | ~ man(X3,X7)
    | ~ of(X3,X8,X7)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X2)
    | ~ of(X3,X9,X2)
    | ~ forename(X3,X10)
    | ~ jules_forename(X3,X10)
    | ~ of(X3,X10,X2)
    | ~ sP5(X3)
    | ~ agent(X0,X1,X2) ) ).

cnf(u110,axiom,
    ( vincent_forename(X0,sK25(X0))
    | ~ sP2(X0) ) ).

cnf(u1223,negated_conjecture,
    ( ~ vincent_forename(X0,sK23(X0))
    | ~ actual_world(X0)
    | ~ sP2(X0) ) ).

cnf(u73,axiom,
    ( of(X0,sK10(X0),sK9(X0))
    | ~ sP5(X0) ) ).

cnf(u1315,negated_conjecture,
    ( ~ agent(X0,sK19(X0),sK12(sK20(X0)))
    | ~ actual_world(X0)
    | ~ smoke(sK20(X0),sK14(sK20(X0)))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK12(sK20(X0)))
    | ~ of(X0,X1,sK12(sK20(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(sK20(X0)))
    | ~ sP5(X0)
    | ~ sP5(sK20(X0)) ) ).

cnf(u481,negated_conjecture,
    ( ~ theme(X0,X2,X1)
    | ~ think_believe_consider(X0,X2)
    | ~ present(X0,X2)
    | ~ event(X0,X2)
    | ~ accessible_world(X0,X1)
    | ~ agent(X0,X2,X3)
    | ~ proposition(X0,X1)
    | ~ actual_world(X0)
    | ~ smoke(X1,X4)
    | man(sK29(X0),sK37(sK29(X0)))
    | ~ present(X1,X4)
    | ~ agent(X1,X4,X3)
    | ~ event(X1,X4)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ man(X0,X3)
    | ~ of(X0,X5,X3)
    | ~ forename(X0,X6)
    | ~ jules_forename(X0,X6)
    | ~ of(X0,X6,X3)
    | ~ sP2(X0) ) ).

cnf(u875,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK12(sK34(X0)))
    | ~ smoke(sK34(X0),sK14(sK34(X0)))
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK12(sK34(X0)))
    | ~ of(X0,X1,sK12(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(sK34(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP5(sK34(X0)) ) ).

cnf(u356,negated_conjecture,
    ( man(sK34(X0),sK37(sK34(X0)))
    | ~ actual_world(X0)
    | ~ vincent_forename(X0,sK23(X0))
    | ~ sP2(X0) ) ).

cnf(u92,axiom,
    ( man(X0,sK31(X0))
    | ~ sP2(X0) ) ).

cnf(u1264,negated_conjecture,
    ( ~ of(X0,X5,sK9(X0))
    | ~ theme(X0,X1,X2)
    | ~ agent(X0,X1,X3)
    | ~ proposition(X0,X2)
    | ~ actual_world(X0)
    | ~ accessible_world(X0,X2)
    | ~ present(X2,X4)
    | ~ agent(X2,X4,X3)
    | ~ smoke(X2,X4)
    | ~ event(X2,X4)
    | ~ think_believe_consider(X0,X1)
    | ~ present(X0,X1)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ event(X0,X1)
    | ~ forename(X0,X6)
    | ~ vincent_forename(X0,X6)
    | ~ man(X0,X3)
    | ~ of(X0,X6,X3)
    | ~ forename(X0,X7)
    | ~ jules_forename(X0,X7)
    | ~ of(X0,X7,X3)
    | ~ sP5(X0)
    | ~ sP1(sK20(X0)) ) ).

cnf(u55,axiom,
    ( sP4(sK15(X0))
    | ~ sP5(X0) ) ).

cnf(u99,axiom,
    ( think_believe_consider(X0,sK28(X0))
    | ~ sP2(X0) ) ).

cnf(u507,negated_conjecture,
    ( ~ agent(sK15(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ smoke(sK15(X0),X2)
    | man(sK29(X0),sK37(sK29(X0)))
    | ~ present(sK15(X0),X2)
    | ~ agent(X0,sK14(X0),X1)
    | ~ event(sK15(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP2(X0)
    | ~ sP5(X0) ) ).

cnf(u1350,negated_conjecture,
    ( ~ agent(X0,sK14(X0),sK26(sK15(X0)))
    | ~ actual_world(X0)
    | ~ smoke(sK15(X0),sK28(sK15(X0)))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK26(sK15(X0)))
    | ~ of(X0,X1,sK26(sK15(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK26(sK15(X0)))
    | ~ sP5(X0)
    | ~ sP2(sK15(X0)) ) ).

cnf(u639,negated_conjecture,
    ( ~ agent(sK20(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ smoke(sK20(X0),X2)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ present(sK20(X0),X2)
    | ~ agent(X0,sK19(X0),X1)
    | ~ event(sK20(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP5(X0) ) ).

cnf(u58,axiom,
    ( present(X0,sK14(X0))
    | ~ sP5(X0) ) ).

cnf(u235,negated_conjecture,
    ( ~ of(X3,X5,sK31(X3))
    | ~ agent(X0,X1,X2)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ forename(X3,X5)
    | ~ jules_forename(X3,X5)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ accessible_world(X3,X6)
    | ~ think_believe_consider(X3,X7)
    | ~ present(X3,X7)
    | ~ event(X3,X7)
    | ~ theme(X3,X7,X6)
    | ~ agent(X3,X7,X8)
    | ~ proposition(X3,X6)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X8)
    | ~ of(X3,X9,X8)
    | ~ forename(X3,X10)
    | ~ vincent_forename(X3,X10)
    | ~ man(X3,X2)
    | ~ of(X3,X10,X2)
    | ~ forename(X3,X11)
    | ~ jules_forename(X3,X11)
    | ~ of(X3,X11,X2)
    | ~ sP2(X3)
    | ~ sP3(X6,sK37(X6)) ) ).

cnf(u118,axiom,
    ( agent(X0,sK35(X0,X1),X1)
    | ~ man(X0,X1)
    | ~ sP1(X0) ) ).

cnf(u573,negated_conjecture,
    ( ~ of(X0,X5,sK26(X0))
    | ~ think_believe_consider(X0,X2)
    | ~ present(X0,X2)
    | ~ event(X0,X2)
    | ~ theme(X0,X2,X1)
    | ~ agent(X0,X2,X3)
    | ~ proposition(X0,X1)
    | ~ actual_world(X0)
    | ~ present(X1,X4)
    | ~ smoke(X1,X4)
    | ~ agent(X1,X4,X3)
    | ~ event(X1,X4)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ accessible_world(X0,X1)
    | ~ forename(X0,X6)
    | ~ vincent_forename(X0,X6)
    | ~ man(X0,X3)
    | ~ of(X0,X6,X3)
    | ~ forename(X0,X7)
    | ~ jules_forename(X0,X7)
    | ~ of(X0,X7,X3)
    | ~ sP2(X0) ) ).

cnf(u692,negated_conjecture,
    ( ~ agent(sK29(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ smoke(sK29(X0),X2)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ present(sK29(X0),X2)
    | ~ agent(X0,sK28(X0),X1)
    | ~ event(sK29(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP5(X0)
    | ~ sP2(X0) ) ).

cnf(u1189,negated_conjecture,
    ( ~ of(X0,X1,sK24(X0))
    | ~ vincent_forename(X0,X1)
    | ~ forename(X0,X1)
    | ~ actual_world(X0)
    | ~ sP2(X0) ) ).

cnf(u281,negated_conjecture,
    ( ~ agent(sK29(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ smoke(sK29(X0),X2)
    | man(sK34(X0),sK37(sK34(X0)))
    | ~ present(sK29(X0),X2)
    | ~ agent(X0,sK28(X0),X1)
    | ~ event(sK29(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP2(X0) ) ).

cnf(u1048,negated_conjecture,
    ( ~ of(X0,X1,sK24(X0))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ actual_world(X0)
    | ~ jules_forename(X0,sK25(X0))
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0) ) ).

cnf(u1148,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ sP3(sK34(X0),X1) ) ).

cnf(u1324,negated_conjecture,
    ( ~ sP0(sK20(X0),sK9(X0))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK9(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(X0))
    | ~ sP5(X0)
    | ~ actual_world(X0) ) ).

cnf(u177,negated_conjecture,
    ( ~ of(X3,X5,sK17(X3))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X2)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ forename(X3,X5)
    | ~ jules_forename(X3,X5)
    | ~ smoke(X0,X1)
    | man(X6,sK37(X6))
    | ~ accessible_world(X3,X6)
    | ~ think_believe_consider(X3,X7)
    | ~ present(X3,X7)
    | ~ event(X3,X7)
    | ~ theme(X3,X7,X6)
    | ~ agent(X3,X7,X8)
    | ~ proposition(X3,X6)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X8)
    | ~ of(X3,X9,X8)
    | ~ forename(X3,X10)
    | ~ vincent_forename(X3,X10)
    | ~ man(X3,X2)
    | ~ of(X3,X10,X2)
    | ~ forename(X3,X11)
    | ~ jules_forename(X3,X11)
    | ~ of(X3,X11,X2)
    | ~ sP5(X3) ) ).

cnf(u77,axiom,
    ( event(X0,sK21(X0,X1))
    | ~ man(X0,X1)
    | ~ sP4(X0) ) ).

cnf(u879,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ man(sK34(X0),X1)
    | ~ sP4(sK34(X0)) ) ).

cnf(u1311,negated_conjecture,
    ( ~ agent(X0,sK19(X0),sK26(sK20(X0)))
    | ~ actual_world(X0)
    | ~ smoke(sK20(X0),sK28(sK20(X0)))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK26(sK20(X0)))
    | ~ of(X0,X1,sK26(sK20(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK26(sK20(X0)))
    | ~ sP5(X0)
    | ~ sP2(sK20(X0)) ) ).

cnf(u319,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK26(sK34(X0)))
    | ~ smoke(sK34(X0),sK28(sK34(X0)))
    | man(sK34(X0),sK37(sK34(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK26(sK34(X0)))
    | ~ of(X0,X1,sK26(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK26(sK34(X0)))
    | ~ sP2(X0)
    | ~ sP2(sK34(X0)) ) ).

cnf(u755,negated_conjecture,
    ( ~ agent(X0,sK14(X0),sK24(sK15(X0)))
    | ~ smoke(sK15(X0),sK33(sK15(X0)))
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK24(sK15(X0)))
    | ~ of(X0,X1,sK24(sK15(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK24(sK15(X0)))
    | ~ sP5(X0)
    | ~ sP2(sK15(X0)) ) ).

cnf(u68,axiom,
    ( jules_forename(X0,sK11(X0))
    | ~ sP5(X0) ) ).

cnf(u80,axiom,
    ( agent(X0,sK22(X0,X1),X1)
    | ~ sP3(X0,X1) ) ).

cnf(u256,negated_conjecture,
    ( ~ of(X3,X5,sK17(X3))
    | ~ agent(X0,X1,X2)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ forename(X3,X5)
    | ~ jules_forename(X3,X5)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ accessible_world(X3,X6)
    | ~ think_believe_consider(X3,X7)
    | ~ present(X3,X7)
    | ~ event(X3,X7)
    | ~ theme(X3,X7,X6)
    | ~ agent(X3,X7,X8)
    | ~ proposition(X3,X6)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X8)
    | ~ of(X3,X9,X8)
    | ~ forename(X3,X10)
    | ~ vincent_forename(X3,X10)
    | ~ man(X3,X2)
    | ~ of(X3,X10,X2)
    | ~ forename(X3,X11)
    | ~ jules_forename(X3,X11)
    | ~ of(X3,X11,X2)
    | ~ sP5(X3)
    | ~ sP0(X6,sK37(X6)) ) ).

cnf(u537,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | man(sK29(X0),sK37(sK29(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ sP3(sK34(X0),X1) ) ).

cnf(u43,axiom,
    ( present(X0,sK19(X0))
    | ~ sP5(X0) ) ).

cnf(u769,negated_conjecture,
    ( ~ theme(X0,X6,X5)
    | ~ present(X0,X1)
    | ~ event(X0,X1)
    | ~ theme(X0,X1,X2)
    | ~ agent(X0,X1,X3)
    | ~ proposition(X0,X2)
    | ~ actual_world(X0)
    | ~ accessible_world(X0,X2)
    | ~ present(X2,X4)
    | ~ agent(X2,X4,X3)
    | ~ smoke(X2,X4)
    | ~ event(X2,X4)
    | ~ accessible_world(X0,X5)
    | ~ think_believe_consider(X0,X6)
    | ~ present(X0,X6)
    | ~ event(X0,X6)
    | ~ think_believe_consider(X0,X1)
    | ~ agent(X0,X6,X7)
    | ~ proposition(X0,X5)
    | ~ forename(X0,X8)
    | ~ vincent_forename(X0,X8)
    | ~ man(X0,X7)
    | ~ of(X0,X8,X7)
    | ~ forename(X0,X9)
    | ~ vincent_forename(X0,X9)
    | ~ man(X0,X3)
    | ~ of(X0,X9,X3)
    | ~ forename(X0,X10)
    | ~ jules_forename(X0,X10)
    | ~ of(X0,X10,X3)
    | ~ sP5(X0)
    | ~ sP4(X5) ) ).

cnf(u664,negated_conjecture,
    ( ~ agent(X0,sK19(X0),sK12(sK20(X0)))
    | ~ smoke(sK20(X0),sK14(sK20(X0)))
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK12(sK20(X0)))
    | ~ of(X0,X1,sK12(sK20(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(sK20(X0)))
    | ~ sP5(X0)
    | ~ sP5(sK20(X0)) ) ).

cnf(u103,axiom,
    ( agent(X0,sK28(X0),sK26(X0))
    | ~ sP2(X0) ) ).

cnf(u791,negated_conjecture,
    ( ~ agent(X0,sK19(X0),sK24(sK20(X0)))
    | ~ smoke(sK20(X0),sK33(sK20(X0)))
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK24(sK20(X0)))
    | ~ of(X0,X1,sK24(sK20(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK24(sK20(X0)))
    | ~ sP5(X0)
    | ~ sP2(sK20(X0)) ) ).

cnf(u1176,negated_conjecture,
    ( ~ agent(X0,sK28(X0),sK9(sK29(X0)))
    | ~ smoke(sK29(X0),sK19(sK29(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK9(sK29(X0)))
    | ~ of(X0,X1,sK9(sK29(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(sK29(X0)))
    | ~ sP2(X0)
    | ~ sP5(sK29(X0)) ) ).

cnf(u62,axiom,
    ( proposition(X0,sK15(X0))
    | ~ sP5(X0) ) ).

cnf(u1368,negated_conjecture,
    ( ~ sP3(sK15(X0),sK12(X0))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK12(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(X0))
    | ~ sP5(X0)
    | ~ actual_world(X0) ) ).

cnf(u106,axiom,
    ( vincent_forename(X0,sK27(X0))
    | ~ sP2(X0) ) ).

cnf(u282,negated_conjecture,
    ( ~ agent(sK20(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ smoke(sK20(X0),X2)
    | man(sK34(X0),sK37(sK34(X0)))
    | ~ present(sK20(X0),X2)
    | ~ agent(X0,sK19(X0),X1)
    | ~ event(sK20(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP2(X0)
    | ~ sP5(X0) ) ).

cnf(u898,negated_conjecture,
    ( ~ agent(X0,sK28(X0),sK24(sK29(X0)))
    | ~ smoke(sK29(X0),sK33(sK29(X0)))
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK24(sK29(X0)))
    | ~ of(X0,X1,sK24(sK29(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK24(sK29(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP2(sK29(X0)) ) ).

cnf(u210,negated_conjecture,
    ( ~ agent(X3,sK33(X3),X5)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ smoke(X0,X1)
    | man(sK34(X3),sK37(sK34(X3)))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X2)
    | ~ forename(X3,X6)
    | ~ vincent_forename(X3,X6)
    | ~ man(X3,X5)
    | ~ of(X3,X6,X5)
    | ~ forename(X3,X7)
    | ~ vincent_forename(X3,X7)
    | ~ man(X3,X2)
    | ~ of(X3,X7,X2)
    | ~ forename(X3,X8)
    | ~ jules_forename(X3,X8)
    | ~ of(X3,X8,X2)
    | ~ sP2(X3) ) ).

cnf(u665,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X1)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP0(sK20(X0),X1) ) ).

cnf(u693,negated_conjecture,
    ( ~ agent(sK20(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ smoke(sK20(X0),X2)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ present(sK20(X0),X2)
    | ~ agent(X0,sK19(X0),X1)
    | ~ event(sK20(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP5(X0) ) ).

cnf(u121,axiom,
    ( present(X0,sK36(X0,X1))
    | ~ sP0(X0,X1) ) ).

cnf(u1088,negated_conjecture,
    ( man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ vincent_forename(X0,sK23(X0))
    | ~ sP5(X0)
    | ~ sP2(X0) ) ).

cnf(u181,negated_conjecture,
    ( ~ theme(X3,X6,X5)
    | ~ agent(X0,X1,X2)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ smoke(X0,X1)
    | man(X5,sK37(X5))
    | ~ accessible_world(X3,X5)
    | ~ think_believe_consider(X3,X6)
    | ~ present(X3,X6)
    | ~ event(X3,X6)
    | ~ present(X0,X1)
    | ~ agent(X3,X6,X7)
    | ~ proposition(X3,X5)
    | ~ forename(X3,X8)
    | ~ vincent_forename(X3,X8)
    | ~ man(X3,X7)
    | ~ of(X3,X8,X7)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X2)
    | ~ of(X3,X9,X2)
    | ~ forename(X3,X10)
    | ~ jules_forename(X3,X10)
    | ~ of(X3,X10,X2)
    | ~ sP2(X3) ) ).

cnf(u1212,negated_conjecture,
    ( ~ agent(X0,sK19(X0),sK9(sK20(X0)))
    | ~ smoke(sK20(X0),sK19(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK9(sK20(X0)))
    | ~ of(X0,X1,sK9(sK20(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(sK20(X0)))
    | ~ sP2(X0)
    | ~ sP5(X0)
    | ~ sP5(sK20(X0)) ) ).

cnf(u1317,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ man(sK20(X0),X1)
    | ~ sP1(sK20(X0)) ) ).

cnf(u253,negated_conjecture,
    ( ~ smoke(X6,sK21(X6,sK37(X6)))
    | ~ agent(X0,X1,X2)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ forename(X3,X5)
    | ~ jules_forename(X3,X5)
    | ~ of(X3,X5,sK17(X3))
    | ~ present(X0,X1)
    | ~ present(X6,sK21(X6,sK37(X6)))
    | ~ smoke(X0,X1)
    | ~ event(X6,sK21(X6,sK37(X6)))
    | ~ accessible_world(X3,X6)
    | ~ think_believe_consider(X3,X7)
    | ~ present(X3,X7)
    | ~ event(X3,X7)
    | ~ theme(X3,X7,X6)
    | ~ agent(X3,X7,X8)
    | ~ proposition(X3,X6)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X8)
    | ~ of(X3,X9,X8)
    | ~ forename(X3,X10)
    | ~ vincent_forename(X3,X10)
    | ~ man(X3,X2)
    | ~ of(X3,X10,X2)
    | ~ forename(X3,X11)
    | ~ jules_forename(X3,X11)
    | ~ of(X3,X11,X2)
    | ~ sP5(X3)
    | ~ sP4(X6) ) ).

cnf(u963,negated_conjecture,
    ( ~ agent(X0,sK28(X0),sK12(sK29(X0)))
    | ~ smoke(sK29(X0),sK14(sK29(X0)))
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK12(sK29(X0)))
    | ~ of(X0,X1,sK12(sK29(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(sK29(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP5(sK29(X0)) ) ).

cnf(u1144,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK9(sK34(X0)))
    | ~ smoke(sK34(X0),sK19(sK34(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK9(sK34(X0)))
    | ~ of(X0,X1,sK9(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(sK34(X0)))
    | ~ sP2(X0)
    | ~ sP5(sK34(X0)) ) ).

cnf(u1089,negated_conjecture,
    ( man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ sP5(X0)
    | ~ sP2(X0) ) ).

cnf(u84,axiom,
    ( think_believe_consider(X0,sK33(X0))
    | ~ sP2(X0) ) ).

cnf(u536,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | man(sK29(X0),sK37(sK29(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ man(sK34(X0),X1)
    | ~ sP1(sK34(X0)) ) ).

cnf(u244,negated_conjecture,
    ( ~ theme(X0,X2,X1)
    | ~ think_believe_consider(X0,X2)
    | ~ present(X0,X2)
    | ~ event(X0,X2)
    | ~ accessible_world(X0,X1)
    | ~ agent(X0,X2,X3)
    | ~ proposition(X0,X1)
    | ~ actual_world(X0)
    | ~ smoke(X1,X4)
    | man(sK34(X0),sK37(sK34(X0)))
    | ~ present(X1,X4)
    | ~ agent(X1,X4,X3)
    | ~ vincent_forename(X0,sK23(X0))
    | ~ event(X1,X4)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ man(X0,X3)
    | ~ of(X0,X5,X3)
    | ~ forename(X0,X6)
    | ~ jules_forename(X0,X6)
    | ~ of(X0,X6,X3)
    | ~ sP2(X0) ) ).

cnf(u668,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X1)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ man(sK20(X0),X1)
    | ~ sP4(sK20(X0)) ) ).

cnf(u772,negated_conjecture,
    ( ~ sP0(sK15(X0),sK12(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK12(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(X0))
    | ~ sP5(X0)
    | man(sK20(X0),sK37(sK20(X0))) ) ).

cnf(u1033,negated_conjecture,
    ( ~ agent(X0,sK14(X0),X5)
    | ~ event(X0,X1)
    | ~ theme(X0,X1,X2)
    | ~ agent(X0,X1,X3)
    | ~ proposition(X0,X2)
    | ~ actual_world(X0)
    | ~ accessible_world(X0,X2)
    | ~ present(X2,X4)
    | ~ agent(X2,X4,X3)
    | ~ smoke(X2,X4)
    | ~ event(X2,X4)
    | ~ think_believe_consider(X0,X1)
    | ~ present(X0,X1)
    | ~ forename(X0,X6)
    | ~ vincent_forename(X0,X6)
    | ~ man(X0,X5)
    | ~ of(X0,X6,X5)
    | ~ forename(X0,X7)
    | ~ vincent_forename(X0,X7)
    | ~ man(X0,X3)
    | ~ of(X0,X7,X3)
    | ~ forename(X0,X8)
    | ~ jules_forename(X0,X8)
    | ~ of(X0,X8,X3)
    | ~ sP5(X0) ) ).

cnf(u640,negated_conjecture,
    ( ~ agent(sK15(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ smoke(sK15(X0),X2)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ present(sK15(X0),X2)
    | ~ agent(X0,sK14(X0),X1)
    | ~ event(sK15(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP5(X0) ) ).

cnf(u79,axiom,
    ( present(X0,sK22(X0,X1))
    | ~ sP3(X0,X1) ) ).

cnf(u91,axiom,
    ( state(X0,sK32(X0))
    | ~ sP2(X0) ) ).

cnf(u826,negated_conjecture,
    ( ~ agent(X0,sK14(X0),X1)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ man(sK15(X0),X1)
    | ~ sP1(sK15(X0)) ) ).

cnf(u60,axiom,
    ( theme(X0,sK14(X0),sK15(X0))
    | ~ sP5(X0) ) ).

cnf(u45,axiom,
    ( theme(X0,sK19(X0),sK20(X0))
    | ~ sP5(X0) ) ).

cnf(u902,negated_conjecture,
    ( ~ agent(X0,sK28(X0),sK9(sK29(X0)))
    | ~ smoke(sK29(X0),sK19(sK29(X0)))
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK9(sK29(X0)))
    | ~ of(X0,X1,sK9(sK29(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(sK29(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP5(sK29(X0)) ) ).

cnf(u1224,negated_conjecture,
    ( ~ sP2(X0)
    | ~ actual_world(X0) ) ).

cnf(u663,negated_conjecture,
    ( ~ agent(X0,sK19(X0),sK9(sK20(X0)))
    | ~ smoke(sK20(X0),sK19(sK20(X0)))
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK9(sK20(X0)))
    | ~ of(X0,X1,sK9(sK20(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(sK20(X0)))
    | ~ sP5(X0)
    | ~ sP5(sK20(X0)) ) ).

cnf(u82,axiom,
    ( sP0(sK34(X0),sK24(X0))
    | ~ sP2(X0) ) ).

cnf(u238,negated_conjecture,
    ( ~ of(X3,X5,sK31(X3))
    | ~ agent(X0,X1,X2)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ forename(X3,X5)
    | ~ jules_forename(X3,X5)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ accessible_world(X3,X6)
    | ~ think_believe_consider(X3,X7)
    | ~ present(X3,X7)
    | ~ event(X3,X7)
    | ~ theme(X3,X7,X6)
    | ~ agent(X3,X7,X8)
    | ~ proposition(X3,X6)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X8)
    | ~ of(X3,X9,X8)
    | ~ forename(X3,X10)
    | ~ vincent_forename(X3,X10)
    | ~ man(X3,X2)
    | ~ of(X3,X10,X2)
    | ~ forename(X3,X11)
    | ~ jules_forename(X3,X11)
    | ~ of(X3,X11,X2)
    | ~ sP2(X3)
    | ~ sP4(X6) ) ).

cnf(u707,negated_conjecture,
    ( ~ theme(X0,X1,X2)
    | ~ present(X0,X1)
    | ~ event(X0,X1)
    | ~ think_believe_consider(X0,X1)
    | ~ agent(X0,X1,X3)
    | ~ proposition(X0,X2)
    | ~ actual_world(X0)
    | ~ present(X2,X4)
    | ~ smoke(X2,X4)
    | ~ agent(X2,X4,X3)
    | ~ event(X2,X4)
    | ~ accessible_world(X0,X2)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ man(X0,X3)
    | ~ of(X0,X5,X3)
    | ~ forename(X0,X6)
    | ~ jules_forename(X0,X6)
    | ~ of(X0,X6,X3)
    | ~ sP2(X0) ) ).

cnf(u1181,negated_conjecture,
    ( ~ agent(X0,sK28(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ man(sK29(X0),X1)
    | ~ sP4(sK29(X0)) ) ).

cnf(u97,axiom,
    ( sP1(sK29(X0))
    | ~ sP2(X0) ) ).

cnf(u1146,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ sP0(sK34(X0),X1) ) ).

cnf(u505,negated_conjecture,
    ( ~ agent(sK29(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ smoke(sK29(X0),X2)
    | man(sK29(X0),sK37(sK29(X0)))
    | ~ present(sK29(X0),X2)
    | ~ agent(X0,sK28(X0),X1)
    | ~ event(sK29(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP2(X0) ) ).

cnf(u691,negated_conjecture,
    ( ~ agent(sK34(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ smoke(sK34(X0),X2)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ present(sK34(X0),X2)
    | ~ agent(X0,sK33(X0),X1)
    | ~ event(sK34(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP5(X0)
    | ~ sP2(X0) ) ).

cnf(u56,axiom,
    ( accessible_world(X0,sK15(X0))
    | ~ sP5(X0) ) ).

cnf(u1371,negated_conjecture,
    ( ~ man(sK15(X0),sK12(X0))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK12(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(X0))
    | ~ sP5(X0)
    | ~ actual_world(X0) ) ).

cnf(u1355,negated_conjecture,
    ( ~ agent(X0,sK14(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP0(sK15(X0),X1) ) ).

cnf(u1147,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ man(sK34(X0),X1)
    | ~ sP1(sK34(X0)) ) ).

cnf(u1141,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK26(sK34(X0)))
    | ~ smoke(sK34(X0),sK28(sK34(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK26(sK34(X0)))
    | ~ of(X0,X1,sK26(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK26(sK34(X0)))
    | ~ sP2(X0)
    | ~ sP2(sK34(X0)) ) ).

cnf(u1177,negated_conjecture,
    ( ~ agent(X0,sK28(X0),sK12(sK29(X0)))
    | ~ smoke(sK29(X0),sK14(sK29(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK12(sK29(X0)))
    | ~ of(X0,X1,sK12(sK29(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(sK29(X0)))
    | ~ sP2(X0)
    | ~ sP5(sK29(X0)) ) ).

cnf(u299,negated_conjecture,
    ( ~ agent(X3,sK14(X3),X5)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ smoke(X0,X1)
    | man(sK15(X3),sK37(sK15(X3)))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X2)
    | ~ forename(X3,X6)
    | ~ vincent_forename(X3,X6)
    | ~ man(X3,X5)
    | ~ of(X3,X6,X5)
    | ~ forename(X3,X7)
    | ~ vincent_forename(X3,X7)
    | ~ man(X3,X2)
    | ~ of(X3,X7,X2)
    | ~ forename(X3,X8)
    | ~ jules_forename(X3,X8)
    | ~ of(X3,X8,X2)
    | ~ sP5(X3) ) ).

cnf(u1149,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ man(sK34(X0),X1)
    | ~ sP4(sK34(X0)) ) ).

cnf(u876,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP0(sK34(X0),X1) ) ).

cnf(u823,negated_conjecture,
    ( ~ agent(X0,sK14(X0),sK9(sK15(X0)))
    | ~ smoke(sK15(X0),sK19(sK15(X0)))
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK9(sK15(X0)))
    | ~ of(X0,X1,sK9(sK15(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(sK15(X0)))
    | ~ sP5(X0)
    | ~ sP5(sK15(X0)) ) ).

cnf(u67,axiom,
    ( forename(X0,sK11(X0))
    | ~ sP5(X0) ) ).

cnf(u535,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | man(sK29(X0),sK37(sK29(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ sP0(sK34(X0),X1) ) ).

cnf(u1270,negated_conjecture,
    ( ~ theme(X0,X1,X2)
    | ~ agent(X0,X1,X3)
    | ~ proposition(X0,X2)
    | ~ actual_world(X0)
    | ~ accessible_world(X0,X2)
    | ~ present(X2,X4)
    | ~ agent(X2,X4,X3)
    | ~ smoke(X2,X4)
    | ~ event(X2,X4)
    | ~ think_believe_consider(X0,X1)
    | ~ present(X0,X1)
    | ~ vincent_forename(X0,sK11(X0))
    | ~ event(X0,X1)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ man(X0,X3)
    | ~ of(X0,X5,X3)
    | ~ forename(X0,X6)
    | ~ jules_forename(X0,X6)
    | ~ of(X0,X6,X3)
    | ~ sP5(X0) ) ).

cnf(u874,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK9(sK34(X0)))
    | ~ smoke(sK34(X0),sK19(sK34(X0)))
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK9(sK34(X0)))
    | ~ of(X0,X1,sK9(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(sK34(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP5(sK34(X0)) ) ).

cnf(u318,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK24(sK34(X0)))
    | ~ smoke(sK34(X0),sK33(sK34(X0)))
    | man(sK34(X0),sK37(sK34(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK24(sK34(X0)))
    | ~ of(X0,X1,sK24(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK24(sK34(X0)))
    | ~ sP2(X0)
    | ~ sP2(sK34(X0)) ) ).

cnf(u934,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK9(sK34(X0)))
    | ~ smoke(sK34(X0),sK19(sK34(X0)))
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK9(sK34(X0)))
    | ~ of(X0,X1,sK9(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(sK34(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP5(sK34(X0)) ) ).

cnf(u86,axiom,
    ( event(X0,sK33(X0))
    | ~ sP2(X0) ) ).

cnf(u541,negated_conjecture,
    ( ~ event(X6,sK21(X6,sK37(X6)))
    | ~ accessible_world(X2,X0)
    | ~ think_believe_consider(X2,X3)
    | ~ present(X2,X3)
    | ~ event(X2,X3)
    | ~ theme(X2,X3,X0)
    | ~ agent(X2,X3,X4)
    | ~ proposition(X2,X0)
    | ~ actual_world(X2)
    | ~ forename(X2,X5)
    | ~ jules_forename(X2,X5)
    | ~ of(X2,X5,sK17(X2))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X4)
    | ~ smoke(X0,X1)
    | ~ event(X0,X1)
    | ~ accessible_world(X2,X6)
    | ~ think_believe_consider(X2,X7)
    | ~ present(X2,X7)
    | ~ event(X2,X7)
    | ~ theme(X2,X7,X6)
    | ~ agent(X2,X7,X8)
    | ~ proposition(X2,X6)
    | ~ forename(X2,X9)
    | ~ vincent_forename(X2,X9)
    | ~ man(X2,X8)
    | ~ of(X2,X9,X8)
    | ~ forename(X2,X10)
    | ~ vincent_forename(X2,X10)
    | ~ man(X2,X4)
    | ~ of(X2,X10,X4)
    | ~ forename(X2,X11)
    | ~ jules_forename(X2,X11)
    | ~ of(X2,X11,X4)
    | ~ sP5(X2)
    | ~ sP4(X6) ) ).

cnf(u1354,negated_conjecture,
    ( ~ agent(X0,sK14(X0),sK12(sK15(X0)))
    | ~ actual_world(X0)
    | ~ smoke(sK15(X0),sK14(sK15(X0)))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK12(sK15(X0)))
    | ~ of(X0,X1,sK12(sK15(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(sK15(X0)))
    | ~ sP5(X0)
    | ~ sP5(sK15(X0)) ) ).

cnf(u41,axiom,
    ( accessible_world(X0,sK20(X0))
    | ~ sP5(X0) ) ).

cnf(u800,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X1)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ man(sK20(X0),X1)
    | ~ sP4(sK20(X0)) ) ).

cnf(u506,negated_conjecture,
    ( ~ agent(sK20(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ smoke(sK20(X0),X2)
    | man(sK29(X0),sK37(sK29(X0)))
    | ~ present(sK20(X0),X2)
    | ~ agent(X0,sK19(X0),X1)
    | ~ event(sK20(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP2(X0)
    | ~ sP5(X0) ) ).

cnf(u101,axiom,
    ( event(X0,sK28(X0))
    | ~ sP2(X0) ) ).

cnf(u1365,negated_conjecture,
    ( ~ sP0(sK15(X0),sK12(X0))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK12(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(X0))
    | ~ sP5(X0)
    | ~ actual_world(X0) ) ).

cnf(u1036,negated_conjecture,
    ( ~ sP3(sK15(X0),sK12(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK12(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(X0))
    | ~ sP5(X0)
    | man(sK15(X0),sK37(sK15(X0))) ) ).

cnf(u283,negated_conjecture,
    ( ~ agent(sK15(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ smoke(sK15(X0),X2)
    | man(sK34(X0),sK37(sK34(X0)))
    | ~ present(sK15(X0),X2)
    | ~ agent(X0,sK14(X0),X1)
    | ~ event(sK15(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP2(X0)
    | ~ sP5(X0) ) ).

cnf(u217,negated_conjecture,
    ( ~ theme(X3,X6,X5)
    | ~ agent(X0,X1,X2)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ smoke(X0,X1)
    | man(X5,sK37(X5))
    | ~ accessible_world(X3,X5)
    | ~ think_believe_consider(X3,X6)
    | ~ present(X3,X6)
    | ~ event(X3,X6)
    | ~ present(X0,X1)
    | ~ agent(X3,X6,X7)
    | ~ proposition(X3,X5)
    | ~ forename(X3,X8)
    | ~ vincent_forename(X3,X8)
    | ~ man(X3,X7)
    | ~ of(X3,X8,X7)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X2)
    | ~ of(X3,X9,X2)
    | ~ forename(X3,X10)
    | ~ jules_forename(X3,X10)
    | ~ of(X3,X10,X2)
    | ~ sP5(X3) ) ).

cnf(u104,axiom,
    ( proposition(X0,sK29(X0))
    | ~ sP2(X0) ) ).

cnf(u280,negated_conjecture,
    ( ~ agent(sK34(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ smoke(sK34(X0),X2)
    | man(sK34(X0),sK37(sK34(X0)))
    | ~ present(sK34(X0),X2)
    | ~ agent(X0,sK33(X0),X1)
    | ~ event(sK34(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP2(X0) ) ).

cnf(u1217,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ sP5(X0)
    | ~ man(sK20(X0),X1)
    | ~ sP4(sK20(X0)) ) ).

cnf(u176,negated_conjecture,
    ( ~ of(X3,X5,sK31(X3))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X2)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ forename(X3,X5)
    | ~ jules_forename(X3,X5)
    | ~ smoke(X0,X1)
    | man(X6,sK37(X6))
    | ~ accessible_world(X3,X6)
    | ~ think_believe_consider(X3,X7)
    | ~ present(X3,X7)
    | ~ event(X3,X7)
    | ~ theme(X3,X7,X6)
    | ~ agent(X3,X7,X8)
    | ~ proposition(X3,X6)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X8)
    | ~ of(X3,X9,X8)
    | ~ forename(X3,X10)
    | ~ vincent_forename(X3,X10)
    | ~ man(X3,X2)
    | ~ of(X3,X10,X2)
    | ~ forename(X3,X11)
    | ~ jules_forename(X3,X11)
    | ~ of(X3,X11,X2)
    | ~ sP2(X3) ) ).

cnf(u65,axiom,
    ( man(X0,sK12(X0))
    | ~ sP5(X0) ) ).

cnf(u820,negated_conjecture,
    ( ~ agent(X0,sK14(X0),sK26(sK15(X0)))
    | ~ smoke(sK15(X0),sK28(sK15(X0)))
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK26(sK15(X0)))
    | ~ of(X0,X1,sK26(sK15(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK26(sK15(X0)))
    | ~ sP5(X0)
    | ~ sP2(sK15(X0)) ) ).

cnf(u570,negated_conjecture,
    ( man(sK29(X0),sK37(sK29(X0)))
    | ~ actual_world(X0)
    | ~ sP2(X0) ) ).

cnf(u760,negated_conjecture,
    ( ~ agent(X0,sK14(X0),sK12(sK15(X0)))
    | ~ smoke(sK15(X0),sK14(sK15(X0)))
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK12(sK15(X0)))
    | ~ of(X0,X1,sK12(sK15(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(sK15(X0)))
    | ~ sP5(X0)
    | ~ sP5(sK15(X0)) ) ).

cnf(u71,axiom,
    ( vincent_forename(X0,sK10(X0))
    | ~ sP5(X0) ) ).

cnf(u968,negated_conjecture,
    ( ~ agent(X0,sK28(X0),X1)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ man(sK29(X0),X1) ) ).

cnf(u1039,negated_conjecture,
    ( ~ man(sK15(X0),sK12(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK12(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(X0))
    | ~ sP5(X0)
    | man(sK15(X0),sK37(sK15(X0))) ) ).

cnf(u931,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK26(sK34(X0)))
    | ~ smoke(sK34(X0),sK28(sK34(X0)))
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK26(sK34(X0)))
    | ~ of(X0,X1,sK26(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK26(sK34(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP2(sK34(X0)) ) ).

cnf(u878,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP3(sK34(X0),X1) ) ).

cnf(u100,axiom,
    ( present(X0,sK28(X0))
    | ~ sP2(X0) ) ).

cnf(u74,axiom,
    ( smoke(X0,sK21(X0,X1))
    | ~ man(X0,X1)
    | ~ sP4(X0) ) ).

cnf(u529,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK24(sK34(X0)))
    | ~ smoke(sK34(X0),sK33(sK34(X0)))
    | man(sK29(X0),sK37(sK29(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK24(sK34(X0)))
    | ~ of(X0,X1,sK24(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK24(sK34(X0)))
    | ~ sP2(X0)
    | ~ sP2(sK34(X0)) ) ).

cnf(u937,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ man(sK34(X0),X1)
    | ~ sP1(sK34(X0)) ) ).

cnf(u381,negated_conjecture,
    ( ~ present(X6,sK21(X6,sK37(X6)))
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ forename(X3,X5)
    | ~ jules_forename(X3,X5)
    | ~ of(X3,X5,sK17(X3))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X2)
    | ~ smoke(X0,X1)
    | ~ event(X6,sK21(X6,sK37(X6)))
    | ~ accessible_world(X3,X6)
    | ~ think_believe_consider(X3,X7)
    | ~ present(X3,X7)
    | ~ event(X3,X7)
    | ~ theme(X3,X7,X6)
    | ~ agent(X3,X7,X8)
    | ~ proposition(X3,X6)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X8)
    | ~ of(X3,X9,X8)
    | ~ forename(X3,X10)
    | ~ vincent_forename(X3,X10)
    | ~ man(X3,X2)
    | ~ of(X3,X10,X2)
    | ~ forename(X3,X11)
    | ~ jules_forename(X3,X11)
    | ~ of(X3,X11,X2)
    | ~ sP5(X3)
    | ~ sP4(X6) ) ).

cnf(u335,negated_conjecture,
    ( ~ of(X0,X2,sK24(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK24(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | man(sK34(X0),sK37(sK34(X0)))
    | ~ sP2(X0) ) ).

cnf(u761,negated_conjecture,
    ( ~ agent(X0,sK14(X0),X1)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP0(sK15(X0),X1) ) ).

cnf(u89,axiom,
    ( proposition(X0,sK34(X0))
    | ~ sP2(X0) ) ).

cnf(u386,negated_conjecture,
    ( ~ of(X2,X5,sK26(X2))
    | ~ accessible_world(X2,X0)
    | ~ think_believe_consider(X2,X3)
    | ~ present(X2,X3)
    | ~ event(X2,X3)
    | ~ theme(X2,X3,X0)
    | ~ agent(X2,X3,X4)
    | ~ proposition(X2,X0)
    | ~ actual_world(X2)
    | ~ smoke(X0,X1)
    | man(sK29(X2),sK37(sK29(X2)))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X4)
    | ~ forename(X2,X5)
    | ~ vincent_forename(X2,X5)
    | ~ event(X0,X1)
    | ~ forename(X2,X6)
    | ~ vincent_forename(X2,X6)
    | ~ man(X2,X4)
    | ~ of(X2,X6,X4)
    | ~ forename(X2,X7)
    | ~ jules_forename(X2,X7)
    | ~ of(X2,X7,X4)
    | ~ sP2(X2) ) ).

cnf(u799,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X1)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP3(sK20(X0),X1) ) ).

cnf(u1289,negated_conjecture,
    ( ~ agent(sK15(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ present(sK15(X0),X2)
    | ~ agent(X0,sK14(X0),X1)
    | ~ smoke(sK15(X0),X2)
    | ~ event(sK15(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP5(X0) ) ).

cnf(u48,axiom,
    ( be(X0,sK18(X0),sK17(X0),sK17(X0))
    | ~ sP5(X0) ) ).

cnf(u996,negated_conjecture,
    ( ~ agent(sK20(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ present(sK20(X0),X2)
    | ~ smoke(sK20(X0),X2)
    | ~ agent(X0,sK19(X0),X1)
    | ~ event(sK20(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP2(X0)
    | ~ sP5(X0) ) ).

cnf(u756,negated_conjecture,
    ( ~ agent(X0,sK14(X0),sK26(sK15(X0)))
    | ~ smoke(sK15(X0),sK28(sK15(X0)))
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK26(sK15(X0)))
    | ~ of(X0,X1,sK26(sK15(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK26(sK15(X0)))
    | ~ sP5(X0)
    | ~ sP2(sK15(X0)) ) ).

cnf(u108,axiom,
    ( of(X0,sK27(X0),sK26(X0))
    | ~ sP2(X0) ) ).

cnf(u1359,negated_conjecture,
    ( ~ agent(X0,sK14(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ man(sK15(X0),X1) ) ).

cnf(u796,negated_conjecture,
    ( ~ agent(X0,sK19(X0),sK12(sK20(X0)))
    | ~ smoke(sK20(X0),sK14(sK20(X0)))
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK12(sK20(X0)))
    | ~ of(X0,X1,sK12(sK20(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(sK20(X0)))
    | ~ sP5(X0)
    | ~ sP5(sK20(X0)) ) ).

cnf(u212,negated_conjecture,
    ( ~ agent(X3,sK19(X3),X5)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ smoke(X0,X1)
    | man(sK20(X3),sK37(sK20(X3)))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X2)
    | ~ forename(X3,X6)
    | ~ vincent_forename(X3,X6)
    | ~ man(X3,X5)
    | ~ of(X3,X6,X5)
    | ~ forename(X3,X7)
    | ~ vincent_forename(X3,X7)
    | ~ man(X3,X2)
    | ~ of(X3,X7,X2)
    | ~ forename(X3,X8)
    | ~ jules_forename(X3,X8)
    | ~ of(X3,X8,X2)
    | ~ sP2(X3)
    | ~ sP5(X3) ) ).

cnf(u323,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK12(sK34(X0)))
    | ~ smoke(sK34(X0),sK14(sK34(X0)))
    | man(sK34(X0),sK37(sK34(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK12(sK34(X0)))
    | ~ of(X0,X1,sK12(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(sK34(X0)))
    | ~ sP2(X0)
    | ~ sP5(sK34(X0)) ) ).

cnf(u115,axiom,
    ( of(X0,sK23(X0),sK24(X0))
    | ~ sP2(X0) ) ).

cnf(u997,negated_conjecture,
    ( ~ agent(sK15(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ present(sK15(X0),X2)
    | ~ smoke(sK15(X0),X2)
    | ~ agent(X0,sK14(X0),X1)
    | ~ event(sK15(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP2(X0)
    | ~ sP5(X0) ) ).

cnf(u431,negated_conjecture,
    ( ~ agent(X2,sK19(X2),X5)
    | ~ accessible_world(X2,X0)
    | ~ think_believe_consider(X2,X3)
    | ~ present(X2,X3)
    | ~ event(X2,X3)
    | ~ theme(X2,X3,X0)
    | ~ agent(X2,X3,X4)
    | ~ proposition(X2,X0)
    | ~ actual_world(X2)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ agent(X0,X1,X4)
    | ~ event(X0,X1)
    | ~ forename(X2,X6)
    | ~ vincent_forename(X2,X6)
    | ~ man(X2,X5)
    | ~ of(X2,X6,X5)
    | ~ forename(X2,X7)
    | ~ vincent_forename(X2,X7)
    | ~ man(X2,X4)
    | ~ of(X2,X7,X4)
    | ~ forename(X2,X8)
    | ~ jules_forename(X2,X8)
    | ~ of(X2,X8,X4)
    | ~ sP2(X2)
    | ~ sP1(sK20(X2))
    | ~ sP5(X2) ) ).

cnf(u187,negated_conjecture,
    ( ~ agent(X6,X7,sK37(X6))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X2)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ forename(X3,X5)
    | ~ jules_forename(X3,X5)
    | ~ of(X3,X5,sK17(X3))
    | ~ smoke(X6,X7)
    | ~ present(X6,X7)
    | ~ smoke(X0,X1)
    | ~ event(X6,X7)
    | ~ accessible_world(X3,X6)
    | ~ think_believe_consider(X3,X8)
    | ~ present(X3,X8)
    | ~ event(X3,X8)
    | ~ theme(X3,X8,X6)
    | ~ agent(X3,X8,X9)
    | ~ proposition(X3,X6)
    | ~ forename(X3,X10)
    | ~ vincent_forename(X3,X10)
    | ~ man(X3,X9)
    | ~ of(X3,X10,X9)
    | ~ forename(X3,X11)
    | ~ vincent_forename(X3,X11)
    | ~ man(X3,X2)
    | ~ of(X3,X11,X2)
    | ~ forename(X3,X12)
    | ~ jules_forename(X3,X12)
    | ~ of(X3,X12,X2)
    | ~ sP5(X3) ) ).

cnf(u455,negated_conjecture,
    ( ~ agent(X2,sK14(X2),X5)
    | ~ accessible_world(X2,X0)
    | ~ think_believe_consider(X2,X3)
    | ~ present(X2,X3)
    | ~ event(X2,X3)
    | ~ theme(X2,X3,X0)
    | ~ agent(X2,X3,X4)
    | ~ proposition(X2,X0)
    | ~ actual_world(X2)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ agent(X0,X1,X4)
    | ~ event(X0,X1)
    | ~ forename(X2,X6)
    | ~ vincent_forename(X2,X6)
    | ~ man(X2,X5)
    | ~ of(X2,X6,X5)
    | ~ forename(X2,X7)
    | ~ vincent_forename(X2,X7)
    | ~ man(X2,X4)
    | ~ of(X2,X7,X4)
    | ~ forename(X2,X8)
    | ~ jules_forename(X2,X8)
    | ~ of(X2,X8,X4)
    | ~ sP2(X2)
    | ~ sP5(X2) ) ).

cnf(u907,negated_conjecture,
    ( ~ agent(X0,sK28(X0),X1)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ man(sK29(X0),X1)
    | ~ sP4(sK29(X0)) ) ).

cnf(u935,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK12(sK34(X0)))
    | ~ smoke(sK34(X0),sK14(sK34(X0)))
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK12(sK34(X0)))
    | ~ of(X0,X1,sK12(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(sK34(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP5(sK34(X0)) ) ).

cnf(u797,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X1)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP0(sK20(X0),X1) ) ).

cnf(u967,negated_conjecture,
    ( ~ agent(X0,sK28(X0),X1)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ man(sK29(X0),X1)
    | ~ sP4(sK29(X0)) ) ).

cnf(u759,negated_conjecture,
    ( ~ agent(X0,sK14(X0),sK9(sK15(X0)))
    | ~ smoke(sK15(X0),sK19(sK15(X0)))
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK9(sK15(X0)))
    | ~ of(X0,X1,sK9(sK15(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(sK15(X0)))
    | ~ sP5(X0)
    | ~ sP5(sK15(X0)) ) ).

cnf(u78,axiom,
    ( smoke(X0,sK22(X0,X1))
    | ~ sP3(X0,X1) ) ).

cnf(u533,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK9(sK34(X0)))
    | ~ smoke(sK34(X0),sK19(sK34(X0)))
    | man(sK29(X0),sK37(sK29(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK9(sK34(X0)))
    | ~ of(X0,X1,sK9(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(sK34(X0)))
    | ~ sP2(X0)
    | ~ sP5(sK34(X0)) ) ).

cnf(u357,negated_conjecture,
    ( man(sK34(X0),sK37(sK34(X0)))
    | ~ actual_world(X0)
    | ~ sP2(X0) ) ).

cnf(u369,negated_conjecture,
    ( ~ sP3(X5,sK37(X5))
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ accessible_world(X3,X5)
    | ~ think_believe_consider(X3,X6)
    | ~ present(X3,X6)
    | ~ event(X3,X6)
    | ~ theme(X3,X6,X5)
    | ~ agent(X3,X6,X7)
    | ~ proposition(X3,X5)
    | ~ forename(X3,X8)
    | ~ vincent_forename(X3,X8)
    | ~ man(X3,X7)
    | ~ of(X3,X8,X7)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X2)
    | ~ of(X3,X9,X2)
    | ~ forename(X3,X10)
    | ~ jules_forename(X3,X10)
    | ~ of(X3,X10,X2)
    | ~ sP5(X3)
    | ~ agent(X0,X1,X2) ) ).

cnf(u765,negated_conjecture,
    ( ~ agent(X0,sK14(X0),X1)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ man(sK15(X0),X1) ) ).

cnf(u429,negated_conjecture,
    ( ~ agent(X2,sK33(X2),X5)
    | ~ accessible_world(X2,X0)
    | ~ think_believe_consider(X2,X3)
    | ~ present(X2,X3)
    | ~ event(X2,X3)
    | ~ theme(X2,X3,X0)
    | ~ agent(X2,X3,X4)
    | ~ proposition(X2,X0)
    | ~ actual_world(X2)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ agent(X0,X1,X4)
    | ~ event(X0,X1)
    | ~ forename(X2,X6)
    | ~ vincent_forename(X2,X6)
    | ~ man(X2,X5)
    | ~ of(X2,X6,X5)
    | ~ forename(X2,X7)
    | ~ vincent_forename(X2,X7)
    | ~ man(X2,X4)
    | ~ of(X2,X7,X4)
    | ~ forename(X2,X8)
    | ~ jules_forename(X2,X8)
    | ~ of(X2,X8,X4)
    | ~ sP2(X2)
    | ~ sP1(sK34(X2)) ) ).

cnf(u93,axiom,
    ( forename(X0,sK30(X0))
    | ~ sP2(X0) ) ).

cnf(u660,negated_conjecture,
    ( ~ agent(X0,sK19(X0),sK26(sK20(X0)))
    | ~ smoke(sK20(X0),sK28(sK20(X0)))
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK26(sK20(X0)))
    | ~ of(X0,X1,sK26(sK20(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK26(sK20(X0)))
    | ~ sP5(X0)
    | ~ sP2(sK20(X0)) ) ).

cnf(u994,negated_conjecture,
    ( ~ agent(sK34(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ present(sK34(X0),X2)
    | ~ smoke(sK34(X0),X2)
    | ~ agent(X0,sK33(X0),X1)
    | ~ event(sK34(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP2(X0) ) ).

cnf(u1043,negated_conjecture,
    ( ~ of(X0,X2,sK24(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK24(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0) ) ).

cnf(u52,axiom,
    ( jules_forename(X0,sK16(X0))
    | ~ sP5(X0) ) ).

cnf(u96,axiom,
    ( of(X0,sK30(X0),sK31(X0))
    | ~ sP2(X0) ) ).

cnf(u432,negated_conjecture,
    ( ~ agent(X2,sK14(X2),X5)
    | ~ accessible_world(X2,X0)
    | ~ think_believe_consider(X2,X3)
    | ~ present(X2,X3)
    | ~ event(X2,X3)
    | ~ theme(X2,X3,X0)
    | ~ agent(X2,X3,X4)
    | ~ proposition(X2,X0)
    | ~ actual_world(X2)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ agent(X0,X1,X4)
    | ~ event(X0,X1)
    | ~ forename(X2,X6)
    | ~ vincent_forename(X2,X6)
    | ~ man(X2,X5)
    | ~ of(X2,X6,X5)
    | ~ forename(X2,X7)
    | ~ vincent_forename(X2,X7)
    | ~ man(X2,X4)
    | ~ of(X2,X7,X4)
    | ~ forename(X2,X8)
    | ~ jules_forename(X2,X8)
    | ~ of(X2,X8,X4)
    | ~ sP2(X2)
    | ~ sP1(sK15(X2))
    | ~ sP5(X2) ) ).

cnf(u47,axiom,
    ( proposition(X0,sK20(X0))
    | ~ sP5(X0) ) ).

cnf(u59,axiom,
    ( event(X0,sK14(X0))
    | ~ sP5(X0) ) ).

cnf(u504,negated_conjecture,
    ( ~ agent(sK34(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ smoke(sK34(X0),X2)
    | man(sK29(X0),sK37(sK29(X0)))
    | ~ present(sK34(X0),X2)
    | ~ agent(X0,sK33(X0),X1)
    | ~ event(sK34(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP2(X0) ) ).

cnf(u327,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | man(sK34(X0),sK37(sK34(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ man(sK34(X0),X1)
    | ~ sP4(sK34(X0)) ) ).

cnf(u119,axiom,
    ( event(X0,sK35(X0,X1))
    | ~ man(X0,X1)
    | ~ sP1(X0) ) ).

cnf(u562,negated_conjecture,
    ( ~ theme(X0,X2,X1)
    | ~ think_believe_consider(X0,X2)
    | ~ present(X0,X2)
    | ~ event(X0,X2)
    | ~ accessible_world(X0,X1)
    | ~ agent(X0,X2,X3)
    | ~ proposition(X0,X1)
    | ~ actual_world(X0)
    | ~ smoke(X1,X4)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ present(X1,X4)
    | ~ agent(X1,X4,X3)
    | ~ vincent_forename(X0,sK11(X0))
    | ~ event(X1,X4)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ man(X0,X3)
    | ~ of(X0,X5,X3)
    | ~ forename(X0,X6)
    | ~ jules_forename(X0,X6)
    | ~ of(X0,X6,X3)
    | ~ sP5(X0) ) ).

cnf(u1016,negated_conjecture,
    ( ~ sP0(sK15(X0),sK12(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK12(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(X0))
    | ~ sP5(X0)
    | man(sK15(X0),sK37(sK15(X0))) ) ).

cnf(u851,negated_conjecture,
    ( ~ man(sK15(X0),sK12(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK12(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(X0))
    | ~ sP5(X0)
    | man(sK20(X0),sK37(sK20(X0))) ) ).

cnf(u50,axiom,
    ( man(X0,sK17(X0))
    | ~ sP5(X0) ) ).

cnf(u939,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ man(sK34(X0),X1)
    | ~ sP4(sK34(X0)) ) ).

cnf(u666,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X1)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ man(sK20(X0),X1)
    | ~ sP1(sK20(X0)) ) ).

cnf(u694,negated_conjecture,
    ( ~ agent(sK15(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ smoke(sK15(X0),X2)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ present(sK15(X0),X2)
    | ~ agent(X0,sK14(X0),X1)
    | ~ event(sK15(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP5(X0) ) ).

cnf(u122,axiom,
    ( agent(X0,sK36(X0,X1),X1)
    | ~ sP0(X0,X1) ) ).

cnf(u298,negated_conjecture,
    ( ~ agent(X3,sK19(X3),X5)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ smoke(X0,X1)
    | man(sK20(X3),sK37(sK20(X3)))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X2)
    | ~ forename(X3,X6)
    | ~ vincent_forename(X3,X6)
    | ~ man(X3,X5)
    | ~ of(X3,X6,X5)
    | ~ forename(X3,X7)
    | ~ vincent_forename(X3,X7)
    | ~ man(X3,X2)
    | ~ of(X3,X7,X2)
    | ~ forename(X3,X8)
    | ~ jules_forename(X3,X8)
    | ~ of(X3,X8,X2)
    | ~ sP5(X3) ) ).

cnf(u538,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | man(sK29(X0),sK37(sK29(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ man(sK34(X0),X1)
    | ~ sP4(sK34(X0)) ) ).

cnf(u1215,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ sP5(X0)
    | ~ man(sK20(X0),X1)
    | ~ sP1(sK20(X0)) ) ).

cnf(u637,negated_conjecture,
    ( ~ agent(sK34(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ smoke(sK34(X0),X2)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ present(sK34(X0),X2)
    | ~ agent(X0,sK33(X0),X1)
    | ~ event(sK34(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP5(X0)
    | ~ sP2(X0) ) ).

cnf(u114,axiom,
    ( jules_forename(X0,sK23(X0))
    | ~ sP2(X0) ) ).

cnf(u402,negated_conjecture,
    ( ~ of(X2,X5,sK12(X2))
    | ~ accessible_world(X2,X0)
    | ~ think_believe_consider(X2,X3)
    | ~ present(X2,X3)
    | ~ event(X2,X3)
    | ~ theme(X2,X3,X0)
    | ~ agent(X2,X3,X4)
    | ~ proposition(X2,X0)
    | ~ actual_world(X2)
    | ~ smoke(X0,X1)
    | man(sK15(X2),sK37(sK15(X2)))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X4)
    | ~ forename(X2,X5)
    | ~ vincent_forename(X2,X5)
    | ~ event(X0,X1)
    | ~ forename(X2,X6)
    | ~ vincent_forename(X2,X6)
    | ~ man(X2,X4)
    | ~ of(X2,X6,X4)
    | ~ forename(X2,X7)
    | ~ jules_forename(X2,X7)
    | ~ of(X2,X7,X4)
    | ~ sP5(X2) ) ).

cnf(u659,negated_conjecture,
    ( ~ agent(X0,sK19(X0),sK24(sK20(X0)))
    | ~ smoke(sK20(X0),sK33(sK20(X0)))
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK24(sK20(X0)))
    | ~ of(X0,X1,sK24(sK20(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK24(sK20(X0)))
    | ~ sP5(X0)
    | ~ sP2(sK20(X0)) ) ).

cnf(u1316,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP0(sK20(X0),X1) ) ).

cnf(u69,axiom,
    ( of(X0,sK11(X0),sK12(X0))
    | ~ sP5(X0) ) ).

cnf(u819,negated_conjecture,
    ( ~ agent(X0,sK14(X0),sK24(sK15(X0)))
    | ~ smoke(sK15(X0),sK33(sK15(X0)))
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK24(sK15(X0)))
    | ~ of(X0,X1,sK24(sK15(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK24(sK15(X0)))
    | ~ sP5(X0)
    | ~ sP2(sK15(X0)) ) ).

cnf(u1073,negated_conjecture,
    ( ~ of(X0,X2,sK24(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK24(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0) ) ).

cnf(u72,axiom,
    ( man(X0,sK9(X0))
    | ~ sP5(X0) ) ).

cnf(u376,negated_conjecture,
    ( ~ present(X6,sK35(X6,sK37(X6)))
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ forename(X3,X5)
    | ~ jules_forename(X3,X5)
    | ~ of(X3,X5,sK17(X3))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X2)
    | ~ smoke(X0,X1)
    | ~ event(X6,sK35(X6,sK37(X6)))
    | ~ accessible_world(X3,X6)
    | ~ think_believe_consider(X3,X7)
    | ~ present(X3,X7)
    | ~ event(X3,X7)
    | ~ theme(X3,X7,X6)
    | ~ agent(X3,X7,X8)
    | ~ proposition(X3,X6)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X8)
    | ~ of(X3,X9,X8)
    | ~ forename(X3,X10)
    | ~ vincent_forename(X3,X10)
    | ~ man(X3,X2)
    | ~ of(X3,X10,X2)
    | ~ forename(X3,X11)
    | ~ jules_forename(X3,X11)
    | ~ of(X3,X11,X2)
    | ~ sP5(X3)
    | ~ sP1(X6) ) ).

cnf(u958,negated_conjecture,
    ( ~ agent(X0,sK28(X0),sK24(sK29(X0)))
    | ~ smoke(sK29(X0),sK33(sK29(X0)))
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK24(sK29(X0)))
    | ~ of(X0,X1,sK24(sK29(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK24(sK29(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP2(sK29(X0)) ) ).

cnf(u1374,negated_conjecture,
    ( ~ man(sK20(X0),sK9(X0))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK9(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(X0))
    | ~ sP5(X0)
    | ~ actual_world(X0)
    | ~ sP1(sK20(X0)) ) ).

cnf(u903,negated_conjecture,
    ( ~ agent(X0,sK28(X0),sK12(sK29(X0)))
    | ~ smoke(sK29(X0),sK14(sK29(X0)))
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK12(sK29(X0)))
    | ~ of(X0,X1,sK12(sK29(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(sK29(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP5(sK29(X0)) ) ).

cnf(u832,negated_conjecture,
    ( ~ sP3(sK15(X0),sK12(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK12(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(X0))
    | ~ sP5(X0)
    | man(sK20(X0),sK37(sK20(X0))) ) ).

cnf(u107,axiom,
    ( man(X0,sK26(X0))
    | ~ sP2(X0) ) ).

cnf(u1214,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ sP5(X0)
    | ~ sP0(sK20(X0),X1) ) ).

cnf(u1153,negated_conjecture,
    ( ~ of(X0,X2,sK24(X0))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK24(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ actual_world(X0)
    | ~ sP2(X0) ) ).

cnf(u1182,negated_conjecture,
    ( ~ agent(X0,sK28(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ man(sK29(X0),X1) ) ).

cnf(u54,axiom,
    ( of(X0,sK16(X0),sK17(X0))
    | ~ sP5(X0) ) ).

cnf(u211,negated_conjecture,
    ( ~ agent(X3,sK28(X3),X5)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ smoke(X0,X1)
    | man(sK29(X3),sK37(sK29(X3)))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X2)
    | ~ forename(X3,X6)
    | ~ vincent_forename(X3,X6)
    | ~ man(X3,X5)
    | ~ of(X3,X6,X5)
    | ~ forename(X3,X7)
    | ~ vincent_forename(X3,X7)
    | ~ man(X3,X2)
    | ~ of(X3,X7,X2)
    | ~ forename(X3,X8)
    | ~ jules_forename(X3,X8)
    | ~ of(X3,X8,X2)
    | ~ sP2(X3) ) ).

cnf(u899,negated_conjecture,
    ( ~ agent(X0,sK28(X0),sK26(sK29(X0)))
    | ~ smoke(sK29(X0),sK28(sK29(X0)))
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK26(sK29(X0)))
    | ~ of(X0,X1,sK26(sK29(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK26(sK29(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP2(sK29(X0)) ) ).

cnf(u98,axiom,
    ( accessible_world(X0,sK29(X0))
    | ~ sP2(X0) ) ).

cnf(u1031,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X5)
    | ~ event(X0,X1)
    | ~ theme(X0,X1,X2)
    | ~ agent(X0,X1,X3)
    | ~ proposition(X0,X2)
    | ~ actual_world(X0)
    | ~ accessible_world(X0,X2)
    | ~ present(X2,X4)
    | ~ agent(X2,X4,X3)
    | ~ smoke(X2,X4)
    | ~ event(X2,X4)
    | ~ think_believe_consider(X0,X1)
    | ~ present(X0,X1)
    | ~ forename(X0,X6)
    | ~ vincent_forename(X0,X6)
    | ~ man(X0,X5)
    | ~ of(X0,X6,X5)
    | ~ forename(X0,X7)
    | ~ vincent_forename(X0,X7)
    | ~ man(X0,X3)
    | ~ of(X0,X7,X3)
    | ~ forename(X0,X8)
    | ~ jules_forename(X0,X8)
    | ~ of(X0,X8,X3)
    | ~ sP5(X0)
    | ~ sP4(sK20(X0)) ) ).

cnf(u930,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK24(sK34(X0)))
    | ~ smoke(sK34(X0),sK33(sK34(X0)))
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK24(sK34(X0)))
    | ~ of(X0,X1,sK24(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK24(sK34(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP2(sK34(X0)) ) ).

cnf(u1213,negated_conjecture,
    ( ~ agent(X0,sK19(X0),sK12(sK20(X0)))
    | ~ smoke(sK20(X0),sK14(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK12(sK20(X0)))
    | ~ of(X0,X1,sK12(sK20(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(sK20(X0)))
    | ~ sP2(X0)
    | ~ sP5(X0)
    | ~ sP5(sK20(X0)) ) ).

cnf(u346,negated_conjecture,
    ( ~ of(X0,X1,sK24(X0))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ actual_world(X0)
    | man(sK34(X0),sK37(sK34(X0)))
    | ~ sP2(X0) ) ).

cnf(u962,negated_conjecture,
    ( ~ agent(X0,sK28(X0),sK9(sK29(X0)))
    | ~ smoke(sK29(X0),sK19(sK29(X0)))
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK9(sK29(X0)))
    | ~ of(X0,X1,sK9(sK29(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(sK29(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP5(sK29(X0)) ) ).

cnf(u113,axiom,
    ( forename(X0,sK23(X0))
    | ~ sP2(X0) ) ).

cnf(u908,negated_conjecture,
    ( ~ agent(X0,sK28(X0),X1)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ man(sK29(X0),X1) ) ).

cnf(u1145,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK12(sK34(X0)))
    | ~ smoke(sK34(X0),sK14(sK34(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK12(sK34(X0)))
    | ~ of(X0,X1,sK12(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK12(sK34(X0)))
    | ~ sP2(X0)
    | ~ sP5(sK34(X0)) ) ).

cnf(u186,negated_conjecture,
    ( ~ agent(X6,X7,sK37(X6))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X2)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ forename(X3,X5)
    | ~ jules_forename(X3,X5)
    | ~ of(X3,X5,sK31(X3))
    | ~ smoke(X6,X7)
    | ~ present(X6,X7)
    | ~ smoke(X0,X1)
    | ~ event(X6,X7)
    | ~ accessible_world(X3,X6)
    | ~ think_believe_consider(X3,X8)
    | ~ present(X3,X8)
    | ~ event(X3,X8)
    | ~ theme(X3,X8,X6)
    | ~ agent(X3,X8,X9)
    | ~ proposition(X3,X6)
    | ~ forename(X3,X10)
    | ~ vincent_forename(X3,X10)
    | ~ man(X3,X9)
    | ~ of(X3,X10,X9)
    | ~ forename(X3,X11)
    | ~ vincent_forename(X3,X11)
    | ~ man(X3,X2)
    | ~ of(X3,X11,X2)
    | ~ forename(X3,X12)
    | ~ jules_forename(X3,X12)
    | ~ of(X3,X12,X2)
    | ~ sP2(X3) ) ).

cnf(u453,negated_conjecture,
    ( ~ agent(X2,sK19(X2),X5)
    | ~ accessible_world(X2,X0)
    | ~ think_believe_consider(X2,X3)
    | ~ present(X2,X3)
    | ~ event(X2,X3)
    | ~ theme(X2,X3,X0)
    | ~ agent(X2,X3,X4)
    | ~ proposition(X2,X0)
    | ~ actual_world(X2)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ agent(X0,X1,X4)
    | ~ event(X0,X1)
    | ~ forename(X2,X6)
    | ~ vincent_forename(X2,X6)
    | ~ man(X2,X5)
    | ~ of(X2,X6,X5)
    | ~ forename(X2,X7)
    | ~ vincent_forename(X2,X7)
    | ~ man(X2,X4)
    | ~ of(X2,X7,X4)
    | ~ forename(X2,X8)
    | ~ jules_forename(X2,X8)
    | ~ of(X2,X8,X4)
    | ~ sP2(X2)
    | ~ sP4(sK20(X2))
    | ~ sP5(X2) ) ).

cnf(u245,negated_conjecture,
    ( ~ theme(X0,X2,X1)
    | ~ think_believe_consider(X0,X2)
    | ~ present(X0,X2)
    | ~ event(X0,X2)
    | ~ accessible_world(X0,X1)
    | ~ agent(X0,X2,X3)
    | ~ proposition(X0,X1)
    | ~ actual_world(X0)
    | ~ smoke(X1,X4)
    | man(sK34(X0),sK37(sK34(X0)))
    | ~ present(X1,X4)
    | ~ agent(X1,X4,X3)
    | ~ event(X1,X4)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ man(X0,X3)
    | ~ of(X0,X5,X3)
    | ~ forename(X0,X6)
    | ~ jules_forename(X0,X6)
    | ~ of(X0,X6,X3)
    | ~ sP2(X0) ) ).

cnf(u1172,negated_conjecture,
    ( ~ agent(X0,sK28(X0),sK24(sK29(X0)))
    | ~ smoke(sK29(X0),sK33(sK29(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK24(sK29(X0)))
    | ~ of(X0,X1,sK24(sK29(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK24(sK29(X0)))
    | ~ sP2(X0)
    | ~ sP2(sK29(X0)) ) ).

cnf(u76,axiom,
    ( agent(X0,sK21(X0,X1),X1)
    | ~ man(X0,X1)
    | ~ sP4(X0) ) ).

cnf(u1078,negated_conjecture,
    ( ~ of(X0,X1,sK24(X0))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ actual_world(X0)
    | ~ jules_forename(X0,sK25(X0))
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0) ) ).

cnf(u556,negated_conjecture,
    ( ~ of(X0,X1,sK24(X0))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ actual_world(X0)
    | man(sK29(X0),sK37(sK29(X0)))
    | ~ sP2(X0) ) ).

cnf(u1104,negated_conjecture,
    ( ~ man(sK20(X0),sK9(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK9(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(X0))
    | ~ sP5(X0)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ sP1(sK20(X0)) ) ).

cnf(u829,negated_conjecture,
    ( ~ agent(X0,sK14(X0),X1)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ man(sK15(X0),X1) ) ).

cnf(u600,negated_conjecture,
    ( ~ of(X0,X5,sK9(X0))
    | ~ think_believe_consider(X0,X2)
    | ~ present(X0,X2)
    | ~ event(X0,X2)
    | ~ theme(X0,X2,X1)
    | ~ agent(X0,X2,X3)
    | ~ proposition(X0,X1)
    | ~ actual_world(X0)
    | ~ present(X1,X4)
    | ~ smoke(X1,X4)
    | ~ agent(X1,X4,X3)
    | ~ event(X1,X4)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ accessible_world(X0,X1)
    | ~ forename(X0,X6)
    | ~ vincent_forename(X0,X6)
    | ~ man(X0,X3)
    | ~ of(X0,X6,X3)
    | ~ forename(X0,X7)
    | ~ jules_forename(X0,X7)
    | ~ of(X0,X7,X3)
    | ~ sP2(X0)
    | ~ sP4(sK20(X0))
    | ~ sP5(X0) ) ).

cnf(u827,negated_conjecture,
    ( ~ agent(X0,sK14(X0),X1)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP3(sK15(X0),X1) ) ).

cnf(u1271,negated_conjecture,
    ( ~ theme(X0,X1,X2)
    | ~ agent(X0,X1,X3)
    | ~ proposition(X0,X2)
    | ~ actual_world(X0)
    | ~ accessible_world(X0,X2)
    | ~ present(X2,X4)
    | ~ agent(X2,X4,X3)
    | ~ smoke(X2,X4)
    | ~ event(X2,X4)
    | ~ think_believe_consider(X0,X1)
    | ~ present(X0,X1)
    | ~ event(X0,X1)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ man(X0,X3)
    | ~ of(X0,X5,X3)
    | ~ forename(X0,X6)
    | ~ jules_forename(X0,X6)
    | ~ of(X0,X6,X3)
    | ~ sP5(X0) ) ).

cnf(u936,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP0(sK34(X0),X1) ) ).

cnf(u83,axiom,
    ( accessible_world(X0,sK34(X0))
    | ~ sP2(X0) ) ).

cnf(u1288,negated_conjecture,
    ( ~ agent(sK20(X0),X2,X1)
    | ~ actual_world(X0)
    | ~ present(sK20(X0),X2)
    | ~ agent(X0,sK19(X0),X1)
    | ~ smoke(sK20(X0),X2)
    | ~ event(sK20(X0),X2)
    | ~ forename(X0,X3)
    | ~ vincent_forename(X0,X3)
    | ~ man(X0,X1)
    | ~ of(X0,X3,X1)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ of(X0,X4,X1)
    | ~ sP5(X0) ) ).

cnf(u563,negated_conjecture,
    ( ~ theme(X0,X2,X1)
    | ~ think_believe_consider(X0,X2)
    | ~ present(X0,X2)
    | ~ event(X0,X2)
    | ~ accessible_world(X0,X1)
    | ~ agent(X0,X2,X3)
    | ~ proposition(X0,X1)
    | ~ actual_world(X0)
    | ~ smoke(X1,X4)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ present(X1,X4)
    | ~ agent(X1,X4,X3)
    | ~ event(X1,X4)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ man(X0,X3)
    | ~ of(X0,X5,X3)
    | ~ forename(X0,X6)
    | ~ jules_forename(X0,X6)
    | ~ of(X0,X6,X3)
    | ~ sP5(X0) ) ).

cnf(u586,negated_conjecture,
    ( ~ of(X0,X5,sK24(X0))
    | ~ think_believe_consider(X0,X2)
    | ~ present(X0,X2)
    | ~ event(X0,X2)
    | ~ theme(X0,X2,X1)
    | ~ agent(X0,X2,X3)
    | ~ proposition(X0,X1)
    | ~ actual_world(X0)
    | ~ present(X1,X4)
    | ~ smoke(X1,X4)
    | ~ agent(X1,X4,X3)
    | ~ event(X1,X4)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ accessible_world(X0,X1)
    | ~ forename(X0,X6)
    | ~ vincent_forename(X0,X6)
    | ~ man(X0,X3)
    | ~ of(X0,X6,X3)
    | ~ forename(X0,X7)
    | ~ jules_forename(X0,X7)
    | ~ of(X0,X7,X3)
    | ~ sP2(X0)
    | ~ sP4(sK34(X0)) ) ).

cnf(u614,negated_conjecture,
    ( ~ of(X0,X4,sK17(X0))
    | ~ think_believe_consider(X0,X2)
    | ~ present(X0,X2)
    | ~ event(X0,X2)
    | ~ theme(X0,X2,X1)
    | ~ agent(X0,X2,X3)
    | ~ proposition(X0,X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ accessible_world(X0,X1)
    | ~ present(X1,X5)
    | ~ agent(X1,X5,X3)
    | ~ smoke(X1,X5)
    | ~ event(X1,X5)
    | ~ accessible_world(X0,X6)
    | ~ think_believe_consider(X0,X7)
    | ~ present(X0,X7)
    | ~ event(X0,X7)
    | ~ theme(X0,X7,X6)
    | ~ agent(X0,X7,X8)
    | ~ proposition(X0,X6)
    | ~ forename(X0,X9)
    | ~ vincent_forename(X0,X9)
    | ~ man(X0,X8)
    | ~ of(X0,X9,X8)
    | ~ forename(X0,X10)
    | ~ vincent_forename(X0,X10)
    | ~ man(X0,X3)
    | ~ of(X0,X10,X3)
    | ~ forename(X0,X11)
    | ~ jules_forename(X0,X11)
    | ~ of(X0,X11,X3)
    | ~ sP5(X0)
    | ~ sP4(X6) ) ).

cnf(u42,axiom,
    ( think_believe_consider(X0,sK19(X0))
    | ~ sP5(X0) ) ).

cnf(u667,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X1)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP3(sK20(X0),X1) ) ).

cnf(u102,axiom,
    ( theme(X0,sK28(X0),sK29(X0))
    | ~ sP2(X0) ) ).

cnf(u1349,negated_conjecture,
    ( ~ agent(X0,sK14(X0),sK24(sK15(X0)))
    | ~ actual_world(X0)
    | ~ smoke(sK15(X0),sK33(sK15(X0)))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK24(sK15(X0)))
    | ~ of(X0,X1,sK24(sK15(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK24(sK15(X0)))
    | ~ sP5(X0)
    | ~ sP2(sK15(X0)) ) ).

cnf(u569,negated_conjecture,
    ( man(sK29(X0),sK37(sK29(X0)))
    | ~ actual_world(X0)
    | ~ vincent_forename(X0,sK23(X0))
    | ~ sP2(X0) ) ).

cnf(u1173,negated_conjecture,
    ( ~ agent(X0,sK28(X0),sK26(sK29(X0)))
    | ~ smoke(sK29(X0),sK28(sK29(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK26(sK29(X0)))
    | ~ of(X0,X1,sK26(sK29(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK26(sK29(X0)))
    | ~ sP2(X0)
    | ~ sP2(sK29(X0)) ) ).

cnf(u322,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK9(sK34(X0)))
    | ~ smoke(sK34(X0),sK19(sK34(X0)))
    | man(sK34(X0),sK37(sK34(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK9(sK34(X0)))
    | ~ of(X0,X1,sK9(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(sK34(X0)))
    | ~ sP2(X0)
    | ~ sP5(sK34(X0)) ) ).

cnf(u1261,negated_conjecture,
    ( ~ of(X0,X5,sK12(X0))
    | ~ theme(X0,X1,X2)
    | ~ agent(X0,X1,X3)
    | ~ proposition(X0,X2)
    | ~ actual_world(X0)
    | ~ accessible_world(X0,X2)
    | ~ present(X2,X4)
    | ~ agent(X2,X4,X3)
    | ~ smoke(X2,X4)
    | ~ event(X2,X4)
    | ~ think_believe_consider(X0,X1)
    | ~ present(X0,X1)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ event(X0,X1)
    | ~ forename(X0,X6)
    | ~ vincent_forename(X0,X6)
    | ~ man(X0,X3)
    | ~ of(X0,X6,X3)
    | ~ forename(X0,X7)
    | ~ jules_forename(X0,X7)
    | ~ of(X0,X7,X3)
    | ~ sP5(X0) ) ).

cnf(u57,axiom,
    ( think_believe_consider(X0,sK14(X0))
    | ~ sP5(X0) ) ).

cnf(u510,negated_conjecture,
    ( ~ event(X6,sK35(X6,sK37(X6)))
    | ~ accessible_world(X2,X0)
    | ~ think_believe_consider(X2,X3)
    | ~ present(X2,X3)
    | ~ event(X2,X3)
    | ~ theme(X2,X3,X0)
    | ~ agent(X2,X3,X4)
    | ~ proposition(X2,X0)
    | ~ actual_world(X2)
    | ~ forename(X2,X5)
    | ~ jules_forename(X2,X5)
    | ~ of(X2,X5,sK17(X2))
    | ~ present(X0,X1)
    | ~ agent(X0,X1,X4)
    | ~ smoke(X0,X1)
    | ~ event(X0,X1)
    | ~ accessible_world(X2,X6)
    | ~ think_believe_consider(X2,X7)
    | ~ present(X2,X7)
    | ~ event(X2,X7)
    | ~ theme(X2,X7,X6)
    | ~ agent(X2,X7,X8)
    | ~ proposition(X2,X6)
    | ~ forename(X2,X9)
    | ~ vincent_forename(X2,X9)
    | ~ man(X2,X8)
    | ~ of(X2,X9,X8)
    | ~ forename(X2,X10)
    | ~ vincent_forename(X2,X10)
    | ~ man(X2,X4)
    | ~ of(X2,X10,X4)
    | ~ forename(X2,X11)
    | ~ jules_forename(X2,X11)
    | ~ of(X2,X11,X4)
    | ~ sP5(X2)
    | ~ sP1(X6) ) ).

cnf(u325,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | man(sK34(X0),sK37(sK34(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ man(sK34(X0),X1)
    | ~ sP1(sK34(X0)) ) ).

cnf(u117,axiom,
    ( present(X0,sK35(X0,X1))
    | ~ man(X0,X1)
    | ~ sP1(X0) ) ).

cnf(u1314,negated_conjecture,
    ( ~ agent(X0,sK19(X0),sK9(sK20(X0)))
    | ~ actual_world(X0)
    | ~ smoke(sK20(X0),sK19(sK20(X0)))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK9(sK20(X0)))
    | ~ of(X0,X1,sK9(sK20(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(sK20(X0)))
    | ~ sP5(X0)
    | ~ sP5(sK20(X0)) ) ).

cnf(u964,negated_conjecture,
    ( ~ agent(X0,sK28(X0),X1)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP0(sK29(X0),X1) ) ).

cnf(u233,negated_conjecture,
    ( ~ of(X3,X5,sK31(X3))
    | ~ agent(X0,X1,X2)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ forename(X3,X5)
    | ~ jules_forename(X3,X5)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ accessible_world(X3,X6)
    | ~ think_believe_consider(X3,X7)
    | ~ present(X3,X7)
    | ~ event(X3,X7)
    | ~ theme(X3,X7,X6)
    | ~ agent(X3,X7,X8)
    | ~ proposition(X3,X6)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X8)
    | ~ of(X3,X9,X8)
    | ~ forename(X3,X10)
    | ~ vincent_forename(X3,X10)
    | ~ man(X3,X2)
    | ~ of(X3,X10,X2)
    | ~ forename(X3,X11)
    | ~ jules_forename(X3,X11)
    | ~ of(X3,X11,X2)
    | ~ sP2(X3)
    | ~ sP0(X6,sK37(X6)) ) ).

cnf(u120,axiom,
    ( smoke(X0,sK36(X0,X1))
    | ~ sP0(X0,X1) ) ).

cnf(u1080,negated_conjecture,
    ( ~ of(X0,X1,sK24(X0))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ actual_world(X0)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0) ) ).

cnf(u64,axiom,
    ( vincent_forename(X0,sK13(X0))
    | ~ sP5(X0) ) ).

cnf(u123,axiom,
    ( event(X0,sK36(X0,X1))
    | ~ sP0(X0,X1) ) ).

cnf(u1362,negated_conjecture,
    ( ~ sP3(sK20(X0),sK9(X0))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK9(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(X0))
    | ~ sP5(X0)
    | ~ actual_world(X0) ) ).

cnf(u576,negated_conjecture,
    ( ~ of(X0,X5,sK12(X0))
    | ~ think_believe_consider(X0,X2)
    | ~ present(X0,X2)
    | ~ event(X0,X2)
    | ~ theme(X0,X2,X1)
    | ~ agent(X0,X2,X3)
    | ~ proposition(X0,X1)
    | ~ actual_world(X0)
    | ~ present(X1,X4)
    | ~ smoke(X1,X4)
    | ~ agent(X1,X4,X3)
    | ~ event(X1,X4)
    | ~ forename(X0,X5)
    | ~ vincent_forename(X0,X5)
    | ~ accessible_world(X0,X1)
    | ~ forename(X0,X6)
    | ~ vincent_forename(X0,X6)
    | ~ man(X0,X3)
    | ~ of(X0,X6,X3)
    | ~ forename(X0,X7)
    | ~ jules_forename(X0,X7)
    | ~ of(X0,X7,X3)
    | ~ sP2(X0)
    | ~ sP5(X0) ) ).

cnf(u87,axiom,
    ( theme(X0,sK33(X0),sK34(X0))
    | ~ sP2(X0) ) ).

cnf(u530,negated_conjecture,
    ( ~ agent(X0,sK33(X0),sK26(sK34(X0)))
    | ~ smoke(sK34(X0),sK28(sK34(X0)))
    | man(sK29(X0),sK37(sK29(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK26(sK34(X0)))
    | ~ of(X0,X1,sK26(sK34(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK26(sK34(X0)))
    | ~ sP2(X0)
    | ~ sP2(sK34(X0)) ) ).

cnf(u1012,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X5)
    | ~ event(X0,X1)
    | ~ theme(X0,X1,X2)
    | ~ agent(X0,X1,X3)
    | ~ proposition(X0,X2)
    | ~ actual_world(X0)
    | ~ accessible_world(X0,X2)
    | ~ present(X2,X4)
    | ~ agent(X2,X4,X3)
    | ~ smoke(X2,X4)
    | ~ event(X2,X4)
    | ~ think_believe_consider(X0,X1)
    | ~ present(X0,X1)
    | ~ forename(X0,X6)
    | ~ vincent_forename(X0,X6)
    | ~ man(X0,X5)
    | ~ of(X0,X6,X5)
    | ~ forename(X0,X7)
    | ~ vincent_forename(X0,X7)
    | ~ man(X0,X3)
    | ~ of(X0,X7,X3)
    | ~ forename(X0,X8)
    | ~ jules_forename(X0,X8)
    | ~ of(X0,X8,X3)
    | ~ sP5(X0)
    | ~ sP1(sK20(X0)) ) ).

cnf(u111,axiom,
    ( man(X0,sK24(X0))
    | ~ sP2(X0) ) ).

cnf(u611,negated_conjecture,
    ( ~ of(X0,X4,sK17(X0))
    | ~ think_believe_consider(X0,X2)
    | ~ present(X0,X2)
    | ~ event(X0,X2)
    | ~ theme(X0,X2,X1)
    | ~ agent(X0,X2,X3)
    | ~ proposition(X0,X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X4)
    | ~ jules_forename(X0,X4)
    | ~ accessible_world(X0,X1)
    | ~ present(X1,X5)
    | ~ agent(X1,X5,X3)
    | ~ smoke(X1,X5)
    | ~ event(X1,X5)
    | ~ accessible_world(X0,X6)
    | ~ think_believe_consider(X0,X7)
    | ~ present(X0,X7)
    | ~ event(X0,X7)
    | ~ theme(X0,X7,X6)
    | ~ agent(X0,X7,X8)
    | ~ proposition(X0,X6)
    | ~ forename(X0,X9)
    | ~ vincent_forename(X0,X9)
    | ~ man(X0,X8)
    | ~ of(X0,X9,X8)
    | ~ forename(X0,X10)
    | ~ vincent_forename(X0,X10)
    | ~ man(X0,X3)
    | ~ of(X0,X10,X3)
    | ~ forename(X0,X11)
    | ~ jules_forename(X0,X11)
    | ~ of(X0,X11,X3)
    | ~ sP5(X0)
    | ~ sP1(X6) ) ).

cnf(u46,axiom,
    ( agent(X0,sK19(X0),sK9(X0))
    | ~ sP5(X0) ) ).

cnf(u762,negated_conjecture,
    ( ~ agent(X0,sK14(X0),X1)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ man(sK15(X0),X1)
    | ~ sP1(sK15(X0)) ) ).

cnf(u938,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP3(sK34(X0),X1) ) ).

cnf(u90,axiom,
    ( be(X0,sK32(X0),sK31(X0),sK31(X0))
    | ~ sP2(X0) ) ).

cnf(u545,negated_conjecture,
    ( ~ of(X0,X2,sK24(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK24(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | man(sK29(X0),sK37(sK29(X0)))
    | ~ sP2(X0) ) ).

cnf(u1318,negated_conjecture,
    ( ~ agent(X0,sK19(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ sP3(sK20(X0),X1) ) ).

cnf(u85,axiom,
    ( present(X0,sK33(X0))
    | ~ sP2(X0) ) ).

cnf(u326,negated_conjecture,
    ( ~ agent(X0,sK33(X0),X1)
    | man(sK34(X0),sK37(sK34(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ sP3(sK34(X0),X1) ) ).

cnf(u1058,negated_conjecture,
    ( man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ vincent_forename(X0,sK23(X0))
    | ~ sP5(X0)
    | ~ sP2(X0) ) ).

cnf(u61,axiom,
    ( agent(X0,sK14(X0),sK12(X0))
    | ~ sP5(X0) ) ).

cnf(u1013,negated_conjecture,
    ( ~ agent(X0,sK14(X0),X5)
    | ~ event(X0,X1)
    | ~ theme(X0,X1,X2)
    | ~ agent(X0,X1,X3)
    | ~ proposition(X0,X2)
    | ~ actual_world(X0)
    | ~ accessible_world(X0,X2)
    | ~ present(X2,X4)
    | ~ agent(X2,X4,X3)
    | ~ smoke(X2,X4)
    | ~ event(X2,X4)
    | ~ think_believe_consider(X0,X1)
    | ~ present(X0,X1)
    | ~ forename(X0,X6)
    | ~ vincent_forename(X0,X6)
    | ~ man(X0,X5)
    | ~ of(X0,X6,X5)
    | ~ forename(X0,X7)
    | ~ vincent_forename(X0,X7)
    | ~ man(X0,X3)
    | ~ of(X0,X7,X3)
    | ~ forename(X0,X8)
    | ~ jules_forename(X0,X8)
    | ~ of(X0,X8,X3)
    | ~ sP5(X0)
    | ~ sP1(sK15(X0)) ) ).

cnf(u1107,negated_conjecture,
    ( ~ man(sK20(X0),sK9(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK9(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(X0))
    | ~ sP5(X0)
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ sP4(sK20(X0)) ) ).

cnf(u105,axiom,
    ( forename(X0,sK27(X0))
    | ~ sP2(X0) ) ).

cnf(u721,negated_conjecture,
    ( ~ man(sK20(X0),sK9(X0))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK9(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(X0))
    | ~ sP5(X0)
    | man(sK20(X0),sK37(sK20(X0)))
    | ~ sP1(sK20(X0)) ) ).

cnf(u1180,negated_conjecture,
    ( ~ agent(X0,sK28(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP2(X0)
    | ~ sP3(sK29(X0),X1) ) ).

cnf(u1059,negated_conjecture,
    ( man(sK20(X0),sK37(sK20(X0)))
    | ~ actual_world(X0)
    | ~ sP5(X0)
    | ~ sP2(X0) ) ).

cnf(u959,negated_conjecture,
    ( ~ agent(X0,sK28(X0),sK26(sK29(X0)))
    | ~ smoke(sK29(X0),sK28(sK29(X0)))
    | man(sK15(X0),sK37(sK15(X0)))
    | ~ actual_world(X0)
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ man(X0,sK26(sK29(X0)))
    | ~ of(X0,X1,sK26(sK29(X0)))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK26(sK29(X0)))
    | ~ sP5(X0)
    | ~ sP2(X0)
    | ~ sP2(sK29(X0)) ) ).

cnf(u237,negated_conjecture,
    ( ~ of(X3,X5,sK31(X3))
    | ~ agent(X0,X1,X2)
    | ~ event(X0,X1)
    | ~ accessible_world(X3,X0)
    | ~ think_believe_consider(X3,X4)
    | ~ present(X3,X4)
    | ~ event(X3,X4)
    | ~ theme(X3,X4,X0)
    | ~ agent(X3,X4,X2)
    | ~ proposition(X3,X0)
    | ~ actual_world(X3)
    | ~ forename(X3,X5)
    | ~ jules_forename(X3,X5)
    | ~ present(X0,X1)
    | ~ smoke(X0,X1)
    | ~ accessible_world(X3,X6)
    | ~ think_believe_consider(X3,X7)
    | ~ present(X3,X7)
    | ~ event(X3,X7)
    | ~ theme(X3,X7,X6)
    | ~ agent(X3,X7,X8)
    | ~ proposition(X3,X6)
    | ~ forename(X3,X9)
    | ~ vincent_forename(X3,X9)
    | ~ man(X3,X8)
    | ~ of(X3,X9,X8)
    | ~ forename(X3,X10)
    | ~ vincent_forename(X3,X10)
    | ~ man(X3,X2)
    | ~ of(X3,X10,X2)
    | ~ forename(X3,X11)
    | ~ jules_forename(X3,X11)
    | ~ of(X3,X11,X2)
    | ~ sP2(X3)
    | ~ sP1(X6) ) ).

cnf(u1356,negated_conjecture,
    ( ~ agent(X0,sK14(X0),X1)
    | ~ actual_world(X0)
    | ~ forename(X0,X2)
    | ~ vincent_forename(X0,X2)
    | ~ man(X0,X1)
    | ~ of(X0,X2,X1)
    | ~ forename(X0,X3)
    | ~ jules_forename(X0,X3)
    | ~ of(X0,X3,X1)
    | ~ sP5(X0)
    | ~ man(sK15(X0),X1)
    | ~ sP1(sK15(X0)) ) ).

cnf(u1377,negated_conjecture,
    ( ~ man(sK20(X0),sK9(X0))
    | ~ forename(X0,X1)
    | ~ vincent_forename(X0,X1)
    | ~ of(X0,X1,sK9(X0))
    | ~ forename(X0,X2)
    | ~ jules_forename(X0,X2)
    | ~ of(X0,X2,sK9(X0))
    | ~ sP5(X0)
    | ~ actual_world(X0)
    | ~ sP4(sK20(X0)) ) ).

cnf(u1187,negated_conjecture,
    ( ~ of(X0,X1,sK24(X0))
    | ~ vincent_forename(X0,X1)
    | ~ forename(X0,X1)
    | ~ jules_forename(X0,sK25(X0))
    | ~ actual_world(X0)
    | ~ sP2(X0) ) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : NLP233+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.37  % Computer : n016.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 : Sun Sep 27 18:38:02 UTC 2026
% 0.10/0.37  % CPUTime  : 
% 0.10/0.37  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.41  Running first-order theorem proving
% 0.10/0.41  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.22/1.24  % (2919140)Detected formulas, will run a generic FOF schedule.
% 4.22/1.24  % (2919150)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4185480476:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.22/1.24  % (2919151)dis-21_1_sil=8000:lcm=predicate:random_seed=3369555736:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.22/1.24  % (2919149)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=300980769:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.22/1.24  % (2919145)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1295889979:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.22/1.24  % (2919147)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3820391680:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.22/1.24  % (2919148)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4015421965:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.22/1.24  % (2919146)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2870664478:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.22/1.24  % (2919148)Refutation not found, incomplete strategy
% 4.22/1.24  % (2919148)------------------------------
% 4.22/1.24  % (2919148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.24  % (2919148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.24  % (2919148)CaDiCaL version: 2.1.3
% 4.22/1.24  % (2919148)Termination reason: Refutation not found, incomplete strategy
% 4.22/1.24  % (2919148)Time elapsed: 0.017 s
% 4.22/1.24  % (2919148)Peak memory usage: 88 MB
% 4.22/1.24  % (2919148)Instructions burned: 33 (million)
% 4.22/1.24  % (2919150)Refutation not found, incomplete strategy
% 4.22/1.24  % (2919150)------------------------------
% 4.22/1.24  % (2919150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.24  % (2919150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.24  % (2919150)CaDiCaL version: 2.1.3
% 4.22/1.24  % (2919150)Termination reason: Refutation not found, incomplete strategy
% 4.22/1.24  % (2919150)Time elapsed: 0.022 s
% 4.22/1.24  % (2919150)Peak memory usage: 89 MB
% 4.22/1.24  % (2919150)Instructions burned: 42 (million)
% 4.22/1.24  % (2919149)Instruction limit reached! 
% 4.22/1.24  % (2919149)------------------------------
% 4.22/1.24  % (2919149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.24  % (2919149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.24  % (2919149)CaDiCaL version: 2.1.3
% 4.22/1.24  % (2919149)Termination reason: Instruction limit
% 4.22/1.24  % (2919149)Termination phase: Saturation
% 4.22/1.24  % (2919149)Time elapsed: 0.052 s
% 4.22/1.24  % (2919149)Peak memory usage: 88 MB
% 4.22/1.24  % (2919149)Instructions burned: 119 (million)
% 4.22/1.24  % (2919151)Instruction limit reached! 
% 4.22/1.24  % (2919151)------------------------------
% 4.22/1.24  % (2919151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.24  % (2919151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.24  % (2919151)CaDiCaL version: 2.1.3
% 4.22/1.24  % (2919151)Termination reason: Instruction limit
% 4.22/1.24  % (2919151)Termination phase: Saturation
% 4.22/1.24  % (2919151)Time elapsed: 0.067 s
% 4.22/1.24  % (2919151)Peak memory usage: 89 MB
% 4.22/1.24  % (2919151)Instructions burned: 130 (million)
% 4.22/1.24  % (2919159)lrs+10_1_sil=8000:sp=occurrence:random_seed=1775610926:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 4.22/1.24  % (2919160)lrs+10_1_sil=32000:urr=on:br=off:random_seed=566591562:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 4.22/1.24  % (2919160)Refutation not found, incomplete strategy
% 4.22/1.24  % (2919160)------------------------------
% 4.22/1.24  % (2919160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.24  % (2919160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.24  % (2919160)CaDiCaL version: 2.1.3
% 4.22/1.24  % (2919160)Termination reason: Refutation not found, incomplete strategy
% 4.22/1.24  % (2919160)Time elapsed: 0.006 s
% 4.22/1.24  % (2919160)Peak memory usage: 88 MB
% 4.22/1.24  % (2919160)Instructions burned: 8 (million)
% 4.22/1.24  % (2919150)------------------------------
% 4.22/1.24  % (2919150)------------------------------
% 4.22/1.24  % (2919159)First to succeed.
% 4.22/1.24  % (2919159)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2919140"
% 4.22/1.24  % (2919148)------------------------------
% 4.22/1.24  % (2919148)------------------------------
% 4.22/1.24  % (2919163)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3434817293:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 4.22/1.24  % (2919163)Refutation not found, incomplete strategy
% 4.22/1.24  % (2919163)------------------------------
% 4.22/1.24  % (2919163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.24  % (2919163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.24  % (2919163)CaDiCaL version: 2.1.3
% 4.22/1.24  % (2919163)Termination reason: Refutation not found, incomplete strategy
% 4.22/1.24  % (2919163)Time elapsed: 0.014 s
% 4.22/1.24  % (2919163)Peak memory usage: 89 MB
% 4.22/1.24  % (2919163)Instructions burned: 43 (million)
% 4.22/1.24  % (2919164)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3215563834:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 4.22/1.24  % (2919164)Refutation not found, incomplete strategy
% 4.22/1.24  % (2919164)------------------------------
% 4.22/1.24  % (2919164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.24  % (2919164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.24  % (2919164)CaDiCaL version: 2.1.3
% 4.22/1.24  % (2919164)Termination reason: Refutation not found, incomplete strategy
% 4.22/1.24  % (2919164)Time elapsed: 0.025 s
% 4.22/1.24  % (2919164)Peak memory usage: 89 MB
% 4.22/1.24  % (2919164)Instructions burned: 49 (million)
% 4.22/1.24  % (2919160)------------------------------
% 4.22/1.24  % (2919160)------------------------------
% 4.22/1.24  % (2919163)------------------------------
% 4.22/1.24  % (2919163)------------------------------
% 4.22/1.24  % SZS status CounterSatisfiable for theBenchmark
% 4.22/1.24  % SZS output start Saturation.
% See solution above
% 4.86/1.45  % SZS output start Definitions and Model Updates.
% 4.86/1.45  % SZS output end Definitions and Model Updates.
% 4.86/1.45  % (2919159)------------------------------
% 4.86/1.45  % (2919159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.86/1.45  % (2919159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.86/1.45  % (2919159)CaDiCaL version: 2.1.3
% 4.86/1.45  % (2919159)Termination reason: Satisfiable
% 4.86/1.45  % (2919159)Time elapsed: 0.068 s
% 4.86/1.45  % (2919159)Peak memory usage: 90 MB
% 4.86/1.45  % (2919159)Instructions burned: 142 (million)
% 4.86/1.45  % (2919159)------------------------------
% 4.86/1.45  % (2919159)------------------------------
% 4.86/1.45  % (2919140)Success in time 0.631 s
% 4.86/1.45  % Vampire exiting
%------------------------------------------------------------------------------