↑ Up

Metis---2.4.SAT-Sat.s

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

% Computer : n003.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 : Thu Jul 21 09:03:43 EDT 2022

% Result   : Satisfiable 0.20s 0.58s
% Output   : Saturation 0.20s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12  % Problem  : SYN531-1 : TPTP v8.1.0. Released v2.1.0.
% 0.11/0.13  % Command  : metis --show proof --show saturation %s
% 0.13/0.34  % Computer : n003.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 600
% 0.13/0.34  % DateTime : Tue Jul 12 04:32:45 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.13/0.35  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.20/0.58  % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.58  
% 0.20/0.58  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.58  |- c4_0 \/ c5_0
% 0.20/0.58  |- ndr1_0 \/ ssSkC3
% 0.20/0.58  |- ndr1_0 \/ ssSkC2
% 0.20/0.58  |- ndr1_0 \/ ssSkC1
% 0.20/0.58  |- ~c5_0 \/ c2_0
% 0.20/0.58  |- c2_1 a400 \/ ssSkC3
% 0.20/0.58  |- c5_1 a392 \/ ssSkC2
% 0.20/0.58  |- c3_1 a392 \/ ssSkC2
% 0.20/0.58  |- c1_1 a392 \/ ssSkC2
% 0.20/0.58  |- ndr1_1 $U \/ ssSkP0 $U
% 0.20/0.58  |- ~c5_0 \/ c3_0 \/ ndr1_0
% 0.20/0.58  |- ~ssSkC2 \/ c5_0 \/ ndr1_1 a393
% 0.20/0.58  |- ~ssSkC2 \/ c3_1 a393 \/ c5_0
% 0.20/0.58  |- ~c2_0 \/ ~c3_0
% 0.20/0.58  |- ~c5_0 \/ c1_0 \/ c3_0
% 0.20/0.58  |- ~c1_1 a400 \/ ssSkC3
% 0.20/0.58  |- ~c1_1 a390 \/ ssSkC1
% 0.20/0.58  |- c5_2 $U a387 \/ ssSkP0 $U
% 0.20/0.58  |- c2_2 $U a387 \/ ssSkP0 $U
% 0.20/0.58  |- c3_2 $U a387 \/ ssSkP0 $U
% 0.20/0.58  |- ~c2_0 \/ ~ssSkC3 \/ ndr1_1 a401
% 0.20/0.58  |- ~c2_0 \/ ~ssSkC3 \/ c4_1 a401
% 0.20/0.58  |- ~ssSkC2 \/ c2_2 a393 a395 \/ c5_0
% 0.20/0.58  |- ~ssSkC2 \/ c5_0 \/ c5_2 a393 a394
% 0.20/0.58  |- ~c2_0 \/ ~ssSkC3 \/ c2_2 a401 a402
% 0.20/0.58  |- ~c2_1 a399 \/ ~c5_0 \/ c3_0
% 0.20/0.58  |- ~c1_0 \/ ~c2_0 \/ ndr1_1 a396
% 0.20/0.58  |- ~c1_0 \/ ~c2_0 \/ c4_1 a396
% 0.20/0.58  |- ~c1_2 a393 a395 \/ ~ssSkC2 \/ c5_0
% 0.20/0.58  |- ~c2_2 a393 a394 \/ ~ssSkC2 \/ c5_0
% 0.20/0.58  |- ~c3_2 a393 a394 \/ ~ssSkC2 \/ c5_0
% 0.20/0.58  |- ~ndr1_0 \/ c1_0 \/ c4_0 \/ c4_1 $U \/ ndr1_1 $U
% 0.20/0.58  |- ~c1_2 a401 a402 \/ ~c2_0 \/ ~ssSkC3
% 0.20/0.58  |- ~c1_0 \/ ~c2_0 \/ c3_2 a396 a397
% 0.20/0.58  |- ~c1_0 \/ ~c2_0 \/ ~c3_1 a396
% 0.20/0.58  |- ~ndr1_0 \/ c1_0 \/ c1_2 $U a410 \/ c4_0 \/ c4_1 $U
% 0.20/0.58  |- ~ndr1_0 \/ c1_0 \/ c2_2 $U a410 \/ c4_0 \/ c4_1 $U
% 0.20/0.58  |- ~c1_0 \/ ~c2_0 \/ ~c5_2 a396 a397
% 0.20/0.58  |- ~c1_0 \/ ~c2_0 \/ ~c4_2 a396 a397
% 0.20/0.58  |- ~c3_2 a400 $U \/ ~ndr1_1 a400 \/ ssSkC3
% 0.20/0.58  |- ~c4_0 \/ ~ndr1_0 \/ c2_1 $U \/ c4_1 $U \/ c5_1 $U
% 0.20/0.58  |- ~c4_2 $U a410 \/ ~ndr1_0 \/ c1_0 \/ c4_0 \/ c4_1 $U
% 0.20/0.58  |- ~ndr1_0 \/ ~ssSkP0 $U \/ c2_1 $U \/ c3_2 $U a388 \/ ssSkC0
% 0.20/0.58  |- ~ndr1_0 \/ ~ssSkP0 $U \/ c2_1 $U \/ c2_2 $U a388 \/ ssSkC0
% 0.20/0.58  |- ~c1_1 $U \/ ~c5_1 $U \/ ~ndr1_0 \/ ~ssSkC0 \/ ndr1_1 $U
% 0.20/0.58  |- ~c2_0 \/ ~c3_1 $U \/ ~ndr1_0 \/ c4_1 $U \/ c5_1 $U
% 0.20/0.58  |- ~ndr1_1 a390 \/ c1_2 a390 $U \/ c5_2 a390 $U \/ ssSkC1
% 0.20/0.58  |- ~c1_2 $U a388 \/ ~ndr1_0 \/ ~ssSkP0 $U \/ c2_1 $U \/ ssSkC0
% 0.20/0.58  |- ~c1_1 $U \/ ~c3_1 $U \/ ~ndr1_0 \/ c3_0 \/ c4_0 \/ ndr1_1 $U
% 0.20/0.58  |- ~c1_1 $U \/ ~c5_1 $U \/ ~ndr1_0 \/ ~ssSkC0 \/ c1_2 $U a389
% 0.20/0.58  |- ~c3_1 $U \/ ~c5_0 \/ ~ndr1_0 \/ c1_1 $U \/ c2_1 $U \/ ndr1_1 a403
% 0.20/0.58  |- ~c3_1 $U \/ ~c5_0 \/ ~ndr1_0 \/ c1_1 $U \/ c1_1 a403 \/ c2_1 $U
% 0.20/0.58  |- ~c3_1 $U \/ ~c5_0 \/ ~ndr1_0 \/ c1_1 $U \/ c2_1 $U \/ c2_1 a403
% 0.20/0.58  |- ~c1_1 $U \/ ~c3_1 $U \/ ~ndr1_0 \/ c3_0 \/ c3_2 $U a398 \/ c4_0
% 0.20/0.58  |- ~c1_1 $U \/ ~c3_2 $U a389 \/ ~c5_1 $U \/ ~ndr1_0 \/ ~ssSkC0
% 0.20/0.58  |- ~ndr1_0 \/ ~ndr1_1 $U \/ ~ssSkC4 \/ c1_2 $U $V \/ c3_2 $U $V \/
% 0.20/0.58     c4_2 $U a406
% 0.20/0.58  |- ~ndr1_0 \/ ~ndr1_1 $U \/ ~ssSkC4 \/ c1_2 $U $V \/ c2_2 $U a406 \/
% 0.20/0.58     c3_2 $U $V
% 0.20/0.58  |- ~ndr1_0 \/ ~ndr1_1 $U \/ ~ssSkC4 \/ c1_2 $U $V \/ c3_2 $U $V \/
% 0.20/0.58     c3_2 $U a406
% 0.20/0.58  |- ~c3_1 $U \/ ~c5_0 \/ ~ndr1_0 \/ c1_1 $U \/ c2_1 $U \/ c3_2 a403 a404
% 0.20/0.58  |- ~c3_1 $U \/ ~c4_2 a403 a404 \/ ~c5_0 \/ ~ndr1_0 \/ c1_1 $U \/ c2_1 $U
% 0.20/0.58  |- ~c1_0 \/ ~c5_0 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c2_2 $U $V \/ c3_1 $U \/
% 0.20/0.58     c3_2 $U $V
% 0.20/0.58  |- ~ndr1_0 \/ ~ndr1_1 $U \/ c1_1 $U \/ c2_0 \/ c2_2 $U $V \/ c3_0 \/
% 0.20/0.58     c3_2 $U $V \/ c4_2 $U $V
% 0.20/0.58  |- ~c1_2 a399 $U \/ ~c2_2 a399 $U \/ ~c5_0 \/ ~c5_2 a399 $U \/
% 0.20/0.58     ~ndr1_1 a399 \/ c3_0
% 0.20/0.58  |- ~c3_1 a391 \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ ~ssSkC1 \/
% 0.20/0.58     c1_2 $U $V \/ c3_1 $U \/ c5_1 $U
% 0.20/0.58  |- ~c4_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $W \/ c2_2 $U $V \/
% 0.20/0.58     c2_2 $U $W \/ c5_1 $U \/ ndr1_1 a407
% 0.20/0.58  |- ~c4_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $W \/ c1_2 a407 a409 \/
% 0.20/0.58     c2_2 $U $V \/ c2_2 $U $W \/ c5_1 $U
% 0.20/0.58  |- ~c4_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $W \/ c2_2 $U $V \/
% 0.20/0.58     c2_2 $U $W \/ c2_2 a407 a409 \/ c5_1 $U
% 0.20/0.58  |- ~c4_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $W \/ c1_2 a407 a408 \/
% 0.20/0.58     c2_2 $U $V \/ c2_2 $U $W \/ c5_1 $U
% 0.20/0.58  |- ~c2_1 a407 \/ ~c4_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $W \/
% 0.20/0.58     c2_2 $U $V \/ c2_2 $U $W \/ c5_1 $U
% 0.20/0.58  |- ~c3_2 a407 a409 \/ ~c4_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $W \/
% 0.20/0.58     c2_2 $U $V \/ c2_2 $U $W \/ c5_1 $U
% 0.20/0.58  |- ~c3_2 a407 a408 \/ ~c4_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $W \/
% 0.20/0.58     c2_2 $U $V \/ c2_2 $U $W \/ c5_1 $U
% 0.20/0.58  |- ~c4_2 $U $V \/ ~c5_2 a407 a408 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $W \/
% 0.20/0.58     c2_2 $U $V \/ c2_2 $U $W \/ c5_1 $U
% 0.20/0.58  |- ~c1_1 $U \/ ~c3_2 $U $V \/ ~c5_2 $U a405 \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.20/0.58     c2_2 $U $V \/ c5_2 $U $V \/ ssSkC4
% 0.20/0.58  |- ~c1_1 $U \/ ~c2_2 $U a405 \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.20/0.58     c2_2 $U $V \/ c5_2 $U $V \/ ssSkC4
% 0.20/0.58  |- ~c1_1 $U \/ ~c1_2 $U a405 \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.20/0.58     c2_2 $U $V \/ c5_2 $U $V \/ ssSkC4
% 0.20/0.58  |- ~c3_2 $U $V \/ ~c5_2 a391 $W \/ ~ndr1_0 \/ ~ndr1_1 $U \/ ~ndr1_1 a391 \/
% 0.20/0.58     ~ssSkC1 \/ c1_2 $U $V \/ c1_2 a391 $W \/ c3_1 $U \/ c4_2 a391 $W \/
% 0.20/0.58     c5_1 $U
% 0.20/0.58  |- ~c1_2 a391 $W \/ ~c3_2 $U $V \/ ~c3_2 a391 $W \/ ~ndr1_0 \/
% 0.20/0.58     ~ndr1_1 $U \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_2 $U $V \/ c3_1 $U \/
% 0.20/0.58     c4_2 a391 $W \/ c5_1 $U
% 0.20/0.58  |- c2_0 \/ c4_0
% 0.20/0.58  |- c5_0 \/ ndr1_0
% 0.20/0.58  |- ~c2_0 \/ ndr1_0
% 0.20/0.58  |- c3_0 \/ c4_0 \/ ndr1_0
% 0.20/0.58  |- c1_0 \/ c3_0 \/ c4_0
% 0.20/0.58  |- ~c2_0 \/ c4_0
% 0.20/0.58  |- ~ndr1_1 a400 \/ ssSkC3 \/ ssSkP0 a400
% 0.20/0.58  |- ~ndr1_0 \/ ~ssSkC0 \/ ndr1_1 a392 \/ ssSkC2
% 0.20/0.58  |- ~ndr1_0 \/ c2_1 $_10 \/ ndr1_1 $_10 \/ ssSkC0
% 0.20/0.58  |- c2_1 $_11 \/ c3_0 \/ c4_0 \/ ndr1_1 $_11 \/ ssSkC0
% 0.20/0.58  |- c2_1 $_11 \/ c5_0 \/ ndr1_1 $_11 \/ ssSkC0
% 0.20/0.58  |- c1_2 a390 $U \/ c2_1 a390 \/ c5_0 \/ c5_2 a390 $U \/ ssSkC0 \/ ssSkC1
% 0.20/0.58  |- ~c4_0 \/ c2_1 $_13 \/ c4_1 $_13 \/ c5_0 \/ c5_1 $_13
% 0.20/0.58  |- c1_0 \/ c2_1 $_16 \/ c3_0 \/ c4_1 $_16 \/ c5_0 \/ c5_1 $_16
% 0.20/0.58  |- c2_0 \/ c2_1 $_16 \/ c4_1 $_16 \/ c5_0 \/ c5_1 $_16
% 0.20/0.58  |- c1_2 a390 $U \/ c2_1 a390 \/ c3_0 \/ c4_0 \/ c5_2 a390 $U \/ ssSkC0 \/
% 0.20/0.58     ssSkC1
% 0.20/0.58  |- ~ndr1_0 \/ ~ssSkC0 \/ c1_2 a392 a389 \/ ssSkC2
% 0.20/0.58  |- ~c1_1 $_23 \/ ~ndr1_0 \/ ~ssSkC0 \/ c1_2 $_23 a389 \/ c2_0 \/
% 0.20/0.58     c2_1 $_23 \/ c4_1 $_23 \/ c5_0
% 0.20/0.58  |- ~c1_1 $_23 \/ ~ndr1_0 \/ ~ssSkC0 \/ c2_0 \/ c2_1 $_23 \/ c4_1 $_23 \/
% 0.20/0.58     c5_0 \/ ndr1_1 $_23
% 0.20/0.58  |- c3_0 \/ c4_0 \/ ndr1_1 a392 \/ ssSkC2
% 0.20/0.58  |- c3_0 \/ c3_2 a392 a398 \/ c4_0 \/ ssSkC2
% 0.20/0.58  |- ~c1_1 $_29 \/ ~ndr1_0 \/ ~ssSkC0 \/ c1_0 \/ c1_2 $_29 a389 \/
% 0.20/0.58     c2_1 $_29 \/ c3_0 \/ c4_1 $_29 \/ c5_0
% 0.20/0.58  |- ~c1_1 $_29 \/ ~ndr1_0 \/ ~ssSkC0 \/ c1_0 \/ c2_1 $_29 \/ c3_0 \/
% 0.20/0.58     c4_1 $_29 \/ c5_0 \/ ndr1_1 $_29
% 0.20/0.58  |- ~c1_2 a399 a387 \/ ~c5_0 \/ ~ndr1_1 a399 \/ c3_0 \/ ssSkP0 a399
% 0.20/0.58  |- ~ndr1_0 \/ ~ssSkC4 \/ c1_2 a392 $_36 \/ c3_0 \/ c3_2 a392 $_36 \/
% 0.20/0.58     c4_0 \/ c4_2 a392 a406 \/ ssSkC2
% 0.20/0.58  |- ~ndr1_0 \/ ~ssSkC4 \/ c1_2 $_35 $_36 \/ c2_1 $_35 \/ c3_0 \/
% 0.20/0.58     c3_2 $_35 $_36 \/ c4_0 \/ c4_2 $_35 a406 \/ ssSkC0
% 0.20/0.58  |- ~ndr1_0 \/ ~ssSkC4 \/ c1_2 $_35 $_36 \/ c2_1 $_35 \/ c3_2 $_35 $_36 \/
% 0.20/0.58     c4_2 $_35 a406 \/ c5_0 \/ ssSkC0
% 0.20/0.58  |- ~ndr1_0 \/ ~ssSkC4 \/ c1_2 a392 $_38 \/ c2_2 a392 a406 \/ c3_0 \/
% 0.20/0.58     c3_2 a392 $_38 \/ c4_0 \/ ssSkC2
% 0.20/0.58  |- ~ndr1_0 \/ ~ssSkC4 \/ c1_2 $_37 $_38 \/ c2_1 $_37 \/ c2_2 $_37 a406 \/
% 0.20/0.58     c3_0 \/ c3_2 $_37 $_38 \/ c4_0 \/ ssSkC0
% 0.20/0.58  |- ~ndr1_0 \/ ~ssSkC4 \/ c1_2 $_37 $_38 \/ c2_1 $_37 \/ c2_2 $_37 a406 \/
% 0.20/0.58     c3_2 $_37 $_38 \/ c5_0 \/ ssSkC0
% 0.20/0.58  |- ~ndr1_0 \/ ~ssSkC4 \/ c1_2 a392 $_40 \/ c3_0 \/ c3_2 a392 $_40 \/
% 0.20/0.58     c3_2 a392 a406 \/ c4_0 \/ ssSkC2
% 0.20/0.58  |- ~ndr1_0 \/ ~ssSkC4 \/ c1_2 $_39 $_40 \/ c2_1 $_39 \/ c3_0 \/
% 0.20/0.58     c3_2 $_39 $_40 \/ c3_2 $_39 a406 \/ c4_0 \/ ssSkC0
% 0.20/0.58  |- ~ndr1_0 \/ ~ssSkC4 \/ c1_2 $_39 $_40 \/ c2_1 $_39 \/ c3_2 $_39 $_40 \/
% 0.20/0.58     c3_2 $_39 a406 \/ c5_0 \/ ssSkC0
% 0.20/0.58  |- ~c3_1 a391 \/ ~ndr1_0 \/ ~ndr1_1 $_52 \/ ~ssSkC1 \/ c1_2 $_52 a387 \/
% 0.20/0.58     c3_1 $_52 \/ c5_1 $_52 \/ ssSkP0 $_52
% 0.20/0.58  |- ~c3_1 a391 \/ ~ndr1_0 \/ ~ssSkC1 \/ c1_2 $_54 a387 \/ c2_1 $_54 \/
% 0.20/0.58     c3_0 \/ c3_1 $_54 \/ c4_0 \/ c5_1 $_54 \/ ssSkC0 \/ ssSkP0 $_54
% 0.20/0.58  |- ~c3_1 a391 \/ ~ndr1_0 \/ ~ssSkC1 \/ c1_2 $_54 a387 \/ c2_1 $_54 \/
% 0.20/0.58     c3_1 $_54 \/ c5_0 \/ c5_1 $_54 \/ ssSkC0 \/ ssSkP0 $_54
% 0.20/0.58  |- ~c1_1 a392 \/ ~c2_2 a392 a405 \/ ~ndr1_0 \/ ~ndr1_1 a392 \/
% 0.20/0.58     c2_2 a392 a398 \/ c3_0 \/ c4_0 \/ c5_2 a392 a398 \/ ssSkC2 \/ ssSkC4
% 0.20/0.58  |- ~c1_1 a392 \/ ~c1_2 a392 a405 \/ ~ndr1_0 \/ ~ndr1_1 a392 \/
% 0.20/0.58     c2_2 a392 a398 \/ c3_0 \/ c4_0 \/ c5_2 a392 a398 \/ ssSkC2 \/ ssSkC4
% 0.20/0.58  |- ~c1_0 \/ c2_1 $_71 \/ c2_2 $_71 $_72 \/ c3_0 \/ c3_1 $_71 \/
% 0.20/0.58     c3_2 $_71 $_72 \/ c4_0 \/ ssSkC0
% 0.20/0.58  |- c1_1 $_81 \/ c2_0 \/ c2_1 $_81 \/ c2_2 $_81 $_82 \/ c3_0 \/
% 0.20/0.58     c3_2 $_81 $_82 \/ c4_2 $_81 $_82 \/ c5_0 \/ ssSkC0
% 0.20/0.58  |- ~c5_2 a391 $_111 \/ ~ndr1_0 \/ ~ndr1_1 $_109 \/ ~ndr1_1 a391 \/
% 0.20/0.58     ~ssSkC1 \/ c1_2 $_109 a387 \/ c1_2 a391 $_111 \/ c3_1 $_109 \/
% 0.20/0.58     c4_2 a391 $_111 \/ c5_1 $_109 \/ ssSkP0 $_109
% 0.20/0.58  |- ~c3_2 $_109 $_110 \/ ~ndr1_0 \/ ~ndr1_1 $_109 \/ ~ndr1_1 a391 \/
% 0.20/0.58     ~ssSkC1 \/ c1_2 $_109 $_110 \/ c1_2 a391 a387 \/ c3_1 $_109 \/
% 0.20/0.58     c4_2 a391 a387 \/ c5_1 $_109 \/ ssSkP0 a391
% 0.20/0.58  |- ~ndr1_0 \/ ~ndr1_1 $_112 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/
% 0.20/0.58     c1_2 $_112 a387 \/ c1_2 a391 a387 \/ c3_1 $_112 \/ c4_2 a391 a387 \/
% 0.20/0.58     c5_1 $_112 \/ ssSkP0 $_112 \/ ssSkP0 a391
% 0.20/0.58  |- ~c5_2 a391 $_113 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/
% 0.20/0.58     c1_2 $_112 a387 \/ c1_2 a391 $_113 \/ c2_1 $_112 \/ c3_0 \/
% 0.20/0.58     c3_1 $_112 \/ c4_0 \/ c4_2 a391 $_113 \/ c5_1 $_112 \/ ssSkC0 \/
% 0.20/0.58     ssSkP0 $_112
% 0.20/0.58  |- ~c5_2 a391 $_113 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/
% 0.20/0.58     c1_2 $_112 a387 \/ c1_2 a391 $_113 \/ c2_1 $_112 \/ c3_1 $_112 \/
% 0.20/0.58     c4_2 a391 $_113 \/ c5_0 \/ c5_1 $_112 \/ ssSkC0 \/ ssSkP0 $_112
% 0.20/0.58  |- ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_2 a391 a387 \/ c3_1 a391 \/
% 0.20/0.58     c4_2 a391 a387 \/ c5_1 a391 \/ ssSkP0 a391
% 0.20/0.58  |- ~ndr1_0 \/ ~ssSkC1 \/ c1_2 a391 a387 \/ c2_1 a391 \/ c3_0 \/
% 0.20/0.58     c3_1 a391 \/ c4_0 \/ c4_2 a391 a387 \/ c5_1 a391 \/ ssSkC0 \/
% 0.20/0.58     ssSkP0 a391
% 0.20/0.58  |- ~ndr1_0 \/ ~ssSkC1 \/ c1_2 a391 a387 \/ c2_1 a391 \/ c3_1 a391 \/
% 0.20/0.58     c4_2 a391 a387 \/ c5_0 \/ c5_1 a391 \/ ssSkC0 \/ ssSkP0 a391
% 0.20/0.58  |- ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_2 $_114 a387 \/
% 0.20/0.58     c1_2 a391 a387 \/ c2_1 $_114 \/ c3_0 \/ c3_1 $_114 \/ c4_0 \/
% 0.20/0.58     c4_2 a391 a387 \/ c5_1 $_114 \/ ssSkC0 \/ ssSkP0 $_114 \/ ssSkP0 a391
% 0.20/0.59  |- ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_2 $_114 a387 \/
% 0.20/0.59     c1_2 a391 a387 \/ c2_1 $_114 \/ c3_1 $_114 \/ c4_2 a391 a387 \/ c5_0 \/
% 0.20/0.59     c5_1 $_114 \/ ssSkC0 \/ ssSkP0 $_114 \/ ssSkP0 a391
% 0.20/0.59  |- ~ndr1_0 \/ ~ndr1_1 $_114 \/ ~ssSkC1 \/ c1_2 $_114 a387 \/
% 0.20/0.59     c1_2 a391 a387 \/ c2_1 a391 \/ c3_0 \/ c3_1 $_114 \/ c4_0 \/
% 0.20/0.59     c4_2 a391 a387 \/ c5_1 $_114 \/ ssSkC0 \/ ssSkP0 $_114 \/ ssSkP0 a391
% 0.20/0.59  |- ~ndr1_0 \/ ~ndr1_1 $_114 \/ ~ssSkC1 \/ c1_2 $_114 a387 \/
% 0.20/0.59     c1_2 a391 a387 \/ c2_1 a391 \/ c3_1 $_114 \/ c4_2 a391 a387 \/ c5_0 \/
% 0.20/0.59     c5_1 $_114 \/ ssSkC0 \/ ssSkP0 $_114 \/ ssSkP0 a391
% 0.20/0.59  |- ~c1_2 a391 $_119 \/ ~c3_2 a391 $_119 \/ ~ndr1_0 \/ ~ndr1_1 $_117 \/
% 0.20/0.59     ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_2 $_117 a387 \/ c3_1 $_117 \/
% 0.20/0.59     c4_2 a391 $_119 \/ c5_1 $_117 \/ ssSkP0 $_117
% 0.20/0.59  |- ~c1_2 a391 a387 \/ ~c3_2 $_117 $_118 \/ ~ndr1_0 \/ ~ndr1_1 $_117 \/
% 0.20/0.59     ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_2 $_117 $_118 \/ c3_1 $_117 \/
% 0.20/0.59     c4_2 a391 a387 \/ c5_1 $_117 \/ ssSkP0 a391
% 0.20/0.59  |- ~c1_2 a391 a387 \/ ~ndr1_0 \/ ~ndr1_1 $_120 \/ ~ndr1_1 a391 \/
% 0.20/0.59     ~ssSkC1 \/ c1_2 $_120 a387 \/ c3_1 $_120 \/ c4_2 a391 a387 \/
% 0.20/0.59     c5_1 $_120 \/ ssSkP0 $_120 \/ ssSkP0 a391
% 0.20/0.59  |- ~c1_2 a391 $_121 \/ ~c3_2 a391 $_121 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/
% 0.20/0.59     ~ssSkC1 \/ c1_2 $_120 a387 \/ c2_1 $_120 \/ c3_0 \/ c3_1 $_120 \/
% 0.20/0.59     c4_0 \/ c4_2 a391 $_121 \/ c5_1 $_120 \/ ssSkC0 \/ ssSkP0 $_120
% 0.20/0.59  |- ~c1_2 a391 $_121 \/ ~c3_2 a391 $_121 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/
% 0.20/0.59     ~ssSkC1 \/ c1_2 $_120 a387 \/ c2_1 $_120 \/ c3_1 $_120 \/
% 0.20/0.59     c4_2 a391 $_121 \/ c5_0 \/ c5_1 $_120 \/ ssSkC0 \/ ssSkP0 $_120
% 0.20/0.59  |- ~c1_2 a391 a387 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/
% 0.20/0.59     c1_2 $_122 a387 \/ c2_1 $_122 \/ c3_0 \/ c3_1 $_122 \/ c4_0 \/
% 0.20/0.59     c4_2 a391 a387 \/ c5_1 $_122 \/ ssSkC0 \/ ssSkP0 $_122 \/ ssSkP0 a391
% 0.20/0.59  |- ~c1_2 a391 a387 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/
% 0.20/0.59     c1_2 $_122 a387 \/ c2_1 $_122 \/ c3_1 $_122 \/ c4_2 a391 a387 \/ c5_0 \/
% 0.20/0.59     c5_1 $_122 \/ ssSkC0 \/ ssSkP0 $_122 \/ ssSkP0 a391
% 0.20/0.59  |- ~ndr1_0 \/ ~ssSkC1 \/ c1_2 $_127 a387 \/ c1_2 a391 a387 \/ c2_1 $_127 \/
% 0.20/0.59     c2_1 a391 \/ c3_1 $_127 \/ c4_2 a391 a387 \/ c5_0 \/ c5_1 $_127 \/
% 0.20/0.59     ssSkC0 \/ ssSkP0 $_127 \/ ssSkP0 a391
% 0.20/0.59  |- ~ndr1_0 \/ ~ssSkC1 \/ c1_2 $_130 a387 \/ c1_2 a391 a387 \/ c2_1 $_130 \/
% 0.20/0.59     c2_1 a391 \/ c3_0 \/ c3_1 $_130 \/ c4_0 \/ c4_2 a391 a387 \/
% 0.20/0.59     c5_1 $_130 \/ ssSkC0 \/ ssSkP0 $_130 \/ ssSkP0 a391
% 0.20/0.59  |- c1_1 $_140 \/ c1_2 $_140 $_142 \/ c2_0 \/ c2_1 $_140 \/
% 0.20/0.59     c2_2 $_140 $_141 \/ c2_2 $_140 $_142 \/ c3_0 \/ c3_2 $_140 $_141 \/
% 0.20/0.59     c5_0 \/ c5_1 $_140 \/ ndr1_1 a407 \/ ssSkC0
% 0.20/0.59  |- ~c1_2 a391 $_144 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 a391 \/
% 0.20/0.59     c1_2 $_120 a387 \/ c1_2 a391 $_145 \/ c2_0 \/ c2_1 $_120 \/ c2_1 a391 \/
% 0.20/0.59     c2_2 a391 $_144 \/ c2_2 a391 $_145 \/ c3_0 \/ c3_1 $_120 \/
% 0.20/0.59     c4_2 a391 $_144 \/ c5_0 \/ c5_1 $_120 \/ c5_1 a391 \/ ndr1_1 a407 \/
% 0.20/0.59     ssSkC0 \/ ssSkP0 $_120
% 0.20/0.59  |- ~c1_2 a391 $_144 \/ ~ndr1_0 \/ ~ndr1_1 $_117 \/ ~ndr1_1 a391 \/
% 0.20/0.59     ~ssSkC1 \/ c1_1 a391 \/ c1_2 $_117 a387 \/ c1_2 a391 $_145 \/ c2_0 \/
% 0.20/0.59     c2_1 a391 \/ c2_2 a391 $_144 \/ c2_2 a391 $_145 \/ c3_0 \/ c3_1 $_117 \/
% 0.20/0.59     c4_2 a391 $_144 \/ c5_0 \/ c5_1 $_117 \/ c5_1 a391 \/ ndr1_1 a407 \/
% 0.20/0.59     ssSkC0 \/ ssSkP0 $_117
% 0.20/0.59  |- ~c1_2 a391 $_144 \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.20/0.59     ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 a391 \/ c1_2 $U $V \/ c1_2 a391 $_145 \/
% 0.20/0.59     c2_0 \/ c2_1 a391 \/ c2_2 a391 $_144 \/ c2_2 a391 $_145 \/ c3_0 \/
% 0.20/0.59     c3_1 $U \/ c4_2 a391 $_144 \/ c5_0 \/ c5_1 $U \/ c5_1 a391 \/
% 0.20/0.59     ndr1_1 a407 \/ ssSkC0
% 0.20/0.59  |- ~ssSkC2 \/ c1_1 a393 \/ c1_2 a393 $_145 \/ c2_0 \/ c2_1 a393 \/
% 0.20/0.59     c2_2 a393 $_145 \/ c2_2 a393 a394 \/ c3_0 \/ c5_0 \/ c5_1 a393 \/
% 0.20/0.59     ndr1_1 a407 \/ ssSkC0
% 0.20/0.59  |- ~c2_1 a407 \/ ~ndr1_0 \/ c1_1 $_147 \/ c1_2 $_147 $_149 \/ c2_0 \/
% 0.20/0.59     c2_1 $_147 \/ c2_2 $_147 $_148 \/ c2_2 $_147 $_149 \/ c3_0 \/
% 0.20/0.59     c3_2 $_147 $_148 \/ c5_0 \/ c5_1 $_147 \/ ssSkC0
% 0.20/0.59  |- c1_1 $_156 \/ c1_2 $_156 $_158 \/ c1_2 a407 a409 \/ c2_0 \/
% 0.20/0.59     c2_1 $_156 \/ c2_2 $_156 $_157 \/ c2_2 $_156 $_158 \/ c3_0 \/
% 0.20/0.59     c3_2 $_156 $_157 \/ c5_0 \/ c5_1 $_156 \/ ssSkC0
% 0.20/0.59  |- ~c1_2 a391 $_160 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 a391 \/
% 0.20/0.59     c1_2 $_120 a387 \/ c1_2 a391 $_161 \/ c1_2 a407 a409 \/ c2_0 \/
% 0.20/0.59     c2_1 $_120 \/ c2_1 a391 \/ c2_2 a391 $_160 \/ c2_2 a391 $_161 \/ c3_0 \/
% 0.20/0.59     c3_1 $_120 \/ c4_2 a391 $_160 \/ c5_0 \/ c5_1 $_120 \/ c5_1 a391 \/
% 0.20/0.59     ssSkC0 \/ ssSkP0 $_120
% 0.20/0.59  |- ~c1_2 a391 $_160 \/ ~ndr1_0 \/ ~ndr1_1 $_117 \/ ~ndr1_1 a391 \/
% 0.20/0.59     ~ssSkC1 \/ c1_1 a391 \/ c1_2 $_117 a387 \/ c1_2 a391 $_161 \/
% 0.20/0.59     c1_2 a407 a409 \/ c2_0 \/ c2_1 a391 \/ c2_2 a391 $_160 \/
% 0.20/0.59     c2_2 a391 $_161 \/ c3_0 \/ c3_1 $_117 \/ c4_2 a391 $_160 \/ c5_0 \/
% 0.20/0.59     c5_1 $_117 \/ c5_1 a391 \/ ssSkC0 \/ ssSkP0 $_117
% 0.20/0.59  |- ~c1_2 a391 $_160 \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.20/0.59     ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 a391 \/ c1_2 $U $V \/ c1_2 a391 $_161 \/
% 0.20/0.59     c1_2 a407 a409 \/ c2_0 \/ c2_1 a391 \/ c2_2 a391 $_160 \/
% 0.20/0.59     c2_2 a391 $_161 \/ c3_0 \/ c3_1 $U \/ c4_2 a391 $_160 \/ c5_0 \/
% 0.20/0.59     c5_1 $U \/ c5_1 a391 \/ ssSkC0
% 0.20/0.59  |- ~ssSkC2 \/ c1_1 a393 \/ c1_2 a393 $_161 \/ c1_2 a407 a409 \/ c2_0 \/
% 0.20/0.59     c2_1 a393 \/ c2_2 a393 $_161 \/ c2_2 a393 a394 \/ c3_0 \/ c5_0 \/
% 0.20/0.59     c5_1 a393 \/ ssSkC0
% 0.20/0.59  |- c1_1 $_166 \/ c1_2 $_166 $_168 \/ c2_0 \/ c2_1 $_166 \/
% 0.20/0.59     c2_2 $_166 $_167 \/ c2_2 $_166 $_168 \/ c2_2 a407 a409 \/ c3_0 \/
% 0.20/0.59     c3_2 $_166 $_167 \/ c5_0 \/ c5_1 $_166 \/ ssSkC0
% 0.20/0.59  |- ~c1_2 a391 $_170 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 a391 \/
% 0.20/0.59     c1_2 $_120 a387 \/ c1_2 a391 $_171 \/ c2_0 \/ c2_1 $_120 \/ c2_1 a391 \/
% 0.20/0.59     c2_2 a391 $_170 \/ c2_2 a391 $_171 \/ c2_2 a407 a409 \/ c3_0 \/
% 0.20/0.59     c3_1 $_120 \/ c4_2 a391 $_170 \/ c5_0 \/ c5_1 $_120 \/ c5_1 a391 \/
% 0.20/0.59     ssSkC0 \/ ssSkP0 $_120
% 0.20/0.59  |- ~c1_2 a391 $_170 \/ ~ndr1_0 \/ ~ndr1_1 $_117 \/ ~ndr1_1 a391 \/
% 0.20/0.59     ~ssSkC1 \/ c1_1 a391 \/ c1_2 $_117 a387 \/ c1_2 a391 $_171 \/ c2_0 \/
% 0.20/0.59     c2_1 a391 \/ c2_2 a391 $_170 \/ c2_2 a391 $_171 \/ c2_2 a407 a409 \/
% 0.20/0.59     c3_0 \/ c3_1 $_117 \/ c4_2 a391 $_170 \/ c5_0 \/ c5_1 $_117 \/
% 0.20/0.59     c5_1 a391 \/ ssSkC0 \/ ssSkP0 $_117
% 0.20/0.59  |- ~c1_2 a391 $_170 \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.20/0.59     ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 a391 \/ c1_2 $U $V \/ c1_2 a391 $_171 \/
% 0.20/0.59     c2_0 \/ c2_1 a391 \/ c2_2 a391 $_170 \/ c2_2 a391 $_171 \/
% 0.20/0.59     c2_2 a407 a409 \/ c3_0 \/ c3_1 $U \/ c4_2 a391 $_170 \/ c5_0 \/
% 0.20/0.59     c5_1 $U \/ c5_1 a391 \/ ssSkC0
% 0.20/0.59  |- ~ssSkC2 \/ c1_1 a393 \/ c1_2 a393 $_171 \/ c2_0 \/ c2_1 a393 \/
% 0.20/0.59     c2_2 a393 $_171 \/ c2_2 a393 a394 \/ c2_2 a407 a409 \/ c3_0 \/ c5_0 \/
% 0.20/0.59     c5_1 a393 \/ ssSkC0
% 0.20/0.59  |- ~c3_2 a407 a409 \/ ~ndr1_0 \/ c1_1 $_173 \/ c1_2 $_173 $_175 \/ c2_0 \/
% 0.20/0.59     c2_1 $_173 \/ c2_2 $_173 $_174 \/ c2_2 $_173 $_175 \/ c3_0 \/
% 0.20/0.59     c3_2 $_173 $_174 \/ c5_0 \/ c5_1 $_173 \/ ssSkC0
% 0.20/0.59  |- c1_1 $_182 \/ c1_2 $_182 $_184 \/ c1_2 a407 a408 \/ c2_0 \/
% 0.20/0.59     c2_1 $_182 \/ c2_2 $_182 $_183 \/ c2_2 $_182 $_184 \/ c3_0 \/
% 0.20/0.59     c3_2 $_182 $_183 \/ c5_0 \/ c5_1 $_182 \/ ssSkC0
% 0.20/0.59  |- ~c1_2 a391 $_186 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 a391 \/
% 0.20/0.59     c1_2 $_120 a387 \/ c1_2 a391 $_187 \/ c1_2 a407 a408 \/ c2_0 \/
% 0.20/0.59     c2_1 $_120 \/ c2_1 a391 \/ c2_2 a391 $_186 \/ c2_2 a391 $_187 \/ c3_0 \/
% 0.20/0.59     c3_1 $_120 \/ c4_2 a391 $_186 \/ c5_0 \/ c5_1 $_120 \/ c5_1 a391 \/
% 0.20/0.59     ssSkC0 \/ ssSkP0 $_120
% 0.20/0.59  |- ~c1_2 a391 $_186 \/ ~ndr1_0 \/ ~ndr1_1 $_117 \/ ~ndr1_1 a391 \/
% 0.20/0.59     ~ssSkC1 \/ c1_1 a391 \/ c1_2 $_117 a387 \/ c1_2 a391 $_187 \/
% 0.20/0.59     c1_2 a407 a408 \/ c2_0 \/ c2_1 a391 \/ c2_2 a391 $_186 \/
% 0.20/0.59     c2_2 a391 $_187 \/ c3_0 \/ c3_1 $_117 \/ c4_2 a391 $_186 \/ c5_0 \/
% 0.20/0.59     c5_1 $_117 \/ c5_1 a391 \/ ssSkC0 \/ ssSkP0 $_117
% 0.20/0.59  |- ~c1_2 a391 $_186 \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.20/0.59     ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 a391 \/ c1_2 $U $V \/ c1_2 a391 $_187 \/
% 0.20/0.59     c1_2 a407 a408 \/ c2_0 \/ c2_1 a391 \/ c2_2 a391 $_186 \/
% 0.20/0.59     c2_2 a391 $_187 \/ c3_0 \/ c3_1 $U \/ c4_2 a391 $_186 \/ c5_0 \/
% 0.20/0.59     c5_1 $U \/ c5_1 a391 \/ ssSkC0
% 0.20/0.59  |- ~ssSkC2 \/ c1_1 a393 \/ c1_2 a393 $_187 \/ c1_2 a407 a408 \/ c2_0 \/
% 0.20/0.59     c2_1 a393 \/ c2_2 a393 $_187 \/ c2_2 a393 a394 \/ c3_0 \/ c5_0 \/
% 0.20/0.59     c5_1 a393 \/ ssSkC0
% 0.20/0.59  |- ~c5_2 a407 a408 \/ ~ndr1_0 \/ c1_1 $_189 \/ c1_2 $_189 $_191 \/ c2_0 \/
% 0.20/0.59     c2_1 $_189 \/ c2_2 $_189 $_190 \/ c2_2 $_189 $_191 \/ c3_0 \/
% 0.20/0.59     c3_2 $_189 $_190 \/ c5_0 \/ c5_1 $_189 \/ ssSkC0
% 0.20/0.59  |- ~c3_2 a407 a408 \/ ~ndr1_0 \/ c1_1 $_195 \/ c1_2 $_195 $_197 \/ c2_0 \/
% 0.20/0.59     c2_1 $_195 \/ c2_2 $_195 $_196 \/ c2_2 $_195 $_197 \/ c3_0 \/
% 0.20/0.59     c3_2 $_195 $_196 \/ c5_0 \/ c5_1 $_195 \/ ssSkC0
% 0.20/0.59  |- ~c3_1 a391 \/ ~ndr1_0 \/ ~ssSkC1 \/ c1_1 $_205 \/ c1_2 $_205 $_206 \/
% 0.20/0.59     c1_2 $_205 $_207 \/ c2_0 \/ c2_1 $_205 \/ c2_2 $_205 $_206 \/
% 0.20/0.59     c2_2 $_205 $_207 \/ c3_0 \/ c3_1 $_205 \/ c5_0 \/ c5_1 $_205 \/
% 0.20/0.59     ndr1_1 a407 \/ ssSkC0
% 0.20/0.59  |- ~c3_1 a391 \/ ~ndr1_0 \/ ~ssSkC1 \/ c1_1 $_211 \/ c1_2 $_211 $_212 \/
% 0.20/0.59     c1_2 $_211 $_213 \/ c1_2 a407 a409 \/ c2_0 \/ c2_1 $_211 \/
% 0.20/0.59     c2_2 $_211 $_212 \/ c2_2 $_211 $_213 \/ c3_0 \/ c3_1 $_211 \/ c5_0 \/
% 0.20/0.59     c5_1 $_211 \/ ssSkC0
% 0.20/0.59  |- ~c3_1 a391 \/ ~ndr1_0 \/ ~ssSkC1 \/ c1_1 $_217 \/ c1_2 $_217 $_218 \/
% 0.20/0.59     c1_2 $_217 $_219 \/ c2_0 \/ c2_1 $_217 \/ c2_2 $_217 $_218 \/
% 0.20/0.59     c2_2 $_217 $_219 \/ c2_2 a407 a409 \/ c3_0 \/ c3_1 $_217 \/ c5_0 \/
% 0.20/0.59     c5_1 $_217 \/ ssSkC0
% 0.20/0.59  |- ~c3_1 a391 \/ ~ndr1_0 \/ ~ssSkC1 \/ c1_1 $_223 \/ c1_2 $_223 $_224 \/
% 0.20/0.59     c1_2 $_223 $_225 \/ c1_2 a407 a408 \/ c2_0 \/ c2_1 $_223 \/
% 0.20/0.59     c2_2 $_223 $_224 \/ c2_2 $_223 $_225 \/ c3_0 \/ c3_1 $_223 \/ c5_0 \/
% 0.20/0.59     c5_1 $_223 \/ ssSkC0
% 0.20/0.59  |- ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 $_229 \/ c1_2 $_229 $_230 \/
% 0.20/0.59     c1_2 $_229 $_231 \/ c1_2 a391 a387 \/ c2_0 \/ c2_1 $_229 \/
% 0.20/0.59     c2_2 $_229 $_230 \/ c2_2 $_229 $_231 \/ c3_0 \/ c3_1 $_229 \/
% 0.20/0.59     c4_2 a391 a387 \/ c5_0 \/ c5_1 $_229 \/ ndr1_1 a407 \/ ssSkC0 \/
% 0.20/0.59     ssSkP0 a391
% 0.20/0.59  |- ~ndr1_0 \/ ~ssSkC1 \/ c1_1 $_232 \/ c1_2 $_232 $_233 \/
% 0.20/0.59     c1_2 $_232 $_234 \/ c1_2 a391 a387 \/ c2_0 \/ c2_1 $_232 \/ c2_1 a391 \/
% 0.20/0.59     c2_2 $_232 $_233 \/ c2_2 $_232 $_234 \/ c3_0 \/ c3_1 $_232 \/
% 0.20/0.59     c4_2 a391 a387 \/ c5_0 \/ c5_1 $_232 \/ ndr1_1 a407 \/ ssSkC0 \/
% 0.20/0.59     ssSkP0 a391
% 0.20/0.59  |- ~c1_2 a391 a387 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 $_238 \/
% 0.20/0.59     c1_2 $_238 $_239 \/ c1_2 $_238 $_240 \/ c2_0 \/ c2_1 $_238 \/
% 0.20/0.59     c2_2 $_238 $_239 \/ c2_2 $_238 $_240 \/ c3_0 \/ c3_1 $_238 \/
% 0.20/0.59     c4_2 a391 a387 \/ c5_0 \/ c5_1 $_238 \/ ndr1_1 a407 \/ ssSkC0 \/
% 0.20/0.59     ssSkP0 a391
% 0.20/0.59  |- ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 $_244 \/ c1_2 $_244 $_245 \/
% 0.20/0.59     c1_2 $_244 $_246 \/ c1_2 a391 a387 \/ c1_2 a407 a409 \/ c2_0 \/
% 0.20/0.59     c2_1 $_244 \/ c2_2 $_244 $_245 \/ c2_2 $_244 $_246 \/ c3_0 \/
% 0.20/0.59     c3_1 $_244 \/ c4_2 a391 a387 \/ c5_0 \/ c5_1 $_244 \/ ssSkC0 \/
% 0.20/0.59     ssSkP0 a391
% 0.20/0.59  |- ~ndr1_0 \/ ~ssSkC1 \/ c1_1 $_247 \/ c1_2 $_247 $_248 \/
% 0.20/0.59     c1_2 $_247 $_249 \/ c1_2 a391 a387 \/ c1_2 a407 a409 \/ c2_0 \/
% 0.20/0.59     c2_1 $_247 \/ c2_1 a391 \/ c2_2 $_247 $_248 \/ c2_2 $_247 $_249 \/
% 0.20/0.59     c3_0 \/ c3_1 $_247 \/ c4_2 a391 a387 \/ c5_0 \/ c5_1 $_247 \/ ssSkC0 \/
% 0.20/0.59     ssSkP0 a391
% 0.20/0.59  |- ~c1_2 a391 a387 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 $_253 \/
% 0.20/0.59     c1_2 $_253 $_254 \/ c1_2 $_253 $_255 \/ c1_2 a407 a409 \/ c2_0 \/
% 0.20/0.59     c2_1 $_253 \/ c2_2 $_253 $_254 \/ c2_2 $_253 $_255 \/ c3_0 \/
% 0.20/0.59     c3_1 $_253 \/ c4_2 a391 a387 \/ c5_0 \/ c5_1 $_253 \/ ssSkC0 \/
% 0.20/0.59     ssSkP0 a391
% 0.20/0.59  |- ~c1_2 a391 a387 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 $_259 \/
% 0.20/0.59     c1_2 $_259 $_260 \/ c1_2 $_259 $_261 \/ c2_0 \/ c2_1 $_259 \/
% 0.20/0.59     c2_2 $_259 $_260 \/ c2_2 $_259 $_261 \/ c2_2 a407 a409 \/ c3_0 \/
% 0.20/0.59     c3_1 $_259 \/ c4_2 a391 a387 \/ c5_0 \/ c5_1 $_259 \/ ssSkC0 \/
% 0.20/0.59     ssSkP0 a391
% 0.20/0.59  |- ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 $_265 \/ c1_2 $_265 $_266 \/
% 0.20/0.59     c1_2 $_265 $_267 \/ c1_2 a391 a387 \/ c2_0 \/ c2_1 $_265 \/
% 0.20/0.59     c2_2 $_265 $_266 \/ c2_2 $_265 $_267 \/ c2_2 a407 a409 \/ c3_0 \/
% 0.20/0.59     c3_1 $_265 \/ c4_2 a391 a387 \/ c5_0 \/ c5_1 $_265 \/ ssSkC0 \/
% 0.20/0.59     ssSkP0 a391
% 0.20/0.59  |- ~ndr1_0 \/ ~ssSkC1 \/ c1_1 $_268 \/ c1_2 $_268 $_269 \/
% 0.20/0.59     c1_2 $_268 $_270 \/ c1_2 a391 a387 \/ c2_0 \/ c2_1 $_268 \/ c2_1 a391 \/
% 0.20/0.59     c2_2 $_268 $_269 \/ c2_2 $_268 $_270 \/ c2_2 a407 a409 \/ c3_0 \/
% 0.20/0.59     c3_1 $_268 \/ c4_2 a391 a387 \/ c5_0 \/ c5_1 $_268 \/ ssSkC0 \/
% 0.20/0.59     ssSkP0 a391
% 0.20/0.59  |- ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 $_274 \/ c1_2 $_274 $_275 \/
% 0.20/0.59     c1_2 $_274 $_276 \/ c1_2 a391 a387 \/ c1_2 a407 a408 \/ c2_0 \/
% 0.20/0.59     c2_1 $_274 \/ c2_2 $_274 $_275 \/ c2_2 $_274 $_276 \/ c3_0 \/
% 0.20/0.59     c3_1 $_274 \/ c4_2 a391 a387 \/ c5_0 \/ c5_1 $_274 \/ ssSkC0 \/
% 0.20/0.59     ssSkP0 a391
% 0.20/0.59  |- ~ndr1_0 \/ ~ssSkC1 \/ c1_1 $_277 \/ c1_2 $_277 $_278 \/
% 0.20/0.59     c1_2 $_277 $_279 \/ c1_2 a391 a387 \/ c1_2 a407 a408 \/ c2_0 \/
% 0.20/0.59     c2_1 $_277 \/ c2_1 a391 \/ c2_2 $_277 $_278 \/ c2_2 $_277 $_279 \/
% 0.20/0.59     c3_0 \/ c3_1 $_277 \/ c4_2 a391 a387 \/ c5_0 \/ c5_1 $_277 \/ ssSkC0 \/
% 0.20/0.59     ssSkP0 a391
% 0.20/0.59  |- ~c1_2 a391 a387 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 $_283 \/
% 0.20/0.59     c1_2 $_283 $_284 \/ c1_2 $_283 $_285 \/ c1_2 a407 a408 \/ c2_0 \/
% 0.20/0.59     c2_1 $_283 \/ c2_2 $_283 $_284 \/ c2_2 $_283 $_285 \/ c3_0 \/
% 0.20/0.59     c3_1 $_283 \/ c4_2 a391 a387 \/ c5_0 \/ c5_1 $_283 \/ ssSkC0 \/
% 0.20/0.59     ssSkP0 a391
% 0.20/0.59  |- ~c1_2 a391 $_313 \/ ~c3_2 a391 $_313 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/
% 0.20/0.59     ~ssSkC1 \/ c1_1 $_314 \/ c1_2 $_314 $_315 \/ c1_2 $_314 $_316 \/ c2_0 \/
% 0.20/0.59     c2_1 $_314 \/ c2_2 $_314 $_315 \/ c2_2 $_314 $_316 \/ c3_0 \/
% 0.20/0.59     c3_1 $_314 \/ c4_2 a391 $_313 \/ c5_0 \/ c5_1 $_314 \/ ndr1_1 a407 \/
% 0.20/0.59     ssSkC0
% 0.20/0.59  |- ~c5_2 a391 $_321 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 $_322 \/
% 0.20/0.59     c1_2 $_322 $_323 \/ c1_2 $_322 $_324 \/ c1_2 a391 $_321 \/ c2_0 \/
% 0.20/0.59     c2_1 $_322 \/ c2_2 $_322 $_323 \/ c2_2 $_322 $_324 \/ c3_0 \/
% 0.20/0.59     c3_1 $_322 \/ c4_2 a391 $_321 \/ c5_0 \/ c5_1 $_322 \/ ndr1_1 a407 \/
% 0.20/0.59     ssSkC0
% 0.20/0.59  |- ~c5_2 a391 $_329 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 $_330 \/
% 0.20/0.59     c1_2 $_330 $_331 \/ c1_2 $_330 $_332 \/ c1_2 a391 $_329 \/
% 0.20/0.59     c1_2 a407 a409 \/ c2_0 \/ c2_1 $_330 \/ c2_2 $_330 $_331 \/
% 0.20/0.59     c2_2 $_330 $_332 \/ c3_0 \/ c3_1 $_330 \/ c4_2 a391 $_329 \/ c5_0 \/
% 0.20/0.59     c5_1 $_330 \/ ssSkC0
% 0.20/0.59  |- ~c1_2 a391 $_337 \/ ~c3_2 a391 $_337 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/
% 0.20/0.59     ~ssSkC1 \/ c1_1 $_338 \/ c1_2 $_338 $_339 \/ c1_2 $_338 $_340 \/
% 0.20/0.59     c1_2 a407 a409 \/ c2_0 \/ c2_1 $_338 \/ c2_2 $_338 $_339 \/
% 0.20/0.59     c2_2 $_338 $_340 \/ c3_0 \/ c3_1 $_338 \/ c4_2 a391 $_337 \/ c5_0 \/
% 0.20/0.59     c5_1 $_338 \/ ssSkC0
% 0.20/0.59  |- ~c1_2 a391 $_345 \/ ~c3_2 a391 $_345 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/
% 0.20/0.59     ~ssSkC1 \/ c1_1 $_346 \/ c1_2 $_346 $_347 \/ c1_2 $_346 $_348 \/ c2_0 \/
% 0.20/0.59     c2_1 $_346 \/ c2_2 $_346 $_347 \/ c2_2 $_346 $_348 \/ c2_2 a407 a409 \/
% 0.20/0.59     c3_0 \/ c3_1 $_346 \/ c4_2 a391 $_345 \/ c5_0 \/ c5_1 $_346 \/ ssSkC0
% 0.20/0.59  |- ~c5_2 a391 $_353 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 $_354 \/
% 0.20/0.59     c1_2 $_354 $_355 \/ c1_2 $_354 $_356 \/ c1_2 a391 $_353 \/ c2_0 \/
% 0.20/0.59     c2_1 $_354 \/ c2_2 $_354 $_355 \/ c2_2 $_354 $_356 \/ c2_2 a407 a409 \/
% 0.20/0.59     c3_0 \/ c3_1 $_354 \/ c4_2 a391 $_353 \/ c5_0 \/ c5_1 $_354 \/ ssSkC0
% 0.20/0.59  |- ~c5_2 a391 $_361 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 $_362 \/
% 0.20/0.59     c1_2 $_362 $_363 \/ c1_2 $_362 $_364 \/ c1_2 a391 $_361 \/
% 0.20/0.59     c1_2 a407 a408 \/ c2_0 \/ c2_1 $_362 \/ c2_2 $_362 $_363 \/
% 0.20/0.59     c2_2 $_362 $_364 \/ c3_0 \/ c3_1 $_362 \/ c4_2 a391 $_361 \/ c5_0 \/
% 0.20/0.59     c5_1 $_362 \/ ssSkC0
% 0.20/0.59  |- ~c1_2 a391 $_369 \/ ~c3_2 a391 $_369 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/
% 0.20/0.59     ~ssSkC1 \/ c1_1 $_370 \/ c1_2 $_370 $_371 \/ c1_2 $_370 $_372 \/
% 0.20/0.59     c1_2 a407 a408 \/ c2_0 \/ c2_1 $_370 \/ c2_2 $_370 $_371 \/
% 0.20/0.59     c2_2 $_370 $_372 \/ c3_0 \/ c3_1 $_370 \/ c4_2 a391 $_369 \/ c5_0 \/
% 0.20/0.59     c5_1 $_370 \/ ssSkC0
% 0.20/0.59  |- ~c1_2 a391 $_396 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 $_394 \/
% 0.20/0.59     c1_1 a391 \/ c1_2 $_394 $_393 \/ c1_2 $_394 $_395 \/ c1_2 a391 $_397 \/
% 0.20/0.59     c2_0 \/ c2_1 $_394 \/ c2_1 a391 \/ c2_2 $_394 $_393 \/
% 0.20/0.59     c2_2 $_394 $_395 \/ c2_2 a391 $_396 \/ c2_2 a391 $_397 \/ c3_0 \/
% 0.20/0.59     c3_1 $_394 \/ c4_2 a391 $_396 \/ c5_0 \/ c5_1 $_394 \/ c5_1 a391 \/
% 0.20/0.59     ndr1_1 a407 \/ ssSkC0
% 0.20/0.59  |- ~c1_2 a391 $_406 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 $_404 \/
% 0.20/0.59     c1_1 a391 \/ c1_2 $_404 $_403 \/ c1_2 $_404 $_405 \/ c1_2 a391 $_407 \/
% 0.20/0.59     c1_2 a407 a408 \/ c2_0 \/ c2_1 $_404 \/ c2_1 a391 \/ c2_2 $_404 $_403 \/
% 0.20/0.59     c2_2 $_404 $_405 \/ c2_2 a391 $_406 \/ c2_2 a391 $_407 \/ c3_0 \/
% 0.20/0.59     c3_1 $_404 \/ c4_2 a391 $_406 \/ c5_0 \/ c5_1 $_404 \/ c5_1 a391 \/
% 0.20/0.59     ssSkC0
% 0.20/0.59  |- ~c1_2 a391 $_416 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 $_414 \/
% 0.20/0.59     c1_1 a391 \/ c1_2 $_414 $_413 \/ c1_2 $_414 $_415 \/ c1_2 a391 $_417 \/
% 0.20/0.59     c1_2 a407 a409 \/ c2_0 \/ c2_1 $_414 \/ c2_1 a391 \/ c2_2 $_414 $_413 \/
% 0.20/0.59     c2_2 $_414 $_415 \/ c2_2 a391 $_416 \/ c2_2 a391 $_417 \/ c3_0 \/
% 0.20/0.59     c3_1 $_414 \/ c4_2 a391 $_416 \/ c5_0 \/ c5_1 $_414 \/ c5_1 a391 \/
% 0.20/0.59     ssSkC0
% 0.20/0.59  |- ~c1_2 a391 $_426 \/ ~ndr1_0 \/ ~ndr1_1 a391 \/ ~ssSkC1 \/ c1_1 $_424 \/
% 0.20/0.59     c1_1 a391 \/ c1_2 $_424 $_423 \/ c1_2 $_424 $_425 \/ c1_2 a391 $_427 \/
% 0.20/0.59     c2_0 \/ c2_1 $_424 \/ c2_1 a391 \/ c2_2 $_424 $_423 \/
% 0.20/0.59     c2_2 $_424 $_425 \/ c2_2 a391 $_426 \/ c2_2 a391 $_427 \/
% 0.20/0.59     c2_2 a407 a409 \/ c3_0 \/ c3_1 $_424 \/ c4_2 a391 $_426 \/ c5_0 \/
% 0.20/0.59     c5_1 $_424 \/ c5_1 a391 \/ ssSkC0
% 0.20/0.59  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.59  
%------------------------------------------------------------------------------