%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : NLP005-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n016.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:39 EDT 2022 % Result : Satisfiable 0.20s 0.49s % Output : Saturation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NLP005-1 : TPTP v8.1.0. Released v2.4.0. % 0.12/0.13 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n016.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Jun 30 23:20:11 EDT 2022 % 0.12/0.34 % CPUTime : % 0.20/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.20/0.49 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.49 % 0.20/0.49 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.49 |- city skc29 % 0.20/0.49 |- event skc28 % 0.20/0.49 |- old skc27 % 0.20/0.49 |- street skc26 % 0.20/0.49 |- seat skc25 % 0.20/0.49 |- young skc24 % 0.20/0.49 |- fellow skc23 % 0.20/0.49 |- hollywood skc22 % 0.20/0.49 |- event skc21 % 0.20/0.49 |- street skc20 % 0.20/0.49 |- old skc19 % 0.20/0.49 |- front skc18 % 0.20/0.49 |- seat skc17 % 0.20/0.49 |- fellow skc16 % 0.20/0.49 |- young skc15 % 0.20/0.49 |- lonely skc26 \/ ssSkC0 % 0.20/0.49 |- ssSkC0 \/ way skc26 % 0.20/0.49 |- chevy skc27 \/ ssSkC0 % 0.20/0.49 |- car skc27 \/ ssSkC0 % 0.20/0.49 |- ssSkC0 \/ white skc27 % 0.20/0.49 |- dirty skc27 \/ ssSkC0 % 0.20/0.49 |- hollywood skc29 \/ ssSkC0 % 0.20/0.49 |- ssSkC0 \/ young skc23 % 0.20/0.49 |- man skc23 \/ ssSkC0 % 0.20/0.49 |- fellow skc24 \/ ssSkC0 % 0.20/0.49 |- man skc24 \/ ssSkC0 % 0.20/0.49 |- front skc25 \/ ssSkC0 % 0.20/0.49 |- furniture skc25 \/ ssSkC0 % 0.20/0.49 |- ~ssSkC0 \/ chevy skc19 % 0.20/0.49 |- ~ssSkC0 \/ car skc19 % 0.20/0.49 |- ~ssSkC0 \/ white skc19 % 0.20/0.49 |- ~ssSkC0 \/ dirty skc19 % 0.20/0.49 |- ~ssSkC0 \/ lonely skc20 % 0.20/0.49 |- ~ssSkC0 \/ way skc20 % 0.20/0.49 |- ~ssSkC0 \/ city skc22 % 0.20/0.49 |- ~ssSkC0 \/ seat skc18 % 0.20/0.49 |- ~ssSkC0 \/ furniture skc18 % 0.20/0.49 |- ~ssSkC0 \/ fellow skc15 % 0.20/0.49 |- ~ssSkC0 \/ man skc15 % 0.20/0.49 |- ~ssSkC0 \/ front skc17 % 0.20/0.49 |- ~ssSkC0 \/ furniture skc17 % 0.20/0.49 |- ~ssSkC0 \/ young skc16 % 0.20/0.49 |- ~ssSkC0 \/ man skc16 % 0.20/0.49 |- down skc28 skc26 \/ ssSkC0 % 0.20/0.49 |- barrel skc28 skc27 \/ ssSkC0 % 0.20/0.49 |- in skc28 skc29 \/ ssSkC0 % 0.20/0.49 |- in skc23 skc25 \/ ssSkC0 % 0.20/0.49 |- in skc24 skc25 \/ ssSkC0 % 0.20/0.49 |- ~ssSkC0 \/ barrel skc21 skc19 % 0.20/0.49 |- ~ssSkC0 \/ down skc21 skc20 % 0.20/0.49 |- ~ssSkC0 \/ in skc21 skc22 % 0.20/0.49 |- ~ssSkC0 \/ in skc15 skc18 % 0.20/0.49 |- ~ssSkC0 \/ in skc16 skc17 % 0.20/0.49 |- ~(skc24 = skc23) \/ ssSkC0 % 0.20/0.49 |- ~(skc16 = skc15) \/ ~ssSkC0 % 0.20/0.49 |- ~barrel $W $V \/ ~car $V \/ ~chevy $V \/ ~city $X \/ ~dirty $V \/ % 0.20/0.49 ~down $W $U \/ ~event $W \/ ~fellow $Y \/ ~fellow $Z \/ ~front $X1 \/ % 0.20/0.49 ~furniture $X1 \/ ~hollywood $X \/ ~in $W $X \/ ~in $Y $X1 \/ % 0.20/0.49 ~in $Z $X1 \/ ~lonely $U \/ ~man $Y \/ ~man $Z \/ ~old $V \/ % 0.20/0.49 ~seat $X1 \/ ~ssSkC0 \/ ~street $U \/ ~way $U \/ ~white $V \/ % 0.20/0.49 ~young $Y \/ ~young $Z \/ $Z = $Y % 0.20/0.49 |- ~barrel $W $U \/ ~car $U \/ ~chevy $U \/ ~city $X \/ ~dirty $U \/ % 0.20/0.49 ~down $W $V \/ ~event $W \/ ~fellow $X1 \/ ~fellow $Z \/ ~front $X2 \/ % 0.20/0.49 ~front $Y \/ ~furniture $X2 \/ ~furniture $Y \/ ~hollywood $X \/ % 0.20/0.49 ~in $W $X \/ ~in $X1 $X2 \/ ~in $Z $Y \/ ~lonely $V \/ ~man $X1 \/ % 0.20/0.49 ~man $Z \/ ~old $U \/ ~seat $X2 \/ ~seat $Y \/ ~street $V \/ ~way $V \/ % 0.20/0.49 ~white $U \/ ~young $X1 \/ ~young $Z \/ $X1 = $Z \/ ssSkC0 % 0.20/0.49 |- ~barrel $Y $V \/ ~car $V \/ ~chevy $V \/ ~city $X1 \/ ~dirty $V \/ % 0.20/0.49 ~down $Y $U \/ ~event $Y \/ ~fellow $Y \/ ~fellow $Z \/ ~front $X1 \/ % 0.20/0.49 ~furniture $X1 \/ ~hollywood $X1 \/ ~in $Y $X1 \/ ~in $Z $X1 \/ % 0.20/0.49 ~lonely $U \/ ~man $Y \/ ~man $Z \/ ~old $V \/ ~seat $X1 \/ ~ssSkC0 \/ % 0.20/0.49 ~street $U \/ ~way $U \/ ~white $V \/ ~young $Y \/ ~young $Z \/ $Z = $Y % 0.20/0.49 |- ~barrel $X1 $U \/ ~car $U \/ ~chevy $U \/ ~city $X2 \/ ~dirty $U \/ % 0.20/0.49 ~down $X1 $V \/ ~event $X1 \/ ~fellow $X1 \/ ~fellow $Z \/ ~front $X2 \/ % 0.20/0.49 ~front $Y \/ ~furniture $X2 \/ ~furniture $Y \/ ~hollywood $X2 \/ % 0.20/0.49 ~in $X1 $X2 \/ ~in $Z $Y \/ ~lonely $V \/ ~man $X1 \/ ~man $Z \/ % 0.20/0.49 ~old $U \/ ~seat $X2 \/ ~seat $Y \/ ~street $V \/ ~way $V \/ % 0.20/0.49 ~white $U \/ ~young $X1 \/ ~young $Z \/ $X1 = $Z \/ ssSkC0 % 0.20/0.49 |- ~barrel $_7 $_5 \/ ~car $_5 \/ ~chevy $_5 \/ ~city $_8 \/ ~dirty $_5 \/ % 0.20/0.49 ~down $_7 $_6 \/ ~event $_7 \/ ~fellow $_7 \/ ~front $_8 \/ % 0.20/0.49 ~front skc25 \/ ~furniture $_8 \/ ~furniture skc25 \/ ~hollywood $_8 \/ % 0.20/0.49 ~in $_7 $_8 \/ ~lonely $_6 \/ ~man $_7 \/ ~man skc23 \/ ~old $_5 \/ % 0.20/0.49 ~seat $_8 \/ ~street $_6 \/ ~way $_6 \/ ~white $_5 \/ ~young $_7 \/ % 0.20/0.49 ~young skc23 \/ $_7 = skc23 \/ ssSkC0 % 0.20/0.49 |- ~barrel $_7 $_5 \/ ~car $_5 \/ ~chevy $_5 \/ ~city $_8 \/ ~dirty $_5 \/ % 0.20/0.49 ~down $_7 $_6 \/ ~event $_7 \/ ~fellow $_7 \/ ~fellow skc24 \/ % 0.20/0.49 ~front $_8 \/ ~front skc25 \/ ~furniture $_8 \/ ~furniture skc25 \/ % 0.20/0.49 ~hollywood $_8 \/ ~in $_7 $_8 \/ ~lonely $_6 \/ ~man $_7 \/ % 0.20/0.49 ~man skc24 \/ ~old $_5 \/ ~seat $_8 \/ ~street $_6 \/ ~way $_6 \/ % 0.20/0.49 ~white $_5 \/ ~young $_7 \/ $_7 = skc24 \/ ssSkC0 % 0.20/0.49 |- ~barrel $_7 $_5 \/ ~car $_5 \/ ~chevy $_5 \/ ~city $_8 \/ ~dirty $_5 \/ % 0.20/0.49 ~down $_7 $_6 \/ ~event $_7 \/ ~fellow $_7 \/ ~fellow skc28 \/ % 0.20/0.49 ~front $_8 \/ ~front skc29 \/ ~furniture $_8 \/ ~furniture skc29 \/ % 0.20/0.49 ~hollywood $_8 \/ ~in $_7 $_8 \/ ~lonely $_6 \/ ~man $_7 \/ % 0.20/0.49 ~man skc28 \/ ~old $_5 \/ ~seat $_8 \/ ~seat skc29 \/ ~street $_6 \/ % 0.20/0.49 ~way $_6 \/ ~white $_5 \/ ~young $_7 \/ ~young skc28 \/ $_7 = skc28 \/ % 0.20/0.49 ssSkC0 % 0.20/0.49 |- ~barrel skc23 $_5 \/ ~car $_5 \/ ~chevy $_5 \/ ~city skc25 \/ % 0.20/0.49 ~dirty $_5 \/ ~down skc23 $_6 \/ ~event skc23 \/ ~fellow $_10 \/ % 0.20/0.49 ~front $_9 \/ ~front skc25 \/ ~furniture $_9 \/ ~furniture skc25 \/ % 0.20/0.49 ~hollywood skc25 \/ ~in $_10 $_9 \/ ~lonely $_6 \/ ~man $_10 \/ % 0.20/0.49 ~man skc23 \/ ~old $_5 \/ ~seat $_9 \/ ~street $_6 \/ ~way $_6 \/ % 0.20/0.49 ~white $_5 \/ ~young $_10 \/ ~young skc23 \/ skc23 = $_10 \/ ssSkC0 % 0.20/0.49 |- ~barrel skc24 $_5 \/ ~car $_5 \/ ~chevy $_5 \/ ~city skc25 \/ % 0.20/0.49 ~dirty $_5 \/ ~down skc24 $_6 \/ ~event skc24 \/ ~fellow $_10 \/ % 0.20/0.49 ~fellow skc24 \/ ~front $_9 \/ ~front skc25 \/ ~furniture $_9 \/ % 0.20/0.49 ~furniture skc25 \/ ~hollywood skc25 \/ ~in $_10 $_9 \/ ~lonely $_6 \/ % 0.20/0.49 ~man $_10 \/ ~man skc24 \/ ~old $_5 \/ ~seat $_9 \/ ~street $_6 \/ % 0.20/0.49 ~way $_6 \/ ~white $_5 \/ ~young $_10 \/ skc24 = $_10 \/ ssSkC0 % 0.20/0.49 |- ~barrel skc28 $_5 \/ ~car $_5 \/ ~chevy $_5 \/ ~dirty $_5 \/ % 0.20/0.49 ~down skc28 $_6 \/ ~fellow $_10 \/ ~fellow skc28 \/ ~front $_9 \/ % 0.20/0.49 ~front skc29 \/ ~furniture $_9 \/ ~furniture skc29 \/ % 0.20/0.49 ~hollywood skc29 \/ ~in $_10 $_9 \/ ~lonely $_6 \/ ~man $_10 \/ % 0.20/0.49 ~man skc28 \/ ~old $_5 \/ ~seat $_9 \/ ~seat skc29 \/ ~street $_6 \/ % 0.20/0.49 ~way $_6 \/ ~white $_5 \/ ~young $_10 \/ ~young skc28 \/ skc28 = $_10 \/ % 0.20/0.49 ssSkC0 % 0.20/0.49 |- ~barrel skc28 $_12 \/ ~car $_12 \/ ~chevy $_12 \/ ~dirty $_12 \/ % 0.20/0.49 ~down skc28 $_13 \/ ~fellow skc28 \/ ~front skc25 \/ ~front skc29 \/ % 0.20/0.49 ~furniture skc25 \/ ~furniture skc29 \/ ~hollywood skc29 \/ % 0.20/0.49 ~lonely $_13 \/ ~man skc23 \/ ~man skc28 \/ ~old $_12 \/ ~seat skc29 \/ % 0.20/0.49 ~street $_13 \/ ~way $_13 \/ ~white $_12 \/ ~young skc23 \/ % 0.20/0.49 ~young skc28 \/ skc28 = skc23 \/ ssSkC0 % 0.20/0.49 |- ~barrel skc28 $_12 \/ ~car $_12 \/ ~chevy $_12 \/ ~dirty $_12 \/ % 0.20/0.49 ~down skc28 $_13 \/ ~fellow skc24 \/ ~fellow skc28 \/ ~front skc25 \/ % 0.20/0.49 ~front skc29 \/ ~furniture skc25 \/ ~furniture skc29 \/ % 0.20/0.49 ~hollywood skc29 \/ ~lonely $_13 \/ ~man skc24 \/ ~man skc28 \/ % 0.20/0.49 ~old $_12 \/ ~seat skc29 \/ ~street $_13 \/ ~way $_13 \/ ~white $_12 \/ % 0.20/0.49 ~young skc28 \/ skc28 = skc24 \/ ssSkC0 % 0.20/0.49 |- ~barrel skc28 $_15 \/ ~car $_15 \/ ~chevy $_15 \/ ~dirty $_15 \/ % 0.20/0.49 ~fellow skc24 \/ ~fellow skc28 \/ ~front skc25 \/ ~front skc29 \/ % 0.20/0.49 ~furniture skc25 \/ ~furniture skc29 \/ ~hollywood skc29 \/ % 0.20/0.49 ~lonely skc26 \/ ~man skc24 \/ ~man skc28 \/ ~old $_15 \/ ~seat skc29 \/ % 0.20/0.49 ~way skc26 \/ ~white $_15 \/ ~young skc28 \/ skc28 = skc24 \/ ssSkC0 % 0.20/0.50 |- ~car skc27 \/ ~chevy skc27 \/ ~dirty skc27 \/ ~fellow skc24 \/ % 0.20/0.50 ~fellow skc28 \/ ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/ % 0.20/0.50 ~furniture skc29 \/ ~hollywood skc29 \/ ~lonely skc26 \/ ~man skc24 \/ % 0.20/0.50 ~man skc28 \/ ~seat skc29 \/ ~way skc26 \/ ~white skc27 \/ % 0.20/0.50 ~young skc28 \/ skc28 = skc24 \/ ssSkC0 % 0.20/0.50 |- ~barrel skc28 $_18 \/ ~car $_18 \/ ~chevy $_18 \/ ~dirty $_18 \/ % 0.20/0.50 ~fellow skc28 \/ ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/ % 0.20/0.50 ~furniture skc29 \/ ~hollywood skc29 \/ ~lonely skc26 \/ ~man skc23 \/ % 0.20/0.50 ~man skc28 \/ ~old $_18 \/ ~seat skc29 \/ ~way skc26 \/ ~white $_18 \/ % 0.20/0.50 ~young skc23 \/ ~young skc28 \/ skc28 = skc23 \/ ssSkC0 % 0.20/0.50 |- ~car skc27 \/ ~chevy skc27 \/ ~dirty skc27 \/ ~fellow skc28 \/ % 0.20/0.50 ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/ ~furniture skc29 \/ % 0.20/0.50 ~hollywood skc29 \/ ~lonely skc26 \/ ~man skc23 \/ ~man skc28 \/ % 0.20/0.50 ~seat skc29 \/ ~way skc26 \/ ~white skc27 \/ ~young skc23 \/ % 0.20/0.50 ~young skc28 \/ skc28 = skc23 \/ ssSkC0 % 0.20/0.50 |- ~barrel skc24 $_22 \/ ~car $_22 \/ ~chevy $_22 \/ ~city skc25 \/ % 0.20/0.50 ~dirty $_22 \/ ~down skc24 $_23 \/ ~event skc24 \/ ~fellow skc24 \/ % 0.20/0.50 ~fellow skc28 \/ ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/ % 0.20/0.50 ~furniture skc29 \/ ~hollywood skc25 \/ ~lonely $_23 \/ ~man skc24 \/ % 0.20/0.50 ~man skc28 \/ ~old $_22 \/ ~seat skc29 \/ ~street $_23 \/ ~way $_23 \/ % 0.20/0.50 ~white $_22 \/ ~young skc28 \/ skc24 = skc28 \/ ssSkC0 % 0.20/0.50 |- ~barrel skc23 $_30 \/ ~car $_30 \/ ~chevy $_30 \/ ~city skc25 \/ % 0.20/0.50 ~dirty $_30 \/ ~down skc23 $_31 \/ ~event skc23 \/ ~fellow skc28 \/ % 0.20/0.50 ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/ ~furniture skc29 \/ % 0.20/0.50 ~hollywood skc25 \/ ~lonely $_31 \/ ~man skc23 \/ ~man skc28 \/ % 0.20/0.50 ~old $_30 \/ ~seat skc29 \/ ~street $_31 \/ ~way $_31 \/ ~white $_30 \/ % 0.20/0.50 ~young skc23 \/ ~young skc28 \/ skc23 = skc28 \/ ssSkC0 % 0.20/0.50 |- ~barrel skc23 $_56 \/ ~car $_56 \/ ~chevy $_56 \/ ~city skc25 \/ % 0.20/0.50 ~dirty $_56 \/ ~down skc23 $_57 \/ ~event skc23 \/ ~fellow $_60 \/ % 0.20/0.50 ~fellow $_63 \/ ~front $_61 \/ ~front $_62 \/ ~furniture $_61 \/ % 0.20/0.50 ~furniture $_62 \/ ~hollywood skc25 \/ ~in $_60 $_61 \/ ~in $_63 $_62 \/ % 0.20/0.50 ~lonely $_57 \/ ~man $_60 \/ ~man $_63 \/ ~old $_56 \/ ~seat $_61 \/ % 0.20/0.50 ~seat $_62 \/ ~street $_57 \/ ~way $_57 \/ ~white $_56 \/ ~young $_60 \/ % 0.20/0.50 ~young $_63 \/ $_60 = $_63 \/ ssSkC0 % 0.20/0.50 |- ~barrel skc24 $_56 \/ ~car $_56 \/ ~chevy $_56 \/ ~city skc25 \/ % 0.20/0.50 ~dirty $_56 \/ ~down skc24 $_57 \/ ~event skc24 \/ ~fellow $_60 \/ % 0.20/0.50 ~fellow $_63 \/ ~front $_61 \/ ~front $_62 \/ ~furniture $_61 \/ % 0.20/0.50 ~furniture $_62 \/ ~hollywood skc25 \/ ~in $_60 $_61 \/ ~in $_63 $_62 \/ % 0.20/0.50 ~lonely $_57 \/ ~man $_60 \/ ~man $_63 \/ ~old $_56 \/ ~seat $_61 \/ % 0.20/0.50 ~seat $_62 \/ ~street $_57 \/ ~way $_57 \/ ~white $_56 \/ ~young $_60 \/ % 0.20/0.50 ~young $_63 \/ $_60 = $_63 \/ ssSkC0 % 0.20/0.50 |- ~barrel skc28 $_56 \/ ~car $_56 \/ ~chevy $_56 \/ ~dirty $_56 \/ % 0.20/0.50 ~down skc28 $_57 \/ ~fellow $_60 \/ ~fellow $_63 \/ ~front $_61 \/ % 0.20/0.50 ~front $_62 \/ ~furniture $_61 \/ ~furniture $_62 \/ ~hollywood skc29 \/ % 0.20/0.50 ~in $_60 $_61 \/ ~in $_63 $_62 \/ ~lonely $_57 \/ ~man $_60 \/ % 0.20/0.50 ~man $_63 \/ ~old $_56 \/ ~seat $_61 \/ ~seat $_62 \/ ~street $_57 \/ % 0.20/0.50 ~way $_57 \/ ~white $_56 \/ ~young $_60 \/ ~young $_63 \/ $_60 = $_63 \/ % 0.20/0.50 ssSkC0 % 0.20/0.50 |- ~barrel $_58 $_56 \/ ~car $_56 \/ ~chevy $_56 \/ ~city $_59 \/ % 0.20/0.50 ~dirty $_56 \/ ~down $_58 $_57 \/ ~event $_58 \/ ~fellow $_63 \/ % 0.20/0.50 ~front $_62 \/ ~front skc25 \/ ~furniture $_62 \/ ~furniture skc25 \/ % 0.20/0.50 ~hollywood $_59 \/ ~in $_58 $_59 \/ ~in $_63 $_62 \/ ~lonely $_57 \/ % 0.20/0.50 ~man $_63 \/ ~man skc23 \/ ~old $_56 \/ ~seat $_62 \/ ~street $_57 \/ % 0.20/0.50 ~way $_57 \/ ~white $_56 \/ ~young $_63 \/ ~young skc23 \/ % 0.20/0.50 skc23 = $_63 \/ ssSkC0 % 0.20/0.50 |- ~barrel $_58 $_56 \/ ~car $_56 \/ ~chevy $_56 \/ ~city $_59 \/ % 0.20/0.50 ~dirty $_56 \/ ~down $_58 $_57 \/ ~event $_58 \/ ~fellow $_63 \/ % 0.20/0.50 ~fellow skc24 \/ ~front $_62 \/ ~front skc25 \/ ~furniture $_62 \/ % 0.20/0.50 ~furniture skc25 \/ ~hollywood $_59 \/ ~in $_58 $_59 \/ ~in $_63 $_62 \/ % 0.20/0.50 ~lonely $_57 \/ ~man $_63 \/ ~man skc24 \/ ~old $_56 \/ ~seat $_62 \/ % 0.20/0.50 ~street $_57 \/ ~way $_57 \/ ~white $_56 \/ ~young $_63 \/ % 0.20/0.50 skc24 = $_63 \/ ssSkC0 % 0.20/0.50 |- ~barrel $_58 $_56 \/ ~car $_56 \/ ~chevy $_56 \/ ~city $_59 \/ % 0.20/0.50 ~dirty $_56 \/ ~down $_58 $_57 \/ ~event $_58 \/ ~fellow $_63 \/ % 0.20/0.50 ~fellow skc28 \/ ~front $_62 \/ ~front skc29 \/ ~furniture $_62 \/ % 0.20/0.50 ~furniture skc29 \/ ~hollywood $_59 \/ ~in $_58 $_59 \/ ~in $_63 $_62 \/ % 0.20/0.50 ~lonely $_57 \/ ~man $_63 \/ ~man skc28 \/ ~old $_56 \/ ~seat $_62 \/ % 0.20/0.50 ~seat skc29 \/ ~street $_57 \/ ~way $_57 \/ ~white $_56 \/ % 0.20/0.50 ~young $_63 \/ ~young skc28 \/ skc28 = $_63 \/ ssSkC0 % 0.20/0.50 |- ~barrel skc23 $_64 \/ ~car $_64 \/ ~chevy $_64 \/ ~city skc25 \/ % 0.20/0.50 ~dirty $_64 \/ ~down skc23 $_65 \/ ~event skc23 \/ ~fellow $_69 \/ % 0.20/0.50 ~fellow skc24 \/ ~front $_68 \/ ~front skc25 \/ ~furniture $_68 \/ % 0.20/0.50 ~furniture skc25 \/ ~hollywood skc25 \/ ~in $_69 $_68 \/ ~lonely $_65 \/ % 0.20/0.50 ~man $_69 \/ ~man skc24 \/ ~old $_64 \/ ~seat $_68 \/ ~street $_65 \/ % 0.20/0.50 ~way $_65 \/ ~white $_64 \/ ~young $_69 \/ skc24 = $_69 \/ ssSkC0 % 0.20/0.50 |- ~barrel skc28 $_64 \/ ~car $_64 \/ ~chevy $_64 \/ ~dirty $_64 \/ % 0.20/0.50 ~down skc28 $_65 \/ ~fellow $_69 \/ ~fellow skc24 \/ ~front $_68 \/ % 0.20/0.50 ~front skc25 \/ ~furniture $_68 \/ ~furniture skc25 \/ % 0.20/0.50 ~hollywood skc29 \/ ~in $_69 $_68 \/ ~lonely $_65 \/ ~man $_69 \/ % 0.20/0.50 ~man skc24 \/ ~old $_64 \/ ~seat $_68 \/ ~street $_65 \/ ~way $_65 \/ % 0.20/0.50 ~white $_64 \/ ~young $_69 \/ skc24 = $_69 \/ ssSkC0 % 0.20/0.50 |- ~barrel $_66 $_64 \/ ~car $_64 \/ ~chevy $_64 \/ ~city $_67 \/ % 0.20/0.50 ~dirty $_64 \/ ~down $_66 $_65 \/ ~event $_66 \/ ~fellow skc24 \/ % 0.20/0.50 ~fellow skc28 \/ ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/ % 0.20/0.50 ~furniture skc29 \/ ~hollywood $_67 \/ ~in $_66 $_67 \/ ~lonely $_65 \/ % 0.20/0.50 ~man skc24 \/ ~man skc28 \/ ~old $_64 \/ ~seat skc29 \/ ~street $_65 \/ % 0.20/0.50 ~way $_65 \/ ~white $_64 \/ ~young skc28 \/ skc24 = skc28 \/ ssSkC0 % 0.20/0.50 |- skc24 = skc23 \/ ssSkC0 % 0.20/0.50 |- ~(skc16 = skc15) \/ skc24 = skc23 % 0.20/0.50 |- skc24 = skc23 \/ in skc16 skc17 % 0.20/0.50 |- skc24 = skc23 \/ in skc15 skc18 % 0.20/0.50 |- skc24 = skc23 \/ in skc21 skc22 % 0.20/0.50 |- skc24 = skc23 \/ down skc21 skc20 % 0.20/0.50 |- skc24 = skc23 \/ barrel skc21 skc19 % 0.20/0.50 |- skc24 = skc23 \/ man skc16 % 0.20/0.50 |- skc24 = skc23 \/ young skc16 % 0.20/0.50 |- skc24 = skc23 \/ furniture skc17 % 0.20/0.50 |- skc24 = skc23 \/ front skc17 % 0.20/0.50 |- skc24 = skc23 \/ man skc15 % 0.20/0.50 |- skc24 = skc23 \/ fellow skc15 % 0.20/0.50 |- skc24 = skc23 \/ furniture skc18 % 0.20/0.50 |- skc24 = skc23 \/ seat skc18 % 0.20/0.50 |- skc24 = skc23 \/ city skc22 % 0.20/0.50 |- skc24 = skc23 \/ way skc20 % 0.20/0.50 |- skc24 = skc23 \/ lonely skc20 % 0.20/0.50 |- skc24 = skc23 \/ dirty skc19 % 0.20/0.50 |- skc24 = skc23 \/ white skc19 % 0.20/0.50 |- skc24 = skc23 \/ car skc19 % 0.20/0.50 |- skc24 = skc23 \/ chevy skc19 % 0.20/0.50 |- ~barrel $W $V \/ ~car $V \/ ~chevy $V \/ ~city $X \/ ~dirty $V \/ % 0.20/0.50 ~down $W $U \/ ~event $W \/ ~fellow $Y \/ ~front skc17 \/ % 0.20/0.50 ~furniture skc17 \/ ~hollywood $X \/ ~in $W $X \/ ~in $Y skc17 \/ % 0.20/0.50 ~lonely $U \/ ~man $Y \/ ~man skc16 \/ ~old $V \/ ~ssSkC0 \/ % 0.20/0.50 ~street $U \/ ~way $U \/ ~white $V \/ ~young $Y \/ ~young skc16 \/ % 0.20/0.50 skc16 = $Y \/ skc24 = skc23 % 0.20/0.50 |- ~barrel skc16 $V \/ ~car $V \/ ~chevy $V \/ ~city skc17 \/ ~dirty $V \/ % 0.20/0.50 ~down skc16 $U \/ ~event skc16 \/ ~fellow $Y \/ ~fellow $Z \/ % 0.20/0.50 ~front $X1 \/ ~furniture $X1 \/ ~hollywood skc17 \/ ~in $Y $X1 \/ % 0.20/0.50 ~in $Z $X1 \/ ~lonely $U \/ ~man $Y \/ ~man $Z \/ ~old $V \/ % 0.20/0.50 ~seat $X1 \/ ~ssSkC0 \/ ~street $U \/ ~way $U \/ ~white $V \/ % 0.20/0.50 ~young $Y \/ ~young $Z \/ $Z = $Y \/ skc24 = skc23 % 0.20/0.50 |- ~barrel $Y $V \/ ~car $V \/ ~chevy $V \/ ~city skc17 \/ ~dirty $V \/ % 0.20/0.50 ~down $Y $U \/ ~event $Y \/ ~fellow $Y \/ ~front skc17 \/ % 0.20/0.50 ~furniture skc17 \/ ~hollywood skc17 \/ ~in $Y skc17 \/ ~lonely $U \/ % 0.20/0.50 ~man $Y \/ ~man skc16 \/ ~old $V \/ ~ssSkC0 \/ ~street $U \/ ~way $U \/ % 0.20/0.50 ~white $V \/ ~young $Y \/ ~young skc16 \/ skc16 = $Y \/ skc24 = skc23 % 0.20/0.50 |- ~barrel skc16 $V \/ ~car $V \/ ~chevy $V \/ ~city skc17 \/ ~dirty $V \/ % 0.20/0.50 ~down skc16 $U \/ ~event skc16 \/ ~fellow $Z \/ ~front skc17 \/ % 0.20/0.50 ~furniture skc17 \/ ~hollywood skc17 \/ ~in $Z skc17 \/ ~lonely $U \/ % 0.20/0.50 ~man $Z \/ ~man skc16 \/ ~old $V \/ ~ssSkC0 \/ ~street $U \/ ~way $U \/ % 0.20/0.50 ~white $V \/ ~young $Z \/ ~young skc16 \/ $Z = skc16 \/ skc24 = skc23 % 0.20/0.50 |- ~barrel $W $V \/ ~car $V \/ ~chevy $V \/ ~city $X \/ ~dirty $V \/ % 0.20/0.50 ~down $W $U \/ ~event $W \/ ~fellow $Y \/ ~fellow skc15 \/ % 0.20/0.50 ~furniture skc18 \/ ~hollywood $X \/ ~in $W $X \/ ~in $Y skc18 \/ % 0.20/0.50 ~lonely $U \/ ~man $Y \/ ~man skc15 \/ ~old $V \/ ~seat skc18 \/ % 0.20/0.50 ~ssSkC0 \/ ~street $U \/ ~way $U \/ ~white $V \/ ~young $Y \/ % 0.20/0.50 skc15 = $Y \/ skc24 = skc23 % 0.20/0.50 |- ~barrel skc15 $V \/ ~car $V \/ ~chevy $V \/ ~city skc18 \/ ~dirty $V \/ % 0.20/0.50 ~down skc15 $U \/ ~event skc15 \/ ~fellow $Y \/ ~fellow $Z \/ % 0.20/0.50 ~front $X1 \/ ~furniture $X1 \/ ~hollywood skc18 \/ ~in $Y $X1 \/ % 0.20/0.50 ~in $Z $X1 \/ ~lonely $U \/ ~man $Y \/ ~man $Z \/ ~old $V \/ % 0.20/0.50 ~seat $X1 \/ ~ssSkC0 \/ ~street $U \/ ~way $U \/ ~white $V \/ % 0.20/0.50 ~young $Y \/ ~young $Z \/ $Z = $Y \/ skc24 = skc23 % 0.20/0.50 |- ~barrel $Y $V \/ ~car $V \/ ~chevy $V \/ ~city skc18 \/ ~dirty $V \/ % 0.20/0.50 ~down $Y $U \/ ~event $Y \/ ~fellow $Y \/ ~fellow skc15 \/ % 0.20/0.50 ~furniture skc18 \/ ~hollywood skc18 \/ ~in $Y skc18 \/ ~lonely $U \/ % 0.20/0.50 ~man $Y \/ ~man skc15 \/ ~old $V \/ ~seat skc18 \/ ~ssSkC0 \/ % 0.20/0.50 ~street $U \/ ~way $U \/ ~white $V \/ ~young $Y \/ skc15 = $Y \/ % 0.20/0.50 skc24 = skc23 % 0.20/0.50 |- ~barrel skc15 $V \/ ~car $V \/ ~chevy $V \/ ~city skc18 \/ ~dirty $V \/ % 0.20/0.50 ~down skc15 $U \/ ~event skc15 \/ ~fellow $Z \/ ~fellow skc15 \/ % 0.20/0.50 ~furniture skc18 \/ ~hollywood skc18 \/ ~in $Z skc18 \/ ~lonely $U \/ % 0.20/0.50 ~man $Z \/ ~man skc15 \/ ~old $V \/ ~seat skc18 \/ ~ssSkC0 \/ % 0.20/0.50 ~street $U \/ ~way $U \/ ~white $V \/ ~young $Z \/ $Z = skc15 \/ % 0.20/0.50 skc24 = skc23 % 0.20/0.50 |- ~barrel $W $V \/ ~car $V \/ ~chevy $V \/ ~city $X \/ ~dirty $V \/ % 0.20/0.50 ~down $W $U \/ ~event $W \/ ~fellow $Y \/ ~fellow skc21 \/ % 0.20/0.50 ~front skc22 \/ ~furniture skc22 \/ ~hollywood $X \/ ~in $W $X \/ % 0.20/0.50 ~in $Y skc22 \/ ~lonely $U \/ ~man $Y \/ ~man skc21 \/ ~old $V \/ % 0.20/0.50 ~seat skc22 \/ ~ssSkC0 \/ ~street $U \/ ~way $U \/ ~white $V \/ % 0.20/0.50 ~young $Y \/ ~young skc21 \/ skc21 = $Y \/ skc24 = skc23 % 0.20/0.50 |- ~barrel skc21 $V \/ ~car $V \/ ~chevy $V \/ ~city skc22 \/ ~dirty $V \/ % 0.20/0.50 ~down skc21 $U \/ ~fellow $Y \/ ~fellow $Z \/ ~front $X1 \/ % 0.20/0.50 ~furniture $X1 \/ ~in $Y $X1 \/ ~in $Z $X1 \/ ~lonely $U \/ ~man $Y \/ % 0.20/0.50 ~man $Z \/ ~old $V \/ ~seat $X1 \/ ~ssSkC0 \/ ~street $U \/ ~way $U \/ % 0.20/0.50 ~white $V \/ ~young $Y \/ ~young $Z \/ $Z = $Y \/ skc24 = skc23 % 0.20/0.50 |- ~barrel $Y $V \/ ~car $V \/ ~chevy $V \/ ~city skc22 \/ ~dirty $V \/ % 0.20/0.50 ~down $Y $U \/ ~event $Y \/ ~fellow $Y \/ ~fellow skc21 \/ % 0.20/0.50 ~front skc22 \/ ~furniture skc22 \/ ~in $Y skc22 \/ ~lonely $U \/ % 0.20/0.50 ~man $Y \/ ~man skc21 \/ ~old $V \/ ~seat skc22 \/ ~ssSkC0 \/ % 0.20/0.50 ~street $U \/ ~way $U \/ ~white $V \/ ~young $Y \/ ~young skc21 \/ % 0.20/0.50 skc21 = $Y \/ skc24 = skc23 % 0.20/0.50 |- ~barrel skc21 $V \/ ~car $V \/ ~chevy $V \/ ~city skc22 \/ ~dirty $V \/ % 0.20/0.50 ~down skc21 $U \/ ~fellow $Z \/ ~fellow skc21 \/ ~front skc22 \/ % 0.20/0.50 ~furniture skc22 \/ ~in $Z skc22 \/ ~lonely $U \/ ~man $Z \/ % 0.20/0.50 ~man skc21 \/ ~old $V \/ ~seat skc22 \/ ~ssSkC0 \/ ~street $U \/ % 0.20/0.50 ~way $U \/ ~white $V \/ ~young $Z \/ ~young skc21 \/ $Z = skc21 \/ % 0.20/0.50 skc24 = skc23 % 0.20/0.50 |- ~barrel skc23 $_81 \/ ~car $_81 \/ ~chevy $_81 \/ ~city skc25 \/ % 0.20/0.50 ~dirty $_81 \/ ~down skc23 $_82 \/ ~event skc23 \/ ~fellow skc24 \/ % 0.20/0.50 ~fellow skc28 \/ ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/ % 0.20/0.50 ~furniture skc29 \/ ~hollywood skc25 \/ ~lonely $_82 \/ ~man skc24 \/ % 0.20/0.50 ~man skc28 \/ ~old $_81 \/ ~seat skc29 \/ ~street $_82 \/ ~way $_82 \/ % 0.20/0.50 ~white $_81 \/ ~young skc28 \/ skc24 = skc28 \/ ssSkC0 % 0.20/0.50 |- ~barrel skc24 $_109 \/ ~car $_109 \/ ~chevy $_109 \/ ~city skc25 \/ % 0.20/0.50 ~dirty $_109 \/ ~down skc24 $_110 \/ ~event skc24 \/ ~fellow $_114 \/ % 0.20/0.50 ~front $_113 \/ ~front skc25 \/ ~furniture $_113 \/ ~furniture skc25 \/ % 0.20/0.50 ~hollywood skc25 \/ ~in $_114 $_113 \/ ~lonely $_110 \/ ~man $_114 \/ % 0.20/0.50 ~man skc23 \/ ~old $_109 \/ ~seat $_113 \/ ~street $_110 \/ % 0.20/0.50 ~way $_110 \/ ~white $_109 \/ ~young $_114 \/ ~young skc23 \/ % 0.20/0.50 skc23 = $_114 \/ ssSkC0 % 0.20/0.50 |- ~barrel skc28 $_109 \/ ~car $_109 \/ ~chevy $_109 \/ ~dirty $_109 \/ % 0.20/0.50 ~down skc28 $_110 \/ ~fellow $_114 \/ ~front $_113 \/ ~front skc25 \/ % 0.20/0.50 ~furniture $_113 \/ ~furniture skc25 \/ ~hollywood skc29 \/ % 0.20/0.50 ~in $_114 $_113 \/ ~lonely $_110 \/ ~man $_114 \/ ~man skc23 \/ % 0.20/0.50 ~old $_109 \/ ~seat $_113 \/ ~street $_110 \/ ~way $_110 \/ % 0.20/0.50 ~white $_109 \/ ~young $_114 \/ ~young skc23 \/ skc23 = $_114 \/ ssSkC0 % 0.20/0.50 |- ~barrel $_111 $_109 \/ ~car $_109 \/ ~chevy $_109 \/ ~city $_112 \/ % 0.20/0.50 ~dirty $_109 \/ ~down $_111 $_110 \/ ~event $_111 \/ ~fellow skc28 \/ % 0.20/0.50 ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/ ~furniture skc29 \/ % 0.20/0.50 ~hollywood $_112 \/ ~in $_111 $_112 \/ ~lonely $_110 \/ ~man skc23 \/ % 0.20/0.50 ~man skc28 \/ ~old $_109 \/ ~seat skc29 \/ ~street $_110 \/ % 0.20/0.50 ~way $_110 \/ ~white $_109 \/ ~young skc23 \/ ~young skc28 \/ % 0.20/0.50 skc23 = skc28 \/ ssSkC0 % 0.20/0.50 |- ~barrel skc24 $_119 \/ ~car $_119 \/ ~chevy $_119 \/ ~city skc25 \/ % 0.20/0.50 ~dirty $_119 \/ ~down skc24 $_120 \/ ~event skc24 \/ ~fellow skc28 \/ % 0.20/0.50 ~front skc25 \/ ~front skc29 \/ ~furniture skc25 \/ ~furniture skc29 \/ % 0.20/0.50 ~hollywood skc25 \/ ~lonely $_120 \/ ~man skc23 \/ ~man skc28 \/ % 0.20/0.50 ~old $_119 \/ ~seat skc29 \/ ~street $_120 \/ ~way $_120 \/ % 0.20/0.50 ~white $_119 \/ ~young skc23 \/ ~young skc28 \/ skc23 = skc28 \/ ssSkC0 % 0.20/0.50 |- ~barrel skc24 $_135 \/ ~car $_135 \/ ~chevy $_135 \/ ~city skc25 \/ % 0.20/0.50 ~dirty $_135 \/ ~down skc24 $_136 \/ ~event skc24 \/ ~fellow $_140 \/ % 0.20/0.50 ~fellow skc28 \/ ~front $_139 \/ ~front skc29 \/ ~furniture $_139 \/ % 0.20/0.50 ~furniture skc29 \/ ~hollywood skc25 \/ ~in $_140 $_139 \/ % 0.20/0.50 ~lonely $_136 \/ ~man $_140 \/ ~man skc28 \/ ~old $_135 \/ % 0.20/0.50 ~seat $_139 \/ ~seat skc29 \/ ~street $_136 \/ ~way $_136 \/ % 0.20/0.50 ~white $_135 \/ ~young $_140 \/ ~young skc28 \/ skc28 = $_140 \/ ssSkC0 % 0.20/0.50 |- ~barrel skc23 $_145 \/ ~car $_145 \/ ~chevy $_145 \/ ~city skc25 \/ % 0.20/0.50 ~dirty $_145 \/ ~down skc23 $_146 \/ ~event skc23 \/ ~fellow $_150 \/ % 0.20/0.50 ~fellow skc28 \/ ~front $_149 \/ ~front skc29 \/ ~furniture $_149 \/ % 0.20/0.50 ~furniture skc29 \/ ~hollywood skc25 \/ ~in $_150 $_149 \/ % 0.20/0.50 ~lonely $_146 \/ ~man $_150 \/ ~man skc28 \/ ~old $_145 \/ % 0.20/0.50 ~seat $_149 \/ ~seat skc29 \/ ~street $_146 \/ ~way $_146 \/ % 0.20/0.50 ~white $_145 \/ ~young $_150 \/ ~young skc28 \/ skc28 = $_150 \/ ssSkC0 % 0.20/0.50 |- ~barrel skc15 $_162 \/ ~car $_162 \/ ~chevy $_162 \/ ~city skc18 \/ % 0.20/0.50 ~dirty $_162 \/ ~down skc15 $_161 \/ ~event skc15 \/ ~fellow $_165 \/ % 0.20/0.50 ~front skc17 \/ ~furniture skc17 \/ ~hollywood skc18 \/ % 0.20/0.50 ~in $_165 skc17 \/ ~lonely $_161 \/ ~man $_165 \/ ~man skc16 \/ % 0.20/0.50 ~old $_162 \/ ~ssSkC0 \/ ~street $_161 \/ ~way $_161 \/ ~white $_162 \/ % 0.20/0.50 ~young $_165 \/ ~young skc16 \/ skc16 = $_165 \/ skc24 = skc23 % 0.20/0.50 |- ~barrel skc21 $_162 \/ ~car $_162 \/ ~chevy $_162 \/ ~city skc22 \/ % 0.20/0.50 ~dirty $_162 \/ ~down skc21 $_161 \/ ~fellow $_165 \/ ~front skc17 \/ % 0.20/0.50 ~furniture skc17 \/ ~in $_165 skc17 \/ ~lonely $_161 \/ ~man $_165 \/ % 0.20/0.50 ~man skc16 \/ ~old $_162 \/ ~ssSkC0 \/ ~street $_161 \/ ~way $_161 \/ % 0.20/0.50 ~white $_162 \/ ~young $_165 \/ ~young skc16 \/ skc16 = $_165 \/ % 0.20/0.50 skc24 = skc23 % 0.20/0.50 |- ~barrel skc16 $_173 \/ ~car $_173 \/ ~chevy $_173 \/ ~city skc17 \/ % 0.20/0.50 ~dirty $_173 \/ ~down skc16 $_172 \/ ~event skc16 \/ ~fellow $_176 \/ % 0.20/0.50 ~fellow skc15 \/ ~furniture skc18 \/ ~hollywood skc17 \/ % 0.20/0.50 ~in $_176 skc18 \/ ~lonely $_172 \/ ~man $_176 \/ ~man skc15 \/ % 0.20/0.50 ~old $_173 \/ ~seat skc18 \/ ~ssSkC0 \/ ~street $_172 \/ ~way $_172 \/ % 0.20/0.50 ~white $_173 \/ ~young $_176 \/ skc15 = $_176 \/ skc24 = skc23 % 0.20/0.50 |- ~barrel skc21 $_173 \/ ~car $_173 \/ ~chevy $_173 \/ ~city skc22 \/ % 0.20/0.50 ~dirty $_173 \/ ~down skc21 $_172 \/ ~fellow $_176 \/ ~fellow skc15 \/ % 0.20/0.50 ~furniture skc18 \/ ~in $_176 skc18 \/ ~lonely $_172 \/ ~man $_176 \/ % 0.20/0.50 ~man skc15 \/ ~old $_173 \/ ~seat skc18 \/ ~ssSkC0 \/ ~street $_172 \/ % 0.20/0.50 ~way $_172 \/ ~white $_173 \/ ~young $_176 \/ skc15 = $_176 \/ % 0.20/0.50 skc24 = skc23 % 0.20/0.50 |- ~barrel skc16 $_189 \/ ~car $_189 \/ ~chevy $_189 \/ ~city skc17 \/ % 0.20/0.50 ~dirty $_189 \/ ~down skc16 $_188 \/ ~event skc16 \/ ~fellow $_192 \/ % 0.20/0.50 ~fellow skc21 \/ ~front skc22 \/ ~furniture skc22 \/ ~hollywood skc17 \/ % 0.20/0.50 ~in $_192 skc22 \/ ~lonely $_188 \/ ~man $_192 \/ ~man skc21 \/ % 0.20/0.50 ~old $_189 \/ ~seat skc22 \/ ~ssSkC0 \/ ~street $_188 \/ ~way $_188 \/ % 0.20/0.50 ~white $_189 \/ ~young $_192 \/ ~young skc21 \/ $_192 = skc21 \/ % 0.20/0.50 skc24 = skc23 % 0.20/0.51 |- ~barrel skc15 $_197 \/ ~car $_197 \/ ~chevy $_197 \/ ~city skc18 \/ % 0.20/0.51 ~dirty $_197 \/ ~down skc15 $_196 \/ ~event skc15 \/ ~fellow $_200 \/ % 0.20/0.51 ~fellow skc21 \/ ~front skc22 \/ ~furniture skc22 \/ ~hollywood skc18 \/ % 0.20/0.51 ~in $_200 skc22 \/ ~lonely $_196 \/ ~man $_200 \/ ~man skc21 \/ % 0.20/0.51 ~old $_197 \/ ~seat skc22 \/ ~ssSkC0 \/ ~street $_196 \/ ~way $_196 \/ % 0.20/0.51 ~white $_197 \/ ~young $_200 \/ ~young skc21 \/ skc21 = $_200 \/ % 0.20/0.51 skc24 = skc23 % 0.20/0.51 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.51 %------------------------------------------------------------------------------