Metis---2.4.CSA-Sat.s

%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : NLP238+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n013.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 600s
% DateTime : Mon Jul 18 03:16:30 EDT 2022

% Result   : CounterSatisfiable 1.02s 1.20s
% Output   : Saturation 1.08s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13  % Problem  : NLP238+1 : TPTP v8.1.0. Released v2.4.0.
% 0.12/0.14  % Command  : metis --show proof --show saturation %s
% 0.13/0.35  % Computer : n013.cluster.edu
% 0.13/0.35  % Model    : x86_64 x86_64
% 0.13/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35  % Memory   : 8042.1875MB
% 0.13/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35  % CPULimit : 300
% 0.13/0.35  % WCLimit  : 600
% 0.13/0.35  % DateTime : Fri Jul  1 11:22:59 EDT 2022
% 0.13/0.36  % CPUTime  : 
% 0.13/0.36  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 1.02/1.20  % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.02/1.20  
% 1.02/1.20  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.02/1.20  |- actual_world skolemFOFtoCNF_U
% 1.02/1.20  |- accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_X2
% 1.02/1.20  |- accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_X7
% 1.02/1.20  |- agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_Y
% 1.02/1.20  |- agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X4
% 1.02/1.20  |- be skolemFOFtoCNF_U skolemFOFtoCNF_X5 skolemFOFtoCNF_X4
% 1.02/1.20       skolemFOFtoCNF_X4
% 1.02/1.20  |- event skolemFOFtoCNF_U skolemFOFtoCNF_X1
% 1.02/1.20  |- event skolemFOFtoCNF_U skolemFOFtoCNF_X6
% 1.02/1.20  |- forename skolemFOFtoCNF_U skolemFOFtoCNF_W
% 1.02/1.20  |- forename skolemFOFtoCNF_U skolemFOFtoCNF_X
% 1.02/1.20  |- forename skolemFOFtoCNF_U skolemFOFtoCNF_X3
% 1.02/1.20  |- forename skolemFOFtoCNF_U skolemFOFtoCNF_Z
% 1.02/1.20  |- jules_forename skolemFOFtoCNF_U skolemFOFtoCNF_W
% 1.02/1.20  |- jules_forename skolemFOFtoCNF_U skolemFOFtoCNF_X3
% 1.02/1.20  |- man skolemFOFtoCNF_U skolemFOFtoCNF_V
% 1.02/1.20  |- man skolemFOFtoCNF_U skolemFOFtoCNF_X4
% 1.02/1.20  |- man skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 1.02/1.20  |- of skolemFOFtoCNF_U skolemFOFtoCNF_W skolemFOFtoCNF_V
% 1.02/1.20  |- of skolemFOFtoCNF_U skolemFOFtoCNF_X skolemFOFtoCNF_X4
% 1.02/1.20  |- of skolemFOFtoCNF_U skolemFOFtoCNF_X3 skolemFOFtoCNF_X4
% 1.02/1.20  |- of skolemFOFtoCNF_U skolemFOFtoCNF_Z skolemFOFtoCNF_Y
% 1.02/1.20  |- present skolemFOFtoCNF_U skolemFOFtoCNF_X1
% 1.02/1.20  |- present skolemFOFtoCNF_U skolemFOFtoCNF_X6
% 1.02/1.20  |- proposition skolemFOFtoCNF_U skolemFOFtoCNF_X2
% 1.02/1.20  |- proposition skolemFOFtoCNF_U skolemFOFtoCNF_X7
% 1.02/1.20  |- state skolemFOFtoCNF_U skolemFOFtoCNF_X5
% 1.02/1.20  |- theme skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X2
% 1.02/1.20  |- theme skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X7
% 1.02/1.20  |- think_believe_consider skolemFOFtoCNF_U skolemFOFtoCNF_X1
% 1.02/1.20  |- think_believe_consider skolemFOFtoCNF_U skolemFOFtoCNF_X6
% 1.02/1.20  |- vincent_forename skolemFOFtoCNF_U skolemFOFtoCNF_X
% 1.02/1.20  |- vincent_forename skolemFOFtoCNF_U skolemFOFtoCNF_Z
% 1.02/1.20  |- agent skolemFOFtoCNF_X7 skolemFOFtoCNF_X10 skolemFOFtoCNF_V
% 1.02/1.20  |- event skolemFOFtoCNF_X7 skolemFOFtoCNF_X10
% 1.02/1.20  |- present skolemFOFtoCNF_X7 skolemFOFtoCNF_X10
% 1.02/1.20  |- smoke skolemFOFtoCNF_X7 skolemFOFtoCNF_X10
% 1.02/1.20  |- ~man skolemFOFtoCNF_X2 $X8 \/
% 1.02/1.20     agent skolemFOFtoCNF_X2 (skolemFOFtoCNF_X9 $X8) $X8
% 1.02/1.20  |- ~man skolemFOFtoCNF_X2 $X8 \/
% 1.02/1.20     event skolemFOFtoCNF_X2 (skolemFOFtoCNF_X9 $X8)
% 1.02/1.20  |- ~man skolemFOFtoCNF_X2 $X8 \/
% 1.02/1.20     present skolemFOFtoCNF_X2 (skolemFOFtoCNF_X9 $X8)
% 1.02/1.20  |- ~man skolemFOFtoCNF_X2 $X8 \/
% 1.02/1.20     smoke skolemFOFtoCNF_X2 (skolemFOFtoCNF_X9 $X8)
% 1.02/1.20  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 1.02/1.20     ~actual_world $X11 \/ ~agent $X11 $X17 $X15 \/ ~agent $X11 $X22 $X12 \/
% 1.02/1.20     ~agent $X23 $X26 $X20 \/ ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/
% 1.02/1.20     ~event $X11 $X22 \/ ~event $X23 $X26 \/ ~forename $X11 $X13 \/
% 1.02/1.20     ~forename $X11 $X16 \/ ~forename $X11 $X19 \/
% 1.02/1.20     ~jules_forename $X11 $X19 \/ ~man $X11 $X12 \/ ~man $X11 $X15 \/
% 1.02/1.20     ~man $X11 $X20 \/ ~of $X11 $X13 $X12 \/ ~of $X11 $X16 $X15 \/
% 1.02/1.20     ~of $X11 $X19 $X20 \/ ~present $X11 $X17 \/ ~present $X11 $X22 \/
% 1.02/1.20     ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 1.02/1.20     ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/ ~state $X11 $X21 \/
% 1.02/1.20     ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 1.02/1.20     ~think_believe_consider $X11 $X17 \/
% 1.02/1.20     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X13 \/
% 1.02/1.20     ~vincent_forename $X11 $X16 \/ man $X18 (skolemFOFtoCNF_X24 $X18)
% 1.02/1.20  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.02/1.20     ~actual_world $X23 \/ ~agent $X23 $X22 $X12 \/ ~agent $X23 $X26 $X20 \/
% 1.02/1.20     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X22 \/ ~event $X23 $X26 \/
% 1.02/1.20     ~forename $X23 $X13 \/ ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 1.02/1.20     ~jules_forename $X23 $X19 \/ ~man $X23 $X12 \/ ~man $X23 $X20 \/
% 1.02/1.20     ~of $X23 $X13 $X12 \/ ~of $X23 $X16 $X20 \/ ~of $X23 $X19 $X20 \/
% 1.02/1.20     ~present $X23 $X22 \/ ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 1.02/1.20     ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/ ~state $X23 $X21 \/
% 1.02/1.20     ~theme $X23 $X22 $X23 \/ ~theme $X23 $X26 $X18 \/
% 1.02/1.20     ~think_believe_consider $X23 $X22 \/
% 1.02/1.20     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X13 \/
% 1.02/1.20     ~vincent_forename $X23 $X16 \/ man $X18 (skolemFOFtoCNF_X24 $X18)
% 1.02/1.20  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.02/1.20     ~actual_world $X23 \/ ~agent $X23 $X17 $X15 \/ ~agent $X23 $X26 $X20 \/
% 1.02/1.20     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X17 \/ ~event $X23 $X26 \/
% 1.02/1.20     ~forename $X23 $X13 \/ ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 1.02/1.20     ~jules_forename $X23 $X19 \/ ~man $X23 $X15 \/ ~man $X23 $X20 \/
% 1.02/1.20     ~of $X23 $X13 $X20 \/ ~of $X23 $X16 $X15 \/ ~of $X23 $X19 $X20 \/
% 1.02/1.20     ~present $X23 $X17 \/ ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 1.02/1.20     ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/ ~state $X23 $X21 \/
% 1.02/1.20     ~theme $X23 $X17 $X18 \/ ~theme $X23 $X26 $X23 \/
% 1.02/1.20     ~think_believe_consider $X23 $X17 \/
% 1.02/1.20     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X13 \/
% 1.02/1.20     ~vincent_forename $X23 $X16 \/ man $X18 (skolemFOFtoCNF_X24 $X18)
% 1.02/1.20  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 1.02/1.20     ~actual_world $X11 \/ ~agent $X11 $X17 $X15 \/ ~agent $X11 $X22 $X15 \/
% 1.02/1.20     ~agent $X23 $X26 $X20 \/ ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/
% 1.02/1.20     ~event $X11 $X22 \/ ~event $X23 $X26 \/ ~forename $X11 $X16 \/
% 1.02/1.20     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/
% 1.02/1.20     ~man $X11 $X20 \/ ~of $X11 $X16 $X15 \/ ~of $X11 $X19 $X20 \/
% 1.02/1.20     ~present $X11 $X17 \/ ~present $X11 $X22 \/ ~present $X23 $X26 \/
% 1.02/1.20     ~proposition $X11 $X18 \/ ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/
% 1.02/1.20     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 1.02/1.20     ~think_believe_consider $X11 $X17 \/
% 1.02/1.20     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16 \/
% 1.02/1.20     man $X18 (skolemFOFtoCNF_X24 $X18)
% 1.02/1.20  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 1.02/1.20     ~actual_world $X11 \/ ~agent $X11 $X22 $X15 \/ ~agent $X23 $X26 $X20 \/
% 1.02/1.20     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X22 \/ ~event $X23 $X26 \/
% 1.02/1.20     ~forename $X11 $X16 \/ ~forename $X11 $X19 \/
% 1.02/1.20     ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/ ~man $X11 $X20 \/
% 1.02/1.20     ~of $X11 $X16 $X15 \/ ~of $X11 $X19 $X20 \/ ~present $X11 $X22 \/
% 1.02/1.20     ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 1.02/1.20     ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/ ~state $X11 $X21 \/
% 1.02/1.20     ~theme $X11 $X22 $X18 \/ ~theme $X11 $X22 $X23 \/
% 1.02/1.20     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16 \/
% 1.02/1.20     man $X18 (skolemFOFtoCNF_X24 $X18)
% 1.02/1.20  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.02/1.20     ~actual_world $X23 \/ ~agent $X23 $X22 $X20 \/ ~agent $X23 $X26 $X20 \/
% 1.02/1.20     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X22 \/ ~event $X23 $X26 \/
% 1.02/1.20     ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 1.02/1.20     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/ ~of $X23 $X16 $X20 \/
% 1.02/1.20     ~of $X23 $X19 $X20 \/ ~present $X23 $X22 \/ ~present $X23 $X26 \/
% 1.02/1.20     ~proposition $X23 $X18 \/ ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/
% 1.02/1.20     ~state $X23 $X21 \/ ~theme $X23 $X22 $X23 \/ ~theme $X23 $X26 $X18 \/
% 1.02/1.20     ~think_believe_consider $X23 $X22 \/
% 1.02/1.20     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16 \/
% 1.02/1.20     man $X18 (skolemFOFtoCNF_X24 $X18)
% 1.02/1.21  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.02/1.21     ~actual_world $X23 \/ ~agent $X23 $X17 $X20 \/ ~agent $X23 $X26 $X20 \/
% 1.02/1.21     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X17 \/ ~event $X23 $X26 \/
% 1.02/1.21     ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 1.02/1.21     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/ ~of $X23 $X16 $X20 \/
% 1.02/1.21     ~of $X23 $X19 $X20 \/ ~present $X23 $X17 \/ ~present $X23 $X26 \/
% 1.02/1.21     ~proposition $X23 $X18 \/ ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/
% 1.02/1.21     ~state $X23 $X21 \/ ~theme $X23 $X17 $X18 \/ ~theme $X23 $X26 $X23 \/
% 1.02/1.21     ~think_believe_consider $X23 $X17 \/
% 1.02/1.21     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16 \/
% 1.02/1.21     man $X18 (skolemFOFtoCNF_X24 $X18)
% 1.02/1.21  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.02/1.21     ~actual_world $X23 \/ ~agent $X23 $X26 $X20 \/
% 1.02/1.21     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X26 \/ ~forename $X23 $X16 \/
% 1.02/1.21     ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/
% 1.02/1.21     ~of $X23 $X16 $X20 \/ ~of $X23 $X19 $X20 \/ ~present $X23 $X26 \/
% 1.02/1.21     ~proposition $X23 $X18 \/ ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/
% 1.02/1.21     ~state $X23 $X21 \/ ~theme $X23 $X26 $X18 \/ ~theme $X23 $X26 $X23 \/
% 1.02/1.21     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16 \/
% 1.02/1.21     man $X18 (skolemFOFtoCNF_X24 $X18)
% 1.02/1.21  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 1.02/1.21     ~actual_world $X11 \/ ~agent $X11 $X17 $X15 \/ ~agent $X11 $X22 $X20 \/
% 1.02/1.21     ~agent $X23 $X26 $X20 \/ ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/
% 1.02/1.21     ~event $X11 $X22 \/ ~event $X23 $X26 \/ ~forename $X11 $X16 \/
% 1.02/1.21     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/
% 1.02/1.21     ~man $X11 $X20 \/ ~of $X11 $X16 $X15 \/ ~of $X11 $X19 $X20 \/
% 1.02/1.21     ~present $X11 $X17 \/ ~present $X11 $X22 \/ ~present $X23 $X26 \/
% 1.02/1.21     ~proposition $X11 $X18 \/ ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/
% 1.02/1.21     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 1.02/1.21     ~think_believe_consider $X11 $X17 \/
% 1.02/1.21     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16 \/
% 1.02/1.21     ~vincent_forename $X11 $X19 \/ man $X18 (skolemFOFtoCNF_X24 $X18)
% 1.02/1.21  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.02/1.21     ~actual_world $X23 \/ ~agent $X23 $X17 $X15 \/ ~agent $X23 $X26 $X20 \/
% 1.02/1.21     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X17 \/ ~event $X23 $X26 \/
% 1.02/1.21     ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 1.02/1.21     ~jules_forename $X23 $X19 \/ ~man $X23 $X15 \/ ~man $X23 $X20 \/
% 1.02/1.21     ~of $X23 $X16 $X15 \/ ~of $X23 $X19 $X20 \/ ~present $X23 $X17 \/
% 1.02/1.21     ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 1.02/1.21     ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/ ~state $X23 $X21 \/
% 1.02/1.21     ~theme $X23 $X17 $X18 \/ ~theme $X23 $X26 $X23 \/
% 1.02/1.21     ~think_believe_consider $X23 $X17 \/
% 1.02/1.21     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16 \/
% 1.02/1.21     ~vincent_forename $X23 $X19 \/ man $X18 (skolemFOFtoCNF_X24 $X18)
% 1.02/1.21  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 1.02/1.21     ~actual_world $X11 \/ ~agent $X11 $X17 $X20 \/ ~agent $X11 $X22 $X12 \/
% 1.02/1.21     ~agent $X23 $X26 $X20 \/ ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/
% 1.02/1.21     ~event $X11 $X22 \/ ~event $X23 $X26 \/ ~forename $X11 $X13 \/
% 1.02/1.21     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X12 \/
% 1.02/1.21     ~man $X11 $X20 \/ ~of $X11 $X13 $X12 \/ ~of $X11 $X19 $X20 \/
% 1.02/1.21     ~present $X11 $X17 \/ ~present $X11 $X22 \/ ~present $X23 $X26 \/
% 1.02/1.21     ~proposition $X11 $X18 \/ ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/
% 1.02/1.21     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 1.02/1.21     ~think_believe_consider $X11 $X17 \/
% 1.02/1.21     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X13 \/
% 1.02/1.21     ~vincent_forename $X11 $X19 \/ man $X18 (skolemFOFtoCNF_X24 $X18)
% 1.02/1.21  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.02/1.21     ~actual_world $X23 \/ ~agent $X23 $X22 $X12 \/ ~agent $X23 $X26 $X20 \/
% 1.02/1.21     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X22 \/ ~event $X23 $X26 \/
% 1.02/1.21     ~forename $X23 $X13 \/ ~forename $X23 $X19 \/
% 1.02/1.21     ~jules_forename $X23 $X19 \/ ~man $X23 $X12 \/ ~man $X23 $X20 \/
% 1.02/1.21     ~of $X23 $X13 $X12 \/ ~of $X23 $X19 $X20 \/ ~present $X23 $X22 \/
% 1.02/1.21     ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 1.02/1.21     ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/ ~state $X23 $X21 \/
% 1.02/1.21     ~theme $X23 $X22 $X23 \/ ~theme $X23 $X26 $X18 \/
% 1.02/1.21     ~think_believe_consider $X23 $X22 \/
% 1.02/1.21     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X13 \/
% 1.02/1.21     ~vincent_forename $X23 $X19 \/ man $X18 (skolemFOFtoCNF_X24 $X18)
% 1.02/1.21  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 1.02/1.21     ~actual_world $X11 \/ ~agent $X11 $X17 $X20 \/ ~agent $X11 $X22 $X20 \/
% 1.02/1.21     ~agent $X23 $X26 $X20 \/ ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/
% 1.02/1.21     ~event $X11 $X22 \/ ~event $X23 $X26 \/ ~forename $X11 $X19 \/
% 1.02/1.21     ~jules_forename $X11 $X19 \/ ~man $X11 $X20 \/ ~of $X11 $X19 $X20 \/
% 1.02/1.21     ~present $X11 $X17 \/ ~present $X11 $X22 \/ ~present $X23 $X26 \/
% 1.02/1.21     ~proposition $X11 $X18 \/ ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/
% 1.02/1.21     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 1.02/1.21     ~think_believe_consider $X11 $X17 \/
% 1.02/1.21     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X19 \/
% 1.02/1.21     man $X18 (skolemFOFtoCNF_X24 $X18)
% 1.02/1.21  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 1.02/1.21     ~actual_world $X11 \/ ~agent $X11 $X22 $X20 \/ ~agent $X23 $X26 $X20 \/
% 1.02/1.21     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X22 \/ ~event $X23 $X26 \/
% 1.02/1.21     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X20 \/
% 1.02/1.21     ~of $X11 $X19 $X20 \/ ~present $X11 $X22 \/ ~present $X23 $X26 \/
% 1.02/1.21     ~proposition $X11 $X18 \/ ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/
% 1.02/1.21     ~state $X11 $X21 \/ ~theme $X11 $X22 $X18 \/ ~theme $X11 $X22 $X23 \/
% 1.02/1.21     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X19 \/
% 1.02/1.21     man $X18 (skolemFOFtoCNF_X24 $X18)
% 1.02/1.21  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.02/1.21     ~actual_world $X23 \/ ~agent $X23 $X22 $X20 \/ ~agent $X23 $X26 $X20 \/
% 1.02/1.21     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X22 \/ ~event $X23 $X26 \/
% 1.02/1.21     ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/
% 1.02/1.21     ~of $X23 $X19 $X20 \/ ~present $X23 $X22 \/ ~present $X23 $X26 \/
% 1.02/1.21     ~proposition $X23 $X18 \/ ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/
% 1.02/1.21     ~state $X23 $X21 \/ ~theme $X23 $X22 $X23 \/ ~theme $X23 $X26 $X18 \/
% 1.02/1.21     ~think_believe_consider $X23 $X22 \/
% 1.02/1.21     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X19 \/
% 1.02/1.21     man $X18 (skolemFOFtoCNF_X24 $X18)
% 1.02/1.21  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.02/1.21     ~actual_world $X23 \/ ~agent $X23 $X17 $X20 \/ ~agent $X23 $X26 $X20 \/
% 1.02/1.21     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X17 \/ ~event $X23 $X26 \/
% 1.02/1.21     ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/
% 1.02/1.21     ~of $X23 $X19 $X20 \/ ~present $X23 $X17 \/ ~present $X23 $X26 \/
% 1.02/1.21     ~proposition $X23 $X18 \/ ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/
% 1.02/1.21     ~state $X23 $X21 \/ ~theme $X23 $X17 $X18 \/ ~theme $X23 $X26 $X23 \/
% 1.02/1.21     ~think_believe_consider $X23 $X17 \/
% 1.02/1.21     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X19 \/
% 1.02/1.21     man $X18 (skolemFOFtoCNF_X24 $X18)
% 1.02/1.21  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.02/1.21     ~actual_world $X23 \/ ~agent $X23 $X26 $X20 \/
% 1.02/1.21     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X26 \/ ~forename $X23 $X19 \/
% 1.02/1.21     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/ ~of $X23 $X19 $X20 \/
% 1.02/1.21     ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 1.02/1.21     ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/ ~state $X23 $X21 \/
% 1.02/1.21     ~theme $X23 $X26 $X18 \/ ~theme $X23 $X26 $X23 \/
% 1.02/1.21     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X19 \/
% 1.02/1.21     man $X18 (skolemFOFtoCNF_X24 $X18)
% 1.02/1.21  |- ~accessible_world $X11 $X23 \/ ~actual_world $X11 \/
% 1.02/1.21     ~agent $X11 $X22 $X15 \/ ~agent $X23 $X26 $X20 \/
% 1.02/1.21     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X22 \/ ~event $X23 $X26 \/
% 1.02/1.21     ~forename $X11 $X16 \/ ~forename $X11 $X19 \/
% 1.02/1.21     ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/ ~man $X11 $X20 \/
% 1.02/1.21     ~of $X11 $X16 $X15 \/ ~of $X11 $X19 $X20 \/ ~present $X11 $X22 \/
% 1.02/1.21     ~present $X23 $X26 \/ ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/
% 1.02/1.21     ~state $X11 $X21 \/ ~theme $X11 $X22 $X23 \/
% 1.02/1.21     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16 \/
% 1.02/1.21     man $X23 (skolemFOFtoCNF_X24 $X23)
% 1.02/1.21  |- ~accessible_world $X23 $X23 \/ ~actual_world $X23 \/
% 1.02/1.21     ~agent $X23 $X26 $X20 \/ ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X26 \/
% 1.02/1.21     ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 1.02/1.21     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/ ~of $X23 $X16 $X20 \/
% 1.02/1.21     ~of $X23 $X19 $X20 \/ ~present $X23 $X26 \/ ~proposition $X23 $X23 \/
% 1.02/1.21     ~smoke $X23 $X26 \/ ~state $X23 $X21 \/ ~theme $X23 $X26 $X23 \/
% 1.02/1.21     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16 \/
% 1.02/1.21     man $X23 (skolemFOFtoCNF_X24 $X23)
% 1.02/1.21  |- ~accessible_world $X11 $X23 \/ ~actual_world $X11 \/
% 1.02/1.21     ~agent $X11 $X22 $X20 \/ ~agent $X23 $X26 $X20 \/
% 1.02/1.21     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X22 \/ ~event $X23 $X26 \/
% 1.02/1.21     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X20 \/
% 1.02/1.21     ~of $X11 $X19 $X20 \/ ~present $X11 $X22 \/ ~present $X23 $X26 \/
% 1.02/1.21     ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/ ~state $X11 $X21 \/
% 1.02/1.21     ~theme $X11 $X22 $X23 \/ ~think_believe_consider $X11 $X22 \/
% 1.02/1.21     ~vincent_forename $X11 $X19 \/ man $X23 (skolemFOFtoCNF_X24 $X23)
% 1.02/1.21  |- ~accessible_world $X23 $X23 \/ ~actual_world $X23 \/
% 1.02/1.21     ~agent $X23 $X26 $X20 \/ ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X26 \/
% 1.02/1.21     ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/
% 1.02/1.21     ~of $X23 $X19 $X20 \/ ~present $X23 $X26 \/ ~proposition $X23 $X23 \/
% 1.02/1.21     ~smoke $X23 $X26 \/ ~state $X23 $X21 \/ ~theme $X23 $X26 $X23 \/
% 1.02/1.21     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X19 \/
% 1.02/1.21     man $X23 (skolemFOFtoCNF_X24 $X23)
% 1.02/1.21  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 1.02/1.21     ~actual_world $X11 \/ ~agent $X11 $X17 $X15 \/ ~agent $X11 $X22 $X12 \/
% 1.02/1.21     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 1.02/1.21     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/ ~event $X11 $X22 \/
% 1.02/1.21     ~event $X18 $X25 \/ ~event $X23 $X26 \/ ~forename $X11 $X13 \/
% 1.02/1.21     ~forename $X11 $X16 \/ ~forename $X11 $X19 \/
% 1.02/1.21     ~jules_forename $X11 $X19 \/ ~man $X11 $X12 \/ ~man $X11 $X15 \/
% 1.02/1.21     ~man $X11 $X20 \/ ~of $X11 $X13 $X12 \/ ~of $X11 $X16 $X15 \/
% 1.02/1.21     ~of $X11 $X19 $X20 \/ ~present $X11 $X17 \/ ~present $X11 $X22 \/
% 1.02/1.21     ~present $X18 $X25 \/ ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 1.02/1.21     ~proposition $X11 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.02/1.21     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 1.02/1.21     ~think_believe_consider $X11 $X17 \/
% 1.02/1.21     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X13 \/
% 1.02/1.21     ~vincent_forename $X11 $X16
% 1.02/1.21  |- ~accessible_world $X18 $X18 \/ ~accessible_world $X18 $X23 \/
% 1.02/1.21     ~actual_world $X18 \/ ~agent $X18 $X22 $X12 \/
% 1.02/1.21     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 1.02/1.21     ~be $X18 $X21 $X20 $X20 \/ ~event $X18 $X22 \/ ~event $X18 $X25 \/
% 1.02/1.21     ~event $X23 $X26 \/ ~forename $X18 $X13 \/ ~forename $X18 $X16 \/
% 1.02/1.21     ~forename $X18 $X19 \/ ~jules_forename $X18 $X19 \/ ~man $X18 $X12 \/
% 1.02/1.21     ~man $X18 $X20 \/ ~man $X18 (skolemFOFtoCNF_X24 $X18) \/
% 1.02/1.21     ~of $X18 $X13 $X12 \/ ~of $X18 $X16 (skolemFOFtoCNF_X24 $X18) \/
% 1.02/1.21     ~of $X18 $X19 $X20 \/ ~present $X18 $X22 \/ ~present $X18 $X25 \/
% 1.02/1.21     ~present $X23 $X26 \/ ~proposition $X18 $X18 \/
% 1.02/1.21     ~proposition $X18 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.02/1.21     ~state $X18 $X21 \/ ~theme $X18 $X22 $X23 \/ ~theme $X18 $X25 $X18 \/
% 1.02/1.21     ~think_believe_consider $X18 $X22 \/
% 1.02/1.21     ~think_believe_consider $X18 $X25 \/ ~vincent_forename $X18 $X13 \/
% 1.02/1.21     ~vincent_forename $X18 $X16
% 1.02/1.21  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.02/1.21     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 1.02/1.21     ~agent $X23 $X22 $X12 \/ ~agent $X23 $X26 $X20 \/
% 1.02/1.21     ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/ ~event $X23 $X22 \/
% 1.02/1.21     ~event $X23 $X26 \/ ~forename $X23 $X13 \/ ~forename $X23 $X16 \/
% 1.02/1.21     ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/ ~man $X23 $X12 \/
% 1.02/1.21     ~man $X23 $X20 \/ ~of $X23 $X13 $X12 \/ ~of $X23 $X16 $X20 \/
% 1.02/1.21     ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/ ~present $X23 $X22 \/
% 1.02/1.21     ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 1.02/1.21     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.02/1.21     ~state $X23 $X21 \/ ~theme $X23 $X22 $X23 \/ ~theme $X23 $X26 $X18 \/
% 1.02/1.21     ~think_believe_consider $X23 $X22 \/
% 1.02/1.21     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X13 \/
% 1.02/1.21     ~vincent_forename $X23 $X16
% 1.05/1.21  |- ~accessible_world $X18 $X18 \/ ~accessible_world $X18 $X23 \/
% 1.05/1.21     ~actual_world $X18 \/ ~agent $X18 $X17 $X15 \/
% 1.05/1.21     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X18 $X21 $X20 $X20 \/ ~event $X18 $X17 \/ ~event $X18 $X25 \/
% 1.05/1.21     ~event $X23 $X26 \/ ~forename $X18 $X13 \/ ~forename $X18 $X16 \/
% 1.05/1.21     ~forename $X18 $X19 \/ ~jules_forename $X18 $X19 \/ ~man $X18 $X15 \/
% 1.05/1.21     ~man $X18 $X20 \/ ~man $X18 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.21     ~of $X18 $X13 (skolemFOFtoCNF_X24 $X18) \/ ~of $X18 $X16 $X15 \/
% 1.05/1.21     ~of $X18 $X19 $X20 \/ ~present $X18 $X17 \/ ~present $X18 $X25 \/
% 1.05/1.21     ~present $X23 $X26 \/ ~proposition $X18 $X18 \/
% 1.05/1.21     ~proposition $X18 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.21     ~state $X18 $X21 \/ ~theme $X18 $X17 $X18 \/ ~theme $X18 $X25 $X23 \/
% 1.05/1.21     ~think_believe_consider $X18 $X17 \/
% 1.05/1.21     ~think_believe_consider $X18 $X25 \/ ~vincent_forename $X18 $X13 \/
% 1.05/1.21     ~vincent_forename $X18 $X16
% 1.05/1.21  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.05/1.21     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.21     ~agent $X23 $X17 $X15 \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/ ~event $X23 $X17 \/
% 1.05/1.21     ~event $X23 $X26 \/ ~forename $X23 $X13 \/ ~forename $X23 $X16 \/
% 1.05/1.21     ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/ ~man $X23 $X15 \/
% 1.05/1.21     ~man $X23 $X20 \/ ~of $X23 $X13 $X20 \/ ~of $X23 $X16 $X15 \/
% 1.05/1.21     ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/ ~present $X23 $X17 \/
% 1.05/1.21     ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 1.05/1.21     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.21     ~state $X23 $X21 \/ ~theme $X23 $X17 $X18 \/ ~theme $X23 $X26 $X23 \/
% 1.05/1.21     ~think_believe_consider $X23 $X17 \/
% 1.05/1.21     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X13 \/
% 1.05/1.21     ~vincent_forename $X23 $X16
% 1.05/1.21  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 1.05/1.21     ~actual_world $X11 \/ ~agent $X11 $X17 $X15 \/ ~agent $X11 $X22 $X15 \/
% 1.05/1.21     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/ ~event $X11 $X22 \/
% 1.05/1.21     ~event $X18 $X25 \/ ~event $X23 $X26 \/ ~forename $X11 $X16 \/
% 1.05/1.21     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/
% 1.05/1.21     ~man $X11 $X20 \/ ~of $X11 $X16 $X15 \/ ~of $X11 $X19 $X20 \/
% 1.05/1.21     ~present $X11 $X17 \/ ~present $X11 $X22 \/ ~present $X18 $X25 \/
% 1.05/1.21     ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 1.05/1.21     ~proposition $X11 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.21     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 1.05/1.21     ~think_believe_consider $X11 $X17 \/
% 1.05/1.21     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16
% 1.05/1.21  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 1.05/1.21     ~actual_world $X11 \/ ~agent $X11 $X22 $X15 \/
% 1.05/1.21     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X22 \/ ~event $X18 $X25 \/
% 1.05/1.21     ~event $X23 $X26 \/ ~forename $X11 $X16 \/ ~forename $X11 $X19 \/
% 1.05/1.21     ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/ ~man $X11 $X20 \/
% 1.05/1.21     ~of $X11 $X16 $X15 \/ ~of $X11 $X19 $X20 \/ ~present $X11 $X22 \/
% 1.05/1.21     ~present $X18 $X25 \/ ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 1.05/1.21     ~proposition $X11 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.21     ~state $X11 $X21 \/ ~theme $X11 $X22 $X18 \/ ~theme $X11 $X22 $X23 \/
% 1.05/1.21     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16
% 1.05/1.21  |- ~accessible_world $X18 $X18 \/ ~accessible_world $X18 $X23 \/
% 1.05/1.21     ~actual_world $X18 \/ ~agent $X18 $X22 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.21     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X18 $X21 $X20 $X20 \/ ~event $X18 $X22 \/ ~event $X18 $X25 \/
% 1.05/1.21     ~event $X23 $X26 \/ ~forename $X18 $X16 \/ ~forename $X18 $X19 \/
% 1.05/1.21     ~jules_forename $X18 $X19 \/ ~man $X18 $X20 \/
% 1.05/1.21     ~man $X18 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.21     ~of $X18 $X16 (skolemFOFtoCNF_X24 $X18) \/ ~of $X18 $X19 $X20 \/
% 1.05/1.21     ~present $X18 $X22 \/ ~present $X18 $X25 \/ ~present $X23 $X26 \/
% 1.05/1.21     ~proposition $X18 $X18 \/ ~proposition $X18 $X23 \/ ~smoke $X18 $X25 \/
% 1.05/1.21     ~smoke $X23 $X26 \/ ~state $X18 $X21 \/ ~theme $X18 $X22 $X23 \/
% 1.05/1.21     ~theme $X18 $X25 $X18 \/ ~think_believe_consider $X18 $X22 \/
% 1.05/1.21     ~think_believe_consider $X18 $X25 \/ ~vincent_forename $X18 $X16
% 1.05/1.21  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.05/1.21     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.21     ~agent $X23 $X22 $X20 \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/ ~event $X23 $X22 \/
% 1.05/1.21     ~event $X23 $X26 \/ ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 1.05/1.21     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/ ~of $X23 $X16 $X20 \/
% 1.05/1.21     ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/ ~present $X23 $X22 \/
% 1.05/1.21     ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 1.05/1.21     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.21     ~state $X23 $X21 \/ ~theme $X23 $X22 $X23 \/ ~theme $X23 $X26 $X18 \/
% 1.05/1.21     ~think_believe_consider $X23 $X22 \/
% 1.05/1.21     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16
% 1.05/1.21  |- ~accessible_world $X18 $X18 \/ ~accessible_world $X18 $X23 \/
% 1.05/1.21     ~actual_world $X18 \/ ~agent $X18 $X17 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.21     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X18 $X21 $X20 $X20 \/ ~event $X18 $X17 \/ ~event $X18 $X25 \/
% 1.05/1.21     ~event $X23 $X26 \/ ~forename $X18 $X16 \/ ~forename $X18 $X19 \/
% 1.05/1.21     ~jules_forename $X18 $X19 \/ ~man $X18 $X20 \/
% 1.05/1.21     ~man $X18 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.21     ~of $X18 $X16 (skolemFOFtoCNF_X24 $X18) \/ ~of $X18 $X19 $X20 \/
% 1.05/1.21     ~present $X18 $X17 \/ ~present $X18 $X25 \/ ~present $X23 $X26 \/
% 1.05/1.21     ~proposition $X18 $X18 \/ ~proposition $X18 $X23 \/ ~smoke $X18 $X25 \/
% 1.05/1.21     ~smoke $X23 $X26 \/ ~state $X18 $X21 \/ ~theme $X18 $X17 $X18 \/
% 1.05/1.21     ~theme $X18 $X25 $X23 \/ ~think_believe_consider $X18 $X17 \/
% 1.05/1.21     ~think_believe_consider $X18 $X25 \/ ~vincent_forename $X18 $X16
% 1.05/1.21  |- ~accessible_world $X18 $X18 \/ ~accessible_world $X18 $X23 \/
% 1.05/1.21     ~actual_world $X18 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.21     ~agent $X23 $X26 $X20 \/ ~be $X18 $X21 $X20 $X20 \/ ~event $X18 $X25 \/
% 1.05/1.21     ~event $X23 $X26 \/ ~forename $X18 $X16 \/ ~forename $X18 $X19 \/
% 1.05/1.21     ~jules_forename $X18 $X19 \/ ~man $X18 $X20 \/
% 1.05/1.21     ~man $X18 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.21     ~of $X18 $X16 (skolemFOFtoCNF_X24 $X18) \/ ~of $X18 $X19 $X20 \/
% 1.05/1.21     ~present $X18 $X25 \/ ~present $X23 $X26 \/ ~proposition $X18 $X18 \/
% 1.05/1.21     ~proposition $X18 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.21     ~state $X18 $X21 \/ ~theme $X18 $X25 $X18 \/ ~theme $X18 $X25 $X23 \/
% 1.05/1.21     ~think_believe_consider $X18 $X25 \/ ~vincent_forename $X18 $X16
% 1.05/1.21  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.05/1.21     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.21     ~agent $X23 $X17 $X20 \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/ ~event $X23 $X17 \/
% 1.05/1.21     ~event $X23 $X26 \/ ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 1.05/1.21     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/ ~of $X23 $X16 $X20 \/
% 1.05/1.21     ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/ ~present $X23 $X17 \/
% 1.05/1.21     ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 1.05/1.21     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.21     ~state $X23 $X21 \/ ~theme $X23 $X17 $X18 \/ ~theme $X23 $X26 $X23 \/
% 1.05/1.21     ~think_believe_consider $X23 $X17 \/
% 1.05/1.21     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16
% 1.05/1.21  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.05/1.21     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.21     ~agent $X23 $X26 $X20 \/ ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/
% 1.05/1.21     ~event $X23 $X26 \/ ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 1.05/1.21     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/ ~of $X23 $X16 $X20 \/
% 1.05/1.21     ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/ ~present $X23 $X26 \/
% 1.05/1.21     ~proposition $X23 $X18 \/ ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/
% 1.05/1.21     ~smoke $X23 $X26 \/ ~state $X23 $X21 \/ ~theme $X23 $X26 $X18 \/
% 1.05/1.21     ~theme $X23 $X26 $X23 \/ ~think_believe_consider $X23 $X26 \/
% 1.05/1.21     ~vincent_forename $X23 $X16
% 1.05/1.21  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 1.05/1.21     ~actual_world $X11 \/ ~agent $X11 $X17 $X15 \/ ~agent $X11 $X22 $X20 \/
% 1.05/1.21     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/ ~event $X11 $X22 \/
% 1.05/1.21     ~event $X18 $X25 \/ ~event $X23 $X26 \/ ~forename $X11 $X16 \/
% 1.05/1.21     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/
% 1.05/1.21     ~man $X11 $X20 \/ ~of $X11 $X16 $X15 \/ ~of $X11 $X19 $X20 \/
% 1.05/1.21     ~present $X11 $X17 \/ ~present $X11 $X22 \/ ~present $X18 $X25 \/
% 1.05/1.21     ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 1.05/1.21     ~proposition $X11 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.21     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 1.05/1.21     ~think_believe_consider $X11 $X17 \/
% 1.05/1.21     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16 \/
% 1.05/1.21     ~vincent_forename $X11 $X19
% 1.05/1.21  |- ~accessible_world $X18 $X18 \/ ~accessible_world $X18 $X23 \/
% 1.05/1.21     ~actual_world $X18 \/ ~agent $X18 $X22 $X20 \/
% 1.05/1.21     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X18 $X21 $X20 $X20 \/ ~event $X18 $X22 \/ ~event $X18 $X25 \/
% 1.05/1.21     ~event $X23 $X26 \/ ~forename $X18 $X16 \/ ~forename $X18 $X19 \/
% 1.05/1.21     ~jules_forename $X18 $X19 \/ ~man $X18 $X20 \/
% 1.05/1.21     ~man $X18 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.21     ~of $X18 $X16 (skolemFOFtoCNF_X24 $X18) \/ ~of $X18 $X19 $X20 \/
% 1.05/1.21     ~present $X18 $X22 \/ ~present $X18 $X25 \/ ~present $X23 $X26 \/
% 1.05/1.21     ~proposition $X18 $X18 \/ ~proposition $X18 $X23 \/ ~smoke $X18 $X25 \/
% 1.05/1.21     ~smoke $X23 $X26 \/ ~state $X18 $X21 \/ ~theme $X18 $X22 $X23 \/
% 1.05/1.21     ~theme $X18 $X25 $X18 \/ ~think_believe_consider $X18 $X22 \/
% 1.05/1.21     ~think_believe_consider $X18 $X25 \/ ~vincent_forename $X18 $X16 \/
% 1.05/1.21     ~vincent_forename $X18 $X19
% 1.05/1.21  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.05/1.21     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.21     ~agent $X23 $X17 $X15 \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/ ~event $X23 $X17 \/
% 1.05/1.21     ~event $X23 $X26 \/ ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 1.05/1.21     ~jules_forename $X23 $X19 \/ ~man $X23 $X15 \/ ~man $X23 $X20 \/
% 1.05/1.21     ~of $X23 $X16 $X15 \/ ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/
% 1.05/1.21     ~present $X23 $X17 \/ ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 1.05/1.21     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.21     ~state $X23 $X21 \/ ~theme $X23 $X17 $X18 \/ ~theme $X23 $X26 $X23 \/
% 1.05/1.21     ~think_believe_consider $X23 $X17 \/
% 1.05/1.21     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16 \/
% 1.05/1.21     ~vincent_forename $X23 $X19
% 1.05/1.21  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 1.05/1.21     ~actual_world $X11 \/ ~agent $X11 $X17 $X20 \/ ~agent $X11 $X22 $X12 \/
% 1.05/1.21     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/ ~event $X11 $X22 \/
% 1.05/1.21     ~event $X18 $X25 \/ ~event $X23 $X26 \/ ~forename $X11 $X13 \/
% 1.05/1.21     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X12 \/
% 1.05/1.21     ~man $X11 $X20 \/ ~of $X11 $X13 $X12 \/ ~of $X11 $X19 $X20 \/
% 1.05/1.21     ~present $X11 $X17 \/ ~present $X11 $X22 \/ ~present $X18 $X25 \/
% 1.05/1.21     ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 1.05/1.21     ~proposition $X11 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.21     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 1.05/1.21     ~think_believe_consider $X11 $X17 \/
% 1.05/1.21     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X13 \/
% 1.05/1.21     ~vincent_forename $X11 $X19
% 1.05/1.21  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.05/1.21     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.21     ~agent $X23 $X22 $X12 \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/ ~event $X23 $X22 \/
% 1.05/1.21     ~event $X23 $X26 \/ ~forename $X23 $X13 \/ ~forename $X23 $X19 \/
% 1.05/1.21     ~jules_forename $X23 $X19 \/ ~man $X23 $X12 \/ ~man $X23 $X20 \/
% 1.05/1.21     ~of $X23 $X13 $X12 \/ ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/
% 1.05/1.21     ~present $X23 $X22 \/ ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 1.05/1.21     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.21     ~state $X23 $X21 \/ ~theme $X23 $X22 $X23 \/ ~theme $X23 $X26 $X18 \/
% 1.05/1.21     ~think_believe_consider $X23 $X22 \/
% 1.05/1.21     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X13 \/
% 1.05/1.21     ~vincent_forename $X23 $X19
% 1.05/1.21  |- ~accessible_world $X18 $X18 \/ ~accessible_world $X18 $X23 \/
% 1.05/1.21     ~actual_world $X18 \/ ~agent $X18 $X17 $X20 \/
% 1.05/1.21     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X18 $X21 $X20 $X20 \/ ~event $X18 $X17 \/ ~event $X18 $X25 \/
% 1.05/1.21     ~event $X23 $X26 \/ ~forename $X18 $X13 \/ ~forename $X18 $X19 \/
% 1.05/1.21     ~jules_forename $X18 $X19 \/ ~man $X18 $X20 \/
% 1.05/1.21     ~man $X18 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.21     ~of $X18 $X13 (skolemFOFtoCNF_X24 $X18) \/ ~of $X18 $X19 $X20 \/
% 1.05/1.21     ~present $X18 $X17 \/ ~present $X18 $X25 \/ ~present $X23 $X26 \/
% 1.05/1.21     ~proposition $X18 $X18 \/ ~proposition $X18 $X23 \/ ~smoke $X18 $X25 \/
% 1.05/1.21     ~smoke $X23 $X26 \/ ~state $X18 $X21 \/ ~theme $X18 $X17 $X18 \/
% 1.05/1.21     ~theme $X18 $X25 $X23 \/ ~think_believe_consider $X18 $X17 \/
% 1.05/1.21     ~think_believe_consider $X18 $X25 \/ ~vincent_forename $X18 $X13 \/
% 1.05/1.21     ~vincent_forename $X18 $X19
% 1.05/1.21  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 1.05/1.21     ~actual_world $X11 \/ ~agent $X11 $X17 $X20 \/ ~agent $X11 $X22 $X20 \/
% 1.05/1.21     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/ ~event $X11 $X22 \/
% 1.05/1.21     ~event $X18 $X25 \/ ~event $X23 $X26 \/ ~forename $X11 $X19 \/
% 1.05/1.21     ~jules_forename $X11 $X19 \/ ~man $X11 $X20 \/ ~of $X11 $X19 $X20 \/
% 1.05/1.21     ~present $X11 $X17 \/ ~present $X11 $X22 \/ ~present $X18 $X25 \/
% 1.05/1.21     ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 1.05/1.21     ~proposition $X11 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.21     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 1.05/1.21     ~think_believe_consider $X11 $X17 \/
% 1.05/1.21     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X19
% 1.05/1.21  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 1.05/1.21     ~actual_world $X11 \/ ~agent $X11 $X22 $X20 \/
% 1.05/1.21     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X22 \/ ~event $X18 $X25 \/
% 1.05/1.21     ~event $X23 $X26 \/ ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/
% 1.05/1.21     ~man $X11 $X20 \/ ~of $X11 $X19 $X20 \/ ~present $X11 $X22 \/
% 1.05/1.21     ~present $X18 $X25 \/ ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 1.05/1.21     ~proposition $X11 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.21     ~state $X11 $X21 \/ ~theme $X11 $X22 $X18 \/ ~theme $X11 $X22 $X23 \/
% 1.05/1.21     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X19
% 1.05/1.21  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.05/1.21     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.21     ~agent $X23 $X22 $X20 \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/ ~event $X23 $X22 \/
% 1.05/1.21     ~event $X23 $X26 \/ ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/
% 1.05/1.21     ~man $X23 $X20 \/ ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/
% 1.05/1.21     ~present $X23 $X22 \/ ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 1.05/1.21     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.21     ~state $X23 $X21 \/ ~theme $X23 $X22 $X23 \/ ~theme $X23 $X26 $X18 \/
% 1.05/1.21     ~think_believe_consider $X23 $X22 \/
% 1.05/1.21     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X19
% 1.05/1.21  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.05/1.21     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.21     ~agent $X23 $X17 $X20 \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.21     ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/ ~event $X23 $X17 \/
% 1.05/1.21     ~event $X23 $X26 \/ ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/
% 1.05/1.21     ~man $X23 $X20 \/ ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/
% 1.05/1.21     ~present $X23 $X17 \/ ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 1.05/1.21     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.21     ~state $X23 $X21 \/ ~theme $X23 $X17 $X18 \/ ~theme $X23 $X26 $X23 \/
% 1.05/1.21     ~think_believe_consider $X23 $X17 \/
% 1.05/1.21     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X19
% 1.05/1.22  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 1.05/1.22     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 1.05/1.22     ~agent $X23 $X26 $X20 \/ ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/
% 1.05/1.22     ~event $X23 $X26 \/ ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/
% 1.05/1.22     ~man $X23 $X20 \/ ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/
% 1.05/1.22     ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 1.05/1.22     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.22     ~state $X23 $X21 \/ ~theme $X23 $X26 $X18 \/ ~theme $X23 $X26 $X23 \/
% 1.05/1.22     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X19
% 1.05/1.22  |- ~accessible_world $X11 $X23 \/ ~actual_world $X11 \/
% 1.05/1.22     ~agent $X11 $X22 $X15 \/ ~agent $X23 $X25 (skolemFOFtoCNF_X24 $X23) \/
% 1.05/1.22     ~agent $X23 $X26 $X20 \/ ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X22 \/
% 1.05/1.22     ~event $X23 $X25 \/ ~event $X23 $X26 \/ ~forename $X11 $X16 \/
% 1.05/1.22     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/
% 1.05/1.22     ~man $X11 $X20 \/ ~of $X11 $X16 $X15 \/ ~of $X11 $X19 $X20 \/
% 1.05/1.22     ~present $X11 $X22 \/ ~present $X23 $X25 \/ ~present $X23 $X26 \/
% 1.05/1.22     ~proposition $X11 $X23 \/ ~smoke $X23 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.22     ~state $X11 $X21 \/ ~theme $X11 $X22 $X23 \/
% 1.05/1.22     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16
% 1.05/1.22  |- ~accessible_world $X23 $X23 \/ ~actual_world $X23 \/
% 1.05/1.22     ~agent $X23 $X25 (skolemFOFtoCNF_X24 $X23) \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.22     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X25 \/ ~event $X23 $X26 \/
% 1.05/1.22     ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 1.05/1.22     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/
% 1.05/1.22     ~man $X23 (skolemFOFtoCNF_X24 $X23) \/
% 1.05/1.22     ~of $X23 $X16 (skolemFOFtoCNF_X24 $X23) \/ ~of $X23 $X19 $X20 \/
% 1.05/1.22     ~present $X23 $X25 \/ ~present $X23 $X26 \/ ~proposition $X23 $X23 \/
% 1.05/1.22     ~smoke $X23 $X25 \/ ~smoke $X23 $X26 \/ ~state $X23 $X21 \/
% 1.05/1.22     ~theme $X23 $X25 $X23 \/ ~think_believe_consider $X23 $X25 \/
% 1.05/1.22     ~vincent_forename $X23 $X16
% 1.05/1.22  |- ~accessible_world $X23 $X23 \/ ~actual_world $X23 \/
% 1.05/1.22     ~agent $X23 $X25 (skolemFOFtoCNF_X24 $X23) \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.22     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X25 \/ ~event $X23 $X26 \/
% 1.05/1.22     ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 1.05/1.22     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/ ~of $X23 $X16 $X20 \/
% 1.05/1.22     ~of $X23 $X19 $X20 \/ ~present $X23 $X25 \/ ~present $X23 $X26 \/
% 1.05/1.22     ~proposition $X23 $X23 \/ ~smoke $X23 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.22     ~state $X23 $X21 \/ ~theme $X23 $X26 $X23 \/
% 1.05/1.22     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16
% 1.05/1.22  |- ~accessible_world $X11 $X23 \/ ~actual_world $X11 \/
% 1.05/1.22     ~agent $X11 $X22 $X15 \/ ~agent $X23 $X26 (skolemFOFtoCNF_X24 $X23) \/
% 1.05/1.22     ~be $X11 $X21 (skolemFOFtoCNF_X24 $X23) (skolemFOFtoCNF_X24 $X23) \/
% 1.05/1.22     ~event $X11 $X22 \/ ~event $X23 $X26 \/ ~forename $X11 $X16 \/
% 1.05/1.22     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/
% 1.05/1.22     ~man $X11 (skolemFOFtoCNF_X24 $X23) \/ ~of $X11 $X16 $X15 \/
% 1.05/1.22     ~of $X11 $X19 (skolemFOFtoCNF_X24 $X23) \/ ~present $X11 $X22 \/
% 1.05/1.22     ~present $X23 $X26 \/ ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/
% 1.05/1.22     ~state $X11 $X21 \/ ~theme $X11 $X22 $X23 \/
% 1.05/1.22     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16
% 1.05/1.22  |- ~accessible_world $X23 $X23 \/ ~actual_world $X23 \/
% 1.05/1.22     ~agent $X23 $X26 (skolemFOFtoCNF_X24 $X23) \/
% 1.05/1.22     ~be $X23 $X21 (skolemFOFtoCNF_X24 $X23) (skolemFOFtoCNF_X24 $X23) \/
% 1.05/1.22     ~event $X23 $X26 \/ ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 1.05/1.22     ~jules_forename $X23 $X19 \/ ~man $X23 (skolemFOFtoCNF_X24 $X23) \/
% 1.05/1.22     ~of $X23 $X16 (skolemFOFtoCNF_X24 $X23) \/
% 1.05/1.22     ~of $X23 $X19 (skolemFOFtoCNF_X24 $X23) \/ ~present $X23 $X26 \/
% 1.05/1.22     ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/ ~state $X23 $X21 \/
% 1.05/1.22     ~theme $X23 $X26 $X23 \/ ~think_believe_consider $X23 $X26 \/
% 1.05/1.22     ~vincent_forename $X23 $X16
% 1.05/1.22  |- ~accessible_world $X11 $X23 \/ ~actual_world $X11 \/
% 1.05/1.22     ~agent $X11 $X22 $X20 \/ ~agent $X23 $X25 (skolemFOFtoCNF_X24 $X23) \/
% 1.05/1.22     ~agent $X23 $X26 $X20 \/ ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X22 \/
% 1.05/1.22     ~event $X23 $X25 \/ ~event $X23 $X26 \/ ~forename $X11 $X19 \/
% 1.05/1.22     ~jules_forename $X11 $X19 \/ ~man $X11 $X20 \/ ~of $X11 $X19 $X20 \/
% 1.05/1.22     ~present $X11 $X22 \/ ~present $X23 $X25 \/ ~present $X23 $X26 \/
% 1.05/1.22     ~proposition $X11 $X23 \/ ~smoke $X23 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.22     ~state $X11 $X21 \/ ~theme $X11 $X22 $X23 \/
% 1.05/1.22     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X19
% 1.05/1.22  |- ~accessible_world $X23 $X23 \/ ~actual_world $X23 \/
% 1.05/1.22     ~agent $X23 $X25 (skolemFOFtoCNF_X24 $X23) \/ ~agent $X23 $X26 $X20 \/
% 1.05/1.22     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X25 \/ ~event $X23 $X26 \/
% 1.05/1.22     ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/
% 1.05/1.22     ~of $X23 $X19 $X20 \/ ~present $X23 $X25 \/ ~present $X23 $X26 \/
% 1.05/1.22     ~proposition $X23 $X23 \/ ~smoke $X23 $X25 \/ ~smoke $X23 $X26 \/
% 1.05/1.22     ~state $X23 $X21 \/ ~theme $X23 $X26 $X23 \/
% 1.05/1.22     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X19
% 1.05/1.22  |- ~accessible_world $X11 $X23 \/ ~actual_world $X11 \/
% 1.05/1.22     ~agent $X11 $X22 (skolemFOFtoCNF_X24 $X23) \/
% 1.05/1.22     ~agent $X23 $X26 (skolemFOFtoCNF_X24 $X23) \/
% 1.05/1.22     ~be $X11 $X21 (skolemFOFtoCNF_X24 $X23) (skolemFOFtoCNF_X24 $X23) \/
% 1.05/1.22     ~event $X11 $X22 \/ ~event $X23 $X26 \/ ~forename $X11 $X19 \/
% 1.05/1.22     ~jules_forename $X11 $X19 \/ ~man $X11 (skolemFOFtoCNF_X24 $X23) \/
% 1.05/1.22     ~of $X11 $X19 (skolemFOFtoCNF_X24 $X23) \/ ~present $X11 $X22 \/
% 1.05/1.22     ~present $X23 $X26 \/ ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/
% 1.05/1.22     ~state $X11 $X21 \/ ~theme $X11 $X22 $X23 \/
% 1.05/1.22     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X19
% 1.05/1.22  |- ~accessible_world $X23 $X23 \/ ~actual_world $X23 \/
% 1.05/1.22     ~agent $X23 $X26 (skolemFOFtoCNF_X24 $X23) \/
% 1.05/1.22     ~be $X23 $X21 (skolemFOFtoCNF_X24 $X23) (skolemFOFtoCNF_X24 $X23) \/
% 1.05/1.22     ~event $X23 $X26 \/ ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/
% 1.05/1.22     ~man $X23 (skolemFOFtoCNF_X24 $X23) \/
% 1.05/1.22     ~of $X23 $X19 (skolemFOFtoCNF_X24 $X23) \/ ~present $X23 $X26 \/
% 1.05/1.22     ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/ ~state $X23 $X21 \/
% 1.05/1.22     ~theme $X23 $X26 $X23 \/ ~think_believe_consider $X23 $X26 \/
% 1.05/1.22     ~vincent_forename $X23 $X19
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_12 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_12 \/ ~forename skolemFOFtoCNF_U $_8 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_8 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_8 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_12 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_12 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_12 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_12 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_8 \/
% 1.05/1.22     man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_25 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_25 \/ ~forename skolemFOFtoCNF_U $_20 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_21 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_21 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_20 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_21 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_25 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_25 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_25 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_25 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_20 \/
% 1.05/1.22     man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_35 \/
% 1.05/1.22     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_40 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_40 \/ ~forename skolemFOFtoCNF_U $_36 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_36 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_36 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_40 \/ ~proposition skolemFOFtoCNF_U $_35 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_40 \/ ~theme skolemFOFtoCNF_U $_40 $_35 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_40 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_40 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_36 \/
% 1.05/1.22     man $_35 (skolemFOFtoCNF_X24 $_35)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_42 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_42 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_42 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X1 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_U \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_42 \/
% 1.05/1.22     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_42 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_42 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_42 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_U \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_42 \/
% 1.05/1.22     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_50 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_51 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_50 \/ ~event skolemFOFtoCNF_U $_51 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_46 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_46 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_46 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_50 \/ ~present skolemFOFtoCNF_U $_51 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_50 \/ ~smoke skolemFOFtoCNF_U $_51 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_51 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_51 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_46
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_60 \/
% 1.05/1.22     ~agent $_60 $_61 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_59 skolemFOFtoCNF_X4 \/ ~event $_60 $_61 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_59 \/ ~forename skolemFOFtoCNF_U $_56 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_56 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_56 skolemFOFtoCNF_X4 \/ ~present $_60 $_61 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_59 \/ ~proposition skolemFOFtoCNF_U $_60 \/
% 1.05/1.22     ~smoke $_60 $_61 \/ ~theme skolemFOFtoCNF_U $_59 $_60 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_59 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_56 \/
% 1.05/1.22     man $_60 (skolemFOFtoCNF_X24 $_60)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_75 \/
% 1.05/1.22     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_80 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_80 \/ ~forename skolemFOFtoCNF_U $_74 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_76 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_76 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_74 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_76 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_80 \/ ~proposition skolemFOFtoCNF_U $_75 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_80 \/ ~theme skolemFOFtoCNF_U $_80 $_75 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_80 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_80 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_74 \/
% 1.05/1.22     man $_75 (skolemFOFtoCNF_X24 $_75)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_81 \/ ~forename skolemFOFtoCNF_U $_83 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_83 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_81 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_83 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X1 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_U \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_81 \/
% 1.05/1.22     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_81 \/ ~forename skolemFOFtoCNF_U $_83 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_83 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_81 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_83 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_U \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_81 \/
% 1.05/1.22     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_94 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_95 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_94 \/ ~event skolemFOFtoCNF_U $_95 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_89 \/ ~forename skolemFOFtoCNF_U $_90 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_90 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_89 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_90 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_94 \/ ~present skolemFOFtoCNF_U $_95 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_94 \/ ~smoke skolemFOFtoCNF_U $_95 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_95 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_95 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_89
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_100 \/
% 1.05/1.22     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent $_100 $_105 (skolemFOFtoCNF_X24 $_100) \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_106 skolemFOFtoCNF_X4 \/ ~event $_100 $_105 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_106 \/ ~forename skolemFOFtoCNF_U $_101 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_101 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_101 skolemFOFtoCNF_X4 \/ ~present $_100 $_105 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_106 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_100 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_100 $_105 \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_106 \/ ~theme skolemFOFtoCNF_U $_106 $_100 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_106 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_106 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_101
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_116 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_117 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_116 \/ ~event skolemFOFtoCNF_U $_117 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_111 \/ ~forename skolemFOFtoCNF_U $_112 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_112 \/
% 1.05/1.22     ~man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_111 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_112 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_116 \/ ~present skolemFOFtoCNF_U $_117 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_116 \/ ~smoke skolemFOFtoCNF_U $_117 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_116 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_116 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_111
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_123 \/
% 1.05/1.22     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_122 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_128 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_122 \/ ~event skolemFOFtoCNF_U $_128 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_124 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_124 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_124 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_122 \/ ~present skolemFOFtoCNF_U $_128 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_123 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_128 \/ ~theme skolemFOFtoCNF_U $_122 $_123 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_128 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_122 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_128 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_124 \/
% 1.05/1.22     man $_123 (skolemFOFtoCNF_X24 $_123)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_132 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_132 \/ ~forename skolemFOFtoCNF_U $_131 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_131 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_131 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_132 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_132 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_132 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_132 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_131 \/
% 1.05/1.22     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_132 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_132 \/ ~forename skolemFOFtoCNF_U $_131 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_131 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_131 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_132 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_132 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_132 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_132 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_131 \/
% 1.05/1.22     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_137 \/
% 1.05/1.22     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_141 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_143 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_141 \/ ~event skolemFOFtoCNF_U $_143 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_138 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_138 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_138 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_141 \/ ~present skolemFOFtoCNF_U $_143 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_137 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_143 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_141 skolemFOFtoCNF_U \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_143 $_137 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_141 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_143 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_138 \/
% 1.05/1.22     man $_137 (skolemFOFtoCNF_X24 $_137)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_146 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_146 \/ ~forename skolemFOFtoCNF_U $_145 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_145 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_145 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_146 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X1 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_146 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_146 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_145 \/
% 1.05/1.22     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_146 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_146 \/ ~forename skolemFOFtoCNF_U $_145 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_145 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_145 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_146 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_146 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_146 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_145 \/
% 1.05/1.22     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_161 \/
% 1.05/1.22     ~accessible_world skolemFOFtoCNF_U $_166 \/
% 1.05/1.22     ~agent $_166 $_167 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_165 skolemFOFtoCNF_X4 \/ ~event $_166 $_167 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_165 \/ ~forename skolemFOFtoCNF_U $_162 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_162 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_162 skolemFOFtoCNF_X4 \/ ~present $_166 $_167 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_165 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_161 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_166 \/ ~smoke $_166 $_167 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_165 $_161 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_165 $_166 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_165 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_162 \/
% 1.05/1.22     man $_161 (skolemFOFtoCNF_X24 $_161)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_171 \/
% 1.05/1.22     ~agent $_171 $_172 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event $_171 $_172 \/ ~forename skolemFOFtoCNF_U $_169 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_169 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_169 skolemFOFtoCNF_X4 \/ ~present $_171 $_172 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_171 \/ ~smoke $_171 $_172 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_171 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_169 \/
% 1.05/1.22     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_171 \/
% 1.05/1.22     ~agent $_171 $_172 skolemFOFtoCNF_X4 \/ ~event $_171 $_172 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_169 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_169 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_169 skolemFOFtoCNF_X4 \/ ~present $_171 $_172 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_171 \/ ~smoke $_171 $_172 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_171 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_169 \/
% 1.05/1.22     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_168 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_X2 $_172 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_X2 $_172 \/ ~forename skolemFOFtoCNF_U $_169 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_169 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_169 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_X2 $_172 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_168 \/ ~smoke skolemFOFtoCNF_X2 $_172 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_168 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_169 \/
% 1.05/1.22     man $_168 (skolemFOFtoCNF_X24 $_168)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_168 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_X7 $_172 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_X7 $_172 \/ ~forename skolemFOFtoCNF_U $_169 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_169 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_169 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_X7 $_172 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_168 \/ ~smoke skolemFOFtoCNF_X7 $_172 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_168 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_169 \/
% 1.05/1.22     man $_168 (skolemFOFtoCNF_X24 $_168)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_190 \/
% 1.05/1.22     ~agent $_190 $_191 (skolemFOFtoCNF_X24 $_190) \/
% 1.05/1.22     ~agent $_190 $_192 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_189 skolemFOFtoCNF_X4 \/ ~event $_190 $_191 \/
% 1.05/1.22     ~event $_190 $_192 \/ ~event skolemFOFtoCNF_U $_189 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_186 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_186 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_186 skolemFOFtoCNF_X4 \/ ~present $_190 $_191 \/
% 1.05/1.22     ~present $_190 $_192 \/ ~present skolemFOFtoCNF_U $_189 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_190 \/ ~smoke $_190 $_191 \/
% 1.05/1.22     ~smoke $_190 $_192 \/ ~theme skolemFOFtoCNF_U $_189 $_190 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_189 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_186
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_205 \/
% 1.05/1.22     ~agent $_205 $_206 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_204 $_199 \/ ~event $_205 $_206 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_204 \/ ~forename skolemFOFtoCNF_U $_200 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_201 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_201 \/ ~man skolemFOFtoCNF_U $_199 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_200 $_199 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_201 skolemFOFtoCNF_X4 \/ ~present $_205 $_206 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_204 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_205 \/ ~smoke $_205 $_206 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_204 $_205 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_204 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_200 \/
% 1.05/1.22     man $_205 (skolemFOFtoCNF_X24 $_205)
% 1.05/1.22  |- ~agent skolemFOFtoCNF_X7 $_218 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_X7 $_218 \/ ~present skolemFOFtoCNF_X7 $_218 \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_X7 $_218 \/
% 1.05/1.22     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 1.05/1.22  |- ~agent skolemFOFtoCNF_X2 $_225 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_X2 $_225 \/ ~present skolemFOFtoCNF_X2 $_225 \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_X2 $_225 \/
% 1.05/1.22     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_228 \/
% 1.05/1.22     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent $_228 $_233 (skolemFOFtoCNF_X24 $_228) \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_234 skolemFOFtoCNF_X4 \/ ~event $_228 $_233 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_234 \/ ~forename skolemFOFtoCNF_U $_227 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_229 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_229 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_227 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_229 skolemFOFtoCNF_X4 \/ ~present $_228 $_233 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_234 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_228 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_228 $_233 \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_234 \/ ~theme skolemFOFtoCNF_U $_234 $_228 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_234 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_234 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_227
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_241 \/
% 1.05/1.22     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_245 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_247 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_245 \/ ~event skolemFOFtoCNF_U $_247 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_240 \/ ~forename skolemFOFtoCNF_U $_242 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_242 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_240 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_242 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_245 \/ ~present skolemFOFtoCNF_U $_247 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_241 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_247 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_245 skolemFOFtoCNF_U \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_247 $_241 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_245 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_247 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_240 \/
% 1.05/1.22     man $_241 (skolemFOFtoCNF_X24 $_241)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_251 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_251 \/ ~forename skolemFOFtoCNF_U $_248 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_250 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_250 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_248 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_250 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_251 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X1 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_251 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_251 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_248 \/
% 1.05/1.22     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_251 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_251 \/ ~forename skolemFOFtoCNF_U $_248 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_250 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_250 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_248 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_250 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_251 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_251 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_251 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_248 \/
% 1.05/1.22     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_261 \/
% 1.05/1.22     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_260 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_266 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_260 \/ ~event skolemFOFtoCNF_U $_266 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_259 \/ ~forename skolemFOFtoCNF_U $_262 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_262 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_259 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_262 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_260 \/ ~present skolemFOFtoCNF_U $_266 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_261 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_266 \/ ~theme skolemFOFtoCNF_U $_260 $_261 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_266 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_260 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_266 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_259 \/
% 1.05/1.22     man $_261 (skolemFOFtoCNF_X24 $_261)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_271 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_271 \/ ~forename skolemFOFtoCNF_U $_267 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_270 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_270 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_267 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_270 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_271 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_271 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_271 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_271 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_267 \/
% 1.05/1.22     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_271 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_271 \/ ~forename skolemFOFtoCNF_U $_267 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_270 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_270 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_267 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_270 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_271 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_271 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_271 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_271 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_267 \/
% 1.05/1.22     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_283 \/
% 1.05/1.22     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent $_283 $_285 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_284 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.22     ~event $_283 $_285 \/ ~event skolemFOFtoCNF_U $_284 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_278 \/ ~forename skolemFOFtoCNF_U $_280 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_280 \/
% 1.05/1.22     ~man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_278 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_280 skolemFOFtoCNF_X4 \/ ~present $_283 $_285 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_284 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_283 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_283 $_285 \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_284 \/ ~theme skolemFOFtoCNF_U $_284 $_283 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_284 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_284 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_278
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_292 \/
% 1.05/1.22     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent $_292 $_297 (skolemFOFtoCNF_X24 $_292) \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_291 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_298 skolemFOFtoCNF_X4 \/ ~event $_292 $_297 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_291 \/ ~event skolemFOFtoCNF_U $_298 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_293 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_293 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_293 skolemFOFtoCNF_X4 \/ ~present $_292 $_297 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_291 \/ ~present skolemFOFtoCNF_U $_298 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_292 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_292 $_297 \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_298 \/ ~theme skolemFOFtoCNF_U $_291 $_292 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_298 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_291 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_298 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_293
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_304 \/
% 1.05/1.22     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent $_304 $_310 (skolemFOFtoCNF_X24 $_304) \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_308 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_311 skolemFOFtoCNF_X4 \/ ~event $_304 $_310 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_308 \/ ~event skolemFOFtoCNF_U $_311 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_305 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_305 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_305 skolemFOFtoCNF_X4 \/ ~present $_304 $_310 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_308 \/ ~present skolemFOFtoCNF_U $_311 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_304 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_304 $_310 \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_311 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_308 skolemFOFtoCNF_U \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_311 $_304 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_308 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_311 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_305
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_318 \/
% 1.05/1.22     ~accessible_world skolemFOFtoCNF_U $_323 \/
% 1.05/1.22     ~agent $_318 $_324 (skolemFOFtoCNF_X24 $_318) \/
% 1.05/1.22     ~agent $_323 $_325 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_322 skolemFOFtoCNF_X4 \/ ~event $_318 $_324 \/
% 1.05/1.22     ~event $_323 $_325 \/ ~event skolemFOFtoCNF_U $_322 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_319 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_319 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_319 skolemFOFtoCNF_X4 \/ ~present $_318 $_324 \/
% 1.05/1.22     ~present $_323 $_325 \/ ~present skolemFOFtoCNF_U $_322 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_318 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_323 \/ ~smoke $_318 $_324 \/
% 1.05/1.22     ~smoke $_323 $_325 \/ ~theme skolemFOFtoCNF_U $_322 $_318 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_322 $_323 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_322 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_319
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_334 \/
% 1.05/1.22     ~accessible_world skolemFOFtoCNF_U $_339 \/
% 1.05/1.22     ~agent $_339 $_340 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_333 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_338 skolemFOFtoCNF_X4 \/ ~event $_339 $_340 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_333 \/ ~event skolemFOFtoCNF_U $_338 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_335 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_335 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_335 skolemFOFtoCNF_X4 \/ ~present $_339 $_340 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_333 \/ ~present skolemFOFtoCNF_U $_338 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_334 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_339 \/ ~smoke $_339 $_340 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_333 $_334 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_338 $_339 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_333 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_338 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_335 \/
% 1.05/1.22     man $_334 (skolemFOFtoCNF_X24 $_334)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_345 \/
% 1.05/1.22     ~agent $_345 $_346 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_344 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event $_345 $_346 \/ ~event skolemFOFtoCNF_U $_344 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_343 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_343 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_343 skolemFOFtoCNF_X4 \/ ~present $_345 $_346 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_344 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_345 \/ ~smoke $_345 $_346 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_344 $_345 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_344 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_343 \/
% 1.05/1.22     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_345 \/
% 1.05/1.22     ~agent $_345 $_346 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_344 skolemFOFtoCNF_X4 \/ ~event $_345 $_346 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_344 \/ ~forename skolemFOFtoCNF_U $_343 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_343 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_343 skolemFOFtoCNF_X4 \/ ~present $_345 $_346 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_344 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_345 \/ ~smoke $_345 $_346 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_344 $_345 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_344 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_343 \/
% 1.05/1.22     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_342 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_341 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_X2 $_346 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_341 \/ ~event skolemFOFtoCNF_X2 $_346 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_343 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_343 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_343 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_341 \/ ~present skolemFOFtoCNF_X2 $_346 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_342 \/ ~smoke skolemFOFtoCNF_X2 $_346 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_341 $_342 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_341 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_343 \/
% 1.05/1.22     man $_342 (skolemFOFtoCNF_X24 $_342)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_342 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_341 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_X7 $_346 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_341 \/ ~event skolemFOFtoCNF_X7 $_346 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_343 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_343 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_343 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_341 \/ ~present skolemFOFtoCNF_X7 $_346 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_342 \/ ~smoke skolemFOFtoCNF_X7 $_346 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_341 $_342 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_341 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_343 \/
% 1.05/1.22     man $_342 (skolemFOFtoCNF_X24 $_342)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_374 \/
% 1.05/1.22     ~accessible_world skolemFOFtoCNF_U $_379 \/
% 1.05/1.22     ~agent $_379 $_380 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_378 $_372 \/ ~event $_379 $_380 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_378 \/ ~forename skolemFOFtoCNF_U $_373 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_375 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_375 \/ ~man skolemFOFtoCNF_U $_372 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_373 $_372 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_375 skolemFOFtoCNF_X4 \/ ~present $_379 $_380 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_378 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_374 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_379 \/ ~smoke $_379 $_380 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_378 $_374 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_378 $_379 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_378 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_373 \/
% 1.05/1.22     man $_374 (skolemFOFtoCNF_X24 $_374)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_386 \/
% 1.05/1.22     ~agent $_386 $_387 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_381 \/ ~event $_386 $_387 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_382 \/ ~forename skolemFOFtoCNF_U $_384 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_384 \/ ~man skolemFOFtoCNF_U $_381 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_382 $_381 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_384 skolemFOFtoCNF_X4 \/ ~present $_386 $_387 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_386 \/ ~smoke $_386 $_387 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_386 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_382 \/
% 1.05/1.22     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_386 \/
% 1.05/1.22     ~agent $_386 $_387 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_381 \/ ~event $_386 $_387 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_382 \/ ~forename skolemFOFtoCNF_U $_384 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_384 \/ ~man skolemFOFtoCNF_U $_381 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_382 $_381 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_384 skolemFOFtoCNF_X4 \/ ~present $_386 $_387 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_386 \/ ~smoke $_386 $_387 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_386 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_382 \/
% 1.05/1.22     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_383 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_381 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_X2 $_387 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_X2 $_387 \/ ~forename skolemFOFtoCNF_U $_382 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_384 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_384 \/ ~man skolemFOFtoCNF_U $_381 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_382 $_381 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_384 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_X2 $_387 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_383 \/ ~smoke skolemFOFtoCNF_X2 $_387 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_383 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_382 \/
% 1.05/1.22     man $_383 (skolemFOFtoCNF_X24 $_383)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_383 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_381 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_X7 $_387 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_X7 $_387 \/ ~forename skolemFOFtoCNF_U $_382 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_384 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_384 \/ ~man skolemFOFtoCNF_U $_381 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_382 $_381 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_384 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_X7 $_387 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_383 \/ ~smoke skolemFOFtoCNF_X7 $_387 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_383 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_382 \/
% 1.05/1.22     man $_383 (skolemFOFtoCNF_X24 $_383)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_415 \/
% 1.05/1.22     ~agent $_415 $_416 (skolemFOFtoCNF_X24 $_415) \/
% 1.05/1.22     ~agent $_415 $_417 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_414 $_409 \/ ~event $_415 $_416 \/
% 1.05/1.22     ~event $_415 $_417 \/ ~event skolemFOFtoCNF_U $_414 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_410 \/ ~forename skolemFOFtoCNF_U $_411 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_411 \/ ~man skolemFOFtoCNF_U $_409 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_410 $_409 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_411 skolemFOFtoCNF_X4 \/ ~present $_415 $_416 \/
% 1.05/1.22     ~present $_415 $_417 \/ ~present skolemFOFtoCNF_U $_414 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_415 \/ ~smoke $_415 $_416 \/
% 1.05/1.22     ~smoke $_415 $_417 \/ ~theme skolemFOFtoCNF_U $_414 $_415 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_414 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_410
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U $_428 \/
% 1.05/1.22     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_427 $_425 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_433 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_427 \/ ~event skolemFOFtoCNF_U $_433 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_426 \/ ~forename skolemFOFtoCNF_U $_429 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_429 \/ ~man skolemFOFtoCNF_U $_425 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_426 $_425 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_429 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_427 \/ ~present skolemFOFtoCNF_U $_433 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U $_428 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_433 \/ ~theme skolemFOFtoCNF_U $_427 $_428 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_433 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_427 \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_433 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_426 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_429 \/
% 1.05/1.22     man $_428 (skolemFOFtoCNF_X24 $_428)
% 1.05/1.22  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U $_439 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_434 \/
% 1.05/1.22     ~event skolemFOFtoCNF_U $_439 \/ ~forename skolemFOFtoCNF_U $_435 \/
% 1.05/1.22     ~forename skolemFOFtoCNF_U $_438 \/
% 1.05/1.22     ~jules_forename skolemFOFtoCNF_U $_438 \/ ~man skolemFOFtoCNF_U $_434 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_435 $_434 \/
% 1.05/1.22     ~of skolemFOFtoCNF_U $_438 skolemFOFtoCNF_X4 \/
% 1.05/1.22     ~present skolemFOFtoCNF_U $_439 \/
% 1.05/1.22     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.22     ~smoke skolemFOFtoCNF_U $_439 \/
% 1.05/1.22     ~theme skolemFOFtoCNF_U $_439 skolemFOFtoCNF_U \/
% 1.05/1.22     ~think_believe_consider skolemFOFtoCNF_U $_439 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_435 \/
% 1.05/1.22     ~vincent_forename skolemFOFtoCNF_U $_438 \/
% 1.05/1.22     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U $_446 \/
% 1.05/1.23     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_450 $_444 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_452 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~event skolemFOFtoCNF_U $_450 \/ ~event skolemFOFtoCNF_U $_452 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_445 \/ ~forename skolemFOFtoCNF_U $_447 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_447 \/ ~man skolemFOFtoCNF_U $_444 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_445 $_444 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_447 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~present skolemFOFtoCNF_U $_450 \/ ~present skolemFOFtoCNF_U $_452 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U $_446 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~smoke skolemFOFtoCNF_U $_452 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_450 skolemFOFtoCNF_U \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_452 $_446 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_450 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_452 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_445 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_447 \/
% 1.05/1.23     man $_446 (skolemFOFtoCNF_X24 $_446)
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_457 $_453 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~event skolemFOFtoCNF_U $_457 \/ ~forename skolemFOFtoCNF_U $_454 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_456 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_456 \/ ~man skolemFOFtoCNF_U $_453 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_454 $_453 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_456 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~present skolemFOFtoCNF_U $_457 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X1 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_457 skolemFOFtoCNF_U \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_457 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_454 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_456 \/
% 1.05/1.23     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_457 $_453 \/ ~event skolemFOFtoCNF_U $_457 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_454 \/ ~forename skolemFOFtoCNF_U $_456 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_456 \/ ~man skolemFOFtoCNF_U $_453 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_454 $_453 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_456 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~present skolemFOFtoCNF_U $_457 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_457 skolemFOFtoCNF_U \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_457 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_454 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_456 \/
% 1.05/1.23     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U $_469 \/
% 1.05/1.23     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~agent $_469 $_474 (skolemFOFtoCNF_X24 $_469) \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_468 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_475 skolemFOFtoCNF_X4 \/ ~event $_469 $_474 \/
% 1.05/1.23     ~event skolemFOFtoCNF_U $_468 \/ ~event skolemFOFtoCNF_U $_475 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_467 \/ ~forename skolemFOFtoCNF_U $_470 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_470 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_467 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_470 skolemFOFtoCNF_X4 \/ ~present $_469 $_474 \/
% 1.05/1.23     ~present skolemFOFtoCNF_U $_468 \/ ~present skolemFOFtoCNF_U $_475 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U $_469 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_469 $_474 \/
% 1.05/1.23     ~smoke skolemFOFtoCNF_U $_475 \/ ~theme skolemFOFtoCNF_U $_468 $_469 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_475 skolemFOFtoCNF_U \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_468 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_475 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_467
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U $_483 \/
% 1.05/1.23     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~agent $_483 $_489 (skolemFOFtoCNF_X24 $_483) \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_487 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_490 skolemFOFtoCNF_X4 \/ ~event $_483 $_489 \/
% 1.05/1.23     ~event skolemFOFtoCNF_U $_487 \/ ~event skolemFOFtoCNF_U $_490 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_482 \/ ~forename skolemFOFtoCNF_U $_484 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_484 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_482 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_484 skolemFOFtoCNF_X4 \/ ~present $_483 $_489 \/
% 1.05/1.23     ~present skolemFOFtoCNF_U $_487 \/ ~present skolemFOFtoCNF_U $_490 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U $_483 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_483 $_489 \/
% 1.05/1.23     ~smoke skolemFOFtoCNF_U $_490 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_487 skolemFOFtoCNF_U \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_490 $_483 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_487 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_490 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_482
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U $_503 \/
% 1.05/1.23     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~agent $_503 $_505 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_498 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_504 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.23     ~event $_503 $_505 \/ ~event skolemFOFtoCNF_U $_498 \/
% 1.05/1.23     ~event skolemFOFtoCNF_U $_504 \/ ~forename skolemFOFtoCNF_U $_497 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_500 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_500 \/
% 1.05/1.23     ~man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_497 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_500 skolemFOFtoCNF_X4 \/ ~present $_503 $_505 \/
% 1.05/1.23     ~present skolemFOFtoCNF_U $_498 \/ ~present skolemFOFtoCNF_U $_504 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U $_503 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_503 $_505 \/
% 1.05/1.23     ~smoke skolemFOFtoCNF_U $_504 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_498 skolemFOFtoCNF_U \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_504 $_503 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_498 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_504 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_497
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U $_518 \/
% 1.05/1.23     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~agent $_518 $_520 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_517 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_519 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.23     ~event $_518 $_520 \/ ~event skolemFOFtoCNF_U $_517 \/
% 1.05/1.23     ~event skolemFOFtoCNF_U $_519 \/ ~forename skolemFOFtoCNF_U $_512 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_514 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_514 \/
% 1.05/1.23     ~man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_512 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_514 skolemFOFtoCNF_X4 \/ ~present $_518 $_520 \/
% 1.05/1.23     ~present skolemFOFtoCNF_U $_517 \/ ~present skolemFOFtoCNF_U $_519 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U $_518 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_518 $_520 \/
% 1.05/1.23     ~smoke skolemFOFtoCNF_U $_519 \/ ~theme skolemFOFtoCNF_U $_517 $_518 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_519 skolemFOFtoCNF_U \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_517 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_519 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_512
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U $_533 \/
% 1.05/1.23     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~agent $_533 $_535 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_532 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_534 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.23     ~event $_533 $_535 \/ ~event skolemFOFtoCNF_U $_532 \/
% 1.05/1.23     ~event skolemFOFtoCNF_U $_534 \/ ~forename skolemFOFtoCNF_U $_527 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_529 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_529 \/
% 1.05/1.23     ~man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_527 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_529 skolemFOFtoCNF_X4 \/ ~present $_533 $_535 \/
% 1.05/1.23     ~present skolemFOFtoCNF_U $_532 \/ ~present skolemFOFtoCNF_U $_534 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U $_533 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_533 $_535 \/
% 1.05/1.23     ~smoke skolemFOFtoCNF_U $_534 \/ ~theme skolemFOFtoCNF_U $_532 $_533 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_534 skolemFOFtoCNF_U \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_532 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_534 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_527 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_529
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U $_548 \/
% 1.05/1.23     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~agent $_548 $_550 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_543 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_549 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.23     ~event $_548 $_550 \/ ~event skolemFOFtoCNF_U $_543 \/
% 1.05/1.23     ~event skolemFOFtoCNF_U $_549 \/ ~forename skolemFOFtoCNF_U $_542 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_545 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_545 \/
% 1.05/1.23     ~man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_542 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_545 skolemFOFtoCNF_X4 \/ ~present $_548 $_550 \/
% 1.05/1.23     ~present skolemFOFtoCNF_U $_543 \/ ~present skolemFOFtoCNF_U $_549 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U $_548 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_548 $_550 \/
% 1.05/1.23     ~smoke skolemFOFtoCNF_U $_549 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_543 skolemFOFtoCNF_U \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_549 $_548 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_543 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_549 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_542 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_545
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U $_560 \/
% 1.05/1.23     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_564 $_557 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_566 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~event skolemFOFtoCNF_U $_564 \/ ~event skolemFOFtoCNF_U $_566 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_558 \/ ~forename skolemFOFtoCNF_U $_559 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_561 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_561 \/ ~man skolemFOFtoCNF_U $_557 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_558 $_557 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_559 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_561 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~present skolemFOFtoCNF_U $_564 \/ ~present skolemFOFtoCNF_U $_566 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U $_560 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~smoke skolemFOFtoCNF_U $_566 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_564 skolemFOFtoCNF_U \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_566 $_560 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_564 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_566 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_558 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_559 \/
% 1.05/1.23     man $_560 (skolemFOFtoCNF_X24 $_560)
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_572 $_567 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~event skolemFOFtoCNF_U $_572 \/ ~forename skolemFOFtoCNF_U $_568 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_569 \/ ~forename skolemFOFtoCNF_U $_571 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_571 \/ ~man skolemFOFtoCNF_U $_567 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_568 $_567 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_569 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_571 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~present skolemFOFtoCNF_U $_572 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X1 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_572 skolemFOFtoCNF_U \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_572 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_568 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_569 \/
% 1.05/1.23     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_572 $_567 \/ ~event skolemFOFtoCNF_U $_572 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_568 \/ ~forename skolemFOFtoCNF_U $_569 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_571 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_571 \/ ~man skolemFOFtoCNF_U $_567 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_568 $_567 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_569 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_571 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~present skolemFOFtoCNF_U $_572 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_572 skolemFOFtoCNF_U \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_572 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_568 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_569 \/
% 1.05/1.23     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U $_588 \/
% 1.05/1.23     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_587 $_585 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_593 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~event skolemFOFtoCNF_U $_587 \/ ~event skolemFOFtoCNF_U $_593 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_584 \/ ~forename skolemFOFtoCNF_U $_586 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_589 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_589 \/ ~man skolemFOFtoCNF_U $_585 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_584 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_586 $_585 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_589 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~present skolemFOFtoCNF_U $_587 \/ ~present skolemFOFtoCNF_U $_593 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U $_588 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~smoke skolemFOFtoCNF_U $_593 \/ ~theme skolemFOFtoCNF_U $_587 $_588 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_593 skolemFOFtoCNF_U \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_587 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_593 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_584 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_586 \/
% 1.05/1.23     man $_588 (skolemFOFtoCNF_X24 $_588)
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_600 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_595 \/
% 1.05/1.23     ~event skolemFOFtoCNF_U $_600 \/ ~forename skolemFOFtoCNF_U $_594 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_596 \/ ~forename skolemFOFtoCNF_U $_599 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_599 \/ ~man skolemFOFtoCNF_U $_595 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_594 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_596 $_595 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_599 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~present skolemFOFtoCNF_U $_600 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~smoke skolemFOFtoCNF_U $_600 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_600 skolemFOFtoCNF_U \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_600 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_594 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_596 \/
% 1.05/1.23     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U $_608 \/
% 1.05/1.23     ~accessible_world skolemFOFtoCNF_U $_613 \/
% 1.05/1.23     ~agent $_608 $_614 (skolemFOFtoCNF_X24 $_608) \/
% 1.05/1.23     ~agent $_613 $_615 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_607 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_612 skolemFOFtoCNF_X4 \/ ~event $_608 $_614 \/
% 1.05/1.23     ~event $_613 $_615 \/ ~event skolemFOFtoCNF_U $_607 \/
% 1.05/1.23     ~event skolemFOFtoCNF_U $_612 \/ ~forename skolemFOFtoCNF_U $_609 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_609 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_609 skolemFOFtoCNF_X4 \/ ~present $_608 $_614 \/
% 1.05/1.23     ~present $_613 $_615 \/ ~present skolemFOFtoCNF_U $_607 \/
% 1.05/1.23     ~present skolemFOFtoCNF_U $_612 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U $_608 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U $_613 \/ ~smoke $_608 $_614 \/
% 1.05/1.23     ~smoke $_613 $_615 \/ ~theme skolemFOFtoCNF_U $_607 $_608 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_612 $_613 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_607 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_612 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_609
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U $_626 \/
% 1.05/1.23     ~accessible_world skolemFOFtoCNF_U $_631 \/
% 1.05/1.23     ~agent $_626 $_632 (skolemFOFtoCNF_X24 $_626) \/
% 1.05/1.23     ~agent $_631 $_633 skolemFOFtoCNF_X4 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_630 $_624 \/ ~event $_626 $_632 \/
% 1.05/1.23     ~event $_631 $_633 \/ ~event skolemFOFtoCNF_U $_630 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_625 \/ ~forename skolemFOFtoCNF_U $_627 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_627 \/ ~man skolemFOFtoCNF_U $_624 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_625 $_624 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_627 skolemFOFtoCNF_X4 \/ ~present $_626 $_632 \/
% 1.05/1.23     ~present $_631 $_633 \/ ~present skolemFOFtoCNF_U $_630 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U $_626 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U $_631 \/ ~smoke $_626 $_632 \/
% 1.05/1.23     ~smoke $_631 $_633 \/ ~theme skolemFOFtoCNF_U $_630 $_626 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_630 $_631 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_630 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_625
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U $_645 \/
% 1.05/1.23     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~agent $_645 $_650 (skolemFOFtoCNF_X24 $_645) \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_644 $_642 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_651 skolemFOFtoCNF_X4 \/ ~event $_645 $_650 \/
% 1.05/1.23     ~event skolemFOFtoCNF_U $_644 \/ ~event skolemFOFtoCNF_U $_651 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_643 \/ ~forename skolemFOFtoCNF_U $_646 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_646 \/ ~man skolemFOFtoCNF_U $_642 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_643 $_642 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_646 skolemFOFtoCNF_X4 \/ ~present $_645 $_650 \/
% 1.05/1.23     ~present skolemFOFtoCNF_U $_644 \/ ~present skolemFOFtoCNF_U $_651 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U $_645 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_645 $_650 \/
% 1.05/1.23     ~smoke skolemFOFtoCNF_U $_651 \/ ~theme skolemFOFtoCNF_U $_644 $_645 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_651 skolemFOFtoCNF_U \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_644 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_651 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_643 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_646
% 1.05/1.23  |- ~accessible_world skolemFOFtoCNF_U $_661 \/
% 1.05/1.23     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.05/1.23     ~agent $_661 $_667 (skolemFOFtoCNF_X24 $_661) \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_665 $_659 \/
% 1.05/1.23     ~agent skolemFOFtoCNF_U $_668 skolemFOFtoCNF_X4 \/ ~event $_661 $_667 \/
% 1.05/1.23     ~event skolemFOFtoCNF_U $_665 \/ ~event skolemFOFtoCNF_U $_668 \/
% 1.05/1.23     ~forename skolemFOFtoCNF_U $_660 \/ ~forename skolemFOFtoCNF_U $_662 \/
% 1.05/1.23     ~jules_forename skolemFOFtoCNF_U $_662 \/ ~man skolemFOFtoCNF_U $_659 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_660 $_659 \/
% 1.05/1.23     ~of skolemFOFtoCNF_U $_662 skolemFOFtoCNF_X4 \/ ~present $_661 $_667 \/
% 1.05/1.23     ~present skolemFOFtoCNF_U $_665 \/ ~present skolemFOFtoCNF_U $_668 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U $_661 \/
% 1.05/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_661 $_667 \/
% 1.05/1.23     ~smoke skolemFOFtoCNF_U $_668 \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_665 skolemFOFtoCNF_U \/
% 1.05/1.23     ~theme skolemFOFtoCNF_U $_668 $_661 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_665 \/
% 1.05/1.23     ~think_believe_consider skolemFOFtoCNF_U $_668 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_660 \/
% 1.05/1.23     ~vincent_forename skolemFOFtoCNF_U $_662
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_680 \/
% 1.08/1.23     ~accessible_world skolemFOFtoCNF_U $_685 \/
% 1.08/1.23     ~agent $_685 $_686 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_679 $_677 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_684 $_677 \/ ~event $_685 $_686 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_679 \/ ~event skolemFOFtoCNF_U $_684 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_678 \/ ~forename skolemFOFtoCNF_U $_681 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_681 \/ ~man skolemFOFtoCNF_U $_677 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_678 $_677 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_681 skolemFOFtoCNF_X4 \/ ~present $_685 $_686 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_679 \/ ~present skolemFOFtoCNF_U $_684 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_680 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_685 \/ ~smoke $_685 $_686 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_679 $_680 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_684 $_685 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_679 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_684 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_678 \/
% 1.08/1.23     man $_680 (skolemFOFtoCNF_X24 $_680)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_693 \/
% 1.08/1.23     ~agent $_693 $_694 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_692 $_687 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_687 \/ ~event $_693 $_694 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_692 \/ ~forename skolemFOFtoCNF_U $_688 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_691 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_691 \/ ~man skolemFOFtoCNF_U $_687 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_688 $_687 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_691 skolemFOFtoCNF_X4 \/ ~present $_693 $_694 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_692 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_693 \/ ~smoke $_693 $_694 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_692 $_693 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_692 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_688 \/
% 1.08/1.23     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_693 \/
% 1.08/1.23     ~agent $_693 $_694 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_692 $_687 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_687 \/ ~event $_693 $_694 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_692 \/ ~forename skolemFOFtoCNF_U $_688 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_691 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_691 \/ ~man skolemFOFtoCNF_U $_687 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_688 $_687 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_691 skolemFOFtoCNF_X4 \/ ~present $_693 $_694 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_692 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_693 \/ ~smoke $_693 $_694 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_692 $_693 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_692 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_688 \/
% 1.08/1.23     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_690 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_689 $_687 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_687 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_X2 $_694 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_689 \/ ~event skolemFOFtoCNF_X2 $_694 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_688 \/ ~forename skolemFOFtoCNF_U $_691 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_691 \/ ~man skolemFOFtoCNF_U $_687 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_688 $_687 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_691 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_689 \/ ~present skolemFOFtoCNF_X2 $_694 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_690 \/ ~smoke skolemFOFtoCNF_X2 $_694 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_689 $_690 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_689 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_688 \/
% 1.08/1.23     man $_690 (skolemFOFtoCNF_X24 $_690)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_690 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_689 $_687 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_687 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_X7 $_694 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_689 \/ ~event skolemFOFtoCNF_X7 $_694 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_688 \/ ~forename skolemFOFtoCNF_U $_691 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_691 \/ ~man skolemFOFtoCNF_U $_687 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_688 $_687 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_691 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_689 \/ ~present skolemFOFtoCNF_X7 $_694 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_690 \/ ~smoke skolemFOFtoCNF_X7 $_694 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_689 $_690 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_689 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_688 \/
% 1.08/1.23     man $_690 (skolemFOFtoCNF_X24 $_690)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_755 \/
% 1.08/1.23     ~accessible_world skolemFOFtoCNF_U $_760 \/
% 1.08/1.23     ~agent $_760 $_761 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_754 $_752 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_759 skolemFOFtoCNF_X4 \/ ~event $_760 $_761 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_754 \/ ~event skolemFOFtoCNF_U $_759 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_753 \/ ~forename skolemFOFtoCNF_U $_756 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_756 \/ ~man skolemFOFtoCNF_U $_752 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_753 $_752 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_756 skolemFOFtoCNF_X4 \/ ~present $_760 $_761 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_754 \/ ~present skolemFOFtoCNF_U $_759 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_755 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_760 \/ ~smoke $_760 $_761 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_754 $_755 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_759 $_760 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_754 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_759 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_753 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_756 \/
% 1.08/1.23     man $_755 (skolemFOFtoCNF_X24 $_755)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_768 \/
% 1.08/1.23     ~agent $_768 $_769 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_767 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_762 \/ ~event $_768 $_769 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_767 \/ ~forename skolemFOFtoCNF_U $_763 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_766 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_766 \/ ~man skolemFOFtoCNF_U $_762 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_763 $_762 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_766 skolemFOFtoCNF_X4 \/ ~present $_768 $_769 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_767 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_768 \/ ~smoke $_768 $_769 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_767 $_768 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_767 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_763 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_766 \/
% 1.08/1.23     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_765 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_764 $_762 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_X2 $_769 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_764 \/ ~event skolemFOFtoCNF_X2 $_769 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_763 \/ ~forename skolemFOFtoCNF_U $_766 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_766 \/ ~man skolemFOFtoCNF_U $_762 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_763 $_762 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_766 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_764 \/ ~present skolemFOFtoCNF_X2 $_769 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_765 \/ ~smoke skolemFOFtoCNF_X2 $_769 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_764 $_765 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_764 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_763 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_766 \/
% 1.08/1.23     man $_765 (skolemFOFtoCNF_X24 $_765)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_765 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_764 $_762 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_X7 $_769 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_764 \/ ~event skolemFOFtoCNF_X7 $_769 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_763 \/ ~forename skolemFOFtoCNF_U $_766 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_766 \/ ~man skolemFOFtoCNF_U $_762 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_763 $_762 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_766 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_764 \/ ~present skolemFOFtoCNF_X7 $_769 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_765 \/ ~smoke skolemFOFtoCNF_X7 $_769 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_764 $_765 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_764 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_763 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_766 \/
% 1.08/1.23     man $_765 (skolemFOFtoCNF_X24 $_765)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_800 \/
% 1.08/1.23     ~accessible_world skolemFOFtoCNF_U $_805 \/
% 1.08/1.23     ~agent $_805 $_806 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_799 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_804 $_797 \/ ~event $_805 $_806 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_799 \/ ~event skolemFOFtoCNF_U $_804 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_798 \/ ~forename skolemFOFtoCNF_U $_801 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_801 \/ ~man skolemFOFtoCNF_U $_797 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_798 $_797 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_801 skolemFOFtoCNF_X4 \/ ~present $_805 $_806 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_799 \/ ~present skolemFOFtoCNF_U $_804 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_800 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_805 \/ ~smoke $_805 $_806 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_799 $_800 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_804 $_805 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_799 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_804 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_798 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_801 \/
% 1.08/1.23     man $_800 (skolemFOFtoCNF_X24 $_800)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_813 \/
% 1.08/1.23     ~agent $_813 $_814 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_812 $_807 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~event $_813 $_814 \/ ~event skolemFOFtoCNF_U $_812 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_808 \/ ~forename skolemFOFtoCNF_U $_811 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_811 \/ ~man skolemFOFtoCNF_U $_807 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_808 $_807 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_811 skolemFOFtoCNF_X4 \/ ~present $_813 $_814 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_812 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_813 \/ ~smoke $_813 $_814 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_812 $_813 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_812 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_808 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_811 \/
% 1.08/1.23     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_813 \/
% 1.08/1.23     ~agent $_813 $_814 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_812 $_807 \/ ~event $_813 $_814 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_812 \/ ~forename skolemFOFtoCNF_U $_808 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_811 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_811 \/ ~man skolemFOFtoCNF_U $_807 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_808 $_807 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_811 skolemFOFtoCNF_X4 \/ ~present $_813 $_814 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_812 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_813 \/ ~smoke $_813 $_814 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_812 $_813 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_812 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_808 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_811 \/
% 1.08/1.23     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_810 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_809 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_807 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_X2 $_814 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_809 \/ ~event skolemFOFtoCNF_X2 $_814 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_808 \/ ~forename skolemFOFtoCNF_U $_811 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_811 \/ ~man skolemFOFtoCNF_U $_807 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_808 $_807 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_811 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_809 \/ ~present skolemFOFtoCNF_X2 $_814 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_810 \/ ~smoke skolemFOFtoCNF_X2 $_814 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_809 $_810 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_809 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_808 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_811 \/
% 1.08/1.23     man $_810 (skolemFOFtoCNF_X24 $_810)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_844 \/
% 1.08/1.23     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.08/1.23     ~agent $_844 $_850 (skolemFOFtoCNF_X24 $_844) \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_848 $_841 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_851 skolemFOFtoCNF_X4 \/ ~event $_844 $_850 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_848 \/ ~event skolemFOFtoCNF_U $_851 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_842 \/ ~forename skolemFOFtoCNF_U $_843 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_845 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_845 \/ ~man skolemFOFtoCNF_U $_841 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_842 $_841 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_843 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_845 skolemFOFtoCNF_X4 \/ ~present $_844 $_850 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_848 \/ ~present skolemFOFtoCNF_U $_851 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_844 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_844 $_850 \/
% 1.08/1.23     ~smoke skolemFOFtoCNF_U $_851 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_848 skolemFOFtoCNF_U \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_851 $_844 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_848 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_851 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_842 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_843
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_864 \/
% 1.08/1.23     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.08/1.23     ~agent $_864 $_869 (skolemFOFtoCNF_X24 $_864) \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_863 $_861 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_870 skolemFOFtoCNF_X4 \/ ~event $_864 $_869 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_863 \/ ~event skolemFOFtoCNF_U $_870 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_860 \/ ~forename skolemFOFtoCNF_U $_862 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_865 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_865 \/ ~man skolemFOFtoCNF_U $_861 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_860 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_862 $_861 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_865 skolemFOFtoCNF_X4 \/ ~present $_864 $_869 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_863 \/ ~present skolemFOFtoCNF_U $_870 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_864 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_864 $_869 \/
% 1.08/1.23     ~smoke skolemFOFtoCNF_U $_870 \/ ~theme skolemFOFtoCNF_U $_863 $_864 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_870 skolemFOFtoCNF_U \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_863 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_870 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_860 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_862
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_887 \/
% 1.08/1.23     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.08/1.23     ~agent $_887 $_889 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_886 $_879 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_888 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.08/1.23     ~event $_887 $_889 \/ ~event skolemFOFtoCNF_U $_886 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_888 \/ ~forename skolemFOFtoCNF_U $_880 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_881 \/ ~forename skolemFOFtoCNF_U $_883 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_883 \/ ~man skolemFOFtoCNF_U $_879 \/
% 1.08/1.23     ~man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_880 $_879 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_881 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_883 skolemFOFtoCNF_X4 \/ ~present $_887 $_889 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_886 \/ ~present skolemFOFtoCNF_U $_888 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_887 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_887 $_889 \/
% 1.08/1.23     ~smoke skolemFOFtoCNF_U $_888 \/ ~theme skolemFOFtoCNF_U $_886 $_887 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_888 skolemFOFtoCNF_U \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_886 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_888 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_880 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_881
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_906 \/
% 1.08/1.23     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 1.08/1.23     ~agent $_906 $_908 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_901 $_899 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_907 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.08/1.23     ~event $_906 $_908 \/ ~event skolemFOFtoCNF_U $_901 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_907 \/ ~forename skolemFOFtoCNF_U $_898 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_900 \/ ~forename skolemFOFtoCNF_U $_903 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_903 \/ ~man skolemFOFtoCNF_U $_899 \/
% 1.08/1.23     ~man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_898 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_900 $_899 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_903 skolemFOFtoCNF_X4 \/ ~present $_906 $_908 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_901 \/ ~present skolemFOFtoCNF_U $_907 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_906 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_906 $_908 \/
% 1.08/1.23     ~smoke skolemFOFtoCNF_U $_907 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_901 skolemFOFtoCNF_U \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_907 $_906 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_901 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_907 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_898 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_900
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_921 \/
% 1.08/1.23     ~accessible_world skolemFOFtoCNF_U $_926 \/
% 1.08/1.23     ~agent $_921 $_927 (skolemFOFtoCNF_X24 $_921) \/
% 1.08/1.23     ~agent $_926 $_928 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_920 $_918 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_925 $_918 \/ ~event $_921 $_927 \/
% 1.08/1.23     ~event $_926 $_928 \/ ~event skolemFOFtoCNF_U $_920 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_925 \/ ~forename skolemFOFtoCNF_U $_919 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_922 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_922 \/ ~man skolemFOFtoCNF_U $_918 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_919 $_918 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_922 skolemFOFtoCNF_X4 \/ ~present $_921 $_927 \/
% 1.08/1.23     ~present $_926 $_928 \/ ~present skolemFOFtoCNF_U $_920 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_925 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_921 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_926 \/ ~smoke $_921 $_927 \/
% 1.08/1.23     ~smoke $_926 $_928 \/ ~theme skolemFOFtoCNF_U $_920 $_921 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_925 $_926 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_920 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_925 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_919
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_942 \/
% 1.08/1.23     ~accessible_world skolemFOFtoCNF_U $_947 \/
% 1.08/1.23     ~agent $_942 $_948 (skolemFOFtoCNF_X24 $_942) \/
% 1.08/1.23     ~agent $_947 $_949 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_941 $_939 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_946 skolemFOFtoCNF_X4 \/ ~event $_942 $_948 \/
% 1.08/1.23     ~event $_947 $_949 \/ ~event skolemFOFtoCNF_U $_941 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_946 \/ ~forename skolemFOFtoCNF_U $_940 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_943 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_943 \/ ~man skolemFOFtoCNF_U $_939 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_940 $_939 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_943 skolemFOFtoCNF_X4 \/ ~present $_942 $_948 \/
% 1.08/1.23     ~present $_947 $_949 \/ ~present skolemFOFtoCNF_U $_941 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_946 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_942 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_947 \/ ~smoke $_942 $_948 \/
% 1.08/1.23     ~smoke $_947 $_949 \/ ~theme skolemFOFtoCNF_U $_941 $_942 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_946 $_947 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_941 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_946 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_940 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_943
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_963 \/
% 1.08/1.23     ~accessible_world skolemFOFtoCNF_U $_968 \/
% 1.08/1.23     ~agent $_963 $_969 (skolemFOFtoCNF_X24 $_963) \/
% 1.08/1.23     ~agent $_968 $_970 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_962 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_967 $_960 \/ ~event $_963 $_969 \/
% 1.08/1.23     ~event $_968 $_970 \/ ~event skolemFOFtoCNF_U $_962 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_967 \/ ~forename skolemFOFtoCNF_U $_961 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_964 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_964 \/ ~man skolemFOFtoCNF_U $_960 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_961 $_960 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_964 skolemFOFtoCNF_X4 \/ ~present $_963 $_969 \/
% 1.08/1.23     ~present $_968 $_970 \/ ~present skolemFOFtoCNF_U $_962 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_967 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_963 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_968 \/ ~smoke $_963 $_969 \/
% 1.08/1.23     ~smoke $_968 $_970 \/ ~theme skolemFOFtoCNF_U $_962 $_963 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_967 $_968 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_962 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_967 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_961 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_964
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_986 \/
% 1.08/1.23     ~accessible_world skolemFOFtoCNF_U $_991 \/
% 1.08/1.23     ~agent $_991 $_992 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_985 $_983 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_990 $_981 \/ ~event $_991 $_992 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_985 \/ ~event skolemFOFtoCNF_U $_990 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_982 \/ ~forename skolemFOFtoCNF_U $_984 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_987 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_987 \/ ~man skolemFOFtoCNF_U $_981 \/
% 1.08/1.23     ~man skolemFOFtoCNF_U $_983 \/ ~of skolemFOFtoCNF_U $_982 $_981 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_984 $_983 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_987 skolemFOFtoCNF_X4 \/ ~present $_991 $_992 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_985 \/ ~present skolemFOFtoCNF_U $_990 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_986 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_991 \/ ~smoke $_991 $_992 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_985 $_986 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_990 $_991 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_985 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_990 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_982 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_984 \/
% 1.08/1.23     man $_986 (skolemFOFtoCNF_X24 $_986)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_998 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_997 $_995 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_993 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_X2 $_1002 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_997 \/ ~event skolemFOFtoCNF_X2 $_1002 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_994 \/ ~forename skolemFOFtoCNF_U $_996 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_999 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_999 \/ ~man skolemFOFtoCNF_U $_993 \/
% 1.08/1.23     ~man skolemFOFtoCNF_U $_995 \/ ~of skolemFOFtoCNF_U $_994 $_993 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_996 $_995 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_999 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_997 \/ ~present skolemFOFtoCNF_X2 $_1002 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_998 \/
% 1.08/1.23     ~smoke skolemFOFtoCNF_X2 $_1002 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_997 $_998 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_997 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_994 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_996 \/
% 1.08/1.23     man $_998 (skolemFOFtoCNF_X24 $_998)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_998 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_997 $_995 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_993 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_X7 $_1002 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_997 \/ ~event skolemFOFtoCNF_X7 $_1002 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_994 \/ ~forename skolemFOFtoCNF_U $_996 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_999 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_999 \/ ~man skolemFOFtoCNF_U $_993 \/
% 1.08/1.23     ~man skolemFOFtoCNF_U $_995 \/ ~of skolemFOFtoCNF_U $_994 $_993 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_996 $_995 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_999 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_997 \/ ~present skolemFOFtoCNF_X7 $_1002 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_998 \/
% 1.08/1.23     ~smoke skolemFOFtoCNF_X7 $_1002 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_997 $_998 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_997 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_994 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_996 \/
% 1.08/1.23     man $_998 (skolemFOFtoCNF_X24 $_998)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_1001 \/
% 1.08/1.23     ~agent $_1001 $_1002 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_1000 $_993 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_995 \/
% 1.08/1.23     ~event $_1001 $_1002 \/ ~event skolemFOFtoCNF_U $_1000 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_994 \/ ~forename skolemFOFtoCNF_U $_996 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_999 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_999 \/ ~man skolemFOFtoCNF_U $_993 \/
% 1.08/1.23     ~man skolemFOFtoCNF_U $_995 \/ ~of skolemFOFtoCNF_U $_994 $_993 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_996 $_995 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_999 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~present $_1001 $_1002 \/ ~present skolemFOFtoCNF_U $_1000 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_1001 \/ ~smoke $_1001 $_1002 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_1000 $_1001 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_1000 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_994 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_996 \/
% 1.08/1.23     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_1001 \/
% 1.08/1.23     ~agent $_1001 $_1002 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_1000 $_993 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_995 \/
% 1.08/1.23     ~event $_1001 $_1002 \/ ~event skolemFOFtoCNF_U $_1000 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_994 \/ ~forename skolemFOFtoCNF_U $_996 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_999 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_999 \/ ~man skolemFOFtoCNF_U $_993 \/
% 1.08/1.23     ~man skolemFOFtoCNF_U $_995 \/ ~of skolemFOFtoCNF_U $_994 $_993 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_996 $_995 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_999 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~present $_1001 $_1002 \/ ~present skolemFOFtoCNF_U $_1000 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_1001 \/ ~smoke $_1001 $_1002 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_1000 $_1001 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_1000 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_994 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_996 \/
% 1.08/1.23     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 1.08/1.23  |- ~agent skolemFOFtoCNF_X2 $_1021 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~event skolemFOFtoCNF_X2 $_1021 \/ ~present skolemFOFtoCNF_X2 $_1021 \/
% 1.08/1.23     ~smoke skolemFOFtoCNF_X2 $_1021 \/
% 1.08/1.23     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 1.08/1.23  |- ~agent skolemFOFtoCNF_X7 $_1042 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~event skolemFOFtoCNF_X7 $_1042 \/ ~present skolemFOFtoCNF_X7 $_1042 \/
% 1.08/1.23     ~smoke skolemFOFtoCNF_X7 $_1042 \/
% 1.08/1.23     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 1.08/1.23  |- ~accessible_world skolemFOFtoCNF_U $_1067 \/
% 1.08/1.23     ~accessible_world skolemFOFtoCNF_U $_1072 \/
% 1.08/1.23     ~agent $_1067 $_1073 (skolemFOFtoCNF_X24 $_1067) \/
% 1.08/1.23     ~agent $_1072 $_1074 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_1066 $_1064 \/
% 1.08/1.23     ~agent skolemFOFtoCNF_U $_1071 $_1062 \/ ~event $_1067 $_1073 \/
% 1.08/1.23     ~event $_1072 $_1074 \/ ~event skolemFOFtoCNF_U $_1066 \/
% 1.08/1.23     ~event skolemFOFtoCNF_U $_1071 \/ ~forename skolemFOFtoCNF_U $_1063 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_1065 \/
% 1.08/1.23     ~forename skolemFOFtoCNF_U $_1068 \/
% 1.08/1.23     ~jules_forename skolemFOFtoCNF_U $_1068 \/
% 1.08/1.23     ~man skolemFOFtoCNF_U $_1062 \/ ~man skolemFOFtoCNF_U $_1064 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_1063 $_1062 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_1065 $_1064 \/
% 1.08/1.23     ~of skolemFOFtoCNF_U $_1068 skolemFOFtoCNF_X4 \/
% 1.08/1.23     ~present $_1067 $_1073 \/ ~present $_1072 $_1074 \/
% 1.08/1.23     ~present skolemFOFtoCNF_U $_1066 \/ ~present skolemFOFtoCNF_U $_1071 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_1067 \/
% 1.08/1.23     ~proposition skolemFOFtoCNF_U $_1072 \/ ~smoke $_1067 $_1073 \/
% 1.08/1.23     ~smoke $_1072 $_1074 \/ ~theme skolemFOFtoCNF_U $_1066 $_1067 \/
% 1.08/1.23     ~theme skolemFOFtoCNF_U $_1071 $_1072 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_1066 \/
% 1.08/1.23     ~think_believe_consider skolemFOFtoCNF_U $_1071 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_1063 \/
% 1.08/1.23     ~vincent_forename skolemFOFtoCNF_U $_1065
% 1.08/1.23  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.08/1.23  
%------------------------------------------------------------------------------