%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : SWV494-1.050 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n009.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 : 300s % DateTime : Tue Jun 25 02:15:45 EDT 2024 % Result : Unknown 0.39s 0.62s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SWV494-1.050 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.13 % Command : run_zenon_modulo %d %s % 0.13/0.34 % Computer : n009.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sat Jun 22 02:50:23 EDT 2024 % 0.13/0.34 % CPUTime : % 0.39/0.62 Zenon error: exhausted search space without finding a proof % 0.39/0.62 (* Current branch: % 0.39/0.62 ((i20) != (i44)) % 0.39/0.62 ((i25) != (i36)) % 0.39/0.62 ((i21) != (i35)) % 0.39/0.62 ((i4) != (i8)) % 0.39/0.62 ((i30) != (i31)) % 0.39/0.62 ((i33) != (i38)) % 0.39/0.62 ((i44) != (i45)) % 0.39/0.62 ((i30) != (i38)) % 0.39/0.62 ((i4) != (i10)) % 0.39/0.62 ((i33) != (i49)) % 0.39/0.62 ((i34) != (i43)) % 0.39/0.62 ((i5) != (i41)) % 0.39/0.62 ((i18) != (i25)) % 0.39/0.62 ((i34) != (i39)) % 0.39/0.62 ((i27) != (i29)) % 0.39/0.62 ((i40) != (i42)) % 0.39/0.62 ((i40) != (i46)) % 0.39/0.62 ((i23) != (i33)) % 0.39/0.62 ((i47) != (i48)) % 0.39/0.62 ((i2) != (i16)) % 0.39/0.62 ((i2) != (i7)) % 0.39/0.62 ((i9) != (i43)) % 0.39/0.62 ((i10) != (i28)) % 0.39/0.62 ((i16) != (i20)) % 0.39/0.62 ((i1) != (i39)) % 0.39/0.62 ((i10) != (i19)) % 0.39/0.62 ((i17) != (i30)) % 0.39/0.62 ((i1) != (i24)) % 0.39/0.62 ((i2) != (i23)) % 0.39/0.62 ((i3) != (i47)) % 0.39/0.62 ((i30) != (i48)) % 0.39/0.62 ((i4) != (i36)) % 0.39/0.62 ((i20) != (i49)) % 0.39/0.62 ((i17) != (i27)) % 0.39/0.62 ((i25) != (i47)) % 0.39/0.62 ((i1) != (i4)) % 0.39/0.62 ((i7) != (i20)) % 0.39/0.62 ((i6) != (i44)) % 0.39/0.62 ((i24) != (i27)) % 0.39/0.62 ((i31) != (i38)) % 0.39/0.62 ((i37) != (i48)) % 0.39/0.62 ((i39) != (i47)) % 0.39/0.62 ((i42) != (i46)) % 0.39/0.62 ((i5) != (i20)) % 0.39/0.62 ((i7) != (i32)) % 0.39/0.62 ((i12) != (i35)) % 0.39/0.62 ((i20) != (i24)) % 0.39/0.62 ((i18) != (i36)) % 0.39/0.62 ((i18) != (i38)) % 0.39/0.62 ((i17) != (i38)) % 0.39/0.62 ((i38) != (i48)) % 0.39/0.62 ((i12) != (i42)) % 0.39/0.62 ((i15) != (i34)) % 0.39/0.62 ((i12) != (i37)) % 0.39/0.62 ((i6) != (i19)) % 0.39/0.62 ((i25) != (i48)) % 0.39/0.62 ((i35) != (i39)) % 0.39/0.62 ((i33) != (i45)) % 0.39/0.62 ((i14) != (i31)) % 0.39/0.62 ((i14) != (i50)) % 0.39/0.62 ((i6) != (i9)) % 0.39/0.62 ((i12) != (i45)) % 0.39/0.62 ((i4) != (i28)) % 0.39/0.62 ((i16) != (i46)) % 0.39/0.62 ((i18) != (i24)) % 0.39/0.62 ((i45) != (i50)) % 0.39/0.62 ((i19) != (i36)) % 0.39/0.62 ((i8) != (i43)) % 0.39/0.62 ((i5) != (i32)) % 0.39/0.62 ((i9) != (i21)) % 0.39/0.62 ((i15) != (i25)) % 0.39/0.62 ((i17) != (i50)) % 0.39/0.62 ((i4) != (i34)) % 0.39/0.62 ((i44) != (i49)) % 0.39/0.62 ((i8) != (i29)) % 0.39/0.62 ((i6) != (i26)) % 0.39/0.62 ((i25) != (i44)) % 0.39/0.62 ((i4) != (i5)) % 0.39/0.62 ((i13) != (i26)) % 0.39/0.62 ((i5) != (i21)) % 0.39/0.62 ((i10) != (i15)) % 0.39/0.62 ((i39) != (i42)) % 0.39/0.62 ((i2) != (i42)) % 0.39/0.62 ((i14) != (i24)) % 0.39/0.62 ((i2) != (i24)) % 0.39/0.62 ((i8) != (i10)) % 0.39/0.62 ((i21) != (i30)) % 0.39/0.62 ((i3) != (i4)) % 0.39/0.62 ((i27) != (i48)) % 0.39/0.62 ((i36) != (i47)) % 0.39/0.62 ((i4) != (i46)) % 0.39/0.62 ((i29) != (i49)) % 0.39/0.62 ((i15) != (i24)) % 0.39/0.62 ((i6) != (i11)) % 0.39/0.62 ((i11) != (i49)) % 0.39/0.62 ((i4) != (i13)) % 0.39/0.62 ((i38) != (i40)) % 0.39/0.62 ((i13) != (i19)) % 0.39/0.62 ((i32) != (i37)) % 0.39/0.62 ((i10) != (i32)) % 0.39/0.62 ((i17) != (i42)) % 0.39/0.62 ((i10) != (i39)) % 0.39/0.62 ((i16) != (i24)) % 0.39/0.62 ((i21) != (i49)) % 0.39/0.62 ((i29) != (i46)) % 0.39/0.62 ((i36) != (i48)) % 0.39/0.62 ((i15) != (i36)) % 0.39/0.62 ((i17) != (i43)) % 0.39/0.62 ((i8) != (i35)) % 0.39/0.62 ((i15) != (i32)) % 0.39/0.62 ((i21) != (i43)) % 0.39/0.62 ((i23) != (i37)) % 0.39/0.62 ((i2) != (i9)) % 0.39/0.62 ((i3) != (i40)) % 0.39/0.62 ((i5) != (i27)) % 0.39/0.62 ((i7) != (i16)) % 0.39/0.62 ((i23) != (i26)) % 0.39/0.62 ((i6) != (i41)) % 0.39/0.62 ((i41) != (i44)) % 0.39/0.62 ((i24) != (i40)) % 0.39/0.62 ((i13) != (i22)) % 0.39/0.62 ((i2) != (i30)) % 0.39/0.62 ((i5) != (i15)) % 0.39/0.62 ((i9) != (i22)) % 0.39/0.62 ((i5) != (i48)) % 0.39/0.62 ((i36) != (i38)) % 0.39/0.62 ((i15) != (i48)) % 0.39/0.62 ((i27) != (i42)) % 0.39/0.62 ((i7) != (i15)) % 0.39/0.62 ((i26) != (i27)) % 0.39/0.62 ((i2) != (i4)) % 0.39/0.62 ((i4) != (i22)) % 0.39/0.62 ((i9) != (i10)) % 0.39/0.62 ((i4) != (i33)) % 0.39/0.62 ((i5) != (i26)) % 0.39/0.62 ((i14) != (i38)) % 0.39/0.62 ((i30) != (i50)) % 0.39/0.62 ((i6) != (i48)) % 0.39/0.62 ((i7) != (i22)) % 0.39/0.62 ((i16) != (i26)) % 0.39/0.62 ((i16) != (i33)) % 0.39/0.62 ((i20) != (i34)) % 0.39/0.62 ((i21) != (i31)) % 0.39/0.62 ((i29) != (i47)) % 0.39/0.62 ((i3) != (i10)) % 0.39/0.62 ((i1) != (i9)) % 0.39/0.62 ((i7) != (i19)) % 0.39/0.62 ((i7) != (i38)) % 0.39/0.62 ((i15) != (i19)) % 0.39/0.62 ((i26) != (i50)) % 0.39/0.62 ((i4) != (i27)) % 0.39/0.62 ((i37) != (i41)) % 0.39/0.62 ((i1) != (i41)) % 0.39/0.62 ((i3) != (i27)) % 0.39/0.62 ((i3) != (i50)) % 0.39/0.62 ((i14) != (i23)) % 0.39/0.62 ((i17) != (i23)) % 0.39/0.62 ((i28) != (i46)) % 0.39/0.62 ((i27) != (i47)) % 0.39/0.62 ((i19) != (i32)) % 0.39/0.62 ((i37) != (i39)) % 0.39/0.62 ((i6) != (i20)) % 0.39/0.62 ((i1) != (i6)) % 0.39/0.62 ((i4) != (i26)) % 0.39/0.62 ((i9) != (i44)) % 0.39/0.62 ((i11) != (i31)) % 0.39/0.62 ((i18) != (i41)) % 0.39/0.62 ((i30) != (i41)) % 0.39/0.62 ((i3) != (i17)) % 0.39/0.62 ((i2) != (i10)) % 0.39/0.62 ((i8) != (i34)) % 0.39/0.62 ((i4) != (i29)) % 0.39/0.62 ((i1) != (i35)) % 0.39/0.62 ((i13) != (i40)) % 0.39/0.62 ((i14) != (i45)) % 0.39/0.62 ((i23) != (i31)) % 0.39/0.62 ((i6) != (i29)) % 0.39/0.62 ((i21) != (i34)) % 0.39/0.62 ((i40) != (i43)) % 0.39/0.62 ((i36) != (i37)) % 0.39/0.62 ((i7) != (i45)) % 0.39/0.62 ((i13) != (i15)) % 0.39/0.62 ((i25) != (i41)) % 0.39/0.62 ((i47) != (i49)) % 0.39/0.62 ((i2) != (i28)) % 0.39/0.62 ((i23) != (i29)) % 0.39/0.62 ((i28) != (i34)) % 0.39/0.62 ((i37) != (i50)) % 0.39/0.62 ((i11) != (i35)) % 0.39/0.62 ((i1) != (i31)) % 0.39/0.62 ((i9) != (i41)) % 0.39/0.62 ((i28) != (i35)) % 0.39/0.62 ((i39) != (i49)) % 0.39/0.62 ((i1) != (i32)) % 0.39/0.62 ((i5) != (i7)) % 0.39/0.62 ((i4) != (i6)) % 0.39/0.62 ((i7) != (i13)) % 0.39/0.62 ((i15) != (i16)) % 0.39/0.62 ((i29) != (i41)) % 0.39/0.62 ((i20) != (i37)) % 0.39/0.62 ((i26) != (i37)) % 0.39/0.62 ((i2) != (i36)) % 0.39/0.62 ((i2) != (i20)) % 0.39/0.62 ((i25) != (i50)) % 0.39/0.62 ((i32) != (i35)) % 0.39/0.62 ((i8) != (i45)) % 0.39/0.62 ((i13) != (i41)) % 0.39/0.62 ((i22) != (i50)) % 0.39/0.62 ((i2) != (i6)) % 0.39/0.62 ((i7) != (i11)) % 0.39/0.62 ((i7) != (i42)) % 0.39/0.62 ((i2) != (i38)) % 0.39/0.62 ((i23) != (i41)) % 0.39/0.62 ((i13) != (i30)) % 0.39/0.62 ((i3) != (i6)) % 0.39/0.62 ((i6) != (i14)) % 0.39/0.62 ((i16) != (i34)) % 0.39/0.62 ((i46) != (i48)) % 0.39/0.62 ((i1) != (i46)) % 0.39/0.62 ((i6) != (i17)) % 0.39/0.62 ((i10) != (i37)) % 0.39/0.62 ((i10) != (i38)) % 0.39/0.62 ((i14) != (i17)) % 0.39/0.62 ((i3) != (i19)) % 0.39/0.62 ((i41) != (i48)) % 0.39/0.62 ((i5) != (i6)) % 0.39/0.62 ((i20) != (i45)) % 0.39/0.62 ((i9) != (i47)) % 0.39/0.62 ((i11) != (i17)) % 0.39/0.62 ((i21) != (i26)) % 0.39/0.62 ((i21) != (i38)) % 0.39/0.62 ((i35) != (i41)) % 0.39/0.62 ((i9) != (i17)) % 0.39/0.62 ((i14) != (i25)) % 0.39/0.62 ((i32) != (i43)) % 0.39/0.62 ((i43) != (i46)) % 0.39/0.62 ((i2) != (i8)) % 0.39/0.62 ((i9) != (i14)) % 0.39/0.62 ((i2) != (i50)) % 0.39/0.62 ((i35) != (i42)) % 0.39/0.62 ((i3) != (i36)) % 0.39/0.62 ((i12) != (i43)) % 0.39/0.62 ((i5) != (i25)) % 0.39/0.62 ((i8) != (i23)) % 0.39/0.62 ((i33) != (i34)) % 0.39/0.62 ((i3) != (i48)) % 0.39/0.62 ((i6) != (i37)) % 0.39/0.62 ((i18) != (i45)) % 0.39/0.62 ((i15) != (i47)) % 0.39/0.62 ((i4) != (i23)) % 0.39/0.62 ((i7) != (i47)) % 0.39/0.62 ((i11) != (i42)) % 0.39/0.62 ((i9) != (i46)) % 0.39/0.62 ((i14) != (i49)) % 0.39/0.62 ((i21) != (i50)) % 0.39/0.62 ((i27) != (i41)) % 0.39/0.62 ((i22) != (i42)) % 0.39/0.62 ((i1) != (i16)) % 0.39/0.62 ((i10) != (i11)) % 0.39/0.62 ((i2) != (i13)) % 0.39/0.62 ((i23) != (i25)) % 0.39/0.62 ((i23) != (i46)) % 0.39/0.62 ((i8) != (i12)) % 0.39/0.62 ((i12) != (i44)) % 0.39/0.62 ((i8) != (i41)) % 0.39/0.62 ((i19) != (i30)) % 0.39/0.62 ((i7) != (i44)) % 0.39/0.62 ((i9) != (i34)) % 0.39/0.62 ((i43) != (i44)) % 0.39/0.62 ((i22) != (i35)) % 0.39/0.62 ((i28) != (i31)) % 0.39/0.62 ((i19) != (i24)) % 0.39/0.62 ((i26) != (i35)) % 0.39/0.62 ((i18) != (i22)) % 0.39/0.62 ((i24) != (i36)) % 0.39/0.62 ((i4) != (i37)) % 0.39/0.62 ((i8) != (i44)) % 0.39/0.62 ((i27) != (i32)) % 0.39/0.62 ((i21) != (i33)) % 0.39/0.62 ((i6) != (i22)) % 0.39/0.62 ((i15) != (i23)) % 0.39/0.62 ((i4) != (i43)) % 0.39/0.62 ((i26) != (i47)) % 0.39/0.62 ((i26) != (i42)) % 0.39/0.62 ((i29) != (i36)) % 0.39/0.62 ((i43) != (i50)) % 0.39/0.62 ((i13) != (i18)) % 0.39/0.62 ((i3) != (i29)) % 0.39/0.62 ((i7) != (i18)) % 0.39/0.62 ((i21) != (i48)) % 0.39/0.62 ((i2) != (i22)) % 0.39/0.62 ((i5) != (i49)) % 0.39/0.62 ((i12) != (i28)) % 0.39/0.62 ((i8) != (i32)) % 0.39/0.62 ((i44) != (i50)) % 0.39/0.62 ((i2) != (i43)) % 0.39/0.62 ((i1) != (i43)) % 0.39/0.62 ((i8) != (i15)) % 0.39/0.62 ((i11) != (i34)) % 0.39/0.62 ((i1) != (i7)) % 0.39/0.62 ((i19) != (i50)) % 0.39/0.62 ((i10) != (i35)) % 0.39/0.62 ((i23) != (i24)) % 0.39/0.62 ((i10) != (i48)) % 0.39/0.62 ((i18) != (i34)) % 0.39/0.62 ((i21) != (i40)) % 0.39/0.62 ((i6) != (i47)) % 0.39/0.62 ((i1) != (i25)) % 0.39/0.62 ((i12) != (i40)) % 0.39/0.62 ((i20) != (i31)) % 0.39/0.62 ((i11) != (i47)) % 0.39/0.62 ((i22) != (i41)) % 0.39/0.62 ((i5) != (i37)) % 0.39/0.62 ((i4) != (i44)) % 0.39/0.62 ((i8) != (i31)) % 0.39/0.62 ((i10) != (i40)) % 0.39/0.62 ((i12) != (i15)) % 0.39/0.62 ((i31) != (i37)) % 0.39/0.62 ((i12) != (i19)) % 0.39/0.62 ((i5) != (i46)) % 0.39/0.62 ((i8) != (i21)) % 0.39/0.62 ((i9) != (i39)) % 0.39/0.62 ((i20) != (i28)) % 0.39/0.62 ((i24) != (i28)) % 0.39/0.62 ((i27) != (i37)) % 0.39/0.62 ((i8) != (i24)) % 0.39/0.62 ((i23) != (i43)) % 0.39/0.62 ((i7) != (i28)) % 0.39/0.62 ((i10) != (i14)) % 0.39/0.62 ((i25) != (i30)) % 0.39/0.62 ((i3) != (i28)) % 0.39/0.62 ((i6) != (i35)) % 0.39/0.62 ((i16) != (i19)) % 0.39/0.62 ((i9) != (i24)) % 0.39/0.62 ((i28) != (i47)) % 0.39/0.62 ((i5) != (i30)) % 0.39/0.62 ((i11) != (i20)) % 0.39/0.62 ((i25) != (i43)) % 0.39/0.62 ((i43) != (i45)) % 0.39/0.62 ((i4) != (i7)) % 0.39/0.62 ((i26) != (i39)) % 0.39/0.62 ((i24) != (i29)) % 0.39/0.62 ((i33) != (i46)) % 0.39/0.62 ((i15) != (i44)) % 0.39/0.62 ((i19) != (i27)) % 0.39/0.62 ((i28) != (i37)) % 0.39/0.62 ((i16) != (i29)) % 0.39/0.62 ((i20) != (i39)) % 0.39/0.62 ((i40) != (i44)) % 0.39/0.62 ((i14) != (i43)) % 0.39/0.62 ((i39) != (i41)) % 0.39/0.62 ((i28) != (i45)) % 0.39/0.62 ((i32) != (i38)) % 0.39/0.62 ((i5) != (i16)) % 0.39/0.62 ((i8) != (i26)) % 0.39/0.62 ((i8) != (i42)) % 0.39/0.62 ((i20) != (i23)) % 0.39/0.62 ((i8) != (i48)) % 0.39/0.62 ((i19) != (i33)) % 0.39/0.62 ((i4) != (i50)) % 0.39/0.62 ((i16) != (i43)) % 0.39/0.62 ((i18) != (i28)) % 0.39/0.62 ((i46) != (i50)) % 0.39/0.62 ((i20) != (i41)) % 0.39/0.62 ((i3) != (i5)) % 0.39/0.62 ((i9) != (i13)) % 0.39/0.62 ((i11) != (i22)) % 0.39/0.62 ((i2) != (i40)) % 0.39/0.62 ((i6) != (i42)) % 0.39/0.62 ((i20) != (i50)) % 0.39/0.62 ((i29) != (i34)) % 0.39/0.62 ((i12) != (i18)) % 0.39/0.62 ((i12) != (i36)) % 0.39/0.62 ((i13) != (i43)) % 0.39/0.62 ((i5) != (i11)) % 0.39/0.62 ((i40) != (i41)) % 0.39/0.62 ((i21) != (i41)) % 0.39/0.62 ((i22) != (i49)) % 0.39/0.62 ((i2) != (i45)) % 0.39/0.62 ((i12) != (i17)) % 0.39/0.62 ((i3) != (i45)) % 0.39/0.62 ((i11) != (i44)) % 0.39/0.62 ((i13) != (i46)) % 0.39/0.62 ((i19) != (i31)) % 0.39/0.62 ((i29) != (i32)) % 0.39/0.62 ((i1) != (i18)) % 0.39/0.62 ((i28) != (i39)) % 0.39/0.62 ((i38) != (i43)) % 0.39/0.62 ((i17) != (i34)) % 0.39/0.62 ((i3) != (i39)) % 0.39/0.62 ((i4) != (i40)) % 0.39/0.62 ((i12) != (i50)) % 0.39/0.62 ((i25) != (i28)) % 0.39/0.62 ((i3) != (i35)) % 0.39/0.62 ((i31) != (i50)) % 0.39/0.62 ((i9) != (i50)) % 0.39/0.62 ((i4) != (i12)) % 0.39/0.62 ((i14) != (i20)) % 0.39/0.62 ((i25) != (i34)) % 0.39/0.62 ((i1) != (i19)) % 0.39/0.62 ((i16) != (i48)) % 0.39/0.62 ((i45) != (i49)) % 0.39/0.62 ((i5) != (i14)) % 0.39/0.62 ((i6) != (i43)) % 0.39/0.62 ((i22) != (i27)) % 0.39/0.62 ((i6) != (i13)) % 0.39/0.62 ((i6) != (i23)) % 0.39/0.62 ((store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (a1) (i1) (e1)) (i2) (e2)) (i3) (e3)) (i4) (e4)) (i5) (e5)) (i6) (e6)) (i7) (e7)) (i8) (e8)) (i9) (e9)) (i10) (e10)) (i11) (e11)) (i12) (e12)) (i13) (e13)) (i14) (e14)) (i15) (e15)) (i16) (e16)) (i17) (e17)) (i18) (e18)) (i19) (e19)) (i20) (e20)) (i21) (e21)) (i22) (e22)) (i23) (e23)) (i24) (e24)) (i25) (e25)) (i26) (e26)) (i27) (e27)) (i28) (e28)) (i29) (e29)) (i30) (e30)) (i31) (e31)) (i32) (e32)) (i33) (e33)) (i34) (e34)) (i35) (e35)) (i36) (e36)) (i37) (e37)) (i38) (e38)) (i39) (e39)) (i40) (e40)) (i41) (e41)) (i42) (e42)) (i43) (e43)) (i44) (e44)) (i45) (e45)) (i46) (e46)) (i47) (e47)) (i48) (e48)) (i49) (e49)) (i1) (e1)) != (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (a1) (i41) (e41)) (i30) (e30)) (i45) (e45)) (i43) (e43)) (i28) (e28)) (i19) (e19)) (i22) (e22)) (i39) (e39)) (i20) (e20)) (i40) (e40)) (i16) (e16)) (i8) (e8)) (i49) (e49)) (i14) (e14)) (i13) (e13)) (i6) (e6)) (i27) (e27)) (i15) (e15)) (i7) (e7)) (i33) (e33)) (i9) (e9)) (i17) (e17)) (i42) (e42)) (i47) (e47)) (i18) (e18)) (i26) (e26)) (i34) (e34)) (i11) (e11)) (i36) (e36)) (i44) (e44)) (i38) (e38)) (i23) (e23)) (i25) (e25)) (i46) (e46)) (i35) (e35)) (i50) (e50)) (i2) (e2)) (i10) (e10)) (i48) (e48)) (i29) (e29)) (i3) (e3)) (i37) (e37)) (i12) (e12)) (i5) (e5)) (i32) (e32)) (i4) (e4)) (i24) (e24)) (i21) (e21)) (i31) (e31)) (i1) (e1))) % 0.39/0.62 ((i5) != (i39)) % 0.39/0.62 ((i6) != (i25)) % 0.39/0.62 ((i24) != (i37)) % 0.39/0.62 ((i16) != (i42)) % 0.39/0.62 ((i14) != (i30)) % 0.39/0.62 ((i23) != (i45)) % 0.39/0.62 ((i34) != (i40)) % 0.39/0.62 ((i35) != (i45)) % 0.39/0.62 ((i42) != (i45)) % 0.39/0.62 ((i24) != (i47)) % 0.39/0.62 ((i32) != (i33)) % 0.39/0.62 ((i11) != (i29)) % 0.39/0.62 ((i24) != (i49)) % 0.39/0.62 ((i31) != (i46)) % 0.39/0.62 ((i11) != (i30)) % 0.39/0.62 ((i16) != (i27)) % 0.39/0.62 ((i15) != (i31)) % 0.39/0.62 ((i27) != (i46)) % 0.39/0.62 ((i31) != (i33)) % 0.39/0.62 ((i15) != (i30)) % 0.39/0.62 ((i16) != (i25)) % 0.39/0.62 ((i21) != (i47)) % 0.39/0.62 ((i26) != (i40)) % 0.39/0.62 ((i29) != (i45)) % 0.39/0.62 ((i13) != (i20)) % 0.39/0.62 ((i25) != (i46)) % 0.39/0.62 ((i18) != (i30)) % 0.39/0.62 ((i19) != (i26)) % 0.39/0.62 ((i23) != (i27)) % 0.39/0.62 ((i7) != (i34)) % 0.39/0.62 ((i21) != (i46)) % 0.39/0.62 ((i22) != (i26)) % 0.39/0.62 ((i39) != (i48)) % 0.39/0.62 ((i27) != (i39)) % 0.39/0.62 ((i9) != (i31)) % 0.39/0.62 ((i6) != (i21)) % 0.39/0.62 ((i22) != (i31)) % 0.39/0.62 ((i26) != (i34)) % 0.39/0.62 ((i17) != (i45)) % 0.39/0.62 ((i35) != (i50)) % 0.39/0.62 ((i9) != (i26)) % 0.39/0.62 ((i18) != (i43)) % 0.39/0.62 ((i19) != (i29)) % 0.39/0.62 ((i43) != (i47)) % 0.39/0.62 ((i31) != (i36)) % 0.39/0.62 ((i34) != (i42)) % 0.39/0.62 ((i8) != (i22)) % 0.39/0.62 ((i13) != (i29)) % 0.39/0.62 ((i19) != (i49)) % 0.39/0.62 ((i32) != (i44)) % 0.39/0.62 ((i25) != (i42)) % 0.39/0.62 ((i1) != (i14)) % 0.39/0.62 ((i24) != (i26)) % 0.39/0.62 ((i16) != (i32)) % 0.39/0.62 ((i19) != (i23)) % 0.39/0.62 ((i38) != (i44)) % 0.39/0.62 ((i5) != (i42)) % 0.39/0.62 ((i5) != (i44)) % 0.39/0.62 ((i8) != (i50)) % 0.39/0.62 ((i18) != (i40)) % 0.39/0.62 ((i6) != (i49)) % 0.39/0.62 ((i1) != (i33)) % 0.39/0.62 ((i7) != (i23)) % 0.39/0.62 ((i22) != (i25)) % 0.39/0.62 ((i29) != (i30)) % 0.39/0.62 ((i30) != (i36)) % 0.39/0.62 ((i32) != (i49)) % 0.39/0.62 ((i28) != (i33)) % 0.39/0.62 ((i1) != (i29)) % 0.39/0.62 ((i11) != (i46)) % 0.39/0.62 ((i6) != (i7)) % 0.39/0.62 ((i11) != (i26)) % 0.39/0.62 ((i10) != (i20)) % 0.39/0.62 ((i9) != (i49)) % 0.39/0.62 ((i41) != (i45)) % 0.39/0.62 ((i17) != (i19)) % 0.39/0.62 ((i23) != (i28)) % 0.39/0.62 ((i23) != (i42)) % 0.39/0.62 ((i8) != (i33)) % 0.39/0.62 ((i8) != (i19)) % 0.39/0.62 ((i10) != (i13)) % 0.39/0.62 ((i18) != (i26)) % 0.39/0.62 ((i4) != (i38)) % 0.39/0.62 ((i20) != (i25)) % 0.39/0.62 ((i7) != (i50)) % 0.39/0.62 ((i16) != (i47)) % 0.39/0.62 ((i32) != (i48)) % 0.39/0.62 ((i4) != (i42)) % 0.39/0.62 ((i22) != (i30)) % 0.39/0.62 ((i31) != (i34)) % 0.39/0.62 ((i9) != (i40)) % 0.39/0.62 ((i16) != (i21)) % 0.39/0.62 ((i31) != (i49)) % 0.39/0.62 ((i15) != (i50)) % 0.39/0.62 ((i26) != (i43)) % 0.39/0.62 ((i20) != (i47)) % 0.39/0.62 ((i26) != (i41)) % 0.39/0.62 ((i30) != (i34)) % 0.39/0.62 ((i32) != (i40)) % 0.39/0.62 ((i24) != (i46)) % 0.39/0.62 ((i10) != (i44)) % 0.39/0.62 ((i25) != (i32)) % 0.39/0.62 ((i10) != (i26)) % 0.39/0.62 ((i2) != (i5)) % 0.39/0.62 ((i17) != (i47)) % 0.39/0.62 ((i4) != (i35)) % 0.39/0.62 ((i5) != (i28)) % 0.39/0.62 ((i17) != (i31)) % 0.39/0.62 ((i5) != (i47)) % 0.39/0.62 ((i17) != (i25)) % 0.39/0.62 ((i4) != (i49)) % 0.39/0.62 ((i7) != (i39)) % 0.39/0.62 ((i18) != (i20)) % 0.39/0.62 ((i1) != (i20)) % 0.39/0.62 ((i14) != (i48)) % 0.39/0.62 ((i23) != (i38)) % 0.39/0.62 ((i37) != (i38)) % 0.39/0.62 ((i29) != (i38)) % 0.39/0.62 ((i44) != (i48)) % 0.39/0.62 ((i31) != (i35)) % 0.39/0.62 ((i3) != (i22)) % 0.39/0.62 ((i18) != (i35)) % 0.39/0.62 ((i27) != (i43)) % 0.39/0.62 ((i9) != (i45)) % 0.39/0.62 ((i47) != (i50)) % 0.39/0.62 ((i5) != (i19)) % 0.39/0.62 ((i42) != (i43)) % 0.39/0.62 ((i10) != (i41)) % 0.39/0.62 ((i8) != (i11)) % 0.39/0.62 ((select (store zenon_X0 zenon_X2 zenon_X1) zenon_X3) = (select zenon_X0 zenon_X3)) % 0.39/0.62 ((i1) != (i50)) % 0.39/0.62 ((i6) != (i10)) % 0.39/0.62 ((i19) != (i25)) % 0.39/0.62 ((i45) != (i46)) % 0.39/0.62 ((i33) != (i41)) % 0.39/0.62 ((i4) != (i41)) % 0.39/0.62 ((i3) != (i33)) % 0.39/0.62 ((i25) != (i33)) % 0.39/0.62 ((i2) != (i37)) % 0.39/0.62 ((i18) != (i42)) % 0.39/0.62 ((i5) != (i22)) % 0.39/0.62 ((i34) != (i50)) % 0.39/0.62 ((i10) != (i42)) % 0.39/0.62 ((i48) != (i50)) % 0.39/0.62 ((i10) != (i25)) % 0.39/0.62 ((i37) != (i49)) % 0.39/0.62 ((i2) != (i44)) % 0.39/0.62 ((i7) != (i21)) % 0.39/0.62 ((i3) != (i34)) % 0.39/0.62 ((i14) != (i40)) % 0.39/0.62 ((i8) != (i17)) % 0.39/0.62 ((i2) != (i18)) % 0.39/0.62 ((i5) != (i17)) % 0.39/0.62 ((i1) != (i17)) % 0.39/0.62 ((i2) != (i46)) % 0.39/0.62 ((i21) != (i39)) % 0.39/0.62 ((i4) != (i21)) % 0.39/0.62 ((i10) != (i31)) % 0.39/0.62 ((i11) != (i43)) % 0.39/0.62 ((i12) != (i16)) % 0.39/0.62 ((i13) != (i48)) % 0.39/0.62 ((i14) != (i35)) % 0.39/0.62 ((i20) != (i48)) % 0.39/0.62 ((i35) != (i48)) % 0.39/0.62 ((i21) != (i29)) % 0.39/0.62 ((i23) != (i49)) % 0.39/0.62 ((i44) != (i46)) % 0.39/0.62 ((i6) != (i30)) % 0.39/0.62 ((i5) != (i13)) % 0.39/0.62 ((i37) != (i47)) % 0.39/0.62 ((i4) != (i24)) % 0.39/0.62 ((i9) != (i42)) % 0.39/0.62 ((i3) != (i16)) % 0.39/0.62 ((i5) != (i50)) % 0.39/0.62 ((i8) != (i14)) % 0.39/0.62 ((i7) != (i12)) % 0.39/0.62 ((i19) != (i45)) % 0.39/0.62 ((i49) != (i50)) % 0.39/0.62 ((i11) != (i32)) % 0.39/0.62 ((i9) != (i32)) % 0.39/0.62 ((i21) != (i32)) % 0.39/0.62 ((i28) != (i41)) % 0.39/0.62 ((i30) != (i49)) % 0.39/0.62 ((i1) != (i44)) % 0.39/0.62 ((i11) != (i45)) % 0.39/0.62 ((i18) != (i37)) % 0.39/0.62 ((i27) != (i45)) % 0.39/0.62 ((i19) != (i46)) % 0.39/0.62 ((i10) != (i36)) % 0.39/0.62 ((i13) != (i28)) % 0.39/0.62 ((i31) != (i48)) % 0.39/0.62 ((i37) != (i42)) % 0.39/0.62 ((i9) != (i48)) % 0.39/0.62 ((i7) != (i14)) % 0.39/0.62 ((i22) != (i46)) % 0.39/0.62 ((i8) != (i37)) % 0.39/0.62 ((i1) != (i2)) % 0.39/0.62 ((i9) != (i19)) % 0.39/0.62 ((i13) != (i49)) % 0.39/0.62 ((i17) != (i49)) % 0.39/0.62 ((i25) != (i31)) % 0.39/0.62 ((i25) != (i35)) % 0.39/0.62 ((i29) != (i40)) % 0.39/0.62 ((i34) != (i45)) % 0.39/0.62 ((i32) != (i42)) % 0.39/0.62 ((i16) != (i50)) % 0.39/0.62 ((i27) != (i44)) % 0.39/0.62 ((i33) != (i42)) % 0.39/0.62 ((i17) != (i33)) % 0.39/0.62 ((i19) != (i35)) % 0.39/0.62 ((i33) != (i40)) % 0.39/0.62 ((i2) != (i19)) % 0.39/0.62 ((i1) != (i28)) % 0.39/0.62 ((i15) != (i27)) % 0.39/0.62 ((i31) != (i45)) % 0.39/0.62 ((i14) != (i46)) % 0.39/0.62 ((i16) != (i28)) % 0.39/0.62 ((i30) != (i44)) % 0.39/0.62 ((i28) != (i38)) % 0.39/0.62 ((i16) != (i36)) % 0.39/0.62 ((i19) != (i21)) % 0.39/0.62 ((i12) != (i38)) % 0.39/0.62 ((i10) != (i27)) % 0.39/0.62 ((i13) != (i35)) % 0.39/0.62 ((i4) != (i30)) % 0.39/0.62 ((i7) != (i35)) % 0.39/0.62 ((i9) != (i33)) % 0.39/0.62 ((i17) != (i22)) % 0.39/0.62 ((i6) != (i50)) % 0.39/0.62 ((i30) != (i45)) % 0.39/0.62 ((i8) != (i13)) % 0.39/0.62 ((i20) != (i43)) % 0.39/0.62 ((i1) != (i21)) % 0.39/0.62 ((i7) != (i37)) % 0.39/0.62 ((i28) != (i29)) % 0.39/0.62 ((i35) != (i36)) % 0.39/0.62 ((i16) != (i39)) % 0.39/0.62 ((i17) != (i26)) % 0.39/0.62 ((i4) != (i48)) % 0.39/0.62 ((i34) != (i35)) % 0.39/0.62 ((store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (a1) (i1) (e1)) (i2) (e2)) (i3) (e3)) (i4) (e4)) (i5) (e5)) (i6) (e6)) (i7) (e7)) (i8) (e8)) (i9) (e9)) (i10) (e10)) (i11) (e11)) (i12) (e12)) (i13) (e13)) (i14) (e14)) (i15) (e15)) (i16) (e16)) (i17) (e17)) (i18) (e18)) (i19) (e19)) (i20) (e20)) (i21) (e21)) (i22) (e22)) (i23) (e23)) (i24) (e24)) (i25) (e25)) (i26) (e26)) (i27) (e27)) (i28) (e28)) (i29) (e29)) (i30) (e30)) (i31) (e31)) (i32) (e32)) (i33) (e33)) (i34) (e34)) (i35) (e35)) (i36) (e36)) (i37) (e37)) (i38) (e38)) (i39) (e39)) (i40) (e40)) (i41) (e41)) (i42) (e42)) (i43) (e43)) (i44) (e44)) (i45) (e45)) (i46) (e46)) (i47) (e47)) (i48) (e48)) (i49) (e49)) != (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (a1) (i41) (e41)) (i30) (e30)) (i45) (e45)) (i43) (e43)) (i28) (e28)) (i19) (e19)) (i22) (e22)) (i39) (e39)) (i20) (e20)) (i40) (e40)) (i16) (e16)) (i8) (e8)) (i49) (e49)) (i14) (e14)) (i13) (e13)) (i6) (e6)) (i27) (e27)) (i15) (e15)) (i7) (e7)) (i33) (e33)) (i9) (e9)) (i17) (e17)) (i42) (e42)) (i47) (e47)) (i18) (e18)) (i26) (e26)) (i34) (e34)) (i11) (e11)) (i36) (e36)) (i44) (e44)) (i38) (e38)) (i23) (e23)) (i25) (e25)) (i46) (e46)) (i35) (e35)) (i50) (e50)) (i2) (e2)) (i10) (e10)) (i48) (e48)) (i29) (e29)) (i3) (e3)) (i37) (e37)) (i12) (e12)) (i5) (e5)) (i32) (e32)) (i4) (e4)) (i24) (e24)) (i21) (e21)) (i31) (e31))) % 0.39/0.62 ((i4) != (i16)) % 0.39/0.62 ((i10) != (i23)) % 0.39/0.62 ((i18) != (i49)) % 0.39/0.62 ((i29) != (i33)) % 0.39/0.62 ((i1) != (i38)) % 0.39/0.62 ((i13) != (i42)) % 0.39/0.62 ((i24) != (i32)) % 0.39/0.62 ((i25) != (i40)) % 0.39/0.62 ((i26) != (i32)) % 0.39/0.62 ((i2) != (i34)) % 0.39/0.62 ((i31) != (i32)) % 0.39/0.62 ((i5) != (i24)) % 0.39/0.62 ((i43) != (i49)) % 0.39/0.62 ((i27) != (i28)) % 0.39/0.62 ((i29) != (i31)) % 0.39/0.62 ((i12) != (i20)) % 0.39/0.62 ((i6) != (i18)) % 0.39/0.62 ((i2) != (i15)) % 0.39/0.62 ((i3) != (i12)) % 0.39/0.62 ((i20) != (i32)) % 0.39/0.62 ((i9) != (i12)) % 0.39/0.62 ((i12) != (i26)) % 0.39/0.62 ((i15) != (i22)) % 0.39/0.62 ((i22) != (i39)) % 0.39/0.62 ((i24) != (i38)) % 0.39/0.62 ((i25) != (i29)) % 0.39/0.62 ((i29) != (i43)) % 0.39/0.62 ((i17) != (i46)) % 0.39/0.62 ((i21) != (i23)) % 0.39/0.62 ((i10) != (i16)) % 0.39/0.62 ((i14) != (i18)) % 0.39/0.62 ((i1) != (i45)) % 0.39/0.62 ((i6) != (i32)) % 0.39/0.62 ((i26) != (i38)) % 0.39/0.62 ((i18) != (i27)) % 0.39/0.62 ((i8) != (i20)) % 0.39/0.62 ((i12) != (i29)) % 0.39/0.62 ((i39) != (i45)) % 0.39/0.62 ((i20) != (i30)) % 0.39/0.62 ((i27) != (i36)) % 0.39/0.62 ((i17) != (i36)) % 0.39/0.62 ((i33) != (i44)) % 0.39/0.62 ((i7) != (i48)) % 0.39/0.62 ((i33) != (i47)) % 0.39/0.62 ((i35) != (i49)) % 0.39/0.62 ((i14) != (i32)) % 0.39/0.62 ((i1) != (i49)) % 0.39/0.62 ((i2) != (i21)) % 0.39/0.62 ((i20) != (i33)) % 0.39/0.62 ((i4) != (i39)) % 0.39/0.62 ((i11) != (i41)) % 0.39/0.62 ((i17) != (i35)) % 0.39/0.62 ((i27) != (i34)) % 0.39/0.62 ((i13) != (i45)) % 0.39/0.62 ((i15) != (i45)) % 0.39/0.62 ((i23) != (i50)) % 0.39/0.62 ((i6) != (i31)) % 0.39/0.62 ((i10) != (i12)) % 0.39/0.62 ((i21) != (i45)) % 0.39/0.62 ((i36) != (i50)) % 0.39/0.62 ((i8) != (i38)) % 0.39/0.62 ((i1) != (i27)) % 0.39/0.62 ((i27) != (i35)) % 0.39/0.62 ((i9) != (i18)) % 0.39/0.62 ((i5) != (i43)) % 0.39/0.62 ((i14) != (i21)) % 0.39/0.62 ((i25) != (i45)) % 0.39/0.62 ((i10) != (i45)) % 0.39/0.62 ((i13) != (i34)) % 0.39/0.62 ((i3) != (i31)) % 0.39/0.62 ((i32) != (i41)) % 0.39/0.62 ((i32) != (i50)) % 0.39/0.62 ((i3) != (i26)) % 0.39/0.62 ((i2) != (i33)) % 0.39/0.62 ((i3) != (i44)) % 0.39/0.62 ((i41) != (i47)) % 0.39/0.62 ((i1) != (i23)) % 0.39/0.62 ((i10) != (i17)) % 0.39/0.62 ((i3) != (i43)) % 0.39/0.62 ((i28) != (i40)) % 0.39/0.62 ((i30) != (i42)) % 0.39/0.62 ((i24) != (i42)) % 0.39/0.62 ((i37) != (i40)) % 0.39/0.62 ((i37) != (i43)) % 0.39/0.62 ((i2) != (i17)) % 0.39/0.62 ((i40) != (i49)) % 0.39/0.62 ((i31) != (i41)) % 0.39/0.62 ((i2) != (i41)) % 0.39/0.62 ((i9) != (i36)) % 0.39/0.62 ((i12) != (i24)) % 0.39/0.62 ((i7) != (i24)) % 0.39/0.62 ((i11) != (i24)) % 0.39/0.62 ((i26) != (i28)) % 0.39/0.62 ((i38) != (i39)) % 0.39/0.62 ((i41) != (i50)) % 0.39/0.62 ((i31) != (i39)) % 0.39/0.62 ((i15) != (i46)) % 0.39/0.62 ((i23) != (i32)) % 0.39/0.62 ((i38) != (i47)) % 0.39/0.62 ((i25) != (i39)) % 0.39/0.62 ((i30) != (i32)) % 0.39/0.62 ((i1) != (i12)) % 0.39/0.62 ((i4) != (i31)) % 0.39/0.62 ((i12) != (i32)) % 0.39/0.62 ((i36) != (i42)) % 0.39/0.62 ((i3) != (i46)) % 0.39/0.62 ((i36) != (i43)) % 0.39/0.62 ((i24) != (i34)) % 0.39/0.62 ((i7) != (i43)) % 0.39/0.62 ((i38) != (i45)) % 0.39/0.62 ((i4) != (i19)) % 0.39/0.62 ((i6) != (i16)) % 0.39/0.62 ((i14) != (i16)) % 0.39/0.62 ((i7) != (i9)) % 0.39/0.62 ((i4) != (i17)) % 0.39/0.62 ((i7) != (i41)) % 0.39/0.62 ((i10) != (i49)) % 0.39/0.62 ((i19) != (i48)) % 0.39/0.62 ((i22) != (i40)) % 0.39/0.62 ((i30) != (i40)) % 0.39/0.62 ((i12) != (i46)) % 0.39/0.62 ((i6) != (i12)) % 0.39/0.62 ((i5) != (i18)) % 0.39/0.62 ((i2) != (i27)) % 0.39/0.62 ((i23) != (i40)) % 0.39/0.62 ((i32) != (i47)) % 0.39/0.62 ((i8) != (i28)) % 0.39/0.62 ((i10) != (i33)) % 0.39/0.62 ((i8) != (i9)) % 0.39/0.62 ((i2) != (i3)) % 0.39/0.62 ((i28) != (i49)) % 0.39/0.62 ((i13) != (i47)) % 0.39/0.62 ((i21) != (i27)) % 0.39/0.62 ((i25) != (i37)) % 0.39/0.62 ((i21) != (i25)) % 0.39/0.62 ((i4) != (i45)) % 0.39/0.62 ((i6) != (i39)) % 0.39/0.62 ((i19) != (i39)) % 0.39/0.62 ((i35) != (i43)) % 0.39/0.62 ((i6) != (i8)) % 0.39/0.62 ((i13) != (i23)) % 0.39/0.62 ((i14) != (i41)) % 0.39/0.62 ((i3) != (i42)) % 0.39/0.62 ((i19) != (i47)) % 0.39/0.62 ((i13) != (i33)) % 0.39/0.62 ((i17) != (i24)) % 0.39/0.62 ((i46) != (i47)) % 0.39/0.62 ((i12) != (i13)) % 0.39/0.62 ((i3) != (i23)) % 0.39/0.62 ((i2) != (i35)) % 0.39/0.62 ((i29) != (i42)) % 0.39/0.62 ((i21) != (i42)) % 0.39/0.62 ((i12) != (i14)) % 0.39/0.62 ((i24) != (i35)) % 0.39/0.62 ((i35) != (i40)) % 0.39/0.62 ((i10) != (i18)) % 0.39/0.62 ((i5) != (i23)) % 0.39/0.62 ((i26) != (i44)) % 0.39/0.62 ((i34) != (i37)) % 0.39/0.62 ((i4) != (i25)) % 0.39/0.62 ((i5) != (i31)) % 0.39/0.62 ((i11) != (i16)) % 0.39/0.62 ((i13) != (i37)) % 0.39/0.62 ((i3) != (i14)) % 0.39/0.62 ((i3) != (i18)) % 0.39/0.62 ((i7) != (i29)) % 0.39/0.62 ((i9) != (i16)) % 0.39/0.62 ((i15) != (i43)) % 0.39/0.62 ((i41) != (i46)) % 0.39/0.62 ((i12) != (i41)) % 0.39/0.62 ((i13) != (i24)) % 0.39/0.62 ((i32) != (i34)) % 0.39/0.62 ((i16) != (i35)) % 0.39/0.62 ((i7) != (i33)) % 0.39/0.62 ((i10) != (i30)) % 0.39/0.62 ((i9) != (i29)) % 0.39/0.62 ((i16) != (i23)) % 0.39/0.62 ((i38) != (i41)) % 0.39/0.62 ((i43) != (i48)) % 0.39/0.62 ((i30) != (i37)) % 0.39/0.62 ((i9) != (i25)) % 0.39/0.62 ((i10) != (i46)) % 0.39/0.62 ((i12) != (i25)) % 0.39/0.62 ((i33) != (i50)) % 0.39/0.62 ((i5) != (i9)) % 0.39/0.62 ((i8) != (i16)) % 0.39/0.62 ((i24) != (i44)) % 0.39/0.62 ((i34) != (i41)) % 0.39/0.62 ((i15) != (i37)) % 0.39/0.62 ((i4) != (i11)) % 0.39/0.62 ((i11) != (i37)) % 0.39/0.62 ((i35) != (i47)) % 0.39/0.62 ((i11) != (i27)) % 0.39/0.62 ((i17) != (i41)) % 0.39/0.62 ((i13) != (i39)) % 0.39/0.62 ((i22) != (i43)) % 0.39/0.62 ((i22) != (i47)) % 0.39/0.62 ((i27) != (i40)) % 0.39/0.62 ((i28) != (i30)) % 0.39/0.62 ((i14) != (i36)) % 0.39/0.62 ((i20) != (i29)) % 0.39/0.62 ((i20) != (i35)) % 0.39/0.62 ((i1) != (i5)) % 0.39/0.62 ((i2) != (i14)) % 0.39/0.62 ((i6) != (i34)) % 0.39/0.62 ((i37) != (i46)) % 0.39/0.62 ((i23) != (i35)) % 0.39/0.62 ((i7) != (i26)) % 0.39/0.62 ((i23) != (i47)) % 0.39/0.62 ((i15) != (i33)) % 0.39/0.62 ((i30) != (i47)) % 0.39/0.62 ((i36) != (i49)) % 0.39/0.62 ((i1) != (i36)) % 0.39/0.62 ((i17) != (i21)) % 0.39/0.62 ((i19) != (i42)) % 0.39/0.62 ((i22) != (i38)) % 0.39/0.62 ((i8) != (i36)) % 0.39/0.62 ((i14) != (i42)) % 0.39/0.62 ((i1) != (i11)) % 0.39/0.62 ((i4) != (i15)) % 0.39/0.62 ((i28) != (i44)) % 0.39/0.62 ((i1) != (i37)) % 0.39/0.62 ((i4) != (i9)) % 0.39/0.62 ((i14) != (i37)) % 0.39/0.62 ((i28) != (i32)) % 0.39/0.62 ((i45) != (i48)) % 0.39/0.62 ((i18) != (i32)) % 0.39/0.62 ((i29) != (i37)) % 0.39/0.62 ((i5) != (i40)) % 0.39/0.62 ((i13) != (i36)) % 0.39/0.62 ((i25) != (i27)) % 0.39/0.62 ((i29) != (i44)) % 0.39/0.62 ((i13) != (i25)) % 0.39/0.62 ((i14) != (i44)) % 0.39/0.62 ((i34) != (i49)) % 0.39/0.62 ((i42) != (i48)) % 0.39/0.62 ((i19) != (i34)) % 0.39/0.62 ((i7) != (i30)) % 0.39/0.62 ((i21) != (i37)) % 0.39/0.62 ((i28) != (i43)) % 0.39/0.62 ((i1) != (i34)) % 0.39/0.62 ((i2) != (i26)) % 0.39/0.62 ((i16) != (i30)) % 0.39/0.62 ((i20) != (i27)) % 0.39/0.62 ((i6) != (i15)) % 0.39/0.62 ((i5) != (i8)) % 0.39/0.62 ((i14) != (i28)) % 0.39/0.62 ((i3) != (i30)) % 0.39/0.62 ((i35) != (i46)) % 0.39/0.62 ((i16) != (i18)) % 0.39/0.62 ((i30) != (i43)) % 0.39/0.62 ((i3) != (i15)) % 0.39/0.62 ((i15) != (i20)) % 0.39/0.62 ((i11) != (i13)) % 0.39/0.62 ((i11) != (i15)) % 0.39/0.62 ((i15) != (i49)) % 0.39/0.62 ((i36) != (i44)) % 0.39/0.62 ((i1) != (i8)) % 0.39/0.62 ((i24) != (i45)) % 0.39/0.62 ((i16) != (i45)) % 0.39/0.62 ((i19) != (i43)) % 0.39/0.62 ((i6) != (i46)) % 0.39/0.62 ((i11) != (i33)) % 0.39/0.62 ((i1) != (i3)) % 0.39/0.62 ((i17) != (i40)) % 0.39/0.62 ((i12) != (i30)) % 0.39/0.62 ((i22) != (i37)) % 0.39/0.62 ((i7) != (i46)) % 0.39/0.62 ((i35) != (i37)) % 0.39/0.62 ((i4) != (i14)) % 0.39/0.62 ((i20) != (i36)) % 0.39/0.62 ((i14) != (i22)) % 0.39/0.62 ((i22) != (i28)) % 0.39/0.62 ((i21) != (i44)) % 0.39/0.62 ((i1) != (i40)) % 0.39/0.62 ((i23) != (i30)) % 0.39/0.62 ((i37) != (i45)) % 0.39/0.62 ((i38) != (i42)) % 0.39/0.62 ((i3) != (i9)) % 0.39/0.62 ((i34) != (i36)) % 0.39/0.62 ((i8) != (i47)) % 0.39/0.62 ((i15) != (i42)) % 0.39/0.62 ((i14) != (i19)) % 0.39/0.62 ((i9) != (i23)) % 0.39/0.62 ((i1) != (i30)) % 0.39/0.62 ((i3) != (i32)) % 0.39/0.62 ((i7) != (i27)) % 0.39/0.62 ((i18) != (i50)) % 0.39/0.62 ((i40) != (i48)) % 0.39/0.62 ((i6) != (i33)) % 0.39/0.62 ((i33) != (i48)) % 0.39/0.62 ((i41) != (i42)) % 0.39/0.62 ((i5) != (i12)) % 0.39/0.62 ((i9) != (i38)) % 0.39/0.62 ((i12) != (i33)) % 0.39/0.62 ((i11) != (i21)) % 0.39/0.62 ((i16) != (i31)) % 0.39/0.62 ((i48) != (i49)) % 0.39/0.62 ((i21) != (i36)) % 0.39/0.62 ((i24) != (i31)) % 0.39/0.62 ((i10) != (i22)) % 0.39/0.62 ((i16) != (i49)) % 0.39/0.62 ((i6) != (i45)) % 0.39/0.62 ((i27) != (i50)) % 0.39/0.62 ((i42) != (i47)) % 0.39/0.62 ((i2) != (i12)) % 0.39/0.62 ((i6) != (i28)) % 0.39/0.62 ((i6) != (i38)) % 0.39/0.62 ((i22) != (i45)) % 0.39/0.62 ((i16) != (i22)) % 0.39/0.62 ((i22) != (i23)) % 0.39/0.62 ((i7) != (i31)) % 0.39/0.62 ((i46) != (i49)) % 0.39/0.62 ((i23) != (i44)) % 0.39/0.62 ((i41) != (i49)) % 0.39/0.62 ((i4) != (i20)) % 0.39/0.62 ((i10) != (i43)) % 0.39/0.62 ((i22) != (i34)) % 0.39/0.62 ((i33) != (i39)) % 0.39/0.62 ((i13) != (i21)) % 0.39/0.62 ((i26) != (i30)) % 0.39/0.62 ((i18) != (i21)) % 0.39/0.62 ((i22) != (i33)) % 0.39/0.62 ((i2) != (i29)) % 0.39/0.62 ((i15) != (i17)) % 0.39/0.62 ((i40) != (i47)) % 0.39/0.62 ((i29) != (i35)) % 0.39/0.62 ((i40) != (i45)) % 0.39/0.62 ((i8) != (i18)) % 0.39/0.62 ((i28) != (i50)) % 0.39/0.62 ((i9) != (i20)) % 0.39/0.62 ((i15) != (i40)) % 0.39/0.62 ((i20) != (i26)) % 0.39/0.62 ((i27) != (i38)) % 0.39/0.62 ((i7) != (i36)) % 0.39/0.62 ((i9) != (i27)) % 0.39/0.62 ((i14) != (i34)) % 0.39/0.62 ((i33) != (i35)) % 0.39/0.62 ((i5) != (i10)) % 0.39/0.62 ((i7) != (i10)) % 0.39/0.62 ((i11) != (i48)) % 0.39/0.62 ((i14) != (i15)) % 0.39/0.62 ((i11) != (i25)) % 0.39/0.62 ((i14) != (i39)) % 0.39/0.62 ((i34) != (i38)) % 0.39/0.62 ((i14) != (i47)) % 0.39/0.62 ((i39) != (i43)) % 0.39/0.62 ((i5) != (i45)) % 0.39/0.62 ((i36) != (i40)) % 0.39/0.62 ((i15) != (i18)) % 0.39/0.62 ((i35) != (i44)) % 0.39/0.62 ((i1) != (i47)) % 0.39/0.62 ((i21) != (i24)) % 0.39/0.62 ((i36) != (i39)) % 0.39/0.62 ((i44) != (i47)) % 0.39/0.62 ((i9) != (i35)) % 0.39/0.62 ((i10) != (i50)) % 0.39/0.62 ((i9) != (i28)) % 0.39/0.62 ((i18) != (i19)) % 0.39/0.62 ((i19) != (i22)) % 0.39/0.62 ((i20) != (i22)) % 0.39/0.62 ((i15) != (i28)) % 0.39/0.62 ((i16) != (i38)) % 0.39/0.62 ((i21) != (i22)) % 0.39/0.62 ((i3) != (i38)) % 0.39/0.62 ((i5) != (i33)) % 0.39/0.62 ((i7) != (i25)) % 0.39/0.62 ((i9) != (i37)) % 0.39/0.62 ((i3) != (i25)) % 0.39/0.62 ((i39) != (i40)) % 0.39/0.62 ((i1) != (i22)) % 0.39/0.62 ((i8) != (i30)) % 0.39/0.62 ((i12) != (i22)) % 0.39/0.62 ((i18) != (i48)) % 0.39/0.62 ((i11) != (i14)) % 0.39/0.62 ((i18) != (i44)) % 0.39/0.62 ((i3) != (i20)) % 0.39/0.62 ((i12) != (i23)) % 0.39/0.62 ((i23) != (i39)) % 0.39/0.62 ((i3) != (i24)) % 0.39/0.62 ((i13) != (i38)) % 0.39/0.62 ((i8) != (i25)) % 0.39/0.62 ((i17) != (i28)) % 0.39/0.62 ((i21) != (i28)) % 0.39/0.62 ((i32) != (i39)) % 0.39/0.62 ((i8) != (i39)) % 0.39/0.62 ((i16) != (i44)) % 0.39/0.62 ((i25) != (i49)) % 0.39/0.62 ((i1) != (i42)) % 0.39/0.62 ((i18) != (i39)) % 0.39/0.62 ((i13) != (i32)) % 0.39/0.62 ((i7) != (i17)) % 0.39/0.62 ((i8) != (i27)) % 0.39/0.62 ((i1) != (i15)) % 0.39/0.62 ((i18) != (i23)) % 0.39/0.62 ((i29) != (i39)) % 0.39/0.62 ((i10) != (i29)) % 0.39/0.62 ((i18) != (i46)) % 0.39/0.62 ((i15) != (i39)) % 0.39/0.62 ((i16) != (i40)) % 0.39/0.62 ((i22) != (i24)) % 0.39/0.62 ((i26) != (i46)) % 0.39/0.62 ((i1) != (i10)) % 0.39/0.62 ((i8) != (i40)) % 0.39/0.62 ((i24) != (i43)) % 0.39/0.62 ((i39) != (i50)) % 0.39/0.62 ((i26) != (i29)) % 0.39/0.62 ((i19) != (i44)) % 0.39/0.62 ((i6) != (i40)) % 0.39/0.62 ((i11) != (i28)) % 0.39/0.62 ((i15) != (i21)) % 0.39/0.62 ((i5) != (i35)) % 0.39/0.62 ((i4) != (i47)) % 0.39/0.62 ((i10) != (i24)) % 0.39/0.62 ((i13) != (i17)) % 0.39/0.62 ((i45) != (i47)) % 0.39/0.62 ((i36) != (i45)) % 0.39/0.62 ((i25) != (i38)) % 0.39/0.62 ((i30) != (i33)) % 0.39/0.62 ((i11) != (i36)) % 0.39/0.62 ((i22) != (i44)) % 0.39/0.62 ((i30) != (i35)) % 0.39/0.62 ((i17) != (i20)) % 0.39/0.62 ((i11) != (i23)) % 0.39/0.62 ((i39) != (i44)) % 0.39/0.62 ((i14) != (i26)) % 0.39/0.62 ((i16) != (i37)) % 0.39/0.62 ((i39) != (i46)) % 0.39/0.62 ((i9) != (i30)) % 0.39/0.62 ((i31) != (i44)) % 0.39/0.62 ((i22) != (i29)) % 0.39/0.62 ((i1) != (i26)) % 0.39/0.62 ((i6) != (i27)) % 0.39/0.62 ((i13) != (i44)) % 0.39/0.62 ((i19) != (i28)) % 0.39/0.62 ((i22) != (i36)) % 0.39/0.62 ((i3) != (i7)) % 0.39/0.62 ((i27) != (i30)) % 0.39/0.62 ((i19) != (i40)) % 0.39/0.62 ((i20) != (i40)) % 0.39/0.62 ((i22) != (i32)) % 0.39/0.62 ((i7) != (i8)) % 0.39/0.62 ((i29) != (i50)) % 0.39/0.62 ((i3) != (i49)) % 0.39/0.62 ((i18) != (i29)) % 0.39/0.62 ((i40) != (i50)) % 0.39/0.62 ((i14) != (i27)) % 0.39/0.62 ((i33) != (i36)) % 0.39/0.62 ((i8) != (i46)) % 0.39/0.62 ((i26) != (i45)) % 0.39/0.62 ((i2) != (i48)) % 0.39/0.62 ((i4) != (i18)) % 0.39/0.62 ((i15) != (i26)) % 0.39/0.62 ((i24) != (i33)) % 0.39/0.62 ((i24) != (i48)) % 0.39/0.62 ((i34) != (i47)) % 0.39/0.62 ((i10) != (i34)) % 0.39/0.62 ((i20) != (i42)) % 0.39/0.62 ((i2) != (i32)) % 0.39/0.62 ((i17) != (i18)) % 0.39/0.62 ((i19) != (i41)) % 0.39/0.62 ((i17) != (i39)) % 0.39/0.62 ((i19) != (i38)) % 0.39/0.62 ((i34) != (i44)) % 0.39/0.62 ((i10) != (i47)) % 0.39/0.62 ((i17) != (i37)) % 0.39/0.62 ((i3) != (i8)) % 0.39/0.62 ((i5) != (i29)) % 0.39/0.62 ((i12) != (i31)) % 0.39/0.62 ((i20) != (i46)) % 0.39/0.62 ((i25) != (i26)) % 0.39/0.62 ((i32) != (i45)) % 0.39/0.62 ((i12) != (i47)) % 0.39/0.62 ((i2) != (i47)) % 0.39/0.62 ((i17) != (i32)) % 0.39/0.62 ((i19) != (i37)) % 0.39/0.62 ((i1) != (i48)) % 0.39/0.62 ((i3) != (i37)) % 0.39/0.62 ((i11) != (i19)) % 0.39/0.62 ((i30) != (i46)) % 0.39/0.62 ((i1) != (i13)) % 0.39/0.62 ((i17) != (i29)) % 0.39/0.62 ((i31) != (i43)) % 0.39/0.62 ((i37) != (i44)) % 0.39/0.62 ((i11) != (i40)) % 0.39/0.62 ((i14) != (i33)) % 0.39/0.62 ((i16) != (i41)) % 0.39/0.62 ((i18) != (i47)) % 0.39/0.62 ((i30) != (i39)) % 0.39/0.62 ((i9) != (i11)) % 0.39/0.62 ((i10) != (i21)) % 0.39/0.62 ((i29) != (i48)) % 0.39/0.62 ((i31) != (i40)) % 0.39/0.62 ((i36) != (i41)) % 0.39/0.62 ((i18) != (i31)) % 0.39/0.62 ((i32) != (i46)) % 0.39/0.62 ((i22) != (i48)) % 0.39/0.62 ((i38) != (i49)) % 0.39/0.62 ((i5) != (i36)) % 0.39/0.62 ((i26) != (i36)) % 0.39/0.62 ((i28) != (i36)) % 0.39/0.62 ((i38) != (i50)) % 0.39/0.62 ((i6) != (i36)) % 0.39/0.62 ((i27) != (i49)) % 0.39/0.62 ((i12) != (i39)) % 0.39/0.62 ((i20) != (i21)) % 0.39/0.62 ((i2) != (i11)) % 0.39/0.62 ((i11) != (i12)) % 0.39/0.62 ((i13) != (i31)) % 0.39/0.62 ((i15) != (i35)) % 0.39/0.62 ((i35) != (i38)) % 0.39/0.62 ((i41) != (i43)) % 0.39/0.62 ((i7) != (i40)) % 0.39/0.62 ((i24) != (i39)) % 0.39/0.62 ((i27) != (i31)) % 0.39/0.62 ((i31) != (i47)) % 0.39/0.62 ((i28) != (i42)) % 0.39/0.62 ((i34) != (i48)) % 0.39/0.62 ((i31) != (i42)) % 0.39/0.62 ((i26) != (i31)) % 0.39/0.62 ((i2) != (i49)) % 0.39/0.62 ((i24) != (i41)) % 0.39/0.62 ((i11) != (i38)) % 0.39/0.62 ((i18) != (i33)) % 0.39/0.62 ((i2) != (i31)) % 0.39/0.62 ((i12) != (i27)) % 0.39/0.62 ((i14) != (i29)) % 0.39/0.62 ((i2) != (i25)) % 0.39/0.62 ((i2) != (i39)) % 0.39/0.62 ((i34) != (i46)) % 0.39/0.62 ((i42) != (i50)) % 0.39/0.62 ((i32) != (i36)) % 0.39/0.62 ((i38) != (i46)) % 0.39/0.62 ((i15) != (i41)) % 0.39/0.62 ((i24) != (i50)) % 0.39/0.62 ((i6) != (i24)) % 0.39/0.62 ((i19) != (i20)) % 0.39/0.62 ((i4) != (i32)) % 0.39/0.62 ((i42) != (i44)) % 0.39/0.62 ((i9) != (i15)) % 0.39/0.62 ((i3) != (i11)) % 0.39/0.62 ((i15) != (i29)) % 0.39/0.62 ((i26) != (i49)) % 0.39/0.62 ((i23) != (i48)) % 0.39/0.62 ((i26) != (i33)) % 0.39/0.62 ((i33) != (i43)) % 0.39/0.62 ((i13) != (i14)) % 0.39/0.62 ((i13) != (i27)) % 0.39/0.62 ((i26) != (i48)) % 0.39/0.62 ((i12) != (i48)) % 0.39/0.62 ((i36) != (i46)) % 0.39/0.62 ((i3) != (i21)) % 0.39/0.62 ((i17) != (i48)) % 0.39/0.62 ((i12) != (i49)) % 0.39/0.62 ((i33) != (i37)) % 0.39/0.62 ((i7) != (i49)) % 0.39/0.62 ((i13) != (i16)) % 0.39/0.62 ((i3) != (i13)) % 0.39/0.62 ((i16) != (i17)) % 0.39/0.62 ((i20) != (i38)) % 0.39/0.62 ((i28) != (i48)) % 0.39/0.62 ((i24) != (i25)) % 0.39/0.62 ((i27) != (i33)) % 0.39/0.62 ((i13) != (i50)) % 0.39/0.62 ((i17) != (i44)) % 0.39/0.62 ((i5) != (i34)) % 0.39/0.62 ((i23) != (i34)) % 0.39/0.62 ((i24) != (i30)) % 0.39/0.62 ((i11) != (i50)) % 0.39/0.62 ((i8) != (i49)) % 0.39/0.62 ((i42) != (i49)) % 0.39/0.62 ((i11) != (i18)) % 0.39/0.62 ((i15) != (i38)) % 0.39/0.62 ((i5) != (i38)) % 0.39/0.62 ((i11) != (i39)) % 0.39/0.62 ((i3) != (i41)) % 0.39/0.62 ((i23) != (i36)) % 0.39/0.62 ((i12) != (i21)) % 0.39/0.62 ((i12) != (i34)) % 0.39/0.62 *) % 0.39/0.62 (* NO-PROOF *) % 0.39/0.62 % SZS status GaveUp % 0.39/0.62 Number of rewrites on terms: 0 % 0.39/0.62 Number of rewrites on props: 0 % 0.39/0.62 nodes searched: 10 % 0.39/0.62 max branch formulas: 1233 % 0.39/0.62 proof nodes created: 2 % 0.39/0.62 formulas created: 8174 % 0.39/0.62 %------------------------------------------------------------------------------