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