Metis---2.4.CSA-Sat.s

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

% Computer : n004.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:28 EDT 2022

% Result   : CounterSatisfiable 0.92s 1.11s
% Output   : Saturation 0.97s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11  % Problem  : NLP235+1 : TPTP v8.1.0. Released v2.4.0.
% 0.06/0.12  % Command  : metis --show proof --show saturation %s
% 0.11/0.32  % Computer : n004.cluster.edu
% 0.11/0.32  % Model    : x86_64 x86_64
% 0.11/0.32  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32  % Memory   : 8042.1875MB
% 0.11/0.32  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33  % CPULimit : 300
% 0.11/0.33  % WCLimit  : 600
% 0.11/0.33  % DateTime : Thu Jun 30 16:46:08 EDT 2022
% 0.11/0.33  % CPUTime  : 
% 0.11/0.33  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.92/1.11  % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.92/1.11  
% 0.92/1.11  SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.92/1.11  |- actual_world skolemFOFtoCNF_U
% 0.92/1.11  |- accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_X2
% 0.92/1.11  |- accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_X7
% 0.92/1.11  |- agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_Y
% 0.92/1.11  |- agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_V
% 0.92/1.11  |- be skolemFOFtoCNF_U skolemFOFtoCNF_X5 skolemFOFtoCNF_X4
% 0.92/1.11       skolemFOFtoCNF_X4
% 0.92/1.11  |- event skolemFOFtoCNF_U skolemFOFtoCNF_X1
% 0.92/1.11  |- event skolemFOFtoCNF_U skolemFOFtoCNF_X6
% 0.92/1.11  |- forename skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.92/1.11  |- forename skolemFOFtoCNF_U skolemFOFtoCNF_X
% 0.92/1.11  |- forename skolemFOFtoCNF_U skolemFOFtoCNF_X3
% 0.92/1.11  |- forename skolemFOFtoCNF_U skolemFOFtoCNF_Z
% 0.92/1.11  |- jules_forename skolemFOFtoCNF_U skolemFOFtoCNF_X
% 0.92/1.11  |- jules_forename skolemFOFtoCNF_U skolemFOFtoCNF_X3
% 0.92/1.11  |- man skolemFOFtoCNF_U skolemFOFtoCNF_V
% 0.92/1.11  |- man skolemFOFtoCNF_U skolemFOFtoCNF_X4
% 0.92/1.11  |- man skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.92/1.11  |- of skolemFOFtoCNF_U skolemFOFtoCNF_W skolemFOFtoCNF_V
% 0.92/1.11  |- of skolemFOFtoCNF_U skolemFOFtoCNF_X skolemFOFtoCNF_Y
% 0.92/1.11  |- of skolemFOFtoCNF_U skolemFOFtoCNF_X3 skolemFOFtoCNF_X4
% 0.92/1.11  |- of skolemFOFtoCNF_U skolemFOFtoCNF_Z skolemFOFtoCNF_Y
% 0.92/1.11  |- present skolemFOFtoCNF_U skolemFOFtoCNF_X1
% 0.92/1.11  |- present skolemFOFtoCNF_U skolemFOFtoCNF_X6
% 0.92/1.11  |- proposition skolemFOFtoCNF_U skolemFOFtoCNF_X2
% 0.92/1.11  |- proposition skolemFOFtoCNF_U skolemFOFtoCNF_X7
% 0.92/1.11  |- state skolemFOFtoCNF_U skolemFOFtoCNF_X5
% 0.92/1.11  |- theme skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X2
% 0.92/1.11  |- theme skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X7
% 0.92/1.11  |- think_believe_consider skolemFOFtoCNF_U skolemFOFtoCNF_X1
% 0.92/1.11  |- think_believe_consider skolemFOFtoCNF_U skolemFOFtoCNF_X6
% 0.92/1.11  |- vincent_forename skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.92/1.11  |- vincent_forename skolemFOFtoCNF_U skolemFOFtoCNF_Z
% 0.92/1.11  |- agent skolemFOFtoCNF_X7 skolemFOFtoCNF_X10 skolemFOFtoCNF_Y
% 0.92/1.11  |- event skolemFOFtoCNF_X7 skolemFOFtoCNF_X10
% 0.92/1.11  |- present skolemFOFtoCNF_X7 skolemFOFtoCNF_X10
% 0.92/1.11  |- smoke skolemFOFtoCNF_X7 skolemFOFtoCNF_X10
% 0.92/1.11  |- ~man skolemFOFtoCNF_X2 $X8 \/
% 0.92/1.11     agent skolemFOFtoCNF_X2 (skolemFOFtoCNF_X9 $X8) $X8
% 0.92/1.11  |- ~man skolemFOFtoCNF_X2 $X8 \/
% 0.92/1.11     event skolemFOFtoCNF_X2 (skolemFOFtoCNF_X9 $X8)
% 0.92/1.11  |- ~man skolemFOFtoCNF_X2 $X8 \/
% 0.92/1.11     present skolemFOFtoCNF_X2 (skolemFOFtoCNF_X9 $X8)
% 0.92/1.11  |- ~man skolemFOFtoCNF_X2 $X8 \/
% 0.92/1.11     smoke skolemFOFtoCNF_X2 (skolemFOFtoCNF_X9 $X8)
% 0.92/1.11  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 0.92/1.11     ~actual_world $X11 \/ ~agent $X11 $X17 $X15 \/ ~agent $X11 $X22 $X12 \/
% 0.92/1.11     ~agent $X23 $X26 $X20 \/ ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/
% 0.92/1.11     ~event $X11 $X22 \/ ~event $X23 $X26 \/ ~forename $X11 $X13 \/
% 0.92/1.11     ~forename $X11 $X16 \/ ~forename $X11 $X19 \/
% 0.92/1.11     ~jules_forename $X11 $X19 \/ ~man $X11 $X12 \/ ~man $X11 $X15 \/
% 0.92/1.11     ~man $X11 $X20 \/ ~of $X11 $X13 $X12 \/ ~of $X11 $X16 $X15 \/
% 0.92/1.11     ~of $X11 $X19 $X20 \/ ~present $X11 $X17 \/ ~present $X11 $X22 \/
% 0.92/1.11     ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 0.92/1.11     ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/ ~state $X11 $X21 \/
% 0.92/1.11     ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 0.92/1.11     ~think_believe_consider $X11 $X17 \/
% 0.92/1.11     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X13 \/
% 0.92/1.11     ~vincent_forename $X11 $X16 \/ man $X18 (skolemFOFtoCNF_X24 $X18)
% 0.92/1.11  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.92/1.11     ~actual_world $X23 \/ ~agent $X23 $X22 $X12 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.11     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X22 \/ ~event $X23 $X26 \/
% 0.92/1.11     ~forename $X23 $X13 \/ ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 0.92/1.11     ~jules_forename $X23 $X19 \/ ~man $X23 $X12 \/ ~man $X23 $X20 \/
% 0.92/1.11     ~of $X23 $X13 $X12 \/ ~of $X23 $X16 $X20 \/ ~of $X23 $X19 $X20 \/
% 0.92/1.11     ~present $X23 $X22 \/ ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 0.92/1.11     ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/ ~state $X23 $X21 \/
% 0.92/1.11     ~theme $X23 $X22 $X23 \/ ~theme $X23 $X26 $X18 \/
% 0.92/1.11     ~think_believe_consider $X23 $X22 \/
% 0.92/1.11     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X13 \/
% 0.92/1.11     ~vincent_forename $X23 $X16 \/ man $X18 (skolemFOFtoCNF_X24 $X18)
% 0.92/1.11  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.92/1.11     ~actual_world $X23 \/ ~agent $X23 $X17 $X15 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.11     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X17 \/ ~event $X23 $X26 \/
% 0.92/1.11     ~forename $X23 $X13 \/ ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 0.92/1.11     ~jules_forename $X23 $X19 \/ ~man $X23 $X15 \/ ~man $X23 $X20 \/
% 0.92/1.11     ~of $X23 $X13 $X20 \/ ~of $X23 $X16 $X15 \/ ~of $X23 $X19 $X20 \/
% 0.92/1.11     ~present $X23 $X17 \/ ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 0.92/1.11     ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/ ~state $X23 $X21 \/
% 0.92/1.11     ~theme $X23 $X17 $X18 \/ ~theme $X23 $X26 $X23 \/
% 0.92/1.11     ~think_believe_consider $X23 $X17 \/
% 0.92/1.11     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X13 \/
% 0.92/1.11     ~vincent_forename $X23 $X16 \/ man $X18 (skolemFOFtoCNF_X24 $X18)
% 0.92/1.11  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 0.92/1.11     ~actual_world $X11 \/ ~agent $X11 $X17 $X15 \/ ~agent $X11 $X22 $X15 \/
% 0.92/1.11     ~agent $X23 $X26 $X20 \/ ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/
% 0.92/1.11     ~event $X11 $X22 \/ ~event $X23 $X26 \/ ~forename $X11 $X16 \/
% 0.92/1.11     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/
% 0.92/1.11     ~man $X11 $X20 \/ ~of $X11 $X16 $X15 \/ ~of $X11 $X19 $X20 \/
% 0.92/1.11     ~present $X11 $X17 \/ ~present $X11 $X22 \/ ~present $X23 $X26 \/
% 0.92/1.11     ~proposition $X11 $X18 \/ ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/
% 0.92/1.11     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 0.92/1.11     ~think_believe_consider $X11 $X17 \/
% 0.92/1.11     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16 \/
% 0.92/1.11     man $X18 (skolemFOFtoCNF_X24 $X18)
% 0.92/1.11  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 0.92/1.11     ~actual_world $X11 \/ ~agent $X11 $X22 $X15 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.11     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X22 \/ ~event $X23 $X26 \/
% 0.92/1.11     ~forename $X11 $X16 \/ ~forename $X11 $X19 \/
% 0.92/1.11     ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/ ~man $X11 $X20 \/
% 0.92/1.11     ~of $X11 $X16 $X15 \/ ~of $X11 $X19 $X20 \/ ~present $X11 $X22 \/
% 0.92/1.11     ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 0.92/1.11     ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/ ~state $X11 $X21 \/
% 0.92/1.11     ~theme $X11 $X22 $X18 \/ ~theme $X11 $X22 $X23 \/
% 0.92/1.11     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16 \/
% 0.92/1.11     man $X18 (skolemFOFtoCNF_X24 $X18)
% 0.92/1.11  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.92/1.11     ~actual_world $X23 \/ ~agent $X23 $X22 $X20 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.11     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X22 \/ ~event $X23 $X26 \/
% 0.92/1.11     ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 0.92/1.11     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/ ~of $X23 $X16 $X20 \/
% 0.92/1.11     ~of $X23 $X19 $X20 \/ ~present $X23 $X22 \/ ~present $X23 $X26 \/
% 0.92/1.11     ~proposition $X23 $X18 \/ ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/
% 0.92/1.11     ~state $X23 $X21 \/ ~theme $X23 $X22 $X23 \/ ~theme $X23 $X26 $X18 \/
% 0.92/1.11     ~think_believe_consider $X23 $X22 \/
% 0.92/1.11     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16 \/
% 0.92/1.11     man $X18 (skolemFOFtoCNF_X24 $X18)
% 0.92/1.11  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.92/1.11     ~actual_world $X23 \/ ~agent $X23 $X17 $X20 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.11     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X17 \/ ~event $X23 $X26 \/
% 0.92/1.11     ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 0.92/1.11     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/ ~of $X23 $X16 $X20 \/
% 0.92/1.11     ~of $X23 $X19 $X20 \/ ~present $X23 $X17 \/ ~present $X23 $X26 \/
% 0.92/1.11     ~proposition $X23 $X18 \/ ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/
% 0.92/1.11     ~state $X23 $X21 \/ ~theme $X23 $X17 $X18 \/ ~theme $X23 $X26 $X23 \/
% 0.92/1.11     ~think_believe_consider $X23 $X17 \/
% 0.92/1.11     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16 \/
% 0.92/1.11     man $X18 (skolemFOFtoCNF_X24 $X18)
% 0.92/1.11  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.92/1.11     ~actual_world $X23 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.11     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X26 \/ ~forename $X23 $X16 \/
% 0.92/1.11     ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/
% 0.92/1.11     ~of $X23 $X16 $X20 \/ ~of $X23 $X19 $X20 \/ ~present $X23 $X26 \/
% 0.92/1.11     ~proposition $X23 $X18 \/ ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/
% 0.92/1.11     ~state $X23 $X21 \/ ~theme $X23 $X26 $X18 \/ ~theme $X23 $X26 $X23 \/
% 0.92/1.11     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16 \/
% 0.92/1.11     man $X18 (skolemFOFtoCNF_X24 $X18)
% 0.92/1.12  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 0.92/1.12     ~actual_world $X11 \/ ~agent $X11 $X17 $X15 \/ ~agent $X11 $X22 $X20 \/
% 0.92/1.12     ~agent $X23 $X26 $X20 \/ ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/
% 0.92/1.12     ~event $X11 $X22 \/ ~event $X23 $X26 \/ ~forename $X11 $X16 \/
% 0.92/1.12     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/
% 0.92/1.12     ~man $X11 $X20 \/ ~of $X11 $X16 $X15 \/ ~of $X11 $X19 $X20 \/
% 0.92/1.12     ~present $X11 $X17 \/ ~present $X11 $X22 \/ ~present $X23 $X26 \/
% 0.92/1.12     ~proposition $X11 $X18 \/ ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 0.92/1.12     ~think_believe_consider $X11 $X17 \/
% 0.92/1.12     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16 \/
% 0.92/1.12     ~vincent_forename $X11 $X19 \/ man $X18 (skolemFOFtoCNF_X24 $X18)
% 0.92/1.12  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.92/1.12     ~actual_world $X23 \/ ~agent $X23 $X17 $X15 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X17 \/ ~event $X23 $X26 \/
% 0.92/1.12     ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 0.92/1.12     ~jules_forename $X23 $X19 \/ ~man $X23 $X15 \/ ~man $X23 $X20 \/
% 0.92/1.12     ~of $X23 $X16 $X15 \/ ~of $X23 $X19 $X20 \/ ~present $X23 $X17 \/
% 0.92/1.12     ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 0.92/1.12     ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/ ~state $X23 $X21 \/
% 0.92/1.12     ~theme $X23 $X17 $X18 \/ ~theme $X23 $X26 $X23 \/
% 0.92/1.12     ~think_believe_consider $X23 $X17 \/
% 0.92/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16 \/
% 0.92/1.12     ~vincent_forename $X23 $X19 \/ man $X18 (skolemFOFtoCNF_X24 $X18)
% 0.92/1.12  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 0.92/1.12     ~actual_world $X11 \/ ~agent $X11 $X17 $X20 \/ ~agent $X11 $X22 $X12 \/
% 0.92/1.12     ~agent $X23 $X26 $X20 \/ ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/
% 0.92/1.12     ~event $X11 $X22 \/ ~event $X23 $X26 \/ ~forename $X11 $X13 \/
% 0.92/1.12     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X12 \/
% 0.92/1.12     ~man $X11 $X20 \/ ~of $X11 $X13 $X12 \/ ~of $X11 $X19 $X20 \/
% 0.92/1.12     ~present $X11 $X17 \/ ~present $X11 $X22 \/ ~present $X23 $X26 \/
% 0.92/1.12     ~proposition $X11 $X18 \/ ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 0.92/1.12     ~think_believe_consider $X11 $X17 \/
% 0.92/1.12     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X13 \/
% 0.92/1.12     ~vincent_forename $X11 $X19 \/ man $X18 (skolemFOFtoCNF_X24 $X18)
% 0.92/1.12  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.92/1.12     ~actual_world $X23 \/ ~agent $X23 $X22 $X12 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X22 \/ ~event $X23 $X26 \/
% 0.92/1.12     ~forename $X23 $X13 \/ ~forename $X23 $X19 \/
% 0.92/1.12     ~jules_forename $X23 $X19 \/ ~man $X23 $X12 \/ ~man $X23 $X20 \/
% 0.92/1.12     ~of $X23 $X13 $X12 \/ ~of $X23 $X19 $X20 \/ ~present $X23 $X22 \/
% 0.92/1.12     ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 0.92/1.12     ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/ ~state $X23 $X21 \/
% 0.92/1.12     ~theme $X23 $X22 $X23 \/ ~theme $X23 $X26 $X18 \/
% 0.92/1.12     ~think_believe_consider $X23 $X22 \/
% 0.92/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X13 \/
% 0.92/1.12     ~vincent_forename $X23 $X19 \/ man $X18 (skolemFOFtoCNF_X24 $X18)
% 0.92/1.12  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 0.92/1.12     ~actual_world $X11 \/ ~agent $X11 $X17 $X20 \/ ~agent $X11 $X22 $X20 \/
% 0.92/1.12     ~agent $X23 $X26 $X20 \/ ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/
% 0.92/1.12     ~event $X11 $X22 \/ ~event $X23 $X26 \/ ~forename $X11 $X19 \/
% 0.92/1.12     ~jules_forename $X11 $X19 \/ ~man $X11 $X20 \/ ~of $X11 $X19 $X20 \/
% 0.92/1.12     ~present $X11 $X17 \/ ~present $X11 $X22 \/ ~present $X23 $X26 \/
% 0.92/1.12     ~proposition $X11 $X18 \/ ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 0.92/1.12     ~think_believe_consider $X11 $X17 \/
% 0.92/1.12     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X19 \/
% 0.92/1.12     man $X18 (skolemFOFtoCNF_X24 $X18)
% 0.92/1.12  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 0.92/1.12     ~actual_world $X11 \/ ~agent $X11 $X22 $X20 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X22 \/ ~event $X23 $X26 \/
% 0.92/1.12     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X20 \/
% 0.92/1.12     ~of $X11 $X19 $X20 \/ ~present $X11 $X22 \/ ~present $X23 $X26 \/
% 0.92/1.12     ~proposition $X11 $X18 \/ ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X11 $X21 \/ ~theme $X11 $X22 $X18 \/ ~theme $X11 $X22 $X23 \/
% 0.92/1.12     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X19 \/
% 0.92/1.12     man $X18 (skolemFOFtoCNF_X24 $X18)
% 0.92/1.12  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.92/1.12     ~actual_world $X23 \/ ~agent $X23 $X22 $X20 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X22 \/ ~event $X23 $X26 \/
% 0.92/1.12     ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/
% 0.92/1.12     ~of $X23 $X19 $X20 \/ ~present $X23 $X22 \/ ~present $X23 $X26 \/
% 0.92/1.12     ~proposition $X23 $X18 \/ ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X23 $X21 \/ ~theme $X23 $X22 $X23 \/ ~theme $X23 $X26 $X18 \/
% 0.92/1.12     ~think_believe_consider $X23 $X22 \/
% 0.92/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X19 \/
% 0.92/1.12     man $X18 (skolemFOFtoCNF_X24 $X18)
% 0.92/1.12  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.92/1.12     ~actual_world $X23 \/ ~agent $X23 $X17 $X20 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X17 \/ ~event $X23 $X26 \/
% 0.92/1.12     ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/
% 0.92/1.12     ~of $X23 $X19 $X20 \/ ~present $X23 $X17 \/ ~present $X23 $X26 \/
% 0.92/1.12     ~proposition $X23 $X18 \/ ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X23 $X21 \/ ~theme $X23 $X17 $X18 \/ ~theme $X23 $X26 $X23 \/
% 0.92/1.12     ~think_believe_consider $X23 $X17 \/
% 0.92/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X19 \/
% 0.92/1.12     man $X18 (skolemFOFtoCNF_X24 $X18)
% 0.92/1.12  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.92/1.12     ~actual_world $X23 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X26 \/ ~forename $X23 $X19 \/
% 0.92/1.12     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/ ~of $X23 $X19 $X20 \/
% 0.92/1.12     ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 0.92/1.12     ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/ ~state $X23 $X21 \/
% 0.92/1.12     ~theme $X23 $X26 $X18 \/ ~theme $X23 $X26 $X23 \/
% 0.92/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X19 \/
% 0.92/1.12     man $X18 (skolemFOFtoCNF_X24 $X18)
% 0.92/1.12  |- ~accessible_world $X11 $X23 \/ ~actual_world $X11 \/
% 0.92/1.12     ~agent $X11 $X22 $X15 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X22 \/ ~event $X23 $X26 \/
% 0.92/1.12     ~forename $X11 $X16 \/ ~forename $X11 $X19 \/
% 0.92/1.12     ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/ ~man $X11 $X20 \/
% 0.92/1.12     ~of $X11 $X16 $X15 \/ ~of $X11 $X19 $X20 \/ ~present $X11 $X22 \/
% 0.92/1.12     ~present $X23 $X26 \/ ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X11 $X21 \/ ~theme $X11 $X22 $X23 \/
% 0.92/1.12     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16 \/
% 0.92/1.12     man $X23 (skolemFOFtoCNF_X24 $X23)
% 0.92/1.12  |- ~accessible_world $X23 $X23 \/ ~actual_world $X23 \/
% 0.92/1.12     ~agent $X23 $X26 $X20 \/ ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X26 \/
% 0.92/1.12     ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 0.92/1.12     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/ ~of $X23 $X16 $X20 \/
% 0.92/1.12     ~of $X23 $X19 $X20 \/ ~present $X23 $X26 \/ ~proposition $X23 $X23 \/
% 0.92/1.12     ~smoke $X23 $X26 \/ ~state $X23 $X21 \/ ~theme $X23 $X26 $X23 \/
% 0.92/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16 \/
% 0.92/1.12     man $X23 (skolemFOFtoCNF_X24 $X23)
% 0.92/1.12  |- ~accessible_world $X11 $X23 \/ ~actual_world $X11 \/
% 0.92/1.12     ~agent $X11 $X22 $X20 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X22 \/ ~event $X23 $X26 \/
% 0.92/1.12     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X20 \/
% 0.92/1.12     ~of $X11 $X19 $X20 \/ ~present $X11 $X22 \/ ~present $X23 $X26 \/
% 0.92/1.12     ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/ ~state $X11 $X21 \/
% 0.92/1.12     ~theme $X11 $X22 $X23 \/ ~think_believe_consider $X11 $X22 \/
% 0.92/1.12     ~vincent_forename $X11 $X19 \/ man $X23 (skolemFOFtoCNF_X24 $X23)
% 0.92/1.12  |- ~accessible_world $X23 $X23 \/ ~actual_world $X23 \/
% 0.92/1.12     ~agent $X23 $X26 $X20 \/ ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X26 \/
% 0.92/1.12     ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/
% 0.92/1.12     ~of $X23 $X19 $X20 \/ ~present $X23 $X26 \/ ~proposition $X23 $X23 \/
% 0.92/1.12     ~smoke $X23 $X26 \/ ~state $X23 $X21 \/ ~theme $X23 $X26 $X23 \/
% 0.92/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X19 \/
% 0.92/1.12     man $X23 (skolemFOFtoCNF_X24 $X23)
% 0.92/1.12  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 0.92/1.12     ~actual_world $X11 \/ ~agent $X11 $X17 $X15 \/ ~agent $X11 $X22 $X12 \/
% 0.92/1.12     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/ ~event $X11 $X22 \/
% 0.92/1.12     ~event $X18 $X25 \/ ~event $X23 $X26 \/ ~forename $X11 $X13 \/
% 0.92/1.12     ~forename $X11 $X16 \/ ~forename $X11 $X19 \/
% 0.92/1.12     ~jules_forename $X11 $X19 \/ ~man $X11 $X12 \/ ~man $X11 $X15 \/
% 0.92/1.12     ~man $X11 $X20 \/ ~of $X11 $X13 $X12 \/ ~of $X11 $X16 $X15 \/
% 0.92/1.12     ~of $X11 $X19 $X20 \/ ~present $X11 $X17 \/ ~present $X11 $X22 \/
% 0.92/1.12     ~present $X18 $X25 \/ ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 0.92/1.12     ~proposition $X11 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 0.92/1.12     ~think_believe_consider $X11 $X17 \/
% 0.92/1.12     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X13 \/
% 0.92/1.12     ~vincent_forename $X11 $X16
% 0.92/1.12  |- ~accessible_world $X18 $X18 \/ ~accessible_world $X18 $X23 \/
% 0.92/1.12     ~actual_world $X18 \/ ~agent $X18 $X22 $X12 \/
% 0.92/1.12     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X18 $X21 $X20 $X20 \/ ~event $X18 $X22 \/ ~event $X18 $X25 \/
% 0.92/1.12     ~event $X23 $X26 \/ ~forename $X18 $X13 \/ ~forename $X18 $X16 \/
% 0.92/1.12     ~forename $X18 $X19 \/ ~jules_forename $X18 $X19 \/ ~man $X18 $X12 \/
% 0.92/1.12     ~man $X18 $X20 \/ ~man $X18 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~of $X18 $X13 $X12 \/ ~of $X18 $X16 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~of $X18 $X19 $X20 \/ ~present $X18 $X22 \/ ~present $X18 $X25 \/
% 0.92/1.12     ~present $X23 $X26 \/ ~proposition $X18 $X18 \/
% 0.92/1.12     ~proposition $X18 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X18 $X21 \/ ~theme $X18 $X22 $X23 \/ ~theme $X18 $X25 $X18 \/
% 0.92/1.12     ~think_believe_consider $X18 $X22 \/
% 0.92/1.12     ~think_believe_consider $X18 $X25 \/ ~vincent_forename $X18 $X13 \/
% 0.92/1.12     ~vincent_forename $X18 $X16
% 0.92/1.12  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.92/1.12     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~agent $X23 $X22 $X12 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/ ~event $X23 $X22 \/
% 0.92/1.12     ~event $X23 $X26 \/ ~forename $X23 $X13 \/ ~forename $X23 $X16 \/
% 0.92/1.12     ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/ ~man $X23 $X12 \/
% 0.92/1.12     ~man $X23 $X20 \/ ~of $X23 $X13 $X12 \/ ~of $X23 $X16 $X20 \/
% 0.92/1.12     ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/ ~present $X23 $X22 \/
% 0.92/1.12     ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 0.92/1.12     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X23 $X21 \/ ~theme $X23 $X22 $X23 \/ ~theme $X23 $X26 $X18 \/
% 0.92/1.12     ~think_believe_consider $X23 $X22 \/
% 0.92/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X13 \/
% 0.92/1.12     ~vincent_forename $X23 $X16
% 0.92/1.12  |- ~accessible_world $X18 $X18 \/ ~accessible_world $X18 $X23 \/
% 0.92/1.12     ~actual_world $X18 \/ ~agent $X18 $X17 $X15 \/
% 0.92/1.12     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X18 $X21 $X20 $X20 \/ ~event $X18 $X17 \/ ~event $X18 $X25 \/
% 0.92/1.12     ~event $X23 $X26 \/ ~forename $X18 $X13 \/ ~forename $X18 $X16 \/
% 0.92/1.12     ~forename $X18 $X19 \/ ~jules_forename $X18 $X19 \/ ~man $X18 $X15 \/
% 0.92/1.12     ~man $X18 $X20 \/ ~man $X18 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~of $X18 $X13 (skolemFOFtoCNF_X24 $X18) \/ ~of $X18 $X16 $X15 \/
% 0.92/1.12     ~of $X18 $X19 $X20 \/ ~present $X18 $X17 \/ ~present $X18 $X25 \/
% 0.92/1.12     ~present $X23 $X26 \/ ~proposition $X18 $X18 \/
% 0.92/1.12     ~proposition $X18 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X18 $X21 \/ ~theme $X18 $X17 $X18 \/ ~theme $X18 $X25 $X23 \/
% 0.92/1.12     ~think_believe_consider $X18 $X17 \/
% 0.92/1.12     ~think_believe_consider $X18 $X25 \/ ~vincent_forename $X18 $X13 \/
% 0.92/1.12     ~vincent_forename $X18 $X16
% 0.92/1.12  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.92/1.12     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~agent $X23 $X17 $X15 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/ ~event $X23 $X17 \/
% 0.92/1.12     ~event $X23 $X26 \/ ~forename $X23 $X13 \/ ~forename $X23 $X16 \/
% 0.92/1.12     ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/ ~man $X23 $X15 \/
% 0.92/1.12     ~man $X23 $X20 \/ ~of $X23 $X13 $X20 \/ ~of $X23 $X16 $X15 \/
% 0.92/1.12     ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/ ~present $X23 $X17 \/
% 0.92/1.12     ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 0.92/1.12     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X23 $X21 \/ ~theme $X23 $X17 $X18 \/ ~theme $X23 $X26 $X23 \/
% 0.92/1.12     ~think_believe_consider $X23 $X17 \/
% 0.92/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X13 \/
% 0.92/1.12     ~vincent_forename $X23 $X16
% 0.92/1.12  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 0.92/1.12     ~actual_world $X11 \/ ~agent $X11 $X17 $X15 \/ ~agent $X11 $X22 $X15 \/
% 0.92/1.12     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/ ~event $X11 $X22 \/
% 0.92/1.12     ~event $X18 $X25 \/ ~event $X23 $X26 \/ ~forename $X11 $X16 \/
% 0.92/1.12     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/
% 0.92/1.12     ~man $X11 $X20 \/ ~of $X11 $X16 $X15 \/ ~of $X11 $X19 $X20 \/
% 0.92/1.12     ~present $X11 $X17 \/ ~present $X11 $X22 \/ ~present $X18 $X25 \/
% 0.92/1.12     ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 0.92/1.12     ~proposition $X11 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 0.92/1.12     ~think_believe_consider $X11 $X17 \/
% 0.92/1.12     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16
% 0.92/1.12  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 0.92/1.12     ~actual_world $X11 \/ ~agent $X11 $X22 $X15 \/
% 0.92/1.12     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X22 \/ ~event $X18 $X25 \/
% 0.92/1.12     ~event $X23 $X26 \/ ~forename $X11 $X16 \/ ~forename $X11 $X19 \/
% 0.92/1.12     ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/ ~man $X11 $X20 \/
% 0.92/1.12     ~of $X11 $X16 $X15 \/ ~of $X11 $X19 $X20 \/ ~present $X11 $X22 \/
% 0.92/1.12     ~present $X18 $X25 \/ ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 0.92/1.12     ~proposition $X11 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X11 $X21 \/ ~theme $X11 $X22 $X18 \/ ~theme $X11 $X22 $X23 \/
% 0.92/1.12     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16
% 0.92/1.12  |- ~accessible_world $X18 $X18 \/ ~accessible_world $X18 $X23 \/
% 0.92/1.12     ~actual_world $X18 \/ ~agent $X18 $X22 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X18 $X21 $X20 $X20 \/ ~event $X18 $X22 \/ ~event $X18 $X25 \/
% 0.92/1.12     ~event $X23 $X26 \/ ~forename $X18 $X16 \/ ~forename $X18 $X19 \/
% 0.92/1.12     ~jules_forename $X18 $X19 \/ ~man $X18 $X20 \/
% 0.92/1.12     ~man $X18 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~of $X18 $X16 (skolemFOFtoCNF_X24 $X18) \/ ~of $X18 $X19 $X20 \/
% 0.92/1.12     ~present $X18 $X22 \/ ~present $X18 $X25 \/ ~present $X23 $X26 \/
% 0.92/1.12     ~proposition $X18 $X18 \/ ~proposition $X18 $X23 \/ ~smoke $X18 $X25 \/
% 0.92/1.12     ~smoke $X23 $X26 \/ ~state $X18 $X21 \/ ~theme $X18 $X22 $X23 \/
% 0.92/1.12     ~theme $X18 $X25 $X18 \/ ~think_believe_consider $X18 $X22 \/
% 0.92/1.12     ~think_believe_consider $X18 $X25 \/ ~vincent_forename $X18 $X16
% 0.92/1.12  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.92/1.12     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~agent $X23 $X22 $X20 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/ ~event $X23 $X22 \/
% 0.92/1.12     ~event $X23 $X26 \/ ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 0.92/1.12     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/ ~of $X23 $X16 $X20 \/
% 0.92/1.12     ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/ ~present $X23 $X22 \/
% 0.92/1.12     ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 0.92/1.12     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X23 $X21 \/ ~theme $X23 $X22 $X23 \/ ~theme $X23 $X26 $X18 \/
% 0.92/1.12     ~think_believe_consider $X23 $X22 \/
% 0.92/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16
% 0.92/1.12  |- ~accessible_world $X18 $X18 \/ ~accessible_world $X18 $X23 \/
% 0.92/1.12     ~actual_world $X18 \/ ~agent $X18 $X17 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X18 $X21 $X20 $X20 \/ ~event $X18 $X17 \/ ~event $X18 $X25 \/
% 0.92/1.12     ~event $X23 $X26 \/ ~forename $X18 $X16 \/ ~forename $X18 $X19 \/
% 0.92/1.12     ~jules_forename $X18 $X19 \/ ~man $X18 $X20 \/
% 0.92/1.12     ~man $X18 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~of $X18 $X16 (skolemFOFtoCNF_X24 $X18) \/ ~of $X18 $X19 $X20 \/
% 0.92/1.12     ~present $X18 $X17 \/ ~present $X18 $X25 \/ ~present $X23 $X26 \/
% 0.92/1.12     ~proposition $X18 $X18 \/ ~proposition $X18 $X23 \/ ~smoke $X18 $X25 \/
% 0.92/1.12     ~smoke $X23 $X26 \/ ~state $X18 $X21 \/ ~theme $X18 $X17 $X18 \/
% 0.92/1.12     ~theme $X18 $X25 $X23 \/ ~think_believe_consider $X18 $X17 \/
% 0.92/1.12     ~think_believe_consider $X18 $X25 \/ ~vincent_forename $X18 $X16
% 0.92/1.12  |- ~accessible_world $X18 $X18 \/ ~accessible_world $X18 $X23 \/
% 0.92/1.12     ~actual_world $X18 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~agent $X23 $X26 $X20 \/ ~be $X18 $X21 $X20 $X20 \/ ~event $X18 $X25 \/
% 0.92/1.12     ~event $X23 $X26 \/ ~forename $X18 $X16 \/ ~forename $X18 $X19 \/
% 0.92/1.12     ~jules_forename $X18 $X19 \/ ~man $X18 $X20 \/
% 0.92/1.12     ~man $X18 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~of $X18 $X16 (skolemFOFtoCNF_X24 $X18) \/ ~of $X18 $X19 $X20 \/
% 0.92/1.12     ~present $X18 $X25 \/ ~present $X23 $X26 \/ ~proposition $X18 $X18 \/
% 0.92/1.12     ~proposition $X18 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X18 $X21 \/ ~theme $X18 $X25 $X18 \/ ~theme $X18 $X25 $X23 \/
% 0.92/1.12     ~think_believe_consider $X18 $X25 \/ ~vincent_forename $X18 $X16
% 0.92/1.12  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.92/1.12     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~agent $X23 $X17 $X20 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/ ~event $X23 $X17 \/
% 0.92/1.12     ~event $X23 $X26 \/ ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 0.92/1.12     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/ ~of $X23 $X16 $X20 \/
% 0.92/1.12     ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/ ~present $X23 $X17 \/
% 0.92/1.12     ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 0.92/1.12     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X23 $X21 \/ ~theme $X23 $X17 $X18 \/ ~theme $X23 $X26 $X23 \/
% 0.92/1.12     ~think_believe_consider $X23 $X17 \/
% 0.92/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16
% 0.92/1.12  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.92/1.12     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~agent $X23 $X26 $X20 \/ ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/
% 0.92/1.12     ~event $X23 $X26 \/ ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 0.92/1.12     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/ ~of $X23 $X16 $X20 \/
% 0.92/1.12     ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/ ~present $X23 $X26 \/
% 0.92/1.12     ~proposition $X23 $X18 \/ ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/
% 0.92/1.12     ~smoke $X23 $X26 \/ ~state $X23 $X21 \/ ~theme $X23 $X26 $X18 \/
% 0.92/1.12     ~theme $X23 $X26 $X23 \/ ~think_believe_consider $X23 $X26 \/
% 0.92/1.12     ~vincent_forename $X23 $X16
% 0.92/1.12  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 0.92/1.12     ~actual_world $X11 \/ ~agent $X11 $X17 $X15 \/ ~agent $X11 $X22 $X20 \/
% 0.92/1.12     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/ ~event $X11 $X22 \/
% 0.92/1.12     ~event $X18 $X25 \/ ~event $X23 $X26 \/ ~forename $X11 $X16 \/
% 0.92/1.12     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/
% 0.92/1.12     ~man $X11 $X20 \/ ~of $X11 $X16 $X15 \/ ~of $X11 $X19 $X20 \/
% 0.92/1.12     ~present $X11 $X17 \/ ~present $X11 $X22 \/ ~present $X18 $X25 \/
% 0.92/1.12     ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 0.92/1.12     ~proposition $X11 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 0.92/1.12     ~think_believe_consider $X11 $X17 \/
% 0.92/1.12     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16 \/
% 0.92/1.12     ~vincent_forename $X11 $X19
% 0.92/1.12  |- ~accessible_world $X18 $X18 \/ ~accessible_world $X18 $X23 \/
% 0.92/1.12     ~actual_world $X18 \/ ~agent $X18 $X22 $X20 \/
% 0.92/1.12     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X18 $X21 $X20 $X20 \/ ~event $X18 $X22 \/ ~event $X18 $X25 \/
% 0.92/1.12     ~event $X23 $X26 \/ ~forename $X18 $X16 \/ ~forename $X18 $X19 \/
% 0.92/1.12     ~jules_forename $X18 $X19 \/ ~man $X18 $X20 \/
% 0.92/1.12     ~man $X18 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~of $X18 $X16 (skolemFOFtoCNF_X24 $X18) \/ ~of $X18 $X19 $X20 \/
% 0.92/1.12     ~present $X18 $X22 \/ ~present $X18 $X25 \/ ~present $X23 $X26 \/
% 0.92/1.12     ~proposition $X18 $X18 \/ ~proposition $X18 $X23 \/ ~smoke $X18 $X25 \/
% 0.92/1.12     ~smoke $X23 $X26 \/ ~state $X18 $X21 \/ ~theme $X18 $X22 $X23 \/
% 0.92/1.12     ~theme $X18 $X25 $X18 \/ ~think_believe_consider $X18 $X22 \/
% 0.92/1.12     ~think_believe_consider $X18 $X25 \/ ~vincent_forename $X18 $X16 \/
% 0.92/1.12     ~vincent_forename $X18 $X19
% 0.92/1.12  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.92/1.12     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~agent $X23 $X17 $X15 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/ ~event $X23 $X17 \/
% 0.92/1.12     ~event $X23 $X26 \/ ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 0.92/1.12     ~jules_forename $X23 $X19 \/ ~man $X23 $X15 \/ ~man $X23 $X20 \/
% 0.92/1.12     ~of $X23 $X16 $X15 \/ ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/
% 0.92/1.12     ~present $X23 $X17 \/ ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 0.92/1.12     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X23 $X21 \/ ~theme $X23 $X17 $X18 \/ ~theme $X23 $X26 $X23 \/
% 0.92/1.12     ~think_believe_consider $X23 $X17 \/
% 0.92/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16 \/
% 0.92/1.12     ~vincent_forename $X23 $X19
% 0.92/1.12  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 0.92/1.12     ~actual_world $X11 \/ ~agent $X11 $X17 $X20 \/ ~agent $X11 $X22 $X12 \/
% 0.92/1.12     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/ ~event $X11 $X22 \/
% 0.92/1.12     ~event $X18 $X25 \/ ~event $X23 $X26 \/ ~forename $X11 $X13 \/
% 0.92/1.12     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X12 \/
% 0.92/1.12     ~man $X11 $X20 \/ ~of $X11 $X13 $X12 \/ ~of $X11 $X19 $X20 \/
% 0.92/1.12     ~present $X11 $X17 \/ ~present $X11 $X22 \/ ~present $X18 $X25 \/
% 0.92/1.12     ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 0.92/1.12     ~proposition $X11 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 0.92/1.12     ~think_believe_consider $X11 $X17 \/
% 0.92/1.12     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X13 \/
% 0.92/1.12     ~vincent_forename $X11 $X19
% 0.92/1.12  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.92/1.12     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~agent $X23 $X22 $X12 \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/ ~event $X23 $X22 \/
% 0.92/1.12     ~event $X23 $X26 \/ ~forename $X23 $X13 \/ ~forename $X23 $X19 \/
% 0.92/1.12     ~jules_forename $X23 $X19 \/ ~man $X23 $X12 \/ ~man $X23 $X20 \/
% 0.92/1.12     ~of $X23 $X13 $X12 \/ ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/
% 0.92/1.12     ~present $X23 $X22 \/ ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 0.92/1.12     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.92/1.12     ~state $X23 $X21 \/ ~theme $X23 $X22 $X23 \/ ~theme $X23 $X26 $X18 \/
% 0.92/1.12     ~think_believe_consider $X23 $X22 \/
% 0.92/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X13 \/
% 0.92/1.12     ~vincent_forename $X23 $X19
% 0.92/1.12  |- ~accessible_world $X18 $X18 \/ ~accessible_world $X18 $X23 \/
% 0.92/1.12     ~actual_world $X18 \/ ~agent $X18 $X17 $X20 \/
% 0.92/1.12     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 0.92/1.12     ~be $X18 $X21 $X20 $X20 \/ ~event $X18 $X17 \/ ~event $X18 $X25 \/
% 0.92/1.12     ~event $X23 $X26 \/ ~forename $X18 $X13 \/ ~forename $X18 $X19 \/
% 0.92/1.12     ~jules_forename $X18 $X19 \/ ~man $X18 $X20 \/
% 0.92/1.12     ~man $X18 (skolemFOFtoCNF_X24 $X18) \/
% 0.92/1.12     ~of $X18 $X13 (skolemFOFtoCNF_X24 $X18) \/ ~of $X18 $X19 $X20 \/
% 0.92/1.12     ~present $X18 $X17 \/ ~present $X18 $X25 \/ ~present $X23 $X26 \/
% 0.92/1.12     ~proposition $X18 $X18 \/ ~proposition $X18 $X23 \/ ~smoke $X18 $X25 \/
% 0.92/1.12     ~smoke $X23 $X26 \/ ~state $X18 $X21 \/ ~theme $X18 $X17 $X18 \/
% 0.92/1.12     ~theme $X18 $X25 $X23 \/ ~think_believe_consider $X18 $X17 \/
% 0.92/1.12     ~think_believe_consider $X18 $X25 \/ ~vincent_forename $X18 $X13 \/
% 0.92/1.12     ~vincent_forename $X18 $X19
% 0.97/1.12  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 0.97/1.12     ~actual_world $X11 \/ ~agent $X11 $X17 $X20 \/ ~agent $X11 $X22 $X20 \/
% 0.97/1.12     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 0.97/1.12     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X17 \/ ~event $X11 $X22 \/
% 0.97/1.12     ~event $X18 $X25 \/ ~event $X23 $X26 \/ ~forename $X11 $X19 \/
% 0.97/1.12     ~jules_forename $X11 $X19 \/ ~man $X11 $X20 \/ ~of $X11 $X19 $X20 \/
% 0.97/1.12     ~present $X11 $X17 \/ ~present $X11 $X22 \/ ~present $X18 $X25 \/
% 0.97/1.12     ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 0.97/1.12     ~proposition $X11 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.97/1.12     ~state $X11 $X21 \/ ~theme $X11 $X17 $X18 \/ ~theme $X11 $X22 $X23 \/
% 0.97/1.12     ~think_believe_consider $X11 $X17 \/
% 0.97/1.12     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X19
% 0.97/1.12  |- ~accessible_world $X11 $X18 \/ ~accessible_world $X11 $X23 \/
% 0.97/1.12     ~actual_world $X11 \/ ~agent $X11 $X22 $X20 \/
% 0.97/1.12     ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/ ~agent $X23 $X26 $X20 \/
% 0.97/1.12     ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X22 \/ ~event $X18 $X25 \/
% 0.97/1.12     ~event $X23 $X26 \/ ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/
% 0.97/1.12     ~man $X11 $X20 \/ ~of $X11 $X19 $X20 \/ ~present $X11 $X22 \/
% 0.97/1.12     ~present $X18 $X25 \/ ~present $X23 $X26 \/ ~proposition $X11 $X18 \/
% 0.97/1.12     ~proposition $X11 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.97/1.12     ~state $X11 $X21 \/ ~theme $X11 $X22 $X18 \/ ~theme $X11 $X22 $X23 \/
% 0.97/1.12     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X19
% 0.97/1.12  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.97/1.12     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 0.97/1.12     ~agent $X23 $X22 $X20 \/ ~agent $X23 $X26 $X20 \/
% 0.97/1.12     ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/ ~event $X23 $X22 \/
% 0.97/1.12     ~event $X23 $X26 \/ ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/
% 0.97/1.12     ~man $X23 $X20 \/ ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/
% 0.97/1.12     ~present $X23 $X22 \/ ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 0.97/1.12     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.97/1.12     ~state $X23 $X21 \/ ~theme $X23 $X22 $X23 \/ ~theme $X23 $X26 $X18 \/
% 0.97/1.12     ~think_believe_consider $X23 $X22 \/
% 0.97/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X19
% 0.97/1.12  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.97/1.12     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 0.97/1.12     ~agent $X23 $X17 $X20 \/ ~agent $X23 $X26 $X20 \/
% 0.97/1.12     ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/ ~event $X23 $X17 \/
% 0.97/1.12     ~event $X23 $X26 \/ ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/
% 0.97/1.12     ~man $X23 $X20 \/ ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/
% 0.97/1.12     ~present $X23 $X17 \/ ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 0.97/1.12     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.97/1.12     ~state $X23 $X21 \/ ~theme $X23 $X17 $X18 \/ ~theme $X23 $X26 $X23 \/
% 0.97/1.12     ~think_believe_consider $X23 $X17 \/
% 0.97/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X19
% 0.97/1.12  |- ~accessible_world $X23 $X18 \/ ~accessible_world $X23 $X23 \/
% 0.97/1.12     ~actual_world $X23 \/ ~agent $X18 $X25 (skolemFOFtoCNF_X24 $X18) \/
% 0.97/1.12     ~agent $X23 $X26 $X20 \/ ~be $X23 $X21 $X20 $X20 \/ ~event $X18 $X25 \/
% 0.97/1.12     ~event $X23 $X26 \/ ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/
% 0.97/1.12     ~man $X23 $X20 \/ ~of $X23 $X19 $X20 \/ ~present $X18 $X25 \/
% 0.97/1.12     ~present $X23 $X26 \/ ~proposition $X23 $X18 \/
% 0.97/1.12     ~proposition $X23 $X23 \/ ~smoke $X18 $X25 \/ ~smoke $X23 $X26 \/
% 0.97/1.12     ~state $X23 $X21 \/ ~theme $X23 $X26 $X18 \/ ~theme $X23 $X26 $X23 \/
% 0.97/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X19
% 0.97/1.12  |- ~accessible_world $X11 $X23 \/ ~actual_world $X11 \/
% 0.97/1.12     ~agent $X11 $X22 $X15 \/ ~agent $X23 $X25 (skolemFOFtoCNF_X24 $X23) \/
% 0.97/1.12     ~agent $X23 $X26 $X20 \/ ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X22 \/
% 0.97/1.12     ~event $X23 $X25 \/ ~event $X23 $X26 \/ ~forename $X11 $X16 \/
% 0.97/1.12     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/
% 0.97/1.12     ~man $X11 $X20 \/ ~of $X11 $X16 $X15 \/ ~of $X11 $X19 $X20 \/
% 0.97/1.12     ~present $X11 $X22 \/ ~present $X23 $X25 \/ ~present $X23 $X26 \/
% 0.97/1.12     ~proposition $X11 $X23 \/ ~smoke $X23 $X25 \/ ~smoke $X23 $X26 \/
% 0.97/1.12     ~state $X11 $X21 \/ ~theme $X11 $X22 $X23 \/
% 0.97/1.12     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16
% 0.97/1.12  |- ~accessible_world $X23 $X23 \/ ~actual_world $X23 \/
% 0.97/1.12     ~agent $X23 $X25 (skolemFOFtoCNF_X24 $X23) \/ ~agent $X23 $X26 $X20 \/
% 0.97/1.12     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X25 \/ ~event $X23 $X26 \/
% 0.97/1.12     ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 0.97/1.12     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/
% 0.97/1.12     ~man $X23 (skolemFOFtoCNF_X24 $X23) \/
% 0.97/1.12     ~of $X23 $X16 (skolemFOFtoCNF_X24 $X23) \/ ~of $X23 $X19 $X20 \/
% 0.97/1.12     ~present $X23 $X25 \/ ~present $X23 $X26 \/ ~proposition $X23 $X23 \/
% 0.97/1.12     ~smoke $X23 $X25 \/ ~smoke $X23 $X26 \/ ~state $X23 $X21 \/
% 0.97/1.12     ~theme $X23 $X25 $X23 \/ ~think_believe_consider $X23 $X25 \/
% 0.97/1.12     ~vincent_forename $X23 $X16
% 0.97/1.12  |- ~accessible_world $X23 $X23 \/ ~actual_world $X23 \/
% 0.97/1.12     ~agent $X23 $X25 (skolemFOFtoCNF_X24 $X23) \/ ~agent $X23 $X26 $X20 \/
% 0.97/1.12     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X25 \/ ~event $X23 $X26 \/
% 0.97/1.12     ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 0.97/1.12     ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/ ~of $X23 $X16 $X20 \/
% 0.97/1.12     ~of $X23 $X19 $X20 \/ ~present $X23 $X25 \/ ~present $X23 $X26 \/
% 0.97/1.12     ~proposition $X23 $X23 \/ ~smoke $X23 $X25 \/ ~smoke $X23 $X26 \/
% 0.97/1.12     ~state $X23 $X21 \/ ~theme $X23 $X26 $X23 \/
% 0.97/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X16
% 0.97/1.12  |- ~accessible_world $X11 $X23 \/ ~actual_world $X11 \/
% 0.97/1.12     ~agent $X11 $X22 $X15 \/ ~agent $X23 $X26 (skolemFOFtoCNF_X24 $X23) \/
% 0.97/1.12     ~be $X11 $X21 (skolemFOFtoCNF_X24 $X23) (skolemFOFtoCNF_X24 $X23) \/
% 0.97/1.12     ~event $X11 $X22 \/ ~event $X23 $X26 \/ ~forename $X11 $X16 \/
% 0.97/1.12     ~forename $X11 $X19 \/ ~jules_forename $X11 $X19 \/ ~man $X11 $X15 \/
% 0.97/1.12     ~man $X11 (skolemFOFtoCNF_X24 $X23) \/ ~of $X11 $X16 $X15 \/
% 0.97/1.12     ~of $X11 $X19 (skolemFOFtoCNF_X24 $X23) \/ ~present $X11 $X22 \/
% 0.97/1.12     ~present $X23 $X26 \/ ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/
% 0.97/1.12     ~state $X11 $X21 \/ ~theme $X11 $X22 $X23 \/
% 0.97/1.12     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X16
% 0.97/1.12  |- ~accessible_world $X23 $X23 \/ ~actual_world $X23 \/
% 0.97/1.12     ~agent $X23 $X26 (skolemFOFtoCNF_X24 $X23) \/
% 0.97/1.12     ~be $X23 $X21 (skolemFOFtoCNF_X24 $X23) (skolemFOFtoCNF_X24 $X23) \/
% 0.97/1.12     ~event $X23 $X26 \/ ~forename $X23 $X16 \/ ~forename $X23 $X19 \/
% 0.97/1.12     ~jules_forename $X23 $X19 \/ ~man $X23 (skolemFOFtoCNF_X24 $X23) \/
% 0.97/1.12     ~of $X23 $X16 (skolemFOFtoCNF_X24 $X23) \/
% 0.97/1.12     ~of $X23 $X19 (skolemFOFtoCNF_X24 $X23) \/ ~present $X23 $X26 \/
% 0.97/1.12     ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/ ~state $X23 $X21 \/
% 0.97/1.12     ~theme $X23 $X26 $X23 \/ ~think_believe_consider $X23 $X26 \/
% 0.97/1.12     ~vincent_forename $X23 $X16
% 0.97/1.12  |- ~accessible_world $X11 $X23 \/ ~actual_world $X11 \/
% 0.97/1.12     ~agent $X11 $X22 $X20 \/ ~agent $X23 $X25 (skolemFOFtoCNF_X24 $X23) \/
% 0.97/1.12     ~agent $X23 $X26 $X20 \/ ~be $X11 $X21 $X20 $X20 \/ ~event $X11 $X22 \/
% 0.97/1.12     ~event $X23 $X25 \/ ~event $X23 $X26 \/ ~forename $X11 $X19 \/
% 0.97/1.12     ~jules_forename $X11 $X19 \/ ~man $X11 $X20 \/ ~of $X11 $X19 $X20 \/
% 0.97/1.12     ~present $X11 $X22 \/ ~present $X23 $X25 \/ ~present $X23 $X26 \/
% 0.97/1.12     ~proposition $X11 $X23 \/ ~smoke $X23 $X25 \/ ~smoke $X23 $X26 \/
% 0.97/1.12     ~state $X11 $X21 \/ ~theme $X11 $X22 $X23 \/
% 0.97/1.12     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X19
% 0.97/1.12  |- ~accessible_world $X23 $X23 \/ ~actual_world $X23 \/
% 0.97/1.12     ~agent $X23 $X25 (skolemFOFtoCNF_X24 $X23) \/ ~agent $X23 $X26 $X20 \/
% 0.97/1.12     ~be $X23 $X21 $X20 $X20 \/ ~event $X23 $X25 \/ ~event $X23 $X26 \/
% 0.97/1.12     ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/ ~man $X23 $X20 \/
% 0.97/1.12     ~of $X23 $X19 $X20 \/ ~present $X23 $X25 \/ ~present $X23 $X26 \/
% 0.97/1.12     ~proposition $X23 $X23 \/ ~smoke $X23 $X25 \/ ~smoke $X23 $X26 \/
% 0.97/1.12     ~state $X23 $X21 \/ ~theme $X23 $X26 $X23 \/
% 0.97/1.12     ~think_believe_consider $X23 $X26 \/ ~vincent_forename $X23 $X19
% 0.97/1.12  |- ~accessible_world $X11 $X23 \/ ~actual_world $X11 \/
% 0.97/1.12     ~agent $X11 $X22 (skolemFOFtoCNF_X24 $X23) \/
% 0.97/1.12     ~agent $X23 $X26 (skolemFOFtoCNF_X24 $X23) \/
% 0.97/1.12     ~be $X11 $X21 (skolemFOFtoCNF_X24 $X23) (skolemFOFtoCNF_X24 $X23) \/
% 0.97/1.12     ~event $X11 $X22 \/ ~event $X23 $X26 \/ ~forename $X11 $X19 \/
% 0.97/1.12     ~jules_forename $X11 $X19 \/ ~man $X11 (skolemFOFtoCNF_X24 $X23) \/
% 0.97/1.12     ~of $X11 $X19 (skolemFOFtoCNF_X24 $X23) \/ ~present $X11 $X22 \/
% 0.97/1.12     ~present $X23 $X26 \/ ~proposition $X11 $X23 \/ ~smoke $X23 $X26 \/
% 0.97/1.12     ~state $X11 $X21 \/ ~theme $X11 $X22 $X23 \/
% 0.97/1.12     ~think_believe_consider $X11 $X22 \/ ~vincent_forename $X11 $X19
% 0.97/1.12  |- ~accessible_world $X23 $X23 \/ ~actual_world $X23 \/
% 0.97/1.12     ~agent $X23 $X26 (skolemFOFtoCNF_X24 $X23) \/
% 0.97/1.12     ~be $X23 $X21 (skolemFOFtoCNF_X24 $X23) (skolemFOFtoCNF_X24 $X23) \/
% 0.97/1.12     ~event $X23 $X26 \/ ~forename $X23 $X19 \/ ~jules_forename $X23 $X19 \/
% 0.97/1.12     ~man $X23 (skolemFOFtoCNF_X24 $X23) \/
% 0.97/1.12     ~of $X23 $X19 (skolemFOFtoCNF_X24 $X23) \/ ~present $X23 $X26 \/
% 0.97/1.12     ~proposition $X23 $X23 \/ ~smoke $X23 $X26 \/ ~state $X23 $X21 \/
% 0.97/1.12     ~theme $X23 $X26 $X23 \/ ~think_believe_consider $X23 $X26 \/
% 0.97/1.12     ~vincent_forename $X23 $X19
% 0.97/1.12  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.12     ~agent skolemFOFtoCNF_U $_12 skolemFOFtoCNF_X4 \/
% 0.97/1.12     ~event skolemFOFtoCNF_U $_12 \/ ~forename skolemFOFtoCNF_U $_8 \/
% 0.97/1.12     ~jules_forename skolemFOFtoCNF_U $_8 \/
% 0.97/1.12     ~of skolemFOFtoCNF_U $_8 skolemFOFtoCNF_X4 \/
% 0.97/1.12     ~present skolemFOFtoCNF_U $_12 \/
% 0.97/1.12     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.12     ~smoke skolemFOFtoCNF_U $_12 \/
% 0.97/1.12     ~theme skolemFOFtoCNF_U $_12 skolemFOFtoCNF_U \/
% 0.97/1.12     ~think_believe_consider skolemFOFtoCNF_U $_12 \/
% 0.97/1.12     ~vincent_forename skolemFOFtoCNF_U $_8 \/
% 0.97/1.12     man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U)
% 0.97/1.12  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.12     ~agent skolemFOFtoCNF_U $_25 skolemFOFtoCNF_X4 \/
% 0.97/1.12     ~event skolemFOFtoCNF_U $_25 \/ ~forename skolemFOFtoCNF_U $_20 \/
% 0.97/1.12     ~forename skolemFOFtoCNF_U $_21 \/
% 0.97/1.12     ~jules_forename skolemFOFtoCNF_U $_21 \/
% 0.97/1.12     ~of skolemFOFtoCNF_U $_20 skolemFOFtoCNF_X4 \/
% 0.97/1.12     ~of skolemFOFtoCNF_U $_21 skolemFOFtoCNF_X4 \/
% 0.97/1.12     ~present skolemFOFtoCNF_U $_25 \/
% 0.97/1.12     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.12     ~smoke skolemFOFtoCNF_U $_25 \/
% 0.97/1.12     ~theme skolemFOFtoCNF_U $_25 skolemFOFtoCNF_U \/
% 0.97/1.12     ~think_believe_consider skolemFOFtoCNF_U $_25 \/
% 0.97/1.12     ~vincent_forename skolemFOFtoCNF_U $_20 \/
% 0.97/1.12     man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U)
% 0.97/1.12  |- ~accessible_world skolemFOFtoCNF_U $_35 \/
% 0.97/1.12     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.12     ~agent skolemFOFtoCNF_U $_40 skolemFOFtoCNF_X4 \/
% 0.97/1.12     ~event skolemFOFtoCNF_U $_40 \/ ~forename skolemFOFtoCNF_U $_36 \/
% 0.97/1.12     ~jules_forename skolemFOFtoCNF_U $_36 \/
% 0.97/1.12     ~of skolemFOFtoCNF_U $_36 skolemFOFtoCNF_X4 \/
% 0.97/1.12     ~present skolemFOFtoCNF_U $_40 \/ ~proposition skolemFOFtoCNF_U $_35 \/
% 0.97/1.12     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.12     ~smoke skolemFOFtoCNF_U $_40 \/ ~theme skolemFOFtoCNF_U $_40 $_35 \/
% 0.97/1.12     ~theme skolemFOFtoCNF_U $_40 skolemFOFtoCNF_U \/
% 0.97/1.12     ~think_believe_consider skolemFOFtoCNF_U $_40 \/
% 0.97/1.12     ~vincent_forename skolemFOFtoCNF_U $_36 \/
% 0.97/1.12     man $_35 (skolemFOFtoCNF_X24 $_35)
% 0.97/1.12  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.12     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 0.97/1.12     ~forename skolemFOFtoCNF_U $_42 \/
% 0.97/1.12     ~jules_forename skolemFOFtoCNF_U $_42 \/
% 0.97/1.12     ~of skolemFOFtoCNF_U $_42 skolemFOFtoCNF_X4 \/
% 0.97/1.12     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.12     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X1 \/
% 0.97/1.12     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_U \/
% 0.97/1.12     ~vincent_forename skolemFOFtoCNF_U $_42 \/
% 0.97/1.12     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.12  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.12     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X4 \/
% 0.97/1.12     ~forename skolemFOFtoCNF_U $_42 \/
% 0.97/1.12     ~jules_forename skolemFOFtoCNF_U $_42 \/
% 0.97/1.12     ~of skolemFOFtoCNF_U $_42 skolemFOFtoCNF_X4 \/
% 0.97/1.12     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.12     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/
% 0.97/1.12     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_U \/
% 0.97/1.12     ~vincent_forename skolemFOFtoCNF_U $_42 \/
% 0.97/1.12     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_50 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_51 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_50 \/ ~event skolemFOFtoCNF_U $_51 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_46 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_46 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_46 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_50 \/ ~present skolemFOFtoCNF_U $_51 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_50 \/ ~smoke skolemFOFtoCNF_U $_51 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_51 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_51 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_46
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_60 \/
% 0.97/1.13     ~agent $_60 $_61 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_59 skolemFOFtoCNF_X4 \/ ~event $_60 $_61 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_59 \/ ~forename skolemFOFtoCNF_U $_56 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_56 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_56 skolemFOFtoCNF_X4 \/ ~present $_60 $_61 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_59 \/ ~proposition skolemFOFtoCNF_U $_60 \/
% 0.97/1.13     ~smoke $_60 $_61 \/ ~theme skolemFOFtoCNF_U $_59 $_60 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_59 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_56 \/
% 0.97/1.13     man $_60 (skolemFOFtoCNF_X24 $_60)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_73 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_78 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_78 \/ ~forename skolemFOFtoCNF_U $_72 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_74 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_74 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_72 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_74 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_78 \/ ~proposition skolemFOFtoCNF_U $_73 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_78 \/ ~theme skolemFOFtoCNF_U $_78 $_73 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_78 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_78 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_72 \/
% 0.97/1.13     man $_73 (skolemFOFtoCNF_X24 $_73)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_79 \/ ~forename skolemFOFtoCNF_U $_81 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_81 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_79 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_81 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X1 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_U \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_79 \/
% 0.97/1.13     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_79 \/ ~forename skolemFOFtoCNF_U $_81 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_81 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_79 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_81 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_U \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_79 \/
% 0.97/1.13     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_92 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_93 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_92 \/ ~event skolemFOFtoCNF_U $_93 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_87 \/ ~forename skolemFOFtoCNF_U $_88 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_88 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_87 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_88 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_92 \/ ~present skolemFOFtoCNF_U $_93 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_92 \/ ~smoke skolemFOFtoCNF_U $_93 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_93 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_93 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_87
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_98 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent $_98 $_103 (skolemFOFtoCNF_X24 $_98) \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_104 skolemFOFtoCNF_X4 \/ ~event $_98 $_103 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_104 \/ ~forename skolemFOFtoCNF_U $_99 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_99 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_99 skolemFOFtoCNF_X4 \/ ~present $_98 $_103 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_104 \/ ~proposition skolemFOFtoCNF_U $_98 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_98 $_103 \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_104 \/ ~theme skolemFOFtoCNF_U $_104 $_98 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_104 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_104 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_99
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_114 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_115 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_114 \/ ~event skolemFOFtoCNF_U $_115 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_109 \/ ~forename skolemFOFtoCNF_U $_110 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_110 \/
% 0.97/1.13     ~man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_109 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_110 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_114 \/ ~present skolemFOFtoCNF_U $_115 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_114 \/ ~smoke skolemFOFtoCNF_U $_115 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_114 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_114 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_109
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_120 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_124 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_126 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_124 \/ ~event skolemFOFtoCNF_U $_126 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_121 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_121 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_121 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_124 \/ ~present skolemFOFtoCNF_U $_126 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_120 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_126 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_124 skolemFOFtoCNF_U \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_126 $_120 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_124 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_126 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_121 \/
% 0.97/1.13     man $_120 (skolemFOFtoCNF_X24 $_120)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_129 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_129 \/ ~forename skolemFOFtoCNF_U $_128 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_128 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_128 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_129 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X1 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_129 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_129 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_128 \/
% 0.97/1.13     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_129 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_129 \/ ~forename skolemFOFtoCNF_U $_128 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_128 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_128 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_129 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_129 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_129 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_128 \/
% 0.97/1.13     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_136 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_135 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_141 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_135 \/ ~event skolemFOFtoCNF_U $_141 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_137 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_137 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_137 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_135 \/ ~present skolemFOFtoCNF_U $_141 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_136 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_141 \/ ~theme skolemFOFtoCNF_U $_135 $_136 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_141 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_135 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_141 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_137 \/
% 0.97/1.13     man $_136 (skolemFOFtoCNF_X24 $_136)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_145 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_145 \/ ~forename skolemFOFtoCNF_U $_144 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_144 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_144 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_145 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_145 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_145 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_145 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_144 \/
% 0.97/1.13     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_145 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_145 \/ ~forename skolemFOFtoCNF_U $_144 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_144 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_144 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_145 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_145 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_145 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_145 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_144 \/
% 0.97/1.13     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_159 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U $_164 \/
% 0.97/1.13     ~agent $_164 $_165 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_163 skolemFOFtoCNF_X4 \/ ~event $_164 $_165 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_163 \/ ~forename skolemFOFtoCNF_U $_160 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_160 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_160 skolemFOFtoCNF_X4 \/ ~present $_164 $_165 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_163 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_159 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_164 \/ ~smoke $_164 $_165 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_163 $_159 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_163 $_164 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_163 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_160 \/
% 0.97/1.13     man $_159 (skolemFOFtoCNF_X24 $_159)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_169 \/
% 0.97/1.13     ~agent $_169 $_170 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event $_169 $_170 \/ ~forename skolemFOFtoCNF_U $_167 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_167 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_167 skolemFOFtoCNF_X4 \/ ~present $_169 $_170 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_169 \/ ~smoke $_169 $_170 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_169 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_167 \/
% 0.97/1.13     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_169 \/
% 0.97/1.13     ~agent $_169 $_170 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event $_169 $_170 \/ ~forename skolemFOFtoCNF_U $_167 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_167 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_167 skolemFOFtoCNF_X4 \/ ~present $_169 $_170 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_169 \/ ~smoke $_169 $_170 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_169 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_167 \/
% 0.97/1.13     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_166 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_X2 $_170 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_X2 $_170 \/ ~forename skolemFOFtoCNF_U $_167 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_167 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_167 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_X2 $_170 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_166 \/ ~smoke skolemFOFtoCNF_X2 $_170 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_166 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_167 \/
% 0.97/1.13     man $_166 (skolemFOFtoCNF_X24 $_166)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_166 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_X7 $_170 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_X7 $_170 \/ ~forename skolemFOFtoCNF_U $_167 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_167 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_167 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_X7 $_170 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_166 \/ ~smoke skolemFOFtoCNF_X7 $_170 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_166 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_167 \/
% 0.97/1.13     man $_166 (skolemFOFtoCNF_X24 $_166)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_188 \/
% 0.97/1.13     ~agent $_188 $_189 (skolemFOFtoCNF_X24 $_188) \/
% 0.97/1.13     ~agent $_188 $_190 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_187 skolemFOFtoCNF_X4 \/ ~event $_188 $_189 \/
% 0.97/1.13     ~event $_188 $_190 \/ ~event skolemFOFtoCNF_U $_187 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_184 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_184 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_184 skolemFOFtoCNF_X4 \/ ~present $_188 $_189 \/
% 0.97/1.13     ~present $_188 $_190 \/ ~present skolemFOFtoCNF_U $_187 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_188 \/ ~smoke $_188 $_189 \/
% 0.97/1.13     ~smoke $_188 $_190 \/ ~theme skolemFOFtoCNF_U $_187 $_188 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_187 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_184
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_203 \/
% 0.97/1.13     ~agent $_203 $_204 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_202 $_197 \/ ~event $_203 $_204 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_202 \/ ~forename skolemFOFtoCNF_U $_198 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_199 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_199 \/ ~man skolemFOFtoCNF_U $_197 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_198 $_197 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_199 skolemFOFtoCNF_X4 \/ ~present $_203 $_204 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_202 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_203 \/ ~smoke $_203 $_204 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_202 $_203 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_202 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_198 \/
% 0.97/1.13     man $_203 (skolemFOFtoCNF_X24 $_203)
% 0.97/1.13  |- ~agent skolemFOFtoCNF_X7 $_216 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_X7 $_216 \/ ~present skolemFOFtoCNF_X7 $_216 \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_X7 $_216 \/
% 0.97/1.13     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.13  |- ~agent skolemFOFtoCNF_X2 $_223 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_X2 $_223 \/ ~present skolemFOFtoCNF_X2 $_223 \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_X2 $_223 \/
% 0.97/1.13     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_226 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent $_226 $_231 (skolemFOFtoCNF_X24 $_226) \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_232 skolemFOFtoCNF_X4 \/ ~event $_226 $_231 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_232 \/ ~forename skolemFOFtoCNF_U $_225 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_227 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_227 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_225 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_227 skolemFOFtoCNF_X4 \/ ~present $_226 $_231 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_232 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_226 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_226 $_231 \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_232 \/ ~theme skolemFOFtoCNF_U $_232 $_226 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_232 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_232 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_225
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_239 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_243 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_245 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_243 \/ ~event skolemFOFtoCNF_U $_245 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_238 \/ ~forename skolemFOFtoCNF_U $_240 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_240 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_238 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_240 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_243 \/ ~present skolemFOFtoCNF_U $_245 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_239 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_245 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_243 skolemFOFtoCNF_U \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_245 $_239 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_243 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_245 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_238 \/
% 0.97/1.13     man $_239 (skolemFOFtoCNF_X24 $_239)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_249 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_249 \/ ~forename skolemFOFtoCNF_U $_246 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_248 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_248 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_246 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_248 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_249 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X1 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_249 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_249 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_246 \/
% 0.97/1.13     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_249 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_249 \/ ~forename skolemFOFtoCNF_U $_246 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_248 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_248 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_246 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_248 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_249 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_249 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_249 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_246 \/
% 0.97/1.13     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_259 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_258 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_264 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_258 \/ ~event skolemFOFtoCNF_U $_264 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_257 \/ ~forename skolemFOFtoCNF_U $_260 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_260 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_257 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_260 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_258 \/ ~present skolemFOFtoCNF_U $_264 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_259 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_264 \/ ~theme skolemFOFtoCNF_U $_258 $_259 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_264 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_258 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_264 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_257 \/
% 0.97/1.13     man $_259 (skolemFOFtoCNF_X24 $_259)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_269 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_269 \/ ~forename skolemFOFtoCNF_U $_265 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_268 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_268 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_265 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_268 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_269 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_269 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_269 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_269 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_265 \/
% 0.97/1.13     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_269 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_269 \/ ~forename skolemFOFtoCNF_U $_265 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_268 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_268 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_265 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_268 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_269 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_269 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_269 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_269 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_265 \/
% 0.97/1.13     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_281 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent $_281 $_283 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_282 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~event $_281 $_283 \/ ~event skolemFOFtoCNF_U $_282 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_276 \/ ~forename skolemFOFtoCNF_U $_278 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_278 \/
% 0.97/1.13     ~man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_276 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_278 skolemFOFtoCNF_X4 \/ ~present $_281 $_283 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_282 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_281 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_281 $_283 \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_282 \/ ~theme skolemFOFtoCNF_U $_282 $_281 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_282 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_282 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_276
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_290 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent $_290 $_295 (skolemFOFtoCNF_X24 $_290) \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_289 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_296 skolemFOFtoCNF_X4 \/ ~event $_290 $_295 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_289 \/ ~event skolemFOFtoCNF_U $_296 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_291 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_291 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_291 skolemFOFtoCNF_X4 \/ ~present $_290 $_295 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_289 \/ ~present skolemFOFtoCNF_U $_296 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_290 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_290 $_295 \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_296 \/ ~theme skolemFOFtoCNF_U $_289 $_290 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_296 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_289 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_296 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_291
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_302 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent $_302 $_308 (skolemFOFtoCNF_X24 $_302) \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_306 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_309 skolemFOFtoCNF_X4 \/ ~event $_302 $_308 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_306 \/ ~event skolemFOFtoCNF_U $_309 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_303 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_303 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_303 skolemFOFtoCNF_X4 \/ ~present $_302 $_308 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_306 \/ ~present skolemFOFtoCNF_U $_309 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_302 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_302 $_308 \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_309 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_306 skolemFOFtoCNF_U \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_309 $_302 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_306 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_309 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_303
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_316 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U $_321 \/
% 0.97/1.13     ~agent $_316 $_322 (skolemFOFtoCNF_X24 $_316) \/
% 0.97/1.13     ~agent $_321 $_323 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_320 skolemFOFtoCNF_X4 \/ ~event $_316 $_322 \/
% 0.97/1.13     ~event $_321 $_323 \/ ~event skolemFOFtoCNF_U $_320 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_317 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_317 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_317 skolemFOFtoCNF_X4 \/ ~present $_316 $_322 \/
% 0.97/1.13     ~present $_321 $_323 \/ ~present skolemFOFtoCNF_U $_320 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_316 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_321 \/ ~smoke $_316 $_322 \/
% 0.97/1.13     ~smoke $_321 $_323 \/ ~theme skolemFOFtoCNF_U $_320 $_316 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_320 $_321 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_320 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_317
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_332 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U $_337 \/
% 0.97/1.13     ~agent $_337 $_338 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_331 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_336 skolemFOFtoCNF_X4 \/ ~event $_337 $_338 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_331 \/ ~event skolemFOFtoCNF_U $_336 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_333 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_333 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_333 skolemFOFtoCNF_X4 \/ ~present $_337 $_338 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_331 \/ ~present skolemFOFtoCNF_U $_336 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_332 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_337 \/ ~smoke $_337 $_338 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_331 $_332 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_336 $_337 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_331 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_336 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_333 \/
% 0.97/1.13     man $_332 (skolemFOFtoCNF_X24 $_332)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_343 \/
% 0.97/1.13     ~agent $_343 $_344 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_342 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event $_343 $_344 \/ ~event skolemFOFtoCNF_U $_342 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_341 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_341 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_341 skolemFOFtoCNF_X4 \/ ~present $_343 $_344 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_342 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_343 \/ ~smoke $_343 $_344 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_342 $_343 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_342 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_341 \/
% 0.97/1.13     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_343 \/
% 0.97/1.13     ~agent $_343 $_344 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_342 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event $_343 $_344 \/ ~event skolemFOFtoCNF_U $_342 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_341 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_341 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_341 skolemFOFtoCNF_X4 \/ ~present $_343 $_344 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_342 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_343 \/ ~smoke $_343 $_344 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_342 $_343 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_342 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_341 \/
% 0.97/1.13     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_340 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_339 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_X2 $_344 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_339 \/ ~event skolemFOFtoCNF_X2 $_344 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_341 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_341 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_341 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_339 \/ ~present skolemFOFtoCNF_X2 $_344 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_340 \/ ~smoke skolemFOFtoCNF_X2 $_344 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_339 $_340 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_339 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_341 \/
% 0.97/1.13     man $_340 (skolemFOFtoCNF_X24 $_340)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_340 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_339 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_X7 $_344 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_339 \/ ~event skolemFOFtoCNF_X7 $_344 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_341 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_341 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_341 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_339 \/ ~present skolemFOFtoCNF_X7 $_344 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_340 \/ ~smoke skolemFOFtoCNF_X7 $_344 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_339 $_340 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_339 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_341 \/
% 0.97/1.13     man $_340 (skolemFOFtoCNF_X24 $_340)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_370 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U $_375 \/
% 0.97/1.13     ~agent $_375 $_376 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_374 $_368 \/ ~event $_375 $_376 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_374 \/ ~forename skolemFOFtoCNF_U $_369 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_371 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_371 \/ ~man skolemFOFtoCNF_U $_368 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_369 $_368 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_371 skolemFOFtoCNF_X4 \/ ~present $_375 $_376 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_374 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_370 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_375 \/ ~smoke $_375 $_376 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_374 $_370 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_374 $_375 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_374 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_369 \/
% 0.97/1.13     man $_370 (skolemFOFtoCNF_X24 $_370)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_382 \/
% 0.97/1.13     ~agent $_382 $_383 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_377 \/ ~event $_382 $_383 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_378 \/ ~forename skolemFOFtoCNF_U $_380 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_380 \/ ~man skolemFOFtoCNF_U $_377 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_378 $_377 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_380 skolemFOFtoCNF_X4 \/ ~present $_382 $_383 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_382 \/ ~smoke $_382 $_383 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_382 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_378 \/
% 0.97/1.13     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_382 \/
% 0.97/1.13     ~agent $_382 $_383 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_377 \/ ~event $_382 $_383 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_378 \/ ~forename skolemFOFtoCNF_U $_380 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_380 \/ ~man skolemFOFtoCNF_U $_377 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_378 $_377 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_380 skolemFOFtoCNF_X4 \/ ~present $_382 $_383 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_382 \/ ~smoke $_382 $_383 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_382 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_378 \/
% 0.97/1.13     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_379 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_377 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_X2 $_383 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_X2 $_383 \/ ~forename skolemFOFtoCNF_U $_378 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_380 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_380 \/ ~man skolemFOFtoCNF_U $_377 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_378 $_377 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_380 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_X2 $_383 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_379 \/ ~smoke skolemFOFtoCNF_X2 $_383 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_379 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_378 \/
% 0.97/1.13     man $_379 (skolemFOFtoCNF_X24 $_379)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_379 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_377 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_X7 $_383 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_X7 $_383 \/ ~forename skolemFOFtoCNF_U $_378 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_380 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_380 \/ ~man skolemFOFtoCNF_U $_377 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_378 $_377 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_380 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_X7 $_383 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_379 \/ ~smoke skolemFOFtoCNF_X7 $_383 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_379 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_378 \/
% 0.97/1.13     man $_379 (skolemFOFtoCNF_X24 $_379)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_411 \/
% 0.97/1.13     ~agent $_411 $_412 (skolemFOFtoCNF_X24 $_411) \/
% 0.97/1.13     ~agent $_411 $_413 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_410 $_405 \/ ~event $_411 $_412 \/
% 0.97/1.13     ~event $_411 $_413 \/ ~event skolemFOFtoCNF_U $_410 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_406 \/ ~forename skolemFOFtoCNF_U $_407 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_407 \/ ~man skolemFOFtoCNF_U $_405 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_406 $_405 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_407 skolemFOFtoCNF_X4 \/ ~present $_411 $_412 \/
% 0.97/1.13     ~present $_411 $_413 \/ ~present skolemFOFtoCNF_U $_410 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_411 \/ ~smoke $_411 $_412 \/
% 0.97/1.13     ~smoke $_411 $_413 \/ ~theme skolemFOFtoCNF_U $_410 $_411 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_410 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_406
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_424 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_423 $_421 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_429 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_423 \/ ~event skolemFOFtoCNF_U $_429 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_422 \/ ~forename skolemFOFtoCNF_U $_425 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_425 \/ ~man skolemFOFtoCNF_U $_421 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_422 $_421 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_425 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_423 \/ ~present skolemFOFtoCNF_U $_429 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_424 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_429 \/ ~theme skolemFOFtoCNF_U $_423 $_424 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_429 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_423 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_429 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_422 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_425 \/
% 0.97/1.13     man $_424 (skolemFOFtoCNF_X24 $_424)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_435 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_430 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_435 \/ ~forename skolemFOFtoCNF_U $_431 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_434 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_434 \/ ~man skolemFOFtoCNF_U $_430 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_431 $_430 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_434 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_435 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_435 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_435 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_435 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_431 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_434 \/
% 0.97/1.13     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_435 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_430 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_435 \/ ~forename skolemFOFtoCNF_U $_431 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_434 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_434 \/ ~man skolemFOFtoCNF_U $_430 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_431 $_430 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_434 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_435 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_435 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_435 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_435 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_431 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_434 \/
% 0.97/1.13     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_446 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_450 $_444 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_452 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_450 \/ ~event skolemFOFtoCNF_U $_452 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_445 \/ ~forename skolemFOFtoCNF_U $_447 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_447 \/ ~man skolemFOFtoCNF_U $_444 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_445 $_444 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_447 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_450 \/ ~present skolemFOFtoCNF_U $_452 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_446 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_452 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_450 skolemFOFtoCNF_U \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_452 $_446 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_450 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_452 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_445 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_447 \/
% 0.97/1.13     man $_446 (skolemFOFtoCNF_X24 $_446)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_457 $_453 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_457 \/ ~forename skolemFOFtoCNF_U $_454 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_456 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_456 \/ ~man skolemFOFtoCNF_U $_453 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_454 $_453 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_456 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_457 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X1 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_457 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_457 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_454 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_456 \/
% 0.97/1.13     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_457 $_453 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_457 \/ ~forename skolemFOFtoCNF_U $_454 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_456 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_456 \/ ~man skolemFOFtoCNF_U $_453 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_454 $_453 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_456 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_457 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_457 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_457 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_454 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_456 \/
% 0.97/1.13     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_469 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent $_469 $_474 (skolemFOFtoCNF_X24 $_469) \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_468 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_475 skolemFOFtoCNF_X4 \/ ~event $_469 $_474 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_468 \/ ~event skolemFOFtoCNF_U $_475 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_467 \/ ~forename skolemFOFtoCNF_U $_470 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_470 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_467 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_470 skolemFOFtoCNF_X4 \/ ~present $_469 $_474 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_468 \/ ~present skolemFOFtoCNF_U $_475 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_469 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_469 $_474 \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_475 \/ ~theme skolemFOFtoCNF_U $_468 $_469 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_475 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_468 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_475 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_467
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_483 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent $_483 $_489 (skolemFOFtoCNF_X24 $_483) \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_487 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_490 skolemFOFtoCNF_X4 \/ ~event $_483 $_489 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_487 \/ ~event skolemFOFtoCNF_U $_490 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_482 \/ ~forename skolemFOFtoCNF_U $_484 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_484 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_482 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_484 skolemFOFtoCNF_X4 \/ ~present $_483 $_489 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_487 \/ ~present skolemFOFtoCNF_U $_490 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_483 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_483 $_489 \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_490 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_487 skolemFOFtoCNF_U \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_490 $_483 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_487 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_490 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_482
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_503 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent $_503 $_505 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_498 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_504 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~event $_503 $_505 \/ ~event skolemFOFtoCNF_U $_498 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_504 \/ ~forename skolemFOFtoCNF_U $_497 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_500 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_500 \/
% 0.97/1.13     ~man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_497 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_500 skolemFOFtoCNF_X4 \/ ~present $_503 $_505 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_498 \/ ~present skolemFOFtoCNF_U $_504 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_503 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_503 $_505 \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_504 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_498 skolemFOFtoCNF_U \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_504 $_503 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_498 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_504 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_497
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_518 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent $_518 $_520 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_517 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_519 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~event $_518 $_520 \/ ~event skolemFOFtoCNF_U $_517 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_519 \/ ~forename skolemFOFtoCNF_U $_512 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_514 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_514 \/
% 0.97/1.13     ~man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_512 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_514 skolemFOFtoCNF_X4 \/ ~present $_518 $_520 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_517 \/ ~present skolemFOFtoCNF_U $_519 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_518 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_518 $_520 \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_519 \/ ~theme skolemFOFtoCNF_U $_517 $_518 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_519 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_517 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_519 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_512
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_533 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent $_533 $_535 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_532 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_534 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~event $_533 $_535 \/ ~event skolemFOFtoCNF_U $_532 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_534 \/ ~forename skolemFOFtoCNF_U $_527 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_529 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_529 \/
% 0.97/1.13     ~man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_527 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_529 skolemFOFtoCNF_X4 \/ ~present $_533 $_535 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_532 \/ ~present skolemFOFtoCNF_U $_534 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_533 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_533 $_535 \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_534 \/ ~theme skolemFOFtoCNF_U $_532 $_533 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_534 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_532 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_534 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_527 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_529
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_548 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent $_548 $_550 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_543 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_549 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~event $_548 $_550 \/ ~event skolemFOFtoCNF_U $_543 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_549 \/ ~forename skolemFOFtoCNF_U $_542 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_545 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_545 \/
% 0.97/1.13     ~man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_542 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_545 skolemFOFtoCNF_X4 \/ ~present $_548 $_550 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_543 \/ ~present skolemFOFtoCNF_U $_549 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_548 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_548 $_550 \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_549 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_543 skolemFOFtoCNF_U \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_549 $_548 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_543 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_549 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_542 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_545
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_561 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_560 $_558 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_566 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_560 \/ ~event skolemFOFtoCNF_U $_566 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_557 \/ ~forename skolemFOFtoCNF_U $_559 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_562 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_562 \/ ~man skolemFOFtoCNF_U $_558 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_557 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_559 $_558 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_562 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_560 \/ ~present skolemFOFtoCNF_U $_566 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_561 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_566 \/ ~theme skolemFOFtoCNF_U $_560 $_561 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_566 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_560 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_566 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_557 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_559 \/
% 0.97/1.13     man $_561 (skolemFOFtoCNF_X24 $_561)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_573 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_568 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_573 \/ ~forename skolemFOFtoCNF_U $_567 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_569 \/ ~forename skolemFOFtoCNF_U $_572 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_572 \/ ~man skolemFOFtoCNF_U $_568 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_567 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_569 $_568 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_572 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_573 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_573 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_573 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_573 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_567 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_569 \/
% 0.97/1.13     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_573 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_568 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_573 \/ ~forename skolemFOFtoCNF_U $_567 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_569 \/ ~forename skolemFOFtoCNF_U $_572 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_572 \/ ~man skolemFOFtoCNF_U $_568 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_567 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_569 $_568 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_572 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_573 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_573 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_573 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_573 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_567 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_569 \/
% 0.97/1.13     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_587 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_591 $_584 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_593 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_591 \/ ~event skolemFOFtoCNF_U $_593 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_585 \/ ~forename skolemFOFtoCNF_U $_586 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_588 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_588 \/ ~man skolemFOFtoCNF_U $_584 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_585 $_584 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_586 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_588 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_591 \/ ~present skolemFOFtoCNF_U $_593 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_587 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U $_593 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_591 skolemFOFtoCNF_U \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_593 $_587 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_591 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_593 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_585 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_586 \/
% 0.97/1.13     man $_587 (skolemFOFtoCNF_X24 $_587)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_599 $_594 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_599 \/ ~forename skolemFOFtoCNF_U $_595 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_596 \/ ~forename skolemFOFtoCNF_U $_598 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_598 \/ ~man skolemFOFtoCNF_U $_594 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_595 $_594 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_596 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_598 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_599 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X1 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_599 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_599 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_595 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_596 \/
% 0.97/1.13     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_599 $_594 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_599 \/ ~forename skolemFOFtoCNF_U $_595 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_596 \/ ~forename skolemFOFtoCNF_U $_598 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_598 \/ ~man skolemFOFtoCNF_U $_594 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_595 $_594 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_596 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_598 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_599 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.13     ~smoke skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_599 skolemFOFtoCNF_U \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_599 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_595 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_596 \/
% 0.97/1.13     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_613 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U $_618 \/
% 0.97/1.13     ~agent $_613 $_619 (skolemFOFtoCNF_X24 $_613) \/
% 0.97/1.13     ~agent $_618 $_620 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_612 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_617 skolemFOFtoCNF_X4 \/ ~event $_613 $_619 \/
% 0.97/1.13     ~event $_618 $_620 \/ ~event skolemFOFtoCNF_U $_612 \/
% 0.97/1.13     ~event skolemFOFtoCNF_U $_617 \/ ~forename skolemFOFtoCNF_U $_614 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_614 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_614 skolemFOFtoCNF_X4 \/ ~present $_613 $_619 \/
% 0.97/1.13     ~present $_618 $_620 \/ ~present skolemFOFtoCNF_U $_612 \/
% 0.97/1.13     ~present skolemFOFtoCNF_U $_617 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_613 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_618 \/ ~smoke $_613 $_619 \/
% 0.97/1.13     ~smoke $_618 $_620 \/ ~theme skolemFOFtoCNF_U $_612 $_613 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_617 $_618 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_612 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_617 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_614
% 0.97/1.13  |- ~accessible_world skolemFOFtoCNF_U $_631 \/
% 0.97/1.13     ~accessible_world skolemFOFtoCNF_U $_636 \/
% 0.97/1.13     ~agent $_631 $_637 (skolemFOFtoCNF_X24 $_631) \/
% 0.97/1.13     ~agent $_636 $_638 skolemFOFtoCNF_X4 \/
% 0.97/1.13     ~agent skolemFOFtoCNF_U $_635 $_629 \/ ~event $_631 $_637 \/
% 0.97/1.13     ~event $_636 $_638 \/ ~event skolemFOFtoCNF_U $_635 \/
% 0.97/1.13     ~forename skolemFOFtoCNF_U $_630 \/ ~forename skolemFOFtoCNF_U $_632 \/
% 0.97/1.13     ~jules_forename skolemFOFtoCNF_U $_632 \/ ~man skolemFOFtoCNF_U $_629 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_630 $_629 \/
% 0.97/1.13     ~of skolemFOFtoCNF_U $_632 skolemFOFtoCNF_X4 \/ ~present $_631 $_637 \/
% 0.97/1.13     ~present $_636 $_638 \/ ~present skolemFOFtoCNF_U $_635 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_631 \/
% 0.97/1.13     ~proposition skolemFOFtoCNF_U $_636 \/ ~smoke $_631 $_637 \/
% 0.97/1.13     ~smoke $_636 $_638 \/ ~theme skolemFOFtoCNF_U $_635 $_631 \/
% 0.97/1.13     ~theme skolemFOFtoCNF_U $_635 $_636 \/
% 0.97/1.13     ~think_believe_consider skolemFOFtoCNF_U $_635 \/
% 0.97/1.13     ~vincent_forename skolemFOFtoCNF_U $_630
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_650 \/
% 0.97/1.14     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.14     ~agent $_650 $_655 (skolemFOFtoCNF_X24 $_650) \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_649 $_647 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_656 skolemFOFtoCNF_X4 \/ ~event $_650 $_655 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_649 \/ ~event skolemFOFtoCNF_U $_656 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_648 \/ ~forename skolemFOFtoCNF_U $_651 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_651 \/ ~man skolemFOFtoCNF_U $_647 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_648 $_647 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_651 skolemFOFtoCNF_X4 \/ ~present $_650 $_655 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_649 \/ ~present skolemFOFtoCNF_U $_656 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_650 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_650 $_655 \/
% 0.97/1.14     ~smoke skolemFOFtoCNF_U $_656 \/ ~theme skolemFOFtoCNF_U $_649 $_650 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_656 skolemFOFtoCNF_U \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_649 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_656 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_648 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_651
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_666 \/
% 0.97/1.14     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.14     ~agent $_666 $_672 (skolemFOFtoCNF_X24 $_666) \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_670 $_664 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_673 skolemFOFtoCNF_X4 \/ ~event $_666 $_672 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_670 \/ ~event skolemFOFtoCNF_U $_673 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_665 \/ ~forename skolemFOFtoCNF_U $_667 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_667 \/ ~man skolemFOFtoCNF_U $_664 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_665 $_664 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_667 skolemFOFtoCNF_X4 \/ ~present $_666 $_672 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_670 \/ ~present skolemFOFtoCNF_U $_673 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_666 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_666 $_672 \/
% 0.97/1.14     ~smoke skolemFOFtoCNF_U $_673 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_670 skolemFOFtoCNF_U \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_673 $_666 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_670 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_673 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_665 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_667
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_685 \/
% 0.97/1.14     ~accessible_world skolemFOFtoCNF_U $_690 \/
% 0.97/1.14     ~agent $_690 $_691 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_684 $_682 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_689 $_682 \/ ~event $_690 $_691 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_684 \/ ~event skolemFOFtoCNF_U $_689 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_683 \/ ~forename skolemFOFtoCNF_U $_686 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_686 \/ ~man skolemFOFtoCNF_U $_682 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_683 $_682 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_686 skolemFOFtoCNF_X4 \/ ~present $_690 $_691 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_684 \/ ~present skolemFOFtoCNF_U $_689 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_685 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_690 \/ ~smoke $_690 $_691 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_684 $_685 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_689 $_690 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_684 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_689 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_683 \/
% 0.97/1.14     man $_685 (skolemFOFtoCNF_X24 $_685)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_698 \/
% 0.97/1.14     ~agent $_698 $_699 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_697 $_692 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_692 \/ ~event $_698 $_699 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_697 \/ ~forename skolemFOFtoCNF_U $_693 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_696 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_696 \/ ~man skolemFOFtoCNF_U $_692 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_693 $_692 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_696 skolemFOFtoCNF_X4 \/ ~present $_698 $_699 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_697 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_698 \/ ~smoke $_698 $_699 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_697 $_698 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_697 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_693 \/
% 0.97/1.14     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_698 \/
% 0.97/1.14     ~agent $_698 $_699 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_697 $_692 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_692 \/ ~event $_698 $_699 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_697 \/ ~forename skolemFOFtoCNF_U $_693 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_696 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_696 \/ ~man skolemFOFtoCNF_U $_692 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_693 $_692 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_696 skolemFOFtoCNF_X4 \/ ~present $_698 $_699 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_697 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_698 \/ ~smoke $_698 $_699 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_697 $_698 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_697 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_693 \/
% 0.97/1.14     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_695 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_694 $_692 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_692 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_X2 $_699 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_694 \/ ~event skolemFOFtoCNF_X2 $_699 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_693 \/ ~forename skolemFOFtoCNF_U $_696 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_696 \/ ~man skolemFOFtoCNF_U $_692 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_693 $_692 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_696 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_694 \/ ~present skolemFOFtoCNF_X2 $_699 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_695 \/ ~smoke skolemFOFtoCNF_X2 $_699 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_694 $_695 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_694 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_693 \/
% 0.97/1.14     man $_695 (skolemFOFtoCNF_X24 $_695)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_695 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_694 $_692 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_692 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_X7 $_699 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_694 \/ ~event skolemFOFtoCNF_X7 $_699 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_693 \/ ~forename skolemFOFtoCNF_U $_696 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_696 \/ ~man skolemFOFtoCNF_U $_692 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_693 $_692 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_696 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_694 \/ ~present skolemFOFtoCNF_X7 $_699 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_695 \/ ~smoke skolemFOFtoCNF_X7 $_699 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_694 $_695 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_694 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_693 \/
% 0.97/1.14     man $_695 (skolemFOFtoCNF_X24 $_695)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_754 \/
% 0.97/1.14     ~accessible_world skolemFOFtoCNF_U $_759 \/
% 0.97/1.14     ~agent $_759 $_760 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_753 $_751 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_758 skolemFOFtoCNF_X4 \/ ~event $_759 $_760 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_753 \/ ~event skolemFOFtoCNF_U $_758 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_752 \/ ~forename skolemFOFtoCNF_U $_755 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_755 \/ ~man skolemFOFtoCNF_U $_751 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_752 $_751 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_755 skolemFOFtoCNF_X4 \/ ~present $_759 $_760 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_753 \/ ~present skolemFOFtoCNF_U $_758 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_754 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_759 \/ ~smoke $_759 $_760 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_753 $_754 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_758 $_759 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_753 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_758 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_752 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_755 \/
% 0.97/1.14     man $_754 (skolemFOFtoCNF_X24 $_754)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_767 \/
% 0.97/1.14     ~agent $_767 $_768 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_766 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_761 \/ ~event $_767 $_768 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_766 \/ ~forename skolemFOFtoCNF_U $_762 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_765 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_765 \/ ~man skolemFOFtoCNF_U $_761 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_762 $_761 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_765 skolemFOFtoCNF_X4 \/ ~present $_767 $_768 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_766 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_767 \/ ~smoke $_767 $_768 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_766 $_767 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_766 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_762 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_765 \/
% 0.97/1.14     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_767 \/
% 0.97/1.14     ~agent $_767 $_768 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_766 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_761 \/ ~event $_767 $_768 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_766 \/ ~forename skolemFOFtoCNF_U $_762 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_765 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_765 \/ ~man skolemFOFtoCNF_U $_761 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_762 $_761 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_765 skolemFOFtoCNF_X4 \/ ~present $_767 $_768 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_766 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_767 \/ ~smoke $_767 $_768 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_766 $_767 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_766 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_762 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_765 \/
% 0.97/1.14     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_764 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_763 $_761 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_X2 $_768 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_763 \/ ~event skolemFOFtoCNF_X2 $_768 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_762 \/ ~forename skolemFOFtoCNF_U $_765 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_765 \/ ~man skolemFOFtoCNF_U $_761 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_762 $_761 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_765 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_763 \/ ~present skolemFOFtoCNF_X2 $_768 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_764 \/ ~smoke skolemFOFtoCNF_X2 $_768 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_763 $_764 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_763 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_762 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_765 \/
% 0.97/1.14     man $_764 (skolemFOFtoCNF_X24 $_764)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_764 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_763 $_761 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_X7 $_768 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_763 \/ ~event skolemFOFtoCNF_X7 $_768 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_762 \/ ~forename skolemFOFtoCNF_U $_765 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_765 \/ ~man skolemFOFtoCNF_U $_761 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_762 $_761 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_765 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_763 \/ ~present skolemFOFtoCNF_X7 $_768 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_764 \/ ~smoke skolemFOFtoCNF_X7 $_768 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_763 $_764 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_763 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_762 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_765 \/
% 0.97/1.14     man $_764 (skolemFOFtoCNF_X24 $_764)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_811 \/
% 0.97/1.14     ~accessible_world skolemFOFtoCNF_U $_816 \/
% 0.97/1.14     ~agent $_816 $_817 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_810 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_815 $_808 \/ ~event $_816 $_817 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_810 \/ ~event skolemFOFtoCNF_U $_815 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_809 \/ ~forename skolemFOFtoCNF_U $_812 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_812 \/ ~man skolemFOFtoCNF_U $_808 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_809 $_808 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_812 skolemFOFtoCNF_X4 \/ ~present $_816 $_817 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_810 \/ ~present skolemFOFtoCNF_U $_815 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_811 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_816 \/ ~smoke $_816 $_817 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_810 $_811 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_815 $_816 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_810 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_815 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_809 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_812 \/
% 0.97/1.14     man $_811 (skolemFOFtoCNF_X24 $_811)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_824 \/
% 0.97/1.14     ~agent $_824 $_825 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_823 $_818 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~event $_824 $_825 \/ ~event skolemFOFtoCNF_U $_823 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_819 \/ ~forename skolemFOFtoCNF_U $_822 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_822 \/ ~man skolemFOFtoCNF_U $_818 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_819 $_818 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_822 skolemFOFtoCNF_X4 \/ ~present $_824 $_825 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_823 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_824 \/ ~smoke $_824 $_825 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_823 $_824 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_823 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_819 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_822 \/
% 0.97/1.14     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_824 \/
% 0.97/1.14     ~agent $_824 $_825 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_823 $_818 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~event $_824 $_825 \/ ~event skolemFOFtoCNF_U $_823 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_819 \/ ~forename skolemFOFtoCNF_U $_822 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_822 \/ ~man skolemFOFtoCNF_U $_818 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_819 $_818 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_822 skolemFOFtoCNF_X4 \/ ~present $_824 $_825 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_823 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_824 \/ ~smoke $_824 $_825 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_823 $_824 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_823 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_819 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_822 \/
% 0.97/1.14     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_821 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_820 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_818 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_X2 $_825 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_820 \/ ~event skolemFOFtoCNF_X2 $_825 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_819 \/ ~forename skolemFOFtoCNF_U $_822 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_822 \/ ~man skolemFOFtoCNF_U $_818 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_819 $_818 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_822 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_820 \/ ~present skolemFOFtoCNF_X2 $_825 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_821 \/ ~smoke skolemFOFtoCNF_X2 $_825 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_820 $_821 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_820 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_819 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_822 \/
% 0.97/1.14     man $_821 (skolemFOFtoCNF_X24 $_821)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_821 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_820 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_818 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_X7 $_825 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_820 \/ ~event skolemFOFtoCNF_X7 $_825 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_819 \/ ~forename skolemFOFtoCNF_U $_822 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_822 \/ ~man skolemFOFtoCNF_U $_818 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_819 $_818 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_822 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_820 \/ ~present skolemFOFtoCNF_X7 $_825 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_821 \/ ~smoke skolemFOFtoCNF_X7 $_825 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_820 $_821 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_820 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_819 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_822 \/
% 0.97/1.14     man $_821 (skolemFOFtoCNF_X24 $_821)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_867 \/
% 0.97/1.14     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.14     ~agent $_867 $_873 (skolemFOFtoCNF_X24 $_867) \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_871 $_864 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_874 skolemFOFtoCNF_X4 \/ ~event $_867 $_873 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_871 \/ ~event skolemFOFtoCNF_U $_874 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_865 \/ ~forename skolemFOFtoCNF_U $_866 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_868 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_868 \/ ~man skolemFOFtoCNF_U $_864 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_865 $_864 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_866 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_868 skolemFOFtoCNF_X4 \/ ~present $_867 $_873 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_871 \/ ~present skolemFOFtoCNF_U $_874 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_867 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_867 $_873 \/
% 0.97/1.14     ~smoke skolemFOFtoCNF_U $_874 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_871 skolemFOFtoCNF_U \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_874 $_867 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_871 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_874 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_865 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_866
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_887 \/
% 0.97/1.14     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.14     ~agent $_887 $_892 (skolemFOFtoCNF_X24 $_887) \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_886 $_884 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_893 skolemFOFtoCNF_X4 \/ ~event $_887 $_892 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_886 \/ ~event skolemFOFtoCNF_U $_893 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_883 \/ ~forename skolemFOFtoCNF_U $_885 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_888 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_888 \/ ~man skolemFOFtoCNF_U $_884 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_883 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_885 $_884 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_888 skolemFOFtoCNF_X4 \/ ~present $_887 $_892 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_886 \/ ~present skolemFOFtoCNF_U $_893 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_887 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_887 $_892 \/
% 0.97/1.14     ~smoke skolemFOFtoCNF_U $_893 \/ ~theme skolemFOFtoCNF_U $_886 $_887 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_893 skolemFOFtoCNF_U \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_886 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_893 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_883 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_885
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_910 \/
% 0.97/1.14     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.14     ~agent $_910 $_912 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_909 $_902 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_911 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.14     ~event $_910 $_912 \/ ~event skolemFOFtoCNF_U $_909 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_911 \/ ~forename skolemFOFtoCNF_U $_903 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_904 \/ ~forename skolemFOFtoCNF_U $_906 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_906 \/ ~man skolemFOFtoCNF_U $_902 \/
% 0.97/1.14     ~man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_903 $_902 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_904 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_906 skolemFOFtoCNF_X4 \/ ~present $_910 $_912 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_909 \/ ~present skolemFOFtoCNF_U $_911 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_910 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_910 $_912 \/
% 0.97/1.14     ~smoke skolemFOFtoCNF_U $_911 \/ ~theme skolemFOFtoCNF_U $_909 $_910 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_911 skolemFOFtoCNF_U \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_909 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_911 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_903 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_904
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_929 \/
% 0.97/1.14     ~accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_U \/
% 0.97/1.14     ~agent $_929 $_931 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_924 $_922 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_930 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.14     ~event $_929 $_931 \/ ~event skolemFOFtoCNF_U $_924 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_930 \/ ~forename skolemFOFtoCNF_U $_921 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_923 \/ ~forename skolemFOFtoCNF_U $_926 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_926 \/ ~man skolemFOFtoCNF_U $_922 \/
% 0.97/1.14     ~man skolemFOFtoCNF_U (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_921 (skolemFOFtoCNF_X24 skolemFOFtoCNF_U) \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_923 $_922 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_926 skolemFOFtoCNF_X4 \/ ~present $_929 $_931 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_924 \/ ~present skolemFOFtoCNF_U $_930 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_929 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U skolemFOFtoCNF_U \/ ~smoke $_929 $_931 \/
% 0.97/1.14     ~smoke skolemFOFtoCNF_U $_930 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_924 skolemFOFtoCNF_U \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_930 $_929 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_924 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_930 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_921 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_923
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_944 \/
% 0.97/1.14     ~accessible_world skolemFOFtoCNF_U $_949 \/
% 0.97/1.14     ~agent $_944 $_950 (skolemFOFtoCNF_X24 $_944) \/
% 0.97/1.14     ~agent $_949 $_951 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_943 $_941 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_948 $_941 \/ ~event $_944 $_950 \/
% 0.97/1.14     ~event $_949 $_951 \/ ~event skolemFOFtoCNF_U $_943 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_948 \/ ~forename skolemFOFtoCNF_U $_942 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_945 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_945 \/ ~man skolemFOFtoCNF_U $_941 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_942 $_941 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_945 skolemFOFtoCNF_X4 \/ ~present $_944 $_950 \/
% 0.97/1.14     ~present $_949 $_951 \/ ~present skolemFOFtoCNF_U $_943 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_948 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_944 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_949 \/ ~smoke $_944 $_950 \/
% 0.97/1.14     ~smoke $_949 $_951 \/ ~theme skolemFOFtoCNF_U $_943 $_944 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_948 $_949 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_943 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_948 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_942
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_965 \/
% 0.97/1.14     ~accessible_world skolemFOFtoCNF_U $_970 \/
% 0.97/1.14     ~agent $_965 $_971 (skolemFOFtoCNF_X24 $_965) \/
% 0.97/1.14     ~agent $_970 $_972 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_964 $_962 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_969 skolemFOFtoCNF_X4 \/ ~event $_965 $_971 \/
% 0.97/1.14     ~event $_970 $_972 \/ ~event skolemFOFtoCNF_U $_964 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_969 \/ ~forename skolemFOFtoCNF_U $_963 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_966 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_966 \/ ~man skolemFOFtoCNF_U $_962 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_963 $_962 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_966 skolemFOFtoCNF_X4 \/ ~present $_965 $_971 \/
% 0.97/1.14     ~present $_970 $_972 \/ ~present skolemFOFtoCNF_U $_964 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_969 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_965 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_970 \/ ~smoke $_965 $_971 \/
% 0.97/1.14     ~smoke $_970 $_972 \/ ~theme skolemFOFtoCNF_U $_964 $_965 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_969 $_970 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_964 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_969 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_963 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_966
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_986 \/
% 0.97/1.14     ~accessible_world skolemFOFtoCNF_U $_991 \/
% 0.97/1.14     ~agent $_986 $_992 (skolemFOFtoCNF_X24 $_986) \/
% 0.97/1.14     ~agent $_991 $_993 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_985 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_990 $_983 \/ ~event $_986 $_992 \/
% 0.97/1.14     ~event $_991 $_993 \/ ~event skolemFOFtoCNF_U $_985 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_990 \/ ~forename skolemFOFtoCNF_U $_984 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_987 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_987 \/ ~man skolemFOFtoCNF_U $_983 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_984 $_983 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_987 skolemFOFtoCNF_X4 \/ ~present $_986 $_992 \/
% 0.97/1.14     ~present $_991 $_993 \/ ~present skolemFOFtoCNF_U $_985 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_990 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_986 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_991 \/ ~smoke $_986 $_992 \/
% 0.97/1.14     ~smoke $_991 $_993 \/ ~theme skolemFOFtoCNF_U $_985 $_986 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_990 $_991 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_985 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_990 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_984 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_987
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_1009 \/
% 0.97/1.14     ~accessible_world skolemFOFtoCNF_U $_1014 \/
% 0.97/1.14     ~agent $_1014 $_1015 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_1008 $_1006 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_1013 $_1004 \/ ~event $_1014 $_1015 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_1008 \/ ~event skolemFOFtoCNF_U $_1013 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_1005 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_1007 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_1010 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_1010 \/
% 0.97/1.14     ~man skolemFOFtoCNF_U $_1004 \/ ~man skolemFOFtoCNF_U $_1006 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1005 $_1004 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1007 $_1006 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1010 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~present $_1014 $_1015 \/ ~present skolemFOFtoCNF_U $_1008 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_1013 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_1009 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_1014 \/ ~smoke $_1014 $_1015 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_1008 $_1009 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_1013 $_1014 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_1008 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_1013 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_1005 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_1007 \/
% 0.97/1.14     man $_1009 (skolemFOFtoCNF_X24 $_1009)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_1024 \/
% 0.97/1.14     ~agent $_1024 $_1025 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_1023 $_1016 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_1018 \/
% 0.97/1.14     ~event $_1024 $_1025 \/ ~event skolemFOFtoCNF_U $_1023 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_1017 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_1019 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_1022 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_1022 \/
% 0.97/1.14     ~man skolemFOFtoCNF_U $_1016 \/ ~man skolemFOFtoCNF_U $_1018 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1017 $_1016 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1019 $_1018 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1022 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~present $_1024 $_1025 \/ ~present skolemFOFtoCNF_U $_1023 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_1024 \/ ~smoke $_1024 $_1025 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_1023 $_1024 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_1023 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_1017 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_1019 \/
% 0.97/1.14     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_1024 \/
% 0.97/1.14     ~agent $_1024 $_1025 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_1023 $_1016 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_1018 \/
% 0.97/1.14     ~event $_1024 $_1025 \/ ~event skolemFOFtoCNF_U $_1023 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_1017 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_1019 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_1022 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_1022 \/
% 0.97/1.14     ~man skolemFOFtoCNF_U $_1016 \/ ~man skolemFOFtoCNF_U $_1018 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1017 $_1016 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1019 $_1018 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1022 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~present $_1024 $_1025 \/ ~present skolemFOFtoCNF_U $_1023 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_1024 \/ ~smoke $_1024 $_1025 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_1023 $_1024 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_1023 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_1017 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_1019 \/
% 0.97/1.14     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_1021 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_1020 $_1018 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X1 $_1016 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_X2 $_1025 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_1020 \/ ~event skolemFOFtoCNF_X2 $_1025 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_1017 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_1019 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_1022 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_1022 \/
% 0.97/1.14     ~man skolemFOFtoCNF_U $_1016 \/ ~man skolemFOFtoCNF_U $_1018 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1017 $_1016 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1019 $_1018 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1022 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_1020 \/ ~present skolemFOFtoCNF_X2 $_1025 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_1021 \/
% 0.97/1.14     ~smoke skolemFOFtoCNF_X2 $_1025 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_1020 $_1021 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_1020 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_1017 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_1019 \/
% 0.97/1.14     man $_1021 (skolemFOFtoCNF_X24 $_1021)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_1021 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_1020 $_1018 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_1016 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_X7 $_1025 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_1020 \/ ~event skolemFOFtoCNF_X7 $_1025 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_1017 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_1019 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_1022 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_1022 \/
% 0.97/1.14     ~man skolemFOFtoCNF_U $_1016 \/ ~man skolemFOFtoCNF_U $_1018 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1017 $_1016 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1019 $_1018 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1022 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_1020 \/ ~present skolemFOFtoCNF_X7 $_1025 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_1021 \/
% 0.97/1.14     ~smoke skolemFOFtoCNF_X7 $_1025 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_1020 $_1021 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_1020 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_1017 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_1019 \/
% 0.97/1.14     man $_1021 (skolemFOFtoCNF_X24 $_1021)
% 0.97/1.14  |- ~agent skolemFOFtoCNF_X7 $_1045 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~event skolemFOFtoCNF_X7 $_1045 \/ ~present skolemFOFtoCNF_X7 $_1045 \/
% 0.97/1.14     ~smoke skolemFOFtoCNF_X7 $_1045 \/
% 0.97/1.14     man skolemFOFtoCNF_X2 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X2)
% 0.97/1.14  |- ~agent skolemFOFtoCNF_X2 $_1066 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~event skolemFOFtoCNF_X2 $_1066 \/ ~present skolemFOFtoCNF_X2 $_1066 \/
% 0.97/1.14     ~smoke skolemFOFtoCNF_X2 $_1066 \/
% 0.97/1.14     man skolemFOFtoCNF_X7 (skolemFOFtoCNF_X24 skolemFOFtoCNF_X7)
% 0.97/1.14  |- ~accessible_world skolemFOFtoCNF_U $_1090 \/
% 0.97/1.14     ~accessible_world skolemFOFtoCNF_U $_1095 \/
% 0.97/1.14     ~agent $_1090 $_1096 (skolemFOFtoCNF_X24 $_1090) \/
% 0.97/1.14     ~agent $_1095 $_1097 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_1089 $_1087 \/
% 0.97/1.14     ~agent skolemFOFtoCNF_U $_1094 $_1085 \/ ~event $_1090 $_1096 \/
% 0.97/1.14     ~event $_1095 $_1097 \/ ~event skolemFOFtoCNF_U $_1089 \/
% 0.97/1.14     ~event skolemFOFtoCNF_U $_1094 \/ ~forename skolemFOFtoCNF_U $_1086 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_1088 \/
% 0.97/1.14     ~forename skolemFOFtoCNF_U $_1091 \/
% 0.97/1.14     ~jules_forename skolemFOFtoCNF_U $_1091 \/
% 0.97/1.14     ~man skolemFOFtoCNF_U $_1085 \/ ~man skolemFOFtoCNF_U $_1087 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1086 $_1085 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1088 $_1087 \/
% 0.97/1.14     ~of skolemFOFtoCNF_U $_1091 skolemFOFtoCNF_X4 \/
% 0.97/1.14     ~present $_1090 $_1096 \/ ~present $_1095 $_1097 \/
% 0.97/1.14     ~present skolemFOFtoCNF_U $_1089 \/ ~present skolemFOFtoCNF_U $_1094 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_1090 \/
% 0.97/1.14     ~proposition skolemFOFtoCNF_U $_1095 \/ ~smoke $_1090 $_1096 \/
% 0.97/1.14     ~smoke $_1095 $_1097 \/ ~theme skolemFOFtoCNF_U $_1089 $_1090 \/
% 0.97/1.14     ~theme skolemFOFtoCNF_U $_1094 $_1095 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_1089 \/
% 0.97/1.14     ~think_believe_consider skolemFOFtoCNF_U $_1094 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_1086 \/
% 0.97/1.14     ~vincent_forename skolemFOFtoCNF_U $_1088
% 0.97/1.14  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.97/1.14  
%------------------------------------------------------------------------------