%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : KRS008-1 : TPTP v8.1.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n019.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.87s 1.06s % Output : Saturation 0.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS008-1 : TPTP v8.1.0. Released v2.0.0. % 0.03/0.12 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n019.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 14:34:55 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.87/1.06 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.87/1.06 % 0.87/1.06 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.87/1.06 |- ~c $X1 \/ s2least $X1 % 0.87/1.06 |- ~s2least $X1 \/ c $X1 % 0.87/1.06 |- ~(u1r2 $X1 == u1r1 $X1) \/ ~s2least $X1 % 0.87/1.06 |- ~s2least $X1 \/ s $X1 (u1r1 $X1) % 0.87/1.06 |- ~s2least $X1 \/ s $X1 (u1r2 $X1) % 0.87/1.06 |- ~s $X1 $X2 \/ ~s $X1 $X3 \/ $X3 == $X2 \/ s2least $X1 % 0.87/1.06 |- ~d $X1 \/ s1most $X1 % 0.87/1.06 |- ~s1most $X1 \/ d $X1 % 0.87/1.06 |- ~s $X1 $X2 \/ ~s $X1 $X3 \/ ~s1most $X1 \/ $X3 == $X2 % 0.87/1.06 |- ~(u3r2 $X1 == u3r1 $X1) \/ s1most $X1 % 0.87/1.06 |- s $X1 (u3r1 $X1) \/ s1most $X1 % 0.87/1.06 |- s $X1 (u3r2 $X1) \/ s1most $X1 % 0.87/1.06 |- ~e $X1 \/ d (u4r2 $X1) % 0.87/1.06 |- ~e $X1 \/ r $X1 (u4r2 $X1) % 0.87/1.06 |- ~e $X1 \/ c (u4r1 $X1) % 0.87/1.06 |- ~e $X1 \/ r $X1 (u4r1 $X1) % 0.87/1.06 |- ~e $X1 \/ r2most $X1 % 0.87/1.06 |- ~c $X2 \/ ~d $X3 \/ ~r $X1 $X2 \/ ~r $X1 $X3 \/ ~r2most $X1 \/ e $X1 % 0.87/1.06 |- ~r $X1 $X2 \/ ~r $X1 $X3 \/ ~r $X1 $X4 \/ ~r2most $X1 \/ $X3 == $X2 \/ % 0.87/1.06 $X4 == $X2 \/ $X4 == $X3 % 0.87/1.06 |- ~(u5r2 $X1 == u5r1 $X1) \/ r2most $X1 % 0.87/1.06 |- ~(u5r3 $X1 == u5r1 $X1) \/ r2most $X1 % 0.87/1.06 |- ~(u5r3 $X1 == u5r2 $X1) \/ r2most $X1 % 0.87/1.06 |- r $X1 (u5r1 $X1) \/ r2most $X1 % 0.87/1.06 |- r $X1 (u5r2 $X1) \/ r2most $X1 % 0.87/1.06 |- r $X1 (u5r3 $X1) \/ r2most $X1 % 0.87/1.06 |- ~d $X4 \/ ~d $X5 \/ ~f $X1 \/ ~r $X1 $X4 \/ ~r $X1 $X5 \/ $X5 == $X4 % 0.87/1.06 |- ~c $X2 \/ ~c $X3 \/ ~f $X1 \/ ~r $X1 $X2 \/ ~r $X1 $X3 \/ $X3 == $X2 % 0.87/1.06 |- ~(u6r2 $X1 == u6r1 $X1) \/ ~(u6r4 $X1 == u6r3 $X1) \/ f $X1 % 0.87/1.06 |- ~(u6r2 $X1 == u6r1 $X1) \/ d (u6r3 $X1) \/ f $X1 % 0.87/1.06 |- ~(u6r2 $X1 == u6r1 $X1) \/ d (u6r4 $X1) \/ f $X1 % 0.87/1.06 |- ~(u6r2 $X1 == u6r1 $X1) \/ f $X1 \/ r $X1 (u6r3 $X1) % 0.87/1.06 |- ~(u6r2 $X1 == u6r1 $X1) \/ f $X1 \/ r $X1 (u6r4 $X1) % 0.87/1.06 |- ~(u6r4 $X1 == u6r3 $X1) \/ c (u6r1 $X1) \/ f $X1 % 0.87/1.06 |- c (u6r1 $X1) \/ d (u6r3 $X1) \/ f $X1 % 0.87/1.06 |- c (u6r1 $X1) \/ d (u6r4 $X1) \/ f $X1 % 0.87/1.06 |- c (u6r1 $X1) \/ f $X1 \/ r $X1 (u6r3 $X1) % 0.87/1.06 |- c (u6r1 $X1) \/ f $X1 \/ r $X1 (u6r4 $X1) % 0.87/1.06 |- ~(u6r4 $X1 == u6r3 $X1) \/ c (u6r2 $X1) \/ f $X1 % 0.87/1.06 |- c (u6r2 $X1) \/ d (u6r3 $X1) \/ f $X1 % 0.87/1.06 |- c (u6r2 $X1) \/ d (u6r4 $X1) \/ f $X1 % 0.87/1.06 |- c (u6r2 $X1) \/ f $X1 \/ r $X1 (u6r3 $X1) % 0.87/1.06 |- c (u6r2 $X1) \/ f $X1 \/ r $X1 (u6r4 $X1) % 0.87/1.06 |- ~(u6r4 $X1 == u6r3 $X1) \/ f $X1 \/ r $X1 (u6r1 $X1) % 0.87/1.06 |- d (u6r3 $X1) \/ f $X1 \/ r $X1 (u6r1 $X1) % 0.87/1.06 |- d (u6r4 $X1) \/ f $X1 \/ r $X1 (u6r1 $X1) % 0.87/1.06 |- f $X1 \/ r $X1 (u6r1 $X1) \/ r $X1 (u6r3 $X1) % 0.87/1.06 |- f $X1 \/ r $X1 (u6r1 $X1) \/ r $X1 (u6r4 $X1) % 0.87/1.06 |- ~(u6r4 $X1 == u6r3 $X1) \/ f $X1 \/ r $X1 (u6r2 $X1) % 0.87/1.06 |- d (u6r3 $X1) \/ f $X1 \/ r $X1 (u6r2 $X1) % 0.87/1.06 |- d (u6r4 $X1) \/ f $X1 \/ r $X1 (u6r2 $X1) % 0.87/1.06 |- f $X1 \/ r $X1 (u6r2 $X1) \/ r $X1 (u6r3 $X1) % 0.87/1.06 |- f $X1 \/ r $X1 (u6r2 $X1) \/ r $X1 (u6r4 $X1) % 0.87/1.06 |- ~s $X1 $X3 \/ $X3 == $X3 \/ s2least $X1 % 0.87/1.06 |- ~s $X1 $X3 \/ ~s1most $X1 \/ $X3 == $X3 % 0.87/1.06 |- ~c $X3 \/ ~d $X3 \/ ~r $X1 $X3 \/ ~r2most $X1 \/ e $X1 % 0.87/1.06 |- ~d $X5 \/ ~f $X1 \/ ~r $X1 $X5 \/ $X5 == $X5 % 0.87/1.06 |- ~c $X3 \/ ~f $X1 \/ ~r $X1 $X3 \/ $X3 == $X3 % 0.87/1.06 |- ~r $X1 $X4 \/ ~r2most $X1 \/ $X4 == $X4 % 0.87/1.06 |- e exist % 0.87/1.06 |- ~f exist % 0.87/1.06 |- r2most exist % 0.87/1.06 |- d (u4r2 exist) % 0.87/1.06 |- s1most (u4r2 exist) % 0.87/1.06 |- c (u4r1 exist) % 0.87/1.06 |- s2least (u4r1 exist) % 0.87/1.06 |- s (u4r1 exist) (u1r1 (u4r1 exist)) % 0.87/1.06 |- s (u4r1 exist) (u1r2 (u4r1 exist)) % 0.87/1.06 |- r exist (u4r2 exist) % 0.87/1.06 |- r exist (u4r1 exist) % 0.87/1.06 |- c (u6r1 $_21) \/ f $_21 \/ s1most (u6r3 $_21) % 0.87/1.06 |- c (u6r1 $_22) \/ f $_22 \/ s1most (u6r4 $_22) % 0.87/1.06 |- c (u6r2 $_23) \/ f $_23 \/ s1most (u6r3 $_23) % 0.87/1.06 |- c (u6r2 $_24) \/ f $_24 \/ s1most (u6r4 $_24) % 0.87/1.06 |- ~s1most (u4r1 exist) \/ u1r1 (u4r1 exist) == u1r1 (u4r1 exist) % 0.87/1.06 |- ~s1most (u4r1 exist) \/ u1r2 (u4r1 exist) == u1r2 (u4r1 exist) % 0.87/1.06 |- u4r1 exist == u4r1 exist % 0.87/1.06 |- u4r2 exist == u4r2 exist % 0.87/1.06 |- ~r2most $_56 \/ u6r1 $_56 == u6r1 $_56 \/ d (u6r4 $_56) \/ f $_56 % 0.87/1.06 |- ~r2most $_56 \/ u6r1 $_56 == u6r1 $_56 \/ d (u6r3 $_56) \/ f $_56 % 0.87/1.06 |- ~r2most $_56 \/ u6r2 $_56 == u6r2 $_56 \/ d (u6r4 $_56) \/ f $_56 % 0.87/1.06 |- ~r2most $_56 \/ u6r2 $_56 == u6r2 $_56 \/ d (u6r3 $_56) \/ f $_56 % 0.87/1.06 |- ~r2most $_56 \/ u6r3 $_56 == u6r3 $_56 \/ f $_56 \/ r $_56 (u6r2 $_56) % 0.87/1.06 |- ~r2most $_56 \/ u6r3 $_56 == u6r3 $_56 \/ f $_56 \/ r $_56 (u6r1 $_56) % 0.87/1.06 |- ~r2most $_56 \/ u6r3 $_56 == u6r3 $_56 \/ c (u6r2 $_56) \/ f $_56 % 0.87/1.06 |- ~r2most $_56 \/ u6r3 $_56 == u6r3 $_56 \/ c (u6r1 $_56) \/ f $_56 % 0.87/1.06 |- ~r2most $_56 \/ u6r4 $_56 == u6r4 $_56 \/ f $_56 \/ r $_56 (u6r2 $_56) % 0.87/1.06 |- ~r2most $_56 \/ u6r4 $_56 == u6r4 $_56 \/ f $_56 \/ r $_56 (u6r1 $_56) % 0.87/1.06 |- ~r2most $_56 \/ u6r4 $_56 == u6r4 $_56 \/ c (u6r2 $_56) \/ f $_56 % 0.87/1.06 |- ~r2most $_56 \/ u6r4 $_56 == u6r4 $_56 \/ c (u6r1 $_56) \/ f $_56 % 0.87/1.06 |- ~d (u5r1 $_58) \/ ~f $_58 \/ u5r1 $_58 == u5r1 $_58 \/ r2most $_58 % 0.87/1.06 |- ~d (u5r2 $_58) \/ ~f $_58 \/ u5r2 $_58 == u5r2 $_58 \/ r2most $_58 % 0.87/1.06 |- ~d (u5r3 $_58) \/ ~f $_58 \/ u5r3 $_58 == u5r3 $_58 \/ r2most $_58 % 0.87/1.06 |- ~c (u5r1 $_60) \/ ~f $_60 \/ u5r1 $_60 == u5r1 $_60 \/ r2most $_60 % 0.87/1.06 |- ~c (u5r2 $_60) \/ ~f $_60 \/ u5r2 $_60 == u5r2 $_60 \/ r2most $_60 % 0.87/1.06 |- ~c (u5r3 $_60) \/ ~f $_60 \/ u5r3 $_60 == u5r3 $_60 \/ r2most $_60 % 0.87/1.06 |- u6r1 exist == u6r1 exist \/ d (u6r4 exist) % 0.87/1.06 |- u6r1 exist == u6r1 exist \/ d (u6r3 exist) % 0.87/1.06 |- u6r2 exist == u6r2 exist \/ d (u6r4 exist) % 0.87/1.06 |- u6r2 exist == u6r2 exist \/ d (u6r3 exist) % 0.87/1.06 |- u6r3 exist == u6r3 exist \/ c (u6r2 exist) % 0.87/1.06 |- u6r3 exist == u6r3 exist \/ c (u6r1 exist) % 0.87/1.06 |- u6r4 exist == u6r4 exist \/ c (u6r2 exist) % 0.87/1.06 |- u6r4 exist == u6r4 exist \/ c (u6r1 exist) % 0.87/1.06 |- ~c (u6r1 $_76) \/ ~d (u6r1 $_76) \/ ~r2most $_76 \/ d (u6r4 $_76) \/ % 0.87/1.06 e $_76 \/ f $_76 % 0.87/1.06 |- ~c (u6r1 $_76) \/ ~d (u6r1 $_76) \/ ~r2most $_76 \/ d (u6r3 $_76) \/ % 0.87/1.06 e $_76 \/ f $_76 % 0.87/1.06 |- ~c (u6r2 $_76) \/ ~d (u6r2 $_76) \/ ~r2most $_76 \/ d (u6r4 $_76) \/ % 0.87/1.06 e $_76 \/ f $_76 % 0.87/1.06 |- ~c (u6r2 $_76) \/ ~d (u6r2 $_76) \/ ~r2most $_76 \/ d (u6r3 $_76) \/ % 0.87/1.06 e $_76 \/ f $_76 % 0.87/1.06 |- ~c (u6r3 $_76) \/ ~d (u6r3 $_76) \/ ~r2most $_76 \/ e $_76 \/ f $_76 \/ % 0.87/1.06 r $_76 (u6r2 $_76) % 0.87/1.06 |- ~c (u6r3 $_76) \/ ~d (u6r3 $_76) \/ ~r2most $_76 \/ e $_76 \/ f $_76 \/ % 0.87/1.06 r $_76 (u6r1 $_76) % 0.87/1.06 |- ~c (u6r4 $_76) \/ ~d (u6r4 $_76) \/ ~r2most $_76 \/ e $_76 \/ f $_76 \/ % 0.87/1.06 r $_76 (u6r2 $_76) % 0.87/1.06 |- ~c (u6r4 $_76) \/ ~d (u6r4 $_76) \/ ~r2most $_76 \/ e $_76 \/ f $_76 \/ % 0.87/1.06 r $_76 (u6r1 $_76) % 0.87/1.06 |- u6r3 exist == u6r3 exist \/ r exist (u6r2 exist) % 0.87/1.06 |- u6r3 exist == u6r3 exist \/ r exist (u6r1 exist) % 0.87/1.06 |- u6r4 exist == u6r4 exist \/ r exist (u6r2 exist) % 0.87/1.06 |- u6r4 exist == u6r4 exist \/ r exist (u6r1 exist) % 0.87/1.06 |- ~s (u4r1 exist) $_87 \/ ~s1most (u4r1 exist) \/ % 0.87/1.06 $_87 == u1r1 (u4r1 exist) % 0.87/1.06 |- ~s (u4r1 exist) $_87 \/ ~s1most (u4r1 exist) \/ % 0.87/1.06 $_87 == u1r2 (u4r1 exist) % 0.87/1.06 |- ~s (u4r1 exist) $_86 \/ ~s1most (u4r1 exist) \/ % 0.87/1.06 u1r1 (u4r1 exist) == $_86 % 0.87/1.06 |- ~s (u4r1 exist) $_86 \/ ~s1most (u4r1 exist) \/ % 0.87/1.06 u1r2 (u4r1 exist) == $_86 % 0.87/1.06 |- ~s1most (u4r1 exist) \/ u1r2 (u4r1 exist) == u1r1 (u4r1 exist) % 0.87/1.06 |- ~s1most (u4r1 exist) \/ u1r1 (u4r1 exist) == u1r2 (u4r1 exist) % 0.87/1.06 |- s1most $_94 \/ s2least $_94 % 0.87/1.06 |- s $_95 (u1r2 $_95) \/ s1most $_95 % 0.87/1.06 |- s $_95 (u1r1 $_95) \/ s1most $_95 % 0.87/1.06 |- c $_95 \/ s1most $_95 % 0.87/1.06 |- c $_96 \/ d $_96 % 0.87/1.06 |- ~f $_58 \/ u5r1 $_58 == u5r1 $_58 \/ c (u5r1 $_58) \/ r2most $_58 % 0.87/1.06 |- ~f $_58 \/ u5r2 $_58 == u5r2 $_58 \/ c (u5r2 $_58) \/ r2most $_58 % 0.87/1.06 |- ~f $_58 \/ u5r3 $_58 == u5r3 $_58 \/ c (u5r3 $_58) \/ r2most $_58 % 0.87/1.06 |- ~c (u6r3 $_107) \/ ~r2most $_107 \/ c (u6r2 $_107) \/ e $_107 \/ f $_107 % 0.87/1.06 |- ~c (u6r3 $_109) \/ ~r2most $_109 \/ c (u6r1 $_109) \/ e $_109 \/ f $_109 % 0.87/1.06 |- ~c (u6r4 $_111) \/ ~r2most $_111 \/ c (u6r2 $_111) \/ e $_111 \/ f $_111 % 0.87/1.06 |- ~c (u6r4 $_113) \/ ~r2most $_113 \/ c (u6r1 $_113) \/ e $_113 \/ f $_113 % 0.87/1.06 |- ~c (u6r1 $_119) \/ ~d $_121 \/ ~r $_119 $_121 \/ ~r2most $_119 \/ % 0.87/1.06 d (u6r4 $_119) \/ e $_119 \/ f $_119 % 0.87/1.06 |- ~c (u6r1 $_119) \/ ~d $_121 \/ ~r $_119 $_121 \/ ~r2most $_119 \/ % 0.87/1.06 d (u6r3 $_119) \/ e $_119 \/ f $_119 % 0.87/1.06 |- ~c (u6r2 $_119) \/ ~d $_121 \/ ~r $_119 $_121 \/ ~r2most $_119 \/ % 0.87/1.06 d (u6r4 $_119) \/ e $_119 \/ f $_119 % 0.87/1.06 |- ~c (u6r2 $_119) \/ ~d $_121 \/ ~r $_119 $_121 \/ ~r2most $_119 \/ % 0.87/1.06 d (u6r3 $_119) \/ e $_119 \/ f $_119 % 0.87/1.06 |- ~c (u6r3 $_119) \/ ~d $_121 \/ ~r $_119 $_121 \/ ~r2most $_119 \/ % 0.87/1.06 e $_119 \/ f $_119 \/ r $_119 (u6r2 $_119) % 0.87/1.06 |- ~c (u6r3 $_119) \/ ~d $_121 \/ ~r $_119 $_121 \/ ~r2most $_119 \/ % 0.87/1.06 e $_119 \/ f $_119 \/ r $_119 (u6r1 $_119) % 0.87/1.06 |- ~c (u6r4 $_119) \/ ~d $_121 \/ ~r $_119 $_121 \/ ~r2most $_119 \/ % 0.87/1.06 e $_119 \/ f $_119 \/ r $_119 (u6r2 $_119) % 0.87/1.06 |- ~c (u6r4 $_119) \/ ~d $_121 \/ ~r $_119 $_121 \/ ~r2most $_119 \/ % 0.87/1.06 e $_119 \/ f $_119 \/ r $_119 (u6r1 $_119) % 0.87/1.06 |- ~c $_120 \/ ~d (u6r1 $_119) \/ ~r $_119 $_120 \/ ~r2most $_119 \/ % 0.87/1.06 d (u6r4 $_119) \/ e $_119 \/ f $_119 % 0.87/1.06 |- ~c $_120 \/ ~d (u6r1 $_119) \/ ~r $_119 $_120 \/ ~r2most $_119 \/ % 0.87/1.06 d (u6r3 $_119) \/ e $_119 \/ f $_119 % 0.87/1.06 |- ~c $_120 \/ ~d (u6r2 $_119) \/ ~r $_119 $_120 \/ ~r2most $_119 \/ % 0.87/1.06 d (u6r4 $_119) \/ e $_119 \/ f $_119 % 0.87/1.06 |- ~c $_120 \/ ~d (u6r2 $_119) \/ ~r $_119 $_120 \/ ~r2most $_119 \/ % 0.87/1.06 d (u6r3 $_119) \/ e $_119 \/ f $_119 % 0.87/1.06 |- ~c $_120 \/ ~d (u6r3 $_119) \/ ~r $_119 $_120 \/ ~r2most $_119 \/ % 0.87/1.06 e $_119 \/ f $_119 \/ r $_119 (u6r2 $_119) % 0.87/1.06 |- ~c $_120 \/ ~d (u6r3 $_119) \/ ~r $_119 $_120 \/ ~r2most $_119 \/ % 0.87/1.06 e $_119 \/ f $_119 \/ r $_119 (u6r1 $_119) % 0.87/1.06 |- ~c $_120 \/ ~d (u6r3 $_119) \/ ~r $_119 $_120 \/ ~r2most $_119 \/ % 0.87/1.06 c (u6r2 $_119) \/ e $_119 \/ f $_119 % 0.87/1.06 |- ~c $_120 \/ ~d (u6r3 $_119) \/ ~r $_119 $_120 \/ ~r2most $_119 \/ % 0.87/1.06 c (u6r1 $_119) \/ e $_119 \/ f $_119 % 0.87/1.06 |- ~c $_120 \/ ~d (u6r4 $_119) \/ ~r $_119 $_120 \/ ~r2most $_119 \/ % 0.87/1.06 e $_119 \/ f $_119 \/ r $_119 (u6r2 $_119) % 0.87/1.06 |- ~c $_120 \/ ~d (u6r4 $_119) \/ ~r $_119 $_120 \/ ~r2most $_119 \/ % 0.87/1.06 e $_119 \/ f $_119 \/ r $_119 (u6r1 $_119) % 0.87/1.06 |- ~c $_120 \/ ~d (u6r4 $_119) \/ ~r $_119 $_120 \/ ~r2most $_119 \/ % 0.87/1.06 c (u6r2 $_119) \/ e $_119 \/ f $_119 % 0.87/1.06 |- ~c $_120 \/ ~d (u6r4 $_119) \/ ~r $_119 $_120 \/ ~r2most $_119 \/ % 0.87/1.06 c (u6r1 $_119) \/ e $_119 \/ f $_119 % 0.87/1.06 |- ~d $_124 \/ ~d (u5r1 $_122) \/ ~f $_122 \/ ~r $_122 $_124 \/ % 0.87/1.06 $_124 == u5r1 $_122 \/ r2most $_122 % 0.87/1.06 |- ~d $_124 \/ ~d (u5r2 $_122) \/ ~f $_122 \/ ~r $_122 $_124 \/ % 0.87/1.06 $_124 == u5r2 $_122 \/ r2most $_122 % 0.87/1.06 |- ~d $_124 \/ ~d (u5r3 $_122) \/ ~f $_122 \/ ~r $_122 $_124 \/ % 0.87/1.06 $_124 == u5r3 $_122 \/ r2most $_122 % 0.87/1.06 |- ~d $_123 \/ ~d (u5r1 $_122) \/ ~f $_122 \/ ~r $_122 $_123 \/ % 0.87/1.06 u5r1 $_122 == $_123 \/ r2most $_122 % 0.87/1.06 |- ~d $_123 \/ ~d (u5r2 $_122) \/ ~f $_122 \/ ~r $_122 $_123 \/ % 0.87/1.06 u5r2 $_122 == $_123 \/ r2most $_122 % 0.87/1.06 |- ~d $_123 \/ ~d (u5r3 $_122) \/ ~f $_122 \/ ~r $_122 $_123 \/ % 0.87/1.06 u5r3 $_122 == $_123 \/ r2most $_122 % 0.87/1.06 |- ~c $_127 \/ ~c (u5r1 $_125) \/ ~f $_125 \/ ~r $_125 $_127 \/ % 0.87/1.06 $_127 == u5r1 $_125 \/ r2most $_125 % 0.87/1.06 |- ~c $_127 \/ ~c (u5r2 $_125) \/ ~f $_125 \/ ~r $_125 $_127 \/ % 0.87/1.06 $_127 == u5r2 $_125 \/ r2most $_125 % 0.87/1.06 |- ~c $_127 \/ ~c (u5r3 $_125) \/ ~f $_125 \/ ~r $_125 $_127 \/ % 0.87/1.06 $_127 == u5r3 $_125 \/ r2most $_125 % 0.87/1.06 |- ~c $_126 \/ ~c (u5r1 $_125) \/ ~f $_125 \/ ~r $_125 $_126 \/ % 0.87/1.06 u5r1 $_125 == $_126 \/ r2most $_125 % 0.87/1.06 |- ~c $_126 \/ ~c (u5r2 $_125) \/ ~f $_125 \/ ~r $_125 $_126 \/ % 0.87/1.06 u5r2 $_125 == $_126 \/ r2most $_125 % 0.87/1.07 |- ~c $_126 \/ ~c (u5r3 $_125) \/ ~f $_125 \/ ~r $_125 $_126 \/ % 0.87/1.07 u5r3 $_125 == $_126 \/ r2most $_125 % 0.87/1.07 |- ~d (u5r1 $_128) \/ ~d (u5r2 $_128) \/ ~f $_128 \/ % 0.87/1.07 u5r2 $_128 == u5r1 $_128 \/ r2most $_128 % 0.87/1.07 |- ~d (u5r1 $_128) \/ ~d (u5r3 $_128) \/ ~f $_128 \/ % 0.87/1.07 u5r3 $_128 == u5r1 $_128 \/ r2most $_128 % 0.87/1.07 |- ~d (u5r1 $_130) \/ ~f $_130 \/ u5r2 $_130 == u5r1 $_130 \/ % 0.87/1.07 c (u5r2 $_130) \/ r2most $_130 % 0.87/1.07 |- ~d (u5r1 $_131) \/ ~f $_131 \/ u5r3 $_131 == u5r1 $_131 \/ % 0.87/1.07 c (u5r3 $_131) \/ r2most $_131 % 0.87/1.07 |- ~f $_132 \/ u5r2 $_132 == u5r1 $_132 \/ c (u5r1 $_132) \/ % 0.87/1.07 c (u5r2 $_132) \/ r2most $_132 % 0.87/1.07 |- ~f $_133 \/ u5r3 $_133 == u5r1 $_133 \/ c (u5r1 $_133) \/ % 0.87/1.07 c (u5r3 $_133) \/ r2most $_133 % 0.87/1.07 |- ~d (u5r1 $_136) \/ ~d (u5r2 $_136) \/ ~f $_136 \/ % 0.87/1.07 u5r1 $_136 == u5r2 $_136 \/ r2most $_136 % 0.87/1.07 |- ~d (u5r2 $_136) \/ ~d (u5r3 $_136) \/ ~f $_136 \/ % 0.87/1.07 u5r3 $_136 == u5r2 $_136 \/ r2most $_136 % 0.87/1.07 |- ~d (u5r2 $_138) \/ ~f $_138 \/ u5r3 $_138 == u5r2 $_138 \/ % 0.87/1.07 c (u5r3 $_138) \/ r2most $_138 % 0.87/1.07 |- ~d (u5r1 $_139) \/ ~f $_139 \/ u5r1 $_139 == u5r2 $_139 \/ % 0.87/1.07 c (u5r2 $_139) \/ r2most $_139 % 0.87/1.07 |- ~f $_140 \/ u5r3 $_140 == u5r2 $_140 \/ c (u5r2 $_140) \/ % 0.87/1.07 c (u5r3 $_140) \/ r2most $_140 % 0.87/1.07 |- ~f $_141 \/ u5r1 $_141 == u5r2 $_141 \/ c (u5r1 $_141) \/ % 0.87/1.07 c (u5r2 $_141) \/ r2most $_141 % 0.87/1.07 |- ~d (u5r1 $_144) \/ ~d (u5r3 $_144) \/ ~f $_144 \/ % 0.87/1.07 u5r1 $_144 == u5r3 $_144 \/ r2most $_144 % 0.87/1.07 |- ~d (u5r2 $_144) \/ ~d (u5r3 $_144) \/ ~f $_144 \/ % 0.87/1.07 u5r2 $_144 == u5r3 $_144 \/ r2most $_144 % 0.87/1.07 |- ~d (u5r2 $_146) \/ ~f $_146 \/ u5r2 $_146 == u5r3 $_146 \/ % 0.87/1.07 c (u5r3 $_146) \/ r2most $_146 % 0.87/1.07 |- ~d (u5r1 $_147) \/ ~f $_147 \/ u5r1 $_147 == u5r3 $_147 \/ % 0.87/1.07 c (u5r3 $_147) \/ r2most $_147 % 0.87/1.07 |- ~f $_148 \/ u5r2 $_148 == u5r3 $_148 \/ c (u5r2 $_148) \/ % 0.87/1.07 c (u5r3 $_148) \/ r2most $_148 % 0.87/1.07 |- ~f $_149 \/ u5r1 $_149 == u5r3 $_149 \/ c (u5r1 $_149) \/ % 0.87/1.07 c (u5r3 $_149) \/ r2most $_149 % 0.87/1.07 |- ~c (u5r1 $_158) \/ ~c (u5r2 $_158) \/ ~f $_158 \/ % 0.87/1.07 u5r2 $_158 == u5r1 $_158 \/ r2most $_158 % 0.87/1.07 |- ~c (u5r1 $_158) \/ ~c (u5r3 $_158) \/ ~f $_158 \/ % 0.87/1.07 u5r3 $_158 == u5r1 $_158 \/ r2most $_158 % 0.87/1.07 |- ~c (u5r1 $_162) \/ ~c (u5r2 $_162) \/ ~f $_162 \/ % 0.87/1.07 u5r1 $_162 == u5r2 $_162 \/ r2most $_162 % 0.87/1.07 |- ~c (u5r2 $_162) \/ ~c (u5r3 $_162) \/ ~f $_162 \/ % 0.87/1.07 u5r3 $_162 == u5r2 $_162 \/ r2most $_162 % 0.87/1.07 |- ~c (u5r1 $_166) \/ ~c (u5r3 $_166) \/ ~f $_166 \/ % 0.87/1.07 u5r1 $_166 == u5r3 $_166 \/ r2most $_166 % 0.87/1.07 |- ~c (u5r2 $_166) \/ ~c (u5r3 $_166) \/ ~f $_166 \/ % 0.87/1.07 u5r2 $_166 == u5r3 $_166 \/ r2most $_166 % 0.87/1.07 |- ~c (u6r1 $_176) \/ ~d (u6r2 $_176) \/ ~r2most $_176 \/ d (u6r4 $_176) \/ % 0.87/1.07 e $_176 \/ f $_176 % 0.87/1.07 |- ~c (u6r1 $_179) \/ ~d (u6r2 $_179) \/ ~r2most $_179 \/ d (u6r3 $_179) \/ % 0.87/1.07 e $_179 \/ f $_179 % 0.87/1.07 |- ~c (u6r2 $_182) \/ ~d (u6r1 $_182) \/ ~r2most $_182 \/ d (u6r4 $_182) \/ % 0.87/1.07 e $_182 \/ f $_182 % 0.87/1.07 |- ~c (u6r2 $_185) \/ ~d (u6r1 $_185) \/ ~r2most $_185 \/ d (u6r3 $_185) \/ % 0.87/1.07 e $_185 \/ f $_185 % 0.87/1.07 |- ~c (u6r3 $_204) \/ ~d (u6r4 $_204) \/ ~r2most $_204 \/ e $_204 \/ % 0.87/1.07 f $_204 \/ r $_204 (u6r2 $_204) % 0.87/1.07 |- ~c (u6r3 $_206) \/ ~r2most $_206 \/ c (u6r4 $_206) \/ e $_206 \/ % 0.87/1.07 f $_206 \/ r $_206 (u6r2 $_206) % 0.87/1.07 |- ~c (u6r3 $_208) \/ ~d (u6r4 $_208) \/ ~r2most $_208 \/ e $_208 \/ % 0.87/1.07 f $_208 \/ r $_208 (u6r1 $_208) % 0.87/1.07 |- ~c (u6r3 $_210) \/ ~r2most $_210 \/ c (u6r4 $_210) \/ e $_210 \/ % 0.87/1.07 f $_210 \/ r $_210 (u6r1 $_210) % 0.87/1.07 |- ~c (u6r4 $_212) \/ ~d (u6r3 $_212) \/ ~r2most $_212 \/ e $_212 \/ % 0.87/1.07 f $_212 \/ r $_212 (u6r2 $_212) % 0.87/1.07 |- ~c (u6r4 $_214) \/ ~r2most $_214 \/ c (u6r3 $_214) \/ e $_214 \/ % 0.87/1.07 f $_214 \/ r $_214 (u6r2 $_214) % 0.87/1.07 |- ~c (u6r4 $_216) \/ ~d (u6r3 $_216) \/ ~r2most $_216 \/ e $_216 \/ % 0.87/1.07 f $_216 \/ r $_216 (u6r1 $_216) % 0.87/1.07 |- ~c (u6r4 $_218) \/ ~r2most $_218 \/ c (u6r3 $_218) \/ e $_218 \/ % 0.87/1.07 f $_218 \/ r $_218 (u6r1 $_218) % 0.87/1.07 |- ~r exist $_230 \/ ~r exist $_231 \/ $_230 == u4r1 exist \/ % 0.87/1.07 $_231 == $_230 \/ $_231 == u4r1 exist % 0.87/1.07 |- ~r exist $_230 \/ ~r exist $_231 \/ $_230 == u4r2 exist \/ % 0.87/1.07 $_231 == $_230 \/ $_231 == u4r2 exist % 0.87/1.07 |- ~r $_228 $_230 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ % 0.87/1.07 $_230 == u6r1 $_228 \/ $_231 == $_230 \/ $_231 == u6r1 $_228 \/ % 0.87/1.07 d (u6r4 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_230 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ % 0.87/1.07 $_230 == u6r1 $_228 \/ $_231 == $_230 \/ $_231 == u6r1 $_228 \/ % 0.87/1.07 d (u6r3 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_230 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ % 0.87/1.07 $_230 == u6r2 $_228 \/ $_231 == $_230 \/ $_231 == u6r2 $_228 \/ % 0.87/1.07 d (u6r4 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_230 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ % 0.87/1.07 $_230 == u6r2 $_228 \/ $_231 == $_230 \/ $_231 == u6r2 $_228 \/ % 0.87/1.07 d (u6r3 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_230 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ % 0.87/1.07 $_230 == u6r3 $_228 \/ $_231 == $_230 \/ $_231 == u6r3 $_228 \/ % 0.87/1.07 f $_228 \/ r $_228 (u6r2 $_228) % 0.87/1.07 |- ~r $_228 $_230 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ % 0.87/1.07 $_230 == u6r3 $_228 \/ $_231 == $_230 \/ $_231 == u6r3 $_228 \/ % 0.87/1.07 f $_228 \/ r $_228 (u6r1 $_228) % 0.87/1.07 |- ~r $_228 $_230 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ % 0.87/1.07 $_230 == u6r3 $_228 \/ $_231 == $_230 \/ $_231 == u6r3 $_228 \/ % 0.87/1.07 c (u6r2 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_230 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ % 0.87/1.07 $_230 == u6r3 $_228 \/ $_231 == $_230 \/ $_231 == u6r3 $_228 \/ % 0.87/1.07 c (u6r1 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_230 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ % 0.87/1.07 $_230 == u6r4 $_228 \/ $_231 == $_230 \/ $_231 == u6r4 $_228 \/ % 0.87/1.07 f $_228 \/ r $_228 (u6r2 $_228) % 0.87/1.07 |- ~r $_228 $_230 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ % 0.87/1.07 $_230 == u6r4 $_228 \/ $_231 == $_230 \/ $_231 == u6r4 $_228 \/ % 0.87/1.07 f $_228 \/ r $_228 (u6r1 $_228) % 0.87/1.07 |- ~r $_228 $_230 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ % 0.87/1.07 $_230 == u6r4 $_228 \/ $_231 == $_230 \/ $_231 == u6r4 $_228 \/ % 0.87/1.07 c (u6r2 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_230 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ % 0.87/1.07 $_230 == u6r4 $_228 \/ $_231 == $_230 \/ $_231 == u6r4 $_228 \/ % 0.87/1.07 c (u6r1 $_228) \/ f $_228 % 0.87/1.07 |- ~r exist $_229 \/ ~r exist $_231 \/ $_231 == $_229 \/ % 0.87/1.07 $_231 == u4r1 exist \/ u4r1 exist == $_229 % 0.87/1.07 |- ~r exist $_229 \/ ~r exist $_231 \/ $_231 == $_229 \/ % 0.87/1.07 $_231 == u4r2 exist \/ u4r2 exist == $_229 % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ $_231 == $_229 \/ % 0.87/1.07 $_231 == u6r1 $_228 \/ u6r1 $_228 == $_229 \/ d (u6r4 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ $_231 == $_229 \/ % 0.87/1.07 $_231 == u6r1 $_228 \/ u6r1 $_228 == $_229 \/ d (u6r3 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ $_231 == $_229 \/ % 0.87/1.07 $_231 == u6r2 $_228 \/ u6r2 $_228 == $_229 \/ d (u6r4 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ $_231 == $_229 \/ % 0.87/1.07 $_231 == u6r2 $_228 \/ u6r2 $_228 == $_229 \/ d (u6r3 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ $_231 == $_229 \/ % 0.87/1.07 $_231 == u6r3 $_228 \/ u6r3 $_228 == $_229 \/ f $_228 \/ % 0.87/1.07 r $_228 (u6r2 $_228) % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ $_231 == $_229 \/ % 0.87/1.07 $_231 == u6r3 $_228 \/ u6r3 $_228 == $_229 \/ f $_228 \/ % 0.87/1.07 r $_228 (u6r1 $_228) % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ $_231 == $_229 \/ % 0.87/1.07 $_231 == u6r3 $_228 \/ u6r3 $_228 == $_229 \/ c (u6r2 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ $_231 == $_229 \/ % 0.87/1.07 $_231 == u6r3 $_228 \/ u6r3 $_228 == $_229 \/ c (u6r1 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ $_231 == $_229 \/ % 0.87/1.07 $_231 == u6r4 $_228 \/ u6r4 $_228 == $_229 \/ f $_228 \/ % 0.87/1.07 r $_228 (u6r2 $_228) % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ $_231 == $_229 \/ % 0.87/1.07 $_231 == u6r4 $_228 \/ u6r4 $_228 == $_229 \/ f $_228 \/ % 0.87/1.07 r $_228 (u6r1 $_228) % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ $_231 == $_229 \/ % 0.87/1.07 $_231 == u6r4 $_228 \/ u6r4 $_228 == $_229 \/ c (u6r2 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_231 \/ ~r2most $_228 \/ $_231 == $_229 \/ % 0.87/1.07 $_231 == u6r4 $_228 \/ u6r4 $_228 == $_229 \/ c (u6r1 $_228) \/ f $_228 % 0.87/1.07 |- ~r exist $_229 \/ ~r exist $_230 \/ $_230 == $_229 \/ % 0.87/1.07 u4r1 exist == $_229 \/ u4r1 exist == $_230 % 0.87/1.07 |- ~r exist $_229 \/ ~r exist $_230 \/ $_230 == $_229 \/ % 0.87/1.07 u4r2 exist == $_229 \/ u4r2 exist == $_230 % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_230 \/ ~r2most $_228 \/ $_230 == $_229 \/ % 0.87/1.07 u6r1 $_228 == $_229 \/ u6r1 $_228 == $_230 \/ d (u6r4 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_230 \/ ~r2most $_228 \/ $_230 == $_229 \/ % 0.87/1.07 u6r1 $_228 == $_229 \/ u6r1 $_228 == $_230 \/ d (u6r3 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_230 \/ ~r2most $_228 \/ $_230 == $_229 \/ % 0.87/1.07 u6r2 $_228 == $_229 \/ u6r2 $_228 == $_230 \/ d (u6r4 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_230 \/ ~r2most $_228 \/ $_230 == $_229 \/ % 0.87/1.07 u6r2 $_228 == $_229 \/ u6r2 $_228 == $_230 \/ d (u6r3 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_230 \/ ~r2most $_228 \/ $_230 == $_229 \/ % 0.87/1.07 u6r3 $_228 == $_229 \/ u6r3 $_228 == $_230 \/ f $_228 \/ % 0.87/1.07 r $_228 (u6r2 $_228) % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_230 \/ ~r2most $_228 \/ $_230 == $_229 \/ % 0.87/1.07 u6r3 $_228 == $_229 \/ u6r3 $_228 == $_230 \/ f $_228 \/ % 0.87/1.07 r $_228 (u6r1 $_228) % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_230 \/ ~r2most $_228 \/ $_230 == $_229 \/ % 0.87/1.07 u6r3 $_228 == $_229 \/ u6r3 $_228 == $_230 \/ c (u6r2 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_230 \/ ~r2most $_228 \/ $_230 == $_229 \/ % 0.87/1.07 u6r3 $_228 == $_229 \/ u6r3 $_228 == $_230 \/ c (u6r1 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_230 \/ ~r2most $_228 \/ $_230 == $_229 \/ % 0.87/1.07 u6r4 $_228 == $_229 \/ u6r4 $_228 == $_230 \/ f $_228 \/ % 0.87/1.07 r $_228 (u6r2 $_228) % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_230 \/ ~r2most $_228 \/ $_230 == $_229 \/ % 0.87/1.07 u6r4 $_228 == $_229 \/ u6r4 $_228 == $_230 \/ f $_228 \/ % 0.87/1.07 r $_228 (u6r1 $_228) % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_230 \/ ~r2most $_228 \/ $_230 == $_229 \/ % 0.87/1.07 u6r4 $_228 == $_229 \/ u6r4 $_228 == $_230 \/ c (u6r2 $_228) \/ f $_228 % 0.87/1.07 |- ~r $_228 $_229 \/ ~r $_228 $_230 \/ ~r2most $_228 \/ $_230 == $_229 \/ % 0.87/1.07 u6r4 $_228 == $_229 \/ u6r4 $_228 == $_230 \/ c (u6r1 $_228) \/ f $_228 % 0.87/1.07 |- ~r exist $_231 \/ $_231 == $_231 \/ $_231 == u4r1 exist % 0.87/1.07 |- ~r exist $_231 \/ $_231 == $_231 \/ $_231 == u4r2 exist % 0.87/1.07 |- ~r exist $_230 \/ $_230 == $_230 \/ u4r1 exist == $_230 % 0.87/1.07 |- ~r exist $_230 \/ $_230 == $_230 \/ u4r2 exist == $_230 % 0.87/1.07 |- ~r exist $_237 \/ $_237 == u4r1 exist \/ $_237 == u6r1 exist \/ % 0.87/1.07 u6r1 exist == u4r1 exist \/ d (u6r4 exist) % 0.87/1.07 |- ~r exist $_237 \/ $_237 == u4r1 exist \/ $_237 == u6r1 exist \/ % 0.87/1.07 u6r1 exist == u4r1 exist \/ d (u6r3 exist) % 0.87/1.07 |- ~r exist $_237 \/ $_237 == u4r1 exist \/ $_237 == u6r2 exist \/ % 0.87/1.07 u6r2 exist == u4r1 exist \/ d (u6r4 exist) % 0.87/1.07 |- ~r exist $_237 \/ $_237 == u4r1 exist \/ $_237 == u6r2 exist \/ % 0.87/1.07 u6r2 exist == u4r1 exist \/ d (u6r3 exist) % 0.87/1.07 |- ~r exist $_237 \/ $_237 == u4r1 exist \/ $_237 == u6r3 exist \/ % 0.87/1.07 u6r3 exist == u4r1 exist \/ r exist (u6r2 exist) % 0.87/1.07 |- ~r exist $_237 \/ $_237 == u4r1 exist \/ $_237 == u6r3 exist \/ % 0.87/1.07 u6r3 exist == u4r1 exist \/ r exist (u6r1 exist) % 0.87/1.07 |- ~r exist $_237 \/ $_237 == u4r1 exist \/ $_237 == u6r3 exist \/ % 0.87/1.07 u6r3 exist == u4r1 exist \/ c (u6r2 exist) % 0.87/1.07 |- ~r exist $_237 \/ $_237 == u4r1 exist \/ $_237 == u6r3 exist \/ % 0.87/1.07 u6r3 exist == u4r1 exist \/ c (u6r1 exist) % 0.87/1.07 |- ~r exist $_237 \/ $_237 == u4r1 exist \/ $_237 == u6r4 exist \/ % 0.87/1.07 u6r4 exist == u4r1 exist \/ r exist (u6r2 exist) % 0.87/1.07 |- ~r exist $_237 \/ $_237 == u4r1 exist \/ $_237 == u6r4 exist \/ % 0.87/1.07 u6r4 exist == u4r1 exist \/ r exist (u6r1 exist) % 0.87/1.07 |- ~r exist $_237 \/ $_237 == u4r1 exist \/ $_237 == u6r4 exist \/ % 0.87/1.07 u6r4 exist == u4r1 exist \/ c (u6r2 exist) % 0.87/1.07 |- ~r exist $_237 \/ $_237 == u4r1 exist \/ $_237 == u6r4 exist \/ % 0.87/1.07 u6r4 exist == u4r1 exist \/ c (u6r1 exist) % 0.87/1.07 |- ~r exist $_237 \/ $_237 == u4r1 exist \/ $_237 == u4r2 exist \/ % 0.87/1.07 u4r2 exist == u4r1 exist % 0.87/1.07 |- ~r exist $_236 \/ $_236 == u4r1 exist \/ u6r1 exist == $_236 \/ % 0.87/1.07 u6r1 exist == u4r1 exist \/ d (u6r4 exist) % 0.87/1.07 |- ~r exist $_236 \/ $_236 == u4r1 exist \/ u6r1 exist == $_236 \/ % 0.87/1.07 u6r1 exist == u4r1 exist \/ d (u6r3 exist) % 0.87/1.07 |- ~r exist $_236 \/ $_236 == u4r1 exist \/ u6r2 exist == $_236 \/ % 0.87/1.07 u6r2 exist == u4r1 exist \/ d (u6r4 exist) % 0.87/1.07 |- ~r exist $_236 \/ $_236 == u4r1 exist \/ u6r2 exist == $_236 \/ % 0.87/1.07 u6r2 exist == u4r1 exist \/ d (u6r3 exist) % 0.87/1.07 |- ~r exist $_236 \/ $_236 == u4r1 exist \/ u6r3 exist == $_236 \/ % 0.87/1.07 u6r3 exist == u4r1 exist \/ r exist (u6r2 exist) % 0.87/1.07 |- ~r exist $_236 \/ $_236 == u4r1 exist \/ u6r3 exist == $_236 \/ % 0.87/1.07 u6r3 exist == u4r1 exist \/ r exist (u6r1 exist) % 0.87/1.07 |- ~r exist $_236 \/ $_236 == u4r1 exist \/ u6r3 exist == $_236 \/ % 0.87/1.07 u6r3 exist == u4r1 exist \/ c (u6r2 exist) % 0.87/1.07 |- ~r exist $_236 \/ $_236 == u4r1 exist \/ u6r3 exist == $_236 \/ % 0.87/1.07 u6r3 exist == u4r1 exist \/ c (u6r1 exist) % 0.87/1.07 |- ~r exist $_236 \/ $_236 == u4r1 exist \/ u6r4 exist == $_236 \/ % 0.87/1.07 u6r4 exist == u4r1 exist \/ r exist (u6r2 exist) % 0.87/1.07 |- ~r exist $_236 \/ $_236 == u4r1 exist \/ u6r4 exist == $_236 \/ % 0.87/1.07 u6r4 exist == u4r1 exist \/ r exist (u6r1 exist) % 0.87/1.07 |- ~r exist $_236 \/ $_236 == u4r1 exist \/ u6r4 exist == $_236 \/ % 0.87/1.07 u6r4 exist == u4r1 exist \/ c (u6r2 exist) % 0.87/1.07 |- ~r exist $_236 \/ $_236 == u4r1 exist \/ u6r4 exist == $_236 \/ % 0.87/1.07 u6r4 exist == u4r1 exist \/ c (u6r1 exist) % 0.87/1.07 |- ~r exist $_236 \/ $_236 == u4r1 exist \/ u4r2 exist == $_236 \/ % 0.87/1.07 u4r2 exist == u4r1 exist % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u6r1 exist == u4r1 exist \/ % 0.87/1.07 u6r1 exist == u4r2 exist \/ d (u6r4 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u6r1 exist == u4r1 exist \/ % 0.87/1.07 u6r1 exist == u4r2 exist \/ d (u6r3 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u6r2 exist == u4r1 exist \/ % 0.87/1.07 u6r2 exist == u4r2 exist \/ d (u6r4 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u6r2 exist == u4r1 exist \/ % 0.87/1.07 u6r2 exist == u4r2 exist \/ d (u6r3 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.87/1.07 u6r3 exist == u4r2 exist \/ r exist (u6r2 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.87/1.07 u6r3 exist == u4r2 exist \/ r exist (u6r1 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.87/1.07 u6r3 exist == u4r2 exist \/ c (u6r2 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.87/1.07 u6r3 exist == u4r2 exist \/ c (u6r1 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.87/1.07 u6r4 exist == u4r2 exist \/ r exist (u6r2 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.87/1.07 u6r4 exist == u4r2 exist \/ r exist (u6r1 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.87/1.07 u6r4 exist == u4r2 exist \/ c (u6r2 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.87/1.07 u6r4 exist == u4r2 exist \/ c (u6r1 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u4r2 exist == u6r1 exist \/ % 0.87/1.07 u6r1 exist == u4r1 exist \/ d (u6r4 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u4r2 exist == u6r1 exist \/ % 0.87/1.07 u6r1 exist == u4r1 exist \/ d (u6r3 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u4r2 exist == u6r2 exist \/ % 0.87/1.07 u6r2 exist == u4r1 exist \/ d (u6r4 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u4r2 exist == u6r2 exist \/ % 0.87/1.07 u6r2 exist == u4r1 exist \/ d (u6r3 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.87/1.07 u6r3 exist == u4r1 exist \/ r exist (u6r2 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.87/1.07 u6r3 exist == u4r1 exist \/ r exist (u6r1 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.87/1.07 u6r3 exist == u4r1 exist \/ c (u6r2 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.87/1.07 u6r3 exist == u4r1 exist \/ c (u6r1 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.87/1.07 u6r4 exist == u4r1 exist \/ r exist (u6r2 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.87/1.07 u6r4 exist == u4r1 exist \/ r exist (u6r1 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.87/1.07 u6r4 exist == u4r1 exist \/ c (u6r2 exist) % 0.87/1.07 |- u4r2 exist == u4r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.87/1.07 u6r4 exist == u4r1 exist \/ c (u6r1 exist) % 0.87/1.07 |- ~r exist $_241 \/ $_241 == u6r1 exist \/ u4r1 exist == $_241 \/ % 0.87/1.07 u4r1 exist == u6r1 exist \/ d (u6r4 exist) % 0.87/1.07 |- ~r exist $_241 \/ $_241 == u6r1 exist \/ u4r1 exist == $_241 \/ % 0.87/1.07 u4r1 exist == u6r1 exist \/ d (u6r3 exist) % 0.87/1.07 |- ~r exist $_241 \/ $_241 == u6r2 exist \/ u4r1 exist == $_241 \/ % 0.87/1.07 u4r1 exist == u6r2 exist \/ d (u6r4 exist) % 0.87/1.07 |- ~r exist $_241 \/ $_241 == u6r2 exist \/ u4r1 exist == $_241 \/ % 0.87/1.07 u4r1 exist == u6r2 exist \/ d (u6r3 exist) % 0.87/1.07 |- ~r exist $_241 \/ $_241 == u6r3 exist \/ u4r1 exist == $_241 \/ % 0.87/1.07 u4r1 exist == u6r3 exist \/ r exist (u6r2 exist) % 0.87/1.07 |- ~r exist $_241 \/ $_241 == u6r3 exist \/ u4r1 exist == $_241 \/ % 0.87/1.07 u4r1 exist == u6r3 exist \/ r exist (u6r1 exist) % 0.87/1.07 |- ~r exist $_241 \/ $_241 == u6r3 exist \/ u4r1 exist == $_241 \/ % 0.87/1.07 u4r1 exist == u6r3 exist \/ c (u6r2 exist) % 0.87/1.07 |- ~r exist $_241 \/ $_241 == u6r3 exist \/ u4r1 exist == $_241 \/ % 0.87/1.07 u4r1 exist == u6r3 exist \/ c (u6r1 exist) % 0.87/1.07 |- ~r exist $_241 \/ $_241 == u6r4 exist \/ u4r1 exist == $_241 \/ % 0.87/1.07 u4r1 exist == u6r4 exist \/ r exist (u6r2 exist) % 0.87/1.07 |- ~r exist $_241 \/ $_241 == u6r4 exist \/ u4r1 exist == $_241 \/ % 0.87/1.07 u4r1 exist == u6r4 exist \/ r exist (u6r1 exist) % 0.87/1.07 |- ~r exist $_241 \/ $_241 == u6r4 exist \/ u4r1 exist == $_241 \/ % 0.87/1.07 u4r1 exist == u6r4 exist \/ c (u6r2 exist) % 0.87/1.07 |- ~r exist $_241 \/ $_241 == u6r4 exist \/ u4r1 exist == $_241 \/ % 0.87/1.07 u4r1 exist == u6r4 exist \/ c (u6r1 exist) % 0.87/1.07 |- ~r exist $_241 \/ $_241 == u4r2 exist \/ u4r1 exist == $_241 \/ % 0.87/1.07 u4r1 exist == u4r2 exist % 0.87/1.07 |- ~r exist $_240 \/ u4r1 exist == $_240 \/ u4r1 exist == u6r1 exist \/ % 0.87/1.07 u6r1 exist == $_240 \/ d (u6r4 exist) % 0.87/1.07 |- ~r exist $_240 \/ u4r1 exist == $_240 \/ u4r1 exist == u6r1 exist \/ % 0.87/1.07 u6r1 exist == $_240 \/ d (u6r3 exist) % 0.87/1.07 |- ~r exist $_240 \/ u4r1 exist == $_240 \/ u4r1 exist == u6r2 exist \/ % 0.87/1.07 u6r2 exist == $_240 \/ d (u6r4 exist) % 0.87/1.08 |- ~r exist $_240 \/ u4r1 exist == $_240 \/ u4r1 exist == u6r2 exist \/ % 0.87/1.08 u6r2 exist == $_240 \/ d (u6r3 exist) % 0.87/1.08 |- ~r exist $_240 \/ u4r1 exist == $_240 \/ u4r1 exist == u6r3 exist \/ % 0.87/1.08 u6r3 exist == $_240 \/ r exist (u6r2 exist) % 0.87/1.08 |- ~r exist $_240 \/ u4r1 exist == $_240 \/ u4r1 exist == u6r3 exist \/ % 0.87/1.08 u6r3 exist == $_240 \/ r exist (u6r1 exist) % 0.87/1.08 |- ~r exist $_240 \/ u4r1 exist == $_240 \/ u4r1 exist == u6r3 exist \/ % 0.87/1.08 u6r3 exist == $_240 \/ c (u6r2 exist) % 0.87/1.08 |- ~r exist $_240 \/ u4r1 exist == $_240 \/ u4r1 exist == u6r3 exist \/ % 0.87/1.08 u6r3 exist == $_240 \/ c (u6r1 exist) % 0.87/1.08 |- ~r exist $_240 \/ u4r1 exist == $_240 \/ u4r1 exist == u6r4 exist \/ % 0.87/1.08 u6r4 exist == $_240 \/ r exist (u6r2 exist) % 0.87/1.08 |- ~r exist $_240 \/ u4r1 exist == $_240 \/ u4r1 exist == u6r4 exist \/ % 0.87/1.08 u6r4 exist == $_240 \/ r exist (u6r1 exist) % 0.87/1.08 |- ~r exist $_240 \/ u4r1 exist == $_240 \/ u4r1 exist == u6r4 exist \/ % 0.87/1.08 u6r4 exist == $_240 \/ c (u6r2 exist) % 0.87/1.08 |- ~r exist $_240 \/ u4r1 exist == $_240 \/ u4r1 exist == u6r4 exist \/ % 0.87/1.08 u6r4 exist == $_240 \/ c (u6r1 exist) % 0.87/1.08 |- ~r exist $_240 \/ u4r1 exist == $_240 \/ u4r1 exist == u4r2 exist \/ % 0.87/1.08 u4r2 exist == $_240 % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r1 exist \/ % 0.87/1.08 u6r1 exist == u4r2 exist \/ d (u6r4 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r1 exist \/ % 0.87/1.08 u6r1 exist == u4r2 exist \/ d (u6r3 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r2 exist \/ % 0.87/1.08 u6r2 exist == u4r2 exist \/ d (u6r4 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r2 exist \/ % 0.87/1.08 u6r2 exist == u4r2 exist \/ d (u6r3 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.87/1.08 u6r3 exist == u4r2 exist \/ r exist (u6r2 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.87/1.08 u6r3 exist == u4r2 exist \/ r exist (u6r1 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.87/1.08 u6r3 exist == u4r2 exist \/ c (u6r2 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.87/1.08 u6r3 exist == u4r2 exist \/ c (u6r1 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.87/1.08 u6r4 exist == u4r2 exist \/ r exist (u6r2 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.87/1.08 u6r4 exist == u4r2 exist \/ r exist (u6r1 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.87/1.08 u6r4 exist == u4r2 exist \/ c (u6r2 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.87/1.08 u6r4 exist == u4r2 exist \/ c (u6r1 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r1 exist \/ % 0.87/1.08 u4r2 exist == u6r1 exist \/ d (u6r4 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r1 exist \/ % 0.87/1.08 u4r2 exist == u6r1 exist \/ d (u6r3 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r2 exist \/ % 0.87/1.08 u4r2 exist == u6r2 exist \/ d (u6r4 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r2 exist \/ % 0.87/1.08 u4r2 exist == u6r2 exist \/ d (u6r3 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.87/1.08 u4r2 exist == u6r3 exist \/ r exist (u6r2 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.87/1.08 u4r2 exist == u6r3 exist \/ r exist (u6r1 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.87/1.08 u4r2 exist == u6r3 exist \/ c (u6r2 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.87/1.08 u4r2 exist == u6r3 exist \/ c (u6r1 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.87/1.08 u4r2 exist == u6r4 exist \/ r exist (u6r2 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.87/1.08 u4r2 exist == u6r4 exist \/ r exist (u6r1 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.87/1.08 u4r2 exist == u6r4 exist \/ c (u6r2 exist) % 0.87/1.08 |- u4r1 exist == u4r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.87/1.08 u4r2 exist == u6r4 exist \/ c (u6r1 exist) % 0.87/1.08 |- u6r1 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.87/1.08 u6r3 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.87/1.08 |- u6r1 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.87/1.08 u6r3 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.87/1.08 |- u6r1 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.87/1.08 u6r3 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.87/1.08 |- u6r1 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.87/1.08 u6r3 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.87/1.08 |- u6r1 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.87/1.08 u6r4 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.87/1.08 |- u6r1 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.87/1.08 u6r4 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.87/1.08 |- u6r1 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.87/1.08 u6r4 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.87/1.08 |- u6r1 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.87/1.08 u6r4 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.87/1.08 |- u6r1 exist == u4r1 exist \/ u6r2 exist == u4r1 exist \/ d (u6r3 exist) % 0.87/1.08 |- u6r2 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.87/1.08 u6r3 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.87/1.08 |- u6r2 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.87/1.08 u6r3 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.87/1.08 |- u6r2 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.87/1.08 u6r3 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u6r2 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.08 u6r3 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u6r2 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.08 u6r4 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.08 |- u6r2 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.08 u6r4 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.08 |- u6r2 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.08 u6r4 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u6r2 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.08 u6r4 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u6r1 exist == u4r1 exist \/ u6r1 exist == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u4r1 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.08 |- u6r1 exist == u4r1 exist \/ u6r1 exist == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u4r1 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.08 |- u6r1 exist == u4r1 exist \/ u6r1 exist == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u4r1 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u6r1 exist == u4r1 exist \/ u6r1 exist == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u4r1 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u6r1 exist == u4r1 exist \/ u6r1 exist == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u4r1 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.08 |- u6r1 exist == u4r1 exist \/ u6r1 exist == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u4r1 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.08 |- u6r1 exist == u4r1 exist \/ u6r1 exist == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u4r1 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u6r1 exist == u4r1 exist \/ u6r1 exist == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u4r1 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u6r2 exist == u4r1 exist \/ u6r2 exist == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u4r1 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.08 |- u6r2 exist == u4r1 exist \/ u6r2 exist == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u4r1 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.08 |- u6r2 exist == u4r1 exist \/ u6r2 exist == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u4r1 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u6r2 exist == u4r1 exist \/ u6r2 exist == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u4r1 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u6r2 exist == u4r1 exist \/ u6r2 exist == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u4r1 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.08 |- u6r2 exist == u4r1 exist \/ u6r2 exist == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u4r1 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.08 |- u6r2 exist == u4r1 exist \/ u6r2 exist == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u4r1 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u6r2 exist == u4r1 exist \/ u6r2 exist == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u4r1 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.08 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.08 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.08 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.08 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r2 exist \/ d (u6r3 exist) % 0.92/1.08 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.08 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.08 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.08 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.08 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.08 u6r1 exist == u6r3 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.08 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.08 u6r1 exist == u6r3 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.08 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.08 u6r1 exist == u6r3 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.08 u6r1 exist == u6r3 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.08 u6r1 exist == u6r4 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.08 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.08 u6r1 exist == u6r4 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.08 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.08 u6r1 exist == u6r4 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.08 u6r1 exist == u6r4 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.08 u6r2 exist == u6r3 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.08 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.08 u6r2 exist == u6r3 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.08 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.08 u6r2 exist == u6r3 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.08 u6r2 exist == u6r3 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.08 u6r2 exist == u6r4 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.08 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.08 u6r2 exist == u6r4 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.08 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.08 u6r2 exist == u6r4 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.08 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.08 u6r2 exist == u6r4 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.08 |- ~r exist $_253 \/ $_253 == u4r2 exist \/ $_253 == u6r1 exist \/ % 0.92/1.08 u6r1 exist == u4r2 exist \/ d (u6r4 exist) % 0.92/1.08 |- ~r exist $_253 \/ $_253 == u4r2 exist \/ $_253 == u6r1 exist \/ % 0.92/1.08 u6r1 exist == u4r2 exist \/ d (u6r3 exist) % 0.92/1.08 |- ~r exist $_253 \/ $_253 == u4r2 exist \/ $_253 == u6r2 exist \/ % 0.92/1.08 u6r2 exist == u4r2 exist \/ d (u6r4 exist) % 0.92/1.08 |- ~r exist $_253 \/ $_253 == u4r2 exist \/ $_253 == u6r2 exist \/ % 0.92/1.08 u6r2 exist == u4r2 exist \/ d (u6r3 exist) % 0.92/1.08 |- ~r exist $_253 \/ $_253 == u4r2 exist \/ $_253 == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u4r2 exist \/ r exist (u6r2 exist) % 0.92/1.08 |- ~r exist $_253 \/ $_253 == u4r2 exist \/ $_253 == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u4r2 exist \/ r exist (u6r1 exist) % 0.92/1.08 |- ~r exist $_253 \/ $_253 == u4r2 exist \/ $_253 == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u4r2 exist \/ c (u6r2 exist) % 0.92/1.08 |- ~r exist $_253 \/ $_253 == u4r2 exist \/ $_253 == u6r3 exist \/ % 0.92/1.08 u6r3 exist == u4r2 exist \/ c (u6r1 exist) % 0.92/1.08 |- ~r exist $_253 \/ $_253 == u4r2 exist \/ $_253 == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u4r2 exist \/ r exist (u6r2 exist) % 0.92/1.08 |- ~r exist $_253 \/ $_253 == u4r2 exist \/ $_253 == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u4r2 exist \/ r exist (u6r1 exist) % 0.92/1.08 |- ~r exist $_253 \/ $_253 == u4r2 exist \/ $_253 == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u4r2 exist \/ c (u6r2 exist) % 0.92/1.08 |- ~r exist $_253 \/ $_253 == u4r2 exist \/ $_253 == u6r4 exist \/ % 0.92/1.08 u6r4 exist == u4r2 exist \/ c (u6r1 exist) % 0.92/1.08 |- ~r exist $_253 \/ $_253 == u4r1 exist \/ $_253 == u4r2 exist \/ % 0.92/1.08 u4r1 exist == u4r2 exist % 0.92/1.08 |- ~r exist $_252 \/ $_252 == u4r2 exist \/ u6r1 exist == $_252 \/ % 0.92/1.08 u6r1 exist == u4r2 exist \/ d (u6r4 exist) % 0.92/1.08 |- ~r exist $_252 \/ $_252 == u4r2 exist \/ u6r1 exist == $_252 \/ % 0.92/1.08 u6r1 exist == u4r2 exist \/ d (u6r3 exist) % 0.92/1.08 |- ~r exist $_252 \/ $_252 == u4r2 exist \/ u6r2 exist == $_252 \/ % 0.92/1.08 u6r2 exist == u4r2 exist \/ d (u6r4 exist) % 0.92/1.08 |- ~r exist $_252 \/ $_252 == u4r2 exist \/ u6r2 exist == $_252 \/ % 0.92/1.08 u6r2 exist == u4r2 exist \/ d (u6r3 exist) % 0.92/1.09 |- ~r exist $_252 \/ $_252 == u4r2 exist \/ u6r3 exist == $_252 \/ % 0.92/1.09 u6r3 exist == u4r2 exist \/ r exist (u6r2 exist) % 0.92/1.09 |- ~r exist $_252 \/ $_252 == u4r2 exist \/ u6r3 exist == $_252 \/ % 0.92/1.09 u6r3 exist == u4r2 exist \/ r exist (u6r1 exist) % 0.92/1.09 |- ~r exist $_252 \/ $_252 == u4r2 exist \/ u6r3 exist == $_252 \/ % 0.92/1.09 u6r3 exist == u4r2 exist \/ c (u6r2 exist) % 0.92/1.09 |- ~r exist $_252 \/ $_252 == u4r2 exist \/ u6r3 exist == $_252 \/ % 0.92/1.09 u6r3 exist == u4r2 exist \/ c (u6r1 exist) % 0.92/1.09 |- ~r exist $_252 \/ $_252 == u4r2 exist \/ u6r4 exist == $_252 \/ % 0.92/1.09 u6r4 exist == u4r2 exist \/ r exist (u6r2 exist) % 0.92/1.09 |- ~r exist $_252 \/ $_252 == u4r2 exist \/ u6r4 exist == $_252 \/ % 0.92/1.09 u6r4 exist == u4r2 exist \/ r exist (u6r1 exist) % 0.92/1.09 |- ~r exist $_252 \/ $_252 == u4r2 exist \/ u6r4 exist == $_252 \/ % 0.92/1.09 u6r4 exist == u4r2 exist \/ c (u6r2 exist) % 0.92/1.09 |- ~r exist $_252 \/ $_252 == u4r2 exist \/ u6r4 exist == $_252 \/ % 0.92/1.09 u6r4 exist == u4r2 exist \/ c (u6r1 exist) % 0.92/1.09 |- u4r1 exist == u4r2 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.09 u6r1 exist == u4r2 exist \/ d (u6r4 exist) % 0.92/1.09 |- u4r1 exist == u4r2 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.09 u6r1 exist == u4r2 exist \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u4r2 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.09 u6r2 exist == u4r2 exist \/ d (u6r4 exist) % 0.92/1.09 |- u4r1 exist == u4r2 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.09 u6r2 exist == u4r2 exist \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u4r2 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.09 u6r3 exist == u4r2 exist \/ r exist (u6r2 exist) % 0.92/1.09 |- u4r1 exist == u4r2 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.09 u6r3 exist == u4r2 exist \/ r exist (u6r1 exist) % 0.92/1.09 |- u4r1 exist == u4r2 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.09 u6r3 exist == u4r2 exist \/ c (u6r2 exist) % 0.92/1.09 |- u4r1 exist == u4r2 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.09 u6r3 exist == u4r2 exist \/ c (u6r1 exist) % 0.92/1.09 |- u4r1 exist == u4r2 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.09 u6r4 exist == u4r2 exist \/ r exist (u6r2 exist) % 0.92/1.09 |- u4r1 exist == u4r2 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.09 u6r4 exist == u4r2 exist \/ r exist (u6r1 exist) % 0.92/1.09 |- u4r1 exist == u4r2 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.09 u6r4 exist == u4r2 exist \/ c (u6r2 exist) % 0.92/1.09 |- u4r1 exist == u4r2 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.09 u6r4 exist == u4r2 exist \/ c (u6r1 exist) % 0.92/1.09 |- u6r1 exist == u4r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.09 u6r3 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.09 |- u6r1 exist == u4r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.09 u6r3 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.09 |- u6r1 exist == u4r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.09 u6r3 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u6r1 exist == u4r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.09 u6r3 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u6r1 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.09 u6r4 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.09 |- u6r1 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.09 u6r4 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.09 |- u6r1 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.09 u6r4 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u6r1 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.09 u6r4 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u6r1 exist == u4r2 exist \/ u6r2 exist == u4r2 exist \/ d (u6r3 exist) % 0.92/1.09 |- u6r2 exist == u4r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.09 u6r3 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.09 |- u6r2 exist == u4r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.09 u6r3 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.09 |- u6r2 exist == u4r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.09 u6r3 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u6r2 exist == u4r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.09 u6r3 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u6r2 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.09 u6r4 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.09 |- u6r2 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.09 u6r4 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.09 |- u6r2 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.09 u6r4 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u6r2 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.09 u6r4 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u6r1 exist == u4r2 exist \/ u6r1 exist == u6r3 exist \/ % 0.92/1.09 u6r3 exist == u4r2 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.09 |- u6r1 exist == u4r2 exist \/ u6r1 exist == u6r3 exist \/ % 0.92/1.09 u6r3 exist == u4r2 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.09 |- u6r1 exist == u4r2 exist \/ u6r1 exist == u6r3 exist \/ % 0.92/1.09 u6r3 exist == u4r2 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u6r1 exist == u4r2 exist \/ u6r1 exist == u6r3 exist \/ % 0.92/1.09 u6r3 exist == u4r2 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u6r1 exist == u4r2 exist \/ u6r1 exist == u6r4 exist \/ % 0.92/1.09 u6r4 exist == u4r2 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.09 |- u6r1 exist == u4r2 exist \/ u6r1 exist == u6r4 exist \/ % 0.92/1.09 u6r4 exist == u4r2 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.09 |- u6r1 exist == u4r2 exist \/ u6r1 exist == u6r4 exist \/ % 0.92/1.09 u6r4 exist == u4r2 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u6r1 exist == u4r2 exist \/ u6r1 exist == u6r4 exist \/ % 0.92/1.09 u6r4 exist == u4r2 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u6r2 exist == u4r2 exist \/ u6r2 exist == u6r3 exist \/ % 0.92/1.09 u6r3 exist == u4r2 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.09 |- u6r2 exist == u4r2 exist \/ u6r2 exist == u6r3 exist \/ % 0.92/1.09 u6r3 exist == u4r2 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.09 |- u6r2 exist == u4r2 exist \/ u6r2 exist == u6r3 exist \/ % 0.92/1.09 u6r3 exist == u4r2 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u6r2 exist == u4r2 exist \/ u6r2 exist == u6r3 exist \/ % 0.92/1.09 u6r3 exist == u4r2 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u6r2 exist == u4r2 exist \/ u6r2 exist == u6r4 exist \/ % 0.92/1.09 u6r4 exist == u4r2 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.09 |- u6r2 exist == u4r2 exist \/ u6r2 exist == u6r4 exist \/ % 0.92/1.09 u6r4 exist == u4r2 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.09 |- u6r2 exist == u4r2 exist \/ u6r2 exist == u6r4 exist \/ % 0.92/1.09 u6r4 exist == u4r2 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u6r2 exist == u4r2 exist \/ u6r2 exist == u6r4 exist \/ % 0.92/1.09 u6r4 exist == u4r2 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.09 |- ~r exist $_260 \/ $_260 == u4r1 exist \/ $_260 == u6r1 exist \/ % 0.92/1.09 u4r1 exist == u6r1 exist \/ d (u6r4 exist) % 0.92/1.09 |- ~r exist $_260 \/ $_260 == u4r1 exist \/ $_260 == u6r1 exist \/ % 0.92/1.09 u4r1 exist == u6r1 exist \/ d (u6r3 exist) % 0.92/1.09 |- ~r exist $_260 \/ $_260 == u4r1 exist \/ $_260 == u6r2 exist \/ % 0.92/1.09 u4r1 exist == u6r2 exist \/ d (u6r4 exist) % 0.92/1.09 |- ~r exist $_260 \/ $_260 == u4r1 exist \/ $_260 == u6r2 exist \/ % 0.92/1.09 u4r1 exist == u6r2 exist \/ d (u6r3 exist) % 0.92/1.09 |- ~r exist $_260 \/ $_260 == u4r1 exist \/ $_260 == u6r3 exist \/ % 0.92/1.09 u4r1 exist == u6r3 exist \/ r exist (u6r2 exist) % 0.92/1.09 |- ~r exist $_260 \/ $_260 == u4r1 exist \/ $_260 == u6r3 exist \/ % 0.92/1.09 u4r1 exist == u6r3 exist \/ r exist (u6r1 exist) % 0.92/1.09 |- ~r exist $_260 \/ $_260 == u4r1 exist \/ $_260 == u6r3 exist \/ % 0.92/1.09 u4r1 exist == u6r3 exist \/ c (u6r2 exist) % 0.92/1.09 |- ~r exist $_260 \/ $_260 == u4r1 exist \/ $_260 == u6r3 exist \/ % 0.92/1.09 u4r1 exist == u6r3 exist \/ c (u6r1 exist) % 0.92/1.09 |- ~r exist $_260 \/ $_260 == u4r1 exist \/ $_260 == u6r4 exist \/ % 0.92/1.09 u4r1 exist == u6r4 exist \/ r exist (u6r2 exist) % 0.92/1.09 |- ~r exist $_260 \/ $_260 == u4r1 exist \/ $_260 == u6r4 exist \/ % 0.92/1.09 u4r1 exist == u6r4 exist \/ r exist (u6r1 exist) % 0.92/1.09 |- ~r exist $_260 \/ $_260 == u4r1 exist \/ $_260 == u6r4 exist \/ % 0.92/1.09 u4r1 exist == u6r4 exist \/ c (u6r2 exist) % 0.92/1.09 |- ~r exist $_260 \/ $_260 == u4r1 exist \/ $_260 == u6r4 exist \/ % 0.92/1.09 u4r1 exist == u6r4 exist \/ c (u6r1 exist) % 0.92/1.09 |- ~r exist $_259 \/ u4r1 exist == $_259 \/ u6r1 exist == $_259 \/ % 0.92/1.09 u6r1 exist == u4r1 exist \/ d (u6r4 exist) % 0.92/1.09 |- ~r exist $_259 \/ u4r1 exist == $_259 \/ u6r1 exist == $_259 \/ % 0.92/1.09 u6r1 exist == u4r1 exist \/ d (u6r3 exist) % 0.92/1.09 |- ~r exist $_259 \/ u4r1 exist == $_259 \/ u6r2 exist == $_259 \/ % 0.92/1.09 u6r2 exist == u4r1 exist \/ d (u6r4 exist) % 0.92/1.09 |- ~r exist $_259 \/ u4r1 exist == $_259 \/ u6r2 exist == $_259 \/ % 0.92/1.09 u6r2 exist == u4r1 exist \/ d (u6r3 exist) % 0.92/1.09 |- ~r exist $_259 \/ u4r1 exist == $_259 \/ u6r3 exist == $_259 \/ % 0.92/1.09 u6r3 exist == u4r1 exist \/ r exist (u6r2 exist) % 0.92/1.09 |- ~r exist $_259 \/ u4r1 exist == $_259 \/ u6r3 exist == $_259 \/ % 0.92/1.09 u6r3 exist == u4r1 exist \/ r exist (u6r1 exist) % 0.92/1.09 |- ~r exist $_259 \/ u4r1 exist == $_259 \/ u6r3 exist == $_259 \/ % 0.92/1.09 u6r3 exist == u4r1 exist \/ c (u6r2 exist) % 0.92/1.09 |- ~r exist $_259 \/ u4r1 exist == $_259 \/ u6r3 exist == $_259 \/ % 0.92/1.09 u6r3 exist == u4r1 exist \/ c (u6r1 exist) % 0.92/1.09 |- ~r exist $_259 \/ u4r1 exist == $_259 \/ u6r4 exist == $_259 \/ % 0.92/1.09 u6r4 exist == u4r1 exist \/ r exist (u6r2 exist) % 0.92/1.09 |- ~r exist $_259 \/ u4r1 exist == $_259 \/ u6r4 exist == $_259 \/ % 0.92/1.09 u6r4 exist == u4r1 exist \/ r exist (u6r1 exist) % 0.92/1.09 |- ~r exist $_259 \/ u4r1 exist == $_259 \/ u6r4 exist == $_259 \/ % 0.92/1.09 u6r4 exist == u4r1 exist \/ c (u6r2 exist) % 0.92/1.09 |- ~r exist $_259 \/ u4r1 exist == $_259 \/ u6r4 exist == $_259 \/ % 0.92/1.09 u6r4 exist == u4r1 exist \/ c (u6r1 exist) % 0.92/1.09 |- ~r exist $_259 \/ u4r1 exist == $_259 \/ u4r2 exist == $_259 \/ % 0.92/1.09 u4r2 exist == u4r1 exist % 0.92/1.09 |- u4r1 exist == u6r1 exist \/ u4r2 exist == u4r1 exist \/ % 0.92/1.09 u4r2 exist == u6r1 exist \/ d (u6r4 exist) % 0.92/1.09 |- u4r1 exist == u6r1 exist \/ u4r2 exist == u4r1 exist \/ % 0.92/1.09 u4r2 exist == u6r1 exist \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r2 exist \/ u4r2 exist == u4r1 exist \/ % 0.92/1.09 u4r2 exist == u6r2 exist \/ d (u6r4 exist) % 0.92/1.09 |- u4r1 exist == u6r2 exist \/ u4r2 exist == u4r1 exist \/ % 0.92/1.09 u4r2 exist == u6r2 exist \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r3 exist \/ u4r2 exist == u4r1 exist \/ % 0.92/1.09 u4r2 exist == u6r3 exist \/ r exist (u6r2 exist) % 0.92/1.09 |- u4r1 exist == u6r3 exist \/ u4r2 exist == u4r1 exist \/ % 0.92/1.09 u4r2 exist == u6r3 exist \/ r exist (u6r1 exist) % 0.92/1.09 |- u4r1 exist == u6r3 exist \/ u4r2 exist == u4r1 exist \/ % 0.92/1.09 u4r2 exist == u6r3 exist \/ c (u6r2 exist) % 0.92/1.09 |- u4r1 exist == u6r3 exist \/ u4r2 exist == u4r1 exist \/ % 0.92/1.09 u4r2 exist == u6r3 exist \/ c (u6r1 exist) % 0.92/1.09 |- u4r1 exist == u6r4 exist \/ u4r2 exist == u4r1 exist \/ % 0.92/1.09 u4r2 exist == u6r4 exist \/ r exist (u6r2 exist) % 0.92/1.09 |- u4r1 exist == u6r4 exist \/ u4r2 exist == u4r1 exist \/ % 0.92/1.09 u4r2 exist == u6r4 exist \/ r exist (u6r1 exist) % 0.92/1.09 |- u4r1 exist == u6r4 exist \/ u4r2 exist == u4r1 exist \/ % 0.92/1.09 u4r2 exist == u6r4 exist \/ c (u6r2 exist) % 0.92/1.09 |- u4r1 exist == u6r4 exist \/ u4r2 exist == u4r1 exist \/ % 0.92/1.09 u4r2 exist == u6r4 exist \/ c (u6r1 exist) % 0.92/1.09 |- u4r1 exist == u6r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.09 u6r3 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.09 |- u4r1 exist == u6r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.09 u6r3 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.09 |- u4r1 exist == u6r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.09 u6r3 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.09 u6r3 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.09 u6r4 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.09 |- u4r1 exist == u6r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.09 u6r4 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.09 |- u4r1 exist == u6r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.09 u6r4 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.09 u6r4 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r1 exist \/ u6r2 exist == u4r1 exist \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r2 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.09 u6r1 exist == u6r2 exist \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r2 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.09 u6r3 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.09 |- u4r1 exist == u6r2 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.09 u6r3 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.09 |- u4r1 exist == u6r2 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.09 u6r3 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r2 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.09 u6r3 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r2 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.09 u6r4 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.09 |- u4r1 exist == u6r2 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.09 u6r4 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.09 |- u4r1 exist == u6r2 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.09 u6r4 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r2 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.09 u6r4 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r3 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.09 u6r1 exist == u6r3 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.09 |- u4r1 exist == u6r3 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.09 u6r1 exist == u6r3 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.09 |- u4r1 exist == u6r3 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.09 u6r1 exist == u6r3 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r3 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.09 u6r1 exist == u6r3 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r4 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.09 u6r1 exist == u6r4 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.09 |- u4r1 exist == u6r4 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.09 u6r1 exist == u6r4 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.09 |- u4r1 exist == u6r4 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.09 u6r1 exist == u6r4 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r4 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.09 u6r1 exist == u6r4 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r3 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.09 u6r2 exist == u6r3 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.09 |- u4r1 exist == u6r3 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.09 u6r2 exist == u6r3 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.09 |- u4r1 exist == u6r3 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.09 u6r2 exist == u6r3 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r3 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.09 u6r2 exist == u6r3 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r4 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.09 u6r2 exist == u6r4 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.09 |- u4r1 exist == u6r4 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.09 u6r2 exist == u6r4 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.09 |- u4r1 exist == u6r4 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.09 u6r2 exist == u6r4 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.09 |- u4r1 exist == u6r4 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.09 u6r2 exist == u6r4 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.09 |- ~r exist $_267 \/ $_267 == u4r2 exist \/ $_267 == u6r1 exist \/ % 0.92/1.09 u4r2 exist == u6r1 exist \/ d (u6r4 exist) % 0.92/1.09 |- ~r exist $_267 \/ $_267 == u4r2 exist \/ $_267 == u6r1 exist \/ % 0.92/1.09 u4r2 exist == u6r1 exist \/ d (u6r3 exist) % 0.92/1.09 |- ~r exist $_267 \/ $_267 == u4r2 exist \/ $_267 == u6r2 exist \/ % 0.92/1.09 u4r2 exist == u6r2 exist \/ d (u6r4 exist) % 0.92/1.09 |- ~r exist $_267 \/ $_267 == u4r2 exist \/ $_267 == u6r2 exist \/ % 0.92/1.09 u4r2 exist == u6r2 exist \/ d (u6r3 exist) % 0.92/1.10 |- ~r exist $_267 \/ $_267 == u4r2 exist \/ $_267 == u6r3 exist \/ % 0.92/1.10 u4r2 exist == u6r3 exist \/ r exist (u6r2 exist) % 0.92/1.10 |- ~r exist $_267 \/ $_267 == u4r2 exist \/ $_267 == u6r3 exist \/ % 0.92/1.10 u4r2 exist == u6r3 exist \/ r exist (u6r1 exist) % 0.92/1.10 |- ~r exist $_267 \/ $_267 == u4r2 exist \/ $_267 == u6r3 exist \/ % 0.92/1.10 u4r2 exist == u6r3 exist \/ c (u6r2 exist) % 0.92/1.10 |- ~r exist $_267 \/ $_267 == u4r2 exist \/ $_267 == u6r3 exist \/ % 0.92/1.10 u4r2 exist == u6r3 exist \/ c (u6r1 exist) % 0.92/1.10 |- ~r exist $_267 \/ $_267 == u4r2 exist \/ $_267 == u6r4 exist \/ % 0.92/1.10 u4r2 exist == u6r4 exist \/ r exist (u6r2 exist) % 0.92/1.10 |- ~r exist $_267 \/ $_267 == u4r2 exist \/ $_267 == u6r4 exist \/ % 0.92/1.10 u4r2 exist == u6r4 exist \/ r exist (u6r1 exist) % 0.92/1.10 |- ~r exist $_267 \/ $_267 == u4r2 exist \/ $_267 == u6r4 exist \/ % 0.92/1.10 u4r2 exist == u6r4 exist \/ c (u6r2 exist) % 0.92/1.10 |- ~r exist $_267 \/ $_267 == u4r2 exist \/ $_267 == u6r4 exist \/ % 0.92/1.10 u4r2 exist == u6r4 exist \/ c (u6r1 exist) % 0.92/1.10 |- ~r exist $_266 \/ u4r2 exist == $_266 \/ u6r1 exist == $_266 \/ % 0.92/1.10 u6r1 exist == u4r2 exist \/ d (u6r4 exist) % 0.92/1.10 |- ~r exist $_266 \/ u4r2 exist == $_266 \/ u6r1 exist == $_266 \/ % 0.92/1.10 u6r1 exist == u4r2 exist \/ d (u6r3 exist) % 0.92/1.10 |- ~r exist $_266 \/ u4r2 exist == $_266 \/ u6r2 exist == $_266 \/ % 0.92/1.10 u6r2 exist == u4r2 exist \/ d (u6r4 exist) % 0.92/1.10 |- ~r exist $_266 \/ u4r2 exist == $_266 \/ u6r2 exist == $_266 \/ % 0.92/1.10 u6r2 exist == u4r2 exist \/ d (u6r3 exist) % 0.92/1.10 |- ~r exist $_266 \/ u4r2 exist == $_266 \/ u6r3 exist == $_266 \/ % 0.92/1.10 u6r3 exist == u4r2 exist \/ r exist (u6r2 exist) % 0.92/1.10 |- ~r exist $_266 \/ u4r2 exist == $_266 \/ u6r3 exist == $_266 \/ % 0.92/1.10 u6r3 exist == u4r2 exist \/ r exist (u6r1 exist) % 0.92/1.10 |- ~r exist $_266 \/ u4r2 exist == $_266 \/ u6r3 exist == $_266 \/ % 0.92/1.10 u6r3 exist == u4r2 exist \/ c (u6r2 exist) % 0.92/1.10 |- ~r exist $_266 \/ u4r2 exist == $_266 \/ u6r3 exist == $_266 \/ % 0.92/1.10 u6r3 exist == u4r2 exist \/ c (u6r1 exist) % 0.92/1.10 |- ~r exist $_266 \/ u4r2 exist == $_266 \/ u6r4 exist == $_266 \/ % 0.92/1.10 u6r4 exist == u4r2 exist \/ r exist (u6r2 exist) % 0.92/1.10 |- ~r exist $_266 \/ u4r2 exist == $_266 \/ u6r4 exist == $_266 \/ % 0.92/1.10 u6r4 exist == u4r2 exist \/ r exist (u6r1 exist) % 0.92/1.10 |- ~r exist $_266 \/ u4r2 exist == $_266 \/ u6r4 exist == $_266 \/ % 0.92/1.10 u6r4 exist == u4r2 exist \/ c (u6r2 exist) % 0.92/1.10 |- ~r exist $_266 \/ u4r2 exist == $_266 \/ u6r4 exist == $_266 \/ % 0.92/1.10 u6r4 exist == u4r2 exist \/ c (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.10 u6r4 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.10 u6r4 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.10 u6r4 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.10 u6r4 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r2 exist == u4r2 exist \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r2 exist \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.10 u6r4 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.10 u6r4 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.10 u6r4 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.10 u6r4 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r3 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r3 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r3 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r3 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r4 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r4 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r4 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r4 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r4 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r4 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r4 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r4 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r2 exist == u4r2 exist \/ % 0.92/1.10 u6r2 exist == u6r3 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r2 exist == u4r2 exist \/ % 0.92/1.10 u6r2 exist == u6r3 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r2 exist == u4r2 exist \/ % 0.92/1.10 u6r2 exist == u6r3 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r2 exist == u4r2 exist \/ % 0.92/1.10 u6r2 exist == u6r3 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r4 exist \/ u6r2 exist == u4r2 exist \/ % 0.92/1.10 u6r2 exist == u6r4 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r4 exist \/ u6r2 exist == u4r2 exist \/ % 0.92/1.10 u6r2 exist == u6r4 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r4 exist \/ u6r2 exist == u4r2 exist \/ % 0.92/1.10 u6r2 exist == u6r4 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r4 exist \/ u6r2 exist == u4r2 exist \/ % 0.92/1.10 u6r2 exist == u6r4 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.10 |- ~r exist $_273 \/ $_273 == u6r1 exist \/ u4r2 exist == $_273 \/ % 0.92/1.10 u4r2 exist == u6r1 exist \/ d (u6r4 exist) % 0.92/1.10 |- ~r exist $_273 \/ $_273 == u6r1 exist \/ u4r2 exist == $_273 \/ % 0.92/1.10 u4r2 exist == u6r1 exist \/ d (u6r3 exist) % 0.92/1.10 |- ~r exist $_273 \/ $_273 == u6r2 exist \/ u4r2 exist == $_273 \/ % 0.92/1.10 u4r2 exist == u6r2 exist \/ d (u6r4 exist) % 0.92/1.10 |- ~r exist $_273 \/ $_273 == u6r2 exist \/ u4r2 exist == $_273 \/ % 0.92/1.10 u4r2 exist == u6r2 exist \/ d (u6r3 exist) % 0.92/1.10 |- ~r exist $_273 \/ $_273 == u6r3 exist \/ u4r2 exist == $_273 \/ % 0.92/1.10 u4r2 exist == u6r3 exist \/ r exist (u6r2 exist) % 0.92/1.10 |- ~r exist $_273 \/ $_273 == u6r3 exist \/ u4r2 exist == $_273 \/ % 0.92/1.10 u4r2 exist == u6r3 exist \/ r exist (u6r1 exist) % 0.92/1.10 |- ~r exist $_273 \/ $_273 == u6r3 exist \/ u4r2 exist == $_273 \/ % 0.92/1.10 u4r2 exist == u6r3 exist \/ c (u6r2 exist) % 0.92/1.10 |- ~r exist $_273 \/ $_273 == u6r3 exist \/ u4r2 exist == $_273 \/ % 0.92/1.10 u4r2 exist == u6r3 exist \/ c (u6r1 exist) % 0.92/1.10 |- ~r exist $_273 \/ $_273 == u6r4 exist \/ u4r2 exist == $_273 \/ % 0.92/1.10 u4r2 exist == u6r4 exist \/ r exist (u6r2 exist) % 0.92/1.10 |- ~r exist $_273 \/ $_273 == u6r4 exist \/ u4r2 exist == $_273 \/ % 0.92/1.10 u4r2 exist == u6r4 exist \/ r exist (u6r1 exist) % 0.92/1.10 |- ~r exist $_273 \/ $_273 == u6r4 exist \/ u4r2 exist == $_273 \/ % 0.92/1.10 u4r2 exist == u6r4 exist \/ c (u6r2 exist) % 0.92/1.10 |- ~r exist $_273 \/ $_273 == u6r4 exist \/ u4r2 exist == $_273 \/ % 0.92/1.10 u4r2 exist == u6r4 exist \/ c (u6r1 exist) % 0.92/1.10 |- ~r exist $_272 \/ u4r2 exist == $_272 \/ u4r2 exist == u6r1 exist \/ % 0.92/1.10 u6r1 exist == $_272 \/ d (u6r4 exist) % 0.92/1.10 |- ~r exist $_272 \/ u4r2 exist == $_272 \/ u4r2 exist == u6r1 exist \/ % 0.92/1.10 u6r1 exist == $_272 \/ d (u6r3 exist) % 0.92/1.10 |- ~r exist $_272 \/ u4r2 exist == $_272 \/ u4r2 exist == u6r2 exist \/ % 0.92/1.10 u6r2 exist == $_272 \/ d (u6r4 exist) % 0.92/1.10 |- ~r exist $_272 \/ u4r2 exist == $_272 \/ u4r2 exist == u6r2 exist \/ % 0.92/1.10 u6r2 exist == $_272 \/ d (u6r3 exist) % 0.92/1.10 |- ~r exist $_272 \/ u4r2 exist == $_272 \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r3 exist == $_272 \/ r exist (u6r2 exist) % 0.92/1.10 |- ~r exist $_272 \/ u4r2 exist == $_272 \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r3 exist == $_272 \/ r exist (u6r1 exist) % 0.92/1.10 |- ~r exist $_272 \/ u4r2 exist == $_272 \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r3 exist == $_272 \/ c (u6r2 exist) % 0.92/1.10 |- ~r exist $_272 \/ u4r2 exist == $_272 \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r3 exist == $_272 \/ c (u6r1 exist) % 0.92/1.10 |- ~r exist $_272 \/ u4r2 exist == $_272 \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r4 exist == $_272 \/ r exist (u6r2 exist) % 0.92/1.10 |- ~r exist $_272 \/ u4r2 exist == $_272 \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r4 exist == $_272 \/ r exist (u6r1 exist) % 0.92/1.10 |- ~r exist $_272 \/ u4r2 exist == $_272 \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r4 exist == $_272 \/ c (u6r2 exist) % 0.92/1.10 |- ~r exist $_272 \/ u4r2 exist == $_272 \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r4 exist == $_272 \/ c (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r3 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r3 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r3 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r3 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r4 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r4 exist == u6r1 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r4 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r4 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r2 exist \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r3 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r3 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r3 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r3 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r4 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r4 exist == u6r2 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r4 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r4 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r1 exist == u6r3 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r1 exist == u6r3 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r1 exist == u6r3 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r1 exist == u6r3 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r1 exist == u6r4 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r1 exist == u6r4 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r1 exist == u6r4 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r1 exist == u6r4 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r2 exist == u6r3 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r2 exist == u6r3 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r2 exist == u6r3 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.10 u6r2 exist == u6r3 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r2 exist == u6r4 exist \/ d (u6r3 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r2 exist == u6r4 exist \/ d (u6r3 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r2 exist == u6r4 exist \/ c (u6r2 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.10 u6r2 exist == u6r4 exist \/ c (u6r1 exist) \/ d (u6r3 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.10 u6r4 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.10 u6r4 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.10 u6r4 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.10 u6r4 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r1 exist \/ u6r2 exist == u4r2 exist \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r2 exist \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.10 u6r4 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.10 u6r4 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.10 u6r4 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.10 u6r4 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r3 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r2 exist == u4r2 exist \/ % 0.92/1.10 u6r2 exist == u6r3 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r4 exist == u4r2 exist \/ c (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r3 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r2 exist == u4r2 exist \/ % 0.92/1.10 u6r2 exist == u6r3 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r4 exist == u4r2 exist \/ c (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r4 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r4 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r4 exist \/ u6r2 exist == u4r2 exist \/ % 0.92/1.10 u6r2 exist == u6r4 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r4 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r4 exist \/ c (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r4 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r4 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r4 exist \/ u6r2 exist == u4r2 exist \/ % 0.92/1.10 u6r2 exist == u6r4 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.10 |- u4r2 exist == u6r4 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.10 u6r3 exist == u6r4 exist \/ c (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r3 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r3 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r4 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r4 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r4 exist \/ u6r1 exist == u4r2 exist \/ % 0.92/1.10 u6r1 exist == u6r4 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r2 exist == u4r2 exist \/ % 0.92/1.10 u6r2 exist == u6r3 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.10 |- u4r2 exist == u6r3 exist \/ u6r2 exist == u4r2 exist \/ % 0.92/1.10 u6r2 exist == u6r3 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u4r2 exist == u6r4 exist \/ u6r2 exist == u4r2 exist \/ % 0.92/1.11 u6r2 exist == u6r4 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u4r2 exist == u6r4 exist \/ u6r2 exist == u4r2 exist \/ % 0.92/1.11 u6r2 exist == u6r4 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r2 exist \/ d (u6r4 exist) % 0.92/1.11 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.11 u6r1 exist == u6r3 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.11 u6r2 exist == u6r3 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r2 exist == u6r3 exist \/ u4r2 exist == u6r4 exist \/ c (u6r2 exist) % 0.92/1.11 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.11 u6r1 exist == u6r3 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.11 u6r2 exist == u6r3 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r2 exist == u6r3 exist \/ u4r2 exist == u6r4 exist \/ c (u6r1 exist) % 0.92/1.11 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.11 u6r1 exist == u6r4 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.11 u6r2 exist == u6r4 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.11 u6r1 exist == u6r4 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.11 u6r2 exist == u6r4 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.11 u6r1 exist == u6r3 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.11 u6r1 exist == u6r3 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.11 u6r1 exist == u6r4 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u4r2 exist == u6r1 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.11 u6r1 exist == u6r4 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.11 u6r2 exist == u6r3 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r3 exist \/ % 0.92/1.11 u6r2 exist == u6r3 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.11 u6r2 exist == u6r4 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u4r2 exist == u6r2 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.11 u6r2 exist == u6r4 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u6r1 exist == u4r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.11 u6r3 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u6r1 exist == u4r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.11 u6r3 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u6r1 exist == u4r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.11 u6r3 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r1 exist == u4r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.11 u6r3 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r1 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.11 u6r4 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u6r1 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.11 u6r4 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u6r1 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.11 u6r4 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r1 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.11 u6r4 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r1 exist == u4r2 exist \/ u6r2 exist == u4r2 exist \/ d (u6r4 exist) % 0.92/1.11 |- u6r2 exist == u4r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.11 u6r3 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u6r2 exist == u4r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.11 u6r3 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u6r2 exist == u4r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.11 u6r3 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r2 exist == u4r2 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.11 u6r3 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r2 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.11 u6r4 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u6r2 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.11 u6r4 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u6r2 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.11 u6r4 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r2 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.11 u6r4 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r1 exist == u4r2 exist \/ u6r1 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u4r2 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r2 exist == u4r2 exist \/ u6r2 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u4r2 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r3 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ c (u6r2 exist) % 0.92/1.11 |- u6r1 exist == u4r2 exist \/ u6r1 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u4r2 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r2 exist == u4r2 exist \/ u6r2 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u4r2 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r3 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ c (u6r1 exist) % 0.92/1.11 |- u6r1 exist == u4r2 exist \/ u6r1 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u4r2 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r2 exist == u4r2 exist \/ u6r2 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u4r2 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r1 exist == u4r2 exist \/ u6r1 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u4r2 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r2 exist == u4r2 exist \/ u6r2 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u4r2 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r1 exist == u4r2 exist \/ u6r1 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u4r2 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u6r1 exist == u4r2 exist \/ u6r1 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u4r2 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u6r1 exist == u4r2 exist \/ u6r1 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u4r2 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u6r1 exist == u4r2 exist \/ u6r1 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u4r2 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u6r2 exist == u4r2 exist \/ u6r2 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u4r2 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u6r2 exist == u4r2 exist \/ u6r2 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u4r2 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u6r2 exist == u4r2 exist \/ u6r2 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u4r2 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u6r2 exist == u4r2 exist \/ u6r2 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u4r2 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u4r1 exist == u6r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u4r1 exist == u6r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u4r1 exist == u6r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.11 u6r4 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u4r1 exist == u6r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.11 u6r4 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u4r1 exist == u6r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.11 u6r4 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.11 u6r4 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r1 exist \/ u6r2 exist == u4r1 exist \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r2 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.11 u6r1 exist == u6r2 exist \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r2 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u4r1 exist == u6r2 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u4r1 exist == u6r2 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r2 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r2 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.11 u6r4 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u4r1 exist == u6r2 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.11 u6r4 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u4r1 exist == u6r2 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.11 u6r4 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r2 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.11 u6r4 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r3 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.11 u6r1 exist == u6r3 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r3 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.11 u6r2 exist == u6r3 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r3 exist \/ u6r4 exist == u4r1 exist \/ c (u6r2 exist) % 0.92/1.11 |- u4r1 exist == u6r3 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.11 u6r1 exist == u6r3 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r3 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.11 u6r2 exist == u6r3 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r3 exist \/ u6r4 exist == u4r1 exist \/ c (u6r1 exist) % 0.92/1.11 |- u4r1 exist == u6r4 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.11 u6r1 exist == u6r4 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r4 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.11 u6r2 exist == u6r4 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r4 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r4 exist \/ c (u6r2 exist) % 0.92/1.11 |- u4r1 exist == u6r4 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.11 u6r1 exist == u6r4 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r4 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.11 u6r2 exist == u6r4 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u4r1 exist == u6r4 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r4 exist \/ c (u6r1 exist) % 0.92/1.11 |- u4r1 exist == u6r3 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.11 u6r1 exist == u6r3 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u4r1 exist == u6r3 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.11 u6r1 exist == u6r3 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u4r1 exist == u6r4 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.11 u6r1 exist == u6r4 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u4r1 exist == u6r4 exist \/ u6r1 exist == u4r1 exist \/ % 0.92/1.11 u6r1 exist == u6r4 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u4r1 exist == u6r3 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.11 u6r2 exist == u6r3 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u4r1 exist == u6r3 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.11 u6r2 exist == u6r3 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u4r1 exist == u6r4 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.11 u6r2 exist == u6r4 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u4r1 exist == u6r4 exist \/ u6r2 exist == u4r1 exist \/ % 0.92/1.11 u6r2 exist == u6r4 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u6r1 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u6r1 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u6r1 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r1 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r1 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.11 u6r4 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u6r1 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.11 u6r4 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u6r1 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.11 u6r4 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r1 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.11 u6r4 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r1 exist == u4r1 exist \/ u6r2 exist == u4r1 exist \/ d (u6r4 exist) % 0.92/1.11 |- u6r2 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u6r2 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u6r2 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r2 exist == u4r1 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.11 u6r3 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r2 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.11 u6r4 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u6r2 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.11 u6r4 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u6r2 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.11 u6r4 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r2 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.11 u6r4 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r1 exist == u4r1 exist \/ u6r1 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u4r1 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r2 exist == u4r1 exist \/ u6r2 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u4r1 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r3 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ c (u6r2 exist) % 0.92/1.11 |- u6r1 exist == u4r1 exist \/ u6r1 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u4r1 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r2 exist == u4r1 exist \/ u6r2 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u4r1 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r3 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ c (u6r1 exist) % 0.92/1.11 |- u6r1 exist == u4r1 exist \/ u6r1 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u4r1 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r2 exist == u4r1 exist \/ u6r2 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u4r1 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r1 exist == u4r1 exist \/ u6r1 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u4r1 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r2 exist == u4r1 exist \/ u6r2 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u4r1 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.11 |- u6r1 exist == u4r1 exist \/ u6r1 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u4r1 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.11 |- u6r1 exist == u4r1 exist \/ u6r1 exist == u6r3 exist \/ % 0.92/1.11 u6r3 exist == u4r1 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.11 |- u6r1 exist == u4r1 exist \/ u6r1 exist == u6r4 exist \/ % 0.92/1.11 u6r4 exist == u4r1 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.12 |- u6r1 exist == u4r1 exist \/ u6r1 exist == u6r4 exist \/ % 0.92/1.12 u6r4 exist == u4r1 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.12 |- u6r2 exist == u4r1 exist \/ u6r2 exist == u6r3 exist \/ % 0.92/1.12 u6r3 exist == u4r1 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.12 |- u6r2 exist == u4r1 exist \/ u6r2 exist == u6r3 exist \/ % 0.92/1.12 u6r3 exist == u4r1 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.12 |- u6r2 exist == u4r1 exist \/ u6r2 exist == u6r4 exist \/ % 0.92/1.12 u6r4 exist == u4r1 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.12 |- u6r2 exist == u4r1 exist \/ u6r2 exist == u6r4 exist \/ % 0.92/1.12 u6r4 exist == u4r1 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.12 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.12 u6r3 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.12 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.12 u6r3 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.12 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.12 u6r3 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.12 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.12 u6r3 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.12 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 u6r4 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.12 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 u6r4 exist == u6r1 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.12 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 u6r4 exist == u6r1 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.12 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 u6r4 exist == u6r1 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.12 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r2 exist \/ d (u6r4 exist) % 0.92/1.12 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.12 u6r3 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.12 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.12 u6r3 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.12 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.12 u6r3 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.12 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.12 u6r3 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.12 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 u6r4 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.12 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 u6r4 exist == u6r2 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.12 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 u6r4 exist == u6r2 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.12 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 u6r4 exist == u6r2 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.12 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.12 u6r1 exist == u6r3 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.12 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.12 u6r2 exist == u6r3 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.12 |- u4r1 exist == u6r3 exist \/ u4r1 exist == u6r4 exist \/ c (u6r2 exist) % 0.92/1.12 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.12 u6r1 exist == u6r3 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.12 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.12 u6r2 exist == u6r3 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.12 |- u4r1 exist == u6r3 exist \/ u4r1 exist == u6r4 exist \/ c (u6r1 exist) % 0.92/1.12 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 u6r1 exist == u6r4 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.12 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 u6r2 exist == u6r4 exist \/ c (u6r2 exist) \/ d (u6r4 exist) % 0.92/1.12 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 u6r1 exist == u6r4 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.12 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 u6r2 exist == u6r4 exist \/ c (u6r1 exist) \/ d (u6r4 exist) % 0.92/1.12 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.12 u6r1 exist == u6r3 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.12 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.12 u6r1 exist == u6r3 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.12 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 u6r1 exist == u6r4 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.12 |- u4r1 exist == u6r1 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 u6r1 exist == u6r4 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.12 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.12 u6r2 exist == u6r3 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.12 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r3 exist \/ % 0.92/1.12 u6r2 exist == u6r3 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.12 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 u6r2 exist == u6r4 exist \/ d (u6r4 exist) \/ r exist (u6r2 exist) % 0.92/1.12 |- u4r1 exist == u6r2 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 u6r2 exist == u6r4 exist \/ d (u6r4 exist) \/ r exist (u6r1 exist) % 0.92/1.12 |- u4r2 exist == u6r3 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.12 r exist (u6r2 exist) % 0.92/1.12 |- u4r2 exist == u6r3 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.12 r exist (u6r1 exist) % 0.92/1.12 |- u4r2 exist == u6r4 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.12 u6r3 exist == u6r4 exist \/ r exist (u6r2 exist) % 0.92/1.12 |- u4r2 exist == u6r4 exist \/ u6r3 exist == u4r2 exist \/ % 0.92/1.12 u6r3 exist == u6r4 exist \/ r exist (u6r1 exist) % 0.92/1.12 |- u4r2 exist == u6r3 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.12 r exist (u6r2 exist) % 0.92/1.12 |- u4r2 exist == u6r3 exist \/ u4r2 exist == u6r4 exist \/ % 0.92/1.12 r exist (u6r1 exist) % 0.92/1.12 |- u6r3 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.12 r exist (u6r2 exist) % 0.92/1.12 |- u6r3 exist == u4r2 exist \/ u6r4 exist == u4r2 exist \/ % 0.92/1.12 r exist (u6r1 exist) % 0.92/1.12 |- u4r1 exist == u6r3 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.12 r exist (u6r2 exist) % 0.92/1.12 |- u4r1 exist == u6r3 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.12 r exist (u6r1 exist) % 0.92/1.12 |- u4r1 exist == u6r4 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.12 u6r3 exist == u6r4 exist \/ r exist (u6r2 exist) % 0.92/1.12 |- u4r1 exist == u6r4 exist \/ u6r3 exist == u4r1 exist \/ % 0.92/1.12 u6r3 exist == u6r4 exist \/ r exist (u6r1 exist) % 0.92/1.12 |- u6r3 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.12 r exist (u6r2 exist) % 0.92/1.12 |- u6r3 exist == u4r1 exist \/ u6r4 exist == u4r1 exist \/ % 0.92/1.12 r exist (u6r1 exist) % 0.92/1.12 |- u4r1 exist == u6r3 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 r exist (u6r2 exist) % 0.92/1.12 |- u4r1 exist == u6r3 exist \/ u4r1 exist == u6r4 exist \/ % 0.92/1.12 r exist (u6r1 exist) % 0.92/1.12 |- ~r $_398 $_400 \/ ~r2most $_398 \/ $_400 == u6r1 $_398 \/ % 0.92/1.12 $_400 == u6r2 $_398 \/ u6r2 $_398 == u6r1 $_398 \/ d (u6r4 $_398) \/ % 0.92/1.12 f $_398 % 0.92/1.12 |- ~r $_398 $_399 \/ ~r2most $_398 \/ $_399 == u6r1 $_398 \/ % 0.92/1.12 u6r2 $_398 == $_399 \/ u6r2 $_398 == u6r1 $_398 \/ d (u6r4 $_398) \/ % 0.92/1.12 f $_398 % 0.92/1.12 |- ~r $_405 $_407 \/ ~r2most $_405 \/ $_407 == u6r1 $_405 \/ % 0.92/1.12 $_407 == u6r2 $_405 \/ u6r2 $_405 == u6r1 $_405 \/ d (u6r3 $_405) \/ % 0.92/1.12 f $_405 % 0.92/1.12 |- ~r $_405 $_406 \/ ~r2most $_405 \/ $_406 == u6r1 $_405 \/ % 0.92/1.12 u6r2 $_405 == $_406 \/ u6r2 $_405 == u6r1 $_405 \/ d (u6r3 $_405) \/ % 0.92/1.12 f $_405 % 0.92/1.12 |- ~r $_412 $_414 \/ ~r2most $_412 \/ $_414 == u6r1 $_412 \/ % 0.92/1.12 $_414 == u6r2 $_412 \/ u6r1 $_412 == u6r2 $_412 \/ d (u6r4 $_412) \/ % 0.92/1.12 f $_412 % 0.92/1.12 |- ~r $_412 $_413 \/ ~r2most $_412 \/ $_413 == u6r2 $_412 \/ % 0.92/1.12 u6r1 $_412 == $_413 \/ u6r1 $_412 == u6r2 $_412 \/ d (u6r4 $_412) \/ % 0.92/1.12 f $_412 % 0.92/1.12 |- ~r $_419 $_421 \/ ~r2most $_419 \/ $_421 == u6r1 $_419 \/ % 0.92/1.12 $_421 == u6r2 $_419 \/ u6r1 $_419 == u6r2 $_419 \/ d (u6r3 $_419) \/ % 0.92/1.12 f $_419 % 0.92/1.12 |- ~r $_419 $_420 \/ ~r2most $_419 \/ $_420 == u6r2 $_419 \/ % 0.92/1.12 u6r1 $_419 == $_420 \/ u6r1 $_419 == u6r2 $_419 \/ d (u6r3 $_419) \/ % 0.92/1.12 f $_419 % 0.92/1.12 |- ~r $_426 $_428 \/ ~r2most $_426 \/ $_428 == u6r3 $_426 \/ % 0.92/1.12 $_428 == u6r4 $_426 \/ u6r4 $_426 == u6r3 $_426 \/ c (u6r2 $_426) \/ % 0.92/1.12 f $_426 % 0.92/1.12 |- ~r $_426 $_427 \/ ~r2most $_426 \/ $_427 == u6r3 $_426 \/ % 0.92/1.12 u6r4 $_426 == $_427 \/ u6r4 $_426 == u6r3 $_426 \/ c (u6r2 $_426) \/ % 0.92/1.12 f $_426 % 0.92/1.12 |- ~r $_433 $_435 \/ ~r2most $_433 \/ $_435 == u6r3 $_433 \/ % 0.92/1.12 $_435 == u6r4 $_433 \/ u6r4 $_433 == u6r3 $_433 \/ c (u6r1 $_433) \/ % 0.92/1.12 f $_433 % 0.92/1.12 |- ~r $_433 $_434 \/ ~r2most $_433 \/ $_434 == u6r3 $_433 \/ % 0.92/1.12 u6r4 $_433 == $_434 \/ u6r4 $_433 == u6r3 $_433 \/ c (u6r1 $_433) \/ % 0.92/1.12 f $_433 % 0.92/1.12 |- ~r $_440 $_442 \/ ~r2most $_440 \/ $_442 == u6r3 $_440 \/ % 0.92/1.12 $_442 == u6r4 $_440 \/ u6r3 $_440 == u6r4 $_440 \/ c (u6r1 $_440) \/ % 0.92/1.12 f $_440 % 0.92/1.12 |- ~r $_440 $_441 \/ ~r2most $_440 \/ $_441 == u6r4 $_440 \/ % 0.92/1.12 u6r3 $_440 == $_441 \/ u6r3 $_440 == u6r4 $_440 \/ c (u6r1 $_440) \/ % 0.92/1.12 f $_440 % 0.92/1.12 |- ~r $_447 $_449 \/ ~r2most $_447 \/ $_449 == u6r3 $_447 \/ % 0.92/1.12 $_449 == u6r4 $_447 \/ u6r3 $_447 == u6r4 $_447 \/ c (u6r2 $_447) \/ % 0.92/1.12 f $_447 % 0.92/1.12 |- ~r $_447 $_448 \/ ~r2most $_447 \/ $_448 == u6r4 $_447 \/ % 0.92/1.12 u6r3 $_447 == $_448 \/ u6r3 $_447 == u6r4 $_447 \/ c (u6r2 $_447) \/ % 0.92/1.12 f $_447 % 0.92/1.12 |- ~r $_454 $_455 \/ ~r2most $_454 \/ u6r1 $_454 == $_455 \/ % 0.92/1.12 u6r2 $_454 == $_455 \/ u6r2 $_454 == u6r1 $_454 \/ d (u6r4 $_454) \/ % 0.92/1.12 f $_454 % 0.92/1.12 |- ~r $_459 $_460 \/ ~r2most $_459 \/ u6r1 $_459 == $_460 \/ % 0.92/1.12 u6r2 $_459 == $_460 \/ u6r2 $_459 == u6r1 $_459 \/ d (u6r3 $_459) \/ % 0.92/1.12 f $_459 % 0.92/1.12 |- ~r $_464 $_465 \/ ~r2most $_464 \/ u6r1 $_464 == $_465 \/ % 0.92/1.12 u6r1 $_464 == u6r2 $_464 \/ u6r2 $_464 == $_465 \/ d (u6r3 $_464) \/ % 0.92/1.12 f $_464 % 0.92/1.12 |- ~r $_469 $_470 \/ ~r2most $_469 \/ u6r1 $_469 == $_470 \/ % 0.92/1.12 u6r1 $_469 == u6r2 $_469 \/ u6r2 $_469 == $_470 \/ d (u6r4 $_469) \/ % 0.92/1.12 f $_469 % 0.92/1.12 |- ~r $_474 $_475 \/ ~r2most $_474 \/ u6r3 $_474 == $_475 \/ % 0.92/1.12 u6r4 $_474 == $_475 \/ u6r4 $_474 == u6r3 $_474 \/ c (u6r1 $_474) \/ % 0.92/1.12 f $_474 % 0.92/1.12 |- ~r $_479 $_480 \/ ~r2most $_479 \/ u6r3 $_479 == $_480 \/ % 0.92/1.12 u6r4 $_479 == $_480 \/ u6r4 $_479 == u6r3 $_479 \/ c (u6r2 $_479) \/ % 0.92/1.12 f $_479 % 0.92/1.12 |- ~r $_484 $_485 \/ ~r2most $_484 \/ u6r3 $_484 == $_485 \/ % 0.92/1.12 u6r3 $_484 == u6r4 $_484 \/ u6r4 $_484 == $_485 \/ c (u6r2 $_484) \/ % 0.92/1.12 f $_484 % 0.92/1.12 |- ~r $_489 $_490 \/ ~r2most $_489 \/ u6r3 $_489 == $_490 \/ % 0.92/1.12 u6r3 $_489 == u6r4 $_489 \/ u6r4 $_489 == $_490 \/ c (u6r1 $_489) \/ % 0.92/1.12 f $_489 % 0.92/1.12 |- ~r $_518 $_520 \/ ~r2most $_518 \/ $_520 == u6r3 $_518 \/ % 0.92/1.12 $_520 == u6r4 $_518 \/ u6r4 $_518 == u6r3 $_518 \/ f $_518 \/ % 0.92/1.12 r $_518 (u6r2 $_518) % 0.92/1.12 |- ~r $_518 $_519 \/ ~r2most $_518 \/ $_519 == u6r3 $_518 \/ % 0.92/1.12 u6r4 $_518 == $_519 \/ u6r4 $_518 == u6r3 $_518 \/ f $_518 \/ % 0.92/1.12 r $_518 (u6r2 $_518) % 0.92/1.12 |- ~r $_525 $_527 \/ ~r2most $_525 \/ $_527 == u6r3 $_525 \/ % 0.92/1.12 $_527 == u6r4 $_525 \/ u6r4 $_525 == u6r3 $_525 \/ f $_525 \/ % 0.92/1.12 r $_525 (u6r1 $_525) % 0.92/1.12 |- ~r $_525 $_526 \/ ~r2most $_525 \/ $_526 == u6r3 $_525 \/ % 0.92/1.12 u6r4 $_525 == $_526 \/ u6r4 $_525 == u6r3 $_525 \/ f $_525 \/ % 0.92/1.12 r $_525 (u6r1 $_525) % 0.92/1.12 |- ~r $_532 $_534 \/ ~r2most $_532 \/ $_534 == u6r3 $_532 \/ % 0.92/1.12 $_534 == u6r4 $_532 \/ u6r3 $_532 == u6r4 $_532 \/ f $_532 \/ % 0.92/1.12 r $_532 (u6r2 $_532) % 0.92/1.12 |- ~r $_532 $_533 \/ ~r2most $_532 \/ $_533 == u6r4 $_532 \/ % 0.92/1.12 u6r3 $_532 == $_533 \/ u6r3 $_532 == u6r4 $_532 \/ f $_532 \/ % 0.92/1.12 r $_532 (u6r2 $_532) % 0.92/1.12 |- ~r $_539 $_541 \/ ~r2most $_539 \/ $_541 == u6r3 $_539 \/ % 0.92/1.12 $_541 == u6r4 $_539 \/ u6r3 $_539 == u6r4 $_539 \/ f $_539 \/ % 0.92/1.12 r $_539 (u6r1 $_539) % 0.92/1.12 |- ~r $_539 $_540 \/ ~r2most $_539 \/ $_540 == u6r4 $_539 \/ % 0.92/1.12 u6r3 $_539 == $_540 \/ u6r3 $_539 == u6r4 $_539 \/ f $_539 \/ % 0.92/1.12 r $_539 (u6r1 $_539) % 0.92/1.12 |- ~r $_546 $_547 \/ ~r2most $_546 \/ u6r3 $_546 == $_547 \/ % 0.92/1.12 u6r4 $_546 == $_547 \/ u6r4 $_546 == u6r3 $_546 \/ f $_546 \/ % 0.92/1.12 r $_546 (u6r2 $_546) % 0.92/1.12 |- ~r $_551 $_552 \/ ~r2most $_551 \/ u6r3 $_551 == $_552 \/ % 0.92/1.12 u6r4 $_551 == $_552 \/ u6r4 $_551 == u6r3 $_551 \/ f $_551 \/ % 0.92/1.12 r $_551 (u6r1 $_551) % 0.92/1.12 |- ~r $_556 $_557 \/ ~r2most $_556 \/ u6r3 $_556 == $_557 \/ % 0.92/1.12 u6r3 $_556 == u6r4 $_556 \/ u6r4 $_556 == $_557 \/ f $_556 \/ % 0.92/1.12 r $_556 (u6r1 $_556) % 0.92/1.12 |- ~r $_561 $_562 \/ ~r2most $_561 \/ u6r3 $_561 == $_562 \/ % 0.92/1.12 u6r3 $_561 == u6r4 $_561 \/ u6r4 $_561 == $_562 \/ f $_561 \/ % 0.92/1.12 r $_561 (u6r2 $_561) % 0.92/1.12 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.92/1.12 %------------------------------------------------------------------------------