↑ Up

Metis---2.4.SAT-Sat.s

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

% Computer : n011.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:41 EDT 2022

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

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : SYN529-1 : TPTP v8.1.0. Released v2.1.0.
% 0.03/0.13  % Command  : metis --show proof --show saturation %s
% 0.13/0.34  % Computer : n011.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 08:19:43 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.13/0.35  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.20/0.46  % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.46  
% 0.20/0.46  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.46  |- c3_0 \/ ndr1_0
% 0.20/0.46  |- ndr1_0 \/ ssSkC8
% 0.20/0.46  |- ndr1_0 \/ ssSkC7
% 0.20/0.46  |- ndr1_0 \/ ssSkC6
% 0.20/0.46  |- ndr1_0 \/ ssSkC5
% 0.20/0.46  |- ndr1_0 \/ ssSkC4
% 0.20/0.46  |- ndr1_0 \/ ssSkC3
% 0.20/0.46  |- ndr1_0 \/ ssSkC2
% 0.20/0.46  |- ndr1_0 \/ ssSkC0
% 0.20/0.46  |- c2_1 a343 \/ c3_0
% 0.20/0.46  |- ~c5_0 \/ c2_0
% 0.20/0.46  |- ~c3_0 \/ c2_0
% 0.20/0.46  |- ndr1_1 a351 \/ ssSkC8
% 0.20/0.46  |- c4_1 a351 \/ ssSkC8
% 0.20/0.46  |- ndr1_1 a348 \/ ssSkC7
% 0.20/0.46  |- ndr1_1 a344 \/ ssSkC6
% 0.20/0.46  |- ndr1_1 $U \/ ssSkP0 $U
% 0.20/0.46  |- ndr1_1 a338 \/ ssSkC5
% 0.20/0.46  |- c1_1 a338 \/ ssSkC5
% 0.20/0.46  |- c4_1 a338 \/ ssSkC5
% 0.20/0.46  |- ndr1_1 a331 \/ ssSkC4
% 0.20/0.46  |- c5_1 a331 \/ ssSkC4
% 0.20/0.46  |- c3_1 a331 \/ ssSkC4
% 0.20/0.46  |- c5_1 a328 \/ ssSkC3
% 0.20/0.46  |- ndr1_1 a324 \/ ssSkC2
% 0.20/0.46  |- ndr1_1 a316 \/ ssSkC0
% 0.20/0.46  |- c1_1 a316 \/ ssSkC0
% 0.20/0.46  |- c2_0 \/ c5_0 \/ ndr1_1 a355
% 0.20/0.46  |- ~ssSkC8 \/ c3_0 \/ ndr1_1 a353
% 0.20/0.46  |- ~ssSkC6 \/ c5_0 \/ ndr1_1 a346
% 0.20/0.46  |- ~ssSkC6 \/ c4_1 a346 \/ c5_0
% 0.20/0.46  |- ~ssSkC6 \/ c3_1 a346 \/ c5_0
% 0.20/0.46  |- ~c1_1 a343 \/ c3_0
% 0.20/0.46  |- c4_0 \/ c5_0 \/ ndr1_1 a335
% 0.20/0.46  |- ~ssSkC3 \/ c4_0 \/ ndr1_1 a329
% 0.20/0.46  |- ~ssSkC3 \/ c1_1 a329 \/ c4_0
% 0.20/0.46  |- ~ssSkC2 \/ c5_0 \/ ndr1_1 a326
% 0.20/0.46  |- ~ssSkC2 \/ c2_1 a326 \/ c5_0
% 0.20/0.47  |- ~ssSkC2 \/ c4_1 a326 \/ c5_0
% 0.20/0.47  |- ~ssSkC1 \/ c4_0 \/ ndr1_1 a322
% 0.20/0.47  |- ~ssSkC1 \/ c3_1 a322 \/ c4_0
% 0.20/0.47  |- ~c1_0 \/ c3_0 \/ c5_0
% 0.20/0.47  |- c2_2 a351 a352 \/ ssSkC8
% 0.20/0.47  |- ~c1_1 a351 \/ ssSkC8
% 0.20/0.47  |- c2_2 a348 a349 \/ ssSkC7
% 0.20/0.47  |- ~c3_1 a348 \/ ssSkC7
% 0.20/0.47  |- c3_2 a344 a345 \/ ssSkC6
% 0.20/0.47  |- ~c2_1 a344 \/ ssSkC6
% 0.20/0.47  |- c2_2 $U a340 \/ ssSkP0 $U
% 0.20/0.47  |- c1_2 a338 a339 \/ ssSkC5
% 0.20/0.47  |- c1_2 a331 a332 \/ ssSkC4
% 0.20/0.47  |- c2_2 a331 a332 \/ ssSkC4
% 0.20/0.47  |- ~c2_1 a328 \/ ssSkC3
% 0.20/0.47  |- c1_2 a324 a325 \/ ssSkC2
% 0.20/0.47  |- c5_2 a324 a325 \/ ssSkC2
% 0.20/0.47  |- c3_2 a316 a317 \/ ssSkC0
% 0.20/0.47  |- c2_2 a316 a317 \/ ssSkC0
% 0.20/0.47  |- ~c4_1 a316 \/ ssSkC0
% 0.20/0.47  |- ~c3_1 a355 \/ c2_0 \/ c5_0
% 0.20/0.47  |- ~ssSkC8 \/ c2_2 a353 a354 \/ c3_0
% 0.20/0.47  |- ~ssSkC8 \/ c3_0 \/ c3_2 a353 a354
% 0.20/0.47  |- ~ssSkC6 \/ c1_2 a346 a347 \/ c5_0
% 0.20/0.47  |- c1_2 a335 a337 \/ c4_0 \/ c5_0
% 0.20/0.47  |- c4_0 \/ c5_0 \/ c5_2 a335 a337
% 0.20/0.47  |- c4_0 \/ c4_2 a335 a336 \/ c5_0
% 0.20/0.47  |- c4_0 \/ c5_0 \/ c5_2 a335 a336
% 0.20/0.47  |- c2_2 a335 a336 \/ c4_0 \/ c5_0
% 0.20/0.47  |- ~ssSkC2 \/ c3_2 a326 a327 \/ c5_0
% 0.20/0.47  |- ~ssSkC1 \/ c4_0 \/ c5_2 a322 a323
% 0.20/0.47  |- ~c4_0 \/ ~ssSkC0 \/ ndr1_1 a318
% 0.20/0.47  |- ~c3_0 \/ ~c5_0 \/ c4_0
% 0.20/0.47  |- ~c1_0 \/ ~c5_0 \/ c4_0
% 0.20/0.47  |- ~c1_2 a351 a352 \/ ssSkC8
% 0.20/0.47  |- ~c4_2 a351 a352 \/ ssSkC8
% 0.20/0.47  |- ~c5_2 a348 a349 \/ ssSkC7
% 0.20/0.47  |- ~c1_2 a344 a345 \/ ssSkC6
% 0.20/0.47  |- ~c4_2 $U a340 \/ ssSkP0 $U
% 0.20/0.47  |- ~c1_2 $U a340 \/ ssSkP0 $U
% 0.20/0.47  |- ~c3_2 a338 a339 \/ ssSkC5
% 0.20/0.47  |- ~c4_2 a338 a339 \/ ssSkC5
% 0.20/0.47  |- ~c5_2 a331 a332 \/ ssSkC4
% 0.20/0.47  |- ~c4_2 a316 a317 \/ ssSkC0
% 0.20/0.47  |- ~c4_2 a355 a356 \/ c2_0 \/ c5_0
% 0.20/0.47  |- ~c5_2 a355 a356 \/ c2_0 \/ c5_0
% 0.20/0.47  |- ~c5_2 a346 a347 \/ ~ssSkC6 \/ c5_0
% 0.20/0.47  |- ~c3_2 a335 a337 \/ c4_0 \/ c5_0
% 0.20/0.47  |- ~c3_1 a333 \/ ~c4_0 \/ ~ssSkC4
% 0.20/0.47  |- ~c2_2 a329 a330 \/ ~ssSkC3 \/ c4_0
% 0.20/0.47  |- ~c2_2 a326 a327 \/ ~ssSkC2 \/ c5_0
% 0.20/0.47  |- ~c5_2 a326 a327 \/ ~ssSkC2 \/ c5_0
% 0.20/0.47  |- ~c4_2 a322 a323 \/ ~ssSkC1 \/ c4_0
% 0.20/0.47  |- ~c1_2 a322 a323 \/ ~ssSkC1 \/ c4_0
% 0.20/0.47  |- ~c4_0 \/ ~ssSkC0 \/ c2_2 a318 a320
% 0.20/0.47  |- ~c4_0 \/ ~ssSkC0 \/ c4_2 a318 a319
% 0.20/0.47  |- ~c4_0 \/ ~ssSkC0 \/ c2_2 a318 a319
% 0.20/0.47  |- ~c2_0 \/ ~c3_0 \/ ~c4_0
% 0.20/0.47  |- ~c4_0 \/ ~c4_2 a318 a320 \/ ~ssSkC0
% 0.20/0.47  |- ~ndr1_0 \/ c1_0 \/ c3_1 $U \/ c5_1 $U \/ ndr1_1 $U
% 0.20/0.47  |- ~c4_1 $U \/ ~ndr1_0 \/ c4_0 \/ c5_1 $U \/ ndr1_1 $U
% 0.20/0.47  |- ~ndr1_0 \/ c1_0 \/ c3_1 $U \/ c4_2 $U a334 \/ c5_1 $U
% 0.20/0.47  |- ~ndr1_0 \/ c1_0 \/ c2_2 $U a334 \/ c3_1 $U \/ c5_1 $U
% 0.20/0.47  |- ~c4_1 $U \/ ~ndr1_0 \/ c4_0 \/ c5_1 $U \/ c5_2 $U a342
% 0.20/0.47  |- ~c4_1 $U \/ ~ndr1_0 \/ c2_2 $U a342 \/ c4_0 \/ c5_1 $U
% 0.20/0.47  |- ~c1_2 a355 $U \/ ~ndr1_1 a355 \/ c2_0 \/ c3_2 a355 $U \/ c5_0
% 0.20/0.47  |- ~c4_2 a324 $U \/ ~ndr1_1 a324 \/ c2_2 a324 $U \/ c3_2 a324 $U \/ ssSkC2
% 0.20/0.47  |- ~c2_2 a348 $U \/ ~c4_2 a348 $U \/ ~ndr1_1 a348 \/ c5_2 a348 $U \/ ssSkC7
% 0.20/0.47  |- ~c2_2 a353 $U \/ ~c5_2 a353 $U \/ ~ndr1_1 a353 \/ ~ssSkC8 \/ c3_0 \/
% 0.20/0.47     c3_2 a353 $U
% 0.20/0.47  |- ~c1_2 a353 $U \/ ~c4_2 a353 $U \/ ~ndr1_1 a353 \/ ~ssSkC8 \/ c3_0 \/
% 0.20/0.47     c3_2 a353 $U
% 0.20/0.47  |- ~c4_2 a329 $U \/ ~c5_2 a329 $U \/ ~ndr1_1 a329 \/ ~ssSkC3 \/
% 0.20/0.47     c1_2 a329 $U \/ c4_0
% 0.20/0.47  |- ~c1_2 a344 $U \/ ~c2_2 a344 $U \/ ~c5_2 a344 $U \/ ~ndr1_1 a344 \/
% 0.20/0.47     ssSkC6
% 0.20/0.47  |- ~c2_1 $U \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c2_2 $U $V \/ c3_1 $U \/
% 0.20/0.47     c3_2 $U $V \/ c4_2 $U $V \/ c5_0
% 0.20/0.47  |- ~c3_1 $U \/ ~c4_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ ~ssSkC7 \/
% 0.20/0.47     c1_2 $U $V \/ c2_2 $U a350 \/ c5_2 $U $V
% 0.20/0.47  |- ~c4_1 $U \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $V \/ c3_2 $U $V \/ c4_0 \/
% 0.20/0.47     c4_2 $U $V \/ c5_1 $U \/ ndr1_1 a314
% 0.20/0.47  |- ~c4_1 $U \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $V \/ c3_2 $U $V \/ c4_0 \/
% 0.20/0.47     c4_1 a314 \/ c4_2 $U $V \/ c5_1 $U
% 0.20/0.47  |- ~c3_1 $U \/ ~c3_2 $U a350 \/ ~c4_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.20/0.47     ~ssSkC7 \/ c1_2 $U $V \/ c5_2 $U $V
% 0.20/0.47  |- ~c1_2 $U a350 \/ ~c3_1 $U \/ ~c4_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.20/0.47     ~ssSkC7 \/ c1_2 $U $V \/ c5_2 $U $V
% 0.20/0.47  |- ~c3_2 $U $V \/ ~c5_0 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ ~ssSkC5 \/
% 0.20/0.47     ~ssSkP0 $U \/ c1_2 $U $V \/ c2_2 $U $V \/ c2_2 $U a341
% 0.20/0.47  |- ~c3_2 $U $V \/ ~c5_0 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ ~ssSkC5 \/
% 0.20/0.47     ~ssSkP0 $U \/ c1_2 $U $V \/ c2_2 $U $V \/ c4_2 $U a341
% 0.20/0.47  |- ~c3_2 $U $V \/ ~c5_0 \/ ~ndr1_0 \/ ~ndr1_1 $U \/ ~ssSkC5 \/
% 0.20/0.47     ~ssSkP0 $U \/ c1_2 $U $V \/ c2_2 $U $V \/ c3_2 $U a341
% 0.20/0.47  |- ~c2_1 $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_1 $X \/ c2_1 $U \/ c4_1 $U \/
% 0.20/0.47     c4_1 $V \/ c4_2 $U $W \/ c5_1 $X \/ c5_2 $U $W
% 0.20/0.47  |- ~c2_1 $U \/ ~c3_2 $U $V \/ ~c4_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.20/0.47     c2_2 $U $V \/ c5_2 $U a321 \/ ssSkC1
% 0.20/0.47  |- ~c3_2 a314 a315 \/ ~c4_1 $U \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $V \/
% 0.20/0.47     c3_2 $U $V \/ c4_0 \/ c4_2 $U $V \/ c5_1 $U
% 0.20/0.47  |- ~c2_2 a314 a315 \/ ~c4_1 $U \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $V \/
% 0.20/0.47     c3_2 $U $V \/ c4_0 \/ c4_2 $U $V \/ c5_1 $U
% 0.20/0.47  |- ~c1_2 a314 a315 \/ ~c4_1 $U \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $V \/
% 0.20/0.47     c3_2 $U $V \/ c4_0 \/ c4_2 $U $V \/ c5_1 $U
% 0.20/0.47  |- ~c1_2 $U a321 \/ ~c2_1 $U \/ ~c3_2 $U $V \/ ~c4_2 $U $V \/ ~ndr1_0 \/
% 0.20/0.47     ~ndr1_1 $U \/ c2_2 $U $V \/ ssSkC1
% 0.20/0.47  |- ~c2_1 $U \/ ~c2_2 $U a321 \/ ~c3_2 $U $V \/ ~c4_2 $U $V \/ ~ndr1_0 \/
% 0.20/0.47     ~ndr1_1 $U \/ c2_2 $U $V \/ ssSkC1
% 0.20/0.47  |- ~c1_2 a314 $V \/ ~c4_1 $U \/ ~ndr1_0 \/ ~ndr1_1 $U \/ ~ndr1_1 a314 \/
% 0.20/0.47     c1_2 $U $W \/ c3_2 $U $W \/ c3_2 a314 $V \/ c4_0 \/ c4_2 $U $W \/
% 0.20/0.47     c4_2 a314 $V \/ c5_1 $U
% 0.20/0.47  |- c5_0 \/ ndr1_0
% 0.20/0.47  |- c4_0 \/ ndr1_0
% 0.20/0.47  |- ~c4_0 \/ ndr1_0
% 0.20/0.47  |- c1_2 a324 $_4 \/ c3_2 a324 $_4 \/ ssSkC2
% 0.20/0.47  |- c1_0 \/ c3_1 $_6 \/ c4_0 \/ c5_1 $_6 \/ ndr1_1 $_6
% 0.20/0.47  |- c1_0 \/ c3_1 $_6 \/ c5_0 \/ c5_1 $_6 \/ ndr1_1 $_6
% 0.20/0.47  |- c1_0 \/ c3_0 \/ c3_1 $_6 \/ c5_1 $_6 \/ ndr1_1 $_6
% 0.20/0.47  |- c1_0 \/ c3_1 $_8 \/ c4_0 \/ c4_2 $_8 a334 \/ c5_1 $_8
% 0.20/0.47  |- c1_0 \/ c3_1 $_8 \/ c4_2 $_8 a334 \/ c5_0 \/ c5_1 $_8
% 0.20/0.47  |- c1_0 \/ c3_0 \/ c3_1 $_8 \/ c4_2 $_8 a334 \/ c5_1 $_8
% 0.20/0.47  |- c1_0 \/ c2_2 $_9 a334 \/ c3_1 $_9 \/ c4_0 \/ c5_1 $_9
% 0.20/0.47  |- c1_0 \/ c2_2 $_9 a334 \/ c3_1 $_9 \/ c5_0 \/ c5_1 $_9
% 0.20/0.47  |- c1_0 \/ c2_2 $_9 a334 \/ c3_0 \/ c3_1 $_9 \/ c5_1 $_9
% 0.20/0.47  |- c4_0 \/ c5_1 a338 \/ c5_2 a338 a342 \/ ssSkC5
% 0.20/0.47  |- c4_0 \/ c5_1 a351 \/ c5_2 a351 a342 \/ ssSkC8
% 0.20/0.47  |- c2_2 a338 a342 \/ c4_0 \/ c5_1 a338 \/ ssSkC5
% 0.20/0.47  |- c2_2 a351 a342 \/ c4_0 \/ c5_1 a351 \/ ssSkC8
% 0.20/0.47  |- c1_0 \/ c3_0 \/ c3_1 a348 \/ c5_1 a348 \/ c5_2 a348 a334 \/ ssSkC7
% 0.20/0.47  |- c1_0 \/ c3_1 a348 \/ c5_0 \/ c5_1 a348 \/ c5_2 a348 a334 \/ ssSkC7
% 0.20/0.48  |- c1_0 \/ c3_1 a348 \/ c4_0 \/ c5_1 a348 \/ c5_2 a348 a334 \/ ssSkC7
% 0.20/0.48  |- ~c1_2 a353 a334 \/ ~ndr1_1 a353 \/ ~ssSkC8 \/ c1_0 \/ c3_0 \/
% 0.20/0.48     c3_1 a353 \/ c3_2 a353 a334 \/ c5_1 a353
% 0.20/0.48  |- ~c2_1 a316 \/ ~ndr1_0 \/ c2_2 a316 $_29 \/ c3_1 a316 \/
% 0.20/0.48     c3_2 a316 $_29 \/ c4_2 a316 $_29 \/ c5_0 \/ ssSkC0
% 0.20/0.48  |- ~c2_1 a324 \/ ~ndr1_0 \/ c2_2 a324 $_29 \/ c3_1 a324 \/
% 0.20/0.48     c3_2 a324 $_29 \/ c4_2 a324 $_29 \/ c5_0 \/ ssSkC2
% 0.20/0.48  |- ~c2_1 a335 \/ ~ndr1_0 \/ c2_2 a335 $_29 \/ c3_1 a335 \/
% 0.20/0.48     c3_2 a335 $_29 \/ c4_0 \/ c4_2 a335 $_29 \/ c5_0
% 0.20/0.48  |- ~c2_1 a338 \/ ~ndr1_0 \/ c2_2 a338 $_29 \/ c3_1 a338 \/
% 0.20/0.48     c3_2 a338 $_29 \/ c4_2 a338 $_29 \/ c5_0 \/ ssSkC5
% 0.20/0.48  |- ~c2_1 a348 \/ ~ndr1_0 \/ c2_2 a348 $_29 \/ c3_1 a348 \/
% 0.20/0.48     c3_2 a348 $_29 \/ c4_2 a348 $_29 \/ c5_0 \/ ssSkC7
% 0.20/0.48  |- ~c2_1 a351 \/ ~ndr1_0 \/ c2_2 a351 $_29 \/ c3_1 a351 \/
% 0.20/0.48     c3_2 a351 $_29 \/ c4_2 a351 $_29 \/ c5_0 \/ ssSkC8
% 0.20/0.48  |- ~c2_1 a355 \/ ~ndr1_0 \/ c2_0 \/ c2_2 a355 $_29 \/ c3_1 a355 \/
% 0.20/0.48     c3_2 a355 $_29 \/ c4_2 a355 $_29 \/ c5_0
% 0.20/0.48  |- ~c2_1 $_28 \/ ~ndr1_0 \/ c1_0 \/ c2_2 $_28 $_29 \/ c3_1 $_28 \/
% 0.20/0.48     c3_2 $_28 $_29 \/ c4_2 $_28 $_29 \/ c5_0 \/ c5_1 $_28
% 0.20/0.48  |- ~c4_1 a335 \/ ~ndr1_0 \/ c1_2 a335 $_50 \/ c3_2 a335 $_50 \/ c4_0 \/
% 0.20/0.48     c4_2 a335 $_50 \/ c5_0 \/ c5_1 a335 \/ ndr1_1 a314
% 0.20/0.48  |- ~c4_1 a344 \/ ~ndr1_0 \/ c1_2 a344 $_50 \/ c3_2 a344 $_50 \/ c4_0 \/
% 0.20/0.48     c4_2 a344 $_50 \/ c5_1 a344 \/ ndr1_1 a314 \/ ssSkC6
% 0.20/0.48  |- ~c4_1 a348 \/ ~ndr1_0 \/ c1_2 a348 $_50 \/ c3_2 a348 $_50 \/ c4_0 \/
% 0.20/0.48     c4_2 a348 $_50 \/ c5_1 a348 \/ ndr1_1 a314 \/ ssSkC7
% 0.20/0.48  |- ~c4_1 a355 \/ ~ndr1_0 \/ c1_2 a355 $_50 \/ c2_0 \/ c3_2 a355 $_50 \/
% 0.20/0.48     c4_0 \/ c4_2 a355 $_50 \/ c5_0 \/ c5_1 a355 \/ ndr1_1 a314
% 0.20/0.48  |- ~c4_1 $_49 \/ ~ndr1_0 \/ c1_0 \/ c1_2 $_49 $_50 \/ c3_1 $_49 \/
% 0.20/0.48     c3_2 $_49 $_50 \/ c4_0 \/ c4_2 $_49 $_50 \/ c5_1 $_49 \/ ndr1_1 a314
% 0.20/0.48  |- c1_2 a338 $_53 \/ c3_2 a338 $_53 \/ c4_0 \/ c4_2 a338 $_53 \/
% 0.20/0.48     c5_1 a338 \/ ndr1_1 a314 \/ ssSkC5
% 0.20/0.48  |- c1_2 a338 a340 \/ c3_2 a338 a340 \/ c4_0 \/ c5_1 a338 \/ ndr1_1 a314 \/
% 0.20/0.48     ssSkC5 \/ ssSkP0 a338
% 0.20/0.48  |- ~c1_2 a338 a350 \/ ~c3_1 a338 \/ ~ndr1_0 \/ ~ndr1_1 a338 \/ ~ssSkC7 \/
% 0.20/0.48     c1_2 a338 $_54 \/ c3_2 a338 $_54 \/ c4_0 \/ c5_1 a338 \/
% 0.20/0.48     c5_2 a338 $_54 \/ ndr1_1 a314 \/ ssSkC5
% 0.20/0.48  |- ~c3_1 a338 \/ ~c3_2 a338 a350 \/ ~ndr1_0 \/ ~ndr1_1 a338 \/ ~ssSkC7 \/
% 0.20/0.48     c1_2 a338 $_54 \/ c3_2 a338 $_54 \/ c4_0 \/ c5_1 a338 \/
% 0.20/0.48     c5_2 a338 $_54 \/ ndr1_1 a314 \/ ssSkC5
% 0.20/0.48  |- c1_2 a351 $_58 \/ c3_2 a351 $_58 \/ c4_0 \/ c4_2 a351 $_58 \/
% 0.20/0.48     c5_1 a351 \/ ndr1_1 a314 \/ ssSkC8
% 0.20/0.48  |- c1_2 a351 a340 \/ c3_2 a351 a340 \/ c4_0 \/ c5_1 a351 \/ ndr1_1 a314 \/
% 0.20/0.48     ssSkC8 \/ ssSkP0 a351
% 0.20/0.48  |- ~c1_2 a351 a350 \/ ~c3_1 a351 \/ ~ndr1_0 \/ ~ndr1_1 a351 \/ ~ssSkC7 \/
% 0.20/0.48     c1_2 a351 $_59 \/ c3_2 a351 $_59 \/ c4_0 \/ c5_1 a351 \/
% 0.20/0.48     c5_2 a351 $_59 \/ ndr1_1 a314 \/ ssSkC8
% 0.20/0.48  |- ~c3_1 a351 \/ ~c3_2 a351 a350 \/ ~ndr1_0 \/ ~ndr1_1 a351 \/ ~ssSkC7 \/
% 0.20/0.48     c1_2 a351 $_59 \/ c3_2 a351 $_59 \/ c4_0 \/ c5_1 a351 \/
% 0.20/0.48     c5_2 a351 $_59 \/ ndr1_1 a314 \/ ssSkC8
% 0.20/0.48  |- c1_2 a351 a352 \/ c3_2 a351 a352 \/ c4_0 \/ c5_1 a351 \/ ndr1_1 a314 \/
% 0.20/0.48     ssSkC8
% 0.20/0.48  |- ~c4_1 a335 \/ ~ndr1_0 \/ c1_2 a335 $_61 \/ c3_2 a335 $_61 \/ c4_0 \/
% 0.20/0.48     c4_1 a314 \/ c4_2 a335 $_61 \/ c5_0 \/ c5_1 a335
% 0.20/0.48  |- ~c4_1 a344 \/ ~ndr1_0 \/ c1_2 a344 $_61 \/ c3_2 a344 $_61 \/ c4_0 \/
% 0.20/0.48     c4_1 a314 \/ c4_2 a344 $_61 \/ c5_1 a344 \/ ssSkC6
% 0.20/0.48  |- ~c4_1 a348 \/ ~ndr1_0 \/ c1_2 a348 $_61 \/ c3_2 a348 $_61 \/ c4_0 \/
% 0.20/0.48     c4_1 a314 \/ c4_2 a348 $_61 \/ c5_1 a348 \/ ssSkC7
% 0.20/0.48  |- ~c4_1 a355 \/ ~ndr1_0 \/ c1_2 a355 $_61 \/ c2_0 \/ c3_2 a355 $_61 \/
% 0.20/0.48     c4_0 \/ c4_1 a314 \/ c4_2 a355 $_61 \/ c5_0 \/ c5_1 a355
% 0.20/0.48  |- ~c4_1 $_60 \/ ~ndr1_0 \/ c1_0 \/ c1_2 $_60 $_61 \/ c3_1 $_60 \/
% 0.20/0.48     c3_2 $_60 $_61 \/ c4_0 \/ c4_1 a314 \/ c4_2 $_60 $_61 \/ c5_1 $_60
% 0.20/0.48  |- c1_2 a338 $_64 \/ c3_2 a338 $_64 \/ c4_0 \/ c4_1 a314 \/
% 0.20/0.48     c4_2 a338 $_64 \/ c5_1 a338 \/ ssSkC5
% 0.20/0.48  |- c1_2 a338 a340 \/ c3_2 a338 a340 \/ c4_0 \/ c4_1 a314 \/ c5_1 a338 \/
% 0.20/0.48     ssSkC5 \/ ssSkP0 a338
% 0.20/0.48  |- ~c1_2 a338 a350 \/ ~c3_1 a338 \/ ~ndr1_0 \/ ~ndr1_1 a338 \/ ~ssSkC7 \/
% 0.20/0.48     c1_2 a338 $_65 \/ c3_2 a338 $_65 \/ c4_0 \/ c4_1 a314 \/ c5_1 a338 \/
% 0.20/0.48     c5_2 a338 $_65 \/ ssSkC5
% 0.20/0.48  |- ~c3_1 a338 \/ ~c3_2 a338 a350 \/ ~ndr1_0 \/ ~ndr1_1 a338 \/ ~ssSkC7 \/
% 0.20/0.48     c1_2 a338 $_65 \/ c3_2 a338 $_65 \/ c4_0 \/ c4_1 a314 \/ c5_1 a338 \/
% 0.20/0.48     c5_2 a338 $_65 \/ ssSkC5
% 0.20/0.48  |- c1_2 a351 $_69 \/ c3_2 a351 $_69 \/ c4_0 \/ c4_1 a314 \/
% 0.20/0.48     c4_2 a351 $_69 \/ c5_1 a351 \/ ssSkC8
% 0.20/0.48  |- c1_2 a351 a340 \/ c3_2 a351 a340 \/ c4_0 \/ c4_1 a314 \/ c5_1 a351 \/
% 0.20/0.48     ssSkC8 \/ ssSkP0 a351
% 0.20/0.48  |- ~c1_2 a351 a350 \/ ~c3_1 a351 \/ ~ndr1_0 \/ ~ndr1_1 a351 \/ ~ssSkC7 \/
% 0.20/0.48     c1_2 a351 $_70 \/ c3_2 a351 $_70 \/ c4_0 \/ c4_1 a314 \/ c5_1 a351 \/
% 0.20/0.48     c5_2 a351 $_70 \/ ssSkC8
% 0.20/0.48  |- ~c3_1 a351 \/ ~c3_2 a351 a350 \/ ~ndr1_0 \/ ~ndr1_1 a351 \/ ~ssSkC7 \/
% 0.20/0.48     c1_2 a351 $_70 \/ c3_2 a351 $_70 \/ c4_0 \/ c4_1 a314 \/ c5_1 a351 \/
% 0.20/0.48     c5_2 a351 $_70 \/ ssSkC8
% 0.20/0.48  |- c1_2 a351 a352 \/ c3_2 a351 a352 \/ c4_0 \/ c4_1 a314 \/ c5_1 a351 \/
% 0.20/0.48     ssSkC8
% 0.20/0.48  |- ~c5_0 \/ ~ndr1_0 \/ ~ndr1_1 a324 \/ ~ssSkC5 \/ ~ssSkP0 a324 \/
% 0.20/0.48     c1_2 a324 $_72 \/ c2_2 a324 $_72 \/ c2_2 a324 a341 \/ ssSkC2
% 0.20/0.48  |- ~c5_0 \/ ~ndr1_0 \/ ~ndr1_1 a344 \/ ~ssSkC5 \/ ~ssSkP0 a344 \/
% 0.20/0.48     c1_2 a344 a345 \/ c2_2 a344 a341 \/ c2_2 a344 a345 \/ ssSkC6
% 0.20/0.48  |- ~c5_0 \/ ~ndr1_0 \/ ~ndr1_1 a324 \/ ~ssSkC5 \/ ~ssSkP0 a324 \/
% 0.20/0.48     c1_2 a324 $_75 \/ c2_2 a324 $_75 \/ c4_2 a324 a341 \/ ssSkC2
% 0.20/0.48  |- ~c5_0 \/ ~ndr1_0 \/ ~ndr1_1 a344 \/ ~ssSkC5 \/ ~ssSkP0 a344 \/
% 0.20/0.48     c1_2 a344 a345 \/ c2_2 a344 a345 \/ c4_2 a344 a341 \/ ssSkC6
% 0.20/0.48  |- ~c5_0 \/ ~ndr1_0 \/ ~ndr1_1 a324 \/ ~ssSkC5 \/ ~ssSkP0 a324 \/
% 0.20/0.48     c1_2 a324 $_78 \/ c2_2 a324 $_78 \/ c3_2 a324 a341 \/ ssSkC2
% 0.20/0.48  |- ~c5_0 \/ ~ndr1_0 \/ ~ndr1_1 a344 \/ ~ssSkC5 \/ ~ssSkP0 a344 \/
% 0.20/0.48     c1_2 a344 a345 \/ c2_2 a344 a345 \/ c3_2 a344 a341 \/ ssSkC6
% 0.20/0.48  |- ~c3_2 a314 a315 \/ ~c4_1 $_82 \/ ~ndr1_0 \/ c1_0 \/ c1_2 $_82 $_83 \/
% 0.20/0.48     c3_1 $_82 \/ c3_2 $_82 $_83 \/ c4_0 \/ c4_2 $_82 $_83 \/ c5_1 $_82
% 0.20/0.48  |- ~c2_2 a314 a315 \/ ~c4_1 $_84 \/ ~ndr1_0 \/ c1_0 \/ c1_2 $_84 $_85 \/
% 0.20/0.48     c3_1 $_84 \/ c3_2 $_84 $_85 \/ c4_0 \/ c4_2 $_84 $_85 \/ c5_1 $_84
% 0.20/0.48  |- ~c1_2 a314 a315 \/ ~c4_1 $_86 \/ ~ndr1_0 \/ c1_0 \/ c1_2 $_86 $_87 \/
% 0.20/0.48     c3_1 $_86 \/ c3_2 $_86 $_87 \/ c4_0 \/ c4_2 $_86 $_87 \/ c5_1 $_86
% 0.20/0.48  |- c1_0 \/ c2_2 a343 $_96 \/ c3_0 \/ c3_1 a343 \/ c3_2 a343 $_96 \/
% 0.20/0.48     c4_2 a343 $_96 \/ c5_0 \/ c5_1 a343
% 0.20/0.48  |- ~c3_1 a338 \/ ~ndr1_0 \/ ~ssSkC7 \/ c1_2 a338 $_104 \/ c2_2 a338 a350 \/
% 0.20/0.48     c3_2 a338 $_104 \/ c4_0 \/ c5_1 a338 \/ c5_2 a338 $_104 \/
% 0.20/0.48     ndr1_1 a314 \/ ssSkC5
% 0.20/0.48  |- ~c3_1 a338 \/ ~ndr1_0 \/ ~ssSkC7 \/ c1_2 a338 $_108 \/ c2_2 a338 a350 \/
% 0.20/0.48     c3_2 a338 $_108 \/ c4_0 \/ c4_1 a314 \/ c5_1 a338 \/ c5_2 a338 $_108 \/
% 0.20/0.48     ssSkC5
% 0.20/0.48  |- ~c3_1 a351 \/ ~ndr1_0 \/ ~ssSkC7 \/ c1_2 a351 $_112 \/ c2_2 a351 a350 \/
% 0.20/0.48     c3_2 a351 $_112 \/ c4_0 \/ c5_1 a351 \/ c5_2 a351 $_112 \/
% 0.20/0.48     ndr1_1 a314 \/ ssSkC8
% 0.20/0.48  |- ~c3_1 a351 \/ ~ndr1_0 \/ ~ssSkC7 \/ c1_2 a351 $_116 \/ c2_2 a351 a350 \/
% 0.20/0.48     c3_2 a351 $_116 \/ c4_0 \/ c4_1 a314 \/ c5_1 a351 \/ c5_2 a351 $_116 \/
% 0.20/0.48     ssSkC8
% 0.20/0.48  |- ~c2_1 $_119 \/ ~ndr1_0 \/ c1_1 $_121 \/ c2_1 a316 \/ c4_1 $_119 \/
% 0.20/0.48     c4_1 a316 \/ c4_2 a316 $_120 \/ c5_1 $_121 \/ c5_2 a316 $_120 \/ ssSkC0
% 0.20/0.48  |- ~c2_1 $_119 \/ ~ndr1_0 \/ c1_1 $_121 \/ c2_1 a324 \/ c4_1 $_119 \/
% 0.20/0.48     c4_1 a324 \/ c4_2 a324 $_120 \/ c5_1 $_121 \/ c5_2 a324 $_120 \/ ssSkC2
% 0.20/0.48  |- ~c2_1 $_119 \/ ~ndr1_0 \/ c1_1 $_121 \/ c2_1 a331 \/ c4_1 $_119 \/
% 0.20/0.48     c4_1 a331 \/ c4_2 a331 $_120 \/ c5_1 $_121 \/ c5_2 a331 $_120 \/ ssSkC4
% 0.20/0.48  |- ~c2_1 $_119 \/ ~ndr1_0 \/ c1_1 $_121 \/ c2_1 a335 \/ c4_0 \/
% 0.20/0.48     c4_1 $_119 \/ c4_1 a335 \/ c4_2 a335 $_120 \/ c5_0 \/ c5_1 $_121 \/
% 0.20/0.48     c5_2 a335 $_120
% 0.20/0.48  |- ~c2_1 $_119 \/ ~ndr1_0 \/ c1_1 $_121 \/ c2_1 a344 \/ c4_1 $_119 \/
% 0.20/0.48     c4_1 a344 \/ c4_2 a344 $_120 \/ c5_1 $_121 \/ c5_2 a344 $_120 \/ ssSkC6
% 0.20/0.48  |- ~c2_1 $_119 \/ ~ndr1_0 \/ c1_1 $_121 \/ c2_1 a348 \/ c4_1 $_119 \/
% 0.20/0.48     c4_1 a348 \/ c4_2 a348 $_120 \/ c5_1 $_121 \/ c5_2 a348 $_120 \/ ssSkC7
% 0.20/0.48  |- ~c2_1 $_119 \/ ~ndr1_0 \/ c1_1 $_121 \/ c2_0 \/ c2_1 a355 \/
% 0.20/0.48     c4_1 $_119 \/ c4_1 a355 \/ c4_2 a355 $_120 \/ c5_0 \/ c5_1 $_121 \/
% 0.20/0.48     c5_2 a355 $_120
% 0.20/0.48  |- ~c2_1 $_119 \/ ~ndr1_0 \/ c1_0 \/ c1_1 $_121 \/ c2_1 $_118 \/ c3_0 \/
% 0.20/0.48     c3_1 $_118 \/ c4_1 $_118 \/ c4_1 $_119 \/ c4_2 $_118 $_120 \/
% 0.20/0.48     c5_1 $_118 \/ c5_1 $_121 \/ c5_2 $_118 $_120
% 0.20/0.48  |- ~c2_1 $_119 \/ ~ndr1_0 \/ c1_0 \/ c1_1 $_121 \/ c2_1 $_118 \/
% 0.20/0.48     c3_1 $_118 \/ c4_1 $_118 \/ c4_1 $_119 \/ c4_2 $_118 $_120 \/ c5_0 \/
% 0.20/0.48     c5_1 $_118 \/ c5_1 $_121 \/ c5_2 $_118 $_120
% 0.20/0.48  |- ~c2_1 $_119 \/ ~ndr1_0 \/ c1_0 \/ c1_1 $_121 \/ c2_1 $_118 \/
% 0.20/0.48     c3_1 $_118 \/ c4_0 \/ c4_1 $_118 \/ c4_1 $_119 \/ c4_2 $_118 $_120 \/
% 0.20/0.48     c5_1 $_118 \/ c5_1 $_121 \/ c5_2 $_118 $_120
% 0.20/0.48  |- c1_1 $_126 \/ c2_1 a316 \/ c3_0 \/ c4_1 a316 \/ c4_1 a343 \/
% 0.20/0.48     c4_2 a316 $_125 \/ c5_1 $_126 \/ c5_2 a316 $_125 \/ ssSkC0
% 0.20/0.48  |- c1_1 $_133 \/ c2_1 a331 \/ c3_0 \/ c4_1 a331 \/ c4_1 a343 \/
% 0.20/0.48     c4_2 a331 $_132 \/ c5_1 $_133 \/ c5_2 a331 $_132 \/ ssSkC4
% 0.20/0.48  |- c1_1 $_135 \/ c2_1 a331 \/ c3_0 \/ c4_1 a331 \/ c4_1 a343 \/
% 0.20/0.48     c4_2 a331 a332 \/ c5_1 $_135 \/ ssSkC4
% 0.20/0.48  |- c1_1 $_141 \/ c2_1 a324 \/ c3_0 \/ c4_1 a324 \/ c4_1 a343 \/
% 0.20/0.48     c4_2 a324 $_140 \/ c5_1 $_141 \/ c5_2 a324 $_140 \/ ssSkC2
% 0.20/0.48  |- c1_1 $_148 \/ c2_1 a344 \/ c3_0 \/ c4_1 a343 \/ c4_1 a344 \/
% 0.20/0.48     c4_2 a344 $_147 \/ c5_1 $_148 \/ c5_2 a344 $_147 \/ ssSkC6
% 0.20/0.48  |- ~c1_2 a344 $_149 \/ ~c2_2 a344 $_149 \/ ~ndr1_1 a344 \/ c1_1 $_150 \/
% 0.20/0.48     c2_1 a344 \/ c3_0 \/ c4_1 a343 \/ c4_1 a344 \/ c4_2 a344 $_149 \/
% 0.20/0.48     c5_1 $_150 \/ ssSkC6
% 0.20/0.48  |- c1_1 $_163 \/ c2_1 a348 \/ c3_0 \/ c4_1 a343 \/ c4_1 a348 \/
% 0.20/0.48     c5_1 $_163 \/ ssSkC7
% 0.20/0.48  |- ~c1_2 a314 $_166 \/ ~c4_1 $_165 \/ ~ndr1_0 \/ ~ndr1_1 a314 \/ c1_0 \/
% 0.20/0.48     c1_2 $_165 $_167 \/ c3_1 $_165 \/ c3_2 $_165 $_167 \/ c3_2 a314 $_166 \/
% 0.20/0.48     c4_0 \/ c4_2 $_165 $_167 \/ c4_2 a314 $_166 \/ c5_1 $_165
% 0.20/0.48  |- c1_1 $_172 \/ c2_1 a335 \/ c3_0 \/ c4_0 \/ c4_1 a335 \/ c4_1 a343 \/
% 0.20/0.48     c4_2 a335 $_171 \/ c5_0 \/ c5_1 $_172 \/ c5_2 a335 $_171
% 0.20/0.48  |- c1_1 $_182 \/ c2_0 \/ c2_1 a355 \/ c3_0 \/ c4_1 a343 \/ c4_1 a355 \/
% 0.20/0.48     c5_0 \/ c5_1 $_182
% 0.20/0.49  |- c1_0 \/ c1_1 $_193 \/ c2_1 $_191 \/ c3_0 \/ c3_1 $_191 \/ c4_1 $_191 \/
% 0.20/0.49     c4_1 a343 \/ c4_2 $_191 $_192 \/ c5_1 $_191 \/ c5_1 $_193 \/
% 0.20/0.49     c5_2 $_191 $_192
% 0.20/0.49  |- ~c2_2 a353 $_195 \/ ~ndr1_1 a353 \/ ~ssSkC8 \/ c1_0 \/ c1_1 $_196 \/
% 0.20/0.49     c2_1 a353 \/ c3_0 \/ c3_1 a353 \/ c3_2 a353 $_195 \/ c4_1 a343 \/
% 0.20/0.49     c4_1 a353 \/ c4_2 a353 $_195 \/ c5_1 $_196 \/ c5_1 a353
% 0.20/0.49  |- ~ssSkC8 \/ c1_0 \/ c1_1 $_199 \/ c2_1 a353 \/ c3_0 \/ c3_1 a353 \/
% 0.20/0.49     c3_2 a353 a340 \/ c4_1 a343 \/ c4_1 a353 \/ c4_2 a353 a340 \/
% 0.20/0.49     c5_1 $_199 \/ c5_1 a353 \/ ssSkP0 a353
% 0.20/0.49  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.49  
%------------------------------------------------------------------------------