Metis---2.4.CSA-Sat.s

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

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

% Result   : CounterSatisfiable 0.44s 0.61s
% Output   : Saturation 0.50s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : NLP025+1 : TPTP v8.1.0. Released v2.4.0.
% 0.00/0.13  % Command  : metis --show proof --show saturation %s
% 0.13/0.33  % Computer : n027.cluster.edu
% 0.13/0.33  % Model    : x86_64 x86_64
% 0.13/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33  % Memory   : 8042.1875MB
% 0.13/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33  % CPULimit : 300
% 0.13/0.33  % WCLimit  : 600
% 0.13/0.33  % DateTime : Fri Jul  1 02:42:52 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.13/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.44/0.61  % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.44/0.61  
% 0.44/0.61  SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.44/0.61  |- ~man $U $V \/ male $U $V
% 0.44/0.61  |- ~man $U $V \/ human_person $U $V
% 0.44/0.61  |- ~vincent_forename $U $V \/ forename $U $V
% 0.44/0.61  |- ~woman $U $V \/ female $U $V
% 0.44/0.61  |- ~human_person $U $V \/ animate $U $V
% 0.44/0.61  |- ~human_person $U $V \/ human $U $V
% 0.44/0.61  |- ~organism $U $V \/ living $U $V
% 0.44/0.61  |- ~organism $U $V \/ impartial $U $V
% 0.44/0.61  |- ~entity $U $V \/ existent $U $V
% 0.44/0.61  |- ~entity $U $V \/ specific $U $V
% 0.44/0.61  |- ~entity $U $V \/ thing $U $V
% 0.44/0.61  |- ~organism $U $V \/ entity $U $V
% 0.44/0.61  |- ~human_person $U $V \/ organism $U $V
% 0.44/0.61  |- ~woman $U $V \/ human_person $U $V
% 0.44/0.61  |- ~mia_forename $U $V \/ forename $U $V
% 0.44/0.61  |- ~relname $U $V \/ relation $U $V
% 0.44/0.61  |- ~forename $U $V \/ relname $U $V
% 0.44/0.61  |- ~abstraction $U $V \/ unisex $U $V
% 0.44/0.61  |- ~abstraction $U $V \/ general $U $V
% 0.44/0.61  |- ~abstraction $U $V \/ nonhuman $U $V
% 0.44/0.61  |- ~abstraction $U $V \/ thing $U $V
% 0.44/0.61  |- ~relation $U $V \/ abstraction $U $V
% 0.44/0.61  |- ~proposition $U $V \/ relation $U $V
% 0.44/0.61  |- ~desire_want $U $V \/ event $U $V
% 0.44/0.61  |- ~eventuality $U $V \/ unisex $U $V
% 0.44/0.62  |- ~eventuality $U $V \/ nonexistent $U $V
% 0.44/0.62  |- ~eventuality $U $V \/ specific $U $V
% 0.44/0.62  |- ~thing $U $V \/ singleton $U $V
% 0.44/0.62  |- ~eventuality $U $V \/ thing $U $V
% 0.44/0.62  |- ~event $U $V \/ eventuality $U $V
% 0.44/0.62  |- ~dance $U $V \/ event $U $V
% 0.44/0.62  |- ~existent $U $V \/ ~nonexistent $U $V
% 0.44/0.62  |- ~female $U $V \/ ~male $U $V
% 0.44/0.62  |- ~human $U $V \/ ~nonhuman $U $V
% 0.44/0.62  |- ~general $U $V \/ ~specific $U $V
% 0.44/0.62  |- ~female $U $V \/ ~unisex $U $V
% 0.44/0.62  |- ~male $U $V \/ ~unisex $U $V
% 0.44/0.62  |- ~accessible_world $V $W \/ ~male $V $U \/ male $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~man $V $U \/ man $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~vincent_forename $V $U \/
% 0.44/0.62     vincent_forename $W $U
% 0.44/0.62  |- ~accessible_world $W $X \/ ~of $W $U $V \/ of $X $U $V
% 0.44/0.62  |- ~accessible_world $V $W \/ ~female $V $U \/ female $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~animate $V $U \/ animate $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~human $V $U \/ human $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~living $V $U \/ living $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~impartial $V $U \/ impartial $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~existent $V $U \/ existent $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~entity $V $U \/ entity $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~organism $V $U \/ organism $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~human_person $V $U \/ human_person $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~woman $V $U \/ woman $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~mia_forename $V $U \/ mia_forename $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~relname $V $U \/ relname $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~forename $V $U \/ forename $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~general $V $U \/ general $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~nonhuman $V $U \/ nonhuman $W $U
% 0.44/0.62  |- ~abstraction $V $U \/ ~accessible_world $V $W \/ abstraction $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~relation $V $U \/ relation $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~proposition $V $U \/ proposition $W $U
% 0.44/0.62  |- ~accessible_world $W $X \/ ~theme $W $U $V \/ theme $X $U $V
% 0.44/0.62  |- ~accessible_world $V $W \/ ~desire_want $V $U \/ desire_want $W $U
% 0.44/0.62  |- ~accessible_world $W $X \/ ~agent $W $U $V \/ agent $X $U $V
% 0.44/0.62  |- ~accessible_world $V $W \/ ~present $V $U \/ present $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~unisex $V $U \/ unisex $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~nonexistent $V $U \/ nonexistent $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~specific $V $U \/ specific $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~singleton $V $U \/ singleton $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~thing $V $U \/ thing $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~eventuality $V $U \/ eventuality $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~event $V $U \/ event $W $U
% 0.44/0.62  |- ~accessible_world $V $W \/ ~dance $V $U \/ dance $W $U
% 0.44/0.62  |- ~entity $U $V \/ ~forename $U $W \/ ~forename $U $X \/ ~of $U $W $V \/
% 0.44/0.62     ~of $U $X $V \/ $X = $W
% 0.44/0.62  |- ~desire_want $U $V \/ ~desire_want $U $W \/ ~proposition $U $X \/
% 0.44/0.62     ~proposition $U $Y \/ ~theme $U $V $X \/ ~theme $U $W $Y \/ $X = $Y
% 0.44/0.62  |- actual_world skolemFOFtoCNF_U
% 0.44/0.62  |- accessible_world skolemFOFtoCNF_U skolemFOFtoCNF_X
% 0.44/0.62  |- agent skolemFOFtoCNF_U skolemFOFtoCNF_Y skolemFOFtoCNF_V
% 0.44/0.62  |- desire_want skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.44/0.62  |- forename skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.44/0.62  |- mia_forename skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.44/0.62  |- of skolemFOFtoCNF_U skolemFOFtoCNF_W skolemFOFtoCNF_V
% 0.44/0.62  |- present skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.44/0.62  |- proposition skolemFOFtoCNF_U skolemFOFtoCNF_X
% 0.44/0.62  |- theme skolemFOFtoCNF_U skolemFOFtoCNF_Y skolemFOFtoCNF_X
% 0.44/0.62  |- woman skolemFOFtoCNF_U skolemFOFtoCNF_V
% 0.44/0.62  |- agent skolemFOFtoCNF_X skolemFOFtoCNF_Z skolemFOFtoCNF_V
% 0.44/0.62  |- dance skolemFOFtoCNF_X skolemFOFtoCNF_Z
% 0.44/0.62  |- event skolemFOFtoCNF_X skolemFOFtoCNF_Z
% 0.44/0.62  |- present skolemFOFtoCNF_X skolemFOFtoCNF_Z
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $V \/
% 0.44/0.62     ~agent $X1 $Y $V \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X $Z \/ ~present $X1 $Y \/ ~proposition $X1 $X \/
% 0.44/0.62     ~theme $X1 $Y $X \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     accessible_world $X1 (skolemFOFtoCNF_X4 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $V \/
% 0.44/0.62     ~agent $X1 $Y $V \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X $Z \/ ~present $X1 $Y \/ ~proposition $X1 $X \/
% 0.44/0.62     ~theme $X1 $Y $X \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     agent $X1 (skolemFOFtoCNF_X5 $X1 $X2) $X2
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $V \/
% 0.44/0.62     ~agent $X1 $Y $V \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X $Z \/ ~present $X1 $Y \/ ~proposition $X1 $X \/
% 0.44/0.62     ~theme $X1 $Y $X \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     agent (skolemFOFtoCNF_X4 $X1 $X2) (skolemFOFtoCNF_X6 $X1 $X2) $X2
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $V \/
% 0.44/0.62     ~agent $X1 $Y $V \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X $Z \/ ~present $X1 $Y \/ ~proposition $X1 $X \/
% 0.44/0.62     ~theme $X1 $Y $X \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     dance (skolemFOFtoCNF_X4 $X1 $X2) (skolemFOFtoCNF_X6 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $V \/
% 0.44/0.62     ~agent $X1 $Y $V \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X $Z \/ ~present $X1 $Y \/ ~proposition $X1 $X \/
% 0.44/0.62     ~theme $X1 $Y $X \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     desire_want $X1 (skolemFOFtoCNF_X5 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $V \/
% 0.44/0.62     ~agent $X1 $Y $V \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X $Z \/ ~present $X1 $Y \/ ~proposition $X1 $X \/
% 0.44/0.62     ~theme $X1 $Y $X \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     event (skolemFOFtoCNF_X4 $X1 $X2) (skolemFOFtoCNF_X6 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $V \/
% 0.44/0.62     ~agent $X1 $Y $V \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X $Z \/ ~present $X1 $Y \/ ~proposition $X1 $X \/
% 0.44/0.62     ~theme $X1 $Y $X \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     present $X1 (skolemFOFtoCNF_X5 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $V \/
% 0.44/0.62     ~agent $X1 $Y $V \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X $Z \/ ~present $X1 $Y \/ ~proposition $X1 $X \/
% 0.44/0.62     ~theme $X1 $Y $X \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     present (skolemFOFtoCNF_X4 $X1 $X2) (skolemFOFtoCNF_X6 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $V \/
% 0.44/0.62     ~agent $X1 $Y $V \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X $Z \/ ~present $X1 $Y \/ ~proposition $X1 $X \/
% 0.44/0.62     ~theme $X1 $Y $X \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     proposition $X1 (skolemFOFtoCNF_X4 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $V \/
% 0.44/0.62     ~agent $X1 $Y $V \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X $Z \/ ~present $X1 $Y \/ ~proposition $X1 $X \/
% 0.44/0.62     ~theme $X1 $Y $X \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     theme $X1 (skolemFOFtoCNF_X5 $X1 $X2) (skolemFOFtoCNF_X4 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $V \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X1 \/ ~theme $X1 $Y $X1 \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     accessible_world $X1 (skolemFOFtoCNF_X4 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $X2 \/
% 0.44/0.62     ~agent $X1 $Y $X2 \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $X3 \/ ~of $X1 $X3 $X2 \/ ~present $X $Z \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X \/ ~theme $X1 $Y $X \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     accessible_world $X1 (skolemFOFtoCNF_X4 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $X2 \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $X3 \/ ~man $X1 $X2 \/ ~mia_forename $X1 $X3 \/
% 0.44/0.62     ~of $X1 $X3 $X2 \/ ~present $X1 $Y \/ ~proposition $X1 $X1 \/
% 0.44/0.62     ~theme $X1 $Y $X1 \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     accessible_world $X1 (skolemFOFtoCNF_X4 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $V \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X1 \/ ~theme $X1 $Y $X1 \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     agent $X1 (skolemFOFtoCNF_X5 $X1 $X2) $X2
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $X2 \/
% 0.44/0.62     ~agent $X1 $Y $X2 \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $X3 \/ ~of $X1 $X3 $X2 \/ ~present $X $Z \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X \/ ~theme $X1 $Y $X \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     agent $X1 (skolemFOFtoCNF_X5 $X1 $X2) $X2
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $X2 \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $X3 \/ ~man $X1 $X2 \/ ~mia_forename $X1 $X3 \/
% 0.44/0.62     ~of $X1 $X3 $X2 \/ ~present $X1 $Y \/ ~proposition $X1 $X1 \/
% 0.44/0.62     ~theme $X1 $Y $X1 \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     agent $X1 (skolemFOFtoCNF_X5 $X1 $X2) $X2
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $V \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X1 \/ ~theme $X1 $Y $X1 \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     agent (skolemFOFtoCNF_X4 $X1 $X2) (skolemFOFtoCNF_X6 $X1 $X2) $X2
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $X2 \/
% 0.44/0.62     ~agent $X1 $Y $X2 \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $X3 \/ ~of $X1 $X3 $X2 \/ ~present $X $Z \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X \/ ~theme $X1 $Y $X \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     agent (skolemFOFtoCNF_X4 $X1 $X2) (skolemFOFtoCNF_X6 $X1 $X2) $X2
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $X2 \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $X3 \/ ~man $X1 $X2 \/ ~mia_forename $X1 $X3 \/
% 0.44/0.62     ~of $X1 $X3 $X2 \/ ~present $X1 $Y \/ ~proposition $X1 $X1 \/
% 0.44/0.62     ~theme $X1 $Y $X1 \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     agent (skolemFOFtoCNF_X4 $X1 $X2) (skolemFOFtoCNF_X6 $X1 $X2) $X2
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $V \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X1 \/ ~theme $X1 $Y $X1 \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     dance (skolemFOFtoCNF_X4 $X1 $X2) (skolemFOFtoCNF_X6 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $X2 \/
% 0.44/0.62     ~agent $X1 $Y $X2 \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $X3 \/ ~of $X1 $X3 $X2 \/ ~present $X $Z \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X \/ ~theme $X1 $Y $X \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     dance (skolemFOFtoCNF_X4 $X1 $X2) (skolemFOFtoCNF_X6 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $X2 \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $X3 \/ ~man $X1 $X2 \/ ~mia_forename $X1 $X3 \/
% 0.44/0.62     ~of $X1 $X3 $X2 \/ ~present $X1 $Y \/ ~proposition $X1 $X1 \/
% 0.44/0.62     ~theme $X1 $Y $X1 \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     dance (skolemFOFtoCNF_X4 $X1 $X2) (skolemFOFtoCNF_X6 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $V \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X1 \/ ~theme $X1 $Y $X1 \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     desire_want $X1 (skolemFOFtoCNF_X5 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $X2 \/
% 0.44/0.62     ~agent $X1 $Y $X2 \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $X3 \/ ~of $X1 $X3 $X2 \/ ~present $X $Z \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X \/ ~theme $X1 $Y $X \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     desire_want $X1 (skolemFOFtoCNF_X5 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $X2 \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $X3 \/ ~man $X1 $X2 \/ ~mia_forename $X1 $X3 \/
% 0.44/0.62     ~of $X1 $X3 $X2 \/ ~present $X1 $Y \/ ~proposition $X1 $X1 \/
% 0.44/0.62     ~theme $X1 $Y $X1 \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     desire_want $X1 (skolemFOFtoCNF_X5 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $V \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X1 \/ ~theme $X1 $Y $X1 \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     event (skolemFOFtoCNF_X4 $X1 $X2) (skolemFOFtoCNF_X6 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $X2 \/
% 0.44/0.62     ~agent $X1 $Y $X2 \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $X3 \/ ~of $X1 $X3 $X2 \/ ~present $X $Z \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X \/ ~theme $X1 $Y $X \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     event (skolemFOFtoCNF_X4 $X1 $X2) (skolemFOFtoCNF_X6 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $X2 \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $X3 \/ ~man $X1 $X2 \/ ~mia_forename $X1 $X3 \/
% 0.44/0.62     ~of $X1 $X3 $X2 \/ ~present $X1 $Y \/ ~proposition $X1 $X1 \/
% 0.44/0.62     ~theme $X1 $Y $X1 \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     event (skolemFOFtoCNF_X4 $X1 $X2) (skolemFOFtoCNF_X6 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $V \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X1 \/ ~theme $X1 $Y $X1 \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     present $X1 (skolemFOFtoCNF_X5 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $X2 \/
% 0.44/0.62     ~agent $X1 $Y $X2 \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $X3 \/ ~of $X1 $X3 $X2 \/ ~present $X $Z \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X \/ ~theme $X1 $Y $X \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     present $X1 (skolemFOFtoCNF_X5 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $X2 \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $X3 \/ ~man $X1 $X2 \/ ~mia_forename $X1 $X3 \/
% 0.44/0.62     ~of $X1 $X3 $X2 \/ ~present $X1 $Y \/ ~proposition $X1 $X1 \/
% 0.44/0.62     ~theme $X1 $Y $X1 \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     present $X1 (skolemFOFtoCNF_X5 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $V \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X1 \/ ~theme $X1 $Y $X1 \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     present (skolemFOFtoCNF_X4 $X1 $X2) (skolemFOFtoCNF_X6 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $X2 \/
% 0.44/0.62     ~agent $X1 $Y $X2 \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $X3 \/ ~of $X1 $X3 $X2 \/ ~present $X $Z \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X \/ ~theme $X1 $Y $X \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     present (skolemFOFtoCNF_X4 $X1 $X2) (skolemFOFtoCNF_X6 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $X2 \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $X3 \/ ~man $X1 $X2 \/ ~mia_forename $X1 $X3 \/
% 0.44/0.62     ~of $X1 $X3 $X2 \/ ~present $X1 $Y \/ ~proposition $X1 $X1 \/
% 0.44/0.62     ~theme $X1 $Y $X1 \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     present (skolemFOFtoCNF_X4 $X1 $X2) (skolemFOFtoCNF_X6 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $V \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X1 \/ ~theme $X1 $Y $X1 \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     proposition $X1 (skolemFOFtoCNF_X4 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $X2 \/
% 0.44/0.62     ~agent $X1 $Y $X2 \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $X3 \/ ~of $X1 $X3 $X2 \/ ~present $X $Z \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X \/ ~theme $X1 $Y $X \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     proposition $X1 (skolemFOFtoCNF_X4 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $X2 \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $X3 \/ ~man $X1 $X2 \/ ~mia_forename $X1 $X3 \/
% 0.44/0.62     ~of $X1 $X3 $X2 \/ ~present $X1 $Y \/ ~proposition $X1 $X1 \/
% 0.44/0.62     ~theme $X1 $Y $X1 \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     proposition $X1 (skolemFOFtoCNF_X4 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $V \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $W \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $W \/ ~of $X1 $W $V \/ ~of $X1 $X3 $X2 \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X1 \/ ~theme $X1 $Y $X1 \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $V \/
% 0.44/0.62     theme $X1 (skolemFOFtoCNF_X5 $X1 $X2) (skolemFOFtoCNF_X4 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X \/ ~actual_world $X1 \/ ~agent $X $Z $X2 \/
% 0.44/0.62     ~agent $X1 $Y $X2 \/ ~dance $X $Z \/ ~desire_want $X1 $Y \/
% 0.44/0.62     ~event $X $Z \/ ~forename $X1 $X3 \/ ~man $X1 $X2 \/
% 0.44/0.62     ~mia_forename $X1 $X3 \/ ~of $X1 $X3 $X2 \/ ~present $X $Z \/
% 0.44/0.62     ~present $X1 $Y \/ ~proposition $X1 $X \/ ~theme $X1 $Y $X \/
% 0.44/0.62     ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     theme $X1 (skolemFOFtoCNF_X5 $X1 $X2) (skolemFOFtoCNF_X4 $X1 $X2)
% 0.44/0.62  |- ~accessible_world $X1 $X1 \/ ~actual_world $X1 \/ ~agent $X1 $Y $X2 \/
% 0.44/0.62     ~dance $X1 $Y \/ ~desire_want $X1 $Y \/ ~event $X1 $Y \/
% 0.44/0.62     ~forename $X1 $X3 \/ ~man $X1 $X2 \/ ~mia_forename $X1 $X3 \/
% 0.44/0.62     ~of $X1 $X3 $X2 \/ ~present $X1 $Y \/ ~proposition $X1 $X1 \/
% 0.44/0.62     ~theme $X1 $Y $X1 \/ ~vincent_forename $X1 $X3 \/ ~woman $X1 $X2 \/
% 0.44/0.62     theme $X1 (skolemFOFtoCNF_X5 $X1 $X2) (skolemFOFtoCNF_X4 $X1 $X2)
% 0.44/0.62  |- relname skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.44/0.62  |- event skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.44/0.62  |- female skolemFOFtoCNF_U skolemFOFtoCNF_V
% 0.44/0.62  |- human_person skolemFOFtoCNF_U skolemFOFtoCNF_V
% 0.44/0.62  |- human skolemFOFtoCNF_U skolemFOFtoCNF_V
% 0.44/0.62  |- animate skolemFOFtoCNF_U skolemFOFtoCNF_V
% 0.44/0.62  |- organism skolemFOFtoCNF_U skolemFOFtoCNF_V
% 0.44/0.62  |- entity skolemFOFtoCNF_U skolemFOFtoCNF_V
% 0.44/0.63  |- impartial skolemFOFtoCNF_U skolemFOFtoCNF_V
% 0.44/0.63  |- living skolemFOFtoCNF_U skolemFOFtoCNF_V
% 0.44/0.63  |- thing skolemFOFtoCNF_U skolemFOFtoCNF_V
% 0.44/0.63  |- specific skolemFOFtoCNF_U skolemFOFtoCNF_V
% 0.44/0.63  |- existent skolemFOFtoCNF_U skolemFOFtoCNF_V
% 0.44/0.63  |- relation skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.44/0.63  |- abstraction skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.44/0.63  |- unisex skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.44/0.63  |- general skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.44/0.63  |- nonhuman skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.44/0.63  |- thing skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.44/0.63  |- relation skolemFOFtoCNF_U skolemFOFtoCNF_X
% 0.44/0.63  |- abstraction skolemFOFtoCNF_U skolemFOFtoCNF_X
% 0.44/0.63  |- thing skolemFOFtoCNF_U skolemFOFtoCNF_X
% 0.44/0.63  |- nonhuman skolemFOFtoCNF_U skolemFOFtoCNF_X
% 0.44/0.63  |- general skolemFOFtoCNF_U skolemFOFtoCNF_X
% 0.44/0.63  |- unisex skolemFOFtoCNF_U skolemFOFtoCNF_X
% 0.44/0.63  |- singleton skolemFOFtoCNF_U skolemFOFtoCNF_V
% 0.44/0.63  |- singleton skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.44/0.63  |- singleton skolemFOFtoCNF_U skolemFOFtoCNF_X
% 0.44/0.63  |- eventuality skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.44/0.63  |- eventuality skolemFOFtoCNF_X skolemFOFtoCNF_Z
% 0.44/0.63  |- thing skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.44/0.63  |- specific skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.44/0.63  |- nonexistent skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.44/0.63  |- unisex skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.44/0.63  |- thing skolemFOFtoCNF_X skolemFOFtoCNF_Z
% 0.44/0.63  |- specific skolemFOFtoCNF_X skolemFOFtoCNF_Z
% 0.44/0.63  |- nonexistent skolemFOFtoCNF_X skolemFOFtoCNF_Z
% 0.44/0.63  |- unisex skolemFOFtoCNF_X skolemFOFtoCNF_Z
% 0.44/0.63  |- singleton skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.44/0.63  |- singleton skolemFOFtoCNF_X skolemFOFtoCNF_Z
% 0.44/0.63  |- ~existent skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.44/0.63  |- ~existent skolemFOFtoCNF_X skolemFOFtoCNF_Z
% 0.44/0.63  |- ~human skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.44/0.63  |- ~human skolemFOFtoCNF_U skolemFOFtoCNF_X
% 0.44/0.63  |- ~general skolemFOFtoCNF_U skolemFOFtoCNF_V
% 0.44/0.63  |- ~general skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.44/0.63  |- ~general skolemFOFtoCNF_X skolemFOFtoCNF_Z
% 0.44/0.63  |- ~female skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.44/0.63  |- ~female skolemFOFtoCNF_U skolemFOFtoCNF_X
% 0.44/0.63  |- ~female skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.44/0.63  |- ~female skolemFOFtoCNF_X skolemFOFtoCNF_Z
% 0.44/0.63  |- ~male skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.48/0.63  |- ~male skolemFOFtoCNF_U skolemFOFtoCNF_X
% 0.48/0.63  |- ~male skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.48/0.63  |- ~male skolemFOFtoCNF_X skolemFOFtoCNF_Z
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_85 \/ female $_85 skolemFOFtoCNF_V
% 0.48/0.63  |- female skolemFOFtoCNF_X skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $W \/ female $W skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_90 \/ animate $_90 skolemFOFtoCNF_V
% 0.48/0.63  |- animate skolemFOFtoCNF_X skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $W \/ animate $W skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_95 \/ human $_95 skolemFOFtoCNF_V
% 0.48/0.63  |- human skolemFOFtoCNF_X skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $W \/ human $W skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_100 \/
% 0.48/0.63     living $_100 skolemFOFtoCNF_V
% 0.48/0.63  |- living skolemFOFtoCNF_X skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $W \/ living $W skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_105 \/
% 0.48/0.63     impartial $_105 skolemFOFtoCNF_V
% 0.48/0.63  |- impartial skolemFOFtoCNF_X skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $W \/ impartial $W skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_110 \/
% 0.48/0.63     existent $_110 skolemFOFtoCNF_V
% 0.48/0.63  |- existent skolemFOFtoCNF_X skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $W \/ existent $W skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_115 \/
% 0.48/0.63     entity $_115 skolemFOFtoCNF_V
% 0.48/0.63  |- entity skolemFOFtoCNF_X skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $W \/ entity $W skolemFOFtoCNF_V
% 0.48/0.63  |- thing skolemFOFtoCNF_X skolemFOFtoCNF_V
% 0.48/0.63  |- specific skolemFOFtoCNF_X skolemFOFtoCNF_V
% 0.48/0.63  |- singleton skolemFOFtoCNF_X skolemFOFtoCNF_V
% 0.48/0.63  |- ~general skolemFOFtoCNF_X skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_120 \/
% 0.48/0.63     organism $_120 skolemFOFtoCNF_V
% 0.48/0.63  |- organism skolemFOFtoCNF_X skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $W \/ organism $W skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_125 \/
% 0.48/0.63     human_person $_125 skolemFOFtoCNF_V
% 0.48/0.63  |- human_person skolemFOFtoCNF_X skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $W \/
% 0.48/0.63     human_person $W skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_130 \/ woman $_130 skolemFOFtoCNF_V
% 0.48/0.63  |- woman skolemFOFtoCNF_X skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $W \/ woman $W skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_135 \/
% 0.48/0.63     mia_forename $_135 skolemFOFtoCNF_W
% 0.48/0.63  |- mia_forename skolemFOFtoCNF_X skolemFOFtoCNF_W
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $W \/
% 0.48/0.63     mia_forename $W skolemFOFtoCNF_W
% 0.48/0.63  |- forename skolemFOFtoCNF_X skolemFOFtoCNF_W
% 0.48/0.63  |- relname skolemFOFtoCNF_X skolemFOFtoCNF_W
% 0.48/0.63  |- relation skolemFOFtoCNF_X skolemFOFtoCNF_W
% 0.48/0.63  |- abstraction skolemFOFtoCNF_X skolemFOFtoCNF_W
% 0.48/0.63  |- thing skolemFOFtoCNF_X skolemFOFtoCNF_W
% 0.48/0.63  |- nonhuman skolemFOFtoCNF_X skolemFOFtoCNF_W
% 0.48/0.63  |- general skolemFOFtoCNF_X skolemFOFtoCNF_W
% 0.48/0.63  |- unisex skolemFOFtoCNF_X skolemFOFtoCNF_W
% 0.48/0.63  |- singleton skolemFOFtoCNF_X skolemFOFtoCNF_W
% 0.48/0.63  |- ~human skolemFOFtoCNF_X skolemFOFtoCNF_W
% 0.48/0.63  |- ~male skolemFOFtoCNF_X skolemFOFtoCNF_W
% 0.48/0.63  |- ~female skolemFOFtoCNF_X skolemFOFtoCNF_W
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_140 \/
% 0.48/0.63     relname $_140 skolemFOFtoCNF_W
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_140 \/
% 0.48/0.63     relname $_140 skolemFOFtoCNF_W
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_145 \/
% 0.48/0.63     forename $_145 skolemFOFtoCNF_W
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_145 \/
% 0.48/0.63     forename $_145 skolemFOFtoCNF_W
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_150 \/
% 0.48/0.63     general $_150 skolemFOFtoCNF_W
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_150 \/
% 0.48/0.63     general $_150 skolemFOFtoCNF_X
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_150 \/
% 0.48/0.63     general $_150 skolemFOFtoCNF_W
% 0.48/0.63  |- general skolemFOFtoCNF_X skolemFOFtoCNF_X
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $W \/ general $W skolemFOFtoCNF_X
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_157 \/
% 0.48/0.63     nonhuman $_157 skolemFOFtoCNF_W
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_157 \/
% 0.48/0.63     nonhuman $_157 skolemFOFtoCNF_X
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_157 \/
% 0.48/0.63     nonhuman $_157 skolemFOFtoCNF_W
% 0.48/0.63  |- nonhuman skolemFOFtoCNF_X skolemFOFtoCNF_X
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $W \/ nonhuman $W skolemFOFtoCNF_X
% 0.48/0.63  |- ~human skolemFOFtoCNF_X skolemFOFtoCNF_X
% 0.48/0.63  |- ~abstraction skolemFOFtoCNF_U $_162 \/
% 0.48/0.63     abstraction skolemFOFtoCNF_X $_162
% 0.48/0.63  |- abstraction skolemFOFtoCNF_X skolemFOFtoCNF_X
% 0.48/0.63  |- thing skolemFOFtoCNF_X skolemFOFtoCNF_X
% 0.48/0.63  |- unisex skolemFOFtoCNF_X skolemFOFtoCNF_X
% 0.48/0.63  |- ~male skolemFOFtoCNF_X skolemFOFtoCNF_X
% 0.48/0.63  |- ~female skolemFOFtoCNF_X skolemFOFtoCNF_X
% 0.48/0.63  |- singleton skolemFOFtoCNF_X skolemFOFtoCNF_X
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_168 \/
% 0.48/0.63     relation $_168 skolemFOFtoCNF_W
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_168 \/
% 0.48/0.63     relation $_168 skolemFOFtoCNF_X
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_168 \/
% 0.48/0.63     relation $_168 skolemFOFtoCNF_W
% 0.48/0.63  |- relation skolemFOFtoCNF_X skolemFOFtoCNF_X
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $W \/ relation $W skolemFOFtoCNF_X
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_175 \/
% 0.48/0.63     proposition $_175 skolemFOFtoCNF_X
% 0.48/0.63  |- proposition skolemFOFtoCNF_X skolemFOFtoCNF_X
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $W \/ proposition $W skolemFOFtoCNF_X
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_180 \/
% 0.48/0.63     desire_want $_180 skolemFOFtoCNF_Y
% 0.48/0.63  |- desire_want skolemFOFtoCNF_X skolemFOFtoCNF_Y
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $W \/ desire_want $W skolemFOFtoCNF_Y
% 0.48/0.63  |- event skolemFOFtoCNF_X skolemFOFtoCNF_Y
% 0.48/0.63  |- eventuality skolemFOFtoCNF_X skolemFOFtoCNF_Y
% 0.48/0.63  |- thing skolemFOFtoCNF_X skolemFOFtoCNF_Y
% 0.48/0.63  |- specific skolemFOFtoCNF_X skolemFOFtoCNF_Y
% 0.48/0.63  |- nonexistent skolemFOFtoCNF_X skolemFOFtoCNF_Y
% 0.48/0.63  |- unisex skolemFOFtoCNF_X skolemFOFtoCNF_Y
% 0.48/0.63  |- singleton skolemFOFtoCNF_X skolemFOFtoCNF_Y
% 0.48/0.63  |- ~existent skolemFOFtoCNF_X skolemFOFtoCNF_Y
% 0.48/0.63  |- ~general skolemFOFtoCNF_X skolemFOFtoCNF_Y
% 0.48/0.63  |- ~male skolemFOFtoCNF_X skolemFOFtoCNF_Y
% 0.48/0.63  |- ~female skolemFOFtoCNF_X skolemFOFtoCNF_Y
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_185 \/
% 0.48/0.63     present $_185 skolemFOFtoCNF_Y
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_185 \/
% 0.48/0.63     present $_185 skolemFOFtoCNF_Z
% 0.48/0.63  |- present skolemFOFtoCNF_X skolemFOFtoCNF_Y
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $W \/ present $W skolemFOFtoCNF_Y
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_191 \/
% 0.48/0.63     unisex $_191 skolemFOFtoCNF_W
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_191 \/
% 0.48/0.63     unisex $_191 skolemFOFtoCNF_X
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_191 \/
% 0.48/0.63     unisex $_191 skolemFOFtoCNF_Y
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_191 \/
% 0.48/0.63     unisex $_191 skolemFOFtoCNF_W
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_191 \/
% 0.48/0.63     unisex $_191 skolemFOFtoCNF_X
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_191 \/
% 0.48/0.63     unisex $_191 skolemFOFtoCNF_Y
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_191 \/
% 0.48/0.63     unisex $_191 skolemFOFtoCNF_Z
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_201 \/
% 0.48/0.63     nonexistent $_201 skolemFOFtoCNF_Y
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_201 \/
% 0.48/0.63     nonexistent $_201 skolemFOFtoCNF_Y
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_201 \/
% 0.48/0.63     nonexistent $_201 skolemFOFtoCNF_Z
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_207 \/
% 0.48/0.63     specific $_207 skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_207 \/
% 0.48/0.63     specific $_207 skolemFOFtoCNF_Y
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_207 \/
% 0.48/0.63     specific $_207 skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_207 \/
% 0.48/0.63     specific $_207 skolemFOFtoCNF_Y
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_207 \/
% 0.48/0.63     specific $_207 skolemFOFtoCNF_Z
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_215 \/
% 0.48/0.63     singleton $_215 skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_215 \/
% 0.48/0.63     singleton $_215 skolemFOFtoCNF_W
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_215 \/
% 0.48/0.63     singleton $_215 skolemFOFtoCNF_X
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_215 \/
% 0.48/0.63     singleton $_215 skolemFOFtoCNF_Y
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_215 \/
% 0.48/0.63     singleton $_215 skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_215 \/
% 0.48/0.63     singleton $_215 skolemFOFtoCNF_W
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_215 \/
% 0.48/0.63     singleton $_215 skolemFOFtoCNF_X
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_215 \/
% 0.48/0.63     singleton $_215 skolemFOFtoCNF_Y
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_X $_215 \/
% 0.48/0.63     singleton $_215 skolemFOFtoCNF_Z
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_227 \/ thing $_227 skolemFOFtoCNF_V
% 0.48/0.63  |- ~accessible_world skolemFOFtoCNF_U $_227 \/ thing $_227 skolemFOFtoCNF_W
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_U $_227 \/ thing $_227 skolemFOFtoCNF_X
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_U $_227 \/ thing $_227 skolemFOFtoCNF_Y
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X $_227 \/ thing $_227 skolemFOFtoCNF_V
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X $_227 \/ thing $_227 skolemFOFtoCNF_W
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X $_227 \/ thing $_227 skolemFOFtoCNF_X
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X $_227 \/ thing $_227 skolemFOFtoCNF_Y
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X $_227 \/ thing $_227 skolemFOFtoCNF_Z
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_U $_239 \/
% 0.48/0.64     eventuality $_239 skolemFOFtoCNF_Y
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X $_239 \/
% 0.48/0.64     eventuality $_239 skolemFOFtoCNF_Y
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X $_239 \/
% 0.48/0.64     eventuality $_239 skolemFOFtoCNF_Z
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_U $_245 \/ event $_245 skolemFOFtoCNF_Y
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X $_245 \/ event $_245 skolemFOFtoCNF_Y
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X $_245 \/ event $_245 skolemFOFtoCNF_Z
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X $_251 \/ dance $_251 skolemFOFtoCNF_Z
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_U $_256 \/
% 0.48/0.64     of $_256 skolemFOFtoCNF_W skolemFOFtoCNF_V
% 0.48/0.64  |- of skolemFOFtoCNF_X skolemFOFtoCNF_W skolemFOFtoCNF_V
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X $X \/
% 0.48/0.64     of $X skolemFOFtoCNF_W skolemFOFtoCNF_V
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_U $_262 \/
% 0.48/0.64     theme $_262 skolemFOFtoCNF_Y skolemFOFtoCNF_X
% 0.48/0.64  |- theme skolemFOFtoCNF_X skolemFOFtoCNF_Y skolemFOFtoCNF_X
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X $X \/
% 0.48/0.64     theme $X skolemFOFtoCNF_Y skolemFOFtoCNF_X
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_U $_268 \/
% 0.48/0.64     agent $_268 skolemFOFtoCNF_Y skolemFOFtoCNF_V
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X $_268 \/
% 0.48/0.64     agent $_268 skolemFOFtoCNF_Z skolemFOFtoCNF_V
% 0.48/0.64  |- agent skolemFOFtoCNF_X skolemFOFtoCNF_Y skolemFOFtoCNF_V
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X $X \/
% 0.48/0.64     agent $X skolemFOFtoCNF_Y skolemFOFtoCNF_V
% 0.48/0.64  |- ~forename skolemFOFtoCNF_U $_275 \/
% 0.48/0.64     ~of skolemFOFtoCNF_U $_275 skolemFOFtoCNF_V \/ $_275 = skolemFOFtoCNF_W
% 0.48/0.64  |- ~forename skolemFOFtoCNF_X $_275 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_275 skolemFOFtoCNF_V \/ $_275 = skolemFOFtoCNF_W
% 0.48/0.64  |- ~desire_want skolemFOFtoCNF_U $_280 \/
% 0.48/0.64     ~proposition skolemFOFtoCNF_U $_282 \/
% 0.48/0.64     ~theme skolemFOFtoCNF_U $_280 $_282 \/ skolemFOFtoCNF_X = $_282
% 0.48/0.64  |- ~desire_want skolemFOFtoCNF_X $_280 \/
% 0.48/0.64     ~proposition skolemFOFtoCNF_X $_282 \/
% 0.48/0.64     ~theme skolemFOFtoCNF_X $_280 $_282 \/ skolemFOFtoCNF_X = $_282
% 0.48/0.64  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_349 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X $_352 $_349 \/ ~dance skolemFOFtoCNF_X $_352 \/
% 0.48/0.64     ~event skolemFOFtoCNF_X $_352 \/ ~forename skolemFOFtoCNF_U $_350 \/
% 0.48/0.64     ~man skolemFOFtoCNF_U $_349 \/ ~mia_forename skolemFOFtoCNF_U $_350 \/
% 0.48/0.64     ~of skolemFOFtoCNF_U $_350 $_349 \/ ~present skolemFOFtoCNF_X $_352 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U $_350 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_U $_349 \/
% 0.48/0.64     accessible_world skolemFOFtoCNF_U
% 0.48/0.64       (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_349)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_352 $_349 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_349 \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X $_352 \/ ~event skolemFOFtoCNF_X $_352 \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_350 \/ ~man skolemFOFtoCNF_X $_349 \/
% 0.48/0.64     ~mia_forename skolemFOFtoCNF_X $_350 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_350 $_349 \/ ~present skolemFOFtoCNF_X $_352 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_350 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_X $_349 \/
% 0.48/0.64     accessible_world skolemFOFtoCNF_X
% 0.48/0.64       (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_349)
% 0.48/0.64  |- ~man skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.48/0.64     accessible_world skolemFOFtoCNF_U
% 0.48/0.64       (skolemFOFtoCNF_X4 skolemFOFtoCNF_U skolemFOFtoCNF_V)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~man skolemFOFtoCNF_X skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X skolemFOFtoCNF_W \/
% 0.48/0.64     accessible_world skolemFOFtoCNF_X
% 0.48/0.64       (skolemFOFtoCNF_X4 skolemFOFtoCNF_X skolemFOFtoCNF_V)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X skolemFOFtoCNF_Y \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_370 \/ ~man skolemFOFtoCNF_X $_369 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_370 $_369 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_370 \/
% 0.48/0.64     accessible_world skolemFOFtoCNF_X
% 0.48/0.64       (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_369)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X skolemFOFtoCNF_Y \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_382 \/ ~man skolemFOFtoCNF_X $_381 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_382 $_381 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_382 \/
% 0.48/0.64     desire_want skolemFOFtoCNF_X (skolemFOFtoCNF_X5 skolemFOFtoCNF_X $_381)
% 0.48/0.64  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_387 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X $_390 $_387 \/ ~dance skolemFOFtoCNF_X $_390 \/
% 0.48/0.64     ~event skolemFOFtoCNF_X $_390 \/ ~forename skolemFOFtoCNF_U $_388 \/
% 0.48/0.64     ~man skolemFOFtoCNF_U $_387 \/ ~mia_forename skolemFOFtoCNF_U $_388 \/
% 0.48/0.64     ~of skolemFOFtoCNF_U $_388 $_387 \/ ~present skolemFOFtoCNF_X $_390 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U $_388 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_U $_387 \/
% 0.48/0.64     present skolemFOFtoCNF_U (skolemFOFtoCNF_X5 skolemFOFtoCNF_U $_387)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_390 $_387 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_387 \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X $_390 \/ ~event skolemFOFtoCNF_X $_390 \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_388 \/ ~man skolemFOFtoCNF_X $_387 \/
% 0.48/0.64     ~mia_forename skolemFOFtoCNF_X $_388 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_388 $_387 \/ ~present skolemFOFtoCNF_X $_390 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_388 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_X $_387 \/
% 0.48/0.64     present skolemFOFtoCNF_X (skolemFOFtoCNF_X5 skolemFOFtoCNF_X $_387)
% 0.48/0.64  |- ~man skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.48/0.64     present skolemFOFtoCNF_U
% 0.48/0.64       (skolemFOFtoCNF_X5 skolemFOFtoCNF_U skolemFOFtoCNF_V)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~man skolemFOFtoCNF_X skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X skolemFOFtoCNF_W \/
% 0.48/0.64     present skolemFOFtoCNF_X
% 0.48/0.64       (skolemFOFtoCNF_X5 skolemFOFtoCNF_X skolemFOFtoCNF_V)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X skolemFOFtoCNF_Y \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_408 \/ ~man skolemFOFtoCNF_X $_407 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_408 $_407 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_408 \/
% 0.48/0.64     present skolemFOFtoCNF_X (skolemFOFtoCNF_X5 skolemFOFtoCNF_X $_407)
% 0.48/0.64  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_413 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X $_416 $_413 \/ ~dance skolemFOFtoCNF_X $_416 \/
% 0.48/0.64     ~event skolemFOFtoCNF_X $_416 \/ ~forename skolemFOFtoCNF_U $_414 \/
% 0.48/0.64     ~man skolemFOFtoCNF_U $_413 \/ ~mia_forename skolemFOFtoCNF_U $_414 \/
% 0.48/0.64     ~of skolemFOFtoCNF_U $_414 $_413 \/ ~present skolemFOFtoCNF_X $_416 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U $_414 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_U $_413 \/
% 0.48/0.64     desire_want skolemFOFtoCNF_U (skolemFOFtoCNF_X5 skolemFOFtoCNF_U $_413)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_416 $_413 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_413 \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X $_416 \/ ~event skolemFOFtoCNF_X $_416 \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_414 \/ ~man skolemFOFtoCNF_X $_413 \/
% 0.48/0.64     ~mia_forename skolemFOFtoCNF_X $_414 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_414 $_413 \/ ~present skolemFOFtoCNF_X $_416 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_414 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_X $_413 \/
% 0.48/0.64     desire_want skolemFOFtoCNF_X (skolemFOFtoCNF_X5 skolemFOFtoCNF_X $_413)
% 0.48/0.64  |- ~man skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.48/0.64     desire_want skolemFOFtoCNF_U
% 0.48/0.64       (skolemFOFtoCNF_X5 skolemFOFtoCNF_U skolemFOFtoCNF_V)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~man skolemFOFtoCNF_X skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X skolemFOFtoCNF_W \/
% 0.48/0.64     desire_want skolemFOFtoCNF_X
% 0.48/0.64       (skolemFOFtoCNF_X5 skolemFOFtoCNF_X skolemFOFtoCNF_V)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X skolemFOFtoCNF_Y \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_434 \/ ~man skolemFOFtoCNF_X $_433 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_434 $_433 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_434 \/
% 0.48/0.64     proposition skolemFOFtoCNF_X (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_433)
% 0.48/0.64  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_439 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X $_442 $_439 \/ ~dance skolemFOFtoCNF_X $_442 \/
% 0.48/0.64     ~event skolemFOFtoCNF_X $_442 \/ ~forename skolemFOFtoCNF_U $_440 \/
% 0.48/0.64     ~man skolemFOFtoCNF_U $_439 \/ ~mia_forename skolemFOFtoCNF_U $_440 \/
% 0.48/0.64     ~of skolemFOFtoCNF_U $_440 $_439 \/ ~present skolemFOFtoCNF_X $_442 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U $_440 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_U $_439 \/
% 0.48/0.64     proposition skolemFOFtoCNF_U (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_439)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_442 $_439 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_439 \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X $_442 \/ ~event skolemFOFtoCNF_X $_442 \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_440 \/ ~man skolemFOFtoCNF_X $_439 \/
% 0.48/0.64     ~mia_forename skolemFOFtoCNF_X $_440 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_440 $_439 \/ ~present skolemFOFtoCNF_X $_442 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_440 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_X $_439 \/
% 0.48/0.64     proposition skolemFOFtoCNF_X (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_439)
% 0.48/0.64  |- ~man skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.48/0.64     proposition skolemFOFtoCNF_U
% 0.48/0.64       (skolemFOFtoCNF_X4 skolemFOFtoCNF_U skolemFOFtoCNF_V)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~man skolemFOFtoCNF_X skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X skolemFOFtoCNF_W \/
% 0.48/0.64     proposition skolemFOFtoCNF_X
% 0.48/0.64       (skolemFOFtoCNF_X4 skolemFOFtoCNF_X skolemFOFtoCNF_V)
% 0.48/0.64  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_453 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X $_456 $_453 \/ ~dance skolemFOFtoCNF_X $_456 \/
% 0.48/0.64     ~event skolemFOFtoCNF_X $_456 \/ ~forename skolemFOFtoCNF_U $_454 \/
% 0.48/0.64     ~man skolemFOFtoCNF_U $_453 \/ ~mia_forename skolemFOFtoCNF_U $_454 \/
% 0.48/0.64     ~of skolemFOFtoCNF_U $_454 $_453 \/ ~present skolemFOFtoCNF_X $_456 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U $_454 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_U $_453 \/
% 0.48/0.64     agent skolemFOFtoCNF_U (skolemFOFtoCNF_X5 skolemFOFtoCNF_U $_453) $_453
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_456 $_453 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_453 \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X $_456 \/ ~event skolemFOFtoCNF_X $_456 \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_454 \/ ~man skolemFOFtoCNF_X $_453 \/
% 0.48/0.64     ~mia_forename skolemFOFtoCNF_X $_454 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_454 $_453 \/ ~present skolemFOFtoCNF_X $_456 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_454 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_X $_453 \/
% 0.48/0.64     agent skolemFOFtoCNF_X (skolemFOFtoCNF_X5 skolemFOFtoCNF_X $_453) $_453
% 0.48/0.64  |- ~man skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.48/0.64     agent skolemFOFtoCNF_U
% 0.48/0.64       (skolemFOFtoCNF_X5 skolemFOFtoCNF_U skolemFOFtoCNF_V) skolemFOFtoCNF_V
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~man skolemFOFtoCNF_X skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X skolemFOFtoCNF_W \/
% 0.48/0.64     agent skolemFOFtoCNF_X
% 0.48/0.64       (skolemFOFtoCNF_X5 skolemFOFtoCNF_X skolemFOFtoCNF_V) skolemFOFtoCNF_V
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X skolemFOFtoCNF_Y \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_474 \/ ~man skolemFOFtoCNF_X $_473 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_474 $_473 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_474 \/
% 0.48/0.64     agent skolemFOFtoCNF_X (skolemFOFtoCNF_X5 skolemFOFtoCNF_X $_473) $_473
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X skolemFOFtoCNF_Y \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_486 \/ ~man skolemFOFtoCNF_X $_485 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_486 $_485 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_486 \/
% 0.48/0.64     dance (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_485)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X $_485)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X skolemFOFtoCNF_Y \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_498 \/ ~man skolemFOFtoCNF_X $_497 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_498 $_497 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_498 \/
% 0.48/0.64     event (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_497)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X $_497)
% 0.48/0.64  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_503 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X $_506 $_503 \/ ~dance skolemFOFtoCNF_X $_506 \/
% 0.48/0.64     ~event skolemFOFtoCNF_X $_506 \/ ~forename skolemFOFtoCNF_U $_504 \/
% 0.48/0.64     ~man skolemFOFtoCNF_U $_503 \/ ~mia_forename skolemFOFtoCNF_U $_504 \/
% 0.48/0.64     ~of skolemFOFtoCNF_U $_504 $_503 \/ ~present skolemFOFtoCNF_X $_506 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U $_504 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_U $_503 \/
% 0.48/0.64     present (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_503)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_U $_503)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_506 $_503 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_503 \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X $_506 \/ ~event skolemFOFtoCNF_X $_506 \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_504 \/ ~man skolemFOFtoCNF_X $_503 \/
% 0.48/0.64     ~mia_forename skolemFOFtoCNF_X $_504 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_504 $_503 \/ ~present skolemFOFtoCNF_X $_506 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_504 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_X $_503 \/
% 0.48/0.64     present (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_503)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X $_503)
% 0.48/0.64  |- ~man skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.48/0.64     present (skolemFOFtoCNF_X4 skolemFOFtoCNF_U skolemFOFtoCNF_V)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_U skolemFOFtoCNF_V)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~man skolemFOFtoCNF_X skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X skolemFOFtoCNF_W \/
% 0.48/0.64     present (skolemFOFtoCNF_X4 skolemFOFtoCNF_X skolemFOFtoCNF_V)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X skolemFOFtoCNF_V)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X skolemFOFtoCNF_Y \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_524 \/ ~man skolemFOFtoCNF_X $_523 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_524 $_523 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_524 \/
% 0.48/0.64     present (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_523)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X $_523)
% 0.48/0.64  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_529 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X $_532 $_529 \/ ~dance skolemFOFtoCNF_X $_532 \/
% 0.48/0.64     ~event skolemFOFtoCNF_X $_532 \/ ~forename skolemFOFtoCNF_U $_530 \/
% 0.48/0.64     ~man skolemFOFtoCNF_U $_529 \/ ~mia_forename skolemFOFtoCNF_U $_530 \/
% 0.48/0.64     ~of skolemFOFtoCNF_U $_530 $_529 \/ ~present skolemFOFtoCNF_X $_532 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U $_530 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_U $_529 \/
% 0.48/0.64     event (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_529)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_U $_529)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_532 $_529 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_529 \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X $_532 \/ ~event skolemFOFtoCNF_X $_532 \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_530 \/ ~man skolemFOFtoCNF_X $_529 \/
% 0.48/0.64     ~mia_forename skolemFOFtoCNF_X $_530 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_530 $_529 \/ ~present skolemFOFtoCNF_X $_532 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_530 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_X $_529 \/
% 0.48/0.64     event (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_529)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X $_529)
% 0.48/0.64  |- ~man skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.48/0.64     event (skolemFOFtoCNF_X4 skolemFOFtoCNF_U skolemFOFtoCNF_V)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_U skolemFOFtoCNF_V)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~man skolemFOFtoCNF_X skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X skolemFOFtoCNF_W \/
% 0.48/0.64     event (skolemFOFtoCNF_X4 skolemFOFtoCNF_X skolemFOFtoCNF_V)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X skolemFOFtoCNF_V)
% 0.48/0.64  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_543 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X $_546 $_543 \/ ~dance skolemFOFtoCNF_X $_546 \/
% 0.48/0.64     ~event skolemFOFtoCNF_X $_546 \/ ~forename skolemFOFtoCNF_U $_544 \/
% 0.48/0.64     ~man skolemFOFtoCNF_U $_543 \/ ~mia_forename skolemFOFtoCNF_U $_544 \/
% 0.48/0.64     ~of skolemFOFtoCNF_U $_544 $_543 \/ ~present skolemFOFtoCNF_X $_546 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U $_544 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_U $_543 \/
% 0.48/0.64     dance (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_543)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_U $_543)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_546 $_543 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_543 \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X $_546 \/ ~event skolemFOFtoCNF_X $_546 \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_544 \/ ~man skolemFOFtoCNF_X $_543 \/
% 0.48/0.64     ~mia_forename skolemFOFtoCNF_X $_544 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_544 $_543 \/ ~present skolemFOFtoCNF_X $_546 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_544 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_X $_543 \/
% 0.48/0.64     dance (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_543)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X $_543)
% 0.48/0.64  |- ~man skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.48/0.64     dance (skolemFOFtoCNF_X4 skolemFOFtoCNF_U skolemFOFtoCNF_V)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_U skolemFOFtoCNF_V)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~man skolemFOFtoCNF_X skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X skolemFOFtoCNF_W \/
% 0.48/0.64     dance (skolemFOFtoCNF_X4 skolemFOFtoCNF_X skolemFOFtoCNF_V)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X skolemFOFtoCNF_V)
% 0.48/0.64  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_557 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X $_560 $_557 \/ ~dance skolemFOFtoCNF_X $_560 \/
% 0.48/0.64     ~event skolemFOFtoCNF_X $_560 \/ ~forename skolemFOFtoCNF_U $_558 \/
% 0.48/0.64     ~man skolemFOFtoCNF_U $_557 \/ ~mia_forename skolemFOFtoCNF_U $_558 \/
% 0.48/0.64     ~of skolemFOFtoCNF_U $_558 $_557 \/ ~present skolemFOFtoCNF_X $_560 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U $_558 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_U $_557 \/
% 0.48/0.64     agent (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_557)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_U $_557) $_557
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_560 $_557 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_557 \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X $_560 \/ ~event skolemFOFtoCNF_X $_560 \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_558 \/ ~man skolemFOFtoCNF_X $_557 \/
% 0.48/0.64     ~mia_forename skolemFOFtoCNF_X $_558 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_558 $_557 \/ ~present skolemFOFtoCNF_X $_560 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_558 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_X $_557 \/
% 0.48/0.64     agent (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_557)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X $_557) $_557
% 0.48/0.64  |- ~man skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.48/0.64     agent (skolemFOFtoCNF_X4 skolemFOFtoCNF_U skolemFOFtoCNF_V)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_U skolemFOFtoCNF_V) skolemFOFtoCNF_V
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~man skolemFOFtoCNF_X skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X skolemFOFtoCNF_W \/
% 0.48/0.64     agent (skolemFOFtoCNF_X4 skolemFOFtoCNF_X skolemFOFtoCNF_V)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X skolemFOFtoCNF_V) skolemFOFtoCNF_V
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X skolemFOFtoCNF_Y \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_578 \/ ~man skolemFOFtoCNF_X $_577 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_578 $_577 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_578 \/
% 0.48/0.64     agent (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_577)
% 0.48/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X $_577) $_577
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X skolemFOFtoCNF_Y \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_590 \/ ~man skolemFOFtoCNF_X $_589 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_590 $_589 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_590 \/
% 0.48/0.64     theme skolemFOFtoCNF_X (skolemFOFtoCNF_X5 skolemFOFtoCNF_X $_589)
% 0.48/0.64       (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_589)
% 0.48/0.64  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_595 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X $_598 $_595 \/ ~dance skolemFOFtoCNF_X $_598 \/
% 0.48/0.64     ~event skolemFOFtoCNF_X $_598 \/ ~forename skolemFOFtoCNF_U $_596 \/
% 0.48/0.64     ~man skolemFOFtoCNF_U $_595 \/ ~mia_forename skolemFOFtoCNF_U $_596 \/
% 0.48/0.64     ~of skolemFOFtoCNF_U $_596 $_595 \/ ~present skolemFOFtoCNF_X $_598 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U $_596 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_U $_595 \/
% 0.48/0.64     theme skolemFOFtoCNF_U (skolemFOFtoCNF_X5 skolemFOFtoCNF_U $_595)
% 0.48/0.64       (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_595)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_598 $_595 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_595 \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X $_598 \/ ~event skolemFOFtoCNF_X $_598 \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_596 \/ ~man skolemFOFtoCNF_X $_595 \/
% 0.48/0.64     ~mia_forename skolemFOFtoCNF_X $_596 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_596 $_595 \/ ~present skolemFOFtoCNF_X $_598 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_596 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_X $_595 \/
% 0.48/0.64     theme skolemFOFtoCNF_X (skolemFOFtoCNF_X5 skolemFOFtoCNF_X $_595)
% 0.48/0.64       (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_595)
% 0.48/0.64  |- ~man skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.48/0.64     theme skolemFOFtoCNF_U
% 0.48/0.64       (skolemFOFtoCNF_X5 skolemFOFtoCNF_U skolemFOFtoCNF_V)
% 0.48/0.64       (skolemFOFtoCNF_X4 skolemFOFtoCNF_U skolemFOFtoCNF_V)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~man skolemFOFtoCNF_X skolemFOFtoCNF_V \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X skolemFOFtoCNF_W \/
% 0.48/0.64     theme skolemFOFtoCNF_X
% 0.48/0.64       (skolemFOFtoCNF_X5 skolemFOFtoCNF_X skolemFOFtoCNF_V)
% 0.48/0.64       (skolemFOFtoCNF_X4 skolemFOFtoCNF_X skolemFOFtoCNF_V)
% 0.48/0.64  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_607 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X $_614 $_607 \/ ~dance skolemFOFtoCNF_X $_614 \/
% 0.48/0.64     ~event skolemFOFtoCNF_X $_614 \/ ~forename skolemFOFtoCNF_U $_608 \/
% 0.48/0.64     ~forename skolemFOFtoCNF_U $_612 \/ ~man skolemFOFtoCNF_U $_611 \/
% 0.48/0.64     ~mia_forename skolemFOFtoCNF_U $_608 \/
% 0.48/0.64     ~of skolemFOFtoCNF_U $_608 $_607 \/ ~of skolemFOFtoCNF_U $_612 $_611 \/
% 0.48/0.64     ~present skolemFOFtoCNF_X $_614 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U $_612 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_U $_607 \/
% 0.48/0.64     desire_want skolemFOFtoCNF_U (skolemFOFtoCNF_X5 skolemFOFtoCNF_U $_611)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_614 $_607 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_607 \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X $_614 \/ ~event skolemFOFtoCNF_X $_614 \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_608 \/ ~forename skolemFOFtoCNF_X $_612 \/
% 0.48/0.64     ~man skolemFOFtoCNF_X $_611 \/ ~mia_forename skolemFOFtoCNF_X $_608 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_608 $_607 \/ ~of skolemFOFtoCNF_X $_612 $_611 \/
% 0.48/0.64     ~present skolemFOFtoCNF_X $_614 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_612 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_X $_607 \/
% 0.48/0.64     desire_want skolemFOFtoCNF_X (skolemFOFtoCNF_X5 skolemFOFtoCNF_X $_611)
% 0.48/0.64  |- ~agent skolemFOFtoCNF_X $_619 skolemFOFtoCNF_V \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X $_619 \/ ~event skolemFOFtoCNF_X $_619 \/
% 0.48/0.64     ~forename skolemFOFtoCNF_U $_618 \/ ~man skolemFOFtoCNF_U $_617 \/
% 0.48/0.64     ~of skolemFOFtoCNF_U $_618 $_617 \/ ~present skolemFOFtoCNF_X $_619 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U $_618 \/
% 0.48/0.64     desire_want skolemFOFtoCNF_U (skolemFOFtoCNF_X5 skolemFOFtoCNF_U $_617)
% 0.48/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.48/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X $_627 skolemFOFtoCNF_V \/
% 0.48/0.64     ~dance skolemFOFtoCNF_X $_627 \/ ~event skolemFOFtoCNF_X $_627 \/
% 0.48/0.64     ~forename skolemFOFtoCNF_X $_626 \/ ~man skolemFOFtoCNF_X $_625 \/
% 0.48/0.64     ~of skolemFOFtoCNF_X $_626 $_625 \/ ~present skolemFOFtoCNF_X $_627 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_X $_626 \/
% 0.48/0.64     desire_want skolemFOFtoCNF_X (skolemFOFtoCNF_X5 skolemFOFtoCNF_X $_625)
% 0.48/0.64  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_631 \/
% 0.48/0.64     ~agent skolemFOFtoCNF_X $_638 $_631 \/ ~dance skolemFOFtoCNF_X $_638 \/
% 0.48/0.64     ~event skolemFOFtoCNF_X $_638 \/ ~forename skolemFOFtoCNF_U $_632 \/
% 0.48/0.64     ~forename skolemFOFtoCNF_U $_636 \/ ~man skolemFOFtoCNF_U $_635 \/
% 0.48/0.64     ~mia_forename skolemFOFtoCNF_U $_632 \/
% 0.48/0.64     ~of skolemFOFtoCNF_U $_632 $_631 \/ ~of skolemFOFtoCNF_U $_636 $_635 \/
% 0.48/0.64     ~present skolemFOFtoCNF_X $_638 \/
% 0.48/0.64     ~vincent_forename skolemFOFtoCNF_U $_636 \/
% 0.48/0.64     ~woman skolemFOFtoCNF_U $_631 \/
% 0.48/0.64     accessible_world skolemFOFtoCNF_U
% 0.48/0.64       (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_635)
% 0.50/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.64     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_638 $_631 \/
% 0.50/0.64     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_631 \/
% 0.50/0.64     ~dance skolemFOFtoCNF_X $_638 \/ ~event skolemFOFtoCNF_X $_638 \/
% 0.50/0.64     ~forename skolemFOFtoCNF_X $_632 \/ ~forename skolemFOFtoCNF_X $_636 \/
% 0.50/0.64     ~man skolemFOFtoCNF_X $_635 \/ ~mia_forename skolemFOFtoCNF_X $_632 \/
% 0.50/0.64     ~of skolemFOFtoCNF_X $_632 $_631 \/ ~of skolemFOFtoCNF_X $_636 $_635 \/
% 0.50/0.64     ~present skolemFOFtoCNF_X $_638 \/
% 0.50/0.64     ~vincent_forename skolemFOFtoCNF_X $_636 \/
% 0.50/0.64     ~woman skolemFOFtoCNF_X $_631 \/
% 0.50/0.64     accessible_world skolemFOFtoCNF_X
% 0.50/0.64       (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_635)
% 0.50/0.64  |- ~agent skolemFOFtoCNF_X $_643 skolemFOFtoCNF_V \/
% 0.50/0.64     ~dance skolemFOFtoCNF_X $_643 \/ ~event skolemFOFtoCNF_X $_643 \/
% 0.50/0.64     ~forename skolemFOFtoCNF_U $_642 \/ ~man skolemFOFtoCNF_U $_641 \/
% 0.50/0.64     ~of skolemFOFtoCNF_U $_642 $_641 \/ ~present skolemFOFtoCNF_X $_643 \/
% 0.50/0.64     ~vincent_forename skolemFOFtoCNF_U $_642 \/
% 0.50/0.64     accessible_world skolemFOFtoCNF_U
% 0.50/0.64       (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_641)
% 0.50/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.50/0.64     ~agent skolemFOFtoCNF_X $_651 skolemFOFtoCNF_V \/
% 0.50/0.64     ~dance skolemFOFtoCNF_X $_651 \/ ~event skolemFOFtoCNF_X $_651 \/
% 0.50/0.64     ~forename skolemFOFtoCNF_X $_650 \/ ~man skolemFOFtoCNF_X $_649 \/
% 0.50/0.64     ~of skolemFOFtoCNF_X $_650 $_649 \/ ~present skolemFOFtoCNF_X $_651 \/
% 0.50/0.64     ~vincent_forename skolemFOFtoCNF_X $_650 \/
% 0.50/0.64     accessible_world skolemFOFtoCNF_X
% 0.50/0.64       (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_649)
% 0.50/0.64  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_655 \/
% 0.50/0.64     ~agent skolemFOFtoCNF_X $_662 $_655 \/ ~dance skolemFOFtoCNF_X $_662 \/
% 0.50/0.64     ~event skolemFOFtoCNF_X $_662 \/ ~forename skolemFOFtoCNF_U $_656 \/
% 0.50/0.64     ~forename skolemFOFtoCNF_U $_660 \/ ~man skolemFOFtoCNF_U $_659 \/
% 0.50/0.64     ~mia_forename skolemFOFtoCNF_U $_656 \/
% 0.50/0.64     ~of skolemFOFtoCNF_U $_656 $_655 \/ ~of skolemFOFtoCNF_U $_660 $_659 \/
% 0.50/0.64     ~present skolemFOFtoCNF_X $_662 \/
% 0.50/0.64     ~vincent_forename skolemFOFtoCNF_U $_660 \/
% 0.50/0.64     ~woman skolemFOFtoCNF_U $_655 \/
% 0.50/0.64     proposition skolemFOFtoCNF_U (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_659)
% 0.50/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.64     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_662 $_655 \/
% 0.50/0.64     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_655 \/
% 0.50/0.64     ~dance skolemFOFtoCNF_X $_662 \/ ~event skolemFOFtoCNF_X $_662 \/
% 0.50/0.64     ~forename skolemFOFtoCNF_X $_656 \/ ~forename skolemFOFtoCNF_X $_660 \/
% 0.50/0.64     ~man skolemFOFtoCNF_X $_659 \/ ~mia_forename skolemFOFtoCNF_X $_656 \/
% 0.50/0.64     ~of skolemFOFtoCNF_X $_656 $_655 \/ ~of skolemFOFtoCNF_X $_660 $_659 \/
% 0.50/0.64     ~present skolemFOFtoCNF_X $_662 \/
% 0.50/0.64     ~vincent_forename skolemFOFtoCNF_X $_660 \/
% 0.50/0.64     ~woman skolemFOFtoCNF_X $_655 \/
% 0.50/0.64     proposition skolemFOFtoCNF_X (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_659)
% 0.50/0.64  |- ~agent skolemFOFtoCNF_X $_667 skolemFOFtoCNF_V \/
% 0.50/0.64     ~dance skolemFOFtoCNF_X $_667 \/ ~event skolemFOFtoCNF_X $_667 \/
% 0.50/0.64     ~forename skolemFOFtoCNF_U $_666 \/ ~man skolemFOFtoCNF_U $_665 \/
% 0.50/0.64     ~of skolemFOFtoCNF_U $_666 $_665 \/ ~present skolemFOFtoCNF_X $_667 \/
% 0.50/0.64     ~vincent_forename skolemFOFtoCNF_U $_666 \/
% 0.50/0.64     proposition skolemFOFtoCNF_U (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_665)
% 0.50/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.50/0.64     ~agent skolemFOFtoCNF_X $_675 skolemFOFtoCNF_V \/
% 0.50/0.64     ~dance skolemFOFtoCNF_X $_675 \/ ~event skolemFOFtoCNF_X $_675 \/
% 0.50/0.64     ~forename skolemFOFtoCNF_X $_674 \/ ~man skolemFOFtoCNF_X $_673 \/
% 0.50/0.64     ~of skolemFOFtoCNF_X $_674 $_673 \/ ~present skolemFOFtoCNF_X $_675 \/
% 0.50/0.64     ~vincent_forename skolemFOFtoCNF_X $_674 \/
% 0.50/0.64     proposition skolemFOFtoCNF_X (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_673)
% 0.50/0.64  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_679 \/
% 0.50/0.64     ~agent skolemFOFtoCNF_X $_686 $_679 \/ ~dance skolemFOFtoCNF_X $_686 \/
% 0.50/0.64     ~event skolemFOFtoCNF_X $_686 \/ ~forename skolemFOFtoCNF_U $_680 \/
% 0.50/0.64     ~forename skolemFOFtoCNF_U $_684 \/ ~man skolemFOFtoCNF_U $_683 \/
% 0.50/0.64     ~mia_forename skolemFOFtoCNF_U $_680 \/
% 0.50/0.64     ~of skolemFOFtoCNF_U $_680 $_679 \/ ~of skolemFOFtoCNF_U $_684 $_683 \/
% 0.50/0.64     ~present skolemFOFtoCNF_X $_686 \/
% 0.50/0.64     ~vincent_forename skolemFOFtoCNF_U $_684 \/
% 0.50/0.64     ~woman skolemFOFtoCNF_U $_679 \/
% 0.50/0.64     present skolemFOFtoCNF_U (skolemFOFtoCNF_X5 skolemFOFtoCNF_U $_683)
% 0.50/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.64     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_686 $_679 \/
% 0.50/0.64     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_679 \/
% 0.50/0.64     ~dance skolemFOFtoCNF_X $_686 \/ ~event skolemFOFtoCNF_X $_686 \/
% 0.50/0.64     ~forename skolemFOFtoCNF_X $_680 \/ ~forename skolemFOFtoCNF_X $_684 \/
% 0.50/0.64     ~man skolemFOFtoCNF_X $_683 \/ ~mia_forename skolemFOFtoCNF_X $_680 \/
% 0.50/0.64     ~of skolemFOFtoCNF_X $_680 $_679 \/ ~of skolemFOFtoCNF_X $_684 $_683 \/
% 0.50/0.64     ~present skolemFOFtoCNF_X $_686 \/
% 0.50/0.64     ~vincent_forename skolemFOFtoCNF_X $_684 \/
% 0.50/0.64     ~woman skolemFOFtoCNF_X $_679 \/
% 0.50/0.64     present skolemFOFtoCNF_X (skolemFOFtoCNF_X5 skolemFOFtoCNF_X $_683)
% 0.50/0.64  |- ~agent skolemFOFtoCNF_X $_691 skolemFOFtoCNF_V \/
% 0.50/0.64     ~dance skolemFOFtoCNF_X $_691 \/ ~event skolemFOFtoCNF_X $_691 \/
% 0.50/0.64     ~forename skolemFOFtoCNF_U $_690 \/ ~man skolemFOFtoCNF_U $_689 \/
% 0.50/0.64     ~of skolemFOFtoCNF_U $_690 $_689 \/ ~present skolemFOFtoCNF_X $_691 \/
% 0.50/0.64     ~vincent_forename skolemFOFtoCNF_U $_690 \/
% 0.50/0.64     present skolemFOFtoCNF_U (skolemFOFtoCNF_X5 skolemFOFtoCNF_U $_689)
% 0.50/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.50/0.64     ~agent skolemFOFtoCNF_X $_699 skolemFOFtoCNF_V \/
% 0.50/0.64     ~dance skolemFOFtoCNF_X $_699 \/ ~event skolemFOFtoCNF_X $_699 \/
% 0.50/0.64     ~forename skolemFOFtoCNF_X $_698 \/ ~man skolemFOFtoCNF_X $_697 \/
% 0.50/0.64     ~of skolemFOFtoCNF_X $_698 $_697 \/ ~present skolemFOFtoCNF_X $_699 \/
% 0.50/0.64     ~vincent_forename skolemFOFtoCNF_X $_698 \/
% 0.50/0.64     present skolemFOFtoCNF_X (skolemFOFtoCNF_X5 skolemFOFtoCNF_X $_697)
% 0.50/0.64  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_703 \/
% 0.50/0.64     ~agent skolemFOFtoCNF_X $_710 $_703 \/ ~dance skolemFOFtoCNF_X $_710 \/
% 0.50/0.64     ~event skolemFOFtoCNF_X $_710 \/ ~forename skolemFOFtoCNF_U $_704 \/
% 0.50/0.64     ~forename skolemFOFtoCNF_U $_708 \/ ~man skolemFOFtoCNF_U $_707 \/
% 0.50/0.64     ~mia_forename skolemFOFtoCNF_U $_704 \/
% 0.50/0.64     ~of skolemFOFtoCNF_U $_704 $_703 \/ ~of skolemFOFtoCNF_U $_708 $_707 \/
% 0.50/0.64     ~present skolemFOFtoCNF_X $_710 \/
% 0.50/0.64     ~vincent_forename skolemFOFtoCNF_U $_708 \/
% 0.50/0.64     ~woman skolemFOFtoCNF_U $_703 \/
% 0.50/0.64     agent skolemFOFtoCNF_U (skolemFOFtoCNF_X5 skolemFOFtoCNF_U $_707) $_707
% 0.50/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.64     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_710 $_703 \/
% 0.50/0.64     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_703 \/
% 0.50/0.64     ~dance skolemFOFtoCNF_X $_710 \/ ~event skolemFOFtoCNF_X $_710 \/
% 0.50/0.64     ~forename skolemFOFtoCNF_X $_704 \/ ~forename skolemFOFtoCNF_X $_708 \/
% 0.50/0.64     ~man skolemFOFtoCNF_X $_707 \/ ~mia_forename skolemFOFtoCNF_X $_704 \/
% 0.50/0.64     ~of skolemFOFtoCNF_X $_704 $_703 \/ ~of skolemFOFtoCNF_X $_708 $_707 \/
% 0.50/0.64     ~present skolemFOFtoCNF_X $_710 \/
% 0.50/0.64     ~vincent_forename skolemFOFtoCNF_X $_708 \/
% 0.50/0.64     ~woman skolemFOFtoCNF_X $_703 \/
% 0.50/0.64     agent skolemFOFtoCNF_X (skolemFOFtoCNF_X5 skolemFOFtoCNF_X $_707) $_707
% 0.50/0.64  |- ~agent skolemFOFtoCNF_X $_715 skolemFOFtoCNF_V \/
% 0.50/0.64     ~dance skolemFOFtoCNF_X $_715 \/ ~event skolemFOFtoCNF_X $_715 \/
% 0.50/0.64     ~forename skolemFOFtoCNF_U $_714 \/ ~man skolemFOFtoCNF_U $_713 \/
% 0.50/0.64     ~of skolemFOFtoCNF_U $_714 $_713 \/ ~present skolemFOFtoCNF_X $_715 \/
% 0.50/0.64     ~vincent_forename skolemFOFtoCNF_U $_714 \/
% 0.50/0.64     agent skolemFOFtoCNF_U (skolemFOFtoCNF_X5 skolemFOFtoCNF_U $_713) $_713
% 0.50/0.64  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.64     ~actual_world skolemFOFtoCNF_X \/
% 0.50/0.64     ~agent skolemFOFtoCNF_X $_723 skolemFOFtoCNF_V \/
% 0.50/0.64     ~dance skolemFOFtoCNF_X $_723 \/ ~event skolemFOFtoCNF_X $_723 \/
% 0.50/0.64     ~forename skolemFOFtoCNF_X $_722 \/ ~man skolemFOFtoCNF_X $_721 \/
% 0.50/0.64     ~of skolemFOFtoCNF_X $_722 $_721 \/ ~present skolemFOFtoCNF_X $_723 \/
% 0.50/0.64     ~vincent_forename skolemFOFtoCNF_X $_722 \/
% 0.50/0.64     agent skolemFOFtoCNF_X (skolemFOFtoCNF_X5 skolemFOFtoCNF_X $_721) $_721
% 0.50/0.64  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_727 \/
% 0.50/0.64     ~agent skolemFOFtoCNF_X $_734 $_727 \/ ~dance skolemFOFtoCNF_X $_734 \/
% 0.50/0.64     ~event skolemFOFtoCNF_X $_734 \/ ~forename skolemFOFtoCNF_U $_728 \/
% 0.50/0.64     ~forename skolemFOFtoCNF_U $_732 \/ ~man skolemFOFtoCNF_U $_731 \/
% 0.50/0.64     ~mia_forename skolemFOFtoCNF_U $_728 \/
% 0.50/0.64     ~of skolemFOFtoCNF_U $_728 $_727 \/ ~of skolemFOFtoCNF_U $_732 $_731 \/
% 0.50/0.64     ~present skolemFOFtoCNF_X $_734 \/
% 0.50/0.64     ~vincent_forename skolemFOFtoCNF_U $_732 \/
% 0.50/0.64     ~woman skolemFOFtoCNF_U $_727 \/
% 0.50/0.64     dance (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_731)
% 0.50/0.64       (skolemFOFtoCNF_X6 skolemFOFtoCNF_U $_731)
% 0.50/0.65  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.65     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_734 $_727 \/
% 0.50/0.65     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_727 \/
% 0.50/0.65     ~dance skolemFOFtoCNF_X $_734 \/ ~event skolemFOFtoCNF_X $_734 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_X $_728 \/ ~forename skolemFOFtoCNF_X $_732 \/
% 0.50/0.65     ~man skolemFOFtoCNF_X $_731 \/ ~mia_forename skolemFOFtoCNF_X $_728 \/
% 0.50/0.65     ~of skolemFOFtoCNF_X $_728 $_727 \/ ~of skolemFOFtoCNF_X $_732 $_731 \/
% 0.50/0.65     ~present skolemFOFtoCNF_X $_734 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_X $_732 \/
% 0.50/0.65     ~woman skolemFOFtoCNF_X $_727 \/
% 0.50/0.65     dance (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_731)
% 0.50/0.65       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X $_731)
% 0.50/0.65  |- ~agent skolemFOFtoCNF_X $_739 skolemFOFtoCNF_V \/
% 0.50/0.65     ~dance skolemFOFtoCNF_X $_739 \/ ~event skolemFOFtoCNF_X $_739 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_U $_738 \/ ~man skolemFOFtoCNF_U $_737 \/
% 0.50/0.65     ~of skolemFOFtoCNF_U $_738 $_737 \/ ~present skolemFOFtoCNF_X $_739 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_U $_738 \/
% 0.50/0.65     dance (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_737)
% 0.50/0.65       (skolemFOFtoCNF_X6 skolemFOFtoCNF_U $_737)
% 0.50/0.65  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.65     ~actual_world skolemFOFtoCNF_X \/
% 0.50/0.65     ~agent skolemFOFtoCNF_X $_747 skolemFOFtoCNF_V \/
% 0.50/0.65     ~dance skolemFOFtoCNF_X $_747 \/ ~event skolemFOFtoCNF_X $_747 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_X $_746 \/ ~man skolemFOFtoCNF_X $_745 \/
% 0.50/0.65     ~of skolemFOFtoCNF_X $_746 $_745 \/ ~present skolemFOFtoCNF_X $_747 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_X $_746 \/
% 0.50/0.65     dance (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_745)
% 0.50/0.65       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X $_745)
% 0.50/0.65  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_751 \/
% 0.50/0.65     ~agent skolemFOFtoCNF_X $_758 $_751 \/ ~dance skolemFOFtoCNF_X $_758 \/
% 0.50/0.65     ~event skolemFOFtoCNF_X $_758 \/ ~forename skolemFOFtoCNF_U $_752 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_U $_756 \/ ~man skolemFOFtoCNF_U $_755 \/
% 0.50/0.65     ~mia_forename skolemFOFtoCNF_U $_752 \/
% 0.50/0.65     ~of skolemFOFtoCNF_U $_752 $_751 \/ ~of skolemFOFtoCNF_U $_756 $_755 \/
% 0.50/0.65     ~present skolemFOFtoCNF_X $_758 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_U $_756 \/
% 0.50/0.65     ~woman skolemFOFtoCNF_U $_751 \/
% 0.50/0.65     present (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_755)
% 0.50/0.65       (skolemFOFtoCNF_X6 skolemFOFtoCNF_U $_755)
% 0.50/0.65  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.65     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_758 $_751 \/
% 0.50/0.65     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_751 \/
% 0.50/0.65     ~dance skolemFOFtoCNF_X $_758 \/ ~event skolemFOFtoCNF_X $_758 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_X $_752 \/ ~forename skolemFOFtoCNF_X $_756 \/
% 0.50/0.65     ~man skolemFOFtoCNF_X $_755 \/ ~mia_forename skolemFOFtoCNF_X $_752 \/
% 0.50/0.65     ~of skolemFOFtoCNF_X $_752 $_751 \/ ~of skolemFOFtoCNF_X $_756 $_755 \/
% 0.50/0.65     ~present skolemFOFtoCNF_X $_758 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_X $_756 \/
% 0.50/0.65     ~woman skolemFOFtoCNF_X $_751 \/
% 0.50/0.65     present (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_755)
% 0.50/0.65       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X $_755)
% 0.50/0.65  |- ~agent skolemFOFtoCNF_X $_763 skolemFOFtoCNF_V \/
% 0.50/0.65     ~dance skolemFOFtoCNF_X $_763 \/ ~event skolemFOFtoCNF_X $_763 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_U $_762 \/ ~man skolemFOFtoCNF_U $_761 \/
% 0.50/0.65     ~of skolemFOFtoCNF_U $_762 $_761 \/ ~present skolemFOFtoCNF_X $_763 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_U $_762 \/
% 0.50/0.65     present (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_761)
% 0.50/0.65       (skolemFOFtoCNF_X6 skolemFOFtoCNF_U $_761)
% 0.50/0.65  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.65     ~actual_world skolemFOFtoCNF_X \/
% 0.50/0.65     ~agent skolemFOFtoCNF_X $_771 skolemFOFtoCNF_V \/
% 0.50/0.65     ~dance skolemFOFtoCNF_X $_771 \/ ~event skolemFOFtoCNF_X $_771 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_X $_770 \/ ~man skolemFOFtoCNF_X $_769 \/
% 0.50/0.65     ~of skolemFOFtoCNF_X $_770 $_769 \/ ~present skolemFOFtoCNF_X $_771 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_X $_770 \/
% 0.50/0.65     present (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_769)
% 0.50/0.65       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X $_769)
% 0.50/0.65  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_775 \/
% 0.50/0.65     ~agent skolemFOFtoCNF_X $_782 $_775 \/ ~dance skolemFOFtoCNF_X $_782 \/
% 0.50/0.65     ~event skolemFOFtoCNF_X $_782 \/ ~forename skolemFOFtoCNF_U $_776 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_U $_780 \/ ~man skolemFOFtoCNF_U $_779 \/
% 0.50/0.65     ~mia_forename skolemFOFtoCNF_U $_776 \/
% 0.50/0.65     ~of skolemFOFtoCNF_U $_776 $_775 \/ ~of skolemFOFtoCNF_U $_780 $_779 \/
% 0.50/0.65     ~present skolemFOFtoCNF_X $_782 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_U $_780 \/
% 0.50/0.65     ~woman skolemFOFtoCNF_U $_775 \/
% 0.50/0.65     event (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_779)
% 0.50/0.65       (skolemFOFtoCNF_X6 skolemFOFtoCNF_U $_779)
% 0.50/0.65  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.65     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_782 $_775 \/
% 0.50/0.65     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_775 \/
% 0.50/0.65     ~dance skolemFOFtoCNF_X $_782 \/ ~event skolemFOFtoCNF_X $_782 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_X $_776 \/ ~forename skolemFOFtoCNF_X $_780 \/
% 0.50/0.65     ~man skolemFOFtoCNF_X $_779 \/ ~mia_forename skolemFOFtoCNF_X $_776 \/
% 0.50/0.65     ~of skolemFOFtoCNF_X $_776 $_775 \/ ~of skolemFOFtoCNF_X $_780 $_779 \/
% 0.50/0.65     ~present skolemFOFtoCNF_X $_782 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_X $_780 \/
% 0.50/0.65     ~woman skolemFOFtoCNF_X $_775 \/
% 0.50/0.65     event (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_779)
% 0.50/0.65       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X $_779)
% 0.50/0.65  |- ~agent skolemFOFtoCNF_X $_787 skolemFOFtoCNF_V \/
% 0.50/0.65     ~dance skolemFOFtoCNF_X $_787 \/ ~event skolemFOFtoCNF_X $_787 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_U $_786 \/ ~man skolemFOFtoCNF_U $_785 \/
% 0.50/0.65     ~of skolemFOFtoCNF_U $_786 $_785 \/ ~present skolemFOFtoCNF_X $_787 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_U $_786 \/
% 0.50/0.65     event (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_785)
% 0.50/0.65       (skolemFOFtoCNF_X6 skolemFOFtoCNF_U $_785)
% 0.50/0.65  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.65     ~actual_world skolemFOFtoCNF_X \/
% 0.50/0.65     ~agent skolemFOFtoCNF_X $_795 skolemFOFtoCNF_V \/
% 0.50/0.65     ~dance skolemFOFtoCNF_X $_795 \/ ~event skolemFOFtoCNF_X $_795 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_X $_794 \/ ~man skolemFOFtoCNF_X $_793 \/
% 0.50/0.65     ~of skolemFOFtoCNF_X $_794 $_793 \/ ~present skolemFOFtoCNF_X $_795 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_X $_794 \/
% 0.50/0.65     event (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_793)
% 0.50/0.65       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X $_793)
% 0.50/0.65  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_799 \/
% 0.50/0.65     ~agent skolemFOFtoCNF_X $_806 $_799 \/ ~dance skolemFOFtoCNF_X $_806 \/
% 0.50/0.65     ~event skolemFOFtoCNF_X $_806 \/ ~forename skolemFOFtoCNF_U $_800 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_U $_804 \/ ~man skolemFOFtoCNF_U $_803 \/
% 0.50/0.65     ~mia_forename skolemFOFtoCNF_U $_800 \/
% 0.50/0.65     ~of skolemFOFtoCNF_U $_800 $_799 \/ ~of skolemFOFtoCNF_U $_804 $_803 \/
% 0.50/0.65     ~present skolemFOFtoCNF_X $_806 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_U $_804 \/
% 0.50/0.65     ~woman skolemFOFtoCNF_U $_799 \/
% 0.50/0.65     agent (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_803)
% 0.50/0.65       (skolemFOFtoCNF_X6 skolemFOFtoCNF_U $_803) $_803
% 0.50/0.65  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.65     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_806 $_799 \/
% 0.50/0.65     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_799 \/
% 0.50/0.65     ~dance skolemFOFtoCNF_X $_806 \/ ~event skolemFOFtoCNF_X $_806 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_X $_800 \/ ~forename skolemFOFtoCNF_X $_804 \/
% 0.50/0.65     ~man skolemFOFtoCNF_X $_803 \/ ~mia_forename skolemFOFtoCNF_X $_800 \/
% 0.50/0.65     ~of skolemFOFtoCNF_X $_800 $_799 \/ ~of skolemFOFtoCNF_X $_804 $_803 \/
% 0.50/0.65     ~present skolemFOFtoCNF_X $_806 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_X $_804 \/
% 0.50/0.65     ~woman skolemFOFtoCNF_X $_799 \/
% 0.50/0.65     agent (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_803)
% 0.50/0.65       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X $_803) $_803
% 0.50/0.65  |- ~agent skolemFOFtoCNF_X $_811 skolemFOFtoCNF_V \/
% 0.50/0.65     ~dance skolemFOFtoCNF_X $_811 \/ ~event skolemFOFtoCNF_X $_811 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_U $_810 \/ ~man skolemFOFtoCNF_U $_809 \/
% 0.50/0.65     ~of skolemFOFtoCNF_U $_810 $_809 \/ ~present skolemFOFtoCNF_X $_811 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_U $_810 \/
% 0.50/0.65     agent (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_809)
% 0.50/0.65       (skolemFOFtoCNF_X6 skolemFOFtoCNF_U $_809) $_809
% 0.50/0.65  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.65     ~actual_world skolemFOFtoCNF_X \/
% 0.50/0.65     ~agent skolemFOFtoCNF_X $_819 skolemFOFtoCNF_V \/
% 0.50/0.65     ~dance skolemFOFtoCNF_X $_819 \/ ~event skolemFOFtoCNF_X $_819 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_X $_818 \/ ~man skolemFOFtoCNF_X $_817 \/
% 0.50/0.65     ~of skolemFOFtoCNF_X $_818 $_817 \/ ~present skolemFOFtoCNF_X $_819 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_X $_818 \/
% 0.50/0.65     agent (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_817)
% 0.50/0.65       (skolemFOFtoCNF_X6 skolemFOFtoCNF_X $_817) $_817
% 0.50/0.65  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_Y $_823 \/
% 0.50/0.65     ~agent skolemFOFtoCNF_X $_830 $_823 \/ ~dance skolemFOFtoCNF_X $_830 \/
% 0.50/0.65     ~event skolemFOFtoCNF_X $_830 \/ ~forename skolemFOFtoCNF_U $_824 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_U $_828 \/ ~man skolemFOFtoCNF_U $_827 \/
% 0.50/0.65     ~mia_forename skolemFOFtoCNF_U $_824 \/
% 0.50/0.65     ~of skolemFOFtoCNF_U $_824 $_823 \/ ~of skolemFOFtoCNF_U $_828 $_827 \/
% 0.50/0.65     ~present skolemFOFtoCNF_X $_830 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_U $_828 \/
% 0.50/0.65     ~woman skolemFOFtoCNF_U $_823 \/
% 0.50/0.65     theme skolemFOFtoCNF_U (skolemFOFtoCNF_X5 skolemFOFtoCNF_U $_827)
% 0.50/0.65       (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_827)
% 0.50/0.65  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.65     ~actual_world skolemFOFtoCNF_X \/ ~agent skolemFOFtoCNF_X $_830 $_823 \/
% 0.50/0.65     ~agent skolemFOFtoCNF_X skolemFOFtoCNF_Y $_823 \/
% 0.50/0.65     ~dance skolemFOFtoCNF_X $_830 \/ ~event skolemFOFtoCNF_X $_830 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_X $_824 \/ ~forename skolemFOFtoCNF_X $_828 \/
% 0.50/0.65     ~man skolemFOFtoCNF_X $_827 \/ ~mia_forename skolemFOFtoCNF_X $_824 \/
% 0.50/0.65     ~of skolemFOFtoCNF_X $_824 $_823 \/ ~of skolemFOFtoCNF_X $_828 $_827 \/
% 0.50/0.65     ~present skolemFOFtoCNF_X $_830 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_X $_828 \/
% 0.50/0.65     ~woman skolemFOFtoCNF_X $_823 \/
% 0.50/0.65     theme skolemFOFtoCNF_X (skolemFOFtoCNF_X5 skolemFOFtoCNF_X $_827)
% 0.50/0.65       (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_827)
% 0.50/0.65  |- ~agent skolemFOFtoCNF_X $_835 skolemFOFtoCNF_V \/
% 0.50/0.65     ~dance skolemFOFtoCNF_X $_835 \/ ~event skolemFOFtoCNF_X $_835 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_U $_834 \/ ~man skolemFOFtoCNF_U $_833 \/
% 0.50/0.65     ~of skolemFOFtoCNF_U $_834 $_833 \/ ~present skolemFOFtoCNF_X $_835 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_U $_834 \/
% 0.50/0.65     theme skolemFOFtoCNF_U (skolemFOFtoCNF_X5 skolemFOFtoCNF_U $_833)
% 0.50/0.65       (skolemFOFtoCNF_X4 skolemFOFtoCNF_U $_833)
% 0.50/0.65  |- ~accessible_world skolemFOFtoCNF_X skolemFOFtoCNF_X \/
% 0.50/0.65     ~actual_world skolemFOFtoCNF_X \/
% 0.50/0.65     ~agent skolemFOFtoCNF_X $_843 skolemFOFtoCNF_V \/
% 0.50/0.65     ~dance skolemFOFtoCNF_X $_843 \/ ~event skolemFOFtoCNF_X $_843 \/
% 0.50/0.65     ~forename skolemFOFtoCNF_X $_842 \/ ~man skolemFOFtoCNF_X $_841 \/
% 0.50/0.65     ~of skolemFOFtoCNF_X $_842 $_841 \/ ~present skolemFOFtoCNF_X $_843 \/
% 0.50/0.65     ~vincent_forename skolemFOFtoCNF_X $_842 \/
% 0.50/0.65     theme skolemFOFtoCNF_X (skolemFOFtoCNF_X5 skolemFOFtoCNF_X $_841)
% 0.50/0.65       (skolemFOFtoCNF_X4 skolemFOFtoCNF_X $_841)
% 0.50/0.65  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.50/0.65  
%------------------------------------------------------------------------------