↑ Up

Metis---2.4.SAT-Sat.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : NLP013-1 : TPTP v8.1.0. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n007.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:13:47 EDT 2022

% Result   : Satisfiable 0.18s 0.48s
% Output   : Saturation 0.18s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : NLP013-1 : TPTP v8.1.0. Released v2.4.0.
% 0.07/0.12  % Command  : metis --show proof --show saturation %s
% 0.12/0.33  % Computer : n007.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33  % CPULimit : 300
% 0.12/0.33  % WCLimit  : 600
% 0.12/0.33  % DateTime : Fri Jul  1 11:36:09 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 0.12/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.18/0.48  % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.48  
% 0.18/0.48  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.48  |- hollywood skc29
% 0.18/0.48  |- event skc28
% 0.18/0.48  |- chevy skc27
% 0.18/0.48  |- lonely skc26
% 0.18/0.48  |- seat skc25
% 0.18/0.48  |- young skc24
% 0.18/0.48  |- fellow skc23
% 0.18/0.48  |- city skc22
% 0.18/0.48  |- event skc21
% 0.18/0.48  |- lonely skc20
% 0.18/0.48  |- chevy skc19
% 0.18/0.48  |- seat skc18
% 0.18/0.48  |- front skc17
% 0.18/0.48  |- fellow skc16
% 0.18/0.48  |- young skc15
% 0.18/0.48  |- ssSkC0 \/ street skc26
% 0.18/0.48  |- ssSkC0 \/ way skc26
% 0.18/0.48  |- old skc27 \/ ssSkC0
% 0.18/0.48  |- dirty skc27 \/ ssSkC0
% 0.18/0.48  |- ssSkC0 \/ white skc27
% 0.18/0.48  |- car skc27 \/ ssSkC0
% 0.18/0.48  |- city skc29 \/ ssSkC0
% 0.18/0.48  |- ssSkC0 \/ young skc23
% 0.18/0.48  |- man skc23 \/ ssSkC0
% 0.18/0.48  |- fellow skc24 \/ ssSkC0
% 0.18/0.48  |- man skc24 \/ ssSkC0
% 0.18/0.48  |- front skc25 \/ ssSkC0
% 0.18/0.48  |- furniture skc25 \/ ssSkC0
% 0.18/0.48  |- ~ssSkC0 \/ old skc19
% 0.18/0.48  |- ~ssSkC0 \/ dirty skc19
% 0.18/0.48  |- ~ssSkC0 \/ white skc19
% 0.18/0.48  |- ~ssSkC0 \/ car skc19
% 0.18/0.48  |- ~ssSkC0 \/ street skc20
% 0.18/0.48  |- ~ssSkC0 \/ way skc20
% 0.18/0.48  |- ~ssSkC0 \/ hollywood skc22
% 0.18/0.49  |- ~ssSkC0 \/ fellow skc15
% 0.18/0.49  |- ~ssSkC0 \/ man skc15
% 0.18/0.49  |- ~ssSkC0 \/ front skc18
% 0.18/0.49  |- ~ssSkC0 \/ furniture skc18
% 0.18/0.49  |- ~ssSkC0 \/ young skc16
% 0.18/0.49  |- ~ssSkC0 \/ man skc16
% 0.18/0.49  |- ~ssSkC0 \/ seat skc17
% 0.18/0.49  |- ~ssSkC0 \/ furniture skc17
% 0.18/0.49  |- barrel skc28 skc27 \/ ssSkC0
% 0.18/0.49  |- down skc28 skc26 \/ ssSkC0
% 0.18/0.49  |- in skc28 skc29 \/ ssSkC0
% 0.18/0.49  |- in skc23 skc25 \/ ssSkC0
% 0.18/0.49  |- in skc24 skc25 \/ ssSkC0
% 0.18/0.49  |- ~ssSkC0 \/ down skc21 skc20
% 0.18/0.49  |- ~ssSkC0 \/ barrel skc21 skc19
% 0.18/0.49  |- ~ssSkC0 \/ in skc21 skc22
% 0.18/0.49  |- ~ssSkC0 \/ in skc15 skc18
% 0.18/0.49  |- ~ssSkC0 \/ in skc16 skc17
% 0.18/0.49  |- ~(skc24 = skc23) \/ ssSkC0
% 0.18/0.49  |- ~(skc16 = skc15) \/ ~ssSkC0
% 0.18/0.49  |- ~barrel $W $V \/ ~car $V \/ ~chevy $V \/ ~city $X \/ ~dirty $V \/
% 0.18/0.49     ~down $W $U \/ ~event $W \/ ~fellow $Y \/ ~fellow $Z \/ ~front $X1 \/
% 0.18/0.49     ~furniture $X1 \/ ~hollywood $X \/ ~in $W $X \/ ~in $Y $X1 \/
% 0.18/0.49     ~in $Z $X1 \/ ~lonely $U \/ ~man $Y \/ ~man $Z \/ ~old $V \/
% 0.18/0.49     ~seat $X1 \/ ~ssSkC0 \/ ~street $U \/ ~way $U \/ ~white $V \/
% 0.18/0.49     ~young $Y \/ ~young $Z \/ $Z = $Y
% 0.18/0.49  |- ~barrel $W $U \/ ~car $U \/ ~chevy $U \/ ~city $X \/ ~dirty $U \/
% 0.18/0.49     ~down $W $V \/ ~event $W \/ ~fellow $X1 \/ ~fellow $Y \/ ~front $X2 \/
% 0.18/0.49     ~front $Z \/ ~furniture $X2 \/ ~furniture $Z \/ ~hollywood $X \/
% 0.18/0.49     ~in $W $X \/ ~in $X1 $X2 \/ ~in $Y $Z \/ ~lonely $V \/ ~man $X1 \/
% 0.18/0.49     ~man $Y \/ ~old $U \/ ~seat $X2 \/ ~seat $Z \/ ~street $V \/ ~way $V \/
% 0.18/0.49     ~white $U \/ ~young $X1 \/ ~young $Y \/ $X1 = $Y \/ ssSkC0
% 0.18/0.49  |- ~barrel $Y $V \/ ~car $V \/ ~chevy $V \/ ~city $X1 \/ ~dirty $V \/
% 0.18/0.49     ~down $Y $U \/ ~event $Y \/ ~fellow $Y \/ ~fellow $Z \/ ~front $X1 \/
% 0.18/0.49     ~furniture $X1 \/ ~hollywood $X1 \/ ~in $Y $X1 \/ ~in $Z $X1 \/
% 0.18/0.49     ~lonely $U \/ ~man $Y \/ ~man $Z \/ ~old $V \/ ~seat $X1 \/ ~ssSkC0 \/
% 0.18/0.49     ~street $U \/ ~way $U \/ ~white $V \/ ~young $Y \/ ~young $Z \/ $Z = $Y
% 0.18/0.49  |- ~barrel $X1 $U \/ ~car $U \/ ~chevy $U \/ ~city $X2 \/ ~dirty $U \/
% 0.18/0.49     ~down $X1 $V \/ ~event $X1 \/ ~fellow $X1 \/ ~fellow $Y \/ ~front $X2 \/
% 0.18/0.49     ~front $Z \/ ~furniture $X2 \/ ~furniture $Z \/ ~hollywood $X2 \/
% 0.18/0.49     ~in $X1 $X2 \/ ~in $Y $Z \/ ~lonely $V \/ ~man $X1 \/ ~man $Y \/
% 0.18/0.49     ~old $U \/ ~seat $X2 \/ ~seat $Z \/ ~street $V \/ ~way $V \/
% 0.18/0.49     ~white $U \/ ~young $X1 \/ ~young $Y \/ $X1 = $Y \/ ssSkC0
% 0.18/0.49  |- ~barrel skc23 $_5 \/ ~car $_5 \/ ~chevy $_5 \/ ~city skc25 \/
% 0.18/0.49     ~dirty $_5 \/ ~down skc23 $_6 \/ ~event skc23 \/ ~fellow $_9 \/
% 0.18/0.49     ~front $_10 \/ ~front skc25 \/ ~furniture $_10 \/ ~furniture skc25 \/
% 0.18/0.49     ~hollywood skc25 \/ ~in $_9 $_10 \/ ~lonely $_6 \/ ~man $_9 \/
% 0.18/0.49     ~man skc23 \/ ~old $_5 \/ ~seat $_10 \/ ~street $_6 \/ ~way $_6 \/
% 0.18/0.49     ~white $_5 \/ ~young $_9 \/ ~young skc23 \/ skc23 = $_9 \/ ssSkC0
% 0.18/0.49  |- ~barrel skc24 $_5 \/ ~car $_5 \/ ~chevy $_5 \/ ~city skc25 \/
% 0.18/0.49     ~dirty $_5 \/ ~down skc24 $_6 \/ ~event skc24 \/ ~fellow $_9 \/
% 0.18/0.49     ~fellow skc24 \/ ~front $_10 \/ ~front skc25 \/ ~furniture $_10 \/
% 0.18/0.49     ~furniture skc25 \/ ~hollywood skc25 \/ ~in $_9 $_10 \/ ~lonely $_6 \/
% 0.18/0.49     ~man $_9 \/ ~man skc24 \/ ~old $_5 \/ ~seat $_10 \/ ~street $_6 \/
% 0.18/0.49     ~way $_6 \/ ~white $_5 \/ ~young $_9 \/ skc24 = $_9 \/ ssSkC0
% 0.18/0.49  |- ~barrel skc28 $_5 \/ ~car $_5 \/ ~chevy $_5 \/ ~city skc29 \/
% 0.18/0.49     ~dirty $_5 \/ ~down skc28 $_6 \/ ~fellow $_9 \/ ~fellow skc28 \/
% 0.18/0.49     ~front $_10 \/ ~front skc29 \/ ~furniture $_10 \/ ~furniture skc29 \/
% 0.18/0.49     ~in $_9 $_10 \/ ~lonely $_6 \/ ~man $_9 \/ ~man skc28 \/ ~old $_5 \/
% 0.18/0.49     ~seat $_10 \/ ~seat skc29 \/ ~street $_6 \/ ~way $_6 \/ ~white $_5 \/
% 0.18/0.49     ~young $_9 \/ ~young skc28 \/ skc28 = $_9 \/ ssSkC0
% 0.18/0.49  |- ~barrel $_7 $_5 \/ ~car $_5 \/ ~chevy $_5 \/ ~city $_8 \/ ~dirty $_5 \/
% 0.18/0.49     ~down $_7 $_6 \/ ~event $_7 \/ ~fellow $_7 \/ ~front $_8 \/
% 0.18/0.49     ~front skc25 \/ ~furniture $_8 \/ ~furniture skc25 \/ ~hollywood $_8 \/
% 0.18/0.49     ~in $_7 $_8 \/ ~lonely $_6 \/ ~man $_7 \/ ~man skc23 \/ ~old $_5 \/
% 0.18/0.49     ~seat $_8 \/ ~street $_6 \/ ~way $_6 \/ ~white $_5 \/ ~young $_7 \/
% 0.18/0.49     ~young skc23 \/ $_7 = skc23 \/ ssSkC0
% 0.18/0.49  |- ~barrel $_7 $_5 \/ ~car $_5 \/ ~chevy $_5 \/ ~city $_8 \/ ~dirty $_5 \/
% 0.18/0.49     ~down $_7 $_6 \/ ~event $_7 \/ ~fellow $_7 \/ ~fellow skc24 \/
% 0.18/0.49     ~front $_8 \/ ~front skc25 \/ ~furniture $_8 \/ ~furniture skc25 \/
% 0.18/0.49     ~hollywood $_8 \/ ~in $_7 $_8 \/ ~lonely $_6 \/ ~man $_7 \/
% 0.18/0.49     ~man skc24 \/ ~old $_5 \/ ~seat $_8 \/ ~street $_6 \/ ~way $_6 \/
% 0.18/0.49     ~white $_5 \/ ~young $_7 \/ $_7 = skc24 \/ ssSkC0
% 0.18/0.49  |- ~barrel $_7 $_5 \/ ~car $_5 \/ ~chevy $_5 \/ ~city $_8 \/ ~dirty $_5 \/
% 0.18/0.49     ~down $_7 $_6 \/ ~event $_7 \/ ~fellow $_7 \/ ~fellow skc28 \/
% 0.18/0.49     ~front $_8 \/ ~front skc29 \/ ~furniture $_8 \/ ~furniture skc29 \/
% 0.18/0.49     ~hollywood $_8 \/ ~in $_7 $_8 \/ ~lonely $_6 \/ ~man $_7 \/
% 0.18/0.49     ~man skc28 \/ ~old $_5 \/ ~seat $_8 \/ ~seat skc29 \/ ~street $_6 \/
% 0.18/0.49     ~way $_6 \/ ~white $_5 \/ ~young $_7 \/ ~young skc28 \/ $_7 = skc28 \/
% 0.18/0.49     ssSkC0
% 0.18/0.49  |- ~barrel skc28 $_11 \/ ~car $_11 \/ ~chevy $_11 \/ ~city skc29 \/
% 0.18/0.49     ~dirty $_11 \/ ~down skc28 $_12 \/ ~fellow skc24 \/ ~fellow skc28 \/
% 0.18/0.49     ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/ ~furniture skc29 \/
% 0.18/0.49     ~lonely $_12 \/ ~man skc24 \/ ~man skc28 \/ ~old $_11 \/ ~seat skc29 \/
% 0.18/0.49     ~street $_12 \/ ~way $_12 \/ ~white $_11 \/ ~young skc28 \/
% 0.18/0.49     skc28 = skc24 \/ ssSkC0
% 0.18/0.49  |- ~barrel skc28 $_17 \/ ~car $_17 \/ ~chevy $_17 \/ ~city skc29 \/
% 0.18/0.49     ~dirty $_17 \/ ~fellow skc24 \/ ~fellow skc28 \/ ~front skc25 \/
% 0.18/0.49     ~front skc29 \/ ~furniture skc25 \/ ~furniture skc29 \/ ~man skc24 \/
% 0.18/0.49     ~man skc28 \/ ~old $_17 \/ ~seat skc29 \/ ~street skc26 \/ ~way skc26 \/
% 0.18/0.49     ~white $_17 \/ ~young skc28 \/ skc28 = skc24 \/ ssSkC0
% 0.18/0.49  |- ~car skc27 \/ ~city skc29 \/ ~dirty skc27 \/ ~fellow skc24 \/
% 0.18/0.49     ~fellow skc28 \/ ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/
% 0.18/0.49     ~furniture skc29 \/ ~man skc24 \/ ~man skc28 \/ ~old skc27 \/
% 0.18/0.49     ~seat skc29 \/ ~street skc26 \/ ~way skc26 \/ ~white skc27 \/
% 0.18/0.49     ~young skc28 \/ skc28 = skc24 \/ ssSkC0
% 0.18/0.49  |- ~barrel skc28 $_20 \/ ~car $_20 \/ ~chevy $_20 \/ ~city skc29 \/
% 0.18/0.49     ~dirty $_20 \/ ~down skc28 $_21 \/ ~fellow skc28 \/ ~front skc25 \/
% 0.18/0.49     ~front skc29 \/ ~furniture skc25 \/ ~furniture skc29 \/ ~lonely $_21 \/
% 0.18/0.49     ~man skc23 \/ ~man skc28 \/ ~old $_20 \/ ~seat skc29 \/ ~street $_21 \/
% 0.18/0.49     ~way $_21 \/ ~white $_20 \/ ~young skc23 \/ ~young skc28 \/
% 0.18/0.49     skc28 = skc23 \/ ssSkC0
% 0.18/0.49  |- ~barrel skc28 $_26 \/ ~car $_26 \/ ~chevy $_26 \/ ~city skc29 \/
% 0.18/0.49     ~dirty $_26 \/ ~fellow skc28 \/ ~front skc25 \/ ~front skc29 \/
% 0.18/0.49     ~furniture skc25 \/ ~furniture skc29 \/ ~man skc23 \/ ~man skc28 \/
% 0.18/0.49     ~old $_26 \/ ~seat skc29 \/ ~street skc26 \/ ~way skc26 \/
% 0.18/0.49     ~white $_26 \/ ~young skc23 \/ ~young skc28 \/ skc28 = skc23 \/ ssSkC0
% 0.18/0.49  |- ~car skc27 \/ ~city skc29 \/ ~dirty skc27 \/ ~fellow skc28 \/
% 0.18/0.49     ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/ ~furniture skc29 \/
% 0.18/0.49     ~man skc23 \/ ~man skc28 \/ ~old skc27 \/ ~seat skc29 \/
% 0.18/0.49     ~street skc26 \/ ~way skc26 \/ ~white skc27 \/ ~young skc23 \/
% 0.18/0.49     ~young skc28 \/ skc28 = skc23 \/ ssSkC0
% 0.18/0.49  |- ~barrel skc24 $_34 \/ ~car $_34 \/ ~chevy $_34 \/ ~city skc25 \/
% 0.18/0.49     ~dirty $_34 \/ ~down skc24 $_35 \/ ~event skc24 \/ ~fellow skc24 \/
% 0.18/0.49     ~fellow skc28 \/ ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/
% 0.18/0.49     ~furniture skc29 \/ ~hollywood skc25 \/ ~lonely $_35 \/ ~man skc24 \/
% 0.18/0.49     ~man skc28 \/ ~old $_34 \/ ~seat skc29 \/ ~street $_35 \/ ~way $_35 \/
% 0.18/0.49     ~white $_34 \/ ~young skc28 \/ skc24 = skc28 \/ ssSkC0
% 0.18/0.49  |- ~barrel skc23 $_40 \/ ~car $_40 \/ ~chevy $_40 \/ ~city skc25 \/
% 0.18/0.49     ~dirty $_40 \/ ~down skc23 $_41 \/ ~event skc23 \/ ~fellow skc28 \/
% 0.18/0.49     ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/ ~furniture skc29 \/
% 0.18/0.49     ~hollywood skc25 \/ ~lonely $_41 \/ ~man skc23 \/ ~man skc28 \/
% 0.18/0.49     ~old $_40 \/ ~seat skc29 \/ ~street $_41 \/ ~way $_41 \/ ~white $_40 \/
% 0.18/0.49     ~young skc23 \/ ~young skc28 \/ skc23 = skc28 \/ ssSkC0
% 0.18/0.49  |- ~barrel skc23 $_56 \/ ~car $_56 \/ ~chevy $_56 \/ ~city skc25 \/
% 0.18/0.49     ~dirty $_56 \/ ~down skc23 $_57 \/ ~event skc23 \/ ~fellow $_60 \/
% 0.18/0.49     ~fellow $_62 \/ ~front $_61 \/ ~front $_63 \/ ~furniture $_61 \/
% 0.18/0.49     ~furniture $_63 \/ ~hollywood skc25 \/ ~in $_60 $_61 \/ ~in $_62 $_63 \/
% 0.18/0.49     ~lonely $_57 \/ ~man $_60 \/ ~man $_62 \/ ~old $_56 \/ ~seat $_61 \/
% 0.18/0.49     ~seat $_63 \/ ~street $_57 \/ ~way $_57 \/ ~white $_56 \/ ~young $_60 \/
% 0.18/0.49     ~young $_62 \/ $_60 = $_62 \/ ssSkC0
% 0.18/0.49  |- ~barrel skc24 $_56 \/ ~car $_56 \/ ~chevy $_56 \/ ~city skc25 \/
% 0.18/0.49     ~dirty $_56 \/ ~down skc24 $_57 \/ ~event skc24 \/ ~fellow $_60 \/
% 0.18/0.49     ~fellow $_62 \/ ~front $_61 \/ ~front $_63 \/ ~furniture $_61 \/
% 0.18/0.49     ~furniture $_63 \/ ~hollywood skc25 \/ ~in $_60 $_61 \/ ~in $_62 $_63 \/
% 0.18/0.49     ~lonely $_57 \/ ~man $_60 \/ ~man $_62 \/ ~old $_56 \/ ~seat $_61 \/
% 0.18/0.49     ~seat $_63 \/ ~street $_57 \/ ~way $_57 \/ ~white $_56 \/ ~young $_60 \/
% 0.18/0.49     ~young $_62 \/ $_60 = $_62 \/ ssSkC0
% 0.18/0.49  |- ~barrel skc28 $_56 \/ ~car $_56 \/ ~chevy $_56 \/ ~city skc29 \/
% 0.18/0.49     ~dirty $_56 \/ ~down skc28 $_57 \/ ~fellow $_60 \/ ~fellow $_62 \/
% 0.18/0.49     ~front $_61 \/ ~front $_63 \/ ~furniture $_61 \/ ~furniture $_63 \/
% 0.18/0.49     ~in $_60 $_61 \/ ~in $_62 $_63 \/ ~lonely $_57 \/ ~man $_60 \/
% 0.18/0.49     ~man $_62 \/ ~old $_56 \/ ~seat $_61 \/ ~seat $_63 \/ ~street $_57 \/
% 0.18/0.49     ~way $_57 \/ ~white $_56 \/ ~young $_60 \/ ~young $_62 \/ $_60 = $_62 \/
% 0.18/0.49     ssSkC0
% 0.18/0.49  |- ~barrel $_58 $_56 \/ ~car $_56 \/ ~chevy $_56 \/ ~city $_59 \/
% 0.18/0.49     ~dirty $_56 \/ ~down $_58 $_57 \/ ~event $_58 \/ ~fellow $_62 \/
% 0.18/0.49     ~front $_63 \/ ~front skc25 \/ ~furniture $_63 \/ ~furniture skc25 \/
% 0.18/0.49     ~hollywood $_59 \/ ~in $_58 $_59 \/ ~in $_62 $_63 \/ ~lonely $_57 \/
% 0.18/0.49     ~man $_62 \/ ~man skc23 \/ ~old $_56 \/ ~seat $_63 \/ ~street $_57 \/
% 0.18/0.49     ~way $_57 \/ ~white $_56 \/ ~young $_62 \/ ~young skc23 \/
% 0.18/0.49     skc23 = $_62 \/ ssSkC0
% 0.18/0.49  |- ~barrel $_58 $_56 \/ ~car $_56 \/ ~chevy $_56 \/ ~city $_59 \/
% 0.18/0.49     ~dirty $_56 \/ ~down $_58 $_57 \/ ~event $_58 \/ ~fellow $_62 \/
% 0.18/0.49     ~fellow skc24 \/ ~front $_63 \/ ~front skc25 \/ ~furniture $_63 \/
% 0.18/0.49     ~furniture skc25 \/ ~hollywood $_59 \/ ~in $_58 $_59 \/ ~in $_62 $_63 \/
% 0.18/0.49     ~lonely $_57 \/ ~man $_62 \/ ~man skc24 \/ ~old $_56 \/ ~seat $_63 \/
% 0.18/0.49     ~street $_57 \/ ~way $_57 \/ ~white $_56 \/ ~young $_62 \/
% 0.18/0.49     skc24 = $_62 \/ ssSkC0
% 0.18/0.49  |- ~barrel $_58 $_56 \/ ~car $_56 \/ ~chevy $_56 \/ ~city $_59 \/
% 0.18/0.49     ~dirty $_56 \/ ~down $_58 $_57 \/ ~event $_58 \/ ~fellow $_62 \/
% 0.18/0.49     ~fellow skc28 \/ ~front $_63 \/ ~front skc29 \/ ~furniture $_63 \/
% 0.18/0.49     ~furniture skc29 \/ ~hollywood $_59 \/ ~in $_58 $_59 \/ ~in $_62 $_63 \/
% 0.18/0.49     ~lonely $_57 \/ ~man $_62 \/ ~man skc28 \/ ~old $_56 \/ ~seat $_63 \/
% 0.18/0.49     ~seat skc29 \/ ~street $_57 \/ ~way $_57 \/ ~white $_56 \/
% 0.18/0.49     ~young $_62 \/ ~young skc28 \/ skc28 = $_62 \/ ssSkC0
% 0.18/0.49  |- ~barrel skc23 $_64 \/ ~car $_64 \/ ~chevy $_64 \/ ~city skc25 \/
% 0.18/0.49     ~dirty $_64 \/ ~down skc23 $_65 \/ ~event skc23 \/ ~fellow $_68 \/
% 0.18/0.49     ~fellow skc24 \/ ~front $_69 \/ ~front skc25 \/ ~furniture $_69 \/
% 0.18/0.49     ~furniture skc25 \/ ~hollywood skc25 \/ ~in $_68 $_69 \/ ~lonely $_65 \/
% 0.18/0.49     ~man $_68 \/ ~man skc24 \/ ~old $_64 \/ ~seat $_69 \/ ~street $_65 \/
% 0.18/0.49     ~way $_65 \/ ~white $_64 \/ ~young $_68 \/ skc24 = $_68 \/ ssSkC0
% 0.18/0.49  |- ~barrel skc28 $_64 \/ ~car $_64 \/ ~chevy $_64 \/ ~city skc29 \/
% 0.18/0.49     ~dirty $_64 \/ ~down skc28 $_65 \/ ~fellow $_68 \/ ~fellow skc24 \/
% 0.18/0.49     ~front $_69 \/ ~front skc25 \/ ~furniture $_69 \/ ~furniture skc25 \/
% 0.18/0.49     ~in $_68 $_69 \/ ~lonely $_65 \/ ~man $_68 \/ ~man skc24 \/ ~old $_64 \/
% 0.18/0.49     ~seat $_69 \/ ~street $_65 \/ ~way $_65 \/ ~white $_64 \/ ~young $_68 \/
% 0.18/0.49     skc24 = $_68 \/ ssSkC0
% 0.18/0.49  |- ~barrel $_66 $_64 \/ ~car $_64 \/ ~chevy $_64 \/ ~city $_67 \/
% 0.18/0.49     ~dirty $_64 \/ ~down $_66 $_65 \/ ~event $_66 \/ ~fellow skc24 \/
% 0.18/0.49     ~fellow skc28 \/ ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/
% 0.18/0.49     ~furniture skc29 \/ ~hollywood $_67 \/ ~in $_66 $_67 \/ ~lonely $_65 \/
% 0.18/0.49     ~man skc24 \/ ~man skc28 \/ ~old $_64 \/ ~seat skc29 \/ ~street $_65 \/
% 0.18/0.49     ~way $_65 \/ ~white $_64 \/ ~young skc28 \/ skc24 = skc28 \/ ssSkC0
% 0.18/0.49  |- skc24 = skc23 \/ ssSkC0
% 0.18/0.49  |- ~(skc16 = skc15) \/ skc24 = skc23
% 0.18/0.49  |- skc24 = skc23 \/ in skc16 skc17
% 0.18/0.49  |- skc24 = skc23 \/ in skc15 skc18
% 0.18/0.49  |- skc24 = skc23 \/ in skc21 skc22
% 0.18/0.49  |- skc24 = skc23 \/ barrel skc21 skc19
% 0.18/0.49  |- skc24 = skc23 \/ down skc21 skc20
% 0.18/0.49  |- skc24 = skc23 \/ furniture skc17
% 0.18/0.49  |- skc24 = skc23 \/ seat skc17
% 0.18/0.49  |- skc24 = skc23 \/ man skc16
% 0.18/0.49  |- skc24 = skc23 \/ young skc16
% 0.18/0.49  |- skc24 = skc23 \/ furniture skc18
% 0.18/0.49  |- skc24 = skc23 \/ front skc18
% 0.18/0.49  |- skc24 = skc23 \/ man skc15
% 0.18/0.49  |- skc24 = skc23 \/ fellow skc15
% 0.18/0.49  |- skc24 = skc23 \/ hollywood skc22
% 0.18/0.49  |- skc24 = skc23 \/ way skc20
% 0.18/0.49  |- skc24 = skc23 \/ street skc20
% 0.18/0.49  |- skc24 = skc23 \/ car skc19
% 0.18/0.49  |- skc24 = skc23 \/ white skc19
% 0.18/0.49  |- skc24 = skc23 \/ dirty skc19
% 0.18/0.49  |- skc24 = skc23 \/ old skc19
% 0.18/0.49  |- ~barrel $W $V \/ ~car $V \/ ~chevy $V \/ ~city $X \/ ~dirty $V \/
% 0.18/0.49     ~down $W $U \/ ~event $W \/ ~fellow $Y \/ ~furniture skc17 \/
% 0.18/0.49     ~hollywood $X \/ ~in $W $X \/ ~in $Y skc17 \/ ~lonely $U \/ ~man $Y \/
% 0.18/0.49     ~man skc16 \/ ~old $V \/ ~seat skc17 \/ ~ssSkC0 \/ ~street $U \/
% 0.18/0.49     ~way $U \/ ~white $V \/ ~young $Y \/ ~young skc16 \/ skc16 = $Y \/
% 0.18/0.49     skc24 = skc23
% 0.18/0.49  |- ~barrel skc16 $V \/ ~car $V \/ ~chevy $V \/ ~city skc17 \/ ~dirty $V \/
% 0.18/0.49     ~down skc16 $U \/ ~event skc16 \/ ~fellow $Y \/ ~fellow $Z \/
% 0.18/0.49     ~front $X1 \/ ~furniture $X1 \/ ~hollywood skc17 \/ ~in $Y $X1 \/
% 0.18/0.49     ~in $Z $X1 \/ ~lonely $U \/ ~man $Y \/ ~man $Z \/ ~old $V \/
% 0.18/0.49     ~seat $X1 \/ ~ssSkC0 \/ ~street $U \/ ~way $U \/ ~white $V \/
% 0.18/0.49     ~young $Y \/ ~young $Z \/ $Z = $Y \/ skc24 = skc23
% 0.18/0.49  |- ~barrel $Y $V \/ ~car $V \/ ~chevy $V \/ ~city skc17 \/ ~dirty $V \/
% 0.18/0.49     ~down $Y $U \/ ~event $Y \/ ~fellow $Y \/ ~furniture skc17 \/
% 0.18/0.49     ~hollywood skc17 \/ ~in $Y skc17 \/ ~lonely $U \/ ~man $Y \/
% 0.18/0.49     ~man skc16 \/ ~old $V \/ ~seat skc17 \/ ~ssSkC0 \/ ~street $U \/
% 0.18/0.49     ~way $U \/ ~white $V \/ ~young $Y \/ ~young skc16 \/ skc16 = $Y \/
% 0.18/0.49     skc24 = skc23
% 0.18/0.49  |- ~barrel skc16 $V \/ ~car $V \/ ~chevy $V \/ ~city skc17 \/ ~dirty $V \/
% 0.18/0.49     ~down skc16 $U \/ ~event skc16 \/ ~fellow $Z \/ ~furniture skc17 \/
% 0.18/0.49     ~hollywood skc17 \/ ~in $Z skc17 \/ ~lonely $U \/ ~man $Z \/
% 0.18/0.49     ~man skc16 \/ ~old $V \/ ~seat skc17 \/ ~ssSkC0 \/ ~street $U \/
% 0.18/0.49     ~way $U \/ ~white $V \/ ~young $Z \/ ~young skc16 \/ $Z = skc16 \/
% 0.18/0.49     skc24 = skc23
% 0.18/0.49  |- ~barrel $W $V \/ ~car $V \/ ~chevy $V \/ ~city $X \/ ~dirty $V \/
% 0.18/0.49     ~down $W $U \/ ~event $W \/ ~fellow $Y \/ ~fellow skc15 \/
% 0.18/0.49     ~front skc18 \/ ~furniture skc18 \/ ~hollywood $X \/ ~in $W $X \/
% 0.18/0.49     ~in $Y skc18 \/ ~lonely $U \/ ~man $Y \/ ~man skc15 \/ ~old $V \/
% 0.18/0.49     ~ssSkC0 \/ ~street $U \/ ~way $U \/ ~white $V \/ ~young $Y \/
% 0.18/0.49     skc15 = $Y \/ skc24 = skc23
% 0.18/0.49  |- ~barrel skc15 $V \/ ~car $V \/ ~chevy $V \/ ~city skc18 \/ ~dirty $V \/
% 0.18/0.49     ~down skc15 $U \/ ~event skc15 \/ ~fellow $Y \/ ~fellow $Z \/
% 0.18/0.49     ~front $X1 \/ ~furniture $X1 \/ ~hollywood skc18 \/ ~in $Y $X1 \/
% 0.18/0.49     ~in $Z $X1 \/ ~lonely $U \/ ~man $Y \/ ~man $Z \/ ~old $V \/
% 0.18/0.49     ~seat $X1 \/ ~ssSkC0 \/ ~street $U \/ ~way $U \/ ~white $V \/
% 0.18/0.49     ~young $Y \/ ~young $Z \/ $Z = $Y \/ skc24 = skc23
% 0.18/0.49  |- ~barrel $Y $V \/ ~car $V \/ ~chevy $V \/ ~city skc18 \/ ~dirty $V \/
% 0.18/0.49     ~down $Y $U \/ ~event $Y \/ ~fellow $Y \/ ~fellow skc15 \/
% 0.18/0.49     ~front skc18 \/ ~furniture skc18 \/ ~hollywood skc18 \/ ~in $Y skc18 \/
% 0.18/0.49     ~lonely $U \/ ~man $Y \/ ~man skc15 \/ ~old $V \/ ~ssSkC0 \/
% 0.18/0.49     ~street $U \/ ~way $U \/ ~white $V \/ ~young $Y \/ skc15 = $Y \/
% 0.18/0.49     skc24 = skc23
% 0.18/0.49  |- ~barrel skc15 $V \/ ~car $V \/ ~chevy $V \/ ~city skc18 \/ ~dirty $V \/
% 0.18/0.49     ~down skc15 $U \/ ~event skc15 \/ ~fellow $Z \/ ~fellow skc15 \/
% 0.18/0.49     ~front skc18 \/ ~furniture skc18 \/ ~hollywood skc18 \/ ~in $Z skc18 \/
% 0.18/0.49     ~lonely $U \/ ~man $Z \/ ~man skc15 \/ ~old $V \/ ~ssSkC0 \/
% 0.18/0.49     ~street $U \/ ~way $U \/ ~white $V \/ ~young $Z \/ $Z = skc15 \/
% 0.18/0.49     skc24 = skc23
% 0.18/0.49  |- ~barrel $W $V \/ ~car $V \/ ~chevy $V \/ ~city $X \/ ~dirty $V \/
% 0.18/0.49     ~down $W $U \/ ~event $W \/ ~fellow $Y \/ ~fellow skc21 \/
% 0.18/0.49     ~front skc22 \/ ~furniture skc22 \/ ~hollywood $X \/ ~in $W $X \/
% 0.18/0.49     ~in $Y skc22 \/ ~lonely $U \/ ~man $Y \/ ~man skc21 \/ ~old $V \/
% 0.18/0.49     ~seat skc22 \/ ~ssSkC0 \/ ~street $U \/ ~way $U \/ ~white $V \/
% 0.18/0.49     ~young $Y \/ ~young skc21 \/ skc21 = $Y \/ skc24 = skc23
% 0.18/0.50  |- ~barrel skc21 $V \/ ~car $V \/ ~chevy $V \/ ~dirty $V \/
% 0.18/0.50     ~down skc21 $U \/ ~fellow $Y \/ ~fellow $Z \/ ~front $X1 \/
% 0.18/0.50     ~furniture $X1 \/ ~hollywood skc22 \/ ~in $Y $X1 \/ ~in $Z $X1 \/
% 0.18/0.50     ~lonely $U \/ ~man $Y \/ ~man $Z \/ ~old $V \/ ~seat $X1 \/ ~ssSkC0 \/
% 0.18/0.50     ~street $U \/ ~way $U \/ ~white $V \/ ~young $Y \/ ~young $Z \/
% 0.18/0.50     $Z = $Y \/ skc24 = skc23
% 0.18/0.50  |- ~barrel $Y $V \/ ~car $V \/ ~chevy $V \/ ~dirty $V \/ ~down $Y $U \/
% 0.18/0.50     ~event $Y \/ ~fellow $Y \/ ~fellow skc21 \/ ~front skc22 \/
% 0.18/0.50     ~furniture skc22 \/ ~hollywood skc22 \/ ~in $Y skc22 \/ ~lonely $U \/
% 0.18/0.50     ~man $Y \/ ~man skc21 \/ ~old $V \/ ~seat skc22 \/ ~ssSkC0 \/
% 0.18/0.50     ~street $U \/ ~way $U \/ ~white $V \/ ~young $Y \/ ~young skc21 \/
% 0.18/0.50     skc21 = $Y \/ skc24 = skc23
% 0.18/0.50  |- ~barrel skc21 $V \/ ~car $V \/ ~chevy $V \/ ~dirty $V \/
% 0.18/0.50     ~down skc21 $U \/ ~fellow $Z \/ ~fellow skc21 \/ ~front skc22 \/
% 0.18/0.50     ~furniture skc22 \/ ~hollywood skc22 \/ ~in $Z skc22 \/ ~lonely $U \/
% 0.18/0.50     ~man $Z \/ ~man skc21 \/ ~old $V \/ ~seat skc22 \/ ~ssSkC0 \/
% 0.18/0.50     ~street $U \/ ~way $U \/ ~white $V \/ ~young $Z \/ ~young skc21 \/
% 0.18/0.50     $Z = skc21 \/ skc24 = skc23
% 0.18/0.50  |- ~barrel skc23 $_81 \/ ~car $_81 \/ ~chevy $_81 \/ ~city skc25 \/
% 0.18/0.50     ~dirty $_81 \/ ~down skc23 $_82 \/ ~event skc23 \/ ~fellow skc24 \/
% 0.18/0.50     ~fellow skc28 \/ ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/
% 0.18/0.50     ~furniture skc29 \/ ~hollywood skc25 \/ ~lonely $_82 \/ ~man skc24 \/
% 0.18/0.50     ~man skc28 \/ ~old $_81 \/ ~seat skc29 \/ ~street $_82 \/ ~way $_82 \/
% 0.18/0.50     ~white $_81 \/ ~young skc28 \/ skc24 = skc28 \/ ssSkC0
% 0.18/0.50  |- ~barrel skc24 $_109 \/ ~car $_109 \/ ~chevy $_109 \/ ~city skc25 \/
% 0.18/0.50     ~dirty $_109 \/ ~down skc24 $_110 \/ ~event skc24 \/ ~fellow $_113 \/
% 0.18/0.50     ~front $_114 \/ ~front skc25 \/ ~furniture $_114 \/ ~furniture skc25 \/
% 0.18/0.50     ~hollywood skc25 \/ ~in $_113 $_114 \/ ~lonely $_110 \/ ~man $_113 \/
% 0.18/0.50     ~man skc23 \/ ~old $_109 \/ ~seat $_114 \/ ~street $_110 \/
% 0.18/0.50     ~way $_110 \/ ~white $_109 \/ ~young $_113 \/ ~young skc23 \/
% 0.18/0.50     skc23 = $_113 \/ ssSkC0
% 0.18/0.50  |- ~barrel skc28 $_109 \/ ~car $_109 \/ ~chevy $_109 \/ ~city skc29 \/
% 0.18/0.50     ~dirty $_109 \/ ~down skc28 $_110 \/ ~fellow $_113 \/ ~front $_114 \/
% 0.18/0.50     ~front skc25 \/ ~furniture $_114 \/ ~furniture skc25 \/
% 0.18/0.50     ~in $_113 $_114 \/ ~lonely $_110 \/ ~man $_113 \/ ~man skc23 \/
% 0.18/0.50     ~old $_109 \/ ~seat $_114 \/ ~street $_110 \/ ~way $_110 \/
% 0.18/0.50     ~white $_109 \/ ~young $_113 \/ ~young skc23 \/ skc23 = $_113 \/ ssSkC0
% 0.18/0.50  |- ~barrel $_111 $_109 \/ ~car $_109 \/ ~chevy $_109 \/ ~city $_112 \/
% 0.18/0.50     ~dirty $_109 \/ ~down $_111 $_110 \/ ~event $_111 \/ ~fellow skc28 \/
% 0.18/0.50     ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/ ~furniture skc29 \/
% 0.18/0.50     ~hollywood $_112 \/ ~in $_111 $_112 \/ ~lonely $_110 \/ ~man skc23 \/
% 0.18/0.50     ~man skc28 \/ ~old $_109 \/ ~seat skc29 \/ ~street $_110 \/
% 0.18/0.50     ~way $_110 \/ ~white $_109 \/ ~young skc23 \/ ~young skc28 \/
% 0.18/0.50     skc23 = skc28 \/ ssSkC0
% 0.18/0.50  |- ~barrel skc24 $_119 \/ ~car $_119 \/ ~chevy $_119 \/ ~city skc25 \/
% 0.18/0.50     ~dirty $_119 \/ ~down skc24 $_120 \/ ~event skc24 \/ ~fellow skc28 \/
% 0.18/0.50     ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/ ~furniture skc29 \/
% 0.18/0.50     ~hollywood skc25 \/ ~lonely $_120 \/ ~man skc23 \/ ~man skc28 \/
% 0.18/0.50     ~old $_119 \/ ~seat skc29 \/ ~street $_120 \/ ~way $_120 \/
% 0.18/0.50     ~white $_119 \/ ~young skc23 \/ ~young skc28 \/ skc23 = skc28 \/ ssSkC0
% 0.18/0.50  |- ~barrel skc24 $_135 \/ ~car $_135 \/ ~chevy $_135 \/ ~city skc25 \/
% 0.18/0.50     ~dirty $_135 \/ ~down skc24 $_136 \/ ~event skc24 \/ ~fellow $_139 \/
% 0.18/0.50     ~fellow skc28 \/ ~front $_140 \/ ~front skc29 \/ ~furniture $_140 \/
% 0.18/0.50     ~furniture skc29 \/ ~hollywood skc25 \/ ~in $_139 $_140 \/
% 0.18/0.50     ~lonely $_136 \/ ~man $_139 \/ ~man skc28 \/ ~old $_135 \/
% 0.18/0.50     ~seat $_140 \/ ~seat skc29 \/ ~street $_136 \/ ~way $_136 \/
% 0.18/0.50     ~white $_135 \/ ~young $_139 \/ ~young skc28 \/ skc28 = $_139 \/ ssSkC0
% 0.18/0.50  |- ~barrel skc23 $_145 \/ ~car $_145 \/ ~chevy $_145 \/ ~city skc25 \/
% 0.18/0.50     ~dirty $_145 \/ ~down skc23 $_146 \/ ~event skc23 \/ ~fellow $_149 \/
% 0.18/0.50     ~fellow skc28 \/ ~front $_150 \/ ~front skc29 \/ ~furniture $_150 \/
% 0.18/0.50     ~furniture skc29 \/ ~hollywood skc25 \/ ~in $_149 $_150 \/
% 0.18/0.50     ~lonely $_146 \/ ~man $_149 \/ ~man skc28 \/ ~old $_145 \/
% 0.18/0.50     ~seat $_150 \/ ~seat skc29 \/ ~street $_146 \/ ~way $_146 \/
% 0.18/0.50     ~white $_145 \/ ~young $_149 \/ ~young skc28 \/ skc28 = $_149 \/ ssSkC0
% 0.18/0.50  |- ~barrel skc15 $_162 \/ ~car $_162 \/ ~chevy $_162 \/ ~city skc18 \/
% 0.18/0.50     ~dirty $_162 \/ ~down skc15 $_161 \/ ~event skc15 \/ ~fellow $_165 \/
% 0.18/0.50     ~furniture skc17 \/ ~hollywood skc18 \/ ~in $_165 skc17 \/
% 0.18/0.50     ~lonely $_161 \/ ~man $_165 \/ ~man skc16 \/ ~old $_162 \/
% 0.18/0.50     ~seat skc17 \/ ~ssSkC0 \/ ~street $_161 \/ ~way $_161 \/ ~white $_162 \/
% 0.18/0.50     ~young $_165 \/ ~young skc16 \/ skc16 = $_165 \/ skc24 = skc23
% 0.18/0.50  |- ~barrel skc21 $_162 \/ ~car $_162 \/ ~chevy $_162 \/ ~dirty $_162 \/
% 0.18/0.50     ~down skc21 $_161 \/ ~fellow $_165 \/ ~furniture skc17 \/
% 0.18/0.50     ~hollywood skc22 \/ ~in $_165 skc17 \/ ~lonely $_161 \/ ~man $_165 \/
% 0.18/0.50     ~man skc16 \/ ~old $_162 \/ ~seat skc17 \/ ~ssSkC0 \/ ~street $_161 \/
% 0.18/0.50     ~way $_161 \/ ~white $_162 \/ ~young $_165 \/ ~young skc16 \/
% 0.18/0.50     skc16 = $_165 \/ skc24 = skc23
% 0.18/0.50  |- ~barrel skc16 $_173 \/ ~car $_173 \/ ~chevy $_173 \/ ~city skc17 \/
% 0.18/0.50     ~dirty $_173 \/ ~down skc16 $_172 \/ ~event skc16 \/ ~fellow $_176 \/
% 0.18/0.50     ~fellow skc15 \/ ~front skc18 \/ ~furniture skc18 \/ ~hollywood skc17 \/
% 0.18/0.50     ~in $_176 skc18 \/ ~lonely $_172 \/ ~man $_176 \/ ~man skc15 \/
% 0.18/0.50     ~old $_173 \/ ~ssSkC0 \/ ~street $_172 \/ ~way $_172 \/ ~white $_173 \/
% 0.18/0.50     ~young $_176 \/ skc15 = $_176 \/ skc24 = skc23
% 0.18/0.50  |- ~barrel skc21 $_173 \/ ~car $_173 \/ ~chevy $_173 \/ ~dirty $_173 \/
% 0.18/0.50     ~down skc21 $_172 \/ ~fellow $_176 \/ ~fellow skc15 \/ ~front skc18 \/
% 0.18/0.50     ~furniture skc18 \/ ~hollywood skc22 \/ ~in $_176 skc18 \/
% 0.18/0.50     ~lonely $_172 \/ ~man $_176 \/ ~man skc15 \/ ~old $_173 \/ ~ssSkC0 \/
% 0.18/0.50     ~street $_172 \/ ~way $_172 \/ ~white $_173 \/ ~young $_176 \/
% 0.18/0.50     skc15 = $_176 \/ skc24 = skc23
% 0.18/0.50  |- ~barrel skc16 $_189 \/ ~car $_189 \/ ~chevy $_189 \/ ~city skc17 \/
% 0.18/0.50     ~dirty $_189 \/ ~down skc16 $_188 \/ ~event skc16 \/ ~fellow $_192 \/
% 0.18/0.50     ~fellow skc21 \/ ~front skc22 \/ ~furniture skc22 \/ ~hollywood skc17 \/
% 0.18/0.50     ~in $_192 skc22 \/ ~lonely $_188 \/ ~man $_192 \/ ~man skc21 \/
% 0.18/0.50     ~old $_189 \/ ~seat skc22 \/ ~ssSkC0 \/ ~street $_188 \/ ~way $_188 \/
% 0.18/0.50     ~white $_189 \/ ~young $_192 \/ ~young skc21 \/ $_192 = skc21 \/
% 0.18/0.50     skc24 = skc23
% 0.18/0.50  |- ~barrel skc15 $_197 \/ ~car $_197 \/ ~chevy $_197 \/ ~city skc18 \/
% 0.18/0.50     ~dirty $_197 \/ ~down skc15 $_196 \/ ~event skc15 \/ ~fellow $_200 \/
% 0.18/0.50     ~fellow skc21 \/ ~front skc22 \/ ~furniture skc22 \/ ~hollywood skc18 \/
% 0.18/0.50     ~in $_200 skc22 \/ ~lonely $_196 \/ ~man $_200 \/ ~man skc21 \/
% 0.18/0.50     ~old $_197 \/ ~seat skc22 \/ ~ssSkC0 \/ ~street $_196 \/ ~way $_196 \/
% 0.18/0.50     ~white $_197 \/ ~young $_200 \/ ~young skc21 \/ skc21 = $_200 \/
% 0.18/0.50     skc24 = skc23
% 0.18/0.50  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.50  
%------------------------------------------------------------------------------