↑ Up

Metis---2.4.SAT-Sat.s

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

% Computer : n021.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:50 EDT 2022

% Result   : Satisfiable 0.19s 0.44s
% Output   : Saturation 0.19s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12  % Problem  : SYN540-1 : TPTP v8.1.0. Released v2.1.0.
% 0.11/0.13  % Command  : metis --show proof --show saturation %s
% 0.13/0.33  % Computer : n021.cluster.edu
% 0.13/0.33  % Model    : x86_64 x86_64
% 0.13/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33  % Memory   : 8042.1875MB
% 0.13/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33  % CPULimit : 300
% 0.13/0.33  % WCLimit  : 600
% 0.13/0.33  % DateTime : Mon Jul 11 13:25:08 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.13/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.19/0.44  % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.44  
% 0.19/0.44  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.44  |- c1_0 \/ ndr1_0
% 0.19/0.44  |- c5_0 \/ ndr1_0
% 0.19/0.44  |- c4_0 \/ ndr1_0
% 0.19/0.44  |- ndr1_0 \/ ssSkC6
% 0.19/0.44  |- ndr1_0 \/ ssSkC5
% 0.19/0.44  |- ndr1_0 \/ ssSkC4
% 0.19/0.44  |- ndr1_0 \/ ssSkC3
% 0.19/0.44  |- ndr1_0 \/ ssSkC2
% 0.19/0.44  |- ndr1_0 \/ ssSkC1
% 0.19/0.44  |- c5_0 \/ ndr1_1 a698
% 0.19/0.44  |- c3_1 a698 \/ c5_0
% 0.19/0.44  |- ~c4_0 \/ ndr1_0
% 0.19/0.44  |- ~c1_0 \/ c2_0
% 0.19/0.44  |- ~c4_0 \/ c2_0
% 0.19/0.44  |- c3_1 a722 \/ ssSkC6
% 0.19/0.44  |- ndr1_1 a717 \/ ssSkC5
% 0.19/0.44  |- c4_1 a717 \/ ssSkC5
% 0.19/0.44  |- c1_1 a710 \/ ssSkC4
% 0.19/0.44  |- ndr1_1 a706 \/ ssSkC3
% 0.19/0.44  |- ndr1_1 a687 \/ ssSkC1
% 0.19/0.44  |- ndr1_1 $U \/ ssSkP0 $U
% 0.19/0.44  |- ~ssSkC6 \/ c1_0 \/ ndr1_1 a723
% 0.19/0.44  |- ~c4_0 \/ c5_1 a697
% 0.19/0.44  |- ~c3_1 a694 \/ c4_0
% 0.19/0.44  |- ~c1_1 a694 \/ c4_0
% 0.19/0.44  |- ~ssSkC2 \/ c2_1 a693 \/ c3_0
% 0.19/0.44  |- ~ssSkC0 \/ c3_0 \/ ndr1_1 a685
% 0.19/0.44  |- ~c5_0 \/ c2_0 \/ c3_0
% 0.19/0.44  |- ~c1_0 \/ ~c2_0
% 0.19/0.44  |- c5_2 a717 a718 \/ ssSkC5
% 0.19/0.44  |- c1_2 a717 a718 \/ ssSkC5
% 0.19/0.44  |- ~c4_1 a706 \/ ssSkC3
% 0.19/0.44  |- ~c1_1 a692 \/ ssSkC2
% 0.19/0.44  |- ~c4_1 a692 \/ ssSkC2
% 0.19/0.44  |- c4_2 a687 a688 \/ ssSkC1
% 0.19/0.44  |- c2_2 a687 a688 \/ ssSkC1
% 0.19/0.44  |- ~c1_1 a687 \/ ssSkC1
% 0.19/0.44  |- c4_2 $U a683 \/ ssSkP0 $U
% 0.19/0.44  |- c1_2 $U a683 \/ ssSkP0 $U
% 0.19/0.44  |- ~ssSkC6 \/ c1_0 \/ c4_2 a723 a724
% 0.19/0.44  |- ~ssSkC6 \/ c1_0 \/ c2_2 a723 a724
% 0.19/0.44  |- ~c3_0 \/ ~ssSkC5 \/ ndr1_1 a719
% 0.19/0.44  |- ~c3_0 \/ c1_0 \/ ndr1_1 a713
% 0.19/0.44  |- ~c1_0 \/ c4_0 \/ ndr1_1 a700
% 0.19/0.45  |- ~c4_2 a698 a699 \/ c5_0
% 0.19/0.45  |- ~c1_2 a698 a699 \/ c5_0
% 0.19/0.45  |- ~c2_1 a697 \/ ~c4_0
% 0.19/0.45  |- ~c4_0 \/ ~c4_1 a697
% 0.19/0.45  |- ~c5_1 a693 \/ ~ssSkC2 \/ c3_0
% 0.19/0.45  |- ~c1_1 a685 \/ ~ssSkC0 \/ c3_0
% 0.19/0.45  |- ~c2_0 \/ ~c4_0 \/ c1_0
% 0.19/0.45  |- ~c1_0 \/ ~c5_0 \/ c4_0
% 0.19/0.45  |- ~c1_2 a706 a707 \/ ssSkC3
% 0.19/0.45  |- ~c5_2 a706 a707 \/ ssSkC3
% 0.19/0.45  |- ~c5_2 a687 a688 \/ ssSkC1
% 0.19/0.45  |- ~c5_2 a723 a724 \/ ~ssSkC6 \/ c1_0
% 0.19/0.45  |- ~c3_0 \/ ~ssSkC5 \/ c4_2 a719 a721
% 0.19/0.45  |- ~c3_0 \/ ~ssSkC5 \/ c1_2 a719 a721
% 0.19/0.45  |- ~c3_0 \/ ~ssSkC5 \/ c4_2 a719 a720
% 0.19/0.45  |- ~c3_0 \/ ~ssSkC5 \/ c2_2 a719 a720
% 0.19/0.45  |- ~c2_1 a719 \/ ~c3_0 \/ ~ssSkC5
% 0.19/0.45  |- ~c3_0 \/ ~c3_1 a713 \/ c1_0
% 0.19/0.45  |- ~c1_0 \/ ~c5_1 a700 \/ c4_0
% 0.19/0.45  |- ~c1_0 \/ ~c3_1 a700 \/ c4_0
% 0.19/0.45  |- ~c4_2 a689 a691 \/ ~ssSkC1 \/ c4_0
% 0.19/0.45  |- ~c1_2 a689 a690 \/ ~ssSkC1 \/ c4_0
% 0.19/0.45  |- ~c3_2 a685 a686 \/ ~ssSkC0 \/ c3_0
% 0.19/0.45  |- ~c5_2 a685 a686 \/ ~ssSkC0 \/ c3_0
% 0.19/0.45  |- ~c4_2 a685 a686 \/ ~ssSkC0 \/ c3_0
% 0.19/0.45  |- ~c3_0 \/ ~c5_2 a719 a721 \/ ~ssSkC5
% 0.19/0.45  |- ~c1_2 a713 a714 \/ ~c3_0 \/ c1_0
% 0.19/0.45  |- ~c2_2 a713 a714 \/ ~c3_0 \/ c1_0
% 0.19/0.45  |- ~c3_0 \/ ~c3_2 a713 a714 \/ c1_0
% 0.19/0.45  |- ~c1_0 \/ ~c1_2 a700 a701 \/ c4_0
% 0.19/0.45  |- ~c1_0 \/ ~c4_2 a700 a701 \/ c4_0
% 0.19/0.45  |- ~c1_0 \/ ~c2_2 a700 a701 \/ c4_0
% 0.19/0.45  |- ~ndr1_0 \/ ~ssSkP0 $U \/ c1_2 $U a684 \/ ssSkC0
% 0.19/0.45  |- ~c2_1 $U \/ ~ndr1_0 \/ c4_0 \/ c5_0 \/ ndr1_1 $U
% 0.19/0.45  |- ~c3_0 \/ ~ndr1_1 a713 \/ c1_0 \/ c2_2 a713 $U
% 0.19/0.45  |- ~c2_2 $U a684 \/ ~ndr1_0 \/ ~ssSkP0 $U \/ ssSkC0
% 0.19/0.45  |- ~c2_1 $U \/ ~ndr1_0 \/ c2_2 $U a709 \/ c4_0 \/ c5_0
% 0.19/0.45  |- ~c2_1 $U \/ ~ndr1_0 \/ c4_0 \/ c4_2 $U a709 \/ c5_0
% 0.19/0.45  |- ~c5_1 $U \/ ~ndr1_0 \/ c1_1 $U \/ c2_0 \/ c2_1 $U \/ c5_0
% 0.19/0.45  |- ~c1_2 $U a709 \/ ~c2_1 $U \/ ~ndr1_0 \/ c4_0 \/ c5_0
% 0.19/0.45  |- ~c1_2 $U a703 \/ ~c5_0 \/ ~ndr1_0 \/ c3_0 \/ c5_1 $U
% 0.19/0.45  |- ~c3_2 $U a703 \/ ~c5_0 \/ ~ndr1_0 \/ c3_0 \/ c5_1 $U
% 0.19/0.45  |- ~c1_2 a702 $U \/ ~ndr1_1 a702 \/ c1_0 \/ c4_2 a702 $U
% 0.19/0.45  |- ~c5_2 a702 $U \/ ~ndr1_1 a702 \/ c1_0 \/ c1_2 a702 $U
% 0.19/0.45  |- ~c3_0 \/ ~c4_1 $U \/ ~ndr1_0 \/ ~ssSkC3 \/ c5_1 $U \/ ndr1_1 $U
% 0.19/0.45  |- ~c3_0 \/ ~c3_1 $U \/ ~c5_1 $U \/ ~ndr1_0 \/ c4_1 $U
% 0.19/0.45  |- ~c1_2 a693 $U \/ ~ndr1_1 a693 \/ ~ssSkC2 \/ c2_2 a693 $U \/ c3_0
% 0.19/0.45  |- ~c2_2 a685 $U \/ ~ndr1_1 a685 \/ ~ssSkC0 \/ c1_2 a685 $U \/ c3_0
% 0.19/0.45  |- ~c3_0 \/ ~c4_1 $U \/ ~ndr1_0 \/ ~ssSkC3 \/ c2_2 $U a708 \/ c5_1 $U
% 0.19/0.45  |- ~c3_0 \/ ~c4_1 $U \/ ~ndr1_0 \/ ~ssSkC3 \/ c1_2 $U a708 \/ c5_1 $U
% 0.19/0.45  |- ~ndr1_1 a694 \/ c2_2 a694 $U \/ c3_2 a694 $U \/ c4_0 \/ c4_2 a694 $U
% 0.19/0.45  |- ~c2_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_1 $U \/ c1_2 $U $V \/ c4_0
% 0.19/0.45  |- ~c3_0 \/ ~c4_1 $U \/ ~c5_2 $U a708 \/ ~ndr1_0 \/ ~ssSkC3 \/ c5_1 $U
% 0.19/0.45  |- ~c3_2 a692 $U \/ ~ndr1_1 a692 \/ c2_2 a692 $U \/ c4_2 a692 $U \/ ssSkC2
% 0.19/0.45  |- ~c2_2 a722 $U \/ ~c3_2 a722 $U \/ ~ndr1_1 a722 \/ c1_2 a722 $U \/ ssSkC6
% 0.19/0.45  |- ~c3_2 a710 $U \/ ~c5_2 a710 $U \/ ~ndr1_1 a710 \/ c4_2 a710 $U \/ ssSkC4
% 0.19/0.45  |- ~c3_2 a706 $U \/ ~c5_2 a706 $U \/ ~ndr1_1 a706 \/ c2_2 a706 $U \/ ssSkC3
% 0.19/0.45  |- ~c4_2 a689 $U \/ ~c5_2 a689 $U \/ ~ndr1_1 a689 \/ ~ssSkC1 \/
% 0.19/0.45     c3_2 a689 $U \/ c4_0
% 0.19/0.45  |- ~c1_0 \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $V \/
% 0.19/0.45     c2_1 a696 \/ c4_1 $U
% 0.19/0.45  |- ~c1_0 \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $V \/
% 0.19/0.45     c4_1 $U \/ c5_1 a696
% 0.19/0.45  |- ~c1_2 a722 $U \/ ~c4_2 a722 $U \/ ~c5_2 a722 $U \/ ~ndr1_1 a722 \/
% 0.19/0.45     ssSkC6
% 0.19/0.45  |- ~c1_2 a687 $U \/ ~c2_2 a687 $U \/ ~c4_2 a687 $U \/ ~ndr1_1 a687 \/
% 0.19/0.45     ssSkC1
% 0.19/0.45  |- ~c2_2 a723 $U \/ ~c4_2 a723 $U \/ ~c5_2 a723 $U \/ ~ndr1_1 a723 \/
% 0.19/0.45     ~ssSkC6 \/ c1_0
% 0.19/0.45  |- ~c4_1 $U \/ ~ndr1_0 \/ ~ndr1_1 $U \/ ~ssSkC4 \/ c1_2 $U $V \/
% 0.19/0.45     c2_2 $U $V \/ c3_0 \/ c4_2 $U a711
% 0.19/0.45  |- ~c2_0 \/ ~c2_2 $U $V \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.19/0.45     c3_1 $U \/ ndr1_1 a704
% 0.19/0.45  |- ~c2_2 $U a711 \/ ~c4_1 $U \/ ~ndr1_0 \/ ~ndr1_1 $U \/ ~ssSkC4 \/
% 0.19/0.45     c1_2 $U $V \/ c2_2 $U $V \/ c3_0
% 0.19/0.45  |- ~c2_0 \/ ~c2_2 $U $V \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.19/0.45     c3_1 $U \/ c3_2 a704 a705
% 0.19/0.45  |- ~c2_0 \/ ~c2_2 $U $V \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.19/0.45     c3_1 $U \/ c4_2 a704 a705
% 0.19/0.45  |- ~c2_0 \/ ~c2_2 $U $V \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.19/0.45     c1_2 a704 a705 \/ c3_1 $U
% 0.19/0.45  |- ~c2_0 \/ ~c2_2 $U $V \/ ~c3_2 $U $V \/ ~c4_1 a704 \/ ~ndr1_0 \/
% 0.19/0.45     ~ndr1_1 $U \/ c3_1 $U
% 0.19/0.45  |- ~c2_0 \/ ~c2_2 $U $V \/ ~c3_2 $U $V \/ ~c5_1 a704 \/ ~ndr1_0 \/
% 0.19/0.45     ~ndr1_1 $U \/ c3_1 $U
% 0.19/0.45  |- ~c4_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_0 \/ c1_2 $U $V \/ c2_1 $U \/
% 0.19/0.45     c2_2 $U $V \/ c4_0 \/ c5_2 $U a681
% 0.19/0.45  |- ~c4_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_0 \/ c1_2 $U $V \/ c2_1 $U \/
% 0.19/0.45     c2_2 $U $V \/ c4_0 \/ c4_2 $U a681
% 0.19/0.45  |- ~c1_2 $U a681 \/ ~c4_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_0 \/
% 0.19/0.45     c1_2 $U $V \/ c2_1 $U \/ c2_2 $U $V \/ c4_0
% 0.19/0.45  |- ~c1_1 $U \/ ~c1_2 $U $V \/ ~c3_0 \/ ~c4_2 $U $V \/ ~ndr1_0 \/
% 0.19/0.45     ~ndr1_1 $U \/ c4_1 $U \/ c5_2 $U $V
% 0.19/0.45  |- ~c2_2 $U $V \/ ~c3_0 \/ ~c3_2 $U $W \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.19/0.45     c2_1 $U \/ c2_2 $U $W \/ c3_2 $U $V \/ ndr1_1 a715
% 0.19/0.45  |- ~c2_2 $U $V \/ ~c3_0 \/ ~c3_1 a715 \/ ~c3_2 $U $W \/ ~ndr1_0 \/
% 0.19/0.45     ~ndr1_1 $U \/ c2_1 $U \/ c2_2 $U $W \/ c3_2 $U $V
% 0.19/0.45  |- ~c1_2 $U $V \/ ~c3_2 $U $V \/ ~c4_0 \/ ~c4_1 $U \/ ~c5_0 \/ ~ndr1_0 \/
% 0.19/0.45     ~ndr1_1 $U \/ c3_2 $U a712 \/ c4_2 $U $V
% 0.19/0.45  |- ~c1_2 $U $V \/ ~c3_2 $U $V \/ ~c4_0 \/ ~c4_1 $U \/ ~c5_0 \/ ~ndr1_0 \/
% 0.19/0.45     ~ndr1_1 $U \/ c1_2 $U a712 \/ c4_2 $U $V
% 0.19/0.45  |- ~c2_2 $U $V \/ ~c3_0 \/ ~c3_2 $U $W \/ ~c5_2 a715 a716 \/ ~ndr1_0 \/
% 0.19/0.45     ~ndr1_1 $U \/ c2_1 $U \/ c2_2 $U $W \/ c3_2 $U $V
% 0.19/0.45  |- ~c2_2 $U $V \/ ~c3_0 \/ ~c3_2 $U $W \/ ~c4_2 a715 a716 \/ ~ndr1_0 \/
% 0.19/0.45     ~ndr1_1 $U \/ c2_1 $U \/ c2_2 $U $W \/ c3_2 $U $V
% 0.19/0.45  |- ~c2_2 $U $V \/ ~c2_2 a715 a716 \/ ~c3_0 \/ ~c3_2 $U $W \/ ~ndr1_0 \/
% 0.19/0.45     ~ndr1_1 $U \/ c2_1 $U \/ c2_2 $U $W \/ c3_2 $U $V
% 0.19/0.45  |- ~c1_2 $U $W \/ ~c2_2 $U $V \/ ~c2_2 $U $W \/ ~c4_2 $U $V \/ ~ndr1_0 \/
% 0.19/0.45     ~ndr1_1 $U \/ c2_0 \/ c3_2 $U $V \/ c3_2 $U a695
% 0.19/0.45  |- ~c1_2 $U $W \/ ~c2_2 $U $V \/ ~c2_2 $U $W \/ ~c4_2 $U $V \/ ~ndr1_0 \/
% 0.19/0.45     ~ndr1_1 $U \/ c2_0 \/ c2_2 $U a695 \/ c3_2 $U $V
% 0.19/0.45  |- ~c1_2 $U $V \/ ~c3_2 $U $V \/ ~c4_0 \/ ~c4_1 $U \/ ~c5_0 \/
% 0.19/0.45     ~c5_2 $U a712 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c4_2 $U $V
% 0.19/0.45  |- ~c2_2 $V $W \/ ~c2_2 $V $X \/ ~c4_1 $U \/ ~c4_2 $V $W \/ ~ndr1_0 \/
% 0.19/0.45     ~ndr1_1 $V \/ c1_2 $V a682 \/ c3_2 $V $W \/ c4_0 \/ c5_1 $U \/
% 0.19/0.45     c5_2 $V $X
% 0.19/0.45  |- ~c2_2 $V $W \/ ~c2_2 $V $X \/ ~c4_1 $U \/ ~c4_2 $V $W \/
% 0.19/0.45     ~c4_2 $V a682 \/ ~ndr1_0 \/ ~ndr1_1 $V \/ c3_2 $V $W \/ c4_0 \/
% 0.19/0.45     c5_1 $U \/ c5_2 $V $X
% 0.19/0.45  |- ~c2_2 $V $X \/ ~c2_2 $V a682 \/ ~c4_1 $U \/ ~c4_2 $V a682 \/ ~ndr1_0 \/
% 0.19/0.45     ~ndr1_1 $V \/ c3_2 $V a682 \/ c4_0 \/ c5_1 $U \/ c5_2 $V $X
% 0.19/0.45  |- c3_0 \/ ndr1_0
% 0.19/0.45  |- ~c3_0 \/ ndr1_0
% 0.19/0.45  |- ~ndr1_0 \/ ndr1_1 $_3 \/ ssSkC0
% 0.19/0.45  |- c3_0 \/ ndr1_1 $_4 \/ ssSkC0
% 0.19/0.45  |- c4_0 \/ ndr1_1 $_4 \/ ssSkC0
% 0.19/0.45  |- c5_0 \/ ndr1_1 $_4 \/ ssSkC0
% 0.19/0.45  |- c1_0 \/ ndr1_1 $_4 \/ ssSkC0
% 0.19/0.45  |- ~c3_0 \/ c1_0 \/ c2_2 a713 $_10 \/ ssSkC0
% 0.19/0.45  |- ~c5_0 \/ c3_0 \/ c5_1 $_15 \/ ndr1_1 $_15
% 0.19/0.45  |- ~ndr1_1 a693 \/ ~ssSkC2 \/ c2_2 a693 a683 \/ c3_0 \/ ssSkP0 a693
% 0.19/0.45  |- ~ssSkC2 \/ c2_2 a693 a683 \/ c3_0 \/ ssSkC0 \/ ssSkP0 a693
% 0.19/0.45  |- ~c3_0 \/ ~ndr1_0 \/ ~ssSkC3 \/ c2_2 a717 a708 \/ c5_1 a717 \/ ssSkC5
% 0.19/0.45  |- ~c3_0 \/ ~ndr1_0 \/ ~ssSkC3 \/ c1_2 a717 a708 \/ c5_1 a717 \/ ssSkC5
% 0.19/0.45  |- c1_2 a698 $_30 \/ c4_2 a698 $_30 \/ c5_0 \/ c5_2 a698 $_30
% 0.19/0.46  |- c2_2 a694 $_32 \/ c3_2 a694 $_32 \/ c4_0 \/ c4_2 a694 $_32 \/ ssSkC0
% 0.19/0.46  |- ~c1_2 a687 a683 \/ ~c2_2 a687 a683 \/ ~ndr1_1 a687 \/ ssSkC1 \/
% 0.19/0.46     ssSkP0 a687
% 0.19/0.46  |- ~c1_2 a687 a688 \/ ~ndr1_1 a687 \/ ssSkC1
% 0.19/0.46  |- c4_0 \/ ssSkC1
% 0.19/0.46  |- c3_2 a689 a690 \/ c4_0
% 0.19/0.46  |- c2_2 a689 a690 \/ c4_0
% 0.19/0.46  |- c1_2 a689 a691 \/ c4_0
% 0.19/0.46  |- c4_0 \/ c5_2 a689 a691
% 0.19/0.46  |- c4_0 \/ ndr1_1 a689
% 0.19/0.46  |- c1_1 a689 \/ c4_0
% 0.19/0.46  |- ~c1_0 \/ c1_2 a689 a690 \/ c2_1 a696 \/ c4_0 \/ c4_1 a689
% 0.19/0.46  |- ~c1_0 \/ c1_2 a689 a690 \/ c4_0 \/ c4_1 a689 \/ c5_1 a696
% 0.19/0.46  |- ~c2_0 \/ c3_1 a689 \/ c4_0 \/ ndr1_1 a704
% 0.19/0.46  |- ~c2_0 \/ ~c4_1 a704 \/ ~ndr1_0 \/ c3_1 a689 \/ c4_0
% 0.19/0.46  |- ~c2_0 \/ ~c5_1 a704 \/ ~ndr1_0 \/ c3_1 a689 \/ c4_0
% 0.19/0.46  |- ~c2_0 \/ c3_1 a689 \/ c3_2 a704 a705 \/ c4_0
% 0.19/0.46  |- ~c2_0 \/ c3_1 a689 \/ c4_0 \/ c4_2 a704 a705
% 0.19/0.46  |- ~c2_0 \/ c1_2 a704 a705 \/ c3_1 a689 \/ c4_0
% 0.19/0.46  |- ~c4_1 a687 \/ ~ndr1_0 \/ ~ssSkC4 \/ c1_2 a687 $_62 \/ c2_2 a687 $_62 \/
% 0.19/0.46     c3_0 \/ c4_2 a687 a711 \/ ssSkC1
% 0.19/0.46  |- ~c4_1 a689 \/ ~ndr1_0 \/ ~ssSkC4 \/ c1_2 a689 $_62 \/ c2_2 a689 $_62 \/
% 0.19/0.46     c3_0 \/ c4_0 \/ c4_2 a689 a711
% 0.19/0.46  |- ~c4_1 a698 \/ ~ndr1_0 \/ ~ssSkC4 \/ c1_2 a698 $_62 \/ c2_2 a698 $_62 \/
% 0.19/0.46     c3_0 \/ c4_2 a698 a711 \/ c5_0
% 0.19/0.46  |- ~c4_1 $_61 \/ ~ndr1_0 \/ ~ssSkC4 \/ c1_2 $_61 $_62 \/ c2_2 $_61 $_62 \/
% 0.19/0.46     c3_0 \/ c4_2 $_61 a711 \/ ssSkC0
% 0.19/0.46  |- ~ndr1_0 \/ ~ssSkC4 \/ c1_2 a717 $_66 \/ c2_2 a717 $_66 \/ c3_0 \/
% 0.19/0.46     c4_2 a717 a711 \/ ssSkC5
% 0.19/0.46  |- ~c1_1 $_72 \/ ~c3_0 \/ ~ndr1_0 \/ ~ndr1_1 $_72 \/ c4_1 $_72 \/
% 0.19/0.46     c5_2 $_72 a683 \/ ssSkP0 $_72
% 0.19/0.46  |- ~c1_1 a698 \/ ~c3_0 \/ ~ndr1_0 \/ c4_1 a698 \/ c5_0 \/ c5_2 a698 a683 \/
% 0.19/0.46     ssSkP0 a698
% 0.19/0.46  |- ~c1_1 a706 \/ ~c3_0 \/ ~ndr1_0 \/ c4_1 a706 \/ c5_2 a706 a683 \/
% 0.19/0.46     ssSkC3 \/ ssSkP0 a706
% 0.19/0.46  |- ~c1_1 $_73 \/ ~c3_0 \/ ~ndr1_0 \/ c1_0 \/ c4_1 $_73 \/ c5_2 $_73 a683 \/
% 0.19/0.46     ssSkC0 \/ ssSkP0 $_73
% 0.19/0.46  |- ~c1_1 $_73 \/ ~c3_0 \/ ~ndr1_0 \/ c4_1 $_73 \/ c5_0 \/ c5_2 $_73 a683 \/
% 0.19/0.46     ssSkC0 \/ ssSkP0 $_73
% 0.19/0.46  |- ~c1_1 $_73 \/ ~c3_0 \/ ~ndr1_0 \/ c4_0 \/ c4_1 $_73 \/ c5_2 $_73 a683 \/
% 0.19/0.46     ssSkC0 \/ ssSkP0 $_73
% 0.19/0.46  |- ~c3_0 \/ c4_0 \/ c4_1 a689 \/ c5_2 a689 a683 \/ ssSkP0 a689
% 0.19/0.46  |- ~c3_0 \/ c1_0 \/ c4_1 a710 \/ c5_2 a710 a683 \/ ssSkC0 \/ ssSkC4 \/
% 0.19/0.46     ssSkP0 a710
% 0.19/0.46  |- ~c3_0 \/ c4_1 a710 \/ c5_0 \/ c5_2 a710 a683 \/ ssSkC0 \/ ssSkC4 \/
% 0.19/0.46     ssSkP0 a710
% 0.19/0.46  |- ~c3_0 \/ c4_0 \/ c4_1 a710 \/ c5_2 a710 a683 \/ ssSkC0 \/ ssSkC4 \/
% 0.19/0.46     ssSkP0 a710
% 0.19/0.46  |- c1_0 \/ c1_2 a694 $_82 \/ c2_1 a694 \/ c2_2 a694 $_82 \/
% 0.19/0.46     c3_2 a694 $_82 \/ c4_0 \/ c5_2 a694 a681 \/ ssSkC0
% 0.19/0.46  |- c1_0 \/ c1_2 a694 $_87 \/ c2_1 a694 \/ c2_2 a694 $_87 \/
% 0.19/0.46     c3_2 a694 $_87 \/ c4_0 \/ c4_2 a694 a681 \/ ssSkC0
% 0.19/0.46  |- ~c1_2 a694 a681 \/ ~ndr1_0 \/ ~ndr1_1 a694 \/ c1_0 \/ c1_2 a694 $_90 \/
% 0.19/0.46     c2_1 a694 \/ c2_2 a694 $_90 \/ c3_2 a694 $_90 \/ c4_0 \/ ssSkC0
% 0.19/0.46  |- ~c2_2 a694 $_102 \/ ~c3_0 \/ ~c3_1 a715 \/ ~ndr1_0 \/ ~ndr1_1 a694 \/
% 0.19/0.46     c1_0 \/ c1_2 a694 $_103 \/ c2_1 a694 \/ c2_2 a694 $_103 \/
% 0.19/0.46     c3_2 a694 $_102 \/ c4_0 \/ c4_2 a694 a681 \/ ssSkC0
% 0.19/0.46  |- ~c2_2 a694 $_102 \/ ~c3_0 \/ ~c3_1 a715 \/ ~ndr1_0 \/ ~ndr1_1 a694 \/
% 0.19/0.46     c1_0 \/ c1_2 a694 $_103 \/ c2_1 a694 \/ c2_2 a694 $_103 \/
% 0.19/0.46     c3_2 a694 $_102 \/ c4_0 \/ c5_2 a694 a681 \/ ssSkC0
% 0.19/0.46  |- ~c2_2 a694 $_105 \/ ~c3_0 \/ ~c5_2 a715 a716 \/ ~ndr1_0 \/
% 0.19/0.46     ~ndr1_1 a694 \/ c1_0 \/ c1_2 a694 $_106 \/ c2_1 a694 \/
% 0.19/0.46     c2_2 a694 $_106 \/ c3_2 a694 $_105 \/ c4_0 \/ c4_2 a694 a681 \/ ssSkC0
% 0.19/0.46  |- ~c2_2 a694 $_105 \/ ~c3_0 \/ ~c5_2 a715 a716 \/ ~ndr1_0 \/
% 0.19/0.46     ~ndr1_1 a694 \/ c1_0 \/ c1_2 a694 $_106 \/ c2_1 a694 \/
% 0.19/0.46     c2_2 a694 $_106 \/ c3_2 a694 $_105 \/ c4_0 \/ c5_2 a694 a681 \/ ssSkC0
% 0.19/0.46  |- ~c2_2 a694 $_108 \/ ~c3_0 \/ ~c4_2 a715 a716 \/ ~ndr1_0 \/
% 0.19/0.46     ~ndr1_1 a694 \/ c1_0 \/ c1_2 a694 $_109 \/ c2_1 a694 \/
% 0.19/0.46     c2_2 a694 $_109 \/ c3_2 a694 $_108 \/ c4_0 \/ c4_2 a694 a681 \/ ssSkC0
% 0.19/0.46  |- ~c2_2 a694 $_108 \/ ~c3_0 \/ ~c4_2 a715 a716 \/ ~ndr1_0 \/
% 0.19/0.46     ~ndr1_1 a694 \/ c1_0 \/ c1_2 a694 $_109 \/ c2_1 a694 \/
% 0.19/0.46     c2_2 a694 $_109 \/ c3_2 a694 $_108 \/ c4_0 \/ c5_2 a694 a681 \/ ssSkC0
% 0.19/0.46  |- ~c2_2 a694 $_111 \/ ~c2_2 a715 a716 \/ ~c3_0 \/ ~ndr1_0 \/
% 0.19/0.46     ~ndr1_1 a694 \/ c1_0 \/ c1_2 a694 $_112 \/ c2_1 a694 \/
% 0.19/0.46     c2_2 a694 $_112 \/ c3_2 a694 $_111 \/ c4_0 \/ c4_2 a694 a681 \/ ssSkC0
% 0.19/0.46  |- ~c2_2 a694 $_111 \/ ~c2_2 a715 a716 \/ ~c3_0 \/ ~ndr1_0 \/
% 0.19/0.46     ~ndr1_1 a694 \/ c1_0 \/ c1_2 a694 $_112 \/ c2_1 a694 \/
% 0.19/0.46     c2_2 a694 $_112 \/ c3_2 a694 $_111 \/ c4_0 \/ c5_2 a694 a681 \/ ssSkC0
% 0.19/0.46  |- ~c1_2 a694 $_115 \/ ~c2_2 a694 $_115 \/ ~c2_2 a694 a681 \/ ~ndr1_0 \/
% 0.19/0.46     ~ndr1_1 a694 \/ c1_0 \/ c1_2 a694 $_87 \/ c2_0 \/ c2_1 a694 \/
% 0.19/0.46     c2_2 a694 $_87 \/ c3_2 a694 $_87 \/ c3_2 a694 a681 \/ c3_2 a694 a695 \/
% 0.19/0.46     c4_0 \/ ssSkC0
% 0.19/0.46  |- ~c1_2 $_113 $_115 \/ ~c2_2 $_113 $_115 \/ ~c2_2 $_113 a683 \/ ~ndr1_0 \/
% 0.19/0.46     ~ndr1_1 $_113 \/ c2_0 \/ c3_2 $_113 a683 \/ c3_2 $_113 a695 \/
% 0.19/0.46     ssSkP0 $_113
% 0.19/0.46  |- ~c1_2 $_113 a683 \/ ~c2_2 $_113 a683 \/ ~ndr1_0 \/ ~ndr1_1 $_113 \/
% 0.19/0.46     c2_0 \/ c3_2 $_113 a683 \/ c3_2 $_113 a695 \/ ssSkP0 $_113
% 0.19/0.46  |- ~c1_2 a687 $_117 \/ ~c2_2 a687 $_117 \/ ~ndr1_0 \/ ~ndr1_1 a687 \/
% 0.19/0.46     c2_0 \/ c3_2 a687 a688 \/ c3_2 a687 a695 \/ ssSkC1
% 0.19/0.46  |- ~c1_2 a689 a690 \/ ~c2_2 a689 a683 \/ ~ndr1_0 \/ ~ndr1_1 a689 \/ c2_0 \/
% 0.19/0.46     c3_2 a689 a683 \/ c3_2 a689 a695 \/ c4_0 \/ ssSkP0 a689
% 0.19/0.46  |- ~c1_2 a694 $_123 \/ ~c2_2 a694 $_123 \/ ~c2_2 a694 a681 \/ ~ndr1_0 \/
% 0.19/0.46     ~ndr1_1 a694 \/ c1_0 \/ c1_2 a694 $_87 \/ c2_0 \/ c2_1 a694 \/
% 0.19/0.46     c2_2 a694 $_87 \/ c2_2 a694 a695 \/ c3_2 a694 $_87 \/ c3_2 a694 a681 \/
% 0.19/0.46     c4_0 \/ ssSkC0
% 0.19/0.46  |- ~c1_2 $_121 $_123 \/ ~c2_2 $_121 $_123 \/ ~c2_2 $_121 a683 \/ ~ndr1_0 \/
% 0.19/0.46     ~ndr1_1 $_121 \/ c2_0 \/ c2_2 $_121 a695 \/ c3_2 $_121 a683 \/
% 0.19/0.46     ssSkP0 $_121
% 0.19/0.46  |- ~c1_2 $_121 a683 \/ ~c2_2 $_121 a683 \/ ~ndr1_0 \/ ~ndr1_1 $_121 \/
% 0.19/0.46     c2_0 \/ c2_2 $_121 a695 \/ c3_2 $_121 a683 \/ ssSkP0 $_121
% 0.19/0.46  |- ~c1_2 a687 $_125 \/ ~c2_2 a687 $_125 \/ ~ndr1_0 \/ ~ndr1_1 a687 \/
% 0.19/0.46     c2_0 \/ c2_2 a687 a695 \/ c3_2 a687 a688 \/ ssSkC1
% 0.19/0.46  |- ~c1_2 a689 a690 \/ ~c2_2 a689 a683 \/ ~ndr1_0 \/ ~ndr1_1 a689 \/ c2_0 \/
% 0.19/0.46     c2_2 a689 a695 \/ c3_2 a689 a683 \/ c4_0 \/ ssSkP0 a689
% 0.19/0.46  |- ~c2_2 a694 $_151 \/ ~c2_2 a694 a681 \/ ~c4_1 $_148 \/ ~ndr1_0 \/
% 0.19/0.46     ~ndr1_1 a694 \/ c1_0 \/ c1_2 a694 $_87 \/ c1_2 a694 a682 \/ c2_1 a694 \/
% 0.19/0.46     c2_2 a694 $_87 \/ c3_2 a694 $_87 \/ c3_2 a694 a681 \/ c4_0 \/
% 0.19/0.46     c5_1 $_148 \/ c5_2 a694 $_151 \/ ssSkC0
% 0.19/0.46  |- ~c2_2 $_149 $_151 \/ ~c2_2 $_149 a683 \/ ~c4_1 $_148 \/ ~ndr1_0 \/
% 0.19/0.46     ~ndr1_1 $_149 \/ c1_2 $_149 a682 \/ c3_2 $_149 a683 \/ c4_0 \/
% 0.19/0.46     c5_1 $_148 \/ c5_2 $_149 $_151 \/ ssSkP0 $_149
% 0.19/0.46  |- ~c2_2 $_149 a683 \/ ~c4_1 $_148 \/ ~ndr1_0 \/ ~ndr1_1 $_149 \/
% 0.19/0.46     c1_2 $_149 a682 \/ c3_2 $_149 a683 \/ c4_0 \/ c5_1 $_148 \/
% 0.19/0.46     c5_2 $_149 a683 \/ ssSkP0 $_149
% 0.19/0.46  |- ~c2_2 a689 a683 \/ ~c4_1 $_154 \/ ~ndr1_0 \/ ~ndr1_1 a689 \/
% 0.19/0.46     c1_2 a689 a682 \/ c3_2 a689 a683 \/ c4_0 \/ c5_1 $_154 \/
% 0.19/0.46     c5_2 a689 a690 \/ ssSkP0 a689
% 0.19/0.46  |- ~c2_2 $_159 $_161 \/ ~c2_2 $_159 a683 \/ ~c4_1 $_158 \/
% 0.19/0.46     ~c4_2 $_159 a682 \/ ~ndr1_0 \/ ~ndr1_1 $_159 \/ c3_2 $_159 a683 \/
% 0.19/0.46     c4_0 \/ c5_1 $_158 \/ c5_2 $_159 $_161 \/ ssSkP0 $_159
% 0.19/0.46  |- ~c2_2 a694 $_160 \/ ~c2_2 a694 $_161 \/ ~c4_1 $_158 \/
% 0.19/0.46     ~c4_2 a694 $_160 \/ ~ndr1_0 \/ ~ndr1_1 a694 \/ c2_2 a694 a682 \/
% 0.19/0.46     c3_2 a694 $_160 \/ c3_2 a694 a682 \/ c4_0 \/ c5_1 $_158 \/
% 0.19/0.46     c5_2 a694 $_161 \/ ssSkC0
% 0.19/0.46  |- ~c2_2 a694 $_164 \/ ~c2_2 a694 a683 \/ ~c4_1 $_162 \/ ~ndr1_0 \/
% 0.19/0.46     ~ndr1_1 a694 \/ c2_2 a694 a682 \/ c3_2 a694 a682 \/ c3_2 a694 a683 \/
% 0.19/0.46     c4_0 \/ c5_1 $_162 \/ c5_2 a694 $_164 \/ ssSkC0 \/ ssSkP0 a694
% 0.19/0.46  |- ~c2_2 a694 a683 \/ ~c4_1 $_162 \/ ~ndr1_0 \/ ~ndr1_1 a694 \/
% 0.19/0.46     c2_2 a694 a682 \/ c3_2 a694 a682 \/ c3_2 a694 a683 \/ c4_0 \/
% 0.19/0.46     c5_1 $_162 \/ c5_2 a694 a683 \/ ssSkC0 \/ ssSkP0 a694
% 0.19/0.46  |- ~c2_2 a694 $_170 \/ ~c2_2 a694 a681 \/ ~c4_1 $_168 \/ ~ndr1_0 \/
% 0.19/0.46     ~ndr1_1 a694 \/ c1_0 \/ c1_2 a694 $_87 \/ c2_1 a694 \/ c2_2 a694 $_87 \/
% 0.19/0.46     c2_2 a694 a682 \/ c3_2 a694 $_87 \/ c3_2 a694 a681 \/ c3_2 a694 a682 \/
% 0.19/0.46     c4_0 \/ c5_1 $_168 \/ c5_2 a694 $_170 \/ ssSkC0
% 0.19/0.46  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.46  
%------------------------------------------------------------------------------