%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SYN720-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n007.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:05:00 EDT 2022 % Result : Satisfiable 0.46s 0.61s % Output : Saturation 0.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SYN720-1 : TPTP v8.1.0. Released v2.5.0. % 0.11/0.12 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n007.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 06:48:03 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.46/0.61 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.46/0.61 % 0.46/0.61 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.46/0.61 |- s0 d % 0.46/0.61 |- n0 d e % 0.46/0.61 |- s0 b % 0.46/0.61 |- q0 b b % 0.46/0.61 |- n0 d b % 0.46/0.61 |- r0 b % 0.46/0.61 |- n0 e b % 0.46/0.61 |- m0 a $X a % 0.46/0.61 |- r0 e % 0.46/0.61 |- p0 b $X % 0.46/0.61 |- n0 a b % 0.46/0.61 |- m0 c b a % 0.46/0.61 |- q0 $X d % 0.46/0.61 |- p0 c b % 0.46/0.61 |- m0 $X d $Y % 0.46/0.61 |- l0 a % 0.46/0.61 |- q0 b e % 0.46/0.61 |- m0 a e e % 0.46/0.61 |- l0 c % 0.46/0.61 |- n0 d c % 0.46/0.61 |- m0 e b c % 0.46/0.61 |- k0 e % 0.46/0.61 |- q0 d b % 0.46/0.61 |- n0 e e % 0.46/0.61 |- m0 b b e % 0.46/0.61 |- k0 b % 0.46/0.61 |- q0 d c % 0.46/0.61 |- n0 c d % 0.46/0.61 |- m0 d e c % 0.46/0.61 |- q0 a b % 0.46/0.61 |- n0 b a % 0.46/0.61 |- m0 b a a % 0.46/0.61 |- ~n0 $J $I \/ k1 $I % 0.46/0.61 |- ~n0 $H $G \/ l1 $G $G % 0.46/0.61 |- ~m0 $D $C $E \/ ~p0 $E $C \/ ~r0 $F \/ l1 $C $D % 0.46/0.61 |- ~m0 $C $C $B \/ m1 $B $C $B % 0.46/0.61 |- ~n0 $C $C \/ ~p0 $C $B \/ m1 $B $B c % 0.46/0.61 |- ~k0 $J \/ ~n0 $A $A \/ m1 $J $J $A % 0.46/0.61 |- ~l0 $D \/ ~m0 $C $C $B \/ m1 $B $C $C % 0.46/0.61 |- ~m1 $J $A $I \/ ~m1 $J $I $H \/ m1 $H $I $I % 0.46/0.61 |- ~p0 $A $B \/ ~r0 c \/ m1 $A $B c % 0.46/0.61 |- ~k0 $J \/ ~l0 $I \/ m1 $I $J $I % 0.46/0.61 |- ~m1 $G c $G \/ ~q0 $F $G \/ m1 $F a $G % 0.46/0.61 |- ~p0 $H $I \/ ~s0 $H \/ m1 $H $I $H % 0.46/0.61 |- ~m0 a e c \/ ~r0 $G \/ m1 c a c % 0.46/0.61 |- ~k1 $B \/ ~q0 $A $A \/ m1 $A $B $B % 0.46/0.62 |- ~m0 $F $E c \/ n1 $E c $E % 0.46/0.62 |- ~p0 $D $D \/ ~p0 $E $F \/ n1 $D $E $D % 0.46/0.62 |- ~l1 $J d \/ ~p0 $J $J \/ ~r0 $I \/ n1 $I d $J % 0.46/0.62 |- ~l0 $D \/ n1 $D $E $D % 0.46/0.62 |- ~p0 $H d \/ ~p0 a b \/ n1 a $H b % 0.46/0.62 |- ~l0 $G \/ ~l1 $G $E \/ ~n1 $E $F $E \/ n1 $E $F $F % 0.46/0.62 |- ~k0 $E \/ ~n0 d $D \/ p1 $D $D $E % 0.46/0.62 |- ~p0 $C $B \/ p1 $B $B $C % 0.46/0.62 |- ~l0 $J \/ ~p1 $I $A $H \/ p1 $H $I $H % 0.46/0.62 |- ~m0 b c e \/ p1 c e b % 0.46/0.62 |- ~m0 $J $H $A \/ ~p1 $J $H $A \/ p1 $H $I $J % 0.46/0.62 |- ~k0 $G \/ ~m1 $F $G b \/ p1 $F b $G % 0.46/0.62 |- ~s0 e \/ q1 b e e % 0.46/0.62 |- ~p0 $G $F \/ q1 $F $G $G % 0.46/0.62 |- ~k0 $G \/ ~l0 $E \/ ~q1 $F $F $G \/ q1 $E $F $F % 0.46/0.62 |- ~p0 $D d \/ ~s0 $C \/ q1 $C $C $D % 0.46/0.62 |- q1 e $A $A % 0.46/0.62 |- ~k1 $E \/ ~p0 $G $G \/ ~q0 $F $E \/ q1 $E $E $F % 0.46/0.62 |- ~m1 $H $I $I \/ ~r0 $J \/ q1 $H $H $I % 0.46/0.62 |- ~k1 $F \/ ~k2 $F $D \/ ~m1 $E $D $C \/ k2 $C $D % 0.46/0.62 |- ~p1 $G $H e \/ p2 e $G $H % 0.46/0.62 |- ~l1 $E $F \/ ~p1 $C $E $F \/ ~p2 $C $D $C \/ p2 $C $D $D % 0.46/0.62 |- ~m0 $I $H d \/ p2 $H $H d % 0.46/0.62 |- ~k1 $J \/ ~p2 e $H $I \/ p2 $H $I $I % 0.46/0.62 |- ~n1 e $F a \/ ~q1 a $G $F \/ p2 $F e $G % 0.46/0.62 |- ~p2 $B $D $B \/ ~q1 c $B $D \/ ~s0 e \/ p2 $B $B $C % 0.46/0.62 |- ~m1 a $H d \/ ~n0 $H d \/ p2 a $H d % 0.46/0.62 |- ~m1 $E $D $E \/ p2 $D $E $D % 0.46/0.62 |- ~k0 $F \/ q2 $E $F $F % 0.46/0.62 |- ~q0 e c \/ ~q2 d c a \/ ~s1 c \/ q2 d a a % 0.46/0.62 |- ~n1 $G $F $H \/ ~p1 $F $F $H \/ ~q2 $G $H $F \/ q2 $F $G $F % 0.46/0.62 |- ~k1 $E \/ ~l2 $E $D \/ q2 $D c $E % 0.46/0.62 |- ~l1 $H $G \/ q2 $G $G $H % 0.46/0.62 |- ~q2 b $H b \/ s2 $H % 0.46/0.62 |- ~n0 $J $C \/ ~p2 $B $A $C \/ k3 $J $A $J % 0.46/0.62 |- ~k2 $G $F \/ k3 $F $F $G % 0.46/0.62 |- ~m2 $D \/ ~m2 $E \/ ~p1 $C $D $B \/ k3 $B $B $C % 0.46/0.62 |- ~p2 $D $C $C \/ k3 $C $D $C % 0.46/0.62 |- ~p2 $G $H $G \/ ~r0 $G \/ l3 $G $H % 0.46/0.62 |- ~k2 c $I \/ ~r2 $H \/ m3 $H $I $H % 0.46/0.62 |- ~k3 $B $C $B \/ ~r2 $C \/ m3 $B $B $C % 0.46/0.62 |- ~q2 $J c c \/ ~s2 c \/ m3 $J c $J % 0.46/0.62 |- ~k2 $D $E \/ ~q2 $F d $C \/ p3 $C $D $E % 0.46/0.62 |- ~k3 $A $B $J \/ ~r2 $A \/ p3 $J $A $B % 0.46/0.62 |- ~p2 d b c \/ ~q2 $I d $I \/ p3 $I d e % 0.46/0.62 |- ~m3 $B $C $D \/ ~p2 $A $B $D \/ p3 $A $B $B % 0.46/0.62 |- ~n0 $I $G \/ ~q2 $I $G $H \/ q3 $G $H % 0.46/0.62 |- ~p2 $F $E $E \/ ~q3 $F $E \/ q3 $E $E % 0.46/0.62 |- ~k1 $G \/ ~q3 $H $G \/ ~r2 d \/ q3 $G $G % 0.46/0.62 |- ~l2 c $G \/ ~s2 $H \/ r3 $G $H $H % 0.46/0.62 |- ~p2 $B $D $C \/ r3 $B $C $B % 0.46/0.62 |- ~k2 $A $B \/ ~r2 $B \/ ~r3 $B $J $J \/ r3 $J $A $B % 0.46/0.62 |- ~r0 $G \/ ~r3 $H $G $H \/ p4 $G $G $H % 0.46/0.62 |- ~k3 $B $B $C \/ p4 $B $C $B % 0.46/0.62 |- ~m3 $B c a \/ p4 c c $B % 0.46/0.62 |- ~p4 $D $F $E \/ ~r0 $D \/ m5 $D $E % 0.46/0.62 |- ~k4 $C \/ m5 $C $C % 0.46/0.62 |- ~m2 $A \/ ~s4 $J \/ q5 $J $A % 0.46/0.62 |- ~s4 $C \/ r5 $C $D % 0.46/0.62 |- ~k4 $B \/ r5 $B $B % 0.46/0.62 |- k1 b % 0.46/0.62 |- k1 a % 0.46/0.62 |- k1 d % 0.46/0.62 |- k1 c % 0.46/0.62 |- k1 e % 0.46/0.62 |- m2 b % 0.46/0.62 |- q1 $_39 b b % 0.46/0.62 |- q1 b c c % 0.46/0.62 |- l1 b b % 0.46/0.62 |- l1 a a % 0.46/0.62 |- l1 c c % 0.46/0.62 |- l1 e e % 0.46/0.62 |- n1 a $_50 a % 0.46/0.62 |- n1 c $_50 c % 0.46/0.62 |- p1 $_66 $_66 b % 0.46/0.62 |- p1 $_69 $_69 $_69 % 0.46/0.62 |- q2 $_71 $_71 $_71 % 0.46/0.62 |- k2 $_78 $_78 % 0.46/0.62 |- k3 $_84 $_84 $_84 % 0.46/0.62 |- m1 $_91 d $_91 % 0.46/0.62 |- m1 $_95 $_95 $_95 % 0.46/0.62 |- n1 e c e % 0.46/0.62 |- n1 b c b % 0.46/0.62 |- n1 d c d % 0.46/0.62 |- n2 $_105 % 0.46/0.62 |- l3 $_108 $_108 % 0.46/0.62 |- p3 $_108 $_108 $_108 % 0.46/0.62 |- m3 $_108 $_108 $_108 % 0.46/0.62 |- p2 $_112 $_112 $_112 % 0.46/0.62 |- p2 d $_116 d % 0.46/0.62 |- s2 b % 0.46/0.62 |- n3 $_121 % 0.46/0.62 |- l4 $_127 % 0.46/0.62 |- q5 $_128 $_128 % 0.46/0.62 |- p4 $_131 $_131 $_131 % 0.46/0.62 |- ~k0 $_137 \/ m1 a $_137 a % 0.46/0.62 |- ~k0 $_137 \/ m1 c $_137 c % 0.46/0.62 |- m1 a b a % 0.46/0.62 |- m1 a e a % 0.46/0.62 |- m1 c b c % 0.46/0.62 |- m1 c e c % 0.46/0.62 |- p2 b c b % 0.46/0.62 |- p2 e c e % 0.46/0.62 |- q1 $_157 $_157 $_157 % 0.46/0.62 |- r3 $_162 $_162 $_162 % 0.46/0.62 |- ~s0 $_170 \/ m2 $_170 % 0.46/0.62 |- m2 d % 0.46/0.62 |- ~q0 $_174 b \/ m1 $_174 a b % 0.46/0.62 |- ~q0 $_174 c \/ m1 $_174 a c % 0.46/0.62 |- ~q0 $_174 e \/ m1 $_174 a e % 0.46/0.62 |- ~m1 d c d \/ m1 $_174 a d % 0.46/0.62 |- m1 d a c % 0.46/0.62 |- m1 a a b % 0.46/0.62 |- m1 d a b % 0.46/0.62 |- m1 b a e % 0.46/0.62 |- ~k0 $_181 \/ m1 $_181 $_181 e % 0.46/0.62 |- m1 b b e % 0.46/0.62 |- ~r0 c \/ m1 b $_184 c % 0.46/0.62 |- m1 b $_187 b % 0.46/0.62 |- p2 $_188 b $_188 % 0.46/0.62 |- ~k0 $_191 \/ p1 b b $_191 % 0.46/0.62 |- ~k0 $_191 \/ p1 c c $_191 % 0.46/0.62 |- ~k0 $_191 \/ p1 e e $_191 % 0.46/0.62 |- p1 b b e % 0.46/0.62 |- p1 c c e % 0.46/0.62 |- p2 e c c % 0.46/0.62 |- ~s0 $_195 \/ q1 $_195 $_195 b % 0.46/0.62 |- r1 $_198 % 0.46/0.62 |- ~l0 $_200 \/ r2 $_200 % 0.46/0.62 |- r2 a % 0.46/0.62 |- r2 c % 0.46/0.62 |- l3 b a % 0.46/0.62 |- l3 b c % 0.46/0.62 |- l3 b e % 0.46/0.62 |- ~r0 d \/ l3 d $_205 % 0.46/0.62 |- l3 e a % 0.46/0.62 |- l3 e c % 0.46/0.62 |- ~r0 $_204 \/ l3 $_204 b % 0.46/0.62 |- l3 e b % 0.46/0.62 |- ~r2 $_208 \/ m3 $_208 c $_208 % 0.46/0.62 |- p4 c c a % 0.46/0.62 |- s2 d % 0.46/0.62 |- s1 $_223 % 0.46/0.62 |- n1 b e e % 0.46/0.62 |- ~k1 $_227 \/ n1 $_227 e e % 0.46/0.62 |- n1 d e e % 0.46/0.62 |- q2 $_236 b b % 0.46/0.62 |- q2 $_236 e e % 0.46/0.62 |- ~r0 $_265 \/ m1 $_265 $_266 $_265 % 0.46/0.62 |- m1 e $_269 e % 0.46/0.62 |- p2 $_270 e $_270 % 0.46/0.62 |- ~r0 $_271 \/ l3 $_271 e % 0.46/0.62 |- ~r0 c \/ m5 c a % 0.46/0.62 |- ~r0 $_279 \/ m5 $_279 $_279 % 0.46/0.62 |- ~n0 b b \/ m1 $_285 $_285 c % 0.46/0.62 |- ~n0 c c \/ m1 b b c % 0.46/0.62 |- ~p0 e e \/ ~r0 $_291 \/ l1 e a % 0.46/0.62 |- ~p0 a $_288 \/ ~r0 $_291 \/ l1 $_288 a % 0.46/0.62 |- ~p0 a a \/ ~r0 $_291 \/ l1 a b % 0.46/0.62 |- ~p0 a b \/ ~r0 $_291 \/ l1 b c % 0.46/0.62 |- ~p0 c e \/ ~r0 $_291 \/ l1 e d % 0.46/0.62 |- l1 b e % 0.46/0.62 |- q2 e e b % 0.46/0.62 |- p3 e b e % 0.46/0.62 |- l1 d $_302 % 0.46/0.62 |- q2 $_304 $_304 d % 0.46/0.62 |- ~k1 $_308 \/ l1 $_308 $_308 % 0.46/0.62 |- m1 e b b % 0.46/0.62 |- p1 e b b % 0.46/0.62 |- m1 $_315 d d % 0.46/0.62 |- ~n0 d d \/ p2 a d d % 0.46/0.62 |- ~p0 $_319 $_320 \/ n1 b $_319 b % 0.46/0.62 |- ~p0 $_318 $_318 \/ n1 $_318 b $_318 % 0.46/0.62 |- ~p0 $_318 $_318 \/ n1 $_318 c $_318 % 0.46/0.62 |- q1 e e b % 0.46/0.62 |- q1 $_333 $_333 d % 0.46/0.62 |- ~n1 e d a \/ p2 d e a % 0.46/0.62 |- m3 e e a % 0.46/0.62 |- m3 e e c % 0.46/0.62 |- q3 e b % 0.46/0.63 |- q3 e e % 0.46/0.63 |- ~n0 $_345 $_345 \/ q3 $_345 d % 0.46/0.63 |- ~n0 $_346 $_346 \/ q3 $_346 $_346 % 0.46/0.63 |- q3 b b % 0.46/0.63 |- k4 c % 0.46/0.63 |- n4 $H $H % 0.46/0.63 |- m5 c c % 0.46/0.63 |- ~p3 $_348 $A $A \/ n4 $_348 $A % 0.46/0.63 |- q3 e d % 0.46/0.63 |- ~k1 $_358 \/ m1 b $_358 $_358 % 0.46/0.63 |- ~k1 $_358 \/ m1 d $_358 $_358 % 0.46/0.63 |- m1 b a a % 0.46/0.63 |- m1 b c c % 0.46/0.63 |- m1 b e e % 0.46/0.63 |- q1 b b e % 0.46/0.63 |- q1 b b c % 0.46/0.63 |- m1 d a a % 0.46/0.63 |- m1 d b b % 0.46/0.63 |- m1 d c c % 0.46/0.63 |- m1 d e e % 0.46/0.63 |- q1 b b a % 0.46/0.63 |- ~l1 $_371 $_374 \/ s4 $_371 % 0.46/0.63 |- s4 a % 0.46/0.63 |- s4 d % 0.46/0.63 |- k5 $_254 % 0.46/0.63 |- r5 a $D % 0.46/0.63 |- ~m2 $A \/ q5 a $A % 0.46/0.63 |- r5 d $D % 0.46/0.63 |- ~m2 $A \/ q5 d $A % 0.46/0.63 |- s4 b % 0.46/0.63 |- r5 b $D % 0.46/0.63 |- ~m2 $A \/ q5 b $A % 0.46/0.63 |- s4 c % 0.46/0.63 |- r5 c $D % 0.46/0.63 |- ~m2 $A \/ q5 c $A % 0.46/0.63 |- s4 e % 0.46/0.63 |- r5 e $D % 0.46/0.63 |- ~m2 $A \/ q5 e $A % 0.46/0.63 |- q5 e b % 0.46/0.63 |- q5 e d % 0.46/0.63 |- q5 b d % 0.46/0.63 |- q5 d b % 0.46/0.63 |- q5 c b % 0.46/0.63 |- q5 c d % 0.46/0.63 |- q5 a b % 0.46/0.63 |- q5 a d % 0.46/0.63 |- ~l1 b d \/ ~r0 $_393 \/ n1 $_393 d b % 0.46/0.63 |- p1 e c e % 0.46/0.63 |- p2 e e c % 0.46/0.63 |- p1 c b c % 0.46/0.63 |- p1 e b e % 0.46/0.63 |- p2 e e b % 0.46/0.63 |- p1 b $_412 b % 0.46/0.63 |- ~n0 $_417 $_416 \/ q1 $_419 $_416 $_419 % 0.46/0.63 |- q1 $_424 b $_424 % 0.46/0.63 |- q1 $_424 a $_424 % 0.46/0.63 |- q1 $_424 d $_424 % 0.46/0.63 |- q1 $_424 c $_424 % 0.46/0.63 |- q1 $_424 e $_424 % 0.46/0.63 |- ~n1 e a a \/ p2 a e b % 0.46/0.63 |- p2 $_426 a $_426 % 0.46/0.63 |- ~n1 e a a \/ p2 a e c % 0.46/0.63 |- p2 b c c % 0.46/0.63 |- r3 b c b % 0.46/0.63 |- ~r0 c \/ p4 c c b % 0.46/0.63 |- ~r0 $_428 \/ l3 $_428 a % 0.46/0.63 |- ~n1 e a a \/ p2 a e d % 0.46/0.63 |- ~q2 $_442 d $_439 \/ p3 $_439 $_441 $_441 % 0.46/0.63 |- ~k2 $_440 $_441 \/ p3 d $_440 $_441 % 0.46/0.63 |- p3 d $_444 $_444 % 0.46/0.63 |- n4 d $_445 % 0.46/0.63 |- ~p2 d b c \/ p3 d d e % 0.46/0.63 |- r3 a a e % 0.46/0.63 |- ~l0 $_453 \/ ~r0 $_452 \/ n1 $_452 $_453 $_452 % 0.46/0.63 |- ~l0 $_453 \/ n1 b $_453 b % 0.46/0.63 |- n1 b a b % 0.46/0.63 |- ~l0 $_458 \/ n1 e $_458 e % 0.46/0.63 |- n1 e a e % 0.46/0.63 |- ~m1 b a $_461 \/ m1 $_461 a a % 0.46/0.63 |- ~m1 b c $_461 \/ m1 $_461 c c % 0.46/0.63 |- ~m1 b e $_461 \/ m1 $_461 e e % 0.46/0.63 |- ~m1 d a $_461 \/ m1 $_461 a a % 0.46/0.63 |- ~m1 d b $_461 \/ m1 $_461 b b % 0.46/0.63 |- ~m1 d c $_461 \/ m1 $_461 c c % 0.46/0.63 |- ~m1 d e $_461 \/ m1 $_461 e e % 0.46/0.63 |- ~m1 e b $_461 \/ m1 $_461 b b % 0.47/0.63 |- ~m1 $_462 $_462 $_461 \/ m1 $_461 $_462 $_462 % 0.47/0.63 |- ~m1 a $_460 e \/ m1 a e e % 0.47/0.63 |- ~m1 b $_460 $_462 \/ m1 b $_462 $_462 % 0.47/0.63 |- ~m1 c $_460 b \/ m1 c b b % 0.47/0.63 |- ~m1 c $_460 e \/ m1 c e e % 0.47/0.63 |- ~m1 e $_460 $_462 \/ m1 e $_462 $_462 % 0.47/0.63 |- m1 c a a % 0.47/0.63 |- ~m1 c a $H \/ m1 $H a a % 0.47/0.63 |- q1 c c a % 0.47/0.63 |- m1 e a a % 0.47/0.63 |- ~m1 e a $H \/ m1 $H a a % 0.47/0.63 |- q1 e e a % 0.47/0.63 |- m1 a b b % 0.47/0.63 |- ~m1 a b $H \/ m1 $H b b % 0.47/0.63 |- q1 a a b % 0.47/0.63 |- ~n1 e b a \/ p2 b e a % 0.47/0.63 |- k4 e % 0.47/0.63 |- n1 $_506 $_506 $_507 % 0.47/0.63 |- ~m0 b $_511 b \/ p1 $_511 $_512 b % 0.47/0.63 |- ~m0 c c e \/ p1 c $_512 c % 0.47/0.63 |- ~m0 e b b \/ p1 b $_512 e % 0.47/0.63 |- ~m0 e b e \/ p1 b $_512 e % 0.47/0.63 |- ~m0 e c e \/ p1 c $_512 e % 0.47/0.63 |- ~m0 $_511 $_511 b \/ p1 $_511 $_512 $_511 % 0.47/0.63 |- ~m0 $_510 $_510 $_510 \/ p1 $_510 $_512 $_510 % 0.47/0.63 |- p1 $_516 $I a % 0.47/0.63 |- ~m0 $_519 $_518 a \/ p1 $_518 $I $_519 % 0.47/0.63 |- p1 a $_531 b % 0.47/0.63 |- p1 b $_542 c % 0.47/0.63 |- p1 d $_542 $_544 % 0.47/0.63 |- ~m0 b $_545 c \/ p1 $_545 $I b % 0.47/0.63 |- p2 e d $_546 % 0.47/0.63 |- q3 d d % 0.47/0.63 |- l3 e d % 0.47/0.63 |- r3 e $_547 e % 0.47/0.63 |- k3 d e d % 0.47/0.63 |- ~r2 d \/ p3 d d e % 0.47/0.63 |- ~r2 e \/ m3 d d e % 0.47/0.63 |- ~m0 d $_548 $_549 \/ p1 $_548 $I d % 0.47/0.63 |- ~r0 $_550 \/ p4 $_550 $_550 e % 0.47/0.63 |- p2 e e d % 0.47/0.63 |- p1 $_554 d $_554 % 0.47/0.63 |- p2 d $_557 $_557 % 0.47/0.63 |- ~q3 d $_558 \/ q3 $_558 $_558 % 0.47/0.63 |- r3 d $_558 d % 0.47/0.63 |- k3 $_558 d $_558 % 0.47/0.63 |- ~r2 $_559 \/ p3 $_559 $_559 d % 0.47/0.63 |- ~r2 d \/ m3 $_559 $_559 d % 0.47/0.63 |- ~r0 $_560 \/ p4 $_560 $_560 d % 0.47/0.63 |- p1 e $_569 d % 0.47/0.63 |- ~m0 e $_572 d \/ p1 $_572 $I e % 0.47/0.63 |- ~p2 $_575 $_578 $_578 \/ p3 $_575 $_578 $_578 % 0.47/0.63 |- p3 b c c % 0.47/0.63 |- n4 b c % 0.47/0.63 |- ~r3 $_601 $_601 $_600 \/ p4 $_600 $_601 $_601 % 0.47/0.63 |- p4 e a a % 0.47/0.63 |- ~l0 $_605 \/ q1 $_605 a a % 0.47/0.63 |- ~k0 a \/ ~l0 $_605 \/ q1 $_605 c c % 0.47/0.63 |- ~l0 $_605 \/ q1 $_605 d d % 0.47/0.63 |- ~l0 $_605 \/ q1 $_605 e e % 0.47/0.63 |- ~k0 d \/ ~l0 $_605 \/ q1 $_605 $_606 $_606 % 0.47/0.63 |- ~k0 $_607 \/ ~l0 $_605 \/ q1 $_605 $_607 $_607 % 0.47/0.63 |- q1 c a a % 0.47/0.63 |- q1 a d d % 0.47/0.63 |- q1 c d d % 0.47/0.63 |- q1 a e e % 0.47/0.63 |- q1 c e e % 0.47/0.63 |- ~k0 a \/ q1 a c c % 0.47/0.63 |- ~k0 $_614 \/ q1 a $_614 $_614 % 0.47/0.63 |- ~k0 $_614 \/ q1 c $_614 $_614 % 0.47/0.63 |- ~k0 d \/ q1 a $_618 $_618 % 0.47/0.63 |- ~k0 d \/ q1 c $_618 $_618 % 0.47/0.63 |- q1 d d $_624 % 0.47/0.63 |- ~m2 $_627 \/ m3 $_629 $_627 $_627 % 0.47/0.63 |- m3 $_636 b b % 0.47/0.63 |- m3 $_636 d d % 0.47/0.63 |- ~q3 $_640 $_639 \/ ~s2 $_639 \/ q3 $_639 $_640 % 0.47/0.63 |- q3 b e % 0.47/0.63 |- q3 d e % 0.47/0.63 |- r4 $_651 % 0.47/0.63 |- s5 $H % 0.47/0.63 |- ~l0 $_657 \/ ~l1 $_657 b \/ n1 b a a % 0.47/0.63 |- ~l0 $_657 \/ ~l1 $_657 b \/ n1 b c c % 0.47/0.63 |- ~l0 $_657 \/ ~l1 $_657 d \/ n1 d c c % 0.47/0.63 |- ~l0 $_657 \/ ~l1 $_657 e \/ n1 e a a % 0.47/0.63 |- ~l0 $_657 \/ ~l1 $_657 e \/ n1 e c c % 0.47/0.63 |- ~l0 b \/ n1 e a a % 0.47/0.63 |- ~l0 d \/ n1 e a a % 0.47/0.63 |- ~l0 e \/ n1 e a a % 0.47/0.63 |- ~l0 b \/ n1 b a a % 0.47/0.63 |- ~l0 d \/ n1 b a a % 0.47/0.63 |- ~l0 b \/ n1 b c c % 0.47/0.63 |- ~l0 d \/ n1 b c c % 0.47/0.63 |- ~l0 d \/ n1 d c c % 0.47/0.63 |- ~l0 b \/ n1 e c c % 0.47/0.63 |- ~l0 d \/ n1 e c c % 0.47/0.63 |- ~l0 e \/ n1 e c c % 0.47/0.63 |- n1 a $_663 $_663 % 0.47/0.63 |- n1 c $_666 $_666 % 0.47/0.63 |- ~r2 $_670 \/ ~r3 $_670 $_671 $_671 \/ r3 $_671 $_670 $_670 % 0.47/0.63 |- ~k2 $_669 a \/ r3 a $_669 a % 0.47/0.63 |- ~k2 $_669 c \/ r3 c $_669 c % 0.47/0.63 |- ~k2 $_669 $_671 \/ ~r2 $_671 \/ r3 $_671 $_669 $_671 % 0.47/0.63 |- q2 a c a % 0.47/0.63 |- ~r2 $I \/ q3 $I $I % 0.47/0.63 |- q2 d c d % 0.47/0.63 |- q3 c d % 0.47/0.63 |- q3 d c % 0.47/0.63 |- q3 c c % 0.47/0.63 |- ~n0 a c \/ q3 c a % 0.47/0.63 |- q3 a a % 0.47/0.63 |- q2 b c b % 0.47/0.63 |- l2 $_367 b % 0.47/0.63 |- ~n0 b c \/ q3 c b % 0.47/0.63 |- s2 c % 0.47/0.63 |- ~s2 $H \/ r3 b $H $H % 0.47/0.63 |- ~l1 e c \/ p2 a c b % 0.47/0.63 |- ~k1 $_688 \/ q2 b c $_688 % 0.47/0.63 |- r3 b c c % 0.47/0.63 |- r3 b d d % 0.47/0.63 |- ~k2 $A b \/ ~r2 b \/ r3 c $A b % 0.47/0.63 |- ~r2 b \/ r3 d b b % 0.47/0.64 |- ~k2 $A b \/ ~r2 b \/ r3 d $A b % 0.47/0.64 |- q2 b c a % 0.47/0.64 |- q2 b c c % 0.47/0.64 |- q2 b c d % 0.47/0.64 |- q2 b c e % 0.47/0.64 |- m3 c b d % 0.47/0.64 |- ~n0 b c \/ q3 c e % 0.47/0.64 |- ~n0 b c \/ q3 c a % 0.47/0.64 |- ~k1 $_715 \/ ~m1 $_716 $_715 $_714 \/ k2 $_714 $_715 % 0.47/0.64 |- ~k1 $_717 \/ ~k2 $_717 $_715 \/ k2 b $_715 % 0.47/0.64 |- ~k1 $_717 \/ ~k2 $_717 $_715 \/ k2 e $_715 % 0.47/0.64 |- k2 e a % 0.47/0.64 |- p3 d e a % 0.47/0.64 |- k2 e b % 0.47/0.64 |- p3 d e b % 0.47/0.64 |- ~r2 b \/ r3 d e b % 0.47/0.64 |- ~r2 b \/ r3 c e b % 0.47/0.64 |- k2 c b % 0.47/0.64 |- p3 d c b % 0.47/0.64 |- ~r2 b \/ r3 d c b % 0.47/0.64 |- ~r2 $H \/ m3 $H b $H % 0.47/0.64 |- p3 b c b % 0.47/0.64 |- m3 c b c % 0.47/0.64 |- k2 c a % 0.47/0.64 |- p3 d c a % 0.47/0.64 |- r3 a c a % 0.47/0.64 |- ~r2 $H \/ m3 $H a $H % 0.47/0.64 |- p2 b c a % 0.47/0.64 |- m3 c a c % 0.47/0.64 |- k2 e c % 0.47/0.64 |- p3 d e c % 0.47/0.64 |- k2 b a % 0.47/0.64 |- p3 d b a % 0.47/0.64 |- k2 a b % 0.47/0.64 |- p3 d a b % 0.47/0.64 |- k3 b b a % 0.47/0.64 |- ~r2 b \/ r3 d a b % 0.47/0.64 |- ~r2 b \/ r3 c a b % 0.47/0.64 |- p4 b a b % 0.47/0.64 |- k2 a e % 0.47/0.64 |- p3 d a e % 0.47/0.64 |- k3 e e a % 0.47/0.64 |- p4 e a e % 0.47/0.64 |- k2 b c % 0.47/0.64 |- p3 d b c % 0.47/0.64 |- k2 c e % 0.47/0.64 |- p3 d c e % 0.47/0.64 |- ~r2 $H \/ m3 $H e $H % 0.48/0.64 |- m3 c e c % 0.48/0.64 |- k2 b e % 0.48/0.64 |- ~k1 $_731 \/ k2 b $_731 % 0.48/0.64 |- p3 d b e % 0.48/0.64 |- ~k1 $_734 \/ k2 e $_734 % 0.48/0.64 |- k2 $_737 d % 0.48/0.64 |- ~r2 $H \/ m3 $H d $H % 0.48/0.64 |- ~r2 d \/ ~r3 d $J $J \/ r3 $J $_739 d % 0.48/0.64 |- p3 d $_739 d % 0.48/0.64 |- ~q2 $F d $C \/ p3 $C $_739 d % 0.48/0.64 |- k3 d d $_739 % 0.48/0.64 |- ~r2 d \/ p3 $_741 d d % 0.48/0.64 |- p4 d $_741 d % 0.48/0.64 |- m3 c d c % 0.48/0.64 |- ~s2 $H \/ r3 c $H $H % 0.48/0.64 |- r3 c b b % 0.48/0.64 |- r3 c d d % 0.48/0.64 |- r3 d c c % 0.48/0.64 |- ~k2 $A c \/ r3 d $A c % 0.48/0.64 |- ~k2 $A c \/ r3 b $A c % 0.48/0.64 |- ~r2 d \/ r3 c $_739 d % 0.48/0.64 |- q2 e c e % 0.48/0.64 |- l2 $_367 e % 0.48/0.64 |- ~s2 $H \/ r3 e $H $H % 0.48/0.64 |- ~k1 $_760 \/ q2 e c $_760 % 0.48/0.64 |- ~n0 e c \/ q3 c e % 0.48/0.64 |- q2 e c a % 0.48/0.64 |- q2 e c b % 0.48/0.64 |- q2 e c c % 0.48/0.64 |- q2 e c d % 0.48/0.64 |- ~n0 e c \/ q3 c a % 0.48/0.64 |- ~n0 e c \/ q3 c b % 0.48/0.64 |- l2 $_764 $_764 % 0.48/0.64 |- ~n0 e $_765 \/ l2 $D $_765 % 0.48/0.64 |- ~s4 $F \/ p5 $_765 $_765 $F % 0.48/0.64 |- ~k1 $_765 \/ q2 $_765 c $_765 % 0.48/0.64 |- r3 b b c % 0.48/0.64 |- r3 b e c % 0.48/0.64 |- p4 c b b % 0.48/0.64 |- ~r0 c \/ m5 c b % 0.48/0.64 |- r3 e b b % 0.48/0.64 |- r3 e c c % 0.48/0.64 |- r3 e d d % 0.48/0.64 |- ~k2 $A e \/ ~r2 e \/ r3 b $A e % 0.48/0.64 |- ~k2 $A e \/ ~r2 e \/ r3 c $A e % 0.48/0.64 |- ~r2 e \/ r3 d e e % 0.48/0.64 |- ~k2 $A e \/ ~r2 e \/ r3 d $A e % 0.48/0.64 |- r3 d b c % 0.48/0.64 |- r3 d e c % 0.48/0.64 |- p5 $_780 $_780 a % 0.48/0.64 |- p5 $_780 $_780 b % 0.48/0.64 |- p5 $_780 $_780 c % 0.48/0.64 |- p5 $_780 $_780 d % 0.48/0.64 |- p5 $_780 $_780 e % 0.48/0.64 |- ~r2 e \/ r3 b a e % 0.48/0.64 |- ~r2 e \/ r3 b b e % 0.48/0.64 |- ~r2 e \/ r3 b c e % 0.48/0.64 |- ~r2 e \/ r3 c a e % 0.48/0.64 |- ~r2 e \/ r3 c b e % 0.48/0.64 |- ~r2 e \/ r3 c c e % 0.48/0.64 |- ~r2 e \/ r3 d a e % 0.48/0.64 |- ~r2 e \/ r3 d b e % 0.48/0.64 |- ~r2 e \/ r3 d c e % 0.48/0.64 |- ~p0 $_790 $_791 \/ ~p2 $_790 $_791 $_790 \/ p2 $_790 $_791 $_791 % 0.48/0.64 |- m3 b b c % 0.48/0.64 |- ~m2 $_809 \/ k3 b b $_809 % 0.48/0.64 |- k3 $_813 $_813 d % 0.48/0.64 |- p4 $_815 d $_815 % 0.48/0.64 |- k3 a a $_817 % 0.48/0.64 |- p3 $_819 a a % 0.48/0.64 |- p4 a $_819 a % 0.48/0.64 |- n4 $_820 a % 0.48/0.64 |- ~n1 $_824 $_823 a \/ ~q2 $_824 a $_823 \/ q2 $_823 $_824 $_823 % 0.48/0.64 |- ~n1 $_824 $_823 b \/ ~q2 $_824 b $_823 \/ q2 $_823 $_824 $_823 % 0.48/0.64 |- ~n1 $_824 $_825 $_825 \/ ~q2 $_824 $_825 $_825 \/ q2 $_825 $_824 $_825 % 0.48/0.64 |- ~n1 $_824 b b \/ q2 b $_824 b % 0.48/0.64 |- ~n1 $_824 e e \/ q2 e $_824 e % 0.48/0.64 |- ~n1 $_825 d $_825 \/ q2 d $_825 d % 0.48/0.64 |- q2 d a d % 0.48/0.64 |- ~n0 d a \/ q3 a d % 0.48/0.64 |- q2 b a b % 0.48/0.64 |- q3 a b % 0.48/0.64 |- s2 a % 0.48/0.64 |- q3 b a % 0.48/0.64 |- r3 e a a % 0.48/0.64 |- r3 c a a % 0.48/0.64 |- r3 b a a % 0.48/0.64 |- ~r2 e \/ r3 a e e % 0.48/0.64 |- ~k2 $A e \/ ~r2 e \/ r3 a $A e % 0.48/0.64 |- r3 a c c % 0.48/0.64 |- ~k2 $A c \/ r3 a $A c % 0.48/0.64 |- ~k2 $A a \/ r3 c $A a % 0.48/0.64 |- ~r2 b \/ r3 a b b % 0.48/0.64 |- ~k2 $A b \/ ~r2 b \/ r3 a $A b % 0.48/0.64 |- r3 a b c % 0.48/0.64 |- r3 a e c % 0.48/0.64 |- q2 e a e % 0.48/0.64 |- q2 e d e % 0.48/0.64 |- ~n0 e a \/ q3 a e % 0.48/0.64 |- p3 e $_739 d % 0.48/0.64 |- ~p2 d b c \/ p3 e d e % 0.48/0.64 |- p3 e $_441 $_441 % 0.48/0.64 |- ~k2 $D $E \/ p3 e $D $E % 0.48/0.64 |- n4 e $_831 % 0.48/0.64 |- r3 c b a % 0.48/0.64 |- r3 c c a % 0.48/0.64 |- r3 c e a % 0.48/0.64 |- p4 a c c % 0.48/0.64 |- ~r0 a \/ m5 a c % 0.48/0.64 |- p3 e a b % 0.48/0.64 |- p3 e a e % 0.48/0.64 |- p3 e b a % 0.48/0.64 |- p3 e b c % 0.48/0.64 |- p3 e c a % 0.48/0.64 |- p3 e c b % 0.48/0.64 |- p3 e c e % 0.48/0.64 |- p3 e e a % 0.48/0.64 |- p3 e e b % 0.48/0.64 |- p3 e e c % 0.48/0.64 |- ~r2 e \/ r3 a b e % 0.48/0.64 |- ~r2 e \/ r3 a c e % 0.48/0.64 |- ~r2 b \/ r3 a c b % 0.48/0.64 |- ~r2 b \/ r3 a e b % 0.48/0.64 |- ~n0 $_847 a \/ k3 $_847 c $_847 % 0.48/0.64 |- ~n0 $_847 b \/ k3 $_847 c $_847 % 0.48/0.64 |- ~n0 $_847 d \/ k3 $_847 $_844 $_847 % 0.48/0.64 |- ~n0 $_847 $_846 \/ k3 $_847 $_846 $_847 % 0.48/0.64 |- ~n0 $_847 e \/ k3 $_847 c $_847 % 0.48/0.64 |- ~n0 $_847 $_846 \/ k3 $_847 a $_847 % 0.48/0.64 |- ~n0 $_847 $_846 \/ k3 $_847 b $_847 % 0.48/0.64 |- ~n0 $_847 $_846 \/ k3 $_847 e $_847 % 0.48/0.64 |- m3 b b a % 0.48/0.64 |- k3 d a d % 0.48/0.65 |- ~r2 d \/ p3 d d a % 0.48/0.65 |- m3 d d a % 0.48/0.65 |- k3 d b d % 0.48/0.65 |- ~r2 d \/ p3 d d b % 0.48/0.65 |- ~r2 b \/ m3 d d b % 0.48/0.65 |- k3 d c d % 0.48/0.65 |- ~r2 d \/ p3 d d c % 0.48/0.65 |- m3 d d c % 0.48/0.65 |- m3 a a c % 0.48/0.65 |- l3 d c % 0.48/0.65 |- k3 c $_866 c % 0.48/0.65 |- p3 c c $_868 % 0.48/0.65 |- ~r2 $_868 \/ m3 c c $_868 % 0.48/0.65 |- m3 c c a % 0.48/0.65 |- s3 a $_880 % 0.48/0.65 |- m4 $_881 $_765 % 0.48/0.65 |- ~s4 $B \/ m5 $B $B % 0.48/0.65 |- s3 b $_890 % 0.48/0.65 |- m5 a a % 0.48/0.65 |- m5 d d % 0.48/0.65 |- s3 d $_894 % 0.48/0.65 |- s3 c $_897 % 0.48/0.65 |- ~s2 $_904 \/ s3 $_904 $_905 % 0.48/0.65 |- ~m3 $_914 b $_912 \/ r3 $_912 $_912 b % 0.48/0.65 |- ~m3 $_914 b $_912 \/ r3 $_912 $_912 d % 0.48/0.65 |- ~m2 $_911 \/ ~m3 $_914 b $_912 \/ r3 $_912 $_912 $_911 % 0.48/0.65 |- r3 a a b % 0.48/0.65 |- r3 c c b % 0.48/0.65 |- r3 d d b % 0.48/0.65 |- p4 b c c % 0.48/0.65 |- p4 b a a % 0.48/0.65 |- p4 b d d % 0.48/0.65 |- r3 a a d % 0.48/0.65 |- r3 b b d % 0.48/0.65 |- r3 c c d % 0.48/0.65 |- p4 d a a % 0.48/0.65 |- p4 d b b % 0.48/0.65 |- p4 d c c % 0.48/0.65 |- ~r0 d \/ m5 d a % 0.48/0.65 |- ~r0 d \/ m5 d b % 0.48/0.65 |- ~r0 d \/ m5 d c % 0.48/0.65 |- ~m2 $_921 \/ r3 b b $_921 % 0.48/0.65 |- ~m2 $_928 \/ r3 a a $_928 % 0.48/0.65 |- ~m2 $_928 \/ r3 c c $_928 % 0.48/0.65 |- ~m2 $_928 \/ r3 d d $_928 % 0.48/0.65 |- ~l1 $_936 b \/ ~p2 a $_935 a \/ p2 a $_935 $_935 % 0.48/0.65 |- ~l1 $_936 b \/ ~p2 b $_935 b \/ p2 b $_935 $_935 % 0.48/0.65 |- ~l1 $_936 c \/ ~p2 b $_935 b \/ p2 b $_935 $_935 % 0.48/0.65 |- ~l1 $_936 d \/ ~p2 e $_935 e \/ p2 e $_935 $_935 % 0.48/0.65 |- ~l1 $_936 a \/ ~p2 $_934 $_935 $_934 \/ p2 $_934 $_935 $_935 % 0.48/0.65 |- ~l1 $_937 $_937 \/ ~p2 $_937 $_935 $_937 \/ p2 $_937 $_935 $_935 % 0.48/0.65 |- p2 $_960 a a % 0.48/0.65 |- r3 $_962 a $_962 % 0.48/0.65 |- k3 a $_962 a % 0.48/0.65 |- p3 a a $_963 % 0.48/0.65 |- ~r2 $_963 \/ m3 a a $_963 % 0.48/0.65 |- ~r0 a \/ p4 a a $_965 % 0.48/0.65 |- p2 $_968 b b % 0.48/0.65 |- p3 $_970 b b % 0.48/0.65 |- r3 $_970 b $_970 % 0.48/0.65 |- k3 b $_970 b % 0.48/0.65 |- n4 $_971 b % 0.48/0.65 |- ~r2 b \/ p3 b b $_973 % 0.48/0.65 |- ~r2 $_973 \/ m3 b b $_973 % 0.48/0.65 |- p4 b b $_974 % 0.48/0.65 |- m5 b $_975 % 0.48/0.65 |- p2 $_979 e e % 0.48/0.65 |- p3 $_981 e e % 0.48/0.65 |- r3 $_981 e $_981 % 0.48/0.65 |- k3 e $_981 e % 0.48/0.65 |- m3 $_981 e e % 0.48/0.65 |- n4 $_982 e % 0.48/0.65 |- ~r2 e \/ p3 e e $_984 % 0.48/0.65 |- ~r2 $_984 \/ m3 e e $_984 % 0.48/0.65 |- p4 e e $_985 % 0.48/0.65 |- m5 e $_987 % 0.48/0.65 |- ~q1 c $_991 a \/ ~s0 e \/ p2 $_991 $_991 $_992 % 0.48/0.65 |- ~q1 c $_991 b \/ ~s0 e \/ p2 $_991 $_991 $_992 % 0.48/0.65 |- ~q1 c $_991 e \/ ~s0 e \/ p2 $_991 $_991 $_992 % 0.48/0.65 |- ~q1 c $_993 $_993 \/ ~s0 e \/ p2 $_993 $_993 $_992 % 0.48/0.65 |- ~s0 e \/ p2 b b $_992 % 0.48/0.65 |- ~s0 e \/ p2 c c $_992 % 0.48/0.65 |- ~s0 e \/ p2 d d $_992 % 0.48/0.65 |- ~s0 e \/ p2 e e $_992 % 0.48/0.65 |- ~s0 e \/ p2 a a $_992 % 0.48/0.65 |- ~q0 $_1010 $_1007 \/ k3 $_1008 $_1008 $_1007 % 0.48/0.65 |- k3 $_1012 $_1012 b % 0.48/0.65 |- ~r2 $_1014 \/ p3 b $_1014 $_1014 % 0.48/0.65 |- p4 $_1014 b $_1014 % 0.48/0.65 |- k3 $_1017 $_1017 e % 0.48/0.65 |- p4 $_1019 e $_1019 % 0.48/0.65 |- k3 $_1022 $_1022 c % 0.48/0.65 |- ~r2 $_1024 \/ p3 c $_1024 $_1024 % 0.48/0.65 |- p4 $_1024 c $_1024 % 0.48/0.65 |- ~l0 $_1027 \/ ~q0 $_1028 $_1028 \/ ~r0 $_1029 \/ q1 $_1027 $_1028 $_1027 % 0.48/0.65 |- q4 $I $I % 0.48/0.65 |- ~k1 $H \/ l5 $H % 0.48/0.65 |- p5 $I $_1040 $I % 0.48/0.65 |- l5 a % 0.48/0.65 |- l5 b % 0.48/0.65 |- l5 c % 0.48/0.65 |- l5 d % 0.48/0.65 |- l5 e % 0.48/0.65 |- q4 b c % 0.48/0.65 |- q4 e c % 0.48/0.65 |- q4 b a % 0.48/0.65 |- q4 e a % 0.48/0.65 |- q4 e d % 0.48/0.65 |- q4 d $_1055 % 0.48/0.65 |- q4 a c % 0.48/0.65 |- p5 $_1062 $_1064 $_1064 % 0.48/0.65 |- ~q2 $_1085 $_1083 $_1082 \/ q4 $_1082 $_1083 % 0.48/0.65 |- ~k0 $_1090 \/ q2 $_1089 $_1090 $_1089 % 0.48/0.65 |- q2 $_1096 b $_1096 % 0.48/0.65 |- q2 $_1096 e $_1096 % 0.48/0.65 |- s2 e % 0.48/0.65 |- q4 $_1098 e % 0.48/0.65 |- s3 e $_878 % 0.48/0.65 |- ~n0 $_1098 e \/ q3 e $_1098 % 0.48/0.65 |- r3 c e e % 0.48/0.65 |- r3 b e e % 0.48/0.65 |- ~k2 $A c \/ r3 e $A c % 0.48/0.65 |- ~k2 $A b \/ ~r2 b \/ r3 e $A b % 0.48/0.65 |- q4 $_1101 b % 0.48/0.65 |- ~n0 $_1101 b \/ q3 b $_1101 % 0.48/0.65 |- q3 b d % 0.48/0.65 |- q3 d b % 0.48/0.65 |- r3 e b c % 0.48/0.65 |- r3 e e c % 0.48/0.65 |- p4 c e e % 0.48/0.65 |- ~r0 c \/ m5 c e % 0.48/0.65 |- ~r2 b \/ r3 e a b % 0.48/0.65 |- ~r2 b \/ r3 e c b % 0.48/0.65 |- ~l2 $_1109 $_1110 \/ ~m0 $_1110 $_1109 $_1109 \/ m3 $_1110 $_1107 $_1110 % 0.48/0.65 |- m3 a $_1114 a % 0.48/0.65 |- m3 b $_1117 b % 0.48/0.65 |- ~l2 d $_1125 \/ m3 $_1125 $_1123 $_1125 % 0.48/0.65 |- m3 e $_1126 e % 0.48/0.65 |- m3 d $_1126 d % 0.48/0.65 |- ~m2 $_911 \/ r3 e e $_911 % 0.48/0.65 |- r3 e e d % 0.48/0.65 |- r3 e e b % 0.48/0.65 |- p4 d e e % 0.48/0.65 |- ~r0 d \/ m5 d e % 0.48/0.65 |- p4 b e e % 0.48/0.65 |- n5 $_1156 $_1157 % 0.48/0.65 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.48/0.65 %------------------------------------------------------------------------------