↑ Up

Metis---2.4.SAT-Sat.s

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

% Computer : n017.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:39 EDT 2022

% Result   : Satisfiable 0.12s 0.39s
% Output   : Saturation 0.12s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11  % Problem  : SYN526-1 : TPTP v8.1.0. Released v2.1.0.
% 0.11/0.12  % Command  : metis --show proof --show saturation %s
% 0.12/0.33  % Computer : n017.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 : Mon Jul 11 23:43:19 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 0.12/0.33  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.12/0.39  % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.39  
% 0.12/0.39  SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.39  |- c3_0 \/ ndr1_0
% 0.12/0.39  |- ~c2_0
% 0.12/0.39  |- ndr1_0 \/ ssSkC8
% 0.12/0.39  |- ndr1_0 \/ ssSkC7
% 0.12/0.39  |- ndr1_0 \/ ssSkC4
% 0.12/0.39  |- ndr1_0 \/ ssSkC0
% 0.12/0.39  |- c3_0 \/ ndr1_1 a248
% 0.12/0.39  |- c3_0 \/ c3_1 a248
% 0.12/0.39  |- ~ssSkC8 \/ ~ssSkC9 \/ ndr1_0
% 0.12/0.39  |- ~ssSkC5 \/ ~ssSkC6 \/ ndr1_0
% 0.12/0.39  |- c4_0 \/ c5_0 \/ ndr1_0
% 0.12/0.39  |- ~c3_0 \/ c5_0
% 0.12/0.39  |- c3_1 a236 \/ ssSkC4
% 0.12/0.39  |- ndr1_1 $U \/ ssSkP0 $U
% 0.12/0.39  |- ndr1_1 a223 \/ ssSkC0
% 0.12/0.39  |- c2_1 a223 \/ ssSkC0
% 0.12/0.39  |- c5_1 a223 \/ ssSkC0
% 0.12/0.39  |- c3_0 \/ c4_2 a248 a249
% 0.12/0.39  |- c2_2 a248 a249 \/ c3_0
% 0.12/0.39  |- ~ssSkC5 \/ ~ssSkC6 \/ ndr1_1 a240
% 0.12/0.40  |- ~ssSkC5 \/ ~ssSkC6 \/ c3_1 a240
% 0.12/0.40  |- c4_0 \/ c5_0 \/ ndr1_1 a221
% 0.12/0.40  |- ~c5_1 a245 \/ ssSkC8
% 0.12/0.40  |- ~c3_1 a242 \/ ssSkC7
% 0.12/0.40  |- ~c2_1 a242 \/ ssSkC7
% 0.12/0.40  |- ~c4_1 a242 \/ ssSkC7
% 0.12/0.40  |- ~c4_1 a236 \/ ssSkC4
% 0.12/0.40  |- c4_2 $U a227 \/ ssSkP0 $U
% 0.12/0.40  |- c1_2 $U a227 \/ ssSkP0 $U
% 0.12/0.40  |- c4_2 a223 a224 \/ ssSkC0
% 0.12/0.40  |- c2_2 a223 a224 \/ ssSkC0
% 0.12/0.40  |- ~c1_2 a248 a249 \/ c3_0
% 0.12/0.40  |- ~c3_1 a247 \/ ~ssSkC8 \/ ~ssSkC9
% 0.12/0.40  |- ~ssSkC5 \/ ~ssSkC6 \/ c3_2 a240 a241
% 0.12/0.40  |- ~c2_1 a240 \/ ~ssSkC5 \/ ~ssSkC6
% 0.12/0.40  |- ~c3_0 \/ ~ssSkC4 \/ c2_1 a237
% 0.12/0.40  |- ~c5_0 \/ ~ssSkC0 \/ ndr1_1 a225
% 0.12/0.40  |- ~c5_0 \/ ~ssSkC0 \/ c4_1 a225
% 0.12/0.40  |- c1_2 a221 a222 \/ c4_0 \/ c5_0
% 0.12/0.40  |- ~c5_2 $U a227 \/ ssSkP0 $U
% 0.12/0.40  |- ~c5_2 a223 a224 \/ ssSkC0
% 0.12/0.40  |- ~c5_2 a240 a241 \/ ~ssSkC5 \/ ~ssSkC6
% 0.12/0.40  |- ~c1_2 a240 a241 \/ ~ssSkC5 \/ ~ssSkC6
% 0.12/0.40  |- ~c4_1 a232 \/ ~c5_0 \/ c3_0
% 0.12/0.40  |- ~c3_1 a232 \/ ~c5_0 \/ c3_0
% 0.12/0.40  |- ~c3_0 \/ ~c4_1 a229 \/ ~ssSkC1
% 0.12/0.40  |- ~c5_0 \/ ~ssSkC0 \/ c1_2 a225 a226
% 0.12/0.40  |- ~c5_2 a221 a222 \/ c4_0 \/ c5_0
% 0.12/0.40  |- ~c1_0 \/ ~c3_0 \/ ~c5_0
% 0.12/0.40  |- ~ndr1_0 \/ ~ssSkC2 \/ ~ssSkC3 \/ c5_1 $U \/ ndr1_1 $U
% 0.12/0.40  |- ~c3_2 a225 a226 \/ ~c5_0 \/ ~ssSkC0
% 0.12/0.40  |- ~c2_1 $U \/ ~ndr1_0 \/ ndr1_1 $U \/ ssSkC5
% 0.12/0.40  |- ~c4_0 \/ ~ndr1_0 \/ ~ssSkC7 \/ c4_1 $U \/ ndr1_1 $U
% 0.12/0.40  |- ~ndr1_0 \/ ~ssSkC2 \/ ~ssSkC3 \/ c4_2 $U a235 \/ c5_1 $U
% 0.12/0.40  |- ~ndr1_0 \/ ~ssSkC2 \/ ~ssSkC3 \/ c1_2 $U a235 \/ c5_1 $U
% 0.12/0.40  |- ~ndr1_0 \/ c1_1 $U \/ c3_1 $U \/ ndr1_1 $U \/ ssSkC9
% 0.12/0.40  |- ~c2_1 $U \/ ~ndr1_0 \/ c3_2 $U a238 \/ ssSkC5
% 0.12/0.40  |- ~c2_1 $U \/ ~ndr1_0 \/ c1_2 $U a238 \/ ssSkC5
% 0.12/0.40  |- ~c4_0 \/ ~ndr1_0 \/ ~ssSkC7 \/ c1_2 $U a243 \/ c4_1 $U
% 0.12/0.40  |- ~c5_2 $U a235 \/ ~ndr1_0 \/ ~ssSkC2 \/ ~ssSkC3 \/ c5_1 $U
% 0.12/0.40  |- ~c2_1 $U \/ ~ndr1_0 \/ c4_1 $U \/ ndr1_1 $U \/ ssSkC2
% 0.12/0.40  |- ~ndr1_0 \/ ~ssSkP0 $U \/ c1_2 $U a228 \/ c5_1 $U \/ ssSkC1
% 0.12/0.40  |- ~c2_1 $U \/ ~ndr1_0 \/ c4_0 \/ c4_1 $U \/ c5_0 \/ ndr1_1 $U
% 0.12/0.40  |- ~c2_1 $U \/ ~c2_2 $U a238 \/ ~ndr1_0 \/ ssSkC5
% 0.12/0.40  |- ~c4_0 \/ ~c5_2 $U a243 \/ ~ndr1_0 \/ ~ssSkC7 \/ c4_1 $U
% 0.12/0.40  |- ~c2_1 $U \/ ~c4_0 \/ ~ndr1_0 \/ c5_1 $U \/ ndr1_1 a230
% 0.12/0.40  |- ~c2_1 $U \/ ~c4_0 \/ ~ndr1_0 \/ c2_1 a230 \/ c5_1 $U
% 0.12/0.40  |- ~c2_1 $U \/ ~c4_0 \/ ~ndr1_0 \/ c3_1 a230 \/ c5_1 $U
% 0.12/0.40  |- ~c1_2 $U a246 \/ ~ndr1_0 \/ c1_1 $U \/ c3_1 $U \/ ssSkC9
% 0.12/0.40  |- ~c2_2 $U a246 \/ ~ndr1_0 \/ c1_1 $U \/ c3_1 $U \/ ssSkC9
% 0.12/0.40  |- ~c3_2 $U a246 \/ ~ndr1_0 \/ c1_1 $U \/ c3_1 $U \/ ssSkC9
% 0.12/0.40  |- ~c3_1 $U \/ ~c4_1 $U \/ ~ndr1_0 \/ ndr1_1 $U \/ ssSkC6
% 0.12/0.40  |- ~c2_1 $U \/ ~ndr1_0 \/ c3_2 $U a233 \/ c4_1 $U \/ ssSkC2
% 0.12/0.40  |- ~c2_1 $U \/ ~ndr1_0 \/ c2_2 $U a233 \/ c4_1 $U \/ ssSkC2
% 0.12/0.40  |- ~c2_2 $U a228 \/ ~ndr1_0 \/ ~ssSkP0 $U \/ c5_1 $U \/ ssSkC1
% 0.12/0.40  |- ~c1_0 \/ ~c4_0 \/ ~ndr1_0 \/ c2_1 $U \/ c3_1 $U \/ c4_1 $U
% 0.12/0.40  |- ~c3_2 a245 $U \/ ~ndr1_1 a245 \/ c5_2 a245 $U \/ ssSkC8
% 0.12/0.40  |- ~c3_2 a247 $U \/ ~ndr1_1 a247 \/ ~ssSkC8 \/ ~ssSkC9 \/ c1_2 a247 $U
% 0.12/0.40  |- ~c3_1 $U \/ ~c4_1 $U \/ ~ndr1_0 \/ c2_2 $U a239 \/ ssSkC6
% 0.12/0.40  |- ~c2_1 $U \/ ~c5_2 $U a233 \/ ~ndr1_0 \/ c4_1 $U \/ ssSkC2
% 0.12/0.40  |- ~c1_2 $U a219 \/ ~c2_1 $U \/ ~ndr1_0 \/ c4_0 \/ c4_1 $U \/ c5_0
% 0.12/0.40  |- ~c2_1 $U \/ ~c2_2 $U a219 \/ ~ndr1_0 \/ c4_0 \/ c4_1 $U \/ c5_0
% 0.12/0.40  |- ~c2_1 $U \/ ~c3_2 $U a219 \/ ~ndr1_0 \/ c4_0 \/ c4_1 $U \/ c5_0
% 0.12/0.40  |- ~c3_0 \/ ~c5_2 a237 $U \/ ~ndr1_1 a237 \/ ~ssSkC4 \/ c4_2 a237 $U
% 0.12/0.40  |- ~c1_2 a230 a231 \/ ~c2_1 $U \/ ~c4_0 \/ ~ndr1_0 \/ c5_1 $U
% 0.12/0.40  |- ~c2_1 $U \/ ~c4_0 \/ ~c5_2 a230 a231 \/ ~ndr1_0 \/ c5_1 $U
% 0.12/0.40  |- ~c3_1 $U \/ ~c4_1 $U \/ ~c5_2 $U a239 \/ ~ndr1_0 \/ ssSkC6
% 0.12/0.40  |- ~c3_1 $U \/ ~c4_1 $U \/ ~c4_2 $U a239 \/ ~ndr1_0 \/ ssSkC6
% 0.12/0.40  |- ~c4_2 a245 $U \/ ~ndr1_1 a245 \/ c1_2 a245 $U \/ c5_2 a245 $U \/ ssSkC8
% 0.12/0.40  |- ~c4_2 a236 $U \/ ~ndr1_1 a236 \/ c3_2 a236 $U \/ c5_2 a236 $U \/ ssSkC4
% 0.12/0.40  |- ~c1_2 a229 $U \/ ~c3_0 \/ ~ndr1_1 a229 \/ ~ssSkC1 \/ c4_2 a229 $U \/
% 0.12/0.40     c5_2 a229 $U
% 0.12/0.40  |- ~c1_2 a221 $U \/ ~c2_2 a221 $U \/ ~ndr1_1 a221 \/ c4_0 \/ c5_0 \/
% 0.12/0.40     c5_2 a221 $U
% 0.12/0.40  |- ~c2_2 a237 $U \/ ~c3_0 \/ ~c3_2 a237 $U \/ ~ndr1_1 a237 \/ ~ssSkC4 \/
% 0.12/0.40     c5_2 a237 $U
% 0.12/0.40  |- ~c3_0 \/ ~c3_2 a229 $U \/ ~c4_2 a229 $U \/ ~c5_2 a229 $U \/
% 0.12/0.40     ~ndr1_1 a229 \/ ~ssSkC1
% 0.12/0.40  |- ~c5_0 \/ ~c5_1 $U \/ ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.12/0.40     c3_2 $U $V \/ c4_2 $U $V \/ c5_2 $U a244
% 0.12/0.40  |- ~c5_0 \/ ~c5_1 $U \/ ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.12/0.40     c2_2 $U a244 \/ c3_2 $U $V \/ c4_2 $U $V
% 0.12/0.40  |- ~c3_2 $U a244 \/ ~c5_0 \/ ~c5_1 $U \/ ~c5_2 $U $V \/ ~ndr1_0 \/
% 0.12/0.40     ~ndr1_1 $U \/ c3_2 $U $V \/ c4_2 $U $V
% 0.12/0.40  |- ~c1_1 $U \/ ~c1_2 $U $V \/ ~c3_2 $U $V \/ ~c5_0 \/ ~ndr1_0 \/
% 0.12/0.40     ~ndr1_1 $U \/ c1_1 $W \/ c3_1 $U \/ ndr1_1 $W
% 0.12/0.40  |- ~c1_1 $U \/ ~c2_2 $U $V \/ ~c4_2 $U $V \/ ~c5_2 $U $V \/ ~ndr1_0 \/
% 0.12/0.40     ~ndr1_1 $U \/ c4_2 $U a234 \/ ssSkC3
% 0.12/0.40  |- ~c1_1 $U \/ ~c1_2 $U $V \/ ~c3_2 $U $V \/ ~c5_0 \/ ~ndr1_0 \/
% 0.12/0.40     ~ndr1_1 $U \/ c1_1 $W \/ c3_1 $U \/ c5_2 $W a218
% 0.12/0.40  |- ~c1_1 $U \/ ~c1_2 $U $V \/ ~c3_2 $U $V \/ ~c5_0 \/ ~ndr1_0 \/
% 0.12/0.40     ~ndr1_1 $U \/ c1_1 $W \/ c1_2 $W a218 \/ c3_1 $U
% 0.12/0.40  |- ~c1_1 $U \/ ~c2_2 $U $V \/ ~c4_2 $U $V \/ ~c5_2 $U $V \/
% 0.12/0.40     ~c5_2 $U a234 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ ssSkC3
% 0.12/0.40  |- ~c1_1 $U \/ ~c1_2 $U $V \/ ~c3_2 $U $V \/ ~c3_2 $W a218 \/ ~c5_0 \/
% 0.12/0.40     ~ndr1_0 \/ ~ndr1_1 $U \/ c1_1 $W \/ c3_1 $U
% 0.12/0.40  |- ~c1_2 $U $V \/ ~c2_1 $U \/ ~c3_1 $W \/ ~c4_2 $U $V \/ ~c5_2 $U $V \/
% 0.12/0.40     ~ndr1_0 \/ ~ndr1_1 $U \/ c4_1 $W \/ c5_1 $U \/ ndr1_1 $W
% 0.12/0.40  |- ~c1_2 $U $V \/ ~c2_1 $U \/ ~c3_1 $W \/ ~c4_2 $U $V \/ ~c5_2 $U $V \/
% 0.12/0.40     ~ndr1_0 \/ ~ndr1_1 $U \/ c4_1 $W \/ c4_2 $W a250 \/ c5_1 $U
% 0.12/0.40  |- ~c1_2 $U $V \/ ~c2_1 $U \/ ~c3_1 $W \/ ~c4_2 $U $V \/ ~c5_2 $U $V \/
% 0.12/0.40     ~c5_2 $W a250 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c4_1 $W \/ c5_1 $U
% 0.12/0.40  |- ~c1_2 $U $V \/ ~c2_1 $W \/ ~c2_2 $W $X \/ ~c4_0 \/ ~c5_2 $U $V \/
% 0.12/0.40     ~ndr1_0 \/ ~ndr1_1 $U \/ ~ndr1_1 $W \/ c1_2 $W a220 \/ c2_1 $U \/
% 0.12/0.40     c2_2 $U $V \/ c3_2 $W $X \/ c4_2 $W $X \/ c5_1 $U
% 0.12/0.40  |- ~c1_2 $U $V \/ ~c2_1 $W \/ ~c2_2 $W $X \/ ~c4_0 \/ ~c5_2 $U $V \/
% 0.12/0.40     ~ndr1_0 \/ ~ndr1_1 $U \/ ~ndr1_1 $W \/ c2_1 $U \/ c2_2 $U $V \/
% 0.12/0.40     c3_2 $W $X \/ c4_2 $W $X \/ c4_2 $W a220 \/ c5_1 $U
% 0.12/0.40  |- ~c1_2 $U $V \/ ~c2_1 $W \/ ~c2_2 $W $X \/ ~c3_2 $W a220 \/ ~c4_0 \/
% 0.12/0.40     ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ ~ndr1_1 $W \/ c2_1 $U \/
% 0.12/0.40     c2_2 $U $V \/ c3_2 $W $X \/ c4_2 $W $X \/ c5_1 $U
% 0.12/0.40  |- ~c1_1 $U \/ ~c2_2 $U a234 \/ ~c4_2 $U a234 \/ ~c5_2 $U a234 \/
% 0.12/0.40     ~ndr1_0 \/ ~ndr1_1 $U \/ ssSkC3
% 0.12/0.40  |- ~c1_2 $W a250 \/ ~c2_1 $W \/ ~c3_1 $W \/ ~c4_2 $W a250 \/
% 0.12/0.40     ~c5_2 $W a250 \/ ~ndr1_0 \/ ~ndr1_1 $W \/ c4_1 $W \/ c5_1 $W
% 0.12/0.40  |- ~c3_0 \/ ndr1_0
% 0.12/0.40  |- ~c5_0 \/ ndr1_0
% 0.12/0.40  |- ~ndr1_0 \/ c3_2 a223 a238 \/ ssSkC0 \/ ssSkC5
% 0.12/0.40  |- c3_2 a223 a238 \/ c4_0 \/ c5_0 \/ ssSkC0 \/ ssSkC5
% 0.12/0.40  |- c3_0 \/ c3_2 a223 a238 \/ ssSkC0 \/ ssSkC5
% 0.12/0.40  |- ~ndr1_0 \/ c1_2 a223 a238 \/ ssSkC0 \/ ssSkC5
% 0.12/0.40  |- c1_2 a223 a238 \/ c4_0 \/ c5_0 \/ ssSkC0 \/ ssSkC5
% 0.12/0.41  |- c1_2 a223 a238 \/ c3_0 \/ ssSkC0 \/ ssSkC5
% 0.12/0.41  |- c1_1 $_13 \/ c3_1 $_13 \/ c4_0 \/ c5_0 \/ ndr1_1 $_13 \/ ssSkC9
% 0.12/0.41  |- c1_1 $_13 \/ c3_0 \/ c3_1 $_13 \/ ndr1_1 $_13 \/ ssSkC9
% 0.12/0.41  |- ~ndr1_0 \/ c5_1 $_14 \/ ndr1_1 $_14 \/ ssSkC1
% 0.12/0.41  |- c4_0 \/ c5_0 \/ c5_1 $_15 \/ ndr1_1 $_15 \/ ssSkC1
% 0.12/0.41  |- c3_0 \/ c5_1 $_15 \/ ndr1_1 $_15 \/ ssSkC1
% 0.12/0.41  |- ~ndr1_0 \/ c3_2 a223 a233 \/ c4_1 a223 \/ ssSkC0 \/ ssSkC2
% 0.12/0.41  |- c3_2 a223 a233 \/ c4_0 \/ c4_1 a223 \/ c5_0 \/ ssSkC0 \/ ssSkC2
% 0.12/0.41  |- c3_0 \/ c3_2 a223 a233 \/ c4_1 a223 \/ ssSkC0 \/ ssSkC2
% 0.12/0.41  |- ~ndr1_0 \/ c2_2 a223 a233 \/ c4_1 a223 \/ ssSkC0 \/ ssSkC2
% 0.12/0.41  |- c2_2 a223 a233 \/ c4_0 \/ c4_1 a223 \/ c5_0 \/ ssSkC0 \/ ssSkC2
% 0.12/0.41  |- c2_2 a223 a233 \/ c3_0 \/ c4_1 a223 \/ ssSkC0 \/ ssSkC2
% 0.12/0.41  |- ~c1_0 \/ ~c4_0 \/ c2_1 $_43 \/ c3_0 \/ c3_1 $_43 \/ c4_1 $_43
% 0.12/0.41  |- ~ndr1_1 a236 \/ c3_2 a236 a227 \/ c5_2 a236 a227 \/ ssSkC4 \/
% 0.12/0.41     ssSkP0 a236
% 0.12/0.41  |- c3_0 \/ c3_2 a236 a227 \/ c5_1 a236 \/ ssSkC1 \/ ssSkC4 \/ ssSkP0 a236
% 0.12/0.41  |- c3_2 a236 a227 \/ c4_0 \/ c5_0 \/ c5_1 a236 \/ ssSkC1 \/ ssSkC4 \/
% 0.12/0.41     ssSkP0 a236
% 0.12/0.41  |- ~c1_1 a223 \/ ~c1_2 a223 a233 \/ ~c5_0 \/ ~ndr1_0 \/ ~ndr1_1 a223 \/
% 0.12/0.41     c1_1 $_69 \/ c3_0 \/ c3_1 a223 \/ c4_1 a223 \/ ndr1_1 $_69 \/ ssSkC0 \/
% 0.12/0.41     ssSkC2
% 0.12/0.41  |- ~c1_1 a223 \/ ~c5_0 \/ ~ndr1_0 \/ c1_1 $_71 \/ c3_0 \/ c3_1 a223 \/
% 0.12/0.41     ndr1_1 $_71 \/ ssSkC0 \/ ssSkC5
% 0.12/0.41  |- ~c1_1 a223 \/ ~c1_2 a223 a233 \/ ~c5_0 \/ ~ndr1_0 \/ ~ndr1_1 a223 \/
% 0.12/0.41     c1_1 $_76 \/ c3_0 \/ c3_1 a223 \/ c4_1 a223 \/ c5_2 $_76 a218 \/
% 0.12/0.41     ssSkC0 \/ ssSkC2
% 0.12/0.41  |- ~c1_1 a223 \/ ~c5_0 \/ ~ndr1_0 \/ c1_1 $_78 \/ c3_0 \/ c3_1 a223 \/
% 0.12/0.41     c5_2 $_78 a218 \/ ssSkC0 \/ ssSkC5
% 0.12/0.41  |- ~c1_1 a223 \/ ~c1_2 a223 a233 \/ ~c5_0 \/ ~ndr1_0 \/ ~ndr1_1 a223 \/
% 0.12/0.41     c1_1 $_83 \/ c1_2 $_83 a218 \/ c3_0 \/ c3_1 a223 \/ c4_1 a223 \/
% 0.12/0.41     ssSkC0 \/ ssSkC2
% 0.12/0.41  |- ~c1_1 a223 \/ ~c5_0 \/ ~ndr1_0 \/ c1_1 $_85 \/ c1_2 $_85 a218 \/ c3_0 \/
% 0.12/0.41     c3_1 a223 \/ ssSkC0 \/ ssSkC5
% 0.12/0.41  |- ~c1_1 a223 \/ ~c1_2 a223 a233 \/ ~c3_2 $_90 a218 \/ ~c5_0 \/ ~ndr1_0 \/
% 0.12/0.41     ~ndr1_1 a223 \/ c1_1 $_90 \/ c3_0 \/ c3_1 a223 \/ c4_1 a223 \/ ssSkC0 \/
% 0.12/0.41     ssSkC2
% 0.12/0.41  |- ~c1_1 a223 \/ ~c1_2 a223 a238 \/ ~c3_2 $_90 a218 \/ ~c5_0 \/ ~ndr1_0 \/
% 0.12/0.41     ~ndr1_1 a223 \/ c1_1 $_90 \/ c3_0 \/ c3_1 a223 \/ ssSkC0 \/ ssSkC5
% 0.12/0.41  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.41  
%------------------------------------------------------------------------------