%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : KRS009-1 : TPTP v8.1.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n018.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 : Sun Jul 17 03:18:25 EDT 2022 % Result : Satisfiable 0.18s 0.44s % Output : Saturation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : KRS009-1 : TPTP v8.1.0. Released v2.0.0. % 0.07/0.12 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n018.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 Jun 7 07:48:50 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.18/0.44 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.44 % 0.18/0.44 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.44 |- ~c $X1 \/ p2least $X1 % 0.18/0.44 |- ~p2least $X1 \/ c $X1 % 0.18/0.44 |- ~(u1r2 $X1 == u1r1 $X1) \/ ~p2least $X1 % 0.18/0.44 |- ~p2least $X1 \/ p $X1 (u1r1 $X1) % 0.18/0.45 |- ~p2least $X1 \/ p $X1 (u1r2 $X1) % 0.18/0.45 |- ~p $X1 $X2 \/ ~p $X1 $X3 \/ $X3 == $X2 \/ p2least $X1 % 0.18/0.45 |- ~d $X1 \/ p1most $X1 % 0.18/0.45 |- ~p1most $X1 \/ d $X1 % 0.18/0.45 |- ~p $X1 $X2 \/ ~p $X1 $X3 \/ ~p1most $X1 \/ $X3 == $X2 % 0.18/0.45 |- ~(u3r2 $X1 == u3r1 $X1) \/ p1most $X1 % 0.18/0.45 |- p $X1 (u3r1 $X1) \/ p1most $X1 % 0.18/0.45 |- p $X1 (u3r2 $X1) \/ p1most $X1 % 0.18/0.45 |- ~r $X1 $X2 \/ c $X2 % 0.18/0.45 |- ~r $X1 $X2 \/ t $X1 $X2 % 0.18/0.45 |- ~s $X1 $X2 \/ d $X2 % 0.18/0.45 |- ~s $X1 $X2 \/ t $X1 $X2 % 0.18/0.45 |- ~e $X1 \/ s1most $X1 % 0.18/0.45 |- ~e $X1 \/ r1most $X1 % 0.18/0.45 |- ~e $X1 \/ t3least $X1 % 0.18/0.45 |- ~(u8r2 $X1 == u8r1 $X1) \/ ~t3least $X1 % 0.18/0.45 |- ~(u8r3 $X1 == u8r1 $X1) \/ ~t3least $X1 % 0.18/0.45 |- ~(u8r3 $X1 == u8r2 $X1) \/ ~t3least $X1 % 0.18/0.45 |- ~t3least $X1 \/ t $X1 (u8r1 $X1) % 0.18/0.45 |- ~t3least $X1 \/ t $X1 (u8r2 $X1) % 0.18/0.45 |- ~t3least $X1 \/ t $X1 (u8r3 $X1) % 0.18/0.45 |- ~t $X1 $X2 \/ ~t $X1 $X3 \/ ~t $X1 $X4 \/ $X3 == $X2 \/ $X4 == $X2 \/ % 0.18/0.45 $X4 == $X3 \/ t3least $X1 % 0.18/0.45 |- ~r $X1 $X2 \/ ~r $X1 $X3 \/ ~r1most $X1 \/ $X3 == $X2 % 0.18/0.45 |- ~(u9r2 $X1 == u9r1 $X1) \/ r1most $X1 % 0.18/0.45 |- r $X1 (u9r1 $X1) \/ r1most $X1 % 0.18/0.45 |- r $X1 (u9r2 $X1) \/ r1most $X1 % 0.18/0.45 |- ~s $X1 $X2 \/ ~s $X1 $X3 \/ ~s1most $X1 \/ $X3 == $X2 % 0.18/0.45 |- ~(u10r2 $X1 == u10r1 $X1) \/ s1most $X1 % 0.18/0.45 |- s $X1 (u10r1 $X1) \/ s1most $X1 % 0.18/0.45 |- s $X1 (u10r2 $X1) \/ s1most $X1 % 0.18/0.45 |- ~p $X1 $X3 \/ $X3 == $X3 \/ p2least $X1 % 0.18/0.45 |- ~p $X1 $X3 \/ ~p1most $X1 \/ $X3 == $X3 % 0.18/0.45 |- ~r $X1 $X3 \/ ~r1most $X1 \/ $X3 == $X3 % 0.18/0.45 |- ~s $X1 $X3 \/ ~s1most $X1 \/ $X3 == $X3 % 0.18/0.45 |- ~t $X1 $X4 \/ $X4 == $X4 \/ t3least $X1 % 0.18/0.45 |- e exist % 0.18/0.45 |- s1most exist % 0.18/0.45 |- r1most exist % 0.18/0.45 |- t3least exist % 0.18/0.45 |- t exist (u8r1 exist) % 0.18/0.45 |- t exist (u8r3 exist) % 0.18/0.45 |- t exist (u8r2 exist) % 0.18/0.45 |- c (u9r1 $_19) \/ r1most $_19 % 0.18/0.45 |- p2least (u9r1 $_20) \/ r1most $_20 % 0.18/0.45 |- p (u9r1 $_21) (u1r2 (u9r1 $_21)) \/ r1most $_21 % 0.18/0.45 |- p (u9r1 $_21) (u1r1 (u9r1 $_21)) \/ r1most $_21 % 0.18/0.45 |- c (u9r2 $_23) \/ r1most $_23 % 0.18/0.45 |- p2least (u9r2 $_24) \/ r1most $_24 % 0.18/0.45 |- p (u9r2 $_25) (u1r2 (u9r2 $_25)) \/ r1most $_25 % 0.18/0.45 |- p (u9r2 $_25) (u1r1 (u9r2 $_25)) \/ r1most $_25 % 0.18/0.45 |- d (u10r1 $_35) \/ s1most $_35 % 0.18/0.45 |- d (u10r2 $_35) \/ s1most $_35 % 0.18/0.45 |- p1most (u10r2 $_37) \/ s1most $_37 % 0.18/0.45 |- p1most (u10r1 $_39) \/ s1most $_39 % 0.18/0.45 |- r1most $_44 \/ t $_44 (u9r1 $_44) % 0.18/0.45 |- r1most $_44 \/ t $_44 (u9r2 $_44) % 0.18/0.45 |- s1most $_48 \/ t $_48 (u10r1 $_48) % 0.18/0.45 |- s1most $_48 \/ t $_48 (u10r2 $_48) % 0.18/0.45 |- ~p1most (u9r1 $_21) \/ u1r1 (u9r1 $_21) == u1r1 (u9r1 $_21) \/ % 0.18/0.45 r1most $_21 % 0.18/0.45 |- ~p1most (u9r1 $_21) \/ u1r2 (u9r1 $_21) == u1r2 (u9r1 $_21) \/ % 0.18/0.45 r1most $_21 % 0.18/0.45 |- ~p1most (u9r2 $_25) \/ u1r1 (u9r2 $_25) == u1r1 (u9r2 $_25) \/ % 0.18/0.45 r1most $_25 % 0.18/0.45 |- ~p1most (u9r2 $_25) \/ u1r2 (u9r2 $_25) == u1r2 (u9r2 $_25) \/ % 0.18/0.45 r1most $_25 % 0.18/0.45 |- u10r1 $_68 == u10r1 $_68 \/ s1most $_68 \/ t3least $_68 % 0.18/0.45 |- u10r2 $_68 == u10r2 $_68 \/ s1most $_68 \/ t3least $_68 % 0.18/0.45 |- u9r1 $_68 == u9r1 $_68 \/ r1most $_68 \/ t3least $_68 % 0.18/0.45 |- u9r2 $_68 == u9r2 $_68 \/ r1most $_68 \/ t3least $_68 % 0.18/0.45 |- ~p (u9r1 $_21) $_85 \/ ~p1most (u9r1 $_21) \/ % 0.18/0.45 $_85 == u1r1 (u9r1 $_21) \/ r1most $_21 % 0.18/0.45 |- ~p (u9r1 $_21) $_85 \/ ~p1most (u9r1 $_21) \/ % 0.18/0.45 $_85 == u1r2 (u9r1 $_21) \/ r1most $_21 % 0.18/0.45 |- ~p (u9r2 $_25) $_85 \/ ~p1most (u9r2 $_25) \/ % 0.18/0.45 $_85 == u1r1 (u9r2 $_25) \/ r1most $_25 % 0.18/0.45 |- ~p (u9r2 $_25) $_85 \/ ~p1most (u9r2 $_25) \/ % 0.18/0.45 $_85 == u1r2 (u9r2 $_25) \/ r1most $_25 % 0.18/0.45 |- ~p (u9r1 $_21) $_84 \/ ~p1most (u9r1 $_21) \/ % 0.18/0.45 u1r1 (u9r1 $_21) == $_84 \/ r1most $_21 % 0.18/0.45 |- ~p (u9r1 $_21) $_84 \/ ~p1most (u9r1 $_21) \/ % 0.18/0.45 u1r2 (u9r1 $_21) == $_84 \/ r1most $_21 % 0.18/0.45 |- ~p (u9r2 $_25) $_84 \/ ~p1most (u9r2 $_25) \/ % 0.18/0.45 u1r1 (u9r2 $_25) == $_84 \/ r1most $_25 % 0.18/0.45 |- ~p (u9r2 $_25) $_84 \/ ~p1most (u9r2 $_25) \/ % 0.18/0.45 u1r2 (u9r2 $_25) == $_84 \/ r1most $_25 % 0.18/0.45 |- p1most $_94 \/ p2least $_94 % 0.18/0.45 |- p $_95 (u1r2 $_95) \/ p1most $_95 % 0.18/0.45 |- p $_95 (u1r1 $_95) \/ p1most $_95 % 0.18/0.45 |- c $_95 \/ p1most $_95 % 0.18/0.45 |- c $_96 \/ d $_96 % 0.18/0.45 |- a $_98 % 0.18/0.45 |- ~r1most $X1 \/ ~s1most $X1 \/ ~t3least $X1 \/ e $X1 % 0.18/0.45 |- ~p1most (u9r1 $_103) \/ u1r2 (u9r1 $_103) == u1r1 (u9r1 $_103) \/ % 0.18/0.45 r1most $_103 % 0.18/0.45 |- ~p1most (u9r1 $_106) \/ u1r1 (u9r1 $_106) == u1r2 (u9r1 $_106) \/ % 0.18/0.45 r1most $_106 % 0.18/0.45 |- ~p1most (u9r2 $_109) \/ u1r2 (u9r2 $_109) == u1r1 (u9r2 $_109) \/ % 0.18/0.45 r1most $_109 % 0.18/0.45 |- ~p1most (u9r2 $_112) \/ u1r1 (u9r2 $_112) == u1r2 (u9r2 $_112) \/ % 0.18/0.45 r1most $_112 % 0.18/0.45 |- ~t $_123 $_125 \/ ~t $_123 $_126 \/ $_125 == u10r1 $_123 \/ % 0.18/0.45 $_126 == $_125 \/ $_126 == u10r1 $_123 \/ s1most $_123 \/ t3least $_123 % 0.18/0.45 |- ~t $_123 $_125 \/ ~t $_123 $_126 \/ $_125 == u10r2 $_123 \/ % 0.18/0.45 $_126 == $_125 \/ $_126 == u10r2 $_123 \/ s1most $_123 \/ t3least $_123 % 0.18/0.45 |- ~t $_123 $_125 \/ ~t $_123 $_126 \/ $_125 == u9r1 $_123 \/ % 0.18/0.45 $_126 == $_125 \/ $_126 == u9r1 $_123 \/ r1most $_123 \/ t3least $_123 % 0.18/0.45 |- ~t $_123 $_125 \/ ~t $_123 $_126 \/ $_125 == u9r2 $_123 \/ % 0.18/0.45 $_126 == $_125 \/ $_126 == u9r2 $_123 \/ r1most $_123 \/ t3least $_123 % 0.18/0.45 |- ~t $_123 $_124 \/ ~t $_123 $_126 \/ $_126 == $_124 \/ % 0.18/0.45 $_126 == u10r1 $_123 \/ u10r1 $_123 == $_124 \/ s1most $_123 \/ % 0.18/0.45 t3least $_123 % 0.18/0.45 |- ~t $_123 $_124 \/ ~t $_123 $_126 \/ $_126 == $_124 \/ % 0.18/0.45 $_126 == u10r2 $_123 \/ u10r2 $_123 == $_124 \/ s1most $_123 \/ % 0.18/0.45 t3least $_123 % 0.18/0.45 |- ~t $_123 $_124 \/ ~t $_123 $_126 \/ $_126 == $_124 \/ % 0.18/0.45 $_126 == u9r1 $_123 \/ u9r1 $_123 == $_124 \/ r1most $_123 \/ % 0.18/0.45 t3least $_123 % 0.18/0.45 |- ~t $_123 $_124 \/ ~t $_123 $_126 \/ $_126 == $_124 \/ % 0.18/0.45 $_126 == u9r2 $_123 \/ u9r2 $_123 == $_124 \/ r1most $_123 \/ % 0.18/0.45 t3least $_123 % 0.18/0.45 |- ~t $_123 $_124 \/ ~t $_123 $_125 \/ $_125 == $_124 \/ % 0.18/0.45 u10r1 $_123 == $_124 \/ u10r1 $_123 == $_125 \/ s1most $_123 \/ % 0.18/0.45 t3least $_123 % 0.18/0.45 |- ~t $_123 $_124 \/ ~t $_123 $_125 \/ $_125 == $_124 \/ % 0.18/0.45 u10r2 $_123 == $_124 \/ u10r2 $_123 == $_125 \/ s1most $_123 \/ % 0.18/0.45 t3least $_123 % 0.18/0.45 |- ~t $_123 $_124 \/ ~t $_123 $_125 \/ $_125 == $_124 \/ % 0.18/0.45 u9r1 $_123 == $_124 \/ u9r1 $_123 == $_125 \/ r1most $_123 \/ % 0.18/0.45 t3least $_123 % 0.18/0.45 |- ~t $_123 $_124 \/ ~t $_123 $_125 \/ $_125 == $_124 \/ % 0.18/0.45 u9r2 $_123 == $_124 \/ u9r2 $_123 == $_125 \/ r1most $_123 \/ % 0.18/0.45 t3least $_123 % 0.18/0.45 |- ~t $_127 $_129 \/ $_129 == u10r1 $_127 \/ $_129 == u10r2 $_127 \/ % 0.18/0.45 u10r2 $_127 == u10r1 $_127 \/ s1most $_127 \/ t3least $_127 % 0.18/0.45 |- ~t $_127 $_128 \/ $_128 == u10r1 $_127 \/ u10r2 $_127 == $_128 \/ % 0.18/0.45 u10r2 $_127 == u10r1 $_127 \/ s1most $_127 \/ t3least $_127 % 0.18/0.45 |- ~t $_127 $_128 \/ $_128 == u10r1 $_127 \/ u9r2 $_127 == $_128 \/ % 0.18/0.45 u9r2 $_127 == u10r1 $_127 \/ r1most $_127 \/ s1most $_127 \/ % 0.18/0.45 t3least $_127 % 0.18/0.45 |- u10r2 $_130 == u10r1 $_130 \/ u9r2 $_130 == u10r1 $_130 \/ % 0.18/0.45 u9r2 $_130 == u10r2 $_130 \/ r1most $_130 \/ s1most $_130 \/ % 0.18/0.45 t3least $_130 % 0.18/0.45 |- u9r1 $_133 == u10r1 $_133 \/ u9r2 $_133 == u10r1 $_133 \/ % 0.18/0.45 r1most $_133 \/ s1most $_133 \/ t3least $_133 % 0.18/0.45 |- u10r2 $_135 == u10r1 $_135 \/ u9r1 $_135 == u10r1 $_135 \/ % 0.18/0.45 u9r1 $_135 == u10r2 $_135 \/ r1most $_135 \/ s1most $_135 \/ % 0.18/0.45 t3least $_135 % 0.18/0.45 |- u10r2 $_138 == u10r1 $_138 \/ u10r2 $_138 == u9r1 $_138 \/ % 0.18/0.45 u9r1 $_138 == u10r1 $_138 \/ r1most $_138 \/ s1most $_138 \/ % 0.18/0.45 t3least $_138 % 0.18/0.45 |- u10r2 $_138 == u10r1 $_138 \/ u10r2 $_138 == u9r2 $_138 \/ % 0.18/0.45 u9r2 $_138 == u10r1 $_138 \/ r1most $_138 \/ s1most $_138 \/ % 0.18/0.45 t3least $_138 % 0.18/0.45 |- ~t $_142 $_144 \/ $_144 == u10r1 $_142 \/ $_144 == u10r2 $_142 \/ % 0.18/0.45 u10r1 $_142 == u10r2 $_142 \/ s1most $_142 \/ t3least $_142 % 0.18/0.45 |- ~t $_142 $_143 \/ $_143 == u10r2 $_142 \/ u10r1 $_142 == $_143 \/ % 0.18/0.45 u10r1 $_142 == u10r2 $_142 \/ s1most $_142 \/ t3least $_142 % 0.18/0.45 |- u10r1 $_145 == u10r2 $_145 \/ u9r1 $_145 == u10r1 $_145 \/ % 0.18/0.45 u9r1 $_145 == u10r2 $_145 \/ r1most $_145 \/ s1most $_145 \/ % 0.18/0.45 t3least $_145 % 0.18/0.45 |- u10r1 $_145 == u10r2 $_145 \/ u9r2 $_145 == u10r1 $_145 \/ % 0.18/0.45 u9r2 $_145 == u10r2 $_145 \/ r1most $_145 \/ s1most $_145 \/ % 0.18/0.45 t3least $_145 % 0.18/0.45 |- u10r1 $_149 == u10r2 $_149 \/ u10r1 $_149 == u9r1 $_149 \/ % 0.18/0.45 u9r1 $_149 == u10r2 $_149 \/ r1most $_149 \/ s1most $_149 \/ % 0.18/0.45 t3least $_149 % 0.18/0.45 |- u10r1 $_149 == u10r2 $_149 \/ u10r1 $_149 == u9r2 $_149 \/ % 0.18/0.45 u9r2 $_149 == u10r2 $_149 \/ r1most $_149 \/ s1most $_149 \/ % 0.18/0.45 t3least $_149 % 0.18/0.46 |- ~t $_153 $_155 \/ $_155 == u9r1 $_153 \/ $_155 == u9r2 $_153 \/ % 0.18/0.46 u9r2 $_153 == u9r1 $_153 \/ r1most $_153 \/ t3least $_153 % 0.18/0.46 |- ~t $_153 $_154 \/ $_154 == u9r1 $_153 \/ u9r2 $_153 == $_154 \/ % 0.18/0.46 u9r2 $_153 == u9r1 $_153 \/ r1most $_153 \/ t3least $_153 % 0.18/0.46 |- u10r1 $_158 == u9r1 $_158 \/ u10r1 $_158 == u9r2 $_158 \/ % 0.18/0.46 r1most $_158 \/ s1most $_158 \/ t3least $_158 % 0.18/0.46 |- u10r2 $_160 == u9r1 $_160 \/ u10r2 $_160 == u9r2 $_160 \/ % 0.18/0.46 r1most $_160 \/ s1most $_160 \/ t3least $_160 % 0.18/0.46 |- u10r1 $_164 == u9r1 $_164 \/ u9r2 $_164 == u10r1 $_164 \/ % 0.18/0.46 r1most $_164 \/ s1most $_164 \/ t3least $_164 % 0.18/0.46 |- u10r2 $_166 == u9r1 $_166 \/ u9r2 $_166 == u10r2 $_166 \/ % 0.18/0.46 r1most $_166 \/ s1most $_166 \/ t3least $_166 % 0.18/0.46 |- ~t $_168 $_170 \/ $_170 == u9r1 $_168 \/ $_170 == u9r2 $_168 \/ % 0.18/0.46 u9r1 $_168 == u9r2 $_168 \/ r1most $_168 \/ t3least $_168 % 0.18/0.46 |- ~t $_168 $_169 \/ $_169 == u9r2 $_168 \/ u9r1 $_168 == $_169 \/ % 0.18/0.46 u9r1 $_168 == u9r2 $_168 \/ r1most $_168 \/ t3least $_168 % 0.18/0.46 |- u10r1 $_173 == u9r2 $_173 \/ u9r1 $_173 == u10r1 $_173 \/ % 0.18/0.46 u9r1 $_173 == u9r2 $_173 \/ r1most $_173 \/ s1most $_173 \/ % 0.18/0.46 t3least $_173 % 0.18/0.46 |- u10r2 $_173 == u9r2 $_173 \/ u9r1 $_173 == u10r2 $_173 \/ % 0.18/0.46 u9r1 $_173 == u9r2 $_173 \/ r1most $_173 \/ s1most $_173 \/ % 0.18/0.46 t3least $_173 % 0.18/0.46 |- ~t $_177 $_179 \/ $_179 == u10r1 $_177 \/ $_179 == u9r1 $_177 \/ % 0.18/0.46 u10r1 $_177 == u9r1 $_177 \/ r1most $_177 \/ s1most $_177 \/ % 0.18/0.46 t3least $_177 % 0.18/0.46 |- ~t $_177 $_179 \/ $_179 == u10r1 $_177 \/ $_179 == u9r2 $_177 \/ % 0.18/0.46 u10r1 $_177 == u9r2 $_177 \/ r1most $_177 \/ s1most $_177 \/ % 0.18/0.46 t3least $_177 % 0.18/0.46 |- ~t $_177 $_178 \/ u10r1 $_177 == $_178 \/ u10r2 $_177 == $_178 \/ % 0.18/0.46 u10r2 $_177 == u10r1 $_177 \/ s1most $_177 \/ t3least $_177 % 0.18/0.46 |- ~t $_177 $_178 \/ u10r1 $_177 == $_178 \/ u9r1 $_177 == $_178 \/ % 0.18/0.46 u9r1 $_177 == u10r1 $_177 \/ r1most $_177 \/ s1most $_177 \/ % 0.18/0.46 t3least $_177 % 0.18/0.46 |- ~t $_177 $_178 \/ u10r1 $_177 == $_178 \/ u9r2 $_177 == $_178 \/ % 0.18/0.46 u9r2 $_177 == u10r1 $_177 \/ r1most $_177 \/ s1most $_177 \/ % 0.18/0.46 t3least $_177 % 0.18/0.46 |- u10r1 $_180 == u9r1 $_180 \/ u10r2 $_180 == u10r1 $_180 \/ % 0.18/0.46 u10r2 $_180 == u9r1 $_180 \/ r1most $_180 \/ s1most $_180 \/ % 0.18/0.46 t3least $_180 % 0.18/0.46 |- u10r1 $_180 == u9r2 $_180 \/ u10r2 $_180 == u10r1 $_180 \/ % 0.18/0.46 u10r2 $_180 == u9r2 $_180 \/ r1most $_180 \/ s1most $_180 \/ % 0.18/0.46 t3least $_180 % 0.18/0.46 |- ~t $_192 $_194 \/ $_194 == u10r2 $_192 \/ $_194 == u9r1 $_192 \/ % 0.18/0.46 u10r2 $_192 == u9r1 $_192 \/ r1most $_192 \/ s1most $_192 \/ % 0.18/0.46 t3least $_192 % 0.18/0.46 |- ~t $_192 $_194 \/ $_194 == u10r2 $_192 \/ $_194 == u9r2 $_192 \/ % 0.18/0.46 u10r2 $_192 == u9r2 $_192 \/ r1most $_192 \/ s1most $_192 \/ % 0.18/0.46 t3least $_192 % 0.18/0.46 |- ~t $_192 $_193 \/ u10r1 $_192 == $_193 \/ u10r1 $_192 == u10r2 $_192 \/ % 0.18/0.46 u10r2 $_192 == $_193 \/ s1most $_192 \/ t3least $_192 % 0.18/0.46 |- ~t $_192 $_193 \/ u10r2 $_192 == $_193 \/ u9r1 $_192 == $_193 \/ % 0.18/0.46 u9r1 $_192 == u10r2 $_192 \/ r1most $_192 \/ s1most $_192 \/ % 0.18/0.46 t3least $_192 % 0.18/0.46 |- ~t $_192 $_193 \/ u10r2 $_192 == $_193 \/ u9r2 $_192 == $_193 \/ % 0.18/0.46 u9r2 $_192 == u10r2 $_192 \/ r1most $_192 \/ s1most $_192 \/ % 0.18/0.46 t3least $_192 % 0.18/0.46 |- u10r1 $_195 == u10r2 $_195 \/ u10r1 $_195 == u9r1 $_195 \/ % 0.18/0.46 u10r2 $_195 == u9r1 $_195 \/ r1most $_195 \/ s1most $_195 \/ % 0.18/0.46 t3least $_195 % 0.18/0.46 |- u10r1 $_195 == u10r2 $_195 \/ u10r1 $_195 == u9r2 $_195 \/ % 0.18/0.46 u10r2 $_195 == u9r2 $_195 \/ r1most $_195 \/ s1most $_195 \/ % 0.18/0.46 t3least $_195 % 0.18/0.46 |- ~t $_207 $_209 \/ $_209 == u10r1 $_207 \/ $_209 == u9r1 $_207 \/ % 0.18/0.46 u9r1 $_207 == u10r1 $_207 \/ r1most $_207 \/ s1most $_207 \/ % 0.18/0.46 t3least $_207 % 0.18/0.46 |- ~t $_207 $_209 \/ $_209 == u10r2 $_207 \/ $_209 == u9r1 $_207 \/ % 0.18/0.46 u9r1 $_207 == u10r2 $_207 \/ r1most $_207 \/ s1most $_207 \/ % 0.18/0.46 t3least $_207 % 0.18/0.46 |- ~t $_207 $_208 \/ u10r1 $_207 == $_208 \/ u10r1 $_207 == u9r1 $_207 \/ % 0.18/0.46 u9r1 $_207 == $_208 \/ r1most $_207 \/ s1most $_207 \/ t3least $_207 % 0.18/0.46 |- ~t $_207 $_208 \/ u10r2 $_207 == $_208 \/ u10r2 $_207 == u9r1 $_207 \/ % 0.18/0.46 u9r1 $_207 == $_208 \/ r1most $_207 \/ s1most $_207 \/ t3least $_207 % 0.18/0.46 |- ~t $_207 $_208 \/ u9r1 $_207 == $_208 \/ u9r2 $_207 == $_208 \/ % 0.18/0.46 u9r2 $_207 == u9r1 $_207 \/ r1most $_207 \/ t3least $_207 % 0.18/0.46 |- u9r1 $_212 == u10r2 $_212 \/ u9r2 $_212 == u10r2 $_212 \/ % 0.18/0.46 r1most $_212 \/ s1most $_212 \/ t3least $_212 % 0.18/0.46 |- ~t $_222 $_224 \/ $_224 == u10r1 $_222 \/ $_224 == u9r2 $_222 \/ % 0.18/0.46 u9r2 $_222 == u10r1 $_222 \/ r1most $_222 \/ s1most $_222 \/ % 0.18/0.46 t3least $_222 % 0.18/0.46 |- ~t $_222 $_224 \/ $_224 == u10r2 $_222 \/ $_224 == u9r2 $_222 \/ % 0.18/0.46 u9r2 $_222 == u10r2 $_222 \/ r1most $_222 \/ s1most $_222 \/ % 0.18/0.46 t3least $_222 % 0.18/0.46 |- ~t $_222 $_223 \/ u10r1 $_222 == $_223 \/ u10r1 $_222 == u9r2 $_222 \/ % 0.18/0.46 u9r2 $_222 == $_223 \/ r1most $_222 \/ s1most $_222 \/ t3least $_222 % 0.18/0.46 |- ~t $_222 $_223 \/ u10r2 $_222 == $_223 \/ u10r2 $_222 == u9r2 $_222 \/ % 0.18/0.46 u9r2 $_222 == $_223 \/ r1most $_222 \/ s1most $_222 \/ t3least $_222 % 0.18/0.46 |- ~t $_222 $_223 \/ u9r1 $_222 == $_223 \/ u9r1 $_222 == u9r2 $_222 \/ % 0.18/0.46 u9r2 $_222 == $_223 \/ r1most $_222 \/ t3least $_222 % 0.18/0.46 |- ~t $_235 $_237 \/ $_237 == u9r1 $_235 \/ u10r1 $_235 == $_237 \/ % 0.18/0.46 u10r1 $_235 == u9r1 $_235 \/ r1most $_235 \/ s1most $_235 \/ % 0.18/0.46 t3least $_235 % 0.18/0.46 |- ~t $_235 $_237 \/ $_237 == u9r2 $_235 \/ u10r1 $_235 == $_237 \/ % 0.18/0.46 u10r1 $_235 == u9r2 $_235 \/ r1most $_235 \/ s1most $_235 \/ % 0.18/0.46 t3least $_235 % 0.18/0.46 |- ~t $_242 $_244 \/ $_244 == u9r1 $_242 \/ u10r2 $_242 == $_244 \/ % 0.18/0.46 u10r2 $_242 == u9r1 $_242 \/ r1most $_242 \/ s1most $_242 \/ % 0.18/0.46 t3least $_242 % 0.18/0.46 |- ~t $_242 $_244 \/ $_244 == u9r2 $_242 \/ u10r2 $_242 == $_244 \/ % 0.18/0.46 u10r2 $_242 == u9r2 $_242 \/ r1most $_242 \/ s1most $_242 \/ % 0.18/0.46 t3least $_242 % 0.18/0.46 |- ~t $_249 $_251 \/ $_251 == u10r1 $_249 \/ u9r1 $_249 == $_251 \/ % 0.18/0.46 u9r1 $_249 == u10r1 $_249 \/ r1most $_249 \/ s1most $_249 \/ % 0.18/0.46 t3least $_249 % 0.18/0.46 |- ~t $_249 $_251 \/ $_251 == u10r2 $_249 \/ u9r1 $_249 == $_251 \/ % 0.18/0.46 u9r1 $_249 == u10r2 $_249 \/ r1most $_249 \/ s1most $_249 \/ % 0.18/0.46 t3least $_249 % 0.18/0.46 |- ~t $_256 $_258 \/ $_258 == u10r2 $_256 \/ u9r2 $_256 == $_258 \/ % 0.18/0.46 u9r2 $_256 == u10r2 $_256 \/ r1most $_256 \/ s1most $_256 \/ % 0.18/0.46 t3least $_256 % 0.18/0.46 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.46 %------------------------------------------------------------------------------