Metis---2.4.CSA-Sat.s

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

% Computer : n012.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:14 EDT 2022

% Result   : CounterSatisfiable 0.52s 0.71s
% Output   : Saturation 0.52s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : NLP221+1 : TPTP v8.1.0. Released v2.4.0.
% 0.03/0.12  % Command  : metis --show proof --show saturation %s
% 0.12/0.33  % Computer : n012.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33  % CPULimit : 300
% 0.12/0.33  % WCLimit  : 600
% 0.12/0.33  % DateTime : Thu Jun 30 20:49:32 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 0.12/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.52/0.71  % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.52/0.71  
% 0.52/0.71  SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.52/0.71  |- ~definitionFOFtoCNF_0 $X3 $Z \/ man $Z $X3
% 0.52/0.71  |- ~man $Z $X3 \/ agent $Z (skolemFOFtoCNF_X4_1 $X3 $Z) $X3 \/
% 0.52/0.71     definitionFOFtoCNF_0 $X3 $Z
% 0.52/0.71  |- ~man $Z $X3 \/ definitionFOFtoCNF_0 $X3 $Z \/
% 0.52/0.71     event $Z (skolemFOFtoCNF_X4_1 $X3 $Z)
% 0.52/0.71  |- ~man $Z $X3 \/ definitionFOFtoCNF_0 $X3 $Z \/
% 0.52/0.71     present $Z (skolemFOFtoCNF_X4_1 $X3 $Z)
% 0.52/0.71  |- ~man $Z $X3 \/ definitionFOFtoCNF_0 $X3 $Z \/
% 0.52/0.71     smoke $Z (skolemFOFtoCNF_X4_1 $X3 $Z)
% 0.52/0.71  |- ~agent $Z $X4 $X3 \/ ~definitionFOFtoCNF_0 $X3 $Z \/ ~event $Z $X4 \/
% 0.52/0.71     ~present $Z $X4 \/ ~smoke $Z $X4
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     accessible_world skolemFOFtoCNF_X5 skolemFOFtoCNF_X11 \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/ actual_world skolemFOFtoCNF_X5 \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     agent skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 skolemFOFtoCNF_X8 \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     be skolemFOFtoCNF_X5 skolemFOFtoCNF_X13 skolemFOFtoCNF_X6
% 0.52/0.72       skolemFOFtoCNF_X12 \/ definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     event skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X7
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X9
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     jules_forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X7
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     man skolemFOFtoCNF_X5 skolemFOFtoCNF_X12
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     man skolemFOFtoCNF_X5 skolemFOFtoCNF_X6
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     man skolemFOFtoCNF_X5 skolemFOFtoCNF_X8
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     of skolemFOFtoCNF_X5 skolemFOFtoCNF_X7 skolemFOFtoCNF_X6
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     of skolemFOFtoCNF_X5 skolemFOFtoCNF_X9 skolemFOFtoCNF_X8
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     present skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     proposition skolemFOFtoCNF_X5 skolemFOFtoCNF_X11
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     state skolemFOFtoCNF_X5 skolemFOFtoCNF_X13
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     theme skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 skolemFOFtoCNF_X11
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     think_believe_consider skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     vincent_forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X9
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~man skolemFOFtoCNF_X11 $X14 \/ ~of $U $V $W \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     agent skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $X14) $X14 \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~man skolemFOFtoCNF_X11 $X14 \/ ~of $U $V $W \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     event skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $X14)
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~man skolemFOFtoCNF_X11 $X14 \/ ~of $U $V $W \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     present skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $X14)
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~man skolemFOFtoCNF_X11 $X14 \/ ~of $U $V $W \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     smoke skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $X14)
% 0.52/0.72  |- actual_world skolemFOFtoCNF_X5_1
% 0.52/0.72  |- accessible_world skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X11_1
% 0.52/0.72  |- agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X8_1
% 0.52/0.72  |- be skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X13_1 skolemFOFtoCNF_X6_1
% 0.52/0.72       skolemFOFtoCNF_X12_1
% 0.52/0.72  |- event skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1
% 0.52/0.72  |- forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1
% 0.52/0.72  |- forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X9_1
% 0.52/0.72  |- jules_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1
% 0.52/0.72  |- man skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X12_1
% 0.52/0.72  |- man skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X6_1
% 0.52/0.72  |- man skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X8_1
% 0.52/0.72  |- of skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 skolemFOFtoCNF_X6_1
% 0.52/0.72  |- of skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X9_1 skolemFOFtoCNF_X8_1
% 0.52/0.72  |- present skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1
% 0.52/0.72  |- proposition skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X11_1
% 0.52/0.72  |- state skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X13_1
% 0.52/0.72  |- theme skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X11_1
% 0.52/0.72  |- think_believe_consider skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1
% 0.52/0.72  |- vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X9_1
% 0.52/0.72  |- ~man skolemFOFtoCNF_X11_1 $X14 \/
% 0.52/0.72     agent skolemFOFtoCNF_X11_1 (skolemFOFtoCNF_X15_1 $X14) $X14
% 0.52/0.72  |- ~man skolemFOFtoCNF_X11_1 $X14 \/
% 0.52/0.72     event skolemFOFtoCNF_X11_1 (skolemFOFtoCNF_X15_1 $X14)
% 0.52/0.72  |- ~man skolemFOFtoCNF_X11_1 $X14 \/
% 0.52/0.72     present skolemFOFtoCNF_X11_1 (skolemFOFtoCNF_X15_1 $X14)
% 0.52/0.72  |- ~man skolemFOFtoCNF_X11_1 $X14 \/
% 0.52/0.72     smoke skolemFOFtoCNF_X11_1 (skolemFOFtoCNF_X15_1 $X14)
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $V \/
% 0.52/0.72     ~forename $U $X \/ ~jules_forename $U $V \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~of $U $V $W \/ ~of $U $X $W \/ ~present $U $Y \/ ~proposition $U $Z \/
% 0.52/0.72     ~state $U $X2 \/ ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3_1 $Z) $Z
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3_1 $Z) $Z
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     accessible_world skolemFOFtoCNF_X5 skolemFOFtoCNF_X11 \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/ actual_world skolemFOFtoCNF_X5 \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     agent skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 skolemFOFtoCNF_X8 \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     be skolemFOFtoCNF_X5 skolemFOFtoCNF_X13 skolemFOFtoCNF_X6
% 0.52/0.72       skolemFOFtoCNF_X12 \/ definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     event skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X7
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X9
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     jules_forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X7
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     man skolemFOFtoCNF_X5 skolemFOFtoCNF_X12
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     man skolemFOFtoCNF_X5 skolemFOFtoCNF_X6
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     man skolemFOFtoCNF_X5 skolemFOFtoCNF_X8
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     of skolemFOFtoCNF_X5 skolemFOFtoCNF_X7 skolemFOFtoCNF_X6
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     of skolemFOFtoCNF_X5 skolemFOFtoCNF_X9 skolemFOFtoCNF_X8
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     present skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     proposition skolemFOFtoCNF_X5 skolemFOFtoCNF_X11
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     state skolemFOFtoCNF_X5 skolemFOFtoCNF_X13
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     theme skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 skolemFOFtoCNF_X11
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     think_believe_consider skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $X $W \/
% 0.52/0.72     ~present $U $Y \/ ~proposition $U $Z \/ ~state $U $X2 \/
% 0.52/0.72     ~theme $U $Y $Z \/ ~think_believe_consider $U $Y \/
% 0.52/0.72     ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     vincent_forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X9
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~man skolemFOFtoCNF_X11 $X14 \/ ~of $U $X $W \/ ~present $U $Y \/
% 0.52/0.72     ~proposition $U $Z \/ ~state $U $X2 \/ ~theme $U $Y $Z \/
% 0.52/0.72     ~think_believe_consider $U $Y \/ ~vincent_forename $U $X \/
% 0.52/0.72     agent skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $X14) $X14 \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~man skolemFOFtoCNF_X11 $X14 \/ ~of $U $X $W \/ ~present $U $Y \/
% 0.52/0.72     ~proposition $U $Z \/ ~state $U $X2 \/ ~theme $U $Y $Z \/
% 0.52/0.72     ~think_believe_consider $U $Y \/ ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     event skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $X14)
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~man skolemFOFtoCNF_X11 $X14 \/ ~of $U $X $W \/ ~present $U $Y \/
% 0.52/0.72     ~proposition $U $Z \/ ~state $U $X2 \/ ~theme $U $Y $Z \/
% 0.52/0.72     ~think_believe_consider $U $Y \/ ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     present skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $X14)
% 0.52/0.72  |- ~accessible_world $U $Z \/ ~actual_world $U \/ ~agent $U $Y $W \/
% 0.52/0.72     ~be $U $X2 $W $X1 \/ ~event $U $Y \/ ~forename $U $X \/
% 0.52/0.72     ~jules_forename $U $X \/ ~man $U $W \/ ~man $U $X1 \/
% 0.52/0.72     ~man skolemFOFtoCNF_X11 $X14 \/ ~of $U $X $W \/ ~present $U $Y \/
% 0.52/0.72     ~proposition $U $Z \/ ~state $U $X2 \/ ~theme $U $Y $Z \/
% 0.52/0.72     ~think_believe_consider $U $Y \/ ~vincent_forename $U $X \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Z) $Z \/
% 0.52/0.72     smoke skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $X14)
% 0.52/0.72  |- definitionFOFtoCNF_0 skolemFOFtoCNF_X12_1 skolemFOFtoCNF_X5_1 \/
% 0.52/0.72     event skolemFOFtoCNF_X5_1
% 0.52/0.72       (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X12_1 skolemFOFtoCNF_X5_1)
% 0.52/0.72  |- definitionFOFtoCNF_0 skolemFOFtoCNF_X6_1 skolemFOFtoCNF_X5_1 \/
% 0.52/0.72     event skolemFOFtoCNF_X5_1
% 0.52/0.72       (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X6_1 skolemFOFtoCNF_X5_1)
% 0.52/0.72  |- definitionFOFtoCNF_0 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1 \/
% 0.52/0.72     event skolemFOFtoCNF_X5_1
% 0.52/0.72       (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1)
% 0.52/0.72  |- definitionFOFtoCNF_0 skolemFOFtoCNF_X12_1 skolemFOFtoCNF_X5_1 \/
% 0.52/0.72     present skolemFOFtoCNF_X5_1
% 0.52/0.72       (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X12_1 skolemFOFtoCNF_X5_1)
% 0.52/0.72  |- definitionFOFtoCNF_0 skolemFOFtoCNF_X6_1 skolemFOFtoCNF_X5_1 \/
% 0.52/0.72     present skolemFOFtoCNF_X5_1
% 0.52/0.72       (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X6_1 skolemFOFtoCNF_X5_1)
% 0.52/0.72  |- definitionFOFtoCNF_0 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1 \/
% 0.52/0.72     present skolemFOFtoCNF_X5_1
% 0.52/0.72       (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1)
% 0.52/0.72  |- definitionFOFtoCNF_0 skolemFOFtoCNF_X12_1 skolemFOFtoCNF_X5_1 \/
% 0.52/0.72     smoke skolemFOFtoCNF_X5_1
% 0.52/0.72       (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X12_1 skolemFOFtoCNF_X5_1)
% 0.52/0.72  |- definitionFOFtoCNF_0 skolemFOFtoCNF_X6_1 skolemFOFtoCNF_X5_1 \/
% 0.52/0.72     smoke skolemFOFtoCNF_X5_1
% 0.52/0.72       (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X6_1 skolemFOFtoCNF_X5_1)
% 0.52/0.72  |- definitionFOFtoCNF_0 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1 \/
% 0.52/0.72     smoke skolemFOFtoCNF_X5_1
% 0.52/0.72       (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1)
% 0.52/0.72  |- agent skolemFOFtoCNF_X5_1
% 0.52/0.72       (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X12_1 skolemFOFtoCNF_X5_1)
% 0.52/0.72       skolemFOFtoCNF_X12_1 \/
% 0.52/0.72     definitionFOFtoCNF_0 skolemFOFtoCNF_X12_1 skolemFOFtoCNF_X5_1
% 0.52/0.72  |- agent skolemFOFtoCNF_X5_1
% 0.52/0.72       (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X6_1 skolemFOFtoCNF_X5_1)
% 0.52/0.72       skolemFOFtoCNF_X6_1 \/
% 0.52/0.72     definitionFOFtoCNF_0 skolemFOFtoCNF_X6_1 skolemFOFtoCNF_X5_1
% 0.52/0.72  |- agent skolemFOFtoCNF_X5_1
% 0.52/0.72       (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1)
% 0.52/0.72       skolemFOFtoCNF_X8_1 \/
% 0.52/0.72     definitionFOFtoCNF_0 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1
% 0.52/0.72  |- ~definitionFOFtoCNF_0 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1 \/
% 0.52/0.72     ~smoke skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1
% 0.52/0.72  |- ~accessible_world skolemFOFtoCNF_X5_1 $_139 \/
% 0.52/0.72     ~agent skolemFOFtoCNF_X5_1 $_138 skolemFOFtoCNF_X6_1 \/
% 0.52/0.72     ~event skolemFOFtoCNF_X5_1 $_138 \/
% 0.52/0.72     ~forename skolemFOFtoCNF_X5_1 $_135 \/
% 0.52/0.72     ~jules_forename skolemFOFtoCNF_X5_1 $_135 \/
% 0.52/0.72     ~of skolemFOFtoCNF_X5_1 $_135 skolemFOFtoCNF_X6_1 \/
% 0.52/0.72     ~present skolemFOFtoCNF_X5_1 $_138 \/
% 0.52/0.72     ~proposition skolemFOFtoCNF_X5_1 $_139 \/
% 0.52/0.72     ~theme skolemFOFtoCNF_X5_1 $_138 $_139 \/
% 0.52/0.72     ~think_believe_consider skolemFOFtoCNF_X5_1 $_138 \/
% 0.52/0.72     ~vincent_forename skolemFOFtoCNF_X5_1 $_135 \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3_1 $_139) $_139
% 0.52/0.72  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.72     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.72     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3_1 skolemFOFtoCNF_X11_1)
% 0.52/0.72       skolemFOFtoCNF_X11_1
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_150 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_149 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_149 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_146 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_146 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_146 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_149 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_150 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_149 $_150 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_149 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_146 \/
% 0.52/0.73     actual_world skolemFOFtoCNF_X5 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_150) $_150
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     actual_world skolemFOFtoCNF_X5 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_161 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_160 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_160 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_157 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_157 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_157 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_160 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_161 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_160 $_161 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_160 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_157 \/
% 0.52/0.73     accessible_world skolemFOFtoCNF_X5 skolemFOFtoCNF_X11 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_161) $_161
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     accessible_world skolemFOFtoCNF_X5 skolemFOFtoCNF_X11 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_172 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_171 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_171 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_168 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_168 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_168 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_171 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_172 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_171 $_172 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_171 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_168 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_172) $_172 \/
% 0.52/0.73     event skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/ event skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_183 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_182 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_182 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_179 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_179 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_179 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_182 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_183 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_182 $_183 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_182 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_179 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_183) $_183 \/
% 0.52/0.73     proposition skolemFOFtoCNF_X5 skolemFOFtoCNF_X11
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/
% 0.52/0.73     proposition skolemFOFtoCNF_X5 skolemFOFtoCNF_X11
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_194 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_193 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_193 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_190 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_190 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_190 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_193 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_194 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_193 $_194 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_193 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_190 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_194) $_194 \/
% 0.52/0.73     man skolemFOFtoCNF_X5 skolemFOFtoCNF_X6
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/ man skolemFOFtoCNF_X5 skolemFOFtoCNF_X6
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_205 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_204 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_204 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_201 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_201 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_201 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_204 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_205 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_204 $_205 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_204 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_201 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_205) $_205 \/
% 0.52/0.73     jules_forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X7
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/
% 0.52/0.73     jules_forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X7
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_216 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_215 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_215 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_212 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_212 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_212 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_215 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_216 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_215 $_216 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_215 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_212 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_216) $_216 \/
% 0.52/0.73     vincent_forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X9
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/
% 0.52/0.73     vincent_forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X9
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_227 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_226 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_226 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_223 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_223 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_223 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_226 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_227 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_226 $_227 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_226 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_223 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_227) $_227 \/
% 0.52/0.73     forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X9
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/ forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X9
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_238 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_237 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_237 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_234 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_234 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_234 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_237 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_238 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_237 $_238 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_237 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_234 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_238) $_238 \/
% 0.52/0.73     man skolemFOFtoCNF_X5 skolemFOFtoCNF_X8
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/ man skolemFOFtoCNF_X5 skolemFOFtoCNF_X8
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_249 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_248 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_248 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_245 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_245 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_245 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_248 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_249 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_248 $_249 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_248 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_245 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_249) $_249 \/
% 0.52/0.73     man skolemFOFtoCNF_X5 skolemFOFtoCNF_X12
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/ man skolemFOFtoCNF_X5 skolemFOFtoCNF_X12
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_260 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_259 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_259 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_256 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_256 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_256 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_259 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_260 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_259 $_260 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_259 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_256 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_260) $_260 \/
% 0.52/0.73     present skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/ present skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_271 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_270 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_270 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_267 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_267 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_267 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_270 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_271 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_270 $_271 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_270 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_267 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_271) $_271 \/
% 0.52/0.73     forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X7
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/ forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X7
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_282 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_281 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_281 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_278 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_278 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_278 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_281 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_282 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_281 $_282 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_281 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_278 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_282) $_282 \/
% 0.52/0.73     think_believe_consider skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/
% 0.52/0.73     think_believe_consider skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_293 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_292 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_292 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_289 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_289 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_289 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_292 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_293 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_292 $_293 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_292 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_289 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_293) $_293 \/
% 0.52/0.73     state skolemFOFtoCNF_X5 skolemFOFtoCNF_X13
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/ state skolemFOFtoCNF_X5 skolemFOFtoCNF_X13
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_304 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_303 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_303 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_300 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_300 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_300 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_303 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_304 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_303 $_304 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_303 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_300 \/
% 0.52/0.73     agent skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 skolemFOFtoCNF_X8 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_304) $_304
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     agent skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 skolemFOFtoCNF_X8 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_315 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_314 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_314 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_311 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_311 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_311 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_314 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_315 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_314 $_315 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_314 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_311 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_315) $_315 \/
% 0.52/0.73     of skolemFOFtoCNF_X5 skolemFOFtoCNF_X7 skolemFOFtoCNF_X6
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/
% 0.52/0.73     of skolemFOFtoCNF_X5 skolemFOFtoCNF_X7 skolemFOFtoCNF_X6
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_326 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_325 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_325 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_322 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_322 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_322 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_325 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_326 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_325 $_326 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_325 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_322 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_326) $_326 \/
% 0.52/0.73     of skolemFOFtoCNF_X5 skolemFOFtoCNF_X9 skolemFOFtoCNF_X8
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/
% 0.52/0.73     of skolemFOFtoCNF_X5 skolemFOFtoCNF_X9 skolemFOFtoCNF_X8
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_337 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_336 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_336 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_333 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_333 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_333 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_336 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_337 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_336 $_337 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_336 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_333 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_337) $_337 \/
% 0.52/0.73     theme skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 skolemFOFtoCNF_X11
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/
% 0.52/0.73     theme skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 skolemFOFtoCNF_X11
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_348 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_347 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_347 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_344 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_344 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_344 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_347 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_348 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_347 $_348 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_347 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_344 \/
% 0.52/0.73     be skolemFOFtoCNF_X5 skolemFOFtoCNF_X13 skolemFOFtoCNF_X6
% 0.52/0.73       skolemFOFtoCNF_X12 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_348) $_348
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     be skolemFOFtoCNF_X5 skolemFOFtoCNF_X13 skolemFOFtoCNF_X6
% 0.52/0.73       skolemFOFtoCNF_X12 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_360 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_359 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_359 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_354 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_356 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_354 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_354 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_356 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_359 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_360 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_359 $_360 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_359 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_356 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3_1 $_360) $_360
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_366 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_366 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_366 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3_1 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_375 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_374 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_374 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_370 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_370 \/
% 0.52/0.73     ~man skolemFOFtoCNF_X11 $_372 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_370 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_374 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_375 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_374 $_375 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_374 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_370 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_375) $_375 \/
% 0.52/0.73     event skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $_372)
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~man skolemFOFtoCNF_X11 $_381 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/
% 0.52/0.73     event skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $_381)
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_390 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_389 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_389 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_385 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_385 \/
% 0.52/0.73     ~man skolemFOFtoCNF_X11 $_387 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_385 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_389 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_390 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_389 $_390 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_389 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_385 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_390) $_390 \/
% 0.52/0.73     present skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $_387)
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~man skolemFOFtoCNF_X11 $_396 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/
% 0.52/0.73     present skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $_396)
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_405 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_404 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_404 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_400 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_400 \/
% 0.52/0.73     ~man skolemFOFtoCNF_X11 $_402 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_400 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_404 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_405 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_404 $_405 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_404 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_400 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_405) $_405 \/
% 0.52/0.73     smoke skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $_402)
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~man skolemFOFtoCNF_X11 $_411 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/
% 0.52/0.73     smoke skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $_411)
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_420 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_419 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_419 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_415 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_415 \/
% 0.52/0.73     ~man skolemFOFtoCNF_X11 $_417 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_415 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_419 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_420 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_419 $_420 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_419 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_415 \/
% 0.52/0.73     agent skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $_417) $_417 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_420) $_420
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~man skolemFOFtoCNF_X11 $_426 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 \/
% 0.52/0.73     agent skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $_426) $_426 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_435 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_434 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_434 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_429 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_431 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_429 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_429 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_431 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_434 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_435 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_434 $_435 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_434 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_431 \/
% 0.52/0.73     actual_world skolemFOFtoCNF_X5 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_435) $_435
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_441 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_441 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_441 \/
% 0.52/0.73     actual_world skolemFOFtoCNF_X5 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_450 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_449 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_449 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_444 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_446 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_444 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_444 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_446 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_449 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_450 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_449 $_450 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_449 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_446 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_450) $_450 \/
% 0.52/0.73     event skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_456 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_456 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_456 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/ event skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_465 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_464 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_464 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_459 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_461 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_459 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_459 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_461 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_464 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_465 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_464 $_465 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_464 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_461 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_465) $_465 \/
% 0.52/0.73     forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X9
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_471 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_471 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_471 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/ forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X9
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_480 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_479 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_479 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_474 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_476 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_474 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_474 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_476 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_479 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_480 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_479 $_480 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_479 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_476 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_480) $_480 \/
% 0.52/0.73     jules_forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X7
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_486 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_486 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_486 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/
% 0.52/0.73     jules_forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X7
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_495 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_494 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_494 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_489 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_491 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_489 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_489 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_491 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_494 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_495 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_494 $_495 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_494 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_491 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_495) $_495 \/
% 0.52/0.73     man skolemFOFtoCNF_X5 skolemFOFtoCNF_X12
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_501 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_501 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_501 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/ man skolemFOFtoCNF_X5 skolemFOFtoCNF_X12
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_510 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_509 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_509 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_504 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_506 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_504 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_504 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_506 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_509 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_510 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_509 $_510 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_509 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_506 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_510) $_510 \/
% 0.52/0.73     forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X7
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_516 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_516 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_516 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/ forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X7
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_525 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_524 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_524 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_519 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_521 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_519 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_519 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_521 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_524 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_525 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_524 $_525 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_524 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_521 \/
% 0.52/0.73     accessible_world skolemFOFtoCNF_X5 skolemFOFtoCNF_X11 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_525) $_525
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_531 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_531 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_531 \/
% 0.52/0.73     accessible_world skolemFOFtoCNF_X5 skolemFOFtoCNF_X11 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_540 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_539 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_539 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_534 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_536 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_534 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_534 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_536 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_539 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_540 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_539 $_540 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_539 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_536 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_540) $_540 \/
% 0.52/0.73     state skolemFOFtoCNF_X5 skolemFOFtoCNF_X13
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_546 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_546 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_546 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/ state skolemFOFtoCNF_X5 skolemFOFtoCNF_X13
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_555 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_554 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_554 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_549 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_551 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_549 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_549 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_551 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_554 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_555 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_554 $_555 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_554 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_551 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_555) $_555 \/
% 0.52/0.73     present skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_561 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_561 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_561 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/ present skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_570 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_569 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_569 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_564 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_566 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_564 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_564 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_566 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_569 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_570 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_569 $_570 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_569 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_566 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_570) $_570 \/
% 0.52/0.73     man skolemFOFtoCNF_X5 skolemFOFtoCNF_X6
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_576 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_576 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_576 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/ man skolemFOFtoCNF_X5 skolemFOFtoCNF_X6
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_585 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_584 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_584 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_579 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_581 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_579 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_579 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_581 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_584 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_585 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_584 $_585 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_584 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_581 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_585) $_585 \/
% 0.52/0.73     proposition skolemFOFtoCNF_X5 skolemFOFtoCNF_X11
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_591 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_591 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_591 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/
% 0.52/0.73     proposition skolemFOFtoCNF_X5 skolemFOFtoCNF_X11
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_600 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_599 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_599 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_594 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_596 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_594 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_594 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_596 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_599 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_600 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_599 $_600 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_599 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_596 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_600) $_600 \/
% 0.52/0.73     man skolemFOFtoCNF_X5 skolemFOFtoCNF_X8
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_606 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_606 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_606 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/ man skolemFOFtoCNF_X5 skolemFOFtoCNF_X8
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_615 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_614 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_614 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_609 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_611 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_609 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_609 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_611 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_614 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_615 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_614 $_615 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_614 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_611 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_615) $_615 \/
% 0.52/0.73     think_believe_consider skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_621 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_621 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_621 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/
% 0.52/0.73     think_believe_consider skolemFOFtoCNF_X5 skolemFOFtoCNF_X10
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_630 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_629 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_629 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_624 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_626 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_624 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_624 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_626 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_629 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_630 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_629 $_630 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_629 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_626 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_630) $_630 \/
% 0.52/0.73     vincent_forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X9
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_636 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_636 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_636 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/
% 0.52/0.73     vincent_forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X9
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_645 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_644 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_644 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_639 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_641 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_639 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_639 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_641 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_644 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_645 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_644 $_645 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_644 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_641 \/
% 0.52/0.73     agent skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 skolemFOFtoCNF_X8 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_645) $_645
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_651 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_651 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_651 \/
% 0.52/0.73     agent skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 skolemFOFtoCNF_X8 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_660 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_659 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_659 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_654 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_656 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_654 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_654 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_656 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_659 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_660 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_659 $_660 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_659 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_656 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_660) $_660 \/
% 0.52/0.73     theme skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 skolemFOFtoCNF_X11
% 0.52/0.73  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_666 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_666 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_666 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.73       skolemFOFtoCNF_X11_1 \/
% 0.52/0.73     theme skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 skolemFOFtoCNF_X11
% 0.52/0.73  |- ~accessible_world skolemFOFtoCNF_X5_1 $_675 \/
% 0.52/0.73     ~agent skolemFOFtoCNF_X5_1 $_674 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~event skolemFOFtoCNF_X5_1 $_674 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_669 \/
% 0.52/0.73     ~forename skolemFOFtoCNF_X5_1 $_671 \/
% 0.52/0.73     ~jules_forename skolemFOFtoCNF_X5_1 $_669 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_669 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~of skolemFOFtoCNF_X5_1 $_671 skolemFOFtoCNF_X6_1 \/
% 0.52/0.73     ~present skolemFOFtoCNF_X5_1 $_674 \/
% 0.52/0.73     ~proposition skolemFOFtoCNF_X5_1 $_675 \/
% 0.52/0.73     ~theme skolemFOFtoCNF_X5_1 $_674 $_675 \/
% 0.52/0.73     ~think_believe_consider skolemFOFtoCNF_X5_1 $_674 \/
% 0.52/0.73     ~vincent_forename skolemFOFtoCNF_X5_1 $_671 \/
% 0.52/0.73     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_675) $_675 \/
% 0.52/0.73     of skolemFOFtoCNF_X5 skolemFOFtoCNF_X9 skolemFOFtoCNF_X8
% 0.52/0.74  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_681 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_681 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~vincent_forename skolemFOFtoCNF_X5_1 $_681 \/
% 0.52/0.74     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.74       skolemFOFtoCNF_X11_1 \/
% 0.52/0.74     of skolemFOFtoCNF_X5 skolemFOFtoCNF_X9 skolemFOFtoCNF_X8
% 0.52/0.74  |- ~accessible_world skolemFOFtoCNF_X5_1 $_690 \/
% 0.52/0.74     ~agent skolemFOFtoCNF_X5_1 $_689 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~event skolemFOFtoCNF_X5_1 $_689 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_684 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_686 \/
% 0.52/0.74     ~jules_forename skolemFOFtoCNF_X5_1 $_684 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_684 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_686 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~present skolemFOFtoCNF_X5_1 $_689 \/
% 0.52/0.74     ~proposition skolemFOFtoCNF_X5_1 $_690 \/
% 0.52/0.74     ~theme skolemFOFtoCNF_X5_1 $_689 $_690 \/
% 0.52/0.74     ~think_believe_consider skolemFOFtoCNF_X5_1 $_689 \/
% 0.52/0.74     ~vincent_forename skolemFOFtoCNF_X5_1 $_686 \/
% 0.52/0.74     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_690) $_690 \/
% 0.52/0.74     of skolemFOFtoCNF_X5 skolemFOFtoCNF_X7 skolemFOFtoCNF_X6
% 0.52/0.74  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_696 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_696 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~vincent_forename skolemFOFtoCNF_X5_1 $_696 \/
% 0.52/0.74     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.74       skolemFOFtoCNF_X11_1 \/
% 0.52/0.74     of skolemFOFtoCNF_X5 skolemFOFtoCNF_X7 skolemFOFtoCNF_X6
% 0.52/0.74  |- ~accessible_world skolemFOFtoCNF_X5_1 $_705 \/
% 0.52/0.74     ~agent skolemFOFtoCNF_X5_1 $_704 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~event skolemFOFtoCNF_X5_1 $_704 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_699 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_701 \/
% 0.52/0.74     ~jules_forename skolemFOFtoCNF_X5_1 $_699 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_699 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_701 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~present skolemFOFtoCNF_X5_1 $_704 \/
% 0.52/0.74     ~proposition skolemFOFtoCNF_X5_1 $_705 \/
% 0.52/0.74     ~theme skolemFOFtoCNF_X5_1 $_704 $_705 \/
% 0.52/0.74     ~think_believe_consider skolemFOFtoCNF_X5_1 $_704 \/
% 0.52/0.74     ~vincent_forename skolemFOFtoCNF_X5_1 $_701 \/
% 0.52/0.74     be skolemFOFtoCNF_X5 skolemFOFtoCNF_X13 skolemFOFtoCNF_X6
% 0.52/0.74       skolemFOFtoCNF_X12 \/
% 0.52/0.74     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_705) $_705
% 0.52/0.74  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_711 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_711 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~vincent_forename skolemFOFtoCNF_X5_1 $_711 \/
% 0.52/0.74     be skolemFOFtoCNF_X5 skolemFOFtoCNF_X13 skolemFOFtoCNF_X6
% 0.52/0.74       skolemFOFtoCNF_X12 \/
% 0.52/0.74     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.74       skolemFOFtoCNF_X11_1
% 0.52/0.74  |- ~accessible_world skolemFOFtoCNF_X5_1 $_721 \/
% 0.52/0.74     ~agent skolemFOFtoCNF_X5_1 $_720 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~event skolemFOFtoCNF_X5_1 $_720 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_714 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_716 \/
% 0.52/0.74     ~jules_forename skolemFOFtoCNF_X5_1 $_714 \/
% 0.52/0.74     ~man skolemFOFtoCNF_X11 $_718 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_714 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_716 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~present skolemFOFtoCNF_X5_1 $_720 \/
% 0.52/0.74     ~proposition skolemFOFtoCNF_X5_1 $_721 \/
% 0.52/0.74     ~theme skolemFOFtoCNF_X5_1 $_720 $_721 \/
% 0.52/0.74     ~think_believe_consider skolemFOFtoCNF_X5_1 $_720 \/
% 0.52/0.74     ~vincent_forename skolemFOFtoCNF_X5_1 $_716 \/
% 0.52/0.74     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_721) $_721 \/
% 0.52/0.74     present skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $_718)
% 0.52/0.74  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_728 \/ ~man skolemFOFtoCNF_X11 $_729 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_728 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~vincent_forename skolemFOFtoCNF_X5_1 $_728 \/
% 0.52/0.74     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.74       skolemFOFtoCNF_X11_1 \/
% 0.52/0.74     present skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $_729)
% 0.52/0.74  |- ~accessible_world skolemFOFtoCNF_X5_1 $_740 \/
% 0.52/0.74     ~agent skolemFOFtoCNF_X5_1 $_739 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~event skolemFOFtoCNF_X5_1 $_739 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_733 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_735 \/
% 0.52/0.74     ~jules_forename skolemFOFtoCNF_X5_1 $_733 \/
% 0.52/0.74     ~man skolemFOFtoCNF_X11 $_737 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_733 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_735 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~present skolemFOFtoCNF_X5_1 $_739 \/
% 0.52/0.74     ~proposition skolemFOFtoCNF_X5_1 $_740 \/
% 0.52/0.74     ~theme skolemFOFtoCNF_X5_1 $_739 $_740 \/
% 0.52/0.74     ~think_believe_consider skolemFOFtoCNF_X5_1 $_739 \/
% 0.52/0.74     ~vincent_forename skolemFOFtoCNF_X5_1 $_735 \/
% 0.52/0.74     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_740) $_740 \/
% 0.52/0.74     event skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $_737)
% 0.52/0.74  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_747 \/ ~man skolemFOFtoCNF_X11 $_748 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_747 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~vincent_forename skolemFOFtoCNF_X5_1 $_747 \/
% 0.52/0.74     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.74       skolemFOFtoCNF_X11_1 \/
% 0.52/0.74     event skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $_748)
% 0.52/0.74  |- ~accessible_world skolemFOFtoCNF_X5_1 $_759 \/
% 0.52/0.74     ~agent skolemFOFtoCNF_X5_1 $_758 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~event skolemFOFtoCNF_X5_1 $_758 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_752 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_754 \/
% 0.52/0.74     ~jules_forename skolemFOFtoCNF_X5_1 $_752 \/
% 0.52/0.74     ~man skolemFOFtoCNF_X11 $_756 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_752 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_754 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~present skolemFOFtoCNF_X5_1 $_758 \/
% 0.52/0.74     ~proposition skolemFOFtoCNF_X5_1 $_759 \/
% 0.52/0.74     ~theme skolemFOFtoCNF_X5_1 $_758 $_759 \/
% 0.52/0.74     ~think_believe_consider skolemFOFtoCNF_X5_1 $_758 \/
% 0.52/0.74     ~vincent_forename skolemFOFtoCNF_X5_1 $_754 \/
% 0.52/0.74     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_759) $_759 \/
% 0.52/0.74     smoke skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $_756)
% 0.52/0.74  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_766 \/ ~man skolemFOFtoCNF_X11 $_767 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_766 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~vincent_forename skolemFOFtoCNF_X5_1 $_766 \/
% 0.52/0.74     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.74       skolemFOFtoCNF_X11_1 \/
% 0.52/0.74     smoke skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $_767)
% 0.52/0.74  |- ~accessible_world skolemFOFtoCNF_X5_1 $_778 \/
% 0.52/0.74     ~agent skolemFOFtoCNF_X5_1 $_777 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~event skolemFOFtoCNF_X5_1 $_777 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_771 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_773 \/
% 0.52/0.74     ~jules_forename skolemFOFtoCNF_X5_1 $_771 \/
% 0.52/0.74     ~man skolemFOFtoCNF_X11 $_775 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_771 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_773 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~present skolemFOFtoCNF_X5_1 $_777 \/
% 0.52/0.74     ~proposition skolemFOFtoCNF_X5_1 $_778 \/
% 0.52/0.74     ~theme skolemFOFtoCNF_X5_1 $_777 $_778 \/
% 0.52/0.74     ~think_believe_consider skolemFOFtoCNF_X5_1 $_777 \/
% 0.52/0.74     ~vincent_forename skolemFOFtoCNF_X5_1 $_773 \/
% 0.52/0.74     agent skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $_775) $_775 \/
% 0.52/0.74     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $_778) $_778
% 0.52/0.74  |- ~agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~forename skolemFOFtoCNF_X5_1 $_785 \/ ~man skolemFOFtoCNF_X11 $_786 \/
% 0.52/0.74     ~of skolemFOFtoCNF_X5_1 $_785 skolemFOFtoCNF_X6_1 \/
% 0.52/0.74     ~vincent_forename skolemFOFtoCNF_X5_1 $_785 \/
% 0.52/0.74     agent skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $_786) $_786 \/
% 0.52/0.74     definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 skolemFOFtoCNF_X11_1)
% 0.52/0.74       skolemFOFtoCNF_X11_1
% 0.52/0.74  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.52/0.74  
%------------------------------------------------------------------------------