%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SWW791_1 : TPTP v9.2.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n017.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 : Wed Jun 3 09:05:36 AM UTC 2026 % Result : Unsatisfiable 0.46s 0.82s % Output : Proof 0.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW791_1 : TPTP v9.2.1. Released v7.0.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.16/0.34 % Computer : n017.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Jun 2 22:29:16 EDT 2026 % 0.16/0.34 % CPUTime : % 0.45/0.62 %----Proving TF0_ARI % 0.45/0.64 --- Run --finite-model-find --decision=internal at 45... % 0.46/0.82 % SZS status Unsatisfiable % 0.46/0.82 % SZS output start Proof % 0.46/0.85 ( % 0.46/0.85 (declare-const |tptp.'PurityAxiomsCanBeAssumed'| Int) % 0.46/0.85 (declare-const |tptp.'Heap'| Int) % 0.46/0.85 (declare-const tptp.sharingMode Int) % 0.46/0.85 (declare-const |tptp.'SharingMode_Unshared'| Int) % 0.46/0.85 (declare-const |tptp.'SharingMode_LockProtected'| Int) % 0.46/0.85 (declare-const |tptp.'ClassReprInv'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'ValueArraySet'| (-> Int Int Int Int)) % 0.46/0.85 (declare-const |tptp.'IntArraySet'| (-> Int Int Int Int)) % 0.46/0.85 (declare-const |tptp.'RefArraySet'| (-> Int Int Int Int)) % 0.46/0.85 (declare-const |tptp.'ArrayIndexInvX'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'ArrayIndexInvY'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'ArrayIndex'| (-> Int Int Int Int Int)) % 0.46/0.85 (declare-const |tptp.'IntArrayGet'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'LBound'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'UBound'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'DimLength'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'ArrayCategoryValue'| Int) % 0.46/0.85 (declare-const |tptp.'ArrayCategoryInt'| Int) % 0.46/0.85 (declare-const |tptp.'ArrayCategoryRef'| Int) % 0.46/0.85 (declare-const |tptp.'ArrayCategory'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'ArrayCategoryNonNullRef'| Int) % 0.46/0.85 (declare-const |tptp.'NonNullRefArrayRaw'| (-> Int Int Int Int)) % 0.46/0.85 (declare-const |tptp.'Rank'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'ElementType'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'NonNullRefArray'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'ValueArray'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'IntArray'| (-> Int Int Int)) % 0.46/0.85 (declare-const tptp.elements Int) % 0.46/0.85 (declare-const |tptp.'ElementProxyStruct'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'StructSet'| (-> Int Int Int Int)) % 0.46/0.85 (declare-const |tptp.'OneClassDown'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'System_Boolean'| Int) % 0.46/0.85 (declare-const |tptp.'TypeName'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'TypeObject'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'IsNotNull'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'As'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'StructGet'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'ValueArrayGet'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'RefArray'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'Unbox'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'System_Array'| Int) % 0.46/0.85 (declare-const |tptp.'System_IConvertible'| Int) % 0.46/0.85 (declare-const |tptp.'System_ICloneable'| Int) % 0.46/0.85 (declare-const |tptp.'System_IComparable_1___System_String'| Int) % 0.46/0.85 (declare-const |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| Int) % 0.46/0.85 (declare-const |tptp.'System_IComparable'| Int) % 0.46/0.85 (declare-const |tptp.'System_IEquatable_1___System_String'| Int) % 0.46/0.85 (declare-const tptp.false_1 Int) % 0.46/0.85 (declare-const |tptp.'ArrayRefCount'| Int) % 0.46/0.85 (declare-const |tptp.'System_Runtime_Serialization_ISerializable'| Int) % 0.46/0.85 (declare-const |tptp.'System_Runtime_InteropServices__Exception'| Int) % 0.46/0.85 (declare-const |tptp.'Length'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'AsMutable'| (-> Int Int)) % 0.46/0.85 (declare-const tptp.count_0 (-> Int Int Int Int Int Int)) % 0.46/0.85 (declare-const |tptp.'Microsoft_Contracts_ObjectInvariantException'| Int) % 0.46/0.85 (declare-const |tptp.'System_Collections_IList'| Int) % 0.46/0.85 (declare-const tptp.ownerRef Int) % 0.46/0.85 (declare-const |tptp.'System_Collections_ICollection'| Int) % 0.46/0.85 (declare-const |tptp.'RefArrayGet'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'System_Collections_IEnumerable'| Int) % 0.46/0.85 (declare-const |tptp.'System_UInt32'| Int) % 0.46/0.85 (declare-const tptp.count_x0 (-> Int Int Int Int Int Int)) % 0.46/0.85 (declare-const |tptp.'System_Runtime_InteropServices__MemberInfo'| Int) % 0.46/0.85 (declare-const |tptp.'System_Object'| Int) % 0.46/0.85 (declare-const |tptp.'AsDirectSubClass'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'IsImmutable'| (-> Int Int)) % 0.46/0.85 (declare-const tptp.boolAnd (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'ArrayRefCount_count'| Int) % 0.46/0.85 (declare-const tptp.boolImplies (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'System_Reflection_ICustomAttributeProvider'| Int) % 0.46/0.85 (declare-const tptp.x (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'IsMemberlessType'| (-> Int Int)) % 0.46/0.85 (declare-const tptp.typeof (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'AsInterface'| (-> Int Int)) % 0.46/0.85 (declare-const tptp.anyNeq (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'DeclType'| (-> Int Int)) % 0.46/0.85 (declare-const tptp.intAtLeast (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'IsHeap'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'System_Runtime_InteropServices__Type'| Int) % 0.46/0.85 (declare-const tptp.intGreater (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'System_Reflection_MemberInfo'| Int) % 0.46/0.85 (declare-const tptp.select2 (-> Int Int Int Int)) % 0.46/0.85 (declare-const tptp.boolNot (-> Int Int)) % 0.46/0.85 (declare-const tptp.nullObject Int) % 0.46/0.85 (declare-const |tptp.'System_Reflection_IReflect'| Int) % 0.46/0.85 (declare-const |tptp.'System_Int64'| Int) % 0.46/0.85 (declare-const tptp.intAtMost (-> Int Int Int)) % 0.46/0.85 (declare-const tptp.intLess (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'FirstConsistentOwner'| Int) % 0.46/0.85 (declare-const |tptp.'System_String'| Int) % 0.46/0.85 (declare-const tptp.int_m2147483648 Int) % 0.46/0.85 (declare-const tptp.true_1 Int) % 0.46/0.85 (declare-const tptp.store2 (-> Int Int Int Int Int)) % 0.46/0.85 (declare-const |tptp.'ArrayRefCount_a'| Int) % 0.46/0.85 (declare-const tptp.inv Int) % 0.46/0.85 (declare-const tptp.boolIff (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'Microsoft_Contracts_GuardException'| Int) % 0.46/0.85 (declare-const tptp.store1 (-> Int Int Int Int)) % 0.46/0.85 (declare-const tptp.anyEqual (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'IncludedInModifiesStar'| (-> Int Int)) % 0.46/0.85 (declare-const tptp.select1 (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'Microsoft_Contracts_ICheckedException'| Int) % 0.46/0.85 (declare-const tptp.localinv Int) % 0.46/0.85 (declare-const |tptp.'System_UIntPtr'| Int) % 0.46/0.85 (declare-const |tptp.'AsImmutable'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'System_Exception'| Int) % 0.46/0.85 (declare-const |tptp.'System_Type'| Int) % 0.46/0.85 (declare-const tptp.boolOr (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'AsNonNullRefField'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'AsRepField'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'IncludeInMainFrameCondition'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'AsPureObject'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'IsStaticField'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'System_Int32'| Int) % 0.46/0.85 (declare-const tptp.int_9223372036854775807 Int) % 0.46/0.85 (declare-const |tptp.'AsRangeField'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'System_String_IsInterned_System_String_notnull'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'System_String_Equals_System_String_System_String'| (-> Int Int Int Int)) % 0.46/0.85 (declare-const |tptp.'StringEquals'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'AsElementsRepField'| (-> Int Int Int Int)) % 0.46/0.85 (declare-const |tptp.'System_String_Equals_System_String'| (-> Int Int Int Int)) % 0.46/0.85 (declare-const tptp.max (-> Int Int Int)) % 0.46/0.85 (declare-const tptp.min (-> Int Int Int)) % 0.46/0.85 (declare-const tptp.shr (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'InRange'| (-> Int Int Int)) % 0.46/0.85 (declare-const tptp.x_1 (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'AsOwner'| (-> Int Int Int)) % 0.46/0.85 (declare-const tptp.int_2147483647 Int) % 0.46/0.85 (declare-const tptp.shl (-> Int Int Int)) % 0.46/0.85 (declare-const tptp.or_1 (-> Int Int Int)) % 0.46/0.85 (declare-const tptp.and_1 (-> Int Int Int)) % 0.46/0.85 (declare-const tptp.x_2 (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'IfThenElse'| (-> Int Int Int Int)) % 0.46/0.85 (declare-const |tptp.'IntToInt'| (-> Int Int Int Int)) % 0.46/0.85 (declare-const |tptp.'System_Char'| Int) % 0.46/0.85 (declare-const tptp.int_18446744073709551615 Int) % 0.46/0.85 (declare-const |tptp.'System_UInt64'| Int) % 0.46/0.85 (declare-const tptp.int_m9223372036854775808 Int) % 0.46/0.85 (declare-const tptp.int_4294967295 Int) % 0.46/0.85 (declare-const |tptp.'System_UInt16'| Int) % 0.46/0.85 (declare-const |tptp.'System_Int16'| Int) % 0.46/0.85 (declare-const |tptp.'UnboxedType'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'System_Byte'| Int) % 0.46/0.85 (declare-const |tptp.'System_SByte'| Int) % 0.46/0.85 (declare-const |tptp.'System_IntPtr'| Int) % 0.46/0.85 (declare-const |tptp.'IsValueType'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'Box'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'BoxTester'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'BoxFunc'| (-> Int Int Int Int Int)) % 0.46/0.85 (declare-const |tptp.'BaseClass'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'PeerGroupPlaceholder'| Int) % 0.46/0.85 (declare-const tptp.allocated Int) % 0.46/0.85 (declare-const tptp.ownerFrame Int) % 0.46/0.85 (declare-const tptp.exposeVersion Int) % 0.46/0.85 (declare-const |tptp.'FieldDependsOnFCO'| (-> Int Int Int Int)) % 0.46/0.85 (declare-const |tptp.'ElementProxy'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'AsElementsPeerField'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'AsPeerField'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'StringLength'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'BeingConstructed'| Int) % 0.46/0.85 (declare-const |tptp.'NonNullFieldsAreInitialized'| Int) % 0.46/0.85 (declare-const |tptp.'AsRefField'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'Is'| (-> Int Int Int)) % 0.46/0.85 (declare-const |tptp.'ClassRepr'| (-> Int Int)) % 0.46/0.85 (declare-const |tptp.'IsAllocated'| (-> Int Int Int)) % 0.46/0.85 (define @t1 () (@var "A__questionmark_u" Int)) % 0.46/0.85 (define @t2 () (@var "A__questionmark_t" Int)) % 0.46/0.85 (define @t3 () (not (= (tptp.x @t2 @t1) tptp.true_1))) % 0.46/0.85 (define @t4 () (@var "A__questionmark_v" Int)) % 0.46/0.85 (define @t5 () (@list @t2)) % 0.46/0.85 (define @t6 () (@var "A__questionmark_y" Int)) % 0.46/0.85 (define @t7 () (@var "A__questionmark_x_3" Int)) % 0.46/0.85 (define @t8 () (@list @t7 @t6)) % 0.46/0.85 (define @t9 () (= @t7 @t6)) % 0.46/0.85 (define @t10 () (= @t7 tptp.true_1)) % 0.46/0.85 (define @t11 () (not @t10)) % 0.46/0.85 (define @t12 () (= @t6 tptp.true_1)) % 0.46/0.85 (define @t13 () (@var "A__questionmark_g" Int)) % 0.46/0.85 (define @t14 () (@var "A__questionmark_p" Int)) % 0.46/0.85 (define @t15 () (@var "A__questionmark_A" Int)) % 0.46/0.85 (define @t16 () (@var "A__questionmark_f" Int)) % 0.46/0.85 (define @t17 () (@var "A__questionmark_o" Int)) % 0.46/0.85 (define @t18 () (tptp.store2 @t15 @t17 @t16 @t4)) % 0.46/0.85 (define @t19 () (= (tptp.select2 @t18 @t14 @t13) (tptp.select2 @t15 @t14 @t13))) % 0.46/0.85 (define @t20 () (@list @t15 @t17 @t16 @t14 @t13 @t4)) % 0.46/0.85 (define @t21 () (@var "A__questionmark_j" Int)) % 0.46/0.85 (define @t22 () (@var "A__questionmark_i" Int)) % 0.46/0.85 (define @t23 () (tptp.store1 @t15 @t22 @t4)) % 0.46/0.85 (define @t24 () (not (= @t22 @t21))) % 0.46/0.85 (define @t25 () (@var "A__questionmark_v_7_1" Int)) % 0.46/0.85 (define @t26 () (@var "A__questionmark_oi" Int)) % 0.46/0.85 (define @t27 () (@var "A__questionmark_h" Int)) % 0.46/0.85 (define @t28 () (tptp.select2 @t27 @t26 tptp.localinv)) % 0.46/0.85 (define @t29 () (tptp.select2 @t27 @t26 tptp.inv)) % 0.46/0.85 (define @t30 () (not (= (|tptp.'IsHeap'| @t27) tptp.true_1))) % 0.46/0.85 (define @t31 () (@list @t26 @t27)) % 0.46/0.85 (define @t32 () (@var "A__questionmark_v_6_2" Int)) % 0.46/0.85 (define @t33 () (@var "A__questionmark_x_6" Int)) % 0.46/0.85 (define @t34 () (@var "A__questionmark_x_5" Int)) % 0.46/0.85 (define @t35 () (@var "A__questionmark_x_4" Int)) % 0.46/0.85 (define @t36 () (@var "A__questionmark_v_64_65" Int)) % 0.46/0.85 (define @t37 () (@var "A__questionmark_lo" Int)) % 0.46/0.85 (define @t38 () (@var "A__questionmark_hi" Int)) % 0.46/0.85 (define @t39 () (tptp.count_x0 @t37 @t38 @t35 @t34 @t33)) % 0.46/0.85 (define @t40 () (= @t35 tptp.true_1)) % 0.46/0.85 (define @t41 () (not @t40)) % 0.46/0.85 (define @t42 () (not (< @t37 @t38))) % 0.46/0.85 (define @t43 () (- @t38 1)) % 0.46/0.85 (define @t44 () (@list @t37 @t38 @t35 @t34 @t33)) % 0.46/0.85 (define @t45 () (@var "A__questionmark_v_63_64" Int)) % 0.46/0.85 (define @t46 () (tptp.count_x0 (+ @t37 1) @t38 @t35 @t34 @t33)) % 0.46/0.85 (define @t47 () (not (not (= (|tptp.'RefArrayGet'| @t34 @t37) @t33)))) % 0.46/0.85 (define @t48 () (@var "A__questionmark_mid" Int)) % 0.46/0.85 (define @t49 () (@var "A__questionmark_x_2_1" Int)) % 0.46/0.85 (define @t50 () (@var "A__questionmark_x_1_1" Int)) % 0.46/0.85 (define @t51 () (@var "A__questionmark_x_0" Int)) % 0.46/0.85 (define @t52 () (@var "A__questionmark_x_7" Int)) % 0.46/0.85 (define @t53 () (= (|tptp.'RefArrayGet'| @t34 @t52) @t33)) % 0.46/0.85 (define @t54 () (not (< @t52 @t38))) % 0.46/0.85 (define @t55 () (not (<= @t37 @t52))) % 0.46/0.85 (define @t56 () (@list @t52)) % 0.46/0.85 (define @t57 () (@var "A__questionmark_v_5_3" Int)) % 0.46/0.85 (define @t58 () (@var "A__questionmark_v_4_4" Int)) % 0.46/0.85 (define @t59 () (@var "A__questionmark_v_3_5" Int)) % 0.46/0.85 (define @t60 () (@var "A__questionmark_v_61_62" Int)) % 0.46/0.85 (define @t61 () (@var "A__questionmark_v_0_6" Int)) % 0.46/0.85 (define @t62 () (@var "A__questionmark_v_2_7" Int)) % 0.46/0.85 (define @t63 () (@var "A__questionmark_U" Int)) % 0.46/0.85 (define @t64 () (@var "A__questionmark_v_1_8" Int)) % 0.46/0.85 (define @t65 () (@var "A__questionmark_b" Int)) % 0.46/0.85 (define @t66 () (@var "A__questionmark_h_1" Int)) % 0.46/0.85 (define @t67 () (@var "A__questionmark_a" Int)) % 0.46/0.85 (define @t68 () (= (|tptp.'System_String_Equals_System_String_System_String'| @t66 @t67 @t65) tptp.true_1)) % 0.46/0.85 (define @t69 () (not (not (= @t67 tptp.nullObject)))) % 0.46/0.85 (define @t70 () (@list @t66 @t67 @t65)) % 0.46/0.85 (define @t71 () (@var "A__questionmark_c" Int)) % 0.46/0.85 (define @t72 () (= (|tptp.'StringEquals'| @t67 @t65) tptp.true_1)) % 0.46/0.85 (define @t73 () (@var "A__questionmark_v_58_59" Int)) % 0.46/0.85 (define @t74 () (@var "A__questionmark_v_57_58" Int)) % 0.46/0.85 (define @t75 () (- @t21 1)) % 0.46/0.85 (define @t76 () (<= 1 @t21)) % 0.46/0.85 (define @t77 () (@list @t22 @t21)) % 0.46/0.85 (define @t78 () (@list @t22)) % 0.46/0.85 (define @t79 () (@var "A__questionmark_v_56_57" Int)) % 0.46/0.85 (define @t80 () (not (< @t22 32768))) % 0.46/0.85 (define @t81 () (not (<= 0 @t22))) % 0.46/0.85 (define @t82 () (tptp.shl @t22 @t21)) % 0.46/0.85 (define @t83 () (+ @t7 @t6)) % 0.46/0.85 (define @t84 () (@var "A__questionmark_v_55_56" Int)) % 0.46/0.85 (define @t85 () (<= 0 @t6)) % 0.46/0.85 (define @t86 () (not @t85)) % 0.46/0.85 (define @t87 () (<= 0 @t7)) % 0.46/0.85 (define @t88 () (not @t87)) % 0.46/0.85 (define @t89 () (not (or @t88 @t86))) % 0.46/0.85 (define @t90 () (@var "A__questionmark_d" Int)) % 0.46/0.85 (define @t91 () (tptp.x_2 @t7 @t6)) % 0.46/0.85 (define @t92 () (@var "A__questionmark_v_54_55" Int)) % 0.46/0.85 (define @t93 () (@var "A__questionmark_v_53_54" Int)) % 0.46/0.85 (define @t94 () (not (< @t6 0))) % 0.46/0.85 (define @t95 () (not (<= @t7 0))) % 0.46/0.85 (define @t96 () (@var "A__questionmark_v_52_53" Int)) % 0.46/0.85 (define @t97 () (- 0 @t6)) % 0.46/0.85 (define @t98 () (not (< 0 @t6))) % 0.46/0.85 (define @t99 () (@var "A__questionmark_v_51_52" Int)) % 0.46/0.85 (define @t100 () (@var "A__questionmark_v_50_51" Int)) % 0.46/0.85 (define @t101 () (|tptp.'IfThenElse'| @t65 @t7 @t6)) % 0.46/0.85 (define @t102 () (= @t65 tptp.true_1)) % 0.46/0.85 (define @t103 () (@list @t65 @t7 @t6)) % 0.46/0.85 (define @t104 () (@var "A__questionmark_z" Int)) % 0.46/0.85 (define @t105 () (@var "A__questionmark_C" Int)) % 0.46/0.85 (define @t106 () (@var "A__questionmark_B" Int)) % 0.46/0.85 (define @t107 () (not (or @t81 (not (< @t22 65536))))) % 0.46/0.85 (define @t108 () (@var "A__questionmark_typ" Int)) % 0.46/0.85 (define @t109 () (not (= (|tptp.'BoxTester'| @t14 @t108) tptp.nullObject))) % 0.46/0.85 (define @t110 () (@list @t14 @t108)) % 0.46/0.85 (define @t111 () (|tptp.'UnboxedType'| @t14)) % 0.46/0.85 (define @t112 () (@var "A__questionmark_v_49_50" Int)) % 0.46/0.85 (define @t113 () (|tptp.'Box'| @t7 @t14)) % 0.46/0.85 (define @t114 () (@list @t7 @t14)) % 0.46/0.85 (define @t115 () (@var "A__questionmark_v_48_49" Int)) % 0.46/0.85 (define @t116 () (@var "A__questionmark_v_47_48" Int)) % 0.46/0.85 (define @t117 () (@var "A__questionmark_heap" Int)) % 0.46/0.85 (define @t118 () (= (|tptp.'IsHeap'| @t117) tptp.true_1)) % 0.46/0.85 (define @t119 () (@var "A__questionmark_activity" Int)) % 0.46/0.85 (define @t120 () (@var "A__questionmark_occurrence" Int)) % 0.46/0.85 (define @t121 () (@var "A__questionmark_v_46_47" Int)) % 0.46/0.85 (define @t122 () (@var "A__questionmark_value" Int)) % 0.46/0.85 (define @t123 () (@var "A__questionmark_v_44_43" Int)) % 0.46/0.85 (define @t124 () (@var "A__questionmark_v_45_44" Int)) % 0.46/0.85 (define @t125 () (@var "A__questionmark_v_43_42" Int)) % 0.46/0.85 (define @t126 () (@var "A__questionmark_v_41_45" Int)) % 0.46/0.85 (define @t127 () (@var "A__questionmark_v_42_46" Int)) % 0.46/0.85 (define @t128 () (= (tptp.select2 @t66 @t17 tptp.allocated) tptp.true_1)) % 0.46/0.85 (define @t129 () (not (= @t128 true))) % 0.46/0.85 (define @t130 () (= @t17 tptp.nullObject)) % 0.46/0.85 (define @t131 () (not (not @t130))) % 0.46/0.85 (define @t132 () (= (|tptp.'IsHeap'| @t66) tptp.true_1)) % 0.46/0.85 (define @t133 () (not @t132)) % 0.46/0.85 (define @t134 () (tptp.select2 @t66 @t17 tptp.ownerRef)) % 0.46/0.85 (define @t135 () (tptp.select2 @t66 @t17 tptp.ownerFrame)) % 0.46/0.85 (define @t136 () (tptp.select2 @t66 @t17 |tptp.'FirstConsistentOwner'|)) % 0.46/0.85 (define @t137 () (tptp.select2 @t66 @t17 @t16)) % 0.46/0.85 (define @t138 () (@var "A__questionmark_v_39_40" Int)) % 0.46/0.85 (define @t139 () (@var "A__questionmark_v_40_41" Int)) % 0.46/0.85 (define @t140 () (@var "A__questionmark_v_38_37" Int)) % 0.46/0.85 (define @t141 () (tptp.select2 @t66 @t17 tptp.localinv)) % 0.46/0.85 (define @t142 () (tptp.select2 @t66 @t17 tptp.inv)) % 0.46/0.85 (define @t143 () (@var "A__questionmark_v_36_38" Int)) % 0.46/0.85 (define @t144 () (@var "A__questionmark_v_37_39" Int)) % 0.46/0.85 (define @t145 () (tptp.typeof @t17)) % 0.46/0.85 (define @t146 () (@list @t66 @t17)) % 0.46/0.85 (define @t147 () (@var "A__questionmark_v_35_36" Int)) % 0.46/0.85 (define @t148 () (@var "A__questionmark_v_34_35" Int)) % 0.46/0.85 (define @t149 () (@var "A__questionmark_T" Int)) % 0.46/0.85 (define @t150 () (@var "A__questionmark_v_33_34" Int)) % 0.46/0.85 (define @t151 () (@var "A__questionmark_v_32_33" Int)) % 0.46/0.85 (define @t152 () (@var "A__questionmark_v_31_32" Int)) % 0.46/0.85 (define @t153 () (@list @t66 @t17 @t16)) % 0.46/0.85 (define @t154 () (@var "A__questionmark_v_30_31" Int)) % 0.46/0.85 (define @t155 () (@list @t66 @t17 @t16 @t149)) % 0.46/0.85 (define @t156 () (@var "A__questionmark_s" Int)) % 0.46/0.85 (define @t157 () (@var "A__questionmark_v_29_30" Int)) % 0.46/0.85 (define @t158 () (|tptp.'AsImmutable'| @t149)) % 0.46/0.85 (define @t159 () (not (= @t17 |tptp.'BeingConstructed'|))) % 0.46/0.85 (define @t160 () (@list @t17 @t149)) % 0.46/0.85 (define @t161 () (@var "A__questionmark_U_1" Int)) % 0.46/0.85 (define @t162 () (not (= (|tptp.'IsImmutable'| @t161) tptp.true_1))) % 0.46/0.85 (define @t163 () (@list @t149 @t161)) % 0.46/0.85 (define @t164 () (@var "A__questionmark_J" Int)) % 0.46/0.85 (define @t165 () (@var "A__questionmark_v_28_28" Int)) % 0.46/0.85 (define @t166 () (@var "A__questionmark_v_27_29" Int)) % 0.46/0.85 (define @t167 () (|tptp.'AsNonNullRefField'| @t16 @t149)) % 0.46/0.85 (define @t168 () (|tptp.'AsRefField'| @t16 @t149)) % 0.46/0.85 (define @t169 () (|tptp.'ClassRepr'| @t71)) % 0.46/0.85 (define @t170 () (@var "A__questionmark_e" Int)) % 0.46/0.85 (define @t171 () (= (|tptp.'IsAllocated'| @t66 @t170) tptp.true_1)) % 0.46/0.85 (define @t172 () (@list @t66 @t170 @t22)) % 0.46/0.85 (define @t173 () (not (or @t133 (not @t128)))) % 0.46/0.85 (define @t174 () (@var "A__questionmark_v_26_27" Int)) % 0.46/0.85 (define @t175 () (|tptp.'As'| @t17 @t149)) % 0.46/0.85 (define @t176 () (= (|tptp.'Is'| @t17 @t149) tptp.true_1)) % 0.46/0.85 (define @t177 () (not @t176)) % 0.46/0.85 (define @t178 () (|tptp.'TypeObject'| @t149)) % 0.46/0.85 (define @t179 () (@list @t149)) % 0.46/0.85 (define @t180 () (= @t149 @t161)) % 0.46/0.85 (define @t181 () (= (tptp.x @t161 @t149) tptp.true_1)) % 0.46/0.85 (define @t182 () (@list @t161)) % 0.46/0.85 (define @t183 () (@var "A__questionmark_v_25_26" Int)) % 0.46/0.85 (define @t184 () (@var "A__questionmark_f_prime_" Int)) % 0.46/0.85 (define @t185 () (|tptp.'StructSet'| @t156 @t16 @t7)) % 0.46/0.85 (define @t186 () (@var "A__questionmark_pos" Int)) % 0.46/0.85 (define @t187 () (@list @t17 @t186)) % 0.46/0.85 (define @t188 () (|tptp.'ElementProxy'| @t67 (- 0 1))) % 0.46/0.85 (define @t189 () (tptp.typeof @t67)) % 0.46/0.85 (define @t190 () (not (= (tptp.x @t189 |tptp.'System_Array'|) tptp.true_1))) % 0.46/0.85 (define @t191 () (not @t118)) % 0.46/0.85 (define @t192 () (@var "A__questionmark_v_24_24" Int)) % 0.46/0.85 (define @t193 () (@var "A__questionmark_v_23_25" Int)) % 0.46/0.85 (define @t194 () (tptp.select2 @t117 @t67 tptp.elements)) % 0.46/0.85 (define @t195 () (|tptp.'RefArrayGet'| @t194 @t22)) % 0.46/0.85 (define @t196 () (@list @t67 @t22 @t117)) % 0.46/0.85 (define @t197 () (@var "A__questionmark_v_22_23" Int)) % 0.46/0.85 (define @t198 () (= (tptp.x |tptp.'System_Array'| @t149) tptp.true_1)) % 0.46/0.85 (define @t199 () (@var "A__questionmark_r" Int)) % 0.46/0.85 (define @t200 () (|tptp.'IntArray'| @t15 @t199)) % 0.46/0.85 (define @t201 () (@list @t15 @t199 @t149)) % 0.46/0.85 (define @t202 () (@var "A__questionmark_v_21_22" Int)) % 0.46/0.85 (define @t203 () (|tptp.'ValueArray'| @t15 @t199)) % 0.46/0.85 (define @t204 () (@var "A__questionmark_v_20_21" Int)) % 0.46/0.85 (define @t205 () (|tptp.'NonNullRefArray'| @t15 @t199)) % 0.46/0.85 (define @t206 () (|tptp.'ElementType'| @t149)) % 0.46/0.85 (define @t207 () (@var "A__questionmark_v_19_20" Int)) % 0.46/0.85 (define @t208 () (|tptp.'RefArray'| @t15 @t199)) % 0.46/0.85 (define @t209 () (@var "A__questionmark_v_18_19" Int)) % 0.46/0.85 (define @t210 () (@var "A__questionmark_v_17_18" Int)) % 0.46/0.85 (define @t211 () (@var "A__questionmark_v_16_17" Int)) % 0.46/0.85 (define @t212 () (not (not (= @t149 @t15)))) % 0.46/0.85 (define @t213 () (@var "A__questionmark_v_15_16" Int)) % 0.46/0.85 (define @t214 () (@list @t15 @t199)) % 0.46/0.85 (define @t215 () (|tptp.'NonNullRefArray'| @t149 @t199)) % 0.46/0.85 (define @t216 () (@list @t149 @t161 @t199)) % 0.46/0.85 (define @t217 () (|tptp.'RefArray'| @t149 @t199)) % 0.46/0.85 (define @t218 () (@var "A__questionmark_v_14_15" Int)) % 0.46/0.85 (define @t219 () (@var "A__questionmark_elementType" Int)) % 0.46/0.85 (define @t220 () (@var "A__questionmark_rank" Int)) % 0.46/0.85 (define @t221 () (@var "A__questionmark_array" Int)) % 0.46/0.85 (define @t222 () (@var "A__questionmark_v_13_14" Int)) % 0.46/0.85 (define @t223 () (@list @t149 @t199)) % 0.46/0.85 (define @t224 () (@var "A__questionmark_v_12_13" Int)) % 0.46/0.85 (define @t225 () (@var "A__questionmark_v_11_12" Int)) % 0.46/0.85 (define @t226 () (|tptp.'IntArray'| @t149 @t199)) % 0.46/0.85 (define @t227 () (@var "A__questionmark_v_10_11" Int)) % 0.46/0.85 (define @t228 () (|tptp.'ValueArray'| @t149 @t199)) % 0.46/0.85 (define @t229 () (|tptp.'ArrayCategory'| @t149)) % 0.46/0.85 (define @t230 () (@var "A__questionmark_ET" Int)) % 0.46/0.85 (define @t231 () (@list @t149 @t230 @t199)) % 0.46/0.85 (define @t232 () (|tptp.'DimLength'| @t67 @t22)) % 0.46/0.85 (define @t233 () (@list @t67 @t22)) % 0.46/0.85 (define @t234 () (|tptp.'Length'| @t67)) % 0.46/0.85 (define @t235 () (|tptp.'Rank'| @t67)) % 0.46/0.85 (define @t236 () (@list @t67)) % 0.46/0.85 (define @t237 () (@var "A__questionmark_v_9_10" Int)) % 0.46/0.85 (define @t238 () (= @t235 @t199)) % 0.46/0.85 (define @t239 () (@list @t67 @t149 @t199)) % 0.46/0.85 (define @t240 () (not (= (tptp.x @t189 @t215) tptp.true_1))) % 0.46/0.85 (define @t241 () (|tptp.'ElementType'| @t189)) % 0.46/0.85 (define @t242 () (@var "A__questionmark_v_8_9" Int)) % 0.46/0.85 (define @t243 () (|tptp.'ArrayIndex'| @t67 @t90 @t7 @t6)) % 0.46/0.85 (define @t244 () (@list @t67 @t90 @t7 @t6)) % 0.46/0.85 (define @t245 () (|tptp.'RefArraySet'| @t15 @t22 @t7)) % 0.46/0.85 (define @t246 () (@list @t15 @t22 @t21 @t7)) % 0.46/0.85 (define @t247 () (@list @t15 @t22 @t7)) % 0.46/0.85 (define @t248 () (|tptp.'IntArraySet'| @t15 @t22 @t7)) % 0.46/0.85 (define @t249 () (|tptp.'ValueArraySet'| @t15 @t22 @t7)) % 0.46/0.85 (define @t250 () (|tptp.'ClassRepr'| @t149)) % 0.46/0.85 (define @t251 () (@var "A__questionmark_v_4_71" Int)) % 0.46/0.85 (define @t252 () (@var "A__questionmark_v_1_73" Int)) % 0.46/0.85 (define @t253 () (@var "A__questionmark_v_2_74" Int)) % 0.46/0.85 (define @t254 () (@var "A__questionmark_o_1" Int)) % 0.46/0.85 (define @t255 () (tptp.select2 |tptp.'Heap'| @t254 tptp.allocated)) % 0.46/0.85 (define @t256 () (= @t255 tptp.true_1)) % 0.46/0.85 (define @t257 () (not @t256)) % 0.46/0.85 (define @t258 () (= @t254 tptp.nullObject)) % 0.46/0.85 (define @t259 () (not (not @t258))) % 0.46/0.85 (define @t260 () (@var "A__questionmark_f_1" Int)) % 0.46/0.85 (define @t261 () (|tptp.'IncludeInMainFrameCondition'| @t260)) % 0.46/0.85 (define @t262 () (= @t261 tptp.true_1)) % 0.46/0.85 (define @t263 () (not @t262)) % 0.46/0.85 (define @t264 () (tptp.select2 |tptp.'Heap'| @t254 tptp.ownerRef)) % 0.46/0.85 (define @t265 () (tptp.select2 |tptp.'Heap'| @t254 tptp.ownerFrame)) % 0.46/0.85 (define @t266 () (tptp.select2 |tptp.'Heap'| @t254 @t260)) % 0.46/0.85 (define @t267 () (@list @t254 @t260)) % 0.46/0.85 (define @t268 () (forall @t267 (exists (@list @t251 @t252 @t253) (and (= @t251 @t266) (= @t252 @t265) (= @t253 @t264) (=> (not (or @t263 @t259 @t257 (not (or (= @t252 |tptp.'PeerGroupPlaceholder'|) (not (= (tptp.x (tptp.select2 |tptp.'Heap'| @t253 tptp.inv) @t252) tptp.true_1)) (= (tptp.select2 |tptp.'Heap'| @t253 tptp.localinv) (|tptp.'BaseClass'| @t252)))))) (= @t251 @t251)))))) % 0.46/0.85 (define @t269 () (not (=> @t268 true))) % 0.46/0.85 (define @t270 () (@var "A__questionmark_v_4_67" Int)) % 0.46/0.85 (define @t271 () (@var "A__questionmark_v_1_69" Int)) % 0.46/0.85 (define @t272 () (@var "A__questionmark_v_2_70" Int)) % 0.46/0.85 (define @t273 () (= (tptp.select2 |tptp.'Heap'| @t272 tptp.localinv) (|tptp.'BaseClass'| @t271))) % 0.46/0.85 (define @t274 () (tptp.x (tptp.select2 |tptp.'Heap'| @t272 tptp.inv) @t271)) % 0.46/0.85 (define @t275 () (= @t274 tptp.true_1)) % 0.46/0.85 (define @t276 () (not @t275)) % 0.46/0.85 (define @t277 () (= @t271 |tptp.'PeerGroupPlaceholder'|)) % 0.46/0.85 (define @t278 () (or @t277 @t276 @t273)) % 0.46/0.85 (define @t279 () (not @t278)) % 0.46/0.85 (define @t280 () (or @t263 @t259 @t257 @t279)) % 0.46/0.85 (define @t281 () (not @t280)) % 0.46/0.85 (define @t282 () (=> @t281 (= @t270 @t270))) % 0.46/0.85 (define @t283 () (= @t272 @t264)) % 0.46/0.85 (define @t284 () (= @t271 @t265)) % 0.46/0.85 (define @t285 () (= @t270 @t266)) % 0.46/0.85 (define @t286 () (and @t285 @t284 @t283 @t282)) % 0.46/0.85 (define @t287 () (@list @t270 @t271 @t272)) % 0.46/0.85 (define @t288 () (exists @t287 @t286)) % 0.46/0.85 (define @t289 () (forall @t267 @t288)) % 0.46/0.85 (define @t290 () (not @t289)) % 0.46/0.85 (define @t291 () (or @t290 @t269)) % 0.46/0.85 (define @t292 () (not @t291)) % 0.46/0.85 (define @t293 () (= |tptp.'BeingConstructed'| tptp.nullObject)) % 0.46/0.85 (define @t294 () (=> @t293 @t292)) % 0.46/0.85 (define @t295 () (= |tptp.'PurityAxiomsCanBeAssumed'| tptp.true_1)) % 0.46/0.85 (define @t296 () (=> @t295 @t294)) % 0.46/0.85 (define @t297 () (|tptp.'IsHeap'| |tptp.'Heap'|)) % 0.46/0.85 (define @t298 () (= @t297 tptp.true_1)) % 0.46/0.85 (define @t299 () (=> @t298 @t296)) % 0.46/0.85 (define @t300 () (not @t299)) % 0.46/0.85 (define @t301 () (= tptp.true_1 @t297)) % 0.46/0.85 (define @t302 () (= tptp.true_1 |tptp.'PurityAxiomsCanBeAssumed'|)) % 0.46/0.85 (define @t303 () (not (= @t264 @t264))) % 0.46/0.85 (define @t304 () (not @t283)) % 0.46/0.85 (define @t305 () (or @t304 @t304)) % 0.46/0.85 (define @t306 () (@list @t272)) % 0.46/0.85 (define @t307 () (forall @t306 @t304)) % 0.46/0.85 (define @t308 () (not (= @t265 @t265))) % 0.46/0.85 (define @t309 () (not @t284)) % 0.46/0.85 (define @t310 () (or @t309 @t309)) % 0.46/0.85 (define @t311 () (@list @t271)) % 0.46/0.85 (define @t312 () (forall @t311 @t309)) % 0.46/0.85 (define @t313 () (not (= @t266 @t266))) % 0.46/0.85 (define @t314 () (not @t285)) % 0.46/0.85 (define @t315 () (or @t314 @t314)) % 0.46/0.85 (define @t316 () (@list @t270)) % 0.46/0.85 (define @t317 () (forall @t316 @t314)) % 0.46/0.85 (define @t318 () (or @t317 @t312 @t307)) % 0.46/0.85 (define @t319 () (or @t314 @t309 @t304)) % 0.46/0.85 (define @t320 () (and @t285 @t284 @t283)) % 0.46/0.85 (define @t321 () (forall @t287 (not @t320))) % 0.46/0.85 (define @t322 () (not @t321)) % 0.46/0.85 (define @t323 () (= tptp.true_1 @t274)) % 0.46/0.85 (define @t324 () (= |tptp.'PeerGroupPlaceholder'| @t271)) % 0.46/0.85 (define @t325 () (= tptp.true_1 @t255)) % 0.46/0.85 (define @t326 () (= tptp.nullObject @t254)) % 0.46/0.85 (define @t327 () (= tptp.true_1 @t261)) % 0.46/0.85 (assume @p1 (not (or (not (forall (@list @t15 @t22 @t4) (= (tptp.select1 @t23 @t22) @t4))) (not (forall (@list @t15 @t22 @t21 @t4) (=> @t24 (= (tptp.select1 @t23 @t21) (tptp.select1 @t15 @t21))))) (not (forall (@list @t15 @t17 @t16 @t4) (= (tptp.select2 @t18 @t17 @t16) @t4))) (not (forall @t20 (=> (not (= @t17 @t14)) @t19))) (not (forall @t20 (=> (not (= @t16 @t13)) @t19))) (not (forall @t8 (= (= (tptp.boolIff @t7 @t6) tptp.true_1) (= @t10 @t12)))) (not (forall @t8 (= (= (tptp.boolImplies @t7 @t6) tptp.true_1) (=> @t10 @t12)))) (not (forall @t8 (= (= (tptp.boolAnd @t7 @t6) tptp.true_1) (not (or @t11 (not @t12)))))) (not (forall @t8 (= (= (tptp.boolOr @t7 @t6) tptp.true_1) (or @t10 @t12)))) (not (forall (@list @t7) (= (= (tptp.boolNot @t7) tptp.true_1) @t11))) (not (forall @t8 (= (= (tptp.anyEqual @t7 @t6) tptp.true_1) @t9))) (not (forall @t8 (= (= (tptp.anyNeq @t7 @t6) tptp.true_1) (not @t9)))) (not (forall @t8 (= (= (tptp.intLess @t7 @t6) tptp.true_1) (< @t7 @t6)))) (not (forall @t8 (= (= (tptp.intAtMost @t7 @t6) tptp.true_1) (<= @t7 @t6)))) (not (forall @t8 (= (= (tptp.intAtLeast @t7 @t6) tptp.true_1) (>= @t7 @t6)))) (not (forall @t8 (= (= (tptp.intGreater @t7 @t6) tptp.true_1) (> @t7 @t6)))) (not (not (= tptp.false_1 tptp.true_1))) (not (forall @t5 (= (tptp.x @t2 @t2) tptp.true_1))) (not (forall (@list @t2 @t1 @t4) (=> (not (or @t3 (not (= (tptp.x @t1 @t4) tptp.true_1)))) (= (tptp.x @t2 @t4) tptp.true_1)))) (not (forall (@list @t2 @t1) (=> (not (or @t3 (not (= (tptp.x @t1 @t2) tptp.true_1)))) (= @t2 @t1))))))) % 0.46/0.85 (assume @p2 (exists (@list @t25 @t32 @t57 @t58 @t59 @t61 @t62 @t64) (and (= @t25 (|tptp.'BaseClass'| |tptp.'System_Type'|)) (= @t32 (|tptp.'BaseClass'| |tptp.'System_Reflection_MemberInfo'|)) (= @t57 (|tptp.'BaseClass'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (= @t58 (|tptp.'BaseClass'| |tptp.'Microsoft_Contracts_GuardException'|)) (= @t59 (|tptp.'BaseClass'| |tptp.'System_Exception'|)) (= @t61 (|tptp.'BaseClass'| |tptp.'ArrayRefCount'|)) (= @t62 (|tptp.'BaseClass'| |tptp.'System_String'|)) (= @t64 (|tptp.'BaseClass'| |tptp.'System_Array'|)) (not (or (not (and (not (= tptp.allocated tptp.elements)) (not (= tptp.allocated tptp.inv)) (not (= tptp.allocated tptp.localinv)) (not (= tptp.allocated tptp.exposeVersion)) (not (= tptp.allocated tptp.sharingMode)) (not (= tptp.allocated |tptp.'SharingMode_Unshared'|)) (not (= tptp.allocated |tptp.'SharingMode_LockProtected'|)) (not (= tptp.allocated tptp.ownerRef)) (not (= tptp.allocated tptp.ownerFrame)) (not (= tptp.allocated |tptp.'PeerGroupPlaceholder'|)) (not (= tptp.allocated |tptp.'ArrayCategoryValue'|)) (not (= tptp.allocated |tptp.'ArrayCategoryInt'|)) (not (= tptp.allocated |tptp.'ArrayCategoryRef'|)) (not (= tptp.allocated |tptp.'ArrayCategoryNonNullRef'|)) (not (= tptp.allocated |tptp.'System_Array'|)) (not (= tptp.allocated |tptp.'System_Boolean'|)) (not (= tptp.allocated |tptp.'System_Object'|)) (not (= tptp.allocated |tptp.'System_Type'|)) (not (= tptp.allocated |tptp.'NonNullFieldsAreInitialized'|)) (not (= tptp.allocated |tptp.'System_String'|)) (not (= tptp.allocated |tptp.'FirstConsistentOwner'|)) (not (= tptp.allocated |tptp.'System_SByte'|)) (not (= tptp.allocated |tptp.'System_Byte'|)) (not (= tptp.allocated |tptp.'System_Int16'|)) (not (= tptp.allocated |tptp.'System_UInt16'|)) (not (= tptp.allocated |tptp.'System_Int32'|)) (not (= tptp.allocated |tptp.'System_UInt32'|)) (not (= tptp.allocated |tptp.'System_Int64'|)) (not (= tptp.allocated |tptp.'System_UInt64'|)) (not (= tptp.allocated |tptp.'System_Char'|)) (not (= tptp.allocated |tptp.'System_UIntPtr'|)) (not (= tptp.allocated |tptp.'System_IntPtr'|)) (not (= tptp.allocated |tptp.'ArrayRefCount_a'|)) (not (= tptp.allocated |tptp.'ArrayRefCount_count'|)) (not (= tptp.allocated |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= tptp.allocated |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= tptp.allocated |tptp.'System_Collections_ICollection'|)) (not (= tptp.allocated |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= tptp.allocated |tptp.'System_ICloneable'|)) (not (= tptp.allocated |tptp.'System_IComparable'|)) (not (= tptp.allocated |tptp.'Microsoft_Contracts_GuardException'|)) (not (= tptp.allocated |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= tptp.allocated |tptp.'System_Collections_IEnumerable'|)) (not (= tptp.allocated |tptp.'System_Reflection_MemberInfo'|)) (not (= tptp.allocated |tptp.'System_Reflection_IReflect'|)) (not (= tptp.allocated |tptp.'System_Exception'|)) (not (= tptp.allocated |tptp.'System_Runtime_InteropServices__Type'|)) (not (= tptp.allocated |tptp.'System_IComparable_1___System_String'|)) (not (= tptp.allocated |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= tptp.allocated |tptp.'System_IEquatable_1___System_String'|)) (not (= tptp.allocated |tptp.'ArrayRefCount'|)) (not (= tptp.allocated |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= tptp.allocated |tptp.'System_IConvertible'|)) (not (= tptp.allocated |tptp.'System_Collections_IList'|)) (not (= tptp.allocated |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= tptp.elements tptp.inv)) (not (= tptp.elements tptp.localinv)) (not (= tptp.elements tptp.exposeVersion)) (not (= tptp.elements tptp.sharingMode)) (not (= tptp.elements |tptp.'SharingMode_Unshared'|)) (not (= tptp.elements |tptp.'SharingMode_LockProtected'|)) (not (= tptp.elements tptp.ownerRef)) (not (= tptp.elements tptp.ownerFrame)) (not (= tptp.elements |tptp.'PeerGroupPlaceholder'|)) (not (= tptp.elements |tptp.'ArrayCategoryValue'|)) (not (= tptp.elements |tptp.'ArrayCategoryInt'|)) (not (= tptp.elements |tptp.'ArrayCategoryRef'|)) (not (= tptp.elements |tptp.'ArrayCategoryNonNullRef'|)) (not (= tptp.elements |tptp.'System_Array'|)) (not (= tptp.elements |tptp.'System_Boolean'|)) (not (= tptp.elements |tptp.'System_Object'|)) (not (= tptp.elements |tptp.'System_Type'|)) (not (= tptp.elements |tptp.'NonNullFieldsAreInitialized'|)) (not (= tptp.elements |tptp.'System_String'|)) (not (= tptp.elements |tptp.'FirstConsistentOwner'|)) (not (= tptp.elements |tptp.'System_SByte'|)) (not (= tptp.elements |tptp.'System_Byte'|)) (not (= tptp.elements |tptp.'System_Int16'|)) (not (= tptp.elements |tptp.'System_UInt16'|)) (not (= tptp.elements |tptp.'System_Int32'|)) (not (= tptp.elements |tptp.'System_UInt32'|)) (not (= tptp.elements |tptp.'System_Int64'|)) (not (= tptp.elements |tptp.'System_UInt64'|)) (not (= tptp.elements |tptp.'System_Char'|)) (not (= tptp.elements |tptp.'System_UIntPtr'|)) (not (= tptp.elements |tptp.'System_IntPtr'|)) (not (= tptp.elements |tptp.'ArrayRefCount_a'|)) (not (= tptp.elements |tptp.'ArrayRefCount_count'|)) (not (= tptp.elements |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= tptp.elements |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= tptp.elements |tptp.'System_Collections_ICollection'|)) (not (= tptp.elements |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= tptp.elements |tptp.'System_ICloneable'|)) (not (= tptp.elements |tptp.'System_IComparable'|)) (not (= tptp.elements |tptp.'Microsoft_Contracts_GuardException'|)) (not (= tptp.elements |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= tptp.elements |tptp.'System_Collections_IEnumerable'|)) (not (= tptp.elements |tptp.'System_Reflection_MemberInfo'|)) (not (= tptp.elements |tptp.'System_Reflection_IReflect'|)) (not (= tptp.elements |tptp.'System_Exception'|)) (not (= tptp.elements |tptp.'System_Runtime_InteropServices__Type'|)) (not (= tptp.elements |tptp.'System_IComparable_1___System_String'|)) (not (= tptp.elements |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= tptp.elements |tptp.'System_IEquatable_1___System_String'|)) (not (= tptp.elements |tptp.'ArrayRefCount'|)) (not (= tptp.elements |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= tptp.elements |tptp.'System_IConvertible'|)) (not (= tptp.elements |tptp.'System_Collections_IList'|)) (not (= tptp.elements |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= tptp.inv tptp.localinv)) (not (= tptp.inv tptp.exposeVersion)) (not (= tptp.inv tptp.sharingMode)) (not (= tptp.inv |tptp.'SharingMode_Unshared'|)) (not (= tptp.inv |tptp.'SharingMode_LockProtected'|)) (not (= tptp.inv tptp.ownerRef)) (not (= tptp.inv tptp.ownerFrame)) (not (= tptp.inv |tptp.'PeerGroupPlaceholder'|)) (not (= tptp.inv |tptp.'ArrayCategoryValue'|)) (not (= tptp.inv |tptp.'ArrayCategoryInt'|)) (not (= tptp.inv |tptp.'ArrayCategoryRef'|)) (not (= tptp.inv |tptp.'ArrayCategoryNonNullRef'|)) (not (= tptp.inv |tptp.'System_Array'|)) (not (= tptp.inv |tptp.'System_Boolean'|)) (not (= tptp.inv |tptp.'System_Object'|)) (not (= tptp.inv |tptp.'System_Type'|)) (not (= tptp.inv |tptp.'NonNullFieldsAreInitialized'|)) (not (= tptp.inv |tptp.'System_String'|)) (not (= tptp.inv |tptp.'FirstConsistentOwner'|)) (not (= tptp.inv |tptp.'System_SByte'|)) (not (= tptp.inv |tptp.'System_Byte'|)) (not (= tptp.inv |tptp.'System_Int16'|)) (not (= tptp.inv |tptp.'System_UInt16'|)) (not (= tptp.inv |tptp.'System_Int32'|)) (not (= tptp.inv |tptp.'System_UInt32'|)) (not (= tptp.inv |tptp.'System_Int64'|)) (not (= tptp.inv |tptp.'System_UInt64'|)) (not (= tptp.inv |tptp.'System_Char'|)) (not (= tptp.inv |tptp.'System_UIntPtr'|)) (not (= tptp.inv |tptp.'System_IntPtr'|)) (not (= tptp.inv |tptp.'ArrayRefCount_a'|)) (not (= tptp.inv |tptp.'ArrayRefCount_count'|)) (not (= tptp.inv |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= tptp.inv |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= tptp.inv |tptp.'System_Collections_ICollection'|)) (not (= tptp.inv |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= tptp.inv |tptp.'System_ICloneable'|)) (not (= tptp.inv |tptp.'System_IComparable'|)) (not (= tptp.inv |tptp.'Microsoft_Contracts_GuardException'|)) (not (= tptp.inv |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= tptp.inv |tptp.'System_Collections_IEnumerable'|)) (not (= tptp.inv |tptp.'System_Reflection_MemberInfo'|)) (not (= tptp.inv |tptp.'System_Reflection_IReflect'|)) (not (= tptp.inv |tptp.'System_Exception'|)) (not (= tptp.inv |tptp.'System_Runtime_InteropServices__Type'|)) (not (= tptp.inv |tptp.'System_IComparable_1___System_String'|)) (not (= tptp.inv |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= tptp.inv |tptp.'System_IEquatable_1___System_String'|)) (not (= tptp.inv |tptp.'ArrayRefCount'|)) (not (= tptp.inv |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= tptp.inv |tptp.'System_IConvertible'|)) (not (= tptp.inv |tptp.'System_Collections_IList'|)) (not (= tptp.inv |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= tptp.localinv tptp.exposeVersion)) (not (= tptp.localinv tptp.sharingMode)) (not (= tptp.localinv |tptp.'SharingMode_Unshared'|)) (not (= tptp.localinv |tptp.'SharingMode_LockProtected'|)) (not (= tptp.localinv tptp.ownerRef)) (not (= tptp.localinv tptp.ownerFrame)) (not (= tptp.localinv |tptp.'PeerGroupPlaceholder'|)) (not (= tptp.localinv |tptp.'ArrayCategoryValue'|)) (not (= tptp.localinv |tptp.'ArrayCategoryInt'|)) (not (= tptp.localinv |tptp.'ArrayCategoryRef'|)) (not (= tptp.localinv |tptp.'ArrayCategoryNonNullRef'|)) (not (= tptp.localinv |tptp.'System_Array'|)) (not (= tptp.localinv |tptp.'System_Boolean'|)) (not (= tptp.localinv |tptp.'System_Object'|)) (not (= tptp.localinv |tptp.'System_Type'|)) (not (= tptp.localinv |tptp.'NonNullFieldsAreInitialized'|)) (not (= tptp.localinv |tptp.'System_String'|)) (not (= tptp.localinv |tptp.'FirstConsistentOwner'|)) (not (= tptp.localinv |tptp.'System_SByte'|)) (not (= tptp.localinv |tptp.'System_Byte'|)) (not (= tptp.localinv |tptp.'System_Int16'|)) (not (= tptp.localinv |tptp.'System_UInt16'|)) (not (= tptp.localinv |tptp.'System_Int32'|)) (not (= tptp.localinv |tptp.'System_UInt32'|)) (not (= tptp.localinv |tptp.'System_Int64'|)) (not (= tptp.localinv |tptp.'System_UInt64'|)) (not (= tptp.localinv |tptp.'System_Char'|)) (not (= tptp.localinv |tptp.'System_UIntPtr'|)) (not (= tptp.localinv |tptp.'System_IntPtr'|)) (not (= tptp.localinv |tptp.'ArrayRefCount_a'|)) (not (= tptp.localinv |tptp.'ArrayRefCount_count'|)) (not (= tptp.localinv |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= tptp.localinv |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= tptp.localinv |tptp.'System_Collections_ICollection'|)) (not (= tptp.localinv |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= tptp.localinv |tptp.'System_ICloneable'|)) (not (= tptp.localinv |tptp.'System_IComparable'|)) (not (= tptp.localinv |tptp.'Microsoft_Contracts_GuardException'|)) (not (= tptp.localinv |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= tptp.localinv |tptp.'System_Collections_IEnumerable'|)) (not (= tptp.localinv |tptp.'System_Reflection_MemberInfo'|)) (not (= tptp.localinv |tptp.'System_Reflection_IReflect'|)) (not (= tptp.localinv |tptp.'System_Exception'|)) (not (= tptp.localinv |tptp.'System_Runtime_InteropServices__Type'|)) (not (= tptp.localinv |tptp.'System_IComparable_1___System_String'|)) (not (= tptp.localinv |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= tptp.localinv |tptp.'System_IEquatable_1___System_String'|)) (not (= tptp.localinv |tptp.'ArrayRefCount'|)) (not (= tptp.localinv |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= tptp.localinv |tptp.'System_IConvertible'|)) (not (= tptp.localinv |tptp.'System_Collections_IList'|)) (not (= tptp.localinv |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= tptp.exposeVersion tptp.sharingMode)) (not (= tptp.exposeVersion |tptp.'SharingMode_Unshared'|)) (not (= tptp.exposeVersion |tptp.'SharingMode_LockProtected'|)) (not (= tptp.exposeVersion tptp.ownerRef)) (not (= tptp.exposeVersion tptp.ownerFrame)) (not (= tptp.exposeVersion |tptp.'PeerGroupPlaceholder'|)) (not (= tptp.exposeVersion |tptp.'ArrayCategoryValue'|)) (not (= tptp.exposeVersion |tptp.'ArrayCategoryInt'|)) (not (= tptp.exposeVersion |tptp.'ArrayCategoryRef'|)) (not (= tptp.exposeVersion |tptp.'ArrayCategoryNonNullRef'|)) (not (= tptp.exposeVersion |tptp.'System_Array'|)) (not (= tptp.exposeVersion |tptp.'System_Boolean'|)) (not (= tptp.exposeVersion |tptp.'System_Object'|)) (not (= tptp.exposeVersion |tptp.'System_Type'|)) (not (= tptp.exposeVersion |tptp.'NonNullFieldsAreInitialized'|)) (not (= tptp.exposeVersion |tptp.'System_String'|)) (not (= tptp.exposeVersion |tptp.'FirstConsistentOwner'|)) (not (= tptp.exposeVersion |tptp.'System_SByte'|)) (not (= tptp.exposeVersion |tptp.'System_Byte'|)) (not (= tptp.exposeVersion |tptp.'System_Int16'|)) (not (= tptp.exposeVersion |tptp.'System_UInt16'|)) (not (= tptp.exposeVersion |tptp.'System_Int32'|)) (not (= tptp.exposeVersion |tptp.'System_UInt32'|)) (not (= tptp.exposeVersion |tptp.'System_Int64'|)) (not (= tptp.exposeVersion |tptp.'System_UInt64'|)) (not (= tptp.exposeVersion |tptp.'System_Char'|)) (not (= tptp.exposeVersion |tptp.'System_UIntPtr'|)) (not (= tptp.exposeVersion |tptp.'System_IntPtr'|)) (not (= tptp.exposeVersion |tptp.'ArrayRefCount_a'|)) (not (= tptp.exposeVersion |tptp.'ArrayRefCount_count'|)) (not (= tptp.exposeVersion |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= tptp.exposeVersion |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= tptp.exposeVersion |tptp.'System_Collections_ICollection'|)) (not (= tptp.exposeVersion |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= tptp.exposeVersion |tptp.'System_ICloneable'|)) (not (= tptp.exposeVersion |tptp.'System_IComparable'|)) (not (= tptp.exposeVersion |tptp.'Microsoft_Contracts_GuardException'|)) (not (= tptp.exposeVersion |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= tptp.exposeVersion |tptp.'System_Collections_IEnumerable'|)) (not (= tptp.exposeVersion |tptp.'System_Reflection_MemberInfo'|)) (not (= tptp.exposeVersion |tptp.'System_Reflection_IReflect'|)) (not (= tptp.exposeVersion |tptp.'System_Exception'|)) (not (= tptp.exposeVersion |tptp.'System_Runtime_InteropServices__Type'|)) (not (= tptp.exposeVersion |tptp.'System_IComparable_1___System_String'|)) (not (= tptp.exposeVersion |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= tptp.exposeVersion |tptp.'System_IEquatable_1___System_String'|)) (not (= tptp.exposeVersion |tptp.'ArrayRefCount'|)) (not (= tptp.exposeVersion |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= tptp.exposeVersion |tptp.'System_IConvertible'|)) (not (= tptp.exposeVersion |tptp.'System_Collections_IList'|)) (not (= tptp.exposeVersion |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= tptp.sharingMode |tptp.'SharingMode_Unshared'|)) (not (= tptp.sharingMode |tptp.'SharingMode_LockProtected'|)) (not (= tptp.sharingMode tptp.ownerRef)) (not (= tptp.sharingMode tptp.ownerFrame)) (not (= tptp.sharingMode |tptp.'PeerGroupPlaceholder'|)) (not (= tptp.sharingMode |tptp.'ArrayCategoryValue'|)) (not (= tptp.sharingMode |tptp.'ArrayCategoryInt'|)) (not (= tptp.sharingMode |tptp.'ArrayCategoryRef'|)) (not (= tptp.sharingMode |tptp.'ArrayCategoryNonNullRef'|)) (not (= tptp.sharingMode |tptp.'System_Array'|)) (not (= tptp.sharingMode |tptp.'System_Boolean'|)) (not (= tptp.sharingMode |tptp.'System_Object'|)) (not (= tptp.sharingMode |tptp.'System_Type'|)) (not (= tptp.sharingMode |tptp.'NonNullFieldsAreInitialized'|)) (not (= tptp.sharingMode |tptp.'System_String'|)) (not (= tptp.sharingMode |tptp.'FirstConsistentOwner'|)) (not (= tptp.sharingMode |tptp.'System_SByte'|)) (not (= tptp.sharingMode |tptp.'System_Byte'|)) (not (= tptp.sharingMode |tptp.'System_Int16'|)) (not (= tptp.sharingMode |tptp.'System_UInt16'|)) (not (= tptp.sharingMode |tptp.'System_Int32'|)) (not (= tptp.sharingMode |tptp.'System_UInt32'|)) (not (= tptp.sharingMode |tptp.'System_Int64'|)) (not (= tptp.sharingMode |tptp.'System_UInt64'|)) (not (= tptp.sharingMode |tptp.'System_Char'|)) (not (= tptp.sharingMode |tptp.'System_UIntPtr'|)) (not (= tptp.sharingMode |tptp.'System_IntPtr'|)) (not (= tptp.sharingMode |tptp.'ArrayRefCount_a'|)) (not (= tptp.sharingMode |tptp.'ArrayRefCount_count'|)) (not (= tptp.sharingMode |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= tptp.sharingMode |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= tptp.sharingMode |tptp.'System_Collections_ICollection'|)) (not (= tptp.sharingMode |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= tptp.sharingMode |tptp.'System_ICloneable'|)) (not (= tptp.sharingMode |tptp.'System_IComparable'|)) (not (= tptp.sharingMode |tptp.'Microsoft_Contracts_GuardException'|)) (not (= tptp.sharingMode |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= tptp.sharingMode |tptp.'System_Collections_IEnumerable'|)) (not (= tptp.sharingMode |tptp.'System_Reflection_MemberInfo'|)) (not (= tptp.sharingMode |tptp.'System_Reflection_IReflect'|)) (not (= tptp.sharingMode |tptp.'System_Exception'|)) (not (= tptp.sharingMode |tptp.'System_Runtime_InteropServices__Type'|)) (not (= tptp.sharingMode |tptp.'System_IComparable_1___System_String'|)) (not (= tptp.sharingMode |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= tptp.sharingMode |tptp.'System_IEquatable_1___System_String'|)) (not (= tptp.sharingMode |tptp.'ArrayRefCount'|)) (not (= tptp.sharingMode |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= tptp.sharingMode |tptp.'System_IConvertible'|)) (not (= tptp.sharingMode |tptp.'System_Collections_IList'|)) (not (= tptp.sharingMode |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'SharingMode_LockProtected'|)) (not (= |tptp.'SharingMode_Unshared'| tptp.ownerRef)) (not (= |tptp.'SharingMode_Unshared'| tptp.ownerFrame)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'PeerGroupPlaceholder'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'ArrayCategoryValue'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'ArrayCategoryInt'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'ArrayCategoryRef'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'ArrayCategoryNonNullRef'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Array'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Boolean'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Object'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Type'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'NonNullFieldsAreInitialized'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_String'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'FirstConsistentOwner'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_SByte'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Byte'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Int16'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_UInt16'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Int32'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_UInt32'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Int64'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_UInt64'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Char'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_IntPtr'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_ICloneable'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_IComparable'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Exception'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_IConvertible'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'SharingMode_Unshared'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'SharingMode_LockProtected'| tptp.ownerRef)) (not (= |tptp.'SharingMode_LockProtected'| tptp.ownerFrame)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'PeerGroupPlaceholder'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'ArrayCategoryValue'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'ArrayCategoryInt'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'ArrayCategoryRef'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'ArrayCategoryNonNullRef'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Array'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Boolean'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Object'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Type'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'NonNullFieldsAreInitialized'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_String'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'FirstConsistentOwner'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_SByte'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Byte'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Int16'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_UInt16'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Int32'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_UInt32'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Int64'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_UInt64'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Char'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_IntPtr'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_ICloneable'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_IComparable'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Exception'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_IConvertible'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'SharingMode_LockProtected'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= tptp.ownerRef tptp.ownerFrame)) (not (= tptp.ownerRef |tptp.'PeerGroupPlaceholder'|)) (not (= tptp.ownerRef |tptp.'ArrayCategoryValue'|)) (not (= tptp.ownerRef |tptp.'ArrayCategoryInt'|)) (not (= tptp.ownerRef |tptp.'ArrayCategoryRef'|)) (not (= tptp.ownerRef |tptp.'ArrayCategoryNonNullRef'|)) (not (= tptp.ownerRef |tptp.'System_Array'|)) (not (= tptp.ownerRef |tptp.'System_Boolean'|)) (not (= tptp.ownerRef |tptp.'System_Object'|)) (not (= tptp.ownerRef |tptp.'System_Type'|)) (not (= tptp.ownerRef |tptp.'NonNullFieldsAreInitialized'|)) (not (= tptp.ownerRef |tptp.'System_String'|)) (not (= tptp.ownerRef |tptp.'FirstConsistentOwner'|)) (not (= tptp.ownerRef |tptp.'System_SByte'|)) (not (= tptp.ownerRef |tptp.'System_Byte'|)) (not (= tptp.ownerRef |tptp.'System_Int16'|)) (not (= tptp.ownerRef |tptp.'System_UInt16'|)) (not (= tptp.ownerRef |tptp.'System_Int32'|)) (not (= tptp.ownerRef |tptp.'System_UInt32'|)) (not (= tptp.ownerRef |tptp.'System_Int64'|)) (not (= tptp.ownerRef |tptp.'System_UInt64'|)) (not (= tptp.ownerRef |tptp.'System_Char'|)) (not (= tptp.ownerRef |tptp.'System_UIntPtr'|)) (not (= tptp.ownerRef |tptp.'System_IntPtr'|)) (not (= tptp.ownerRef |tptp.'ArrayRefCount_a'|)) (not (= tptp.ownerRef |tptp.'ArrayRefCount_count'|)) (not (= tptp.ownerRef |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= tptp.ownerRef |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= tptp.ownerRef |tptp.'System_Collections_ICollection'|)) (not (= tptp.ownerRef |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= tptp.ownerRef |tptp.'System_ICloneable'|)) (not (= tptp.ownerRef |tptp.'System_IComparable'|)) (not (= tptp.ownerRef |tptp.'Microsoft_Contracts_GuardException'|)) (not (= tptp.ownerRef |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= tptp.ownerRef |tptp.'System_Collections_IEnumerable'|)) (not (= tptp.ownerRef |tptp.'System_Reflection_MemberInfo'|)) (not (= tptp.ownerRef |tptp.'System_Reflection_IReflect'|)) (not (= tptp.ownerRef |tptp.'System_Exception'|)) (not (= tptp.ownerRef |tptp.'System_Runtime_InteropServices__Type'|)) (not (= tptp.ownerRef |tptp.'System_IComparable_1___System_String'|)) (not (= tptp.ownerRef |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= tptp.ownerRef |tptp.'System_IEquatable_1___System_String'|)) (not (= tptp.ownerRef |tptp.'ArrayRefCount'|)) (not (= tptp.ownerRef |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= tptp.ownerRef |tptp.'System_IConvertible'|)) (not (= tptp.ownerRef |tptp.'System_Collections_IList'|)) (not (= tptp.ownerRef |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= tptp.ownerFrame |tptp.'PeerGroupPlaceholder'|)) (not (= tptp.ownerFrame |tptp.'ArrayCategoryValue'|)) (not (= tptp.ownerFrame |tptp.'ArrayCategoryInt'|)) (not (= tptp.ownerFrame |tptp.'ArrayCategoryRef'|)) (not (= tptp.ownerFrame |tptp.'ArrayCategoryNonNullRef'|)) (not (= tptp.ownerFrame |tptp.'System_Array'|)) (not (= tptp.ownerFrame |tptp.'System_Boolean'|)) (not (= tptp.ownerFrame |tptp.'System_Object'|)) (not (= tptp.ownerFrame |tptp.'System_Type'|)) (not (= tptp.ownerFrame |tptp.'NonNullFieldsAreInitialized'|)) (not (= tptp.ownerFrame |tptp.'System_String'|)) (not (= tptp.ownerFrame |tptp.'FirstConsistentOwner'|)) (not (= tptp.ownerFrame |tptp.'System_SByte'|)) (not (= tptp.ownerFrame |tptp.'System_Byte'|)) (not (= tptp.ownerFrame |tptp.'System_Int16'|)) (not (= tptp.ownerFrame |tptp.'System_UInt16'|)) (not (= tptp.ownerFrame |tptp.'System_Int32'|)) (not (= tptp.ownerFrame |tptp.'System_UInt32'|)) (not (= tptp.ownerFrame |tptp.'System_Int64'|)) (not (= tptp.ownerFrame |tptp.'System_UInt64'|)) (not (= tptp.ownerFrame |tptp.'System_Char'|)) (not (= tptp.ownerFrame |tptp.'System_UIntPtr'|)) (not (= tptp.ownerFrame |tptp.'System_IntPtr'|)) (not (= tptp.ownerFrame |tptp.'ArrayRefCount_a'|)) (not (= tptp.ownerFrame |tptp.'ArrayRefCount_count'|)) (not (= tptp.ownerFrame |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= tptp.ownerFrame |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= tptp.ownerFrame |tptp.'System_Collections_ICollection'|)) (not (= tptp.ownerFrame |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= tptp.ownerFrame |tptp.'System_ICloneable'|)) (not (= tptp.ownerFrame |tptp.'System_IComparable'|)) (not (= tptp.ownerFrame |tptp.'Microsoft_Contracts_GuardException'|)) (not (= tptp.ownerFrame |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= tptp.ownerFrame |tptp.'System_Collections_IEnumerable'|)) (not (= tptp.ownerFrame |tptp.'System_Reflection_MemberInfo'|)) (not (= tptp.ownerFrame |tptp.'System_Reflection_IReflect'|)) (not (= tptp.ownerFrame |tptp.'System_Exception'|)) (not (= tptp.ownerFrame |tptp.'System_Runtime_InteropServices__Type'|)) (not (= tptp.ownerFrame |tptp.'System_IComparable_1___System_String'|)) (not (= tptp.ownerFrame |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= tptp.ownerFrame |tptp.'System_IEquatable_1___System_String'|)) (not (= tptp.ownerFrame |tptp.'ArrayRefCount'|)) (not (= tptp.ownerFrame |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= tptp.ownerFrame |tptp.'System_IConvertible'|)) (not (= tptp.ownerFrame |tptp.'System_Collections_IList'|)) (not (= tptp.ownerFrame |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'ArrayCategoryValue'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'ArrayCategoryInt'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'ArrayCategoryRef'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'ArrayCategoryNonNullRef'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Array'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Boolean'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Object'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Type'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'NonNullFieldsAreInitialized'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_String'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'FirstConsistentOwner'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_SByte'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Byte'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Int16'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_UInt16'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Int32'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_UInt32'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Int64'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_UInt64'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Char'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_IntPtr'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_ICloneable'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_IComparable'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Exception'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_IConvertible'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'PeerGroupPlaceholder'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'ArrayCategoryInt'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'ArrayCategoryRef'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'ArrayCategoryNonNullRef'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Array'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Boolean'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Object'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Type'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'NonNullFieldsAreInitialized'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_String'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'FirstConsistentOwner'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_SByte'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Byte'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Int16'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_UInt16'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Int32'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_UInt32'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Int64'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_UInt64'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Char'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_IntPtr'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_ICloneable'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_IComparable'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Exception'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_IConvertible'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'ArrayCategoryValue'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'ArrayCategoryRef'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'ArrayCategoryNonNullRef'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Array'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Boolean'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Object'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Type'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'NonNullFieldsAreInitialized'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_String'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'FirstConsistentOwner'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_SByte'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Byte'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Int16'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_UInt16'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Int32'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_UInt32'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Int64'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_UInt64'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Char'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_IntPtr'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_ICloneable'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_IComparable'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Exception'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_IConvertible'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'ArrayCategoryInt'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'ArrayCategoryNonNullRef'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Array'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Boolean'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Object'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Type'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'NonNullFieldsAreInitialized'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_String'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'FirstConsistentOwner'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_SByte'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Byte'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Int16'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_UInt16'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Int32'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_UInt32'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Int64'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_UInt64'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Char'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_IntPtr'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_ICloneable'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_IComparable'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Exception'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_IConvertible'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'ArrayCategoryRef'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Array'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Boolean'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Object'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Type'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'NonNullFieldsAreInitialized'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_String'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'FirstConsistentOwner'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_SByte'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Byte'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Int16'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_UInt16'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Int32'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_UInt32'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Int64'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_UInt64'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Char'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_IntPtr'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_ICloneable'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_IComparable'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Exception'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_IConvertible'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'ArrayCategoryNonNullRef'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Array'| |tptp.'System_Boolean'|)) (not (= |tptp.'System_Array'| |tptp.'System_Object'|)) (not (= |tptp.'System_Array'| |tptp.'System_Type'|)) (not (= |tptp.'System_Array'| |tptp.'NonNullFieldsAreInitialized'|)) (not (= |tptp.'System_Array'| |tptp.'System_String'|)) (not (= |tptp.'System_Array'| |tptp.'FirstConsistentOwner'|)) (not (= |tptp.'System_Array'| |tptp.'System_SByte'|)) (not (= |tptp.'System_Array'| |tptp.'System_Byte'|)) (not (= |tptp.'System_Array'| |tptp.'System_Int16'|)) (not (= |tptp.'System_Array'| |tptp.'System_UInt16'|)) (not (= |tptp.'System_Array'| |tptp.'System_Int32'|)) (not (= |tptp.'System_Array'| |tptp.'System_UInt32'|)) (not (= |tptp.'System_Array'| |tptp.'System_Int64'|)) (not (= |tptp.'System_Array'| |tptp.'System_UInt64'|)) (not (= |tptp.'System_Array'| |tptp.'System_Char'|)) (not (= |tptp.'System_Array'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'System_Array'| |tptp.'System_IntPtr'|)) (not (= |tptp.'System_Array'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'System_Array'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'System_Array'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'System_Array'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'System_Array'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_Array'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_Array'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_Array'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_Array'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_Array'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_Array'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_Array'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_Array'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_Array'| |tptp.'System_Exception'|)) (not (= |tptp.'System_Array'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_Array'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Array'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Array'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Array'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Array'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Array'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Array'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Array'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Object'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Type'|)) (not (= |tptp.'System_Boolean'| |tptp.'NonNullFieldsAreInitialized'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_String'|)) (not (= |tptp.'System_Boolean'| |tptp.'FirstConsistentOwner'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_SByte'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Byte'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Int16'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_UInt16'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Int32'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_UInt32'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Int64'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_UInt64'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Char'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_IntPtr'|)) (not (= |tptp.'System_Boolean'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'System_Boolean'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_Boolean'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_Boolean'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Exception'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Boolean'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Boolean'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Boolean'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Object'| |tptp.'System_Type'|)) (not (= |tptp.'System_Object'| |tptp.'NonNullFieldsAreInitialized'|)) (not (= |tptp.'System_Object'| |tptp.'System_String'|)) (not (= |tptp.'System_Object'| |tptp.'FirstConsistentOwner'|)) (not (= |tptp.'System_Object'| |tptp.'System_SByte'|)) (not (= |tptp.'System_Object'| |tptp.'System_Byte'|)) (not (= |tptp.'System_Object'| |tptp.'System_Int16'|)) (not (= |tptp.'System_Object'| |tptp.'System_UInt16'|)) (not (= |tptp.'System_Object'| |tptp.'System_Int32'|)) (not (= |tptp.'System_Object'| |tptp.'System_UInt32'|)) (not (= |tptp.'System_Object'| |tptp.'System_Int64'|)) (not (= |tptp.'System_Object'| |tptp.'System_UInt64'|)) (not (= |tptp.'System_Object'| |tptp.'System_Char'|)) (not (= |tptp.'System_Object'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'System_Object'| |tptp.'System_IntPtr'|)) (not (= |tptp.'System_Object'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'System_Object'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'System_Object'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'System_Object'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'System_Object'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_Object'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_Object'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_Object'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_Object'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_Object'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_Object'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_Object'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_Object'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_Object'| |tptp.'System_Exception'|)) (not (= |tptp.'System_Object'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_Object'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Object'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Object'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Object'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Object'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Object'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Object'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Object'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Type'| |tptp.'NonNullFieldsAreInitialized'|)) (not (= |tptp.'System_Type'| |tptp.'System_String'|)) (not (= |tptp.'System_Type'| |tptp.'FirstConsistentOwner'|)) (not (= |tptp.'System_Type'| |tptp.'System_SByte'|)) (not (= |tptp.'System_Type'| |tptp.'System_Byte'|)) (not (= |tptp.'System_Type'| |tptp.'System_Int16'|)) (not (= |tptp.'System_Type'| |tptp.'System_UInt16'|)) (not (= |tptp.'System_Type'| |tptp.'System_Int32'|)) (not (= |tptp.'System_Type'| |tptp.'System_UInt32'|)) (not (= |tptp.'System_Type'| |tptp.'System_Int64'|)) (not (= |tptp.'System_Type'| |tptp.'System_UInt64'|)) (not (= |tptp.'System_Type'| |tptp.'System_Char'|)) (not (= |tptp.'System_Type'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'System_Type'| |tptp.'System_IntPtr'|)) (not (= |tptp.'System_Type'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'System_Type'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'System_Type'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'System_Type'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'System_Type'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_Type'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_Type'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_Type'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_Type'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_Type'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_Type'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_Type'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_Type'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_Type'| |tptp.'System_Exception'|)) (not (= |tptp.'System_Type'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_Type'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Type'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Type'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Type'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Type'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Type'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Type'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Type'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_String'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'FirstConsistentOwner'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_SByte'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_Byte'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_Int16'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_UInt16'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_Int32'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_UInt32'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_Int64'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_UInt64'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_Char'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_IntPtr'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_ICloneable'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_IComparable'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_Exception'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_IConvertible'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'NonNullFieldsAreInitialized'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_String'| |tptp.'FirstConsistentOwner'|)) (not (= |tptp.'System_String'| |tptp.'System_SByte'|)) (not (= |tptp.'System_String'| |tptp.'System_Byte'|)) (not (= |tptp.'System_String'| |tptp.'System_Int16'|)) (not (= |tptp.'System_String'| |tptp.'System_UInt16'|)) (not (= |tptp.'System_String'| |tptp.'System_Int32'|)) (not (= |tptp.'System_String'| |tptp.'System_UInt32'|)) (not (= |tptp.'System_String'| |tptp.'System_Int64'|)) (not (= |tptp.'System_String'| |tptp.'System_UInt64'|)) (not (= |tptp.'System_String'| |tptp.'System_Char'|)) (not (= |tptp.'System_String'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'System_String'| |tptp.'System_IntPtr'|)) (not (= |tptp.'System_String'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'System_String'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'System_String'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'System_String'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'System_String'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_String'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_String'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_String'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_String'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_String'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_String'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_String'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_String'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_String'| |tptp.'System_Exception'|)) (not (= |tptp.'System_String'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_String'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_String'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_String'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_String'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_String'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_String'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_String'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_String'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_SByte'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_Byte'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_Int16'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_UInt16'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_Int32'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_UInt32'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_Int64'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_UInt64'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_Char'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_IntPtr'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_ICloneable'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_IComparable'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_Exception'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_IConvertible'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'FirstConsistentOwner'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_SByte'| |tptp.'System_Byte'|)) (not (= |tptp.'System_SByte'| |tptp.'System_Int16'|)) (not (= |tptp.'System_SByte'| |tptp.'System_UInt16'|)) (not (= |tptp.'System_SByte'| |tptp.'System_Int32'|)) (not (= |tptp.'System_SByte'| |tptp.'System_UInt32'|)) (not (= |tptp.'System_SByte'| |tptp.'System_Int64'|)) (not (= |tptp.'System_SByte'| |tptp.'System_UInt64'|)) (not (= |tptp.'System_SByte'| |tptp.'System_Char'|)) (not (= |tptp.'System_SByte'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'System_SByte'| |tptp.'System_IntPtr'|)) (not (= |tptp.'System_SByte'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'System_SByte'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'System_SByte'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'System_SByte'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'System_SByte'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_SByte'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_SByte'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_SByte'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_SByte'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_SByte'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_SByte'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_SByte'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_SByte'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_SByte'| |tptp.'System_Exception'|)) (not (= |tptp.'System_SByte'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_SByte'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_SByte'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_SByte'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_SByte'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_SByte'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_SByte'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_SByte'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_SByte'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Byte'| |tptp.'System_Int16'|)) (not (= |tptp.'System_Byte'| |tptp.'System_UInt16'|)) (not (= |tptp.'System_Byte'| |tptp.'System_Int32'|)) (not (= |tptp.'System_Byte'| |tptp.'System_UInt32'|)) (not (= |tptp.'System_Byte'| |tptp.'System_Int64'|)) (not (= |tptp.'System_Byte'| |tptp.'System_UInt64'|)) (not (= |tptp.'System_Byte'| |tptp.'System_Char'|)) (not (= |tptp.'System_Byte'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'System_Byte'| |tptp.'System_IntPtr'|)) (not (= |tptp.'System_Byte'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'System_Byte'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'System_Byte'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'System_Byte'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'System_Byte'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_Byte'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_Byte'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_Byte'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_Byte'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_Byte'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_Byte'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_Byte'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_Byte'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_Byte'| |tptp.'System_Exception'|)) (not (= |tptp.'System_Byte'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_Byte'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Byte'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Byte'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Byte'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Byte'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Byte'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Byte'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Byte'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Int16'| |tptp.'System_UInt16'|)) (not (= |tptp.'System_Int16'| |tptp.'System_Int32'|)) (not (= |tptp.'System_Int16'| |tptp.'System_UInt32'|)) (not (= |tptp.'System_Int16'| |tptp.'System_Int64'|)) (not (= |tptp.'System_Int16'| |tptp.'System_UInt64'|)) (not (= |tptp.'System_Int16'| |tptp.'System_Char'|)) (not (= |tptp.'System_Int16'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'System_Int16'| |tptp.'System_IntPtr'|)) (not (= |tptp.'System_Int16'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'System_Int16'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'System_Int16'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'System_Int16'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'System_Int16'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_Int16'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_Int16'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_Int16'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_Int16'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_Int16'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_Int16'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_Int16'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_Int16'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_Int16'| |tptp.'System_Exception'|)) (not (= |tptp.'System_Int16'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_Int16'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Int16'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Int16'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Int16'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Int16'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Int16'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Int16'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Int16'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_Int32'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_UInt32'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_Int64'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_UInt64'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_Char'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_IntPtr'|)) (not (= |tptp.'System_UInt16'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'System_UInt16'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_UInt16'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_UInt16'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_Exception'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_UInt16'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_UInt16'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_UInt16'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Int32'| |tptp.'System_UInt32'|)) (not (= |tptp.'System_Int32'| |tptp.'System_Int64'|)) (not (= |tptp.'System_Int32'| |tptp.'System_UInt64'|)) (not (= |tptp.'System_Int32'| |tptp.'System_Char'|)) (not (= |tptp.'System_Int32'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'System_Int32'| |tptp.'System_IntPtr'|)) (not (= |tptp.'System_Int32'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'System_Int32'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'System_Int32'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'System_Int32'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'System_Int32'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_Int32'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_Int32'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_Int32'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_Int32'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_Int32'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_Int32'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_Int32'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_Int32'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_Int32'| |tptp.'System_Exception'|)) (not (= |tptp.'System_Int32'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_Int32'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Int32'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Int32'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Int32'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Int32'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Int32'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Int32'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Int32'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_Int64'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_UInt64'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_Char'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_IntPtr'|)) (not (= |tptp.'System_UInt32'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'System_UInt32'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_UInt32'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_UInt32'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_Exception'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_UInt32'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_UInt32'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_UInt32'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Int64'| |tptp.'System_UInt64'|)) (not (= |tptp.'System_Int64'| |tptp.'System_Char'|)) (not (= |tptp.'System_Int64'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'System_Int64'| |tptp.'System_IntPtr'|)) (not (= |tptp.'System_Int64'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'System_Int64'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'System_Int64'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'System_Int64'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'System_Int64'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_Int64'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_Int64'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_Int64'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_Int64'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_Int64'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_Int64'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_Int64'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_Int64'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_Int64'| |tptp.'System_Exception'|)) (not (= |tptp.'System_Int64'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_Int64'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Int64'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Int64'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Int64'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Int64'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Int64'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Int64'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Int64'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_Char'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_IntPtr'|)) (not (= |tptp.'System_UInt64'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'System_UInt64'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_UInt64'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_UInt64'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_Exception'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_UInt64'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_UInt64'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_UInt64'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Char'| |tptp.'System_UIntPtr'|)) (not (= |tptp.'System_Char'| |tptp.'System_IntPtr'|)) (not (= |tptp.'System_Char'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'System_Char'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'System_Char'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'System_Char'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'System_Char'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_Char'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_Char'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_Char'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_Char'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_Char'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_Char'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_Char'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_Char'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_Char'| |tptp.'System_Exception'|)) (not (= |tptp.'System_Char'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_Char'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Char'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Char'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Char'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Char'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Char'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Char'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Char'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_IntPtr'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_Exception'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_UIntPtr'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_IntPtr'| |tptp.'ArrayRefCount_a'|)) (not (= |tptp.'System_IntPtr'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'System_IntPtr'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'System_IntPtr'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'System_IntPtr'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_IntPtr'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_IntPtr'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_IntPtr'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_IntPtr'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_IntPtr'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_IntPtr'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_IntPtr'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_IntPtr'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_IntPtr'| |tptp.'System_Exception'|)) (not (= |tptp.'System_IntPtr'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_IntPtr'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_IntPtr'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_IntPtr'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_IntPtr'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_IntPtr'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_IntPtr'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_IntPtr'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_IntPtr'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'ArrayRefCount_count'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'System_ICloneable'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'System_IComparable'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'System_Exception'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'System_IConvertible'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'ArrayRefCount_a'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'System_ICloneable'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'System_IComparable'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'System_Exception'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'System_IConvertible'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'ArrayRefCount_count'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_Exception'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'System_Collections_ICollection'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'System_Exception'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'System_Exception'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Collections_ICollection'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'System_ICloneable'|)) (not (= |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'System_Exception'|)) (not (= |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_ICloneable'| |tptp.'System_IComparable'|)) (not (= |tptp.'System_ICloneable'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_ICloneable'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_ICloneable'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_ICloneable'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_ICloneable'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_ICloneable'| |tptp.'System_Exception'|)) (not (= |tptp.'System_ICloneable'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_ICloneable'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_ICloneable'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_ICloneable'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_ICloneable'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_ICloneable'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_ICloneable'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_ICloneable'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_ICloneable'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_IComparable'| |tptp.'Microsoft_Contracts_GuardException'|)) (not (= |tptp.'System_IComparable'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'System_IComparable'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'System_IComparable'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_IComparable'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_IComparable'| |tptp.'System_Exception'|)) (not (= |tptp.'System_IComparable'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_IComparable'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_IComparable'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_IComparable'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_IComparable'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_IComparable'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_IComparable'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_IComparable'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_IComparable'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'Microsoft_Contracts_GuardException'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (= |tptp.'Microsoft_Contracts_GuardException'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'Microsoft_Contracts_GuardException'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'Microsoft_Contracts_GuardException'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'Microsoft_Contracts_GuardException'| |tptp.'System_Exception'|)) (not (= |tptp.'Microsoft_Contracts_GuardException'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'Microsoft_Contracts_GuardException'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'Microsoft_Contracts_GuardException'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'Microsoft_Contracts_GuardException'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'Microsoft_Contracts_GuardException'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'Microsoft_Contracts_GuardException'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'Microsoft_Contracts_GuardException'| |tptp.'System_IConvertible'|)) (not (= |tptp.'Microsoft_Contracts_GuardException'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'Microsoft_Contracts_GuardException'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'Microsoft_Contracts_ObjectInvariantException'| |tptp.'System_Collections_IEnumerable'|)) (not (= |tptp.'Microsoft_Contracts_ObjectInvariantException'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'Microsoft_Contracts_ObjectInvariantException'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'Microsoft_Contracts_ObjectInvariantException'| |tptp.'System_Exception'|)) (not (= |tptp.'Microsoft_Contracts_ObjectInvariantException'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'Microsoft_Contracts_ObjectInvariantException'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'Microsoft_Contracts_ObjectInvariantException'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'Microsoft_Contracts_ObjectInvariantException'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'Microsoft_Contracts_ObjectInvariantException'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'Microsoft_Contracts_ObjectInvariantException'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'Microsoft_Contracts_ObjectInvariantException'| |tptp.'System_IConvertible'|)) (not (= |tptp.'Microsoft_Contracts_ObjectInvariantException'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'Microsoft_Contracts_ObjectInvariantException'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Collections_IEnumerable'| |tptp.'System_Reflection_MemberInfo'|)) (not (= |tptp.'System_Collections_IEnumerable'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_Collections_IEnumerable'| |tptp.'System_Exception'|)) (not (= |tptp.'System_Collections_IEnumerable'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_Collections_IEnumerable'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Collections_IEnumerable'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Collections_IEnumerable'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Collections_IEnumerable'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Collections_IEnumerable'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Collections_IEnumerable'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Collections_IEnumerable'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Collections_IEnumerable'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Reflection_MemberInfo'| |tptp.'System_Reflection_IReflect'|)) (not (= |tptp.'System_Reflection_MemberInfo'| |tptp.'System_Exception'|)) (not (= |tptp.'System_Reflection_MemberInfo'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_Reflection_MemberInfo'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Reflection_MemberInfo'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Reflection_MemberInfo'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Reflection_MemberInfo'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Reflection_MemberInfo'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Reflection_MemberInfo'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Reflection_MemberInfo'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Reflection_MemberInfo'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Reflection_IReflect'| |tptp.'System_Exception'|)) (not (= |tptp.'System_Reflection_IReflect'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_Reflection_IReflect'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Reflection_IReflect'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Reflection_IReflect'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Reflection_IReflect'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Reflection_IReflect'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Reflection_IReflect'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Reflection_IReflect'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Reflection_IReflect'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Exception'| |tptp.'System_Runtime_InteropServices__Type'|)) (not (= |tptp.'System_Exception'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Exception'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Exception'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Exception'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Exception'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Exception'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Exception'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Exception'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Runtime_InteropServices__Type'| |tptp.'System_IComparable_1___System_String'|)) (not (= |tptp.'System_Runtime_InteropServices__Type'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_Runtime_InteropServices__Type'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_Runtime_InteropServices__Type'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_Runtime_InteropServices__Type'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_Runtime_InteropServices__Type'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Runtime_InteropServices__Type'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Runtime_InteropServices__Type'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_IComparable_1___System_String'| |tptp.'Microsoft_Contracts_ICheckedException'|)) (not (= |tptp.'System_IComparable_1___System_String'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'System_IComparable_1___System_String'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_IComparable_1___System_String'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_IComparable_1___System_String'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_IComparable_1___System_String'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_IComparable_1___System_String'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'Microsoft_Contracts_ICheckedException'| |tptp.'System_IEquatable_1___System_String'|)) (not (= |tptp.'Microsoft_Contracts_ICheckedException'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'Microsoft_Contracts_ICheckedException'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'Microsoft_Contracts_ICheckedException'| |tptp.'System_IConvertible'|)) (not (= |tptp.'Microsoft_Contracts_ICheckedException'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'Microsoft_Contracts_ICheckedException'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_IEquatable_1___System_String'| |tptp.'ArrayRefCount'|)) (not (= |tptp.'System_IEquatable_1___System_String'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'System_IEquatable_1___System_String'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_IEquatable_1___System_String'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_IEquatable_1___System_String'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'ArrayRefCount'| |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= |tptp.'ArrayRefCount'| |tptp.'System_IConvertible'|)) (not (= |tptp.'ArrayRefCount'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'ArrayRefCount'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Runtime_Serialization_ISerializable'| |tptp.'System_IConvertible'|)) (not (= |tptp.'System_Runtime_Serialization_ISerializable'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_Runtime_Serialization_ISerializable'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_IConvertible'| |tptp.'System_Collections_IList'|)) (not (= |tptp.'System_IConvertible'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= |tptp.'System_Collections_IList'| |tptp.'System_Runtime_InteropServices__MemberInfo'|)))) (not (= (|tptp.'DeclType'| tptp.elements) |tptp.'System_Object'|)) (not (= (|tptp.'DeclType'| tptp.exposeVersion) |tptp.'System_Object'|)) (not (forall (@list @t71) (= (|tptp.'ClassReprInv'| @t169) @t71))) (not (forall @t179 (not (= (tptp.x (tptp.typeof @t250) |tptp.'System_Object'|) tptp.true_1)))) (not (forall @t179 (not (= @t250 tptp.nullObject)))) (not (forall (@list @t149 @t66) (=> @t132 (= (tptp.select2 @t66 @t250 tptp.ownerFrame) |tptp.'PeerGroupPlaceholder'|)))) (not (= (|tptp.'IncludeInMainFrameCondition'| tptp.allocated) tptp.true_1)) (not (= (|tptp.'IncludeInMainFrameCondition'| tptp.elements) tptp.true_1)) (not (not (= (|tptp.'IncludeInMainFrameCondition'| tptp.inv) tptp.true_1))) (not (not (= (|tptp.'IncludeInMainFrameCondition'| tptp.localinv) tptp.true_1))) (not (= (|tptp.'IncludeInMainFrameCondition'| tptp.ownerRef) tptp.true_1)) (not (= (|tptp.'IncludeInMainFrameCondition'| tptp.ownerFrame) tptp.true_1)) (not (= (|tptp.'IncludeInMainFrameCondition'| tptp.exposeVersion) tptp.true_1)) (not (not (= (|tptp.'IncludeInMainFrameCondition'| |tptp.'FirstConsistentOwner'|) tptp.true_1))) (not (not (= (|tptp.'IsStaticField'| tptp.allocated) tptp.true_1))) (not (not (= (|tptp.'IsStaticField'| tptp.elements) tptp.true_1))) (not (not (= (|tptp.'IsStaticField'| tptp.inv) tptp.true_1))) (not (not (= (|tptp.'IsStaticField'| tptp.localinv) tptp.true_1))) (not (not (= (|tptp.'IsStaticField'| tptp.exposeVersion) tptp.true_1))) (not (not (= (|tptp.'IncludedInModifiesStar'| tptp.ownerRef) tptp.true_1))) (not (not (= (|tptp.'IncludedInModifiesStar'| tptp.ownerFrame) tptp.true_1))) (not (= (|tptp.'IncludedInModifiesStar'| tptp.exposeVersion) tptp.true_1)) (not (= (|tptp.'IncludedInModifiesStar'| tptp.elements) tptp.true_1)) (not (forall @t247 (= (|tptp.'ValueArrayGet'| @t249 @t22) @t7))) (not (forall @t246 (=> @t24 (= (|tptp.'ValueArrayGet'| @t249 @t21) (|tptp.'ValueArrayGet'| @t15 @t21))))) (not (forall @t247 (= (|tptp.'IntArrayGet'| @t248 @t22) @t7))) (not (forall @t246 (=> @t24 (= (|tptp.'IntArrayGet'| @t248 @t21) (|tptp.'IntArrayGet'| @t15 @t21))))) (not (forall @t247 (= (|tptp.'RefArrayGet'| @t245 @t22) @t7))) (not (forall @t246 (=> @t24 (= (|tptp.'RefArrayGet'| @t245 @t21) (|tptp.'RefArrayGet'| @t15 @t21))))) (not (forall @t244 (= (|tptp.'ArrayIndexInvX'| @t243) @t7))) (not (forall @t244 (= (|tptp.'ArrayIndexInvY'| @t243) @t6))) (not (forall @t196 (=> @t118 (= (|tptp.'InRange'| (|tptp.'IntArrayGet'| @t194 @t22) @t241) tptp.true_1)))) (not (forall @t196 (exists (@list @t242) (and (= @t242 @t195) (=> (not (or @t191 (not (not (= @t242 tptp.nullObject))))) (= (tptp.x (tptp.typeof @t242) @t241) tptp.true_1)))))) (not (forall (@list @t67 @t149 @t22 @t199 @t117) (=> (not (or @t191 @t240)) (not (= @t195 tptp.nullObject))))) (not (forall @t236 (<= 1 @t235))) (not (forall @t239 (=> (not (or @t69 (not (= (tptp.x @t189 @t217) tptp.true_1)))) @t238))) (not (forall @t239 (=> (not (or @t69 @t240)) @t238))) (not (forall @t239 (=> (not (or @t69 (not (= (tptp.x @t189 @t228) tptp.true_1)))) @t238))) (not (forall @t239 (=> (not (or @t69 (not (= (tptp.x @t189 @t226) tptp.true_1)))) @t238))) (not (forall @t236 (exists (@list @t237) (and (= @t237 @t234) (not (or (not (<= 0 @t237)) (not (<= @t237 tptp.int_2147483647)))))))) (not (forall @t233 (<= 0 @t232))) (not (forall @t236 (=> (= @t235 1) (= (|tptp.'DimLength'| @t67 0) @t234)))) (not (forall @t233 (= (|tptp.'LBound'| @t67 @t22) 0))) (not (forall @t233 (= (|tptp.'UBound'| @t67 @t22) (- @t232 1)))) (not (forall @t231 (=> (= (tptp.x @t149 (|tptp.'ValueArray'| @t230 @t199)) tptp.true_1) (= @t229 |tptp.'ArrayCategoryValue'|)))) (not (forall @t231 (=> (= (tptp.x @t149 (|tptp.'IntArray'| @t230 @t199)) tptp.true_1) (= @t229 |tptp.'ArrayCategoryInt'|)))) (not (forall @t231 (=> (= (tptp.x @t149 (|tptp.'RefArray'| @t230 @t199)) tptp.true_1) (= @t229 |tptp.'ArrayCategoryRef'|)))) (not (forall @t231 (=> (= (tptp.x @t149 (|tptp.'NonNullRefArray'| @t230 @t199)) tptp.true_1) (= @t229 |tptp.'ArrayCategoryNonNullRef'|)))) (not (= (tptp.x |tptp.'System_Array'| |tptp.'System_Object'|) tptp.true_1)) (not (forall @t223 (exists (@list @t227) (and (= @t227 @t228) (not (or (not (= (tptp.x @t227 @t227) tptp.true_1)) (not (= (tptp.x @t227 |tptp.'System_Array'|) tptp.true_1)))))))) (not (forall @t223 (exists (@list @t225) (and (= @t225 @t226) (not (or (not (= (tptp.x @t225 @t225) tptp.true_1)) (not (= (tptp.x @t225 |tptp.'System_Array'|) tptp.true_1)))))))) (not (forall @t223 (exists (@list @t224) (and (= @t224 @t217) (not (or (not (= (tptp.x @t224 @t224) tptp.true_1)) (not (= (tptp.x @t224 |tptp.'System_Array'|) tptp.true_1)))))))) (not (forall @t223 (exists (@list @t222) (and (= @t222 @t215) (not (or (not (= (tptp.x @t222 @t222) tptp.true_1)) (not (= (tptp.x @t222 |tptp.'System_Array'|) tptp.true_1)))))))) (not (forall (@list @t221 @t219 @t220) (exists (@list @t218) (and (= @t218 (tptp.typeof @t221)) (=> (= (|tptp.'NonNullRefArrayRaw'| @t221 @t219 @t220) tptp.true_1) (not (or (not (= (tptp.x @t218 |tptp.'System_Array'|) tptp.true_1)) (not (= (|tptp.'Rank'| @t221) @t220)) (not (= (tptp.x @t219 (|tptp.'ElementType'| @t218)) tptp.true_1))))))))) (not (forall @t216 (=> @t181 (= (tptp.x (|tptp.'RefArray'| @t161 @t199) @t217) tptp.true_1)))) (not (forall @t216 (=> @t181 (= (tptp.x (|tptp.'NonNullRefArray'| @t161 @t199) @t215) tptp.true_1)))) (not (forall @t214 (= (|tptp.'ElementType'| @t203) @t15))) (not (forall @t214 (= (|tptp.'ElementType'| @t200) @t15))) (not (forall @t214 (= (|tptp.'ElementType'| @t208) @t15))) (not (forall @t214 (= (|tptp.'ElementType'| @t205) @t15))) (not (forall @t201 (exists (@list @t213) (and (= @t213 @t206) (=> (= (tptp.x @t149 @t208) tptp.true_1) (not (or @t212 (not (= @t149 (|tptp.'RefArray'| @t213 @t199))) (not (= (tptp.x @t213 @t15) tptp.true_1))))))))) (not (forall @t201 (exists (@list @t211) (and (= @t211 @t206) (=> (= (tptp.x @t149 @t205) tptp.true_1) (not (or @t212 (not (= @t149 (|tptp.'NonNullRefArray'| @t211 @t199))) (not (= (tptp.x @t211 @t15) tptp.true_1))))))))) (not (forall @t201 (exists (@list @t210) (and (= @t210 @t203) (=> (= (tptp.x @t149 @t210) tptp.true_1) (= @t149 @t210)))))) (not (forall @t201 (exists (@list @t209) (and (= @t209 @t200) (=> (= (tptp.x @t149 @t209) tptp.true_1) (= @t149 @t209)))))) (not (forall @t201 (exists (@list @t207) (and (= @t207 @t206) (=> (= (tptp.x @t208 @t149) tptp.true_1) (or @t198 (not (or (not (= @t149 (|tptp.'RefArray'| @t207 @t199))) (not (= (tptp.x @t15 @t207) tptp.true_1)))))))))) (not (forall @t201 (exists (@list @t204) (and (= @t204 @t206) (=> (= (tptp.x @t205 @t149) tptp.true_1) (or @t198 (not (or (not (= @t149 (|tptp.'NonNullRefArray'| @t204 @t199))) (not (= (tptp.x @t15 @t204) tptp.true_1)))))))))) (not (forall @t201 (exists (@list @t202) (and (= @t202 @t203) (=> (= (tptp.x @t202 @t149) tptp.true_1) (or @t198 (= @t149 @t202))))))) (not (forall @t201 (exists (@list @t197) (and (= @t197 @t200) (=> (= (tptp.x @t197 @t149) tptp.true_1) (or @t198 (= @t149 @t197))))))) (not (forall @t196 (exists (@list @t192 @t193) (and (= @t192 @t188) (= @t193 @t195) (=> (not (or @t191 @t190)) (or (= @t193 tptp.nullObject) (= (|tptp.'IsImmutable'| (tptp.typeof @t193)) tptp.true_1) (not (or (not (= (tptp.select2 @t117 @t193 tptp.ownerRef) (tptp.select2 @t117 @t192 tptp.ownerRef))) (not (= (tptp.select2 @t117 @t193 tptp.ownerFrame) (tptp.select2 @t117 @t192 tptp.ownerFrame))))))))))) (not (forall (@list @t67 @t117) (=> (not (or @t191 (not (= (|tptp.'IsAllocated'| @t117 @t67) tptp.true_1)) @t190)) (= (|tptp.'IsAllocated'| @t117 @t188) tptp.true_1)))) (not (forall @t187 (= (tptp.typeof (|tptp.'ElementProxy'| @t17 @t186)) |tptp.'System_Object'|))) (not (forall @t187 (= (tptp.typeof (|tptp.'ElementProxyStruct'| @t17 @t186)) |tptp.'System_Object'|))) (not (forall (@list @t156 @t16 @t7) (= (|tptp.'StructGet'| @t185 @t16) @t7))) (not (forall (@list @t156 @t16 @t184 @t7) (=> (not (= @t16 @t184)) (= (|tptp.'StructGet'| @t185 @t184) (|tptp.'StructGet'| @t156 @t184))))) (not (forall @t179 (exists (@list @t183) (and (= @t183 (|tptp.'BaseClass'| @t149)) (not (or (not (= (tptp.x @t149 @t183) tptp.true_1)) (not (=> (not (= @t149 |tptp.'System_Object'|)) (not (= @t149 @t183)))))))))) (not (forall (@list @t15 @t106 @t105) (=> (= (tptp.x @t105 (|tptp.'AsDirectSubClass'| @t106 @t15)) tptp.true_1) (= (|tptp.'OneClassDown'| @t105 @t15) @t106)))) (not (forall @t179 (=> (= (|tptp.'IsValueType'| @t149) tptp.true_1) (not (or (not (forall @t182 (=> (= (tptp.x @t149 @t161) tptp.true_1) @t180))) (not (forall @t182 (=> @t181 @t180)))))))) (not (= (|tptp.'IsValueType'| |tptp.'System_Boolean'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Type'| |tptp.'System_Object'|) tptp.true_1)) (not (forall @t179 (= (|tptp.'IsNotNull'| @t178 |tptp.'System_Type'|) tptp.true_1))) (not (forall @t179 (= (|tptp.'TypeName'| @t178) @t149))) (not (forall @t160 (= @t176 (or @t130 (= (tptp.x @t145 @t149) tptp.true_1))))) (not (forall @t160 (= (= (|tptp.'IsNotNull'| @t17 @t149) tptp.true_1) (not (or @t131 @t177))))) (not (forall @t160 (=> @t176 (= @t175 @t17)))) (not (forall @t160 (=> @t177 (= @t175 tptp.nullObject)))) (not (forall @t146 (exists (@list @t174) (and (= @t174 @t145) (=> (not (or @t133 @t131 (not (= (tptp.x @t174 |tptp.'System_Array'|) tptp.true_1)))) (not (or (not (= @t142 @t174)) (not (= @t141 @t174))))))))) (not (forall @t153 (=> @t173 (= (|tptp.'IsAllocated'| @t66 @t137) tptp.true_1)))) (not (forall @t153 (=> @t173 (= (tptp.select2 @t66 @t137 tptp.allocated) tptp.true_1)))) (not (forall (@list @t66 @t156 @t16) (=> (= (|tptp.'IsAllocated'| @t66 @t156) tptp.true_1) (= (|tptp.'IsAllocated'| @t66 (|tptp.'StructGet'| @t156 @t16)) tptp.true_1)))) (not (forall @t172 (=> @t171 (= (|tptp.'IsAllocated'| @t66 (|tptp.'RefArrayGet'| @t170 @t22)) tptp.true_1)))) (not (forall @t172 (=> @t171 (= (|tptp.'IsAllocated'| @t66 (|tptp.'ValueArrayGet'| @t170 @t22)) tptp.true_1)))) (not (forall @t146 (=> (= (|tptp.'IsAllocated'| @t66 @t17) tptp.true_1) @t128))) (not (forall (@list @t66 @t71) (=> @t132 (= (tptp.select2 @t66 @t169 tptp.allocated) tptp.true_1)))) (not (= (|tptp.'DeclType'| |tptp.'NonNullFieldsAreInitialized'|) |tptp.'System_Object'|)) (not (forall (@list @t16 @t149) (=> (= @t167 @t16) (= @t168 @t16)))) (not (forall @t155 (=> @t132 (= (|tptp.'Is'| (tptp.select2 @t66 @t17 @t168) @t149) tptp.true_1)))) (not (forall @t155 (=> (not (or @t133 @t131 (not (or @t159 (= (= (tptp.select2 @t66 |tptp.'BeingConstructed'| |tptp.'NonNullFieldsAreInitialized'|) tptp.true_1) true))))) (not (= (tptp.select2 @t66 @t17 @t167) tptp.nullObject))))) (not (forall @t155 (=> @t132 (= (|tptp.'InRange'| (tptp.select2 @t66 @t17 (|tptp.'AsRangeField'| @t16 @t149)) @t149) tptp.true_1)))) (not (forall (@list @t17) (not (= (|tptp.'IsMemberlessType'| @t145) tptp.true_1)))) (not (forall (@list @t164 @t156 @t65) (exists (@list @t165 @t166) (and (= @t165 (|tptp.'AsInterface'| @t164)) (= @t166 (|tptp.'Box'| @t156 @t65)) (=> (not (or (not (= @t165 @t164)) (not (= @t166 @t65)) (not (= (tptp.x (|tptp.'UnboxedType'| @t166) @t165) tptp.true_1)))) (= (tptp.x (tptp.typeof @t65) @t164) tptp.true_1)))))) (not (not (= (|tptp.'IsImmutable'| |tptp.'System_Object'|) tptp.true_1))) (not (forall @t163 (=> (= (tptp.x @t161 @t158) tptp.true_1) (not (or @t162 (not (= (|tptp.'AsImmutable'| @t161) @t161))))))) (not (forall @t163 (=> (= (tptp.x @t161 (|tptp.'AsMutable'| @t149)) tptp.true_1) (not (or (not @t162) (not (= (|tptp.'AsMutable'| @t161) @t161))))))) (not (forall @t160 (=> (not (or @t131 (not @t159) (not (= (tptp.x @t145 @t158) tptp.true_1)))) (forall (@list @t66) (exists (@list @t157) (and (= @t157 @t145) (=> @t132 (not (or (not (= @t142 @t157)) (not (= @t141 @t157)) (not (= @t135 |tptp.'PeerGroupPlaceholder'|)) (not (= (|tptp.'AsOwner'| @t17 @t134) @t17)) (not (forall @t5 (=> (= (|tptp.'AsOwner'| @t17 (tptp.select2 @t66 @t2 tptp.ownerRef)) @t17) (or (= @t2 @t17) (not (= (tptp.select2 @t66 @t2 tptp.ownerFrame) |tptp.'PeerGroupPlaceholder'|))))))))))))))) (not (forall (@list @t156) (<= 0 (|tptp.'StringLength'| @t156)))) (not (forall @t155 (exists (@list @t154) (and (= @t154 (tptp.select2 @t66 @t17 (|tptp.'AsRepField'| @t16 @t149))) (=> (not (or @t133 (not (not (= @t154 tptp.nullObject))))) (not (or (not (= (tptp.select2 @t66 @t154 tptp.ownerRef) @t17)) (not (= (tptp.select2 @t66 @t154 tptp.ownerFrame) @t149))))))))) (not (forall @t153 (exists (@list @t152) (and (= @t152 (tptp.select2 @t66 @t17 (|tptp.'AsPeerField'| @t16))) (=> (not (or @t133 (not (not (= @t152 tptp.nullObject))))) (not (or (not (= (tptp.select2 @t66 @t152 tptp.ownerRef) @t134)) (not (= (tptp.select2 @t66 @t152 tptp.ownerFrame) @t135))))))))) (not (forall (@list @t66 @t17 @t16 @t149 @t22) (exists (@list @t151) (and (= @t151 (tptp.select2 @t66 @t17 (|tptp.'AsElementsRepField'| @t16 @t149 @t22))) (exists (@list @t150) (and (= @t150 (|tptp.'ElementProxy'| @t151 @t22)) (=> (not (or @t133 (not (not (= @t151 tptp.nullObject))))) (not (or (not (= (tptp.select2 @t66 @t150 tptp.ownerRef) @t17)) (not (= (tptp.select2 @t66 @t150 tptp.ownerFrame) @t149))))))))))) (not (forall (@list @t66 @t17 @t16 @t22) (exists (@list @t148) (and (= @t148 (tptp.select2 @t66 @t17 (|tptp.'AsElementsPeerField'| @t16 @t22))) (exists (@list @t147) (and (= @t147 (|tptp.'ElementProxy'| @t148 @t22)) (=> (not (or @t133 (not (not (= @t148 tptp.nullObject))))) (not (or (not (= (tptp.select2 @t66 @t147 tptp.ownerRef) @t134)) (not (= (tptp.select2 @t66 @t147 tptp.ownerFrame) @t135))))))))))) (not (forall @t146 (exists (@list @t140 @t143 @t144) (and (= @t140 @t145) (= @t143 @t135) (= @t144 @t134) (=> (not (or @t133 (not (not (= @t143 |tptp.'PeerGroupPlaceholder'|))) (not (= (tptp.x (tptp.select2 @t66 @t144 tptp.inv) @t143) tptp.true_1)) (not (not (= (tptp.select2 @t66 @t144 tptp.localinv) (|tptp.'BaseClass'| @t143)))))) (not (or (not (= @t142 @t140)) (not (= @t141 @t140))))))))) (not (forall (@list @t17 @t16 @t66) (exists (@list @t138 @t139) (and (= @t138 @t135) (= @t139 @t134) (=> (not (or @t133 @t131 @t129 (not (= (|tptp.'AsPureObject'| @t17) @t17)) (not (not (= @t138 |tptp.'PeerGroupPlaceholder'|))) (not (= (tptp.x (tptp.select2 @t66 @t139 tptp.inv) @t138) tptp.true_1)) (not (not (= (tptp.select2 @t66 @t139 tptp.localinv) (|tptp.'BaseClass'| @t138)))))) (= @t137 (|tptp.'FieldDependsOnFCO'| @t17 @t16 (tptp.select2 @t66 @t136 tptp.exposeVersion)))))))) (not (forall (@list @t17 @t66) (exists (@list @t125) (and (= @t125 @t136) (exists (@list @t123 @t124 @t126 @t127) (and (= @t123 (tptp.select2 @t66 @t125 tptp.ownerFrame)) (= @t124 (tptp.select2 @t66 @t125 tptp.ownerRef)) (= @t126 @t135) (= @t127 @t134) (=> (not (or @t133 @t131 @t129 (not (not (= @t126 |tptp.'PeerGroupPlaceholder'|))) (not (= (tptp.x (tptp.select2 @t66 @t127 tptp.inv) @t126) tptp.true_1)) (not (not (= (tptp.select2 @t66 @t127 tptp.localinv) (|tptp.'BaseClass'| @t126)))))) (not (or (not (not (= @t125 tptp.nullObject))) (not (= (= (tptp.select2 @t66 @t125 tptp.allocated) tptp.true_1) true)) (not (or (= @t123 |tptp.'PeerGroupPlaceholder'|) (not (= (tptp.x (tptp.select2 @t66 @t124 tptp.inv) @t123) tptp.true_1)) (= (tptp.select2 @t66 @t124 tptp.localinv) (|tptp.'BaseClass'| @t123))))))))))))) (not (forall (@list @t122 @t108 @t120 @t119) (exists (@list @t121) (and (= @t121 (|tptp.'BoxFunc'| @t122 @t108 @t120 @t119)) (not (or (not (= (|tptp.'Box'| @t122 @t121) @t121)) (not (= (|tptp.'UnboxedType'| @t121) @t108)))))))) (not (forall (@list @t7 @t108 @t120 @t119) (=> (not (= (|tptp.'IsValueType'| (|tptp.'UnboxedType'| @t7)) tptp.true_1)) (= (|tptp.'BoxFunc'| @t7 @t108 @t120 @t119) @t7)))) (not (forall @t114 (= (|tptp.'Unbox'| @t113) @t7))) (not (forall (@list @t14) (=> (= (|tptp.'IsValueType'| @t111) tptp.true_1) (forall (@list @t117 @t7) (exists (@list @t116) (and (= @t116 @t113) (exists (@list @t115) (and (= @t115 (tptp.typeof @t116)) (=> @t118 (not (or (not (= (tptp.select2 @t117 @t116 tptp.inv) @t115)) (not (= (tptp.select2 @t117 @t116 tptp.localinv) @t115))))))))))))) (not (forall @t114 (exists (@list @t112) (and (= @t112 @t113) (=> (not (or (not (= (tptp.x (|tptp.'UnboxedType'| @t112) |tptp.'System_Object'|) tptp.true_1)) (not (= @t112 @t14)))) (= @t7 @t14)))))) (not (forall @t110 (= (= @t111 @t108) @t109))) (not (forall @t110 (=> @t109 (= (|tptp.'Box'| (|tptp.'Unbox'| @t14) @t14) @t14)))) (not (= (|tptp.'IsValueType'| |tptp.'System_SByte'|) tptp.true_1)) (not (= (|tptp.'IsValueType'| |tptp.'System_Byte'|) tptp.true_1)) (not (= (|tptp.'IsValueType'| |tptp.'System_Int16'|) tptp.true_1)) (not (= (|tptp.'IsValueType'| |tptp.'System_UInt16'|) tptp.true_1)) (not (= (|tptp.'IsValueType'| |tptp.'System_Int32'|) tptp.true_1)) (not (= (|tptp.'IsValueType'| |tptp.'System_UInt32'|) tptp.true_1)) (not (= (|tptp.'IsValueType'| |tptp.'System_Int64'|) tptp.true_1)) (not (= (|tptp.'IsValueType'| |tptp.'System_UInt64'|) tptp.true_1)) (not (= (|tptp.'IsValueType'| |tptp.'System_Char'|) tptp.true_1)) (not (= (|tptp.'IsValueType'| |tptp.'System_UIntPtr'|) tptp.true_1)) (not (= (|tptp.'IsValueType'| |tptp.'System_IntPtr'|) tptp.true_1)) (not (< tptp.int_m9223372036854775808 tptp.int_m2147483648)) (not (< tptp.int_m2147483648 (- 0 100000))) (not (< 100000 tptp.int_2147483647)) (not (< tptp.int_2147483647 tptp.int_4294967295)) (not (< tptp.int_4294967295 tptp.int_9223372036854775807)) (not (< tptp.int_9223372036854775807 tptp.int_18446744073709551615)) (not (= (+ tptp.int_m9223372036854775808 1) (- 0 tptp.int_9223372036854775807))) (not (= (+ tptp.int_m2147483648 1) (- 0 tptp.int_2147483647))) (not (forall @t78 (= (= (|tptp.'InRange'| @t22 |tptp.'System_SByte'|) tptp.true_1) (not (or (not (<= (- 0 128) @t22)) (not (< @t22 128))))))) (not (forall @t78 (= (= (|tptp.'InRange'| @t22 |tptp.'System_Byte'|) tptp.true_1) (not (or @t81 (not (< @t22 256))))))) (not (forall @t78 (= (= (|tptp.'InRange'| @t22 |tptp.'System_Int16'|) tptp.true_1) (not (or (not (<= (- 0 32768) @t22)) @t80))))) (not (forall @t78 (= (= (|tptp.'InRange'| @t22 |tptp.'System_UInt16'|) tptp.true_1) @t107))) (not (forall @t78 (= (= (|tptp.'InRange'| @t22 |tptp.'System_Int32'|) tptp.true_1) (not (or (not (<= tptp.int_m2147483648 @t22)) (not (<= @t22 tptp.int_2147483647))))))) (not (forall @t78 (= (= (|tptp.'InRange'| @t22 |tptp.'System_UInt32'|) tptp.true_1) (not (or @t81 (not (<= @t22 tptp.int_4294967295))))))) (not (forall @t78 (= (= (|tptp.'InRange'| @t22 |tptp.'System_Int64'|) tptp.true_1) (not (or (not (<= tptp.int_m9223372036854775808 @t22)) (not (<= @t22 tptp.int_9223372036854775807))))))) (not (forall @t78 (= (= (|tptp.'InRange'| @t22 |tptp.'System_UInt64'|) tptp.true_1) (not (or @t81 (not (<= @t22 tptp.int_18446744073709551615))))))) (not (forall @t78 (= (= (|tptp.'InRange'| @t22 |tptp.'System_Char'|) tptp.true_1) @t107))) (not (forall (@list @t104 @t106 @t105) (=> (= (|tptp.'InRange'| @t104 @t105) tptp.true_1) (= (|tptp.'IntToInt'| @t104 @t106 @t105) @t104)))) (not (forall @t103 (=> @t102 (= @t101 @t7)))) (not (forall @t103 (=> (not @t102) (= @t101 @t6)))) (not (forall @t8 (= @t91 (- @t7 (* (tptp.x_1 @t7 @t6) @t6))))) (not (forall @t8 (exists (@list @t100) (and (= @t100 @t91) (=> (not (or @t88 @t98)) (not (or (not (<= 0 @t100)) (not (< @t100 @t6))))))))) (not (forall @t8 (exists (@list @t99) (and (= @t99 @t91) (=> (not (or @t88 @t94)) (not (or (not (<= 0 @t99)) (not (< @t99 @t97))))))))) (not (forall @t8 (exists (@list @t96) (and (= @t96 @t91) (=> (not (or @t95 @t98)) (not (or (not (< @t97 @t96)) (not (<= @t96 0))))))))) (not (forall @t8 (exists (@list @t93) (and (= @t93 @t91) (=> (not (or @t95 @t94)) (not (or (not (< @t6 @t93)) (not (<= @t93 0))))))))) (not (forall @t8 (=> @t89 (= (tptp.x_2 @t83 @t6) @t91)))) (not (forall @t8 (=> @t89 (= (tptp.x_2 (+ @t6 @t7) @t6) @t91)))) (not (forall @t8 (exists (@list @t92) (and (= @t92 (- @t7 @t6)) (=> (not (or (not (<= 0 @t92)) @t86)) (= (tptp.x_2 @t92 @t6) @t91)))))) (not (forall (@list @t67 @t65 @t90) (=> (not (or (not (<= 2 @t90)) (not (= (tptp.x_2 @t67 @t90) (tptp.x_2 @t65 @t90))) (not (< @t67 @t65)))) (<= (+ @t67 @t90) @t65)))) (not (forall @t8 (=> (or @t87 @t85) (<= 0 (tptp.and_1 @t7 @t6))))) (not (forall @t8 (exists (@list @t84) (and (= @t84 (tptp.or_1 @t7 @t6)) (=> @t89 (not (or (not (<= 0 @t84)) (not (<= @t84 @t83))))))))) (not (forall @t78 (= (tptp.shl @t22 0) @t22))) (not (forall @t77 (=> @t76 (= @t82 (* (tptp.shl @t22 @t75) 2))))) (not (forall @t77 (exists (@list @t79) (and (= @t79 @t82) (=> (not (or @t81 @t80 (not (<= 0 @t21)) (not (<= @t21 16)))) (not (or (not (<= 0 @t79)) (not (<= @t79 tptp.int_2147483647))))))))) (not (forall @t78 (= (tptp.shr @t22 0) @t22))) (not (forall @t77 (=> @t76 (= (tptp.shr @t22 @t21) (tptp.x_1 (tptp.shr @t22 @t75) 2))))) (not (forall @t8 (exists (@list @t74) (and (= @t74 (tptp.min @t7 @t6)) (not (or (not (or (= @t74 @t7) (= @t74 @t6))) (not (<= @t74 @t7)) (not (<= @t74 @t6)))))))) (not (forall @t8 (exists (@list @t73) (and (= @t73 (tptp.max @t7 @t6)) (not (or (not (or (= @t73 @t7) (= @t73 @t6))) (not (<= @t7 @t73)) (not (<= @t6 @t73)))))))) (not (forall @t70 (= (= (|tptp.'System_String_Equals_System_String'| @t66 @t67 @t65) tptp.true_1) @t68))) (not (forall @t70 (not (or (not (= @t68 @t72)) (not (= @t68 (= (|tptp.'StringEquals'| @t65 @t67) tptp.true_1))) (not (=> (= @t67 @t65) @t72)))))) (not (forall (@list @t67 @t65 @t71) (=> (not (or (not @t72) (not (= (|tptp.'StringEquals'| @t65 @t71) tptp.true_1)))) (= (|tptp.'StringEquals'| @t67 @t71) tptp.true_1)))) (not (forall @t70 (=> (not (or @t69 (not (not (= @t65 tptp.nullObject))) (not @t68))) (= (|tptp.'System_String_IsInterned_System_String_notnull'| @t66 @t67) (|tptp.'System_String_IsInterned_System_String_notnull'| @t66 @t65))))) (not (not (= (|tptp.'IsStaticField'| |tptp.'ArrayRefCount_count'|) tptp.true_1))) (not (= (|tptp.'IncludeInMainFrameCondition'| |tptp.'ArrayRefCount_count'|) tptp.true_1)) (not (= (|tptp.'IncludedInModifiesStar'| |tptp.'ArrayRefCount_count'|) tptp.true_1)) (not (= (|tptp.'DeclType'| |tptp.'ArrayRefCount_count'|) |tptp.'ArrayRefCount'|)) (not (= (|tptp.'AsRangeField'| |tptp.'ArrayRefCount_count'| |tptp.'System_Int32'|) |tptp.'ArrayRefCount_count'|)) (not (not (= (|tptp.'IsStaticField'| |tptp.'ArrayRefCount_a'|) tptp.true_1))) (not (= (|tptp.'IncludeInMainFrameCondition'| |tptp.'ArrayRefCount_a'|) tptp.true_1)) (not (= (|tptp.'IncludedInModifiesStar'| |tptp.'ArrayRefCount_a'|) tptp.true_1)) (not (= (|tptp.'AsRepField'| |tptp.'ArrayRefCount_a'| |tptp.'ArrayRefCount'|) |tptp.'ArrayRefCount_a'|)) (not (= (|tptp.'DeclType'| |tptp.'ArrayRefCount_a'|) |tptp.'ArrayRefCount'|)) (not (= (|tptp.'AsNonNullRefField'| |tptp.'ArrayRefCount_a'| (|tptp.'RefArray'| |tptp.'System_String'| 1)) |tptp.'ArrayRefCount_a'|)) (not (= (tptp.x |tptp.'ArrayRefCount'| |tptp.'ArrayRefCount'|) tptp.true_1)) (not (= @t61 |tptp.'System_Object'|)) (not (= (|tptp.'AsDirectSubClass'| |tptp.'ArrayRefCount'| @t61) |tptp.'ArrayRefCount'|)) (not (not (= (|tptp.'IsImmutable'| |tptp.'ArrayRefCount'|) tptp.true_1))) (not (= (|tptp.'AsMutable'| |tptp.'ArrayRefCount'|) |tptp.'ArrayRefCount'|)) (not (= (tptp.x |tptp.'System_Array'| |tptp.'System_Array'|) tptp.true_1)) (not (= @t64 |tptp.'System_Object'|)) (not (= (|tptp.'AsDirectSubClass'| |tptp.'System_Array'| @t64) |tptp.'System_Array'|)) (not (not (= (|tptp.'IsImmutable'| |tptp.'System_Array'|) tptp.true_1))) (not (= (|tptp.'AsMutable'| |tptp.'System_Array'|) |tptp.'System_Array'|)) (not (= (tptp.x |tptp.'System_ICloneable'| |tptp.'System_ICloneable'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_ICloneable'| |tptp.'System_Object'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_ICloneable'|) tptp.true_1)) (not (= (|tptp.'AsInterface'| |tptp.'System_ICloneable'|) |tptp.'System_ICloneable'|)) (not (= (tptp.x |tptp.'System_Array'| |tptp.'System_ICloneable'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Collections_IList'| |tptp.'System_Collections_IList'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Collections_IList'| |tptp.'System_Object'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Collections_ICollection'| |tptp.'System_Collections_ICollection'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Collections_ICollection'| |tptp.'System_Object'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Collections_IEnumerable'| |tptp.'System_Collections_IEnumerable'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Collections_IEnumerable'| |tptp.'System_Object'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_Collections_IEnumerable'|) tptp.true_1)) (not (= (|tptp.'AsInterface'| |tptp.'System_Collections_IEnumerable'|) |tptp.'System_Collections_IEnumerable'|)) (not (= (tptp.x |tptp.'System_Collections_ICollection'| |tptp.'System_Collections_IEnumerable'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_Collections_ICollection'|) tptp.true_1)) (not (= (|tptp.'AsInterface'| |tptp.'System_Collections_ICollection'|) |tptp.'System_Collections_ICollection'|)) (not (= (tptp.x |tptp.'System_Collections_IList'| |tptp.'System_Collections_ICollection'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Collections_IList'| |tptp.'System_Collections_IEnumerable'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_Collections_IList'|) tptp.true_1)) (not (= (|tptp.'AsInterface'| |tptp.'System_Collections_IList'|) |tptp.'System_Collections_IList'|)) (not (= (tptp.x |tptp.'System_Array'| |tptp.'System_Collections_IList'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Array'| |tptp.'System_Collections_ICollection'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Array'| |tptp.'System_Collections_IEnumerable'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_Array'|) tptp.true_1)) (not (forall @t31 (=> (not (or @t30 (not (= (tptp.x @t29 |tptp.'System_Array'|) tptp.true_1)) (not (not (= @t28 @t64))))) true))) (not (= (tptp.x |tptp.'System_String'| |tptp.'System_String'|) tptp.true_1)) (not (= @t62 |tptp.'System_Object'|)) (not (= (|tptp.'AsDirectSubClass'| |tptp.'System_String'| @t62) |tptp.'System_String'|)) (not (= (|tptp.'IsImmutable'| |tptp.'System_String'|) tptp.true_1)) (not (= (|tptp.'AsImmutable'| |tptp.'System_String'|) |tptp.'System_String'|)) (not (= (tptp.x |tptp.'System_IComparable'| |tptp.'System_IComparable'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_IComparable'| |tptp.'System_Object'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_IComparable'|) tptp.true_1)) (not (= (|tptp.'AsInterface'| |tptp.'System_IComparable'|) |tptp.'System_IComparable'|)) (not (= (tptp.x |tptp.'System_String'| |tptp.'System_IComparable'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_String'| |tptp.'System_ICloneable'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_IConvertible'| |tptp.'System_IConvertible'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_IConvertible'| |tptp.'System_Object'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_IConvertible'|) tptp.true_1)) (not (= (|tptp.'AsInterface'| |tptp.'System_IConvertible'|) |tptp.'System_IConvertible'|)) (not (= (tptp.x |tptp.'System_String'| |tptp.'System_IConvertible'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_IComparable_1___System_String'| |tptp.'System_IComparable_1___System_String'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_IComparable_1___System_String'| |tptp.'System_Object'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_IComparable_1___System_String'|) tptp.true_1)) (not (= (|tptp.'AsInterface'| |tptp.'System_IComparable_1___System_String'|) |tptp.'System_IComparable_1___System_String'|)) (not (= (tptp.x |tptp.'System_String'| |tptp.'System_IComparable_1___System_String'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'System_Object'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'| |tptp.'System_Collections_IEnumerable'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|) tptp.true_1)) (not (= (|tptp.'AsInterface'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|) |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|)) (not (= (tptp.x |tptp.'System_String'| |tptp.'System_Collections_Generic_IEnumerable_1___System_Char'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_String'| |tptp.'System_Collections_IEnumerable'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_IEquatable_1___System_String'| |tptp.'System_IEquatable_1___System_String'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_IEquatable_1___System_String'| |tptp.'System_Object'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_IEquatable_1___System_String'|) tptp.true_1)) (not (= (|tptp.'AsInterface'| |tptp.'System_IEquatable_1___System_String'|) |tptp.'System_IEquatable_1___System_String'|)) (not (= (tptp.x |tptp.'System_String'| |tptp.'System_IEquatable_1___System_String'|) tptp.true_1)) (not (forall (@list @t63) (=> (= (tptp.x @t63 |tptp.'System_String'|) tptp.true_1) (= @t63 |tptp.'System_String'|)))) (not (forall @t31 (=> (not (or @t30 (not (= (tptp.x @t29 |tptp.'System_String'|) tptp.true_1)) (not (not (= @t28 @t62))))) true))) (not (forall @t31 (exists (@list @t60) (and (= @t60 (tptp.select2 @t27 @t26 |tptp.'ArrayRefCount_count'|)) (=> (not (or @t30 (not (= (tptp.x @t29 |tptp.'ArrayRefCount'|) tptp.true_1)) (not (not (= @t28 @t61))))) (not (or (not (<= 0 @t60)) (not (<= @t60 (|tptp.'Length'| (tptp.select2 @t27 @t26 |tptp.'ArrayRefCount_a'|))))))))))) (not (= (tptp.x |tptp.'Microsoft_Contracts_ObjectInvariantException'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|) tptp.true_1)) (not (= (tptp.x |tptp.'Microsoft_Contracts_GuardException'| |tptp.'Microsoft_Contracts_GuardException'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Exception'| |tptp.'System_Exception'|) tptp.true_1)) (not (= @t59 |tptp.'System_Object'|)) (not (= (|tptp.'AsDirectSubClass'| |tptp.'System_Exception'| @t59) |tptp.'System_Exception'|)) (not (not (= (|tptp.'IsImmutable'| |tptp.'System_Exception'|) tptp.true_1))) (not (= (|tptp.'AsMutable'| |tptp.'System_Exception'|) |tptp.'System_Exception'|)) (not (= (tptp.x |tptp.'System_Runtime_Serialization_ISerializable'| |tptp.'System_Runtime_Serialization_ISerializable'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Runtime_Serialization_ISerializable'| |tptp.'System_Object'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_Runtime_Serialization_ISerializable'|) tptp.true_1)) (not (= (|tptp.'AsInterface'| |tptp.'System_Runtime_Serialization_ISerializable'|) |tptp.'System_Runtime_Serialization_ISerializable'|)) (not (= (tptp.x |tptp.'System_Exception'| |tptp.'System_Runtime_Serialization_ISerializable'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_Runtime_InteropServices__Exception'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Runtime_InteropServices__Exception'| |tptp.'System_Object'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_Runtime_InteropServices__Exception'|) tptp.true_1)) (not (= (|tptp.'AsInterface'| |tptp.'System_Runtime_InteropServices__Exception'|) |tptp.'System_Runtime_InteropServices__Exception'|)) (not (= (tptp.x |tptp.'System_Exception'| |tptp.'System_Runtime_InteropServices__Exception'|) tptp.true_1)) (not (forall @t31 (=> (not (or @t30 (not (= (tptp.x @t29 |tptp.'System_Exception'|) tptp.true_1)) (not (not (= @t28 @t59))))) true))) (not (= @t58 |tptp.'System_Exception'|)) (not (= (|tptp.'AsDirectSubClass'| |tptp.'Microsoft_Contracts_GuardException'| @t58) |tptp.'Microsoft_Contracts_GuardException'|)) (not (not (= (|tptp.'IsImmutable'| |tptp.'Microsoft_Contracts_GuardException'|) tptp.true_1))) (not (= (|tptp.'AsMutable'| |tptp.'Microsoft_Contracts_GuardException'|) |tptp.'Microsoft_Contracts_GuardException'|)) (not (forall @t31 (=> (not (or @t30 (not (= (tptp.x @t29 |tptp.'Microsoft_Contracts_GuardException'|) tptp.true_1)) (not (not (= @t28 @t58))))) true))) (not (= @t57 |tptp.'Microsoft_Contracts_GuardException'|)) (not (= (|tptp.'AsDirectSubClass'| |tptp.'Microsoft_Contracts_ObjectInvariantException'| @t57) |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (not (= (|tptp.'IsImmutable'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|) tptp.true_1))) (not (= (|tptp.'AsMutable'| |tptp.'Microsoft_Contracts_ObjectInvariantException'|) |tptp.'Microsoft_Contracts_ObjectInvariantException'|)) (not (forall @t31 (=> (not (or @t30 (not (= (tptp.x @t29 |tptp.'Microsoft_Contracts_ObjectInvariantException'|) tptp.true_1)) (not (not (= @t28 @t57))))) true))) (not (forall @t44 (= (tptp.count_0 @t37 @t38 @t35 @t34 @t33) @t39))) (not (forall @t44 (=> (forall @t56 (=> (not (or @t55 @t54 @t41)) @t53)) (= @t39 0)))) (not (forall (@list @t37 @t38 @t35 @t51 @t34 @t50 @t33 @t49) (=> (forall @t56 (=> (not (or @t55 @t54)) (not (or (not (= @t40 (= @t51 tptp.true_1))) (not (=> @t40 (= (not @t53) (not (= (|tptp.'RefArrayGet'| @t50 @t52) @t49))))))))) (= @t39 (tptp.count_x0 @t37 @t38 @t51 @t50 @t49))))) (not (forall (@list @t37 @t48 @t38 @t35 @t34 @t33) (=> (not (or (not (<= @t37 @t48)) (not (<= @t48 @t38)))) (= (+ (tptp.count_x0 @t37 @t48 @t35 @t34 @t33) (tptp.count_x0 @t48 @t38 @t35 @t34 @t33)) @t39)))) (not (forall @t44 (=> (not (or @t42 @t41 @t47)) (= @t39 (+ @t46 1))))) (not (forall @t44 (=> (not (or @t42 (not (not (not (or @t41 @t47)))))) (= @t39 @t46)))) (not (forall @t44 (exists (@list @t45) (and (= @t45 @t43) (=> (not (or @t42 @t41 (not (not (= (|tptp.'RefArrayGet'| @t34 @t45) @t33))))) (= @t39 (+ (tptp.count_x0 @t37 @t45 @t35 @t34 @t33) 1))))))) (not (forall @t44 (exists (@list @t36) (and (= @t36 @t43) (=> (not (or @t42 (not (not (not (or @t41 (not (not (= (|tptp.'RefArrayGet'| @t34 @t36) @t33))))))))) (= @t39 (tptp.count_x0 @t37 @t36 @t35 @t34 @t33))))))) (not (= (tptp.x |tptp.'System_Type'| |tptp.'System_Type'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Reflection_MemberInfo'| |tptp.'System_Reflection_MemberInfo'|) tptp.true_1)) (not (= @t32 |tptp.'System_Object'|)) (not (= (|tptp.'AsDirectSubClass'| |tptp.'System_Reflection_MemberInfo'| @t32) |tptp.'System_Reflection_MemberInfo'|)) (not (= (|tptp.'IsImmutable'| |tptp.'System_Reflection_MemberInfo'|) tptp.true_1)) (not (= (|tptp.'AsImmutable'| |tptp.'System_Reflection_MemberInfo'|) |tptp.'System_Reflection_MemberInfo'|)) (not (= (tptp.x |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'System_Reflection_ICustomAttributeProvider'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Reflection_ICustomAttributeProvider'| |tptp.'System_Object'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_Reflection_ICustomAttributeProvider'|) tptp.true_1)) (not (= (|tptp.'AsInterface'| |tptp.'System_Reflection_ICustomAttributeProvider'|) |tptp.'System_Reflection_ICustomAttributeProvider'|)) (not (= (tptp.x |tptp.'System_Reflection_MemberInfo'| |tptp.'System_Reflection_ICustomAttributeProvider'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Runtime_InteropServices__MemberInfo'| |tptp.'System_Runtime_InteropServices__MemberInfo'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Runtime_InteropServices__MemberInfo'| |tptp.'System_Object'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_Runtime_InteropServices__MemberInfo'|) tptp.true_1)) (not (= (|tptp.'AsInterface'| |tptp.'System_Runtime_InteropServices__MemberInfo'|) |tptp.'System_Runtime_InteropServices__MemberInfo'|)) (not (= (tptp.x |tptp.'System_Reflection_MemberInfo'| |tptp.'System_Runtime_InteropServices__MemberInfo'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_Reflection_MemberInfo'|) tptp.true_1)) (not (forall @t31 (=> (not (or @t30 (not (= (tptp.x @t29 |tptp.'System_Reflection_MemberInfo'|) tptp.true_1)) (not (not (= @t28 @t32))))) true))) (not (= @t25 |tptp.'System_Reflection_MemberInfo'|)) (not (= (|tptp.'AsDirectSubClass'| |tptp.'System_Type'| @t25) |tptp.'System_Type'|)) (not (= (|tptp.'IsImmutable'| |tptp.'System_Type'|) tptp.true_1)) (not (= (|tptp.'AsImmutable'| |tptp.'System_Type'|) |tptp.'System_Type'|)) (not (= (tptp.x |tptp.'System_Runtime_InteropServices__Type'| |tptp.'System_Runtime_InteropServices__Type'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Runtime_InteropServices__Type'| |tptp.'System_Object'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_Runtime_InteropServices__Type'|) tptp.true_1)) (not (= (|tptp.'AsInterface'| |tptp.'System_Runtime_InteropServices__Type'|) |tptp.'System_Runtime_InteropServices__Type'|)) (not (= (tptp.x |tptp.'System_Type'| |tptp.'System_Runtime_InteropServices__Type'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Reflection_IReflect'| |tptp.'System_Reflection_IReflect'|) tptp.true_1)) (not (= (tptp.x |tptp.'System_Reflection_IReflect'| |tptp.'System_Object'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_Reflection_IReflect'|) tptp.true_1)) (not (= (|tptp.'AsInterface'| |tptp.'System_Reflection_IReflect'|) |tptp.'System_Reflection_IReflect'|)) (not (= (tptp.x |tptp.'System_Type'| |tptp.'System_Reflection_IReflect'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'System_Type'|) tptp.true_1)) (not (forall @t31 (=> (not (or @t30 (not (= (tptp.x @t29 |tptp.'System_Type'|) tptp.true_1)) (not (not (= @t28 @t25))))) true))) (not (= (tptp.x |tptp.'Microsoft_Contracts_ICheckedException'| |tptp.'Microsoft_Contracts_ICheckedException'|) tptp.true_1)) (not (= (tptp.x |tptp.'Microsoft_Contracts_ICheckedException'| |tptp.'System_Object'|) tptp.true_1)) (not (= (|tptp.'IsMemberlessType'| |tptp.'Microsoft_Contracts_ICheckedException'|) tptp.true_1)) (not (= (|tptp.'AsInterface'| |tptp.'Microsoft_Contracts_ICheckedException'|) |tptp.'Microsoft_Contracts_ICheckedException'|))))))) % 0.46/0.85 (assume @p3 @t300) % 0.46/0.85 (step @p4 :rule evaluate :args ((not true))) % 0.46/0.85 (step @p5 :rule bool-impl-true1 :args (@t301)) % 0.46/0.85 (step @p6 :rule bool-impl-true1 :args (@t302)) % 0.46/0.85 (step @p7 :rule bool-impl-true1 :args (@t293)) % 0.46/0.85 (step @p8 :rule evaluate :args ((not false))) % 0.46/0.85 (step @p9 :rule evaluate :args ((or false false))) % 0.46/0.85 (step @p10 :rule bool-impl-true1 :args (@t268)) % 0.46/0.85 (step @p11 :rule cong :premises (@p10) :args (@t269)) % 0.46/0.85 (step @p12 :rule trans :premises (@p11 @p4)) % 0.46/0.85 (step @p13 :rule quant-unused-vars :args ((= (forall @t267 true) true))) % 0.46/0.85 (step @p14 :rule evaluate :args ((or false false false))) % 0.46/0.85 (step @p15 :rule eq-refl :args (@t264)) % 0.46/0.85 (step @p16 :rule cong :premises (@p15) :args (@t303)) % 0.46/0.85 (step @p17 :rule trans :premises (@p16 @p4)) % 0.46/0.85 (step @p18 :rule quant-var-elim-eq :args ((= (forall @t306 @t305) @t303))) % 0.46/0.85 (step @p19 :rule aci_norm :args ((= @t304 @t305))) % 0.46/0.85 (step @p20 :rule cong :premises (@p19) :args (@t307)) % 0.46/0.85 (step @p21 :rule trans :premises (@p20 @p18)) % 0.46/0.85 (step @p22 :rule trans :premises (@p21 @p17)) % 0.46/0.85 (step @p23 :rule eq-refl :args (@t265)) % 0.46/0.85 (step @p24 :rule cong :premises (@p23) :args (@t308)) % 0.46/0.85 (step @p25 :rule trans :premises (@p24 @p4)) % 0.46/0.85 (step @p26 :rule quant-var-elim-eq :args ((= (forall @t311 @t310) @t308))) % 0.46/0.85 (step @p27 :rule aci_norm :args ((= @t309 @t310))) % 0.46/0.85 (step @p28 :rule cong :premises (@p27) :args (@t312)) % 0.46/0.85 (step @p29 :rule trans :premises (@p28 @p26)) % 0.46/0.85 (step @p30 :rule trans :premises (@p29 @p25)) % 0.46/0.85 (step @p31 :rule eq-refl :args (@t266)) % 0.46/0.85 (step @p32 :rule cong :premises (@p31) :args (@t313)) % 0.46/0.85 (step @p33 :rule trans :premises (@p32 @p4)) % 0.46/0.85 (step @p34 :rule quant-var-elim-eq :args ((= (forall @t316 @t315) @t313))) % 0.46/0.85 (step @p35 :rule aci_norm :args ((= @t314 @t315))) % 0.46/0.85 (step @p36 :rule cong :premises (@p35) :args (@t317)) % 0.46/0.85 (step @p37 :rule trans :premises (@p36 @p34)) % 0.46/0.85 (step @p38 :rule trans :premises (@p37 @p33)) % 0.46/0.85 (step @p39 :rule nary_cong :premises (@p38 @p30 @p22) :args (@t318)) % 0.46/0.85 (step @p40 :rule trans :premises (@p39 @p14)) % 0.46/0.85 (step @p41 :rule quant-miniscope-or :args ((= (forall @t287 @t319) @t318))) % 0.46/0.85 (step @p42 :rule trans :premises (@p41 @p40)) % 0.46/0.85 (step @p43 :rule aci_norm :args ((= (or @t314 (or @t309 @t304)) @t319))) % 0.46/0.85 (step @p44 :rule bool-and-de-morgan :args (@t284 @t283 true)) % 0.46/0.85 (step @p45 :rule refl :args (@t314)) % 0.46/0.85 (step @p46 :rule nary_cong :premises (@p45 @p44) :args ((or @t314 (not (and @t284 @t283))))) % 0.46/0.85 (step @p47 :rule bool-and-de-morgan :args (@t285 @t284 (and @t283))) % 0.46/0.85 (step @p48 :rule trans :premises (@p47 @p46)) % 0.46/0.85 (step @p49 :rule trans :premises (@p48 @p43)) % 0.46/0.85 (step @p50 :rule cong :premises (@p49) :args (@t321)) % 0.46/0.85 (step @p51 :rule trans :premises (@p50 @p42)) % 0.46/0.85 (step @p52 :rule cong :premises (@p51) :args (@t322)) % 0.46/0.85 (step @p53 :rule trans :premises (@p52 @p8)) % 0.46/0.85 (step @p54 :rule exists-elim :args ((= (exists @t287 @t320) @t322))) % 0.46/0.85 (step @p55 :rule trans :premises (@p54 @p53)) % 0.46/0.85 (step @p56 :rule aci_norm :args ((= (and @t285 @t284 @t283 true) @t320))) % 0.46/0.85 (step @p57 :rule bool-impl-true1 :args ((not (or (not @t327) @t326 (not @t325) (not (or @t324 (not @t323) @t273)))))) % 0.46/0.85 (step @p58 :rule eq-refl :args (@t270)) % 0.46/0.85 (step @p59 :rule refl :args (@t273)) % 0.46/0.85 (step @p60 :rule arith_poly_norm :args ((= (* 1 (- @t274 tptp.true_1)) (* -1 (- tptp.true_1 @t274))))) % 0.46/0.85 (step @p61 :rule arith_poly_norm_rel :premises (@p60) :args ((= @t275 @t323))) % 0.46/0.85 (step @p62 :rule cong :premises (@p61) :args (@t276)) % 0.46/0.85 (step @p63 :rule arith_poly_norm :args ((= (* 1 (- @t271 |tptp.'PeerGroupPlaceholder'|)) (* -1 (- |tptp.'PeerGroupPlaceholder'| @t271))))) % 0.46/0.85 (step @p64 :rule arith_poly_norm_rel :premises (@p63) :args ((= @t277 @t324))) % 0.46/0.85 (step @p65 :rule nary_cong :premises (@p64 @p62 @p59) :args (@t278)) % 0.46/0.85 (step @p66 :rule cong :premises (@p65) :args (@t279)) % 0.46/0.85 (step @p67 :rule arith_poly_norm :args ((= (* 1 (- @t255 tptp.true_1)) (* -1 (- tptp.true_1 @t255))))) % 0.46/0.85 (step @p68 :rule arith_poly_norm_rel :premises (@p67) :args ((= @t256 @t325))) % 0.46/0.85 (step @p69 :rule cong :premises (@p68) :args (@t257)) % 0.46/0.85 (step @p70 :rule arith_poly_norm :args ((= (* 1 (- @t254 tptp.nullObject)) (* -1 (- tptp.nullObject @t254))))) % 0.46/0.85 (step @p71 :rule arith_poly_norm_rel :premises (@p70) :args ((= @t258 @t326))) % 0.46/0.85 (step @p72 :rule bool-double-not-elim :args (@t258)) % 0.46/0.85 (step @p73 :rule trans :premises (@p72 @p71)) % 0.46/0.85 (step @p74 :rule arith_poly_norm :args ((= (* 1 (- @t261 tptp.true_1)) (* -1 (- tptp.true_1 @t261))))) % 0.46/0.85 (step @p75 :rule arith_poly_norm_rel :premises (@p74) :args ((= @t262 @t327))) % 0.46/0.85 (step @p76 :rule cong :premises (@p75) :args (@t263)) % 0.46/0.85 (step @p77 :rule nary_cong :premises (@p76 @p73 @p69 @p66) :args (@t280)) % 0.46/0.85 (step @p78 :rule cong :premises (@p77) :args (@t281)) % 0.46/0.85 (step @p79 :rule cong :premises (@p78 @p58) :args (@t282)) % 0.46/0.85 (step @p80 :rule trans :premises (@p79 @p57)) % 0.46/0.85 (step @p81 :rule refl :args (@t283)) % 0.46/0.85 (step @p82 :rule refl :args (@t284)) % 0.46/0.85 (step @p83 :rule refl :args (@t285)) % 0.46/0.85 (step @p84 :rule nary_cong :premises (@p83 @p82 @p81 @p80) :args (@t286)) % 0.46/0.85 (step @p85 :rule trans :premises (@p84 @p56)) % 0.46/0.85 (step @p86 :rule cong :premises (@p85) :args (@t288)) % 0.46/0.85 (step @p87 :rule trans :premises (@p86 @p55)) % 0.46/0.85 (step @p88 :rule cong :premises (@p87) :args (@t289)) % 0.46/0.85 (step @p89 :rule trans :premises (@p88 @p13)) % 0.46/0.85 (step @p90 :rule cong :premises (@p89) :args (@t290)) % 0.46/0.85 (step @p91 :rule trans :premises (@p90 @p4)) % 0.46/0.85 (step @p92 :rule nary_cong :premises (@p91 @p12) :args (@t291)) % 0.46/0.85 (step @p93 :rule trans :premises (@p92 @p9)) % 0.46/0.85 (step @p94 :rule cong :premises (@p93) :args (@t292)) % 0.46/0.85 (step @p95 :rule trans :premises (@p94 @p8)) % 0.46/0.85 (step @p96 :rule refl :args (@t293)) % 0.46/0.85 (step @p97 :rule cong :premises (@p96 @p95) :args (@t294)) % 0.46/0.85 (step @p98 :rule trans :premises (@p97 @p7)) % 0.46/0.85 (step @p99 :rule arith_poly_norm :args ((= (* 1 (- |tptp.'PurityAxiomsCanBeAssumed'| tptp.true_1)) (* -1 (- tptp.true_1 |tptp.'PurityAxiomsCanBeAssumed'|))))) % 0.46/0.85 (step @p100 :rule arith_poly_norm_rel :premises (@p99) :args ((= @t295 @t302))) % 0.46/0.85 (step @p101 :rule cong :premises (@p100 @p98) :args (@t296)) % 0.46/0.85 (step @p102 :rule trans :premises (@p101 @p6)) % 0.46/0.85 (step @p103 :rule arith_poly_norm :args ((= (* 1 (- @t297 tptp.true_1)) (* -1 (- tptp.true_1 @t297))))) % 0.46/0.85 (step @p104 :rule arith_poly_norm_rel :premises (@p103) :args ((= @t298 @t301))) % 0.46/0.85 (step @p105 :rule cong :premises (@p104 @p102) :args (@t299)) % 0.46/0.85 (step @p106 :rule trans :premises (@p105 @p5)) % 0.46/0.85 (step @p107 :rule cong :premises (@p106) :args (@t300)) % 0.46/0.85 (step @p108 :rule trans :premises (@p107 @p4)) % 0.46/0.85 (step @p109 false :rule eq_resolve :premises (@p3 @p108)) % 0.46/0.85 ) % 0.46/0.85 % SZS output end Proof % 0.46/0.85 % cvc5 exiting %------------------------------------------------------------------------------