↑ Up

Metis---2.4.SAT-Sat.s

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

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

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

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12  % Problem  : SYN536-1 : TPTP v8.1.0. Released v2.1.0.
% 0.10/0.12  % Command  : metis --show proof --show saturation %s
% 0.12/0.33  % Computer : n009.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 : Tue Jul 12 01:09:22 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 0.12/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.18/0.51  % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.51  
% 0.18/0.51  SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.51  |- ndr1_0 \/ ssSkC5
% 0.18/0.51  |- ndr1_0 \/ ssSkC4
% 0.18/0.51  |- ndr1_0 \/ ssSkC2
% 0.18/0.51  |- ndr1_0 \/ ssSkC0
% 0.18/0.51  |- ~ssSkC6 \/ c1_0 \/ ndr1_0
% 0.18/0.51  |- ~c2_0 \/ ndr1_0
% 0.18/0.51  |- c1_0 \/ c4_0 \/ c5_0
% 0.18/0.51  |- ~c5_0 \/ c2_0
% 0.18/0.51  |- ~c3_0 \/ c5_0
% 0.18/0.51  |- c3_1 a540 \/ ssSkC5
% 0.18/0.51  |- ndr1_1 a537 \/ ssSkC4
% 0.18/0.51  |- ndr1_1 a527 \/ ssSkC2
% 0.18/0.51  |- c5_1 a527 \/ ssSkC2
% 0.18/0.51  |- ~ssSkC6 \/ c1_0 \/ ndr1_1 a544
% 0.18/0.51  |- ~ssSkC6 \/ c1_0 \/ c4_1 a544
% 0.18/0.51  |- ~ssSkC6 \/ c1_0 \/ c1_1 a544
% 0.18/0.51  |- ~c3_0 \/ c2_0 \/ ndr1_0
% 0.18/0.51  |- ~c2_0 \/ ndr1_1 a525
% 0.18/0.51  |- ~c2_0 \/ c3_1 a525
% 0.18/0.51  |- c1_1 a520 \/ c3_0 \/ c5_0
% 0.18/0.51  |- ~c4_1 a540 \/ ssSkC5
% 0.18/0.51  |- c2_2 a537 a538 \/ ssSkC4
% 0.18/0.51  |- c3_2 a537 a538 \/ ssSkC4
% 0.18/0.51  |- ~c5_1 a537 \/ ssSkC4
% 0.18/0.51  |- c1_2 a527 a528 \/ ssSkC2
% 0.18/0.51  |- ~c3_1 a527 \/ ssSkC2
% 0.18/0.51  |- ~c2_1 a521 \/ ssSkC0
% 0.18/0.51  |- ~c1_1 a521 \/ ssSkC0
% 0.18/0.51  |- ~ssSkC6 \/ c1_0 \/ c3_2 a544 a545
% 0.18/0.51  |- ~c4_0 \/ ~ssSkC2 \/ ndr1_1 a529
% 0.18/0.51  |- ~c4_0 \/ ~ssSkC2 \/ c4_1 a529
% 0.18/0.51  |- ~c2_0 \/ c2_2 a525 a526
% 0.18/0.51  |- ~c2_0 \/ c4_2 a525 a526
% 0.18/0.51  |- ~c2_0 \/ ~c2_1 a525
% 0.18/0.51  |- ~c5_1 a520 \/ c3_0 \/ c5_0
% 0.18/0.51  |- ~c3_2 a527 a528 \/ ssSkC2
% 0.18/0.51  |- ~c1_2 a544 a545 \/ ~ssSkC6 \/ c1_0
% 0.18/0.51  |- ~c5_2 a544 a545 \/ ~ssSkC6 \/ c1_0
% 0.18/0.51  |- ~c3_0 \/ ~c5_1 a536 \/ c2_0
% 0.18/0.51  |- ~c1_1 a536 \/ ~c3_0 \/ c2_0
% 0.18/0.51  |- ~c2_0 \/ ~c3_1 a533 \/ ~ssSkC3
% 0.18/0.51  |- ~c4_0 \/ ~ssSkC2 \/ c1_2 a529 a531
% 0.18/0.51  |- ~c4_0 \/ ~ssSkC2 \/ c5_2 a529 a531
% 0.18/0.51  |- ~c4_0 \/ ~ssSkC2 \/ c5_2 a529 a530
% 0.18/0.51  |- ~c4_0 \/ ~ssSkC2 \/ c4_2 a529 a530
% 0.18/0.51  |- ~c4_0 \/ ~ssSkC2 \/ c1_2 a529 a530
% 0.18/0.51  |- ~c1_2 a525 a526 \/ ~c2_0
% 0.18/0.51  |- ~ndr1_0 \/ c1_1 $U \/ ndr1_1 $U \/ ssSkC6
% 0.18/0.51  |- ~ndr1_0 \/ c1_1 $U \/ ndr1_1 $U \/ ssSkC3
% 0.18/0.51  |- ~ndr1_0 \/ c1_1 $U \/ c2_2 $U a543 \/ ssSkC6
% 0.18/0.51  |- ~ndr1_0 \/ c1_1 $U \/ c4_2 $U a532 \/ ssSkC3
% 0.18/0.51  |- ~c3_1 $U \/ ~ndr1_0 \/ ~ssSkC0 \/ c5_1 $U \/ ndr1_1 $U
% 0.18/0.51  |- ~c5_2 $U a543 \/ ~ndr1_0 \/ c1_1 $U \/ ssSkC6
% 0.18/0.51  |- ~c1_2 $U a543 \/ ~ndr1_0 \/ c1_1 $U \/ ssSkC6
% 0.18/0.51  |- ~c3_2 $U a532 \/ ~ndr1_0 \/ c1_1 $U \/ ssSkC3
% 0.18/0.51  |- ~c5_2 $U a532 \/ ~ndr1_0 \/ c1_1 $U \/ ssSkC3
% 0.18/0.51  |- ~c3_1 $U \/ ~ndr1_0 \/ ~ssSkC0 \/ c5_1 $U \/ c5_2 $U a522
% 0.18/0.51  |- ~c3_1 $U \/ ~ndr1_0 \/ ~ssSkC0 \/ c2_2 $U a522 \/ c5_1 $U
% 0.18/0.51  |- ~c3_0 \/ ~ndr1_1 a536 \/ c2_0 \/ c2_2 a536 $U \/ c4_2 a536 $U
% 0.18/0.51  |- ~c4_2 a541 $U \/ ~ndr1_1 a541 \/ ~ssSkC5 \/ c2_2 a541 $U \/
% 0.18/0.51     c3_2 a541 $U \/ c5_0
% 0.18/0.51  |- ~c5_2 a541 $U \/ ~ndr1_1 a541 \/ ~ssSkC5 \/ c2_2 a541 $U \/
% 0.18/0.51     c3_2 a541 $U \/ c5_0
% 0.18/0.51  |- ~c2_2 $U $V \/ ~c4_0 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c2_0 \/ c3_2 $U $V \/
% 0.18/0.51     c5_1 $U
% 0.18/0.51  |- ~c1_0 \/ ~c3_0 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c2_2 $U $V \/ c3_2 $U $V \/
% 0.18/0.51     c5_1 $U
% 0.18/0.51  |- ~c1_2 a540 $U \/ ~c3_2 a540 $U \/ ~ndr1_1 a540 \/ c2_2 a540 $U \/ ssSkC5
% 0.18/0.51  |- ~c2_2 a521 $U \/ ~c5_2 a521 $U \/ ~ndr1_1 a521 \/ c1_2 a521 $U \/ ssSkC0
% 0.18/0.51  |- ~c2_0 \/ ~c3_2 a533 $U \/ ~ndr1_1 a533 \/ ~ssSkC3 \/ c4_2 a533 $U \/
% 0.18/0.51     c5_2 a533 $U
% 0.18/0.51  |- ~c1_2 a520 $U \/ ~c3_2 a520 $U \/ ~c5_2 a520 $U \/ ~ndr1_1 a520 \/
% 0.18/0.51     c3_0 \/ c5_0
% 0.18/0.51  |- ~c3_2 $U a523 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $V \/ c2_2 $U $V \/
% 0.18/0.51     c3_2 $U $V \/ c4_1 $U \/ ssSkC1
% 0.18/0.51  |- ~c1_2 $U a523 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $V \/ c2_2 $U $V \/
% 0.18/0.51     c3_2 $U $V \/ c4_1 $U \/ ssSkC1
% 0.18/0.51  |- ~c1_0 \/ ~c1_2 $U $V \/ ~c2_1 $U \/ ~c2_2 $U a542 \/ ~c5_0 \/ ~ndr1_0 \/
% 0.18/0.51     ~ndr1_1 $U \/ c4_2 $U $V
% 0.18/0.51  |- ~c1_0 \/ ~c1_2 $U $V \/ ~c2_1 $U \/ ~c4_2 $U a542 \/ ~c5_0 \/ ~ndr1_0 \/
% 0.18/0.51     ~ndr1_1 $U \/ c4_2 $U $V
% 0.18/0.51  |- ~c1_0 \/ ~c1_2 $U $V \/ ~c2_1 $U \/ ~c5_0 \/ ~c5_2 $U a542 \/ ~ndr1_0 \/
% 0.18/0.51     ~ndr1_1 $U \/ c4_2 $U $V
% 0.18/0.51  |- ~c1_2 $U $V \/ ~c2_0 \/ ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.18/0.51     ~ssSkC4 \/ c2_2 $U a539 \/ c3_2 $U $V \/ c4_1 $U
% 0.18/0.51  |- ~c1_2 $U $V \/ ~c2_0 \/ ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.18/0.51     ~ssSkC4 \/ c1_2 $U a539 \/ c3_2 $U $V \/ c4_1 $U
% 0.18/0.51  |- ~c1_2 $U $V \/ ~c2_0 \/ ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.18/0.51     ~ssSkC4 \/ c3_2 $U $V \/ c4_1 $U \/ c5_2 $U a539
% 0.18/0.51  |- ~c3_2 $U $V \/ ~c4_0 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_1 $W \/
% 0.18/0.51     c1_2 $U $V \/ c4_1 $W \/ c4_2 $U $V \/ c5_1 $U \/ ndr1_1 $W
% 0.18/0.51  |- ~ndr1_0 \/ ~ndr1_1 $U \/ c1_1 $V \/ c1_2 $U $W \/ c3_1 $U \/
% 0.18/0.51     c3_2 $U $W \/ c4_1 $V \/ c4_2 $U $W \/ c4_2 $U a534 \/ c5_0 \/ c5_1 $V
% 0.18/0.51  |- ~c1_2 $U $V \/ ~c2_2 $U $V \/ ~c3_0 \/ ~c3_2 $U $V \/ ~ndr1_0 \/
% 0.18/0.51     ~ndr1_1 $U \/ ~ssSkC1 \/ c1_2 $U a524 \/ c4_1 $U
% 0.18/0.51  |- ~c1_2 $U $V \/ ~c2_2 $U $V \/ ~c3_0 \/ ~c3_2 $U $V \/ ~ndr1_0 \/
% 0.18/0.51     ~ndr1_1 $U \/ ~ssSkC1 \/ c4_1 $U \/ c5_2 $U a524
% 0.18/0.51  |- ~c3_2 $U a534 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_1 $V \/ c1_2 $U $W \/
% 0.18/0.51     c3_1 $U \/ c3_2 $U $W \/ c4_1 $V \/ c4_2 $U $W \/ c5_0 \/ c5_1 $V
% 0.18/0.51  |- ~c3_2 $U $V \/ ~c4_0 \/ ~c4_2 $W a535 \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.18/0.51     c1_1 $W \/ c1_2 $U $V \/ c4_1 $W \/ c4_2 $U $V \/ c5_1 $U
% 0.18/0.51  |- ~c3_2 $U $V \/ ~c3_2 $W a535 \/ ~c4_0 \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.18/0.51     c1_1 $W \/ c1_2 $U $V \/ c4_1 $W \/ c4_2 $U $V \/ c5_1 $U
% 0.18/0.51  |- ~c1_2 $U $V \/ ~c2_2 $U $V \/ ~c3_0 \/ ~c3_2 $U $V \/ ~c4_2 $U a524 \/
% 0.18/0.51     ~ndr1_0 \/ ~ndr1_1 $U \/ ~ssSkC1 \/ c4_1 $U
% 0.18/0.51  |- ~c1_2 $V $X \/ ~c3_2 $V $W \/ ~c3_2 $V $Y \/ ~c5_1 $U \/ ~c5_2 $V $W \/
% 0.18/0.51     ~ndr1_0 \/ ~ndr1_1 $V \/ c1_0 \/ c2_1 $U \/ c2_2 $V $Y \/ c4_2 $V $W \/
% 0.18/0.51     c4_2 $V $X \/ c4_2 $V $Y
% 0.18/0.51  |- ~c3_2 $W a535 \/ ~c4_0 \/ ~ndr1_0 \/ ~ndr1_1 $W \/ c1_1 $W \/
% 0.18/0.51     c1_2 $W a535 \/ c4_1 $W \/ c4_2 $W a535 \/ c5_1 $W
% 0.18/0.51  |- c5_0 \/ ndr1_0
% 0.18/0.51  |- c1_0 \/ c2_0 \/ c4_0
% 0.18/0.51  |- ~c4_0 \/ ndr1_0
% 0.18/0.51  |- c1_0 \/ c2_0 \/ ndr1_0
% 0.18/0.51  |- c1_0 \/ c1_1 $_0 \/ c2_0 \/ ndr1_1 $_0 \/ ssSkC6
% 0.18/0.51  |- c1_1 $_0 \/ c5_0 \/ ndr1_1 $_0 \/ ssSkC6
% 0.18/0.51  |- c1_0 \/ c1_1 $_1 \/ c2_0 \/ ndr1_1 $_1 \/ ssSkC3
% 0.18/0.51  |- c1_1 $_1 \/ c5_0 \/ ndr1_1 $_1 \/ ssSkC3
% 0.18/0.51  |- c1_0 \/ c1_1 $_6 \/ c2_0 \/ c2_2 $_6 a543 \/ ssSkC6
% 0.18/0.51  |- c1_1 $_6 \/ c2_2 $_6 a543 \/ c5_0 \/ ssSkC6
% 0.18/0.51  |- c1_0 \/ c1_1 $_7 \/ c2_0 \/ c4_2 $_7 a532 \/ ssSkC3
% 0.18/0.51  |- c1_1 $_7 \/ c4_2 $_7 a532 \/ c5_0 \/ ssSkC3
% 0.18/0.51  |- ~ndr1_0 \/ ~ssSkC0 \/ c5_1 a540 \/ ndr1_1 a540 \/ ssSkC5
% 0.18/0.51  |- ~ndr1_0 \/ ~ssSkC0 \/ c5_1 a540 \/ c5_2 a540 a522 \/ ssSkC5
% 0.18/0.51  |- ~ndr1_0 \/ ~ssSkC0 \/ c2_2 a540 a522 \/ c5_1 a540 \/ ssSkC5
% 0.18/0.51  |- ~c3_0 \/ c1_0 \/ c1_1 a536 \/ c2_0 \/ c2_2 a536 $_19 \/
% 0.18/0.51     c4_2 a536 $_19 \/ ssSkC3
% 0.18/0.51  |- ~c3_0 \/ c1_0 \/ c1_1 a536 \/ c2_0 \/ c2_2 a536 $_19 \/
% 0.18/0.51     c4_2 a536 $_19 \/ ssSkC6
% 0.18/0.51  |- ~ssSkC5 \/ c1_1 a541 \/ c2_2 a541 a532 \/ c3_2 a541 a532 \/ c5_0 \/
% 0.18/0.51     ssSkC3
% 0.18/0.51  |- ~c1_0 \/ ~c3_0 \/ ~ndr1_0 \/ c2_2 a537 $_31 \/ c3_2 a537 $_31 \/
% 0.18/0.51     c5_1 a537 \/ ssSkC4
% 0.18/0.51  |- c1_0 \/ c1_1 $_35 \/ c2_0 \/ c3_2 $_35 a543 \/ c5_1 $_35 \/ ssSkC6
% 0.18/0.51  |- ~c4_0 \/ c1_1 $_38 \/ c2_0 \/ c3_2 $_38 a543 \/ c5_0 \/ c5_1 $_38 \/
% 0.18/0.51     ssSkC6
% 0.18/0.51  |- ~c1_2 a537 a538 \/ ~c3_0 \/ ~ndr1_0 \/ ~ndr1_1 a537 \/ ~ssSkC1 \/
% 0.18/0.51     c1_2 a537 a524 \/ c4_1 a537 \/ ssSkC4
% 0.18/0.51  |- ~c1_2 a537 a538 \/ ~c3_0 \/ ~ndr1_0 \/ ~ndr1_1 a537 \/ ~ssSkC1 \/
% 0.18/0.51     c4_1 a537 \/ c5_2 a537 a524 \/ ssSkC4
% 0.18/0.51  |- ~c4_0 \/ ~ndr1_0 \/ c1_1 $_66 \/ c1_2 a537 a538 \/ c4_1 $_66 \/
% 0.18/0.51     c4_2 a537 a538 \/ c5_1 a537 \/ ndr1_1 $_66 \/ ssSkC4
% 0.18/0.51  |- ~c4_0 \/ c1_1 $_67 \/ c1_2 a537 a538 \/ c4_1 $_67 \/ c4_2 a537 a538 \/
% 0.18/0.51     c5_0 \/ c5_1 a537 \/ ndr1_1 $_67 \/ ssSkC4
% 0.18/0.51  |- c1_0 \/ c1_1 $_69 \/ c1_2 a537 a538 \/ c2_0 \/ c4_1 $_69 \/
% 0.18/0.51     c4_2 a537 a538 \/ c5_1 a537 \/ ndr1_1 $_69 \/ ssSkC4
% 0.18/0.51  |- ~c3_2 $_76 a535 \/ ~c4_0 \/ ~ndr1_0 \/ ~ndr1_1 a537 \/ c1_1 $_76 \/
% 0.18/0.51     c1_2 a537 a538 \/ c4_1 $_76 \/ c4_2 a537 a538 \/ c5_1 a537 \/ ssSkC4
% 0.18/0.51  |- ~c4_0 \/ ~c4_2 $_79 a535 \/ ~ndr1_0 \/ c1_0 \/ c1_1 $_78 \/ c1_1 $_79 \/
% 0.18/0.51     c1_2 $_78 a543 \/ c2_0 \/ c4_1 $_79 \/ c4_2 $_78 a543 \/ c5_1 $_78 \/
% 0.18/0.51     ssSkC6
% 0.18/0.51  |- c1_1 $_85 \/ c1_2 a537 $_86 \/ c3_1 a537 \/ c3_2 a537 $_86 \/
% 0.18/0.51     c4_1 $_85 \/ c4_2 a537 $_86 \/ c4_2 a537 a534 \/ c5_0 \/ c5_1 $_85 \/
% 0.18/0.51     ssSkC4
% 0.18/0.51  |- c1_1 $_85 \/ c1_2 a537 a534 \/ c3_1 a537 \/ c3_2 a537 a534 \/
% 0.18/0.51     c4_1 $_85 \/ c4_2 a537 a534 \/ c5_0 \/ c5_1 $_85 \/ ssSkC4
% 0.18/0.51  |- ~c3_2 $U $V \/ ~c4_0 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_1 $_88 \/
% 0.18/0.51     c1_1 a537 \/ c1_2 $U $V \/ c1_2 a537 a535 \/ c3_1 a537 \/
% 0.18/0.51     c3_2 a537 a535 \/ c4_1 $_88 \/ c4_1 a537 \/ c4_2 $U $V \/
% 0.18/0.51     c4_2 a537 a534 \/ c5_0 \/ c5_1 $U \/ c5_1 $_88 \/ ssSkC4
% 0.18/0.51  |- c1_1 $_90 \/ c1_2 a527 $_91 \/ c3_1 a527 \/ c3_2 a527 $_91 \/
% 0.18/0.51     c4_1 $_90 \/ c4_2 a527 $_91 \/ c4_2 a527 a534 \/ c5_0 \/ c5_1 $_90 \/
% 0.18/0.51     ssSkC2
% 0.18/0.51  |- c1_1 $_90 \/ c1_2 a527 a534 \/ c3_1 a527 \/ c3_2 a527 a534 \/
% 0.18/0.51     c4_1 $_90 \/ c4_2 a527 a534 \/ c5_0 \/ c5_1 $_90 \/ ssSkC2
% 0.18/0.51  |- ~c3_2 $U $V \/ ~c4_0 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_1 $_93 \/
% 0.18/0.51     c1_1 a527 \/ c1_2 $U $V \/ c1_2 a527 a535 \/ c3_1 a527 \/
% 0.18/0.51     c3_2 a527 a535 \/ c4_1 $_93 \/ c4_1 a527 \/ c4_2 $U $V \/
% 0.18/0.51     c4_2 a527 a534 \/ c5_0 \/ c5_1 $U \/ c5_1 $_93 \/ ssSkC2
% 0.18/0.51  |- ~c3_2 $_99 a535 \/ ~c4_0 \/ ~ndr1_0 \/ c1_0 \/ c1_1 $_98 \/ c1_1 $_99 \/
% 0.18/0.51     c1_2 $_98 a543 \/ c2_0 \/ c4_1 $_99 \/ c4_2 $_98 a543 \/ c5_1 $_98 \/
% 0.18/0.51     ssSkC6
% 0.18/0.51  |- c1_1 $_102 \/ c1_1 $_103 \/ c1_2 $_102 $_104 \/ c3_1 $_102 \/
% 0.18/0.51     c3_2 $_102 $_104 \/ c4_1 $_103 \/ c4_2 $_102 $_104 \/ c4_2 $_102 a534 \/
% 0.18/0.51     c5_0 \/ c5_1 $_103 \/ ssSkC3
% 0.18/0.51  |- c1_1 $_102 \/ c1_1 $_103 \/ c1_2 $_102 a534 \/ c3_1 $_102 \/
% 0.18/0.51     c3_2 $_102 a534 \/ c4_1 $_103 \/ c4_2 $_102 a534 \/ c5_0 \/
% 0.18/0.51     c5_1 $_103 \/ ssSkC3
% 0.18/0.51  |- ~ssSkC5 \/ c1_1 $_107 \/ c1_1 a541 \/ c1_2 a541 a534 \/
% 0.18/0.51     c2_2 a541 a534 \/ c3_1 a541 \/ c3_2 a541 a534 \/ c4_1 $_107 \/ c5_0 \/
% 0.18/0.51     c5_1 $_107 \/ ssSkC3
% 0.18/0.52  |- ~c3_2 $U $V \/ ~c4_0 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_1 $_109 \/
% 0.18/0.52     c1_1 $_110 \/ c1_2 $U $V \/ c1_2 $_109 a535 \/ c3_1 $_109 \/
% 0.18/0.52     c3_2 $_109 a535 \/ c4_1 $_109 \/ c4_1 $_110 \/ c4_2 $U $V \/
% 0.18/0.52     c4_2 $_109 a534 \/ c5_0 \/ c5_1 $U \/ c5_1 $_110 \/ ssSkC3
% 0.18/0.52  |- c1_1 $_112 \/ c1_1 $_113 \/ c1_2 $_112 $_114 \/ c3_1 $_112 \/
% 0.18/0.52     c3_2 $_112 $_114 \/ c4_1 $_113 \/ c4_2 $_112 $_114 \/ c4_2 $_112 a534 \/
% 0.18/0.52     c5_0 \/ c5_1 $_113 \/ ssSkC6
% 0.18/0.52  |- c1_1 $_112 \/ c1_1 $_113 \/ c1_2 $_112 a534 \/ c3_1 $_112 \/
% 0.18/0.52     c3_2 $_112 a534 \/ c4_1 $_113 \/ c4_2 $_112 a534 \/ c5_0 \/
% 0.18/0.52     c5_1 $_113 \/ ssSkC6
% 0.18/0.52  |- ~ssSkC5 \/ c1_1 $_117 \/ c1_1 a541 \/ c1_2 a541 a534 \/
% 0.18/0.52     c2_2 a541 a534 \/ c3_1 a541 \/ c3_2 a541 a534 \/ c4_1 $_117 \/ c5_0 \/
% 0.18/0.52     c5_1 $_117 \/ ssSkC6
% 0.18/0.52  |- ~c3_2 $U $V \/ ~c4_0 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_1 $_119 \/
% 0.18/0.52     c1_1 $_120 \/ c1_2 $U $V \/ c1_2 $_119 a535 \/ c3_1 $_119 \/
% 0.18/0.52     c3_2 $_119 a535 \/ c4_1 $_119 \/ c4_1 $_120 \/ c4_2 $U $V \/
% 0.18/0.52     c4_2 $_119 a534 \/ c5_0 \/ c5_1 $U \/ c5_1 $_120 \/ ssSkC6
% 0.18/0.52  |- ~ssSkC5 \/ c1_1 $_122 \/ c1_1 a541 \/ c1_2 a541 $_123 \/
% 0.18/0.52     c2_2 a541 $_123 \/ c3_1 a541 \/ c3_2 a541 $_123 \/ c4_1 $_122 \/
% 0.18/0.52     c4_2 a541 a534 \/ c5_0 \/ c5_1 $_122 \/ ssSkC3
% 0.18/0.52  |- ~ssSkC5 \/ c1_1 $_126 \/ c1_1 a541 \/ c1_2 a541 $_127 \/
% 0.18/0.52     c2_2 a541 $_127 \/ c3_1 a541 \/ c3_2 a541 $_127 \/ c4_1 $_126 \/
% 0.18/0.52     c4_2 a541 a534 \/ c5_0 \/ c5_1 $_126 \/ ssSkC6
% 0.18/0.52  |- ~ssSkC5 \/ c1_1 $_130 \/ c1_1 a541 \/ c1_2 a541 $_131 \/
% 0.18/0.52     c2_2 a541 a534 \/ c3_1 a541 \/ c3_2 a541 $_131 \/ c3_2 a541 a534 \/
% 0.18/0.52     c4_1 $_130 \/ c4_2 a541 $_131 \/ c5_0 \/ c5_1 $_130 \/ ssSkC3
% 0.18/0.52  |- ~ssSkC5 \/ c1_1 $_134 \/ c1_1 a541 \/ c1_2 a541 $_135 \/
% 0.18/0.52     c2_2 a541 a534 \/ c3_1 a541 \/ c3_2 a541 $_135 \/ c3_2 a541 a534 \/
% 0.18/0.52     c4_1 $_134 \/ c4_2 a541 $_135 \/ c5_0 \/ c5_1 $_134 \/ ssSkC6
% 0.18/0.52  |- ~c1_2 $_139 $_141 \/ ~c3_2 $_139 $_140 \/ ~c3_2 $_139 $_142 \/
% 0.18/0.52     ~c5_2 $_139 $_140 \/ ~ndr1_0 \/ ~ndr1_1 $_139 \/ c1_0 \/ c1_1 $_112 \/
% 0.18/0.52     c1_1 $_138 \/ c1_2 $_112 $_114 \/ c2_1 $_138 \/ c2_2 $_139 $_142 \/
% 0.18/0.52     c3_1 $_112 \/ c3_2 $_112 $_114 \/ c4_1 $_138 \/ c4_2 $_112 $_114 \/
% 0.18/0.52     c4_2 $_112 a534 \/ c4_2 $_139 $_140 \/ c4_2 $_139 $_141 \/
% 0.18/0.52     c4_2 $_139 $_142 \/ c5_0 \/ ssSkC6
% 0.18/0.52  |- ~c1_2 $_139 $_141 \/ ~c3_2 $_139 $_140 \/ ~c3_2 $_139 $_142 \/
% 0.18/0.52     ~c5_2 $_139 $_140 \/ ~ndr1_0 \/ ~ndr1_1 $_139 \/ c1_0 \/ c1_1 $_112 \/
% 0.18/0.52     c1_1 $_138 \/ c1_2 $_112 a534 \/ c2_1 $_138 \/ c2_2 $_139 $_142 \/
% 0.18/0.52     c3_1 $_112 \/ c3_2 $_112 a534 \/ c4_1 $_138 \/ c4_2 $_112 a534 \/
% 0.18/0.52     c4_2 $_139 $_140 \/ c4_2 $_139 $_141 \/ c4_2 $_139 $_142 \/ c5_0 \/
% 0.18/0.52     ssSkC6
% 0.18/0.52  |- ~c1_2 $_139 $_141 \/ ~c3_2 $_139 $_140 \/ ~c3_2 $_139 $_142 \/
% 0.18/0.52     ~c5_2 $_139 $_140 \/ ~ndr1_0 \/ ~ndr1_1 $_139 \/ c1_0 \/ c1_1 $_102 \/
% 0.18/0.52     c1_1 $_138 \/ c1_2 $_102 $_104 \/ c2_1 $_138 \/ c2_2 $_139 $_142 \/
% 0.18/0.52     c3_1 $_102 \/ c3_2 $_102 $_104 \/ c4_1 $_138 \/ c4_2 $_102 $_104 \/
% 0.18/0.52     c4_2 $_102 a534 \/ c4_2 $_139 $_140 \/ c4_2 $_139 $_141 \/
% 0.18/0.52     c4_2 $_139 $_142 \/ c5_0 \/ ssSkC3
% 0.18/0.52  |- ~c1_2 $_139 $_141 \/ ~c3_2 $_139 $_140 \/ ~c3_2 $_139 $_142 \/
% 0.18/0.52     ~c5_2 $_139 $_140 \/ ~ndr1_0 \/ ~ndr1_1 $_139 \/ c1_0 \/ c1_1 $_102 \/
% 0.18/0.52     c1_1 $_138 \/ c1_2 $_102 a534 \/ c2_1 $_138 \/ c2_2 $_139 $_142 \/
% 0.18/0.52     c3_1 $_102 \/ c3_2 $_102 a534 \/ c4_1 $_138 \/ c4_2 $_102 a534 \/
% 0.18/0.52     c4_2 $_139 $_140 \/ c4_2 $_139 $_141 \/ c4_2 $_139 $_142 \/ c5_0 \/
% 0.18/0.52     ssSkC3
% 0.18/0.52  |- ~c1_2 $_139 $_141 \/ ~c3_2 $_139 $_140 \/ ~c3_2 $_139 $_142 \/
% 0.18/0.52     ~c5_2 $_139 $_140 \/ ~ndr1_0 \/ ~ndr1_1 $_139 \/ c1_0 \/ c1_1 $_138 \/
% 0.18/0.52     c1_2 a527 $_91 \/ c2_1 $_138 \/ c2_2 $_139 $_142 \/ c3_1 a527 \/
% 0.18/0.52     c3_2 a527 $_91 \/ c4_1 $_138 \/ c4_2 $_139 $_140 \/ c4_2 $_139 $_141 \/
% 0.18/0.52     c4_2 $_139 $_142 \/ c4_2 a527 $_91 \/ c4_2 a527 a534 \/ c5_0 \/ ssSkC2
% 0.18/0.52  |- ~c1_2 $_139 $_141 \/ ~c3_2 $_139 $_140 \/ ~c3_2 $_139 $_142 \/
% 0.18/0.52     ~c5_2 $_139 $_140 \/ ~ndr1_0 \/ ~ndr1_1 $_139 \/ c1_0 \/ c1_1 $_138 \/
% 0.18/0.52     c1_2 a527 a534 \/ c2_1 $_138 \/ c2_2 $_139 $_142 \/ c3_1 a527 \/
% 0.18/0.52     c3_2 a527 a534 \/ c4_1 $_138 \/ c4_2 $_139 $_140 \/ c4_2 $_139 $_141 \/
% 0.18/0.52     c4_2 $_139 $_142 \/ c4_2 a527 a534 \/ c5_0 \/ ssSkC2
% 0.18/0.52  |- ~c1_2 $_139 $_141 \/ ~c3_2 $_139 $_140 \/ ~c3_2 $_139 $_142 \/
% 0.18/0.52     ~c5_2 $_139 $_140 \/ ~ndr1_0 \/ ~ndr1_1 $_139 \/ c1_0 \/ c1_1 $_138 \/
% 0.18/0.52     c1_2 a537 $_86 \/ c2_1 $_138 \/ c2_2 $_139 $_142 \/ c3_1 a537 \/
% 0.18/0.52     c3_2 a537 $_86 \/ c4_1 $_138 \/ c4_2 $_139 $_140 \/ c4_2 $_139 $_141 \/
% 0.18/0.52     c4_2 $_139 $_142 \/ c4_2 a537 $_86 \/ c4_2 a537 a534 \/ c5_0 \/ ssSkC4
% 0.18/0.52  |- ~c1_2 $_139 $_141 \/ ~c3_2 $_139 $_140 \/ ~c3_2 $_139 $_142 \/
% 0.18/0.52     ~c5_2 $_139 $_140 \/ ~ndr1_0 \/ ~ndr1_1 $_139 \/ c1_0 \/ c1_1 $_138 \/
% 0.18/0.52     c1_2 a537 a534 \/ c2_1 $_138 \/ c2_2 $_139 $_142 \/ c3_1 a537 \/
% 0.18/0.52     c3_2 a537 a534 \/ c4_1 $_138 \/ c4_2 $_139 $_140 \/ c4_2 $_139 $_141 \/
% 0.18/0.52     c4_2 $_139 $_142 \/ c4_2 a537 a534 \/ c5_0 \/ ssSkC4
% 0.18/0.52  |- c1_0 \/ c1_1 $_143 \/ c1_1 $_144 \/ c1_2 $_143 $_145 \/
% 0.18/0.52     c1_2 a537 a538 \/ c2_0 \/ c3_1 $_143 \/ c3_2 $_143 $_145 \/
% 0.18/0.52     c4_1 $_143 \/ c4_1 $_144 \/ c4_2 $_143 $_145 \/ c4_2 $_143 a534 \/
% 0.18/0.52     c4_2 a537 a538 \/ c5_0 \/ c5_1 $_144 \/ c5_1 a537 \/ ssSkC4
% 0.18/0.52  |- c1_0 \/ c1_1 $_143 \/ c1_1 $_144 \/ c1_2 $_143 a534 \/ c1_2 a537 a538 \/
% 0.18/0.52     c2_0 \/ c3_1 $_143 \/ c3_2 $_143 a534 \/ c4_1 $_143 \/ c4_1 $_144 \/
% 0.18/0.52     c4_2 $_143 a534 \/ c4_2 a537 a538 \/ c5_0 \/ c5_1 $_144 \/ c5_1 a537 \/
% 0.18/0.52     ssSkC4
% 0.18/0.52  |- ~ndr1_1 a541 \/ ~ssSkC5 \/ c1_0 \/ c1_1 $_147 \/ c1_1 a541 \/
% 0.18/0.52     c1_2 a537 a538 \/ c1_2 a541 a534 \/ c2_0 \/ c2_2 a541 a534 \/
% 0.18/0.52     c3_1 a541 \/ c3_2 a541 a534 \/ c4_1 $_147 \/ c4_1 a541 \/
% 0.18/0.52     c4_2 a537 a538 \/ c5_0 \/ c5_1 $_147 \/ c5_1 a537 \/ ssSkC4
% 0.18/0.52  |- ~c1_2 $V $X \/ ~c3_2 $V $W \/ ~c3_2 $V $Y \/ ~c5_2 $V $W \/ ~ndr1_0 \/
% 0.18/0.52     ~ndr1_1 $V \/ c1_0 \/ c1_1 $_146 \/ c1_1 $_147 \/ c1_2 $_146 a534 \/
% 0.18/0.52     c1_2 a537 a538 \/ c2_0 \/ c2_1 $_147 \/ c2_2 $V $Y \/ c3_1 $_146 \/
% 0.18/0.52     c3_2 $_146 a534 \/ c4_1 $_146 \/ c4_1 $_147 \/ c4_2 $V $W \/
% 0.18/0.52     c4_2 $V $X \/ c4_2 $V $Y \/ c4_2 $_146 a534 \/ c4_2 a537 a538 \/ c5_0 \/
% 0.18/0.52     c5_1 a537 \/ ssSkC4
% 0.18/0.52  |- ~ndr1_1 a541 \/ ~ssSkC5 \/ c1_0 \/ c1_1 $_150 \/ c1_1 a541 \/
% 0.18/0.52     c1_2 a537 a538 \/ c1_2 a541 $_151 \/ c2_0 \/ c2_2 a541 $_151 \/
% 0.18/0.52     c3_1 a541 \/ c3_2 a541 $_151 \/ c4_1 $_150 \/ c4_1 a541 \/
% 0.18/0.52     c4_2 a537 a538 \/ c4_2 a541 a534 \/ c5_0 \/ c5_1 $_150 \/ c5_1 a537 \/
% 0.18/0.52     ssSkC4
% 0.18/0.52  |- ~ndr1_1 a541 \/ ~ssSkC5 \/ c1_0 \/ c1_1 $_150 \/ c1_1 a541 \/
% 0.18/0.52     c1_2 a537 a538 \/ c1_2 a541 $_151 \/ c2_0 \/ c2_2 a541 a534 \/
% 0.18/0.52     c3_1 a541 \/ c3_2 a541 $_151 \/ c3_2 a541 a534 \/ c4_1 $_150 \/
% 0.18/0.52     c4_1 a541 \/ c4_2 a537 a538 \/ c4_2 a541 $_151 \/ c5_0 \/ c5_1 $_150 \/
% 0.18/0.52     c5_1 a537 \/ ssSkC4
% 0.18/0.52  |- ~c1_2 $V $X \/ ~c3_2 $V $W \/ ~c3_2 $V $Y \/ ~c5_2 $V $W \/ ~ndr1_0 \/
% 0.18/0.52     ~ndr1_1 $V \/ c1_0 \/ c1_1 $_149 \/ c1_1 $_150 \/ c1_2 $_149 $_151 \/
% 0.18/0.52     c1_2 a537 a538 \/ c2_0 \/ c2_1 $_150 \/ c2_2 $V $Y \/ c3_1 $_149 \/
% 0.18/0.52     c3_2 $_149 $_151 \/ c4_1 $_149 \/ c4_1 $_150 \/ c4_2 $V $W \/
% 0.18/0.52     c4_2 $V $X \/ c4_2 $V $Y \/ c4_2 $_149 $_151 \/ c4_2 $_149 a534 \/
% 0.18/0.52     c4_2 a537 a538 \/ c5_0 \/ c5_1 a537 \/ ssSkC4
% 0.18/0.52  |- ~c4_0 \/ c1_1 $_170 \/ c1_1 a537 \/ c1_2 a537 a535 \/ c1_2 a537 a538 \/
% 0.18/0.52     c3_1 a537 \/ c3_2 a537 a535 \/ c4_1 $_170 \/ c4_1 a537 \/
% 0.18/0.52     c4_2 a537 a534 \/ c4_2 a537 a538 \/ c5_0 \/ c5_1 $_170 \/ c5_1 a537 \/
% 0.18/0.52     ssSkC4
% 0.18/0.52  |- ~c4_0 \/ c1_1 $_177 \/ c1_1 a527 \/ c1_2 a527 a535 \/ c1_2 a537 a538 \/
% 0.18/0.52     c3_1 a527 \/ c3_2 a527 a535 \/ c4_1 $_177 \/ c4_1 a527 \/
% 0.18/0.52     c4_2 a527 a534 \/ c4_2 a537 a538 \/ c5_0 \/ c5_1 $_177 \/ c5_1 a537 \/
% 0.18/0.52     ssSkC2 \/ ssSkC4
% 0.18/0.52  |- c1_0 \/ c1_1 $_185 \/ c1_1 $_186 \/ c1_1 $_187 \/ c1_2 $_185 a535 \/
% 0.18/0.52     c1_2 $_187 a543 \/ c2_0 \/ c3_1 $_185 \/ c3_2 $_185 a535 \/
% 0.18/0.52     c4_1 $_185 \/ c4_1 $_186 \/ c4_2 $_185 a534 \/ c4_2 $_187 a543 \/
% 0.18/0.52     c5_0 \/ c5_1 $_186 \/ c5_1 $_187 \/ ssSkC6
% 0.18/0.52  |- ~c1_2 $V $X \/ ~c3_2 $V $W \/ ~c3_2 $V $Y \/ ~c5_2 $V $W \/ ~ndr1_0 \/
% 0.18/0.52     ~ndr1_1 $V \/ c1_0 \/ c1_1 $_188 \/ c1_1 $_189 \/ c1_1 $_190 \/
% 0.18/0.52     c1_2 $_188 a535 \/ c1_2 $_190 a543 \/ c2_0 \/ c2_1 $_189 \/
% 0.18/0.52     c2_2 $V $Y \/ c3_1 $_188 \/ c3_2 $_188 a535 \/ c4_1 $_188 \/
% 0.18/0.52     c4_1 $_189 \/ c4_2 $V $W \/ c4_2 $V $X \/ c4_2 $V $Y \/
% 0.18/0.52     c4_2 $_188 a534 \/ c4_2 $_190 a543 \/ c5_0 \/ c5_1 $_190 \/ ssSkC6
% 0.18/0.52  |- ~ssSkC5 \/ c1_0 \/ c1_1 $_191 \/ c1_1 $_192 \/ c1_1 a541 \/
% 0.18/0.52     c1_2 $_192 a543 \/ c1_2 a541 a535 \/ c2_0 \/ c2_2 a541 a534 \/
% 0.18/0.52     c3_1 a541 \/ c3_2 a541 a534 \/ c3_2 a541 a535 \/ c4_1 $_191 \/
% 0.18/0.52     c4_1 a541 \/ c4_2 $_192 a543 \/ c5_0 \/ c5_1 $_191 \/ c5_1 $_192 \/
% 0.18/0.52     ssSkC6
% 0.18/0.52  |- ~c4_0 \/ c1_1 $_201 \/ c1_1 $_202 \/ c1_2 $_201 a535 \/
% 0.18/0.52     c1_2 a537 a538 \/ c3_1 $_201 \/ c3_2 $_201 a535 \/ c4_1 $_201 \/
% 0.18/0.52     c4_1 $_202 \/ c4_2 $_201 a534 \/ c4_2 a537 a538 \/ c5_0 \/ c5_1 $_202 \/
% 0.18/0.52     c5_1 a537 \/ ssSkC3 \/ ssSkC4
% 0.18/0.52  |- ~ssSkC5 \/ c1_0 \/ c1_1 $_207 \/ c1_1 a541 \/ c1_2 a537 a538 \/
% 0.18/0.52     c1_2 a541 a535 \/ c2_0 \/ c2_2 a541 a534 \/ c3_1 a541 \/
% 0.18/0.52     c3_2 a541 a534 \/ c3_2 a541 a535 \/ c4_1 $_207 \/ c4_1 a541 \/
% 0.18/0.52     c4_2 a537 a538 \/ c5_0 \/ c5_1 $_207 \/ c5_1 a537 \/ ssSkC3 \/ ssSkC4
% 0.18/0.52  |- ~c4_0 \/ c1_1 $_215 \/ c1_1 $_216 \/ c1_2 $_215 a535 \/
% 0.18/0.52     c1_2 a537 a538 \/ c3_1 $_215 \/ c3_2 $_215 a535 \/ c4_1 $_215 \/
% 0.18/0.52     c4_1 $_216 \/ c4_2 $_215 a534 \/ c4_2 a537 a538 \/ c5_0 \/ c5_1 $_216 \/
% 0.18/0.52     c5_1 a537 \/ ssSkC4 \/ ssSkC6
% 0.18/0.52  |- ~ssSkC5 \/ c1_0 \/ c1_1 $_221 \/ c1_1 a541 \/ c1_2 a537 a538 \/
% 0.18/0.52     c1_2 a541 a535 \/ c2_0 \/ c2_2 a541 a534 \/ c3_1 a541 \/
% 0.18/0.52     c3_2 a541 a534 \/ c3_2 a541 a535 \/ c4_1 $_221 \/ c4_1 a541 \/
% 0.18/0.52     c4_2 a537 a538 \/ c5_0 \/ c5_1 $_221 \/ c5_1 a537 \/ ssSkC4 \/ ssSkC6
% 0.18/0.52  |- c1_0 \/ c1_1 $_241 \/ c1_1 $_242 \/ c1_2 $_241 a535 \/ c1_2 a537 a538 \/
% 0.18/0.52     c2_0 \/ c3_1 $_241 \/ c3_2 $_241 a535 \/ c4_1 $_241 \/ c4_1 $_242 \/
% 0.18/0.52     c4_2 $_241 a534 \/ c4_2 a537 a538 \/ c5_0 \/ c5_1 $_242 \/ c5_1 a537 \/
% 0.18/0.52     ssSkC4
% 0.18/0.52  |- ~ndr1_1 a541 \/ ~ssSkC5 \/ c1_0 \/ c1_1 $_244 \/ c1_1 a541 \/
% 0.18/0.52     c1_2 a537 a538 \/ c1_2 a541 a535 \/ c2_0 \/ c2_2 a541 a534 \/
% 0.18/0.52     c3_1 a541 \/ c3_2 a541 a534 \/ c3_2 a541 a535 \/ c4_1 $_244 \/
% 0.18/0.52     c4_1 a541 \/ c4_2 a537 a538 \/ c5_0 \/ c5_1 $_244 \/ c5_1 a537 \/ ssSkC4
% 0.18/0.52  |- ~c1_2 $V $X \/ ~c3_2 $V $W \/ ~c3_2 $V $Y \/ ~c5_2 $V $W \/ ~ndr1_0 \/
% 0.18/0.52     ~ndr1_1 $V \/ c1_0 \/ c1_1 $_243 \/ c1_1 $_244 \/ c1_2 $_243 a535 \/
% 0.18/0.52     c1_2 a537 a538 \/ c2_0 \/ c2_1 $_244 \/ c2_2 $V $Y \/ c3_1 $_243 \/
% 0.18/0.52     c3_2 $_243 a535 \/ c4_1 $_243 \/ c4_1 $_244 \/ c4_2 $V $W \/
% 0.18/0.52     c4_2 $V $X \/ c4_2 $V $Y \/ c4_2 $_243 a534 \/ c4_2 a537 a538 \/ c5_0 \/
% 0.18/0.52     c5_1 a537 \/ ssSkC4
% 0.18/0.52  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.52  
%------------------------------------------------------------------------------