%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ARI752_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 : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:08:15 AM UTC 2026 % Result : Unsatisfiable 0.43s 0.78s % Output : Proof 0.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ARI752_1 : TPTP v9.2.1. Released v7.0.0. % 0.00/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.16/0.34 % Computer : n019.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Wed Jun 3 02:33:19 EDT 2026 % 0.16/0.34 % CPUTime : % 0.40/0.59 %----Proving TF0_ARI % 0.40/0.60 --- Run --finite-model-find --decision=internal at 45... % 0.43/0.78 % SZS status Unsatisfiable % 0.43/0.78 % SZS output start Proof % 0.43/0.81 ( % 0.43/0.81 (declare-sort |tptp.'Unit'| 0) % 0.43/0.81 (declare-sort tptp.c_type 0) % 0.43/0.81 (declare-sort tptp.c_unsorted 0) % 0.43/0.81 (declare-sort tptp.c_sorted 0) % 0.43/0.81 (declare-sort tptp.c_Boolean 0) % 0.43/0.81 (declare-const tptp.void_P_tag tptp.c_unsorted) % 0.43/0.81 (declare-const tptp.valid_struct_void_P (-> tptp.c_sorted Int Int tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.valid_struct_char_P (-> tptp.c_sorted Int Int tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.valid_root_void_P (-> tptp.c_sorted Int Int tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.valid_root_char_P (-> tptp.c_sorted Int Int tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.valid_bitvector_struct_void_P (-> tptp.c_sorted Int Int tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.valid_bitvector_struct_char_P (-> tptp.c_sorted Int Int tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.strict_valid_struct_void_P (-> tptp.c_sorted Int Int tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.strict_valid_struct_char_P (-> tptp.c_sorted Int Int tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.pset_disjoint (-> tptp.c_sorted tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.offset_max_bytes (-> tptp.c_sorted tptp.c_sorted Int Int)) % 0.43/0.81 (declare-const tptp.in_pset (-> tptp.c_sorted tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.smtlib__store (-> tptp.c_sorted tptp.c_sorted tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.subtag_bool (-> tptp.c_sorted tptp.c_sorted tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.sub_pointer (-> tptp.c_sorted tptp.c_sorted Int)) % 0.43/0.81 (declare-const tptp.neq_pointer_bool (-> tptp.c_sorted tptp.c_sorted tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.eq_pointer_bool (-> tptp.c_sorted tptp.c_sorted tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.block (-> tptp.c_type tptp.c_type)) % 0.43/0.81 (declare-const tptp.smtlib__select (-> tptp.c_sorted tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.alloc_table (-> tptp.c_type tptp.c_type)) % 0.43/0.81 (declare-const tptp.neq_int_bool (-> Int Int tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.pointer (-> tptp.c_type tptp.c_type)) % 0.43/0.81 (declare-const tptp.tag_table (-> tptp.c_type tptp.c_type)) % 0.43/0.81 (declare-const tptp.same_block (-> tptp.c_sorted tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.offset_min (-> tptp.c_sorted tptp.c_sorted Int)) % 0.43/0.81 (declare-const tptp.log (-> Real Real)) % 0.43/0.81 (declare-const tptp.exp (-> Real Real)) % 0.43/0.81 (declare-const tptp.abs_real (-> Real Real)) % 0.43/0.81 (declare-const tptp.real_max (-> Real Real Real)) % 0.43/0.81 (declare-const tptp.memory (-> tptp.c_type tptp.c_type tptp.c_type)) % 0.43/0.81 (declare-const tptp.real_min (-> Real Real Real)) % 0.43/0.81 (declare-const tptp.neq_real_bool (-> Real Real tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.eq_real_bool (-> Real Real tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.gt_real_bool (-> Real Real tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.lt_real_bool (-> Real Real tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.shift (-> tptp.c_sorted Int tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.c_Boolean_true tptp.c_Boolean) % 0.43/0.81 (declare-const tptp.ge_real_bool (-> Real Real tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.downcast (-> tptp.c_sorted tptp.c_sorted tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.s2real (-> tptp.c_sorted Real)) % 0.43/0.81 (declare-const tptp.bool_or (-> tptp.c_Boolean tptp.c_Boolean tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.ge_int_bool (-> Int Int tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.s2bool (-> tptp.c_sorted tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.lt_int_bool (-> Int Int tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.s2int (-> tptp.c_sorted Int)) % 0.43/0.81 (declare-const tptp.valid (-> tptp.c_sorted tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.lsl (-> Int Int Int)) % 0.43/0.81 (declare-const tptp.bool_not (-> tptp.c_Boolean tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.bool_and (-> tptp.c_Boolean tptp.c_Boolean tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.offset_max (-> tptp.c_sorted tptp.c_sorted Int)) % 0.43/0.81 (declare-const tptp.c_int tptp.c_type) % 0.43/0.81 (declare-const tptp.tag_id (-> tptp.c_type tptp.c_type)) % 0.43/0.81 (declare-const tptp.c_unit tptp.c_type) % 0.43/0.81 (declare-const tptp.void_P tptp.c_type) % 0.43/0.81 (declare-const tptp.unit2u (-> |tptp.'Unit'| tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.smtlib__ite (-> tptp.c_Boolean tptp.c_sorted tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.c_sort (-> tptp.c_type tptp.c_unsorted tptp.c_sorted)) % 0.43/0.81 (declare-const tptp.c_Boolean_false tptp.c_Boolean) % 0.43/0.81 (declare-const tptp.le_real_bool (-> Real Real tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.bool_xor (-> tptp.c_Boolean tptp.c_Boolean tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.s2unit (-> tptp.c_sorted |tptp.'Unit'|)) % 0.43/0.81 (declare-const tptp.null tptp.c_unsorted) % 0.43/0.81 (declare-const tptp.address (-> tptp.c_sorted Int)) % 0.43/0.81 (declare-const tptp.le_int_bool (-> Int Int tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.c_real tptp.c_type) % 0.43/0.81 (declare-const tptp.bool2u (-> tptp.c_Boolean tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.int_max (-> Int Int Int)) % 0.43/0.81 (declare-const tptp.int_min (-> Int Int Int)) % 0.43/0.81 (declare-const tptp.base_block (-> tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.fully_packed (-> tptp.c_sorted tptp.c_sorted tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.gt_int_bool (-> Int Int tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.eq_int_bool (-> Int Int tptp.c_Boolean)) % 0.43/0.81 (declare-const tptp.pset_empty tptp.c_unsorted) % 0.43/0.81 (declare-const tptp.c_bool tptp.c_type) % 0.43/0.81 (declare-const tptp.root_tag (-> tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.int2u (-> Int tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.real2u (-> Real tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.abs_int (-> Int Int)) % 0.43/0.81 (declare-const tptp.pset (-> tptp.c_type tptp.c_type)) % 0.43/0.81 (declare-const tptp.pset_included (-> tptp.c_sorted tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.pset_range (-> tptp.c_sorted Int Int tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.pset_singleton (-> tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.pset_all (-> tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.pset_deref (-> tptp.c_sorted tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.asr (-> Int Int Int)) % 0.43/0.81 (declare-const tptp.pset_range_left (-> tptp.c_sorted Int tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.pset_range_right (-> tptp.c_sorted Int tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.pset_union (-> tptp.c_sorted tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.full_separated (-> tptp.c_sorted tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.valid_pset (-> tptp.c_sorted tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.not_assigns (-> tptp.c_sorted tptp.c_sorted tptp.c_sorted tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.subtag (-> tptp.c_sorted tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.parenttag (-> tptp.c_sorted tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.typeof (-> tptp.c_sorted tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.instanceof (-> tptp.c_sorted tptp.c_sorted tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.bottom_tag tptp.c_unsorted) % 0.43/0.81 (declare-const tptp.char_P_tag tptp.c_unsorted) % 0.43/0.81 (declare-const tptp.bw_and (-> Int Int Int)) % 0.43/0.81 (declare-const tptp.lsr (-> Int Int Int)) % 0.43/0.81 (declare-const tptp.left_valid_struct_void_P (-> tptp.c_sorted Int tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.alloc_fresh (-> tptp.c_sorted tptp.c_sorted Int Bool)) % 0.43/0.81 (declare-const tptp.alloc_extends (-> tptp.c_sorted tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.alloc_extends_except (-> tptp.c_sorted tptp.c_sorted tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.offset_min_bytes (-> tptp.c_sorted tptp.c_sorted Int Int)) % 0.43/0.81 (declare-const tptp.bitvector tptp.c_type) % 0.43/0.81 (declare-const tptp.replace_bytes (-> tptp.c_sorted Int Int tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.extract_bytes (-> tptp.c_sorted Int Int tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.concat_bitvector (-> tptp.c_sorted tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.store_bytes (-> tptp.c_sorted tptp.c_sorted Int Int tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.char_P tptp.c_type) % 0.43/0.81 (declare-const tptp.select_bytes (-> tptp.c_sorted tptp.c_sorted Int Int tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.char_P_of_bitvector (-> tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.bitvector_of_char_P (-> tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.int32_of_bitvector (-> tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.int32 tptp.c_type) % 0.43/0.81 (declare-const tptp.bitvector_of_int32 (-> tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.int8_of_bitvector (-> tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.int8 tptp.c_type) % 0.43/0.81 (declare-const tptp.bitvector_of_int8 (-> tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.void_P_of_bitvector (-> tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.bitvector_of_void_P (-> tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.int_of_tag (-> tptp.c_sorted Int)) % 0.43/0.81 (declare-const tptp.pointer_address (-> tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.char_P_of_pointer_address (-> tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.integer_of_int32 (-> tptp.c_sorted Int)) % 0.43/0.81 (declare-const tptp.eq_int32 (-> tptp.c_sorted tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.integer_of_int8 (-> tptp.c_sorted Int)) % 0.43/0.81 (declare-const tptp.eq_int8 (-> tptp.c_sorted tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.int32_of_integer (-> Int tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.int8_of_integer (-> Int tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.left_valid_struct_char_P (-> tptp.c_sorted Int tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.void_P_of_pointer_address (-> tptp.c_sorted tptp.c_unsorted)) % 0.43/0.81 (declare-const tptp.right_valid_struct_char_P (-> tptp.c_sorted Int tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.right_valid_struct_void_P (-> tptp.c_sorted Int tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.strict_valid_root_char_P (-> tptp.c_sorted Int Int tptp.c_sorted Bool)) % 0.43/0.81 (declare-const tptp.strict_valid_root_void_P (-> tptp.c_sorted Int Int tptp.c_sorted Bool)) % 0.43/0.81 (define @t1 () (@var "A__questionmark_bcd" tptp.c_Boolean)) % 0.43/0.81 (define @t2 () (@var "A__questionmark_xu0_1" Int)) % 0.43/0.81 (define @t3 () (@var "A__questionmark_xu0_2" tptp.c_Boolean)) % 0.43/0.81 (define @t4 () (@var "A__questionmark_xu0_3" Real)) % 0.43/0.81 (define @t5 () (@var "A__questionmark_xu0_4" |tptp.'Unit'|)) % 0.43/0.81 (define @t6 () (@var "A__questionmark_xu0_5" tptp.c_unsorted)) % 0.43/0.81 (define @t7 () (@var "A__questionmark_xu0_6" tptp.c_unsorted)) % 0.43/0.81 (define @t8 () (@var "A__questionmark_xu0_7" tptp.c_unsorted)) % 0.43/0.81 (define @t9 () (@var "A__questionmark_xu0_8" tptp.c_unsorted)) % 0.43/0.81 (define @t10 () (@var "A__questionmark_bu0_10" Int)) % 0.43/0.81 (define @t11 () (@var "A__questionmark_au0_9" Int)) % 0.43/0.81 (define @t12 () (and (<= 0 @t10) (< @t11 @t10))) % 0.43/0.81 (define @t13 () (@var "A__questionmark_bu32_12" tptp.c_Boolean)) % 0.43/0.81 (define @t14 () (@var "A__questionmark_au33_11" tptp.c_Boolean)) % 0.43/0.81 (define @t15 () (@var "A__questionmark_bu34_14" tptp.c_Boolean)) % 0.43/0.81 (define @t16 () (@var "A__questionmark_au35_13" tptp.c_Boolean)) % 0.43/0.82 (define @t17 () (@var "A__questionmark_bu36_16" tptp.c_Boolean)) % 0.43/0.82 (define @t18 () (@var "A__questionmark_au37_15" tptp.c_Boolean)) % 0.43/0.82 (define @t19 () (@var "A__questionmark_au38_17" tptp.c_Boolean)) % 0.43/0.82 (define @t20 () (@var "A__questionmark_v_0_2" tptp.c_sorted)) % 0.43/0.82 (define @t21 () (@var "A__questionmark_yu39_20" tptp.c_unsorted)) % 0.43/0.82 (define @t22 () (@var "A__questionmark_t1u0_18" tptp.c_type)) % 0.43/0.82 (define @t23 () (@var "A__questionmark_xu40_19" tptp.c_unsorted)) % 0.43/0.82 (define @t24 () (@var "A__questionmark_v_0_3" tptp.c_sorted)) % 0.43/0.82 (define @t25 () (@var "A__questionmark_xu42_22" tptp.c_unsorted)) % 0.43/0.82 (define @t26 () (@var "A__questionmark_t1u0_21" tptp.c_type)) % 0.43/0.82 (define @t27 () (@var "A__questionmark_yu41_23" tptp.c_unsorted)) % 0.43/0.82 (define @t28 () (@var "A__questionmark_yu44_25" Int)) % 0.43/0.82 (define @t29 () (@var "A__questionmark_xu45_24" Int)) % 0.43/0.82 (define @t30 () (@var "A__questionmark_yu46_27" Int)) % 0.43/0.82 (define @t31 () (@var "A__questionmark_xu47_26" Int)) % 0.43/0.82 (define @t32 () (@var "A__questionmark_yu48_29" Int)) % 0.43/0.82 (define @t33 () (@var "A__questionmark_xu49_28" Int)) % 0.43/0.82 (define @t34 () (@var "A__questionmark_yu50_31" Int)) % 0.43/0.82 (define @t35 () (@var "A__questionmark_xu51_30" Int)) % 0.43/0.82 (define @t36 () (@var "A__questionmark_yu52_33" Int)) % 0.43/0.82 (define @t37 () (@var "A__questionmark_xu53_32" Int)) % 0.43/0.82 (define @t38 () (@var "A__questionmark_yu54_35" Int)) % 0.43/0.82 (define @t39 () (@var "A__questionmark_xu55_34" Int)) % 0.43/0.82 (define @t40 () (@var "A__questionmark_xu56_36" Int)) % 0.43/0.82 (define @t41 () (@var "A__questionmark_xu57_37" Int)) % 0.43/0.82 (define @t42 () (@var "A__questionmark_yu58_39" Int)) % 0.43/0.82 (define @t43 () (@var "A__questionmark_v_0_4" Int)) % 0.43/0.82 (define @t44 () (@var "A__questionmark_xu59_38" Int)) % 0.43/0.82 (define @t45 () (@var "A__questionmark_yu60_41" Int)) % 0.43/0.82 (define @t46 () (@var "A__questionmark_v_0_5" Int)) % 0.43/0.82 (define @t47 () (@var "A__questionmark_xu61_40" Int)) % 0.43/0.82 (define @t48 () (@var "A__questionmark_yu62_43" Int)) % 0.43/0.82 (define @t49 () (@var "A__questionmark_v_0_6" Int)) % 0.43/0.82 (define @t50 () (@var "A__questionmark_xu63_42" Int)) % 0.43/0.82 (define @t51 () (@var "A__questionmark_yu64_45" Int)) % 0.43/0.82 (define @t52 () (@var "A__questionmark_v_0_7" Int)) % 0.43/0.82 (define @t53 () (@var "A__questionmark_xu65_44" Int)) % 0.43/0.82 (define @t54 () (@var "A__questionmark_yu81_47" Real)) % 0.43/0.82 (define @t55 () (@var "A__questionmark_xu82_46" Real)) % 0.43/0.82 (define @t56 () (@var "A__questionmark_yu83_49" Real)) % 0.43/0.82 (define @t57 () (@var "A__questionmark_xu84_48" Real)) % 0.43/0.82 (define @t58 () (@var "A__questionmark_yu85_51" Real)) % 0.43/0.82 (define @t59 () (@var "A__questionmark_xu86_50" Real)) % 0.43/0.82 (define @t60 () (@var "A__questionmark_yu87_53" Real)) % 0.43/0.82 (define @t61 () (@var "A__questionmark_xu88_52" Real)) % 0.43/0.82 (define @t62 () (@var "A__questionmark_yu89_55" Real)) % 0.43/0.82 (define @t63 () (@var "A__questionmark_xu90_54" Real)) % 0.43/0.82 (define @t64 () (@var "A__questionmark_yu91_57" Real)) % 0.43/0.82 (define @t65 () (@var "A__questionmark_xu92_56" Real)) % 0.43/0.82 (define @t66 () (@var "A__questionmark_yu93_59" Real)) % 0.43/0.82 (define @t67 () (@var "A__questionmark_v_0_8" Real)) % 0.43/0.82 (define @t68 () (@var "A__questionmark_xu94_58" Real)) % 0.43/0.82 (define @t69 () (@var "A__questionmark_yu95_61" Real)) % 0.43/0.82 (define @t70 () (@var "A__questionmark_v_0_9" Real)) % 0.43/0.82 (define @t71 () (@var "A__questionmark_xu96_60" Real)) % 0.43/0.82 (define @t72 () (@var "A__questionmark_yu97_63" Real)) % 0.43/0.82 (define @t73 () (@var "A__questionmark_v_0_10" Real)) % 0.43/0.82 (define @t74 () (@var "A__questionmark_xu98_62" Real)) % 0.43/0.82 (define @t75 () (@var "A__questionmark_yu99_65" Real)) % 0.43/0.82 (define @t76 () (@var "A__questionmark_v_0_11" Real)) % 0.43/0.82 (define @t77 () (@var "A__questionmark_xu100_64" Real)) % 0.43/0.82 (define @t78 () (@var "A__questionmark_xu102_66" Real)) % 0.43/0.82 (define @t79 () (@var "A__questionmark_xu103_67" Real)) % 0.43/0.82 (define @t80 () (@var "A__questionmark_xu104_68" Real)) % 0.43/0.82 (define @t81 () (@var "A__questionmark_v_1_13" tptp.c_sorted)) % 0.43/0.82 (define @t82 () (@var "A__questionmark_v_0_12" tptp.c_sorted)) % 0.43/0.82 (define @t83 () (@var "A__questionmark_pu0_71" tptp.c_unsorted)) % 0.43/0.82 (define @t84 () (@var "A__questionmark_t1u0_69" tptp.c_type)) % 0.43/0.82 (define @t85 () (@var "A__questionmark_au0_70" tptp.c_unsorted)) % 0.43/0.82 (define @t86 () (@var "A__questionmark_v_3_16" tptp.c_sorted)) % 0.43/0.82 (define @t87 () (@var "A__questionmark_v_2_17" tptp.c_type)) % 0.43/0.82 (define @t88 () (@var "A__questionmark_v_1_15" tptp.c_sorted)) % 0.43/0.82 (define @t89 () (@var "A__questionmark_t1u0_72" tptp.c_type)) % 0.43/0.82 (define @t90 () (@var "A__questionmark_qu0_74" tptp.c_unsorted)) % 0.43/0.82 (define @t91 () (@var "A__questionmark_v_0_14" tptp.c_type)) % 0.43/0.82 (define @t92 () (@var "A__questionmark_pu0_73" tptp.c_unsorted)) % 0.43/0.82 (define @t93 () (@var "A__questionmark_v_2_20" tptp.c_sorted)) % 0.43/0.82 (define @t94 () (@var "A__questionmark_v_1_19" tptp.c_sorted)) % 0.43/0.82 (define @t95 () (@var "A__questionmark_qu110_77" tptp.c_unsorted)) % 0.43/0.82 (define @t96 () (@var "A__questionmark_v_0_18" tptp.c_type)) % 0.43/0.82 (define @t97 () (@var "A__questionmark_pu111_76" tptp.c_unsorted)) % 0.43/0.82 (define @t98 () (@var "A__questionmark_t1u0_75" tptp.c_type)) % 0.43/0.82 (define @t99 () (@var "A__questionmark_t1u0_78" tptp.c_type)) % 0.43/0.82 (define @t100 () (@var "A__questionmark_pu112_80" tptp.c_unsorted)) % 0.43/0.82 (define @t101 () (@var "A__questionmark_t1u0_79" tptp.c_type)) % 0.43/0.82 (define @t102 () (@var "A__questionmark_ju113_84" Int)) % 0.43/0.82 (define @t103 () (@var "A__questionmark_iu114_83" Int)) % 0.43/0.82 (define @t104 () (@var "A__questionmark_v_1_22" tptp.c_sorted)) % 0.43/0.82 (define @t105 () (@var "A__questionmark_v_0_21" tptp.c_type)) % 0.43/0.82 (define @t106 () (@var "A__questionmark_pu115_82" tptp.c_unsorted)) % 0.43/0.82 (define @t107 () (@var "A__questionmark_t1u0_81" tptp.c_type)) % 0.43/0.82 (define @t108 () (@var "A__questionmark_ju116_88" Int)) % 0.43/0.82 (define @t109 () (@var "A__questionmark_iu117_87" Int)) % 0.43/0.82 (define @t110 () (@var "A__questionmark_v_1_24" tptp.c_sorted)) % 0.43/0.82 (define @t111 () (@var "A__questionmark_v_0_23" tptp.c_type)) % 0.43/0.82 (define @t112 () (@var "A__questionmark_pu118_86" tptp.c_unsorted)) % 0.43/0.82 (define @t113 () (@var "A__questionmark_t1u0_85" tptp.c_type)) % 0.43/0.82 (define @t114 () (@var "A__questionmark_v_1_26" tptp.c_sorted)) % 0.43/0.82 (define @t115 () (@var "A__questionmark_v_0_25" tptp.c_type)) % 0.43/0.82 (define @t116 () (@var "A__questionmark_pu119_90" tptp.c_unsorted)) % 0.43/0.82 (define @t117 () (@var "A__questionmark_t1u0_89" tptp.c_type)) % 0.43/0.82 (define @t118 () (@var "A__questionmark_ju120_94" Int)) % 0.43/0.82 (define @t119 () (@var "A__questionmark_iu121_93" Int)) % 0.43/0.82 (define @t120 () (@var "A__questionmark_v_1_28" tptp.c_sorted)) % 0.43/0.82 (define @t121 () (@var "A__questionmark_v_0_27" tptp.c_type)) % 0.43/0.82 (define @t122 () (@var "A__questionmark_pu122_92" tptp.c_unsorted)) % 0.43/0.82 (define @t123 () (@var "A__questionmark_t1u0_91" tptp.c_type)) % 0.43/0.82 (define @t124 () (@var "A__questionmark_iu123_98" Int)) % 0.43/0.82 (define @t125 () (@var "A__questionmark_v_2_31" tptp.c_sorted)) % 0.43/0.82 (define @t126 () (@var "A__questionmark_v_1_29" tptp.c_sorted)) % 0.43/0.82 (define @t127 () (@var "A__questionmark_v_0_30" tptp.c_type)) % 0.43/0.82 (define @t128 () (@var "A__questionmark_pu124_97" tptp.c_unsorted)) % 0.43/0.82 (define @t129 () (@var "A__questionmark_t1u0_95" tptp.c_type)) % 0.43/0.82 (define @t130 () (@var "A__questionmark_au125_96" tptp.c_unsorted)) % 0.43/0.82 (define @t131 () (@var "A__questionmark_iu126_102" Int)) % 0.43/0.82 (define @t132 () (@var "A__questionmark_v_2_34" tptp.c_sorted)) % 0.43/0.82 (define @t133 () (@var "A__questionmark_v_1_32" tptp.c_sorted)) % 0.43/0.82 (define @t134 () (@var "A__questionmark_v_0_33" tptp.c_type)) % 0.43/0.82 (define @t135 () (@var "A__questionmark_pu127_101" tptp.c_unsorted)) % 0.43/0.82 (define @t136 () (@var "A__questionmark_t1u0_99" tptp.c_type)) % 0.43/0.82 (define @t137 () (@var "A__questionmark_au128_100" tptp.c_unsorted)) % 0.43/0.82 (define @t138 () (@var "A__questionmark_ju129_106" Int)) % 0.43/0.82 (define @t139 () (@var "A__questionmark_v_1_36" tptp.c_sorted)) % 0.43/0.82 (define @t140 () (@var "A__questionmark_v_0_35" tptp.c_type)) % 0.43/0.82 (define @t141 () (@var "A__questionmark_iu130_105" Int)) % 0.43/0.82 (define @t142 () (@var "A__questionmark_pu131_104" tptp.c_unsorted)) % 0.43/0.82 (define @t143 () (@var "A__questionmark_t1u0_103" tptp.c_type)) % 0.43/0.82 (define @t144 () (@var "A__questionmark_t1u0_107" tptp.c_type)) % 0.43/0.82 (define @t145 () (@var "A__questionmark_au132_108" tptp.c_unsorted)) % 0.43/0.82 (define @t146 () (@var "A__questionmark_v_1_38" tptp.c_sorted)) % 0.43/0.82 (define @t147 () (@var "A__questionmark_v_0_37" tptp.c_sorted)) % 0.43/0.82 (define @t148 () (@var "A__questionmark_t1u0_109" tptp.c_type)) % 0.43/0.82 (define @t149 () (@var "A__questionmark_au133_110" tptp.c_unsorted)) % 0.43/0.82 (define @t150 () (@var "A__questionmark_v_2_41" tptp.c_sorted)) % 0.43/0.82 (define @t151 () (@var "A__questionmark_v_1_40" tptp.c_sorted)) % 0.43/0.82 (define @t152 () (@var "A__questionmark_p2u142_113" tptp.c_unsorted)) % 0.43/0.82 (define @t153 () (@var "A__questionmark_v_0_39" tptp.c_type)) % 0.43/0.82 (define @t154 () (@var "A__questionmark_p1u143_112" tptp.c_unsorted)) % 0.43/0.82 (define @t155 () (@var "A__questionmark_t1u0_111" tptp.c_type)) % 0.43/0.82 (define @t156 () (@var "A__questionmark_v_2_44" tptp.c_sorted)) % 0.43/0.82 (define @t157 () (@var "A__questionmark_v_1_43" tptp.c_sorted)) % 0.43/0.82 (define @t158 () (@var "A__questionmark_p2u144_116" tptp.c_unsorted)) % 0.43/0.82 (define @t159 () (@var "A__questionmark_v_0_42" tptp.c_type)) % 0.43/0.82 (define @t160 () (@var "A__questionmark_p1u145_115" tptp.c_unsorted)) % 0.43/0.82 (define @t161 () (@var "A__questionmark_t1u0_114" tptp.c_type)) % 0.43/0.82 (define @t162 () (@var "A__questionmark_iu146_120" Int)) % 0.43/0.82 (define @t163 () (@var "A__questionmark_v_2_47" tptp.c_sorted)) % 0.43/0.82 (define @t164 () (@var "A__questionmark_v_0_45" tptp.c_type)) % 0.43/0.82 (define @t165 () (@var "A__questionmark_v_1_46" tptp.c_sorted)) % 0.43/0.82 (define @t166 () (@var "A__questionmark_qu147_119" tptp.c_unsorted)) % 0.43/0.82 (define @t167 () (@var "A__questionmark_pu148_118" tptp.c_unsorted)) % 0.43/0.82 (define @t168 () (@var "A__questionmark_t1u0_117" tptp.c_type)) % 0.43/0.82 (define @t169 () (@var "A__questionmark_v_2_50" tptp.c_sorted)) % 0.43/0.82 (define @t170 () (@var "A__questionmark_iu149_124" Int)) % 0.43/0.82 (define @t171 () (@var "A__questionmark_v_1_49" tptp.c_sorted)) % 0.43/0.82 (define @t172 () (@var "A__questionmark_v_0_48" tptp.c_type)) % 0.43/0.82 (define @t173 () (@var "A__questionmark_pu151_122" tptp.c_unsorted)) % 0.43/0.82 (define @t174 () (@var "A__questionmark_qu150_123" tptp.c_unsorted)) % 0.43/0.82 (define @t175 () (@var "A__questionmark_t1u0_121" tptp.c_type)) % 0.43/0.82 (define @t176 () (@var "A__questionmark_v_2_53" tptp.c_sorted)) % 0.43/0.82 (define @t177 () (@var "A__questionmark_v_1_52" tptp.c_sorted)) % 0.43/0.82 (define @t178 () (@var "A__questionmark_v_0_51" tptp.c_type)) % 0.43/0.82 (define @t179 () (@var "A__questionmark_qu152_127" tptp.c_unsorted)) % 0.43/0.82 (define @t180 () (@var "A__questionmark_pu153_126" tptp.c_unsorted)) % 0.43/0.82 (define @t181 () (@var "A__questionmark_t1u0_125" tptp.c_type)) % 0.43/0.82 (define @t182 () (@var "A__questionmark_v_0_54" tptp.c_sorted)) % 0.43/0.82 (define @t183 () (@var "A__questionmark_pu154_129" tptp.c_unsorted)) % 0.43/0.82 (define @t184 () (@var "A__questionmark_t1u0_128" tptp.c_type)) % 0.43/0.82 (define @t185 () (@var "A__questionmark_v_2_57" tptp.c_sorted)) % 0.43/0.82 (define @t186 () (@var "A__questionmark_v_1_56" tptp.c_sorted)) % 0.43/0.82 (define @t187 () (@var "A__questionmark_qu155_132" tptp.c_unsorted)) % 0.43/0.82 (define @t188 () (@var "A__questionmark_v_0_55" tptp.c_type)) % 0.43/0.82 (define @t189 () (@var "A__questionmark_pu156_131" tptp.c_unsorted)) % 0.43/0.82 (define @t190 () (@var "A__questionmark_t1u0_130" tptp.c_type)) % 0.43/0.82 (define @t191 () (@var "A__questionmark_iu157_136" Int)) % 0.43/0.82 (define @t192 () (@var "A__questionmark_v_2_60" tptp.c_sorted)) % 0.43/0.82 (define @t193 () (@var "A__questionmark_v_1_59" tptp.c_sorted)) % 0.43/0.82 (define @t194 () (@var "A__questionmark_v_0_58" tptp.c_type)) % 0.43/0.82 (define @t195 () (@var "A__questionmark_qu158_135" tptp.c_unsorted)) % 0.43/0.82 (define @t196 () (@var "A__questionmark_pu159_134" tptp.c_unsorted)) % 0.43/0.82 (define @t197 () (@var "A__questionmark_t1u0_133" tptp.c_type)) % 0.43/0.82 (define @t198 () (@var "A__questionmark_iu160_140" Int)) % 0.43/0.82 (define @t199 () (@var "A__questionmark_v_2_63" tptp.c_sorted)) % 0.43/0.82 (define @t200 () (@var "A__questionmark_v_1_62" tptp.c_sorted)) % 0.43/0.82 (define @t201 () (@var "A__questionmark_v_0_61" tptp.c_type)) % 0.43/0.82 (define @t202 () (@var "A__questionmark_qu161_139" tptp.c_unsorted)) % 0.43/0.82 (define @t203 () (@var "A__questionmark_pu162_138" tptp.c_unsorted)) % 0.43/0.82 (define @t204 () (@var "A__questionmark_t1u0_137" tptp.c_type)) % 0.43/0.82 (define @t205 () (@var "A__questionmark_v_4_68" tptp.c_sorted)) % 0.43/0.82 (define @t206 () (@var "A__questionmark_v_3_66" tptp.c_sorted)) % 0.43/0.82 (define @t207 () (@var "A__questionmark_v_2_65" tptp.c_sorted)) % 0.43/0.82 (define @t208 () (@var "A__questionmark_mu166_143" tptp.c_unsorted)) % 0.43/0.82 (define @t209 () (@var "A__questionmark_v_1_67" tptp.c_type)) % 0.43/0.82 (define @t210 () (@var "A__questionmark_t2u0_141" tptp.c_type)) % 0.43/0.82 (define @t211 () (@var "A__questionmark_au163_146" tptp.c_unsorted)) % 0.43/0.82 (define @t212 () (@var "A__questionmark_t1u0_142" tptp.c_type)) % 0.43/0.82 (define @t213 () (@var "A__questionmark_p2u164_145" tptp.c_unsorted)) % 0.43/0.82 (define @t214 () (@var "A__questionmark_v_0_64" tptp.c_type)) % 0.43/0.82 (define @t215 () (@var "A__questionmark_p1u165_144" tptp.c_unsorted)) % 0.43/0.82 (define @t216 () (@var "A__questionmark_v_3_71" tptp.c_sorted)) % 0.43/0.82 (define @t217 () (@var "A__questionmark_v_4_73" tptp.c_sorted)) % 0.43/0.82 (define @t218 () (@var "A__questionmark_t2u0_147" tptp.c_type)) % 0.43/0.82 (define @t219 () (@var "A__questionmark_au167_152" tptp.c_unsorted)) % 0.43/0.82 (define @t220 () (@var "A__questionmark_v_2_70" tptp.c_sorted)) % 0.43/0.82 (define @t221 () (@var "A__questionmark_v_1_72" tptp.c_type)) % 0.43/0.82 (define @t222 () (@var "A__questionmark_mu170_149" tptp.c_unsorted)) % 0.43/0.82 (define @t223 () (@var "A__questionmark_t1u0_148" tptp.c_type)) % 0.43/0.82 (define @t224 () (@var "A__questionmark_p2u168_151" tptp.c_unsorted)) % 0.43/0.82 (define @t225 () (@var "A__questionmark_v_0_69" tptp.c_type)) % 0.43/0.82 (define @t226 () (@var "A__questionmark_p1u169_150" tptp.c_unsorted)) % 0.43/0.82 (define @t227 () (@var "A__questionmark_ps2u0_155" tptp.c_unsorted)) % 0.43/0.82 (define @t228 () (@var "A__questionmark_v_0_74" tptp.c_type)) % 0.43/0.82 (define @t229 () (tptp.c_sort @t228 @t227)) % 0.43/0.82 (define @t230 () (@var "A__questionmark_v_1_75" tptp.c_sorted)) % 0.43/0.82 (define @t231 () (@var "A__questionmark_ps1u0_154" tptp.c_unsorted)) % 0.43/0.82 (define @t232 () (tptp.c_sort @t228 @t231)) % 0.43/0.82 (define @t233 () (@var "A__questionmark_pu261_156" tptp.c_unsorted)) % 0.43/0.82 (define @t234 () (@var "A__questionmark_t1u0_153" tptp.c_type)) % 0.43/0.82 (define @t235 () (@var "A__questionmark_ps2u0_159" tptp.c_unsorted)) % 0.43/0.82 (define @t236 () (@var "A__questionmark_v_0_76" tptp.c_type)) % 0.43/0.82 (define @t237 () (tptp.c_sort @t236 @t235)) % 0.43/0.82 (define @t238 () (@var "A__questionmark_v_1_77" tptp.c_sorted)) % 0.43/0.82 (define @t239 () (@var "A__questionmark_ps1u0_158" tptp.c_unsorted)) % 0.43/0.82 (define @t240 () (tptp.c_sort @t236 @t239)) % 0.43/0.82 (define @t241 () (@var "A__questionmark_pu262_160" tptp.c_unsorted)) % 0.43/0.82 (define @t242 () (@var "A__questionmark_t1u0_157" tptp.c_type)) % 0.43/0.82 (define @t243 () (@var "A__questionmark_v_0_78" tptp.c_sorted)) % 0.43/0.82 (define @t244 () (@var "A__questionmark_psu263_162" tptp.c_unsorted)) % 0.43/0.82 (define @t245 () (@var "A__questionmark_t1u0_161" tptp.c_type)) % 0.43/0.82 (define @t246 () (@var "A__questionmark_du264_168" Int)) % 0.43/0.82 (define @t247 () (@var "A__questionmark_cu265_167" Int)) % 0.43/0.82 (define @t248 () (@var "A__questionmark_v_1_80" tptp.c_sorted)) % 0.43/0.82 (define @t249 () (@var "A__questionmark_v_0_79" tptp.c_type)) % 0.43/0.82 (define @t250 () (@var "A__questionmark_bu266_166" Int)) % 0.43/0.82 (define @t251 () (@var "A__questionmark_au267_165" Int)) % 0.43/0.82 (define @t252 () (@var "A__questionmark_psu268_164" tptp.c_unsorted)) % 0.43/0.82 (define @t253 () (@var "A__questionmark_t1u0_163" tptp.c_type)) % 0.43/0.82 (define @t254 () (@var "A__questionmark_v_1_82" tptp.c_sorted)) % 0.43/0.82 (define @t255 () (@var "A__questionmark_v_0_81" tptp.c_type)) % 0.43/0.82 (define @t256 () (@var "A__questionmark_bu271_172" Int)) % 0.43/0.82 (define @t257 () (@var "A__questionmark_au272_171" Int)) % 0.43/0.82 (define @t258 () (@var "A__questionmark_psu273_170" tptp.c_unsorted)) % 0.43/0.82 (define @t259 () (@var "A__questionmark_t1u0_169" tptp.c_type)) % 0.43/0.82 (define @t260 () (@var "A__questionmark_t1u0_175" tptp.c_type)) % 0.43/0.82 (define @t261 () (@var "A__questionmark_pu274_176" tptp.c_unsorted)) % 0.43/0.82 (define @t262 () (@var "A__questionmark_v_2_85" tptp.c_sorted)) % 0.43/0.82 (define @t263 () (@var "A__questionmark_v_1_84" tptp.c_sorted)) % 0.43/0.82 (define @t264 () (@var "A__questionmark_t1u0_177" tptp.c_type)) % 0.43/0.82 (define @t265 () (@var "A__questionmark_qu275_179" tptp.c_unsorted)) % 0.43/0.82 (define @t266 () (@var "A__questionmark_v_0_83" tptp.c_type)) % 0.43/0.82 (define @t267 () (@var "A__questionmark_pu276_178" tptp.c_unsorted)) % 0.43/0.82 (define @t268 () (@var "A__questionmark_v_1_87" tptp.c_sorted)) % 0.43/0.82 (define @t269 () (@var "A__questionmark_mu279_183" tptp.c_unsorted)) % 0.43/0.82 (define @t270 () (@var "A__questionmark_v_0_86" tptp.c_type)) % 0.43/0.82 (define @t271 () (@var "A__questionmark_t2u0_180" tptp.c_type)) % 0.43/0.82 (define @t272 () (tptp.c_sort (tptp.memory @t271 @t270) @t269)) % 0.43/0.82 (define @t273 () (@var "A__questionmark_pu280_182" tptp.c_unsorted)) % 0.43/0.82 (define @t274 () (tptp.c_sort @t270 @t273)) % 0.43/0.82 (define @t275 () (@var "A__questionmark_qu278_184" tptp.c_unsorted)) % 0.43/0.82 (define @t276 () (tptp.c_sort (tptp.pset @t271) @t275)) % 0.43/0.82 (define @t277 () (@var "A__questionmark_ru277_185" tptp.c_unsorted)) % 0.43/0.82 (define @t278 () (@var "A__questionmark_t1u0_181" tptp.c_type)) % 0.43/0.82 (define @t279 () (@var "A__questionmark_iu282_189" Int)) % 0.43/0.82 (define @t280 () (@var "A__questionmark_v_2_90" tptp.c_sorted)) % 0.43/0.82 (define @t281 () (@var "A__questionmark_v_1_89" tptp.c_type)) % 0.43/0.82 (define @t282 () (@var "A__questionmark_pu284_187" tptp.c_unsorted)) % 0.43/0.82 (define @t283 () (@var "A__questionmark_qu283_188" tptp.c_unsorted)) % 0.43/0.82 (define @t284 () (@var "A__questionmark_v_0_88" tptp.c_type)) % 0.43/0.82 (define @t285 () (tptp.c_sort @t284 @t283)) % 0.43/0.82 (define @t286 () (@var "A__questionmark_ru281_190" tptp.c_unsorted)) % 0.43/0.82 (define @t287 () (@var "A__questionmark_t1u0_186" tptp.c_type)) % 0.43/0.82 (define @t288 () (tptp.pointer @t287)) % 0.43/0.82 (define @t289 () (@var "A__questionmark_iu286_196" Int)) % 0.43/0.82 (define @t290 () (@var "A__questionmark_v_2_93" tptp.c_sorted)) % 0.43/0.82 (define @t291 () (@var "A__questionmark_v_1_92" tptp.c_type)) % 0.43/0.82 (define @t292 () (@var "A__questionmark_pu290_192" tptp.c_unsorted)) % 0.43/0.82 (define @t293 () (@var "A__questionmark_qu289_193" tptp.c_unsorted)) % 0.43/0.82 (define @t294 () (@var "A__questionmark_v_0_91" tptp.c_type)) % 0.43/0.82 (define @t295 () (tptp.c_sort @t294 @t293)) % 0.43/0.82 (define @t296 () (@var "A__questionmark_bu287_195" Int)) % 0.43/0.82 (define @t297 () (@var "A__questionmark_au288_194" Int)) % 0.43/0.82 (define @t298 () (@var "A__questionmark_ru285_197" tptp.c_unsorted)) % 0.43/0.82 (define @t299 () (@var "A__questionmark_t1u0_191" tptp.c_type)) % 0.43/0.82 (define @t300 () (tptp.pointer @t299)) % 0.43/0.82 (define @t301 () (@var "A__questionmark_iu292_202" Int)) % 0.43/0.82 (define @t302 () (@var "A__questionmark_v_2_96" tptp.c_sorted)) % 0.43/0.82 (define @t303 () (@var "A__questionmark_v_1_95" tptp.c_type)) % 0.43/0.82 (define @t304 () (@var "A__questionmark_pu295_199" tptp.c_unsorted)) % 0.43/0.82 (define @t305 () (@var "A__questionmark_qu294_200" tptp.c_unsorted)) % 0.43/0.82 (define @t306 () (@var "A__questionmark_v_0_94" tptp.c_type)) % 0.43/0.82 (define @t307 () (tptp.c_sort @t306 @t305)) % 0.43/0.82 (define @t308 () (@var "A__questionmark_bu293_201" Int)) % 0.43/0.82 (define @t309 () (@var "A__questionmark_ru291_203" tptp.c_unsorted)) % 0.43/0.82 (define @t310 () (@var "A__questionmark_t1u0_198" tptp.c_type)) % 0.43/0.82 (define @t311 () (tptp.pointer @t310)) % 0.43/0.82 (define @t312 () (@var "A__questionmark_iu297_208" Int)) % 0.43/0.82 (define @t313 () (@var "A__questionmark_v_2_99" tptp.c_sorted)) % 0.43/0.82 (define @t314 () (@var "A__questionmark_v_1_98" tptp.c_type)) % 0.43/0.82 (define @t315 () (@var "A__questionmark_pu300_205" tptp.c_unsorted)) % 0.43/0.82 (define @t316 () (@var "A__questionmark_qu299_206" tptp.c_unsorted)) % 0.43/0.82 (define @t317 () (@var "A__questionmark_v_0_97" tptp.c_type)) % 0.43/0.82 (define @t318 () (tptp.c_sort @t317 @t316)) % 0.43/0.82 (define @t319 () (@var "A__questionmark_au298_207" Int)) % 0.43/0.82 (define @t320 () (@var "A__questionmark_ru296_209" tptp.c_unsorted)) % 0.43/0.82 (define @t321 () (@var "A__questionmark_t1u0_204" tptp.c_type)) % 0.43/0.82 (define @t322 () (tptp.pointer @t321)) % 0.43/0.82 (define @t323 () (@var "A__questionmark_v_3_103" tptp.c_sorted)) % 0.43/0.82 (define @t324 () (@var "A__questionmark_v_1_100" tptp.c_sorted)) % 0.43/0.82 (define @t325 () (@var "A__questionmark_v_2_102" tptp.c_sorted)) % 0.43/0.82 (define @t326 () (@var "A__questionmark_v_0_101" tptp.c_type)) % 0.43/0.82 (define @t327 () (@var "A__questionmark_s2u301_213" tptp.c_unsorted)) % 0.43/0.82 (define @t328 () (@var "A__questionmark_s1u302_212" tptp.c_unsorted)) % 0.43/0.82 (define @t329 () (@var "A__questionmark_t1u0_210" tptp.c_type)) % 0.43/0.82 (define @t330 () (@var "A__questionmark_pu303_211" tptp.c_unsorted)) % 0.43/0.82 (define @t331 () (@var "A__questionmark_t1u0_214" tptp.c_type)) % 0.43/0.82 (define @t332 () (@var "A__questionmark_au304_215" tptp.c_unsorted)) % 0.43/0.82 (define @t333 () (@var "A__questionmark_v_1_105" tptp.c_sorted)) % 0.43/0.82 (define @t334 () (@var "A__questionmark_v_0_104" tptp.c_sorted)) % 0.43/0.82 (define @t335 () (@var "A__questionmark_t1u0_216" tptp.c_type)) % 0.43/0.82 (define @t336 () (@var "A__questionmark_pu305_218" tptp.c_unsorted)) % 0.43/0.82 (define @t337 () (@var "A__questionmark_au306_217" tptp.c_unsorted)) % 0.43/0.82 (define @t338 () (@var "A__questionmark_v_2_108" tptp.c_sorted)) % 0.43/0.82 (define @t339 () (@var "A__questionmark_au311_221" tptp.c_unsorted)) % 0.43/0.82 (define @t340 () (@var "A__questionmark_t1u0_220" tptp.c_type)) % 0.43/0.82 (define @t341 () (tptp.c_sort (tptp.alloc_table @t340) @t339)) % 0.43/0.82 (define @t342 () (@var "A__questionmark_v_1_107" tptp.c_sorted)) % 0.43/0.82 (define @t343 () (@var "A__questionmark_mu310_222" tptp.c_unsorted)) % 0.43/0.82 (define @t344 () (@var "A__questionmark_v_0_106" tptp.c_type)) % 0.43/0.82 (define @t345 () (@var "A__questionmark_t2u0_219" tptp.c_type)) % 0.43/0.82 (define @t346 () (@var "A__questionmark_qu309_223" tptp.c_unsorted)) % 0.43/0.82 (define @t347 () (tptp.c_sort (tptp.pset @t345) @t346)) % 0.43/0.82 (define @t348 () (@var "A__questionmark_pu307_225" tptp.c_unsorted)) % 0.43/0.82 (define @t349 () (@var "A__questionmark_ru308_224" tptp.c_unsorted)) % 0.43/0.82 (define @t350 () (tptp.pointer @t340)) % 0.43/0.82 (define @t351 () (@var "A__questionmark_iu313_231" Int)) % 0.43/0.82 (define @t352 () (@var "A__questionmark_v_2_111" tptp.c_sorted)) % 0.43/0.82 (define @t353 () (@var "A__questionmark_v_1_110" tptp.c_type)) % 0.43/0.82 (define @t354 () (@var "A__questionmark_au317_227" tptp.c_unsorted)) % 0.43/0.82 (define @t355 () (@var "A__questionmark_t1u0_226" tptp.c_type)) % 0.43/0.82 (define @t356 () (tptp.c_sort (tptp.alloc_table @t355) @t354)) % 0.43/0.82 (define @t357 () (@var "A__questionmark_du314_230" Int)) % 0.43/0.82 (define @t358 () (@var "A__questionmark_cu315_229" Int)) % 0.43/0.82 (define @t359 () (@var "A__questionmark_qu316_228" tptp.c_unsorted)) % 0.43/0.82 (define @t360 () (@var "A__questionmark_v_0_109" tptp.c_type)) % 0.43/0.82 (define @t361 () (tptp.c_sort @t360 @t359)) % 0.43/0.82 (define @t362 () (@var "A__questionmark_ru312_232" tptp.c_unsorted)) % 0.43/0.82 (define @t363 () (@var "A__questionmark_v_3_115" tptp.c_sorted)) % 0.43/0.82 (define @t364 () (@var "A__questionmark_v_1_112" tptp.c_sorted)) % 0.43/0.82 (define @t365 () (@var "A__questionmark_v_2_114" tptp.c_sorted)) % 0.43/0.82 (define @t366 () (@var "A__questionmark_v_0_113" tptp.c_type)) % 0.43/0.82 (define @t367 () (@var "A__questionmark_s2u318_236" tptp.c_unsorted)) % 0.43/0.82 (define @t368 () (@var "A__questionmark_s1u319_235" tptp.c_unsorted)) % 0.43/0.82 (define @t369 () (@var "A__questionmark_t1u0_233" tptp.c_type)) % 0.43/0.82 (define @t370 () (@var "A__questionmark_au320_234" tptp.c_unsorted)) % 0.43/0.82 (define @t371 () (@var "A__questionmark_v_1_117" tptp.c_sorted)) % 0.43/0.82 (define @t372 () (@var "A__questionmark_m1u0_240" tptp.c_unsorted)) % 0.43/0.82 (define @t373 () (@var "A__questionmark_v_0_116" tptp.c_type)) % 0.43/0.82 (define @t374 () (tptp.c_sort @t373 @t372)) % 0.43/0.82 (define @t375 () (@var "A__questionmark_t2u0_237" tptp.c_type)) % 0.43/0.82 (define @t376 () (@var "A__questionmark_m2u0_241" tptp.c_unsorted)) % 0.43/0.82 (define @t377 () (tptp.c_sort @t373 @t376)) % 0.43/0.82 (define @t378 () (@var "A__questionmark_lu0_242" tptp.c_unsorted)) % 0.43/0.82 (define @t379 () (@var "A__questionmark_t1u0_238" tptp.c_type)) % 0.43/0.82 (define @t380 () (tptp.c_sort (tptp.pset @t379) @t378)) % 0.43/0.82 (define @t381 () (@var "A__questionmark_au0_239" tptp.c_unsorted)) % 0.43/0.82 (define @t382 () (tptp.c_sort (tptp.alloc_table @t379) @t381)) % 0.43/0.82 (define @t383 () (@var "A__questionmark_pu321_243" tptp.c_unsorted)) % 0.43/0.82 (define @t384 () (@var "A__questionmark_lu322_248" tptp.c_unsorted)) % 0.43/0.82 (define @t385 () (@var "A__questionmark_t1u0_245" tptp.c_type)) % 0.43/0.82 (define @t386 () (@var "A__questionmark_v_0_118" tptp.c_sorted)) % 0.43/0.82 (define @t387 () (@var "A__questionmark_au324_246" tptp.c_unsorted)) % 0.43/0.82 (define @t388 () (@var "A__questionmark_mu323_247" tptp.c_unsorted)) % 0.43/0.82 (define @t389 () (@var "A__questionmark_t2u0_244" tptp.c_type)) % 0.43/0.82 (define @t390 () (@var "A__questionmark_v_3_123" tptp.c_sorted)) % 0.43/0.82 (define @t391 () (@var "A__questionmark_v_5_124" tptp.c_sorted)) % 0.43/0.82 (define @t392 () (@var "A__questionmark_v_4_121" tptp.c_sorted)) % 0.43/0.82 (define @t393 () (@var "A__questionmark_v_1_119" tptp.c_sorted)) % 0.43/0.82 (define @t394 () (@var "A__questionmark_v_2_122" tptp.c_sorted)) % 0.43/0.82 (define @t395 () (@var "A__questionmark_m3u326_254" tptp.c_unsorted)) % 0.43/0.82 (define @t396 () (@var "A__questionmark_v_0_120" tptp.c_type)) % 0.43/0.82 (define @t397 () (@var "A__questionmark_lu325_255" tptp.c_unsorted)) % 0.43/0.82 (define @t398 () (@var "A__questionmark_t1u0_250" tptp.c_type)) % 0.43/0.82 (define @t399 () (@var "A__questionmark_m2u327_253" tptp.c_unsorted)) % 0.43/0.82 (define @t400 () (@var "A__questionmark_m1u328_252" tptp.c_unsorted)) % 0.43/0.82 (define @t401 () (@var "A__questionmark_t2u0_249" tptp.c_type)) % 0.43/0.82 (define @t402 () (@var "A__questionmark_au329_251" tptp.c_unsorted)) % 0.43/0.82 (define @t403 () (@var "A__questionmark_iu330_259" Int)) % 0.43/0.82 (define @t404 () (@var "A__questionmark_v_2_127" tptp.c_sorted)) % 0.43/0.82 (define @t405 () (@var "A__questionmark_v_0_125" tptp.c_type)) % 0.43/0.82 (define @t406 () (@var "A__questionmark_v_1_126" tptp.c_sorted)) % 0.43/0.82 (define @t407 () (@var "A__questionmark_qu331_258" tptp.c_unsorted)) % 0.43/0.82 (define @t408 () (@var "A__questionmark_pu332_257" tptp.c_unsorted)) % 0.43/0.82 (define @t409 () (@var "A__questionmark_t1u0_256" tptp.c_type)) % 0.43/0.82 (define @t410 () (@var "A__questionmark_v_2_129" tptp.c_sorted)) % 0.43/0.82 (define @t411 () (@var "A__questionmark_iu333_263" Int)) % 0.43/0.82 (define @t412 () (@var "A__questionmark_v_1_130" tptp.c_sorted)) % 0.43/0.82 (define @t413 () (@var "A__questionmark_v_0_128" tptp.c_type)) % 0.43/0.82 (define @t414 () (@var "A__questionmark_qu334_262" tptp.c_unsorted)) % 0.43/0.82 (define @t415 () (@var "A__questionmark_pu335_261" tptp.c_unsorted)) % 0.43/0.82 (define @t416 () (@var "A__questionmark_t1u0_260" tptp.c_type)) % 0.43/0.82 (define @t417 () (@var "A__questionmark_v_2_133" tptp.c_sorted)) % 0.43/0.82 (define @t418 () (@var "A__questionmark_iu336_267" Int)) % 0.43/0.82 (define @t419 () (@var "A__questionmark_v_1_132" tptp.c_sorted)) % 0.43/0.82 (define @t420 () (@var "A__questionmark_v_0_131" tptp.c_type)) % 0.43/0.82 (define @t421 () (@var "A__questionmark_pu338_265" tptp.c_unsorted)) % 0.43/0.82 (define @t422 () (@var "A__questionmark_qu337_266" tptp.c_unsorted)) % 0.43/0.82 (define @t423 () (@var "A__questionmark_t1u0_264" tptp.c_type)) % 0.43/0.82 (define @t424 () (@var "A__questionmark_iu339_271" Int)) % 0.43/0.82 (define @t425 () (@var "A__questionmark_v_2_135" tptp.c_sorted)) % 0.43/0.82 (define @t426 () (@var "A__questionmark_v_0_134" tptp.c_type)) % 0.43/0.82 (define @t427 () (@var "A__questionmark_v_1_136" tptp.c_sorted)) % 0.43/0.82 (define @t428 () (@var "A__questionmark_pu341_269" tptp.c_unsorted)) % 0.43/0.82 (define @t429 () (@var "A__questionmark_qu340_270" tptp.c_unsorted)) % 0.43/0.82 (define @t430 () (@var "A__questionmark_t1u0_268" tptp.c_type)) % 0.43/0.82 (define @t431 () (@var "A__questionmark_v_2_139" tptp.c_sorted)) % 0.43/0.82 (define @t432 () (@var "A__questionmark_v_1_138" tptp.c_sorted)) % 0.43/0.82 (define @t433 () (@var "A__questionmark_t2u342_274" tptp.c_unsorted)) % 0.43/0.82 (define @t434 () (@var "A__questionmark_v_0_137" tptp.c_type)) % 0.43/0.82 (define @t435 () (@var "A__questionmark_t1u343_273" tptp.c_unsorted)) % 0.43/0.82 (define @t436 () (@var "A__questionmark_t1u0_272" tptp.c_type)) % 0.43/0.82 (define @t437 () (@var "A__questionmark_v_0_140" tptp.c_sorted)) % 0.43/0.82 (define @t438 () (@var "A__questionmark_tu344_276" tptp.c_unsorted)) % 0.43/0.82 (define @t439 () (@var "A__questionmark_t1u0_275" tptp.c_type)) % 0.43/0.82 (define @t440 () (@var "A__questionmark_v_3_144" tptp.c_sorted)) % 0.43/0.82 (define @t441 () (@var "A__questionmark_v_2_142" tptp.c_sorted)) % 0.43/0.82 (define @t442 () (@var "A__questionmark_v_1_143" tptp.c_sorted)) % 0.43/0.82 (define @t443 () (@var "A__questionmark_t3u345_280" tptp.c_unsorted)) % 0.43/0.82 (define @t444 () (@var "A__questionmark_v_0_141" tptp.c_type)) % 0.43/0.82 (define @t445 () (@var "A__questionmark_t2u346_279" tptp.c_unsorted)) % 0.43/0.82 (define @t446 () (@var "A__questionmark_t1u347_278" tptp.c_unsorted)) % 0.43/0.82 (define @t447 () (@var "A__questionmark_t1u0_277" tptp.c_type)) % 0.43/0.82 (define @t448 () (@var "A__questionmark_v_3_148" tptp.c_sorted)) % 0.43/0.82 (define @t449 () (@var "A__questionmark_v_2_146" tptp.c_sorted)) % 0.43/0.82 (define @t450 () (@var "A__questionmark_v_1_145" tptp.c_sorted)) % 0.43/0.82 (define @t451 () (@var "A__questionmark_v_0_147" tptp.c_type)) % 0.43/0.82 (define @t452 () (@var "A__questionmark_tu0_284" tptp.c_unsorted)) % 0.43/0.82 (define @t453 () (@var "A__questionmark_t1u0_281" tptp.c_type)) % 0.43/0.82 (define @t454 () (@var "A__questionmark_pu0_283" tptp.c_unsorted)) % 0.43/0.82 (define @t455 () (@var "A__questionmark_au0_282" tptp.c_unsorted)) % 0.43/0.82 (define @t456 () (@var "A__questionmark_v_2_151" tptp.c_sorted)) % 0.43/0.82 (define @t457 () (@var "A__questionmark_v_3_152" tptp.c_sorted)) % 0.43/0.82 (define @t458 () (@var "A__questionmark_v_1_149" tptp.c_sorted)) % 0.43/0.82 (define @t459 () (@var "A__questionmark_v_0_150" tptp.c_type)) % 0.43/0.82 (define @t460 () (@var "A__questionmark_su351_288" tptp.c_unsorted)) % 0.43/0.82 (define @t461 () (@var "A__questionmark_t1u0_285" tptp.c_type)) % 0.43/0.82 (define @t462 () (@var "A__questionmark_pu352_287" tptp.c_unsorted)) % 0.43/0.82 (define @t463 () (@var "A__questionmark_au353_286" tptp.c_unsorted)) % 0.43/0.82 (define @t464 () (@var "A__questionmark_v_0_153" tptp.c_type)) % 0.43/0.82 (define @t465 () (@var "A__questionmark_tu360_290" tptp.c_unsorted)) % 0.43/0.82 (define @t466 () (@var "A__questionmark_t1u0_289" tptp.c_type)) % 0.43/0.82 (define @t467 () (@var "A__questionmark_v_1_154" tptp.c_type)) % 0.43/0.82 (define @t468 () (@var "A__questionmark_v_0_155" tptp.c_sorted)) % 0.43/0.82 (define @t469 () (@var "A__questionmark_tu0_292" tptp.c_unsorted)) % 0.43/0.82 (define @t470 () (@var "A__questionmark_t1u0_291" tptp.c_type)) % 0.43/0.82 (define @t471 () (@var "A__questionmark_v_2_158" tptp.c_sorted)) % 0.43/0.82 (define @t472 () (@var "A__questionmark_v_3_159" tptp.c_sorted)) % 0.43/0.82 (define @t473 () (@var "A__questionmark_v_1_157" tptp.c_sorted)) % 0.43/0.82 (define @t474 () (@var "A__questionmark_cu361_296" tptp.c_unsorted)) % 0.43/0.82 (define @t475 () (@var "A__questionmark_v_0_156" tptp.c_type)) % 0.43/0.82 (define @t476 () (@var "A__questionmark_bu362_295" tptp.c_unsorted)) % 0.43/0.82 (define @t477 () (@var "A__questionmark_au363_294" tptp.c_unsorted)) % 0.43/0.82 (define @t478 () (@var "A__questionmark_t1u0_293" tptp.c_type)) % 0.43/0.82 (define @t479 () (@var "A__questionmark_v_2_163" tptp.c_sorted)) % 0.43/0.82 (define @t480 () (@var "A__questionmark_v_3_160" tptp.c_sorted)) % 0.43/0.82 (define @t481 () (@var "A__questionmark_v_0_161" tptp.c_type)) % 0.43/0.82 (define @t482 () (@var "A__questionmark_v_1_162" tptp.c_sorted)) % 0.43/0.82 (define @t483 () (@var "A__questionmark_thisu0_300" tptp.c_unsorted)) % 0.43/0.82 (define @t484 () (@var "A__questionmark_t1u0_297" tptp.c_type)) % 0.43/0.82 (define @t485 () (@var "A__questionmark_mutableu0_299" tptp.c_unsorted)) % 0.43/0.82 (define @t486 () (@var "A__questionmark_tagutableu0_298" tptp.c_unsorted)) % 0.43/0.82 (define @t487 () (@var "A__questionmark_bu368_302" Int)) % 0.43/0.82 (define @t488 () (@var "A__questionmark_au369_301" Int)) % 0.43/0.82 (define @t489 () (@var "A__questionmark_bu370_304" Int)) % 0.43/0.82 (define @t490 () (@var "A__questionmark_au371_303" Int)) % 0.43/0.82 (define @t491 () (@var "A__questionmark_bu372_307" Int)) % 0.43/0.82 (define @t492 () (@var "A__questionmark_a2u373_306" Int)) % 0.43/0.82 (define @t493 () (@var "A__questionmark_a1u374_305" Int)) % 0.43/0.82 (define @t494 () (@var "A__questionmark_bu375_309" Int)) % 0.43/0.82 (define @t495 () (@var "A__questionmark_au376_308" Int)) % 0.43/0.82 (define @t496 () (@var "A__questionmark_au378_310" Int)) % 0.43/0.82 (define @t497 () (@var "A__questionmark_bu377_311" Int)) % 0.43/0.82 (define @t498 () (@var "A__questionmark_bu379_313" Int)) % 0.43/0.82 (define @t499 () (@var "A__questionmark_au380_312" Int)) % 0.43/0.82 (define @t500 () (@var "A__questionmark_au382_314" Int)) % 0.43/0.82 (define @t501 () (@var "A__questionmark_bu381_315" Int)) % 0.43/0.82 (define @t502 () (@var "A__questionmark_bu383_317" Int)) % 0.43/0.82 (define @t503 () (@var "A__questionmark_au384_316" Int)) % 0.43/0.82 (define @t504 () (@var "A__questionmark_au386_318" Int)) % 0.43/0.82 (define @t505 () (@var "A__questionmark_bu385_319" Int)) % 0.43/0.82 (define @t506 () (@var "A__questionmark_au388_320" Int)) % 0.43/0.82 (define @t507 () (@var "A__questionmark_bu387_321" Int)) % 0.43/0.82 (define @t508 () (@var "A__questionmark_iu389_326" Int)) % 0.43/0.82 (define @t509 () (@var "A__questionmark_pu0_324" tptp.c_unsorted)) % 0.43/0.82 (define @t510 () (@var "A__questionmark_v_0_164" tptp.c_type)) % 0.43/0.82 (define @t511 () (@var "A__questionmark_au0_323" tptp.c_unsorted)) % 0.43/0.82 (define @t512 () (@var "A__questionmark_t1u0_322" tptp.c_type)) % 0.43/0.82 (define @t513 () (tptp.c_sort (tptp.alloc_table @t512) @t511)) % 0.43/0.82 (define @t514 () (@var "A__questionmark_nu0_325" Int)) % 0.43/0.82 (define @t515 () (tptp.pointer @t512)) % 0.43/0.82 (define @t516 () (@var "A__questionmark_v_2_167" tptp.c_sorted)) % 0.43/0.82 (define @t517 () (@var "A__questionmark_a2u391_329" tptp.c_unsorted)) % 0.43/0.82 (define @t518 () (@var "A__questionmark_v_0_165" tptp.c_type)) % 0.43/0.82 (define @t519 () (tptp.c_sort @t518 @t517)) % 0.43/0.82 (define @t520 () (@var "A__questionmark_v_1_166" tptp.c_sorted)) % 0.43/0.82 (define @t521 () (@var "A__questionmark_pu390_330" tptp.c_unsorted)) % 0.43/0.82 (define @t522 () (@var "A__questionmark_t1u0_327" tptp.c_type)) % 0.43/0.82 (define @t523 () (@var "A__questionmark_a1u392_328" tptp.c_unsorted)) % 0.43/0.82 (define @t524 () (tptp.c_sort @t518 @t523)) % 0.43/0.82 (define @t525 () (@var "A__questionmark_v_2_170" tptp.c_sorted)) % 0.43/0.82 (define @t526 () (@var "A__questionmark_a2u394_333" tptp.c_unsorted)) % 0.43/0.82 (define @t527 () (@var "A__questionmark_v_0_168" tptp.c_type)) % 0.43/0.82 (define @t528 () (tptp.c_sort @t527 @t526)) % 0.43/0.82 (define @t529 () (@var "A__questionmark_v_1_169" tptp.c_sorted)) % 0.43/0.82 (define @t530 () (@var "A__questionmark_pu393_334" tptp.c_unsorted)) % 0.43/0.82 (define @t531 () (@var "A__questionmark_t1u0_331" tptp.c_type)) % 0.43/0.82 (define @t532 () (@var "A__questionmark_a1u395_332" tptp.c_unsorted)) % 0.43/0.82 (define @t533 () (tptp.c_sort @t527 @t532)) % 0.43/0.82 (define @t534 () (@var "A__questionmark_v_5_178" tptp.c_type)) % 0.43/0.82 (define @t535 () (@var "A__questionmark_v_8_177" tptp.c_sorted)) % 0.43/0.82 (define @t536 () (@var "A__questionmark_v_7_176" tptp.c_sorted)) % 0.43/0.82 (define @t537 () (@var "A__questionmark_v_1_172" tptp.c_sorted)) % 0.43/0.82 (define @t538 () (@var "A__questionmark_v_6_174" tptp.c_sorted)) % 0.43/0.82 (define @t539 () (@var "A__questionmark_v_4_179" tptp.c_sorted)) % 0.43/0.82 (define @t540 () (@var "A__questionmark_v_2_173" tptp.c_sorted)) % 0.43/0.82 (define @t541 () (@var "A__questionmark_nu396_343" Int)) % 0.43/0.82 (define @t542 () (@var "A__questionmark_lu398_341" tptp.c_unsorted)) % 0.43/0.82 (define @t543 () (@var "A__questionmark_t1u0_336" tptp.c_type)) % 0.43/0.82 (define @t544 () (@var "A__questionmark_m2u399_340" tptp.c_unsorted)) % 0.43/0.82 (define @t545 () (@var "A__questionmark_v_3_175" tptp.c_type)) % 0.43/0.82 (define @t546 () (@var "A__questionmark_m1u400_339" tptp.c_unsorted)) % 0.43/0.82 (define @t547 () (@var "A__questionmark_t2u0_335" tptp.c_type)) % 0.43/0.82 (define @t548 () (@var "A__questionmark_pu397_342" tptp.c_unsorted)) % 0.43/0.82 (define @t549 () (@var "A__questionmark_a2u401_338" tptp.c_unsorted)) % 0.43/0.82 (define @t550 () (@var "A__questionmark_v_0_171" tptp.c_type)) % 0.43/0.82 (define @t551 () (@var "A__questionmark_a1u402_337" tptp.c_unsorted)) % 0.43/0.82 (define @t552 () (@var "A__questionmark_v_1_182" tptp.c_sorted)) % 0.43/0.82 (define @t553 () (@var "A__questionmark_a2u405_346" tptp.c_unsorted)) % 0.43/0.82 (define @t554 () (@var "A__questionmark_v_0_180" tptp.c_type)) % 0.43/0.82 (define @t555 () (tptp.c_sort @t554 @t553)) % 0.43/0.82 (define @t556 () (@var "A__questionmark_v_2_181" tptp.c_sorted)) % 0.43/0.82 (define @t557 () (@var "A__questionmark_lu404_347" tptp.c_unsorted)) % 0.43/0.82 (define @t558 () (@var "A__questionmark_t1u0_344" tptp.c_type)) % 0.43/0.82 (define @t559 () (tptp.c_sort (tptp.pset @t558) @t557)) % 0.43/0.82 (define @t560 () (@var "A__questionmark_pu403_348" tptp.c_unsorted)) % 0.43/0.82 (define @t561 () (@var "A__questionmark_a1u406_345" tptp.c_unsorted)) % 0.43/0.82 (define @t562 () (tptp.c_sort @t554 @t561)) % 0.43/0.82 (define @t563 () (@var "A__questionmark_v_1_185" tptp.c_sorted)) % 0.43/0.82 (define @t564 () (@var "A__questionmark_a2u409_351" tptp.c_unsorted)) % 0.43/0.82 (define @t565 () (@var "A__questionmark_v_0_183" tptp.c_type)) % 0.43/0.82 (define @t566 () (tptp.c_sort @t565 @t564)) % 0.43/0.82 (define @t567 () (@var "A__questionmark_v_2_184" tptp.c_sorted)) % 0.43/0.82 (define @t568 () (@var "A__questionmark_lu408_352" tptp.c_unsorted)) % 0.43/0.82 (define @t569 () (@var "A__questionmark_t1u0_349" tptp.c_type)) % 0.43/0.82 (define @t570 () (tptp.c_sort (tptp.pset @t569) @t568)) % 0.43/0.82 (define @t571 () (@var "A__questionmark_pu407_353" tptp.c_unsorted)) % 0.43/0.82 (define @t572 () (@var "A__questionmark_a1u410_350" tptp.c_unsorted)) % 0.43/0.82 (define @t573 () (tptp.c_sort @t565 @t572)) % 0.43/0.82 (define @t574 () (@var "A__questionmark_v_3_189" Int)) % 0.43/0.82 (define @t575 () (@var "A__questionmark_su432_357" Int)) % 0.43/0.82 (define @t576 () (@var "A__questionmark_v_2_188" Int)) % 0.43/0.82 (define @t577 () (@var "A__questionmark_v_1_187" tptp.c_sorted)) % 0.43/0.82 (define @t578 () (@var "A__questionmark_v_0_186" tptp.c_sorted)) % 0.43/0.82 (define @t579 () (@var "A__questionmark_pu433_356" tptp.c_unsorted)) % 0.43/0.82 (define @t580 () (@var "A__questionmark_t1u0_354" tptp.c_type)) % 0.43/0.82 (define @t581 () (@var "A__questionmark_au434_355" tptp.c_unsorted)) % 0.43/0.82 (define @t582 () (@var "A__questionmark_su435_361" Int)) % 0.43/0.82 (define @t583 () (@var "A__questionmark_v_3_193" Int)) % 0.43/0.82 (define @t584 () (@var "A__questionmark_v_2_192" Int)) % 0.43/0.82 (define @t585 () (@var "A__questionmark_v_1_191" tptp.c_sorted)) % 0.43/0.82 (define @t586 () (@var "A__questionmark_v_0_190" tptp.c_sorted)) % 0.43/0.82 (define @t587 () (@var "A__questionmark_pu436_360" tptp.c_unsorted)) % 0.43/0.82 (define @t588 () (@var "A__questionmark_t1u0_358" tptp.c_type)) % 0.43/0.82 (define @t589 () (@var "A__questionmark_au437_359" tptp.c_unsorted)) % 0.43/0.82 (define @t590 () (@var "A__questionmark_v_0_194" tptp.c_sorted)) % 0.43/0.82 (define @t591 () (@var "A__questionmark_s2u440_365" Int)) % 0.43/0.82 (define @t592 () (@var "A__questionmark_o2u441_364" Int)) % 0.43/0.82 (define @t593 () (@var "A__questionmark_s1u442_363" Int)) % 0.43/0.82 (define @t594 () (@var "A__questionmark_o1u443_362" Int)) % 0.43/0.82 (define @t595 () (@var "A__questionmark_v1u439_366" tptp.c_unsorted)) % 0.43/0.82 (define @t596 () (@var "A__questionmark_v2u438_367" tptp.c_unsorted)) % 0.43/0.82 (define @t597 () (@var "A__questionmark_s2u446_371" Int)) % 0.43/0.82 (define @t598 () (@var "A__questionmark_o2u447_370" Int)) % 0.43/0.82 (define @t599 () (@var "A__questionmark_v_0_195" tptp.c_sorted)) % 0.43/0.82 (define @t600 () (@var "A__questionmark_v2u444_373" tptp.c_unsorted)) % 0.43/0.82 (define @t601 () (@var "A__questionmark_s1u448_369" Int)) % 0.43/0.82 (define @t602 () (@var "A__questionmark_o1u449_368" Int)) % 0.43/0.82 (define @t603 () (@var "A__questionmark_v1u445_372" tptp.c_unsorted)) % 0.43/0.82 (define @t604 () (@var "A__questionmark_v_2_198" tptp.c_sorted)) % 0.43/0.82 (define @t605 () (@var "A__questionmark_v_1_197" tptp.c_sorted)) % 0.43/0.82 (define @t606 () (@var "A__questionmark_s2u453_377" Int)) % 0.43/0.82 (define @t607 () (@var "A__questionmark_s1u455_375" Int)) % 0.43/0.82 (define @t608 () (@var "A__questionmark_o1u456_374" Int)) % 0.43/0.82 (define @t609 () (@var "A__questionmark_v_0_196" tptp.c_sorted)) % 0.43/0.82 (define @t610 () (@var "A__questionmark_o2u454_376" Int)) % 0.43/0.82 (define @t611 () (@var "A__questionmark_v3u450_380" tptp.c_unsorted)) % 0.43/0.82 (define @t612 () (@var "A__questionmark_v2u451_379" tptp.c_unsorted)) % 0.43/0.82 (define @t613 () (@var "A__questionmark_v1u452_378" tptp.c_unsorted)) % 0.43/0.82 (define @t614 () (@var "A__questionmark_v_2_200" tptp.c_sorted)) % 0.43/0.82 (define @t615 () (@var "A__questionmark_v_1_201" tptp.c_sorted)) % 0.43/0.82 (define @t616 () (@var "A__questionmark_s2u460_384" Int)) % 0.43/0.82 (define @t617 () (@var "A__questionmark_s1u462_382" Int)) % 0.43/0.82 (define @t618 () (@var "A__questionmark_o2u461_383" Int)) % 0.43/0.82 (define @t619 () (@var "A__questionmark_v_0_199" tptp.c_sorted)) % 0.43/0.82 (define @t620 () (@var "A__questionmark_o1u463_381" Int)) % 0.43/0.82 (define @t621 () (@var "A__questionmark_v3u457_387" tptp.c_unsorted)) % 0.43/0.82 (define @t622 () (@var "A__questionmark_v2u458_386" tptp.c_unsorted)) % 0.43/0.82 (define @t623 () (@var "A__questionmark_v1u459_385" tptp.c_unsorted)) % 0.43/0.82 (define @t624 () (@var "A__questionmark_s2u465_391" Int)) % 0.43/0.82 (define @t625 () (@var "A__questionmark_s1u467_389" Int)) % 0.43/0.82 (define @t626 () (@var "A__questionmark_o1u468_388" Int)) % 0.43/0.82 (define @t627 () (@var "A__questionmark_v_0_202" tptp.c_sorted)) % 0.43/0.82 (define @t628 () (@var "A__questionmark_o2u466_390" Int)) % 0.43/0.82 (define @t629 () (@var "A__questionmark_vu464_392" tptp.c_unsorted)) % 0.43/0.82 (define @t630 () (@var "A__questionmark_v_4_207" tptp.c_sorted)) % 0.43/0.82 (define @t631 () (@var "A__questionmark_s2u470_400" Int)) % 0.43/0.82 (define @t632 () (@var "A__questionmark_o2u471_399" Int)) % 0.43/0.82 (define @t633 () (@var "A__questionmark_v_3_205" tptp.c_sorted)) % 0.43/0.82 (define @t634 () (@var "A__questionmark_s1u472_398" Int)) % 0.43/0.82 (define @t635 () (@var "A__questionmark_o1u473_397" Int)) % 0.43/0.82 (define @t636 () (@var "A__questionmark_v_2_204" tptp.c_sorted)) % 0.43/0.82 (define @t637 () (@var "A__questionmark_mu476_394" tptp.c_unsorted)) % 0.43/0.82 (define @t638 () (@var "A__questionmark_v_1_206" tptp.c_type)) % 0.43/0.82 (define @t639 () (@var "A__questionmark_vu469_401" tptp.c_unsorted)) % 0.43/0.82 (define @t640 () (@var "A__questionmark_t1u0_393" tptp.c_type)) % 0.43/0.82 (define @t641 () (@var "A__questionmark_p2u474_396" tptp.c_unsorted)) % 0.43/0.82 (define @t642 () (@var "A__questionmark_v_0_203" tptp.c_type)) % 0.43/0.82 (define @t643 () (@var "A__questionmark_p1u475_395" tptp.c_unsorted)) % 0.43/0.82 (define @t644 () (@var "A__questionmark_s2u478_409" Int)) % 0.43/0.82 (define @t645 () (@var "A__questionmark_o2u479_408" Int)) % 0.43/0.82 (define @t646 () (@var "A__questionmark_v_4_211" tptp.c_sorted)) % 0.43/0.82 (define @t647 () (@var "A__questionmark_v_5_213" tptp.c_sorted)) % 0.43/0.82 (define @t648 () (@var "A__questionmark_vu477_410" tptp.c_unsorted)) % 0.43/0.82 (define @t649 () (@var "A__questionmark_s1u480_407" Int)) % 0.43/0.82 (define @t650 () (@var "A__questionmark_o1u481_406" Int)) % 0.43/0.82 (define @t651 () (@var "A__questionmark_v_3_210" tptp.c_sorted)) % 0.43/0.82 (define @t652 () (@var "A__questionmark_v_2_212" tptp.c_type)) % 0.43/0.82 (define @t653 () (@var "A__questionmark_v_0_208" tptp.c_type)) % 0.43/0.82 (define @t654 () (@var "A__questionmark_mu484_403" tptp.c_unsorted)) % 0.43/0.82 (define @t655 () (@var "A__questionmark_t1u0_402" tptp.c_type)) % 0.43/0.82 (define @t656 () (@var "A__questionmark_p2u482_405" tptp.c_unsorted)) % 0.43/0.82 (define @t657 () (@var "A__questionmark_v_1_209" tptp.c_type)) % 0.43/0.82 (define @t658 () (@var "A__questionmark_p1u483_404" tptp.c_unsorted)) % 0.43/0.82 (define @t659 () (@var "A__questionmark_v_4_218" tptp.c_sorted)) % 0.43/0.82 (define @t660 () (@var "A__questionmark_su486_416" Int)) % 0.43/0.82 (define @t661 () (@var "A__questionmark_iu488_414" Int)) % 0.43/0.82 (define @t662 () (@var "A__questionmark_ou487_415" Int)) % 0.43/0.82 (define @t663 () (@var "A__questionmark_v_3_217" tptp.c_sorted)) % 0.43/0.82 (define @t664 () (@var "A__questionmark_v_2_215" tptp.c_sorted)) % 0.43/0.82 (define @t665 () (@var "A__questionmark_v_0_214" tptp.c_type)) % 0.43/0.82 (define @t666 () (@var "A__questionmark_v_1_216" tptp.c_type)) % 0.43/0.82 (define @t667 () (@var "A__questionmark_vu485_417" tptp.c_unsorted)) % 0.43/0.82 (define @t668 () (@var "A__questionmark_pu489_413" tptp.c_unsorted)) % 0.43/0.82 (define @t669 () (@var "A__questionmark_t1u0_411" tptp.c_type)) % 0.43/0.82 (define @t670 () (@var "A__questionmark_mu490_412" tptp.c_unsorted)) % 0.43/0.82 (define @t671 () (@var "A__questionmark_su492_423" Int)) % 0.43/0.82 (define @t672 () (@var "A__questionmark_iu494_421" Int)) % 0.43/0.82 (define @t673 () (@var "A__questionmark_ou493_422" Int)) % 0.43/0.82 (define @t674 () (@var "A__questionmark_v_2_221" tptp.c_sorted)) % 0.43/0.82 (define @t675 () (@var "A__questionmark_v_1_219" tptp.c_sorted)) % 0.43/0.82 (define @t676 () (@var "A__questionmark_v_0_220" tptp.c_type)) % 0.43/0.82 (define @t677 () (@var "A__questionmark_pu495_420" tptp.c_unsorted)) % 0.43/0.82 (define @t678 () (@var "A__questionmark_t1u0_418" tptp.c_type)) % 0.43/0.82 (define @t679 () (@var "A__questionmark_mu496_419" tptp.c_unsorted)) % 0.43/0.82 (define @t680 () (@var "A__questionmark_v_4_226" tptp.c_sorted)) % 0.43/0.82 (define @t681 () (@var "A__questionmark_v_3_225" tptp.c_sorted)) % 0.43/0.82 (define @t682 () (@var "A__questionmark_s2u499_431" Int)) % 0.43/0.82 (define @t683 () (@var "A__questionmark_s1u501_429" Int)) % 0.43/0.82 (define @t684 () (@var "A__questionmark_o1u502_428" Int)) % 0.43/0.82 (define @t685 () (@var "A__questionmark_v_1_224" tptp.c_sorted)) % 0.43/0.82 (define @t686 () (@var "A__questionmark_v_2_223" tptp.c_sorted)) % 0.43/0.82 (define @t687 () (@var "A__questionmark_v_0_222" tptp.c_type)) % 0.43/0.82 (define @t688 () (@var "A__questionmark_o2u500_430" Int)) % 0.43/0.82 (define @t689 () (@var "A__questionmark_v2u497_433" tptp.c_unsorted)) % 0.43/0.82 (define @t690 () (@var "A__questionmark_v1u498_432" tptp.c_unsorted)) % 0.43/0.82 (define @t691 () (@var "A__questionmark_pu503_427" tptp.c_unsorted)) % 0.43/0.82 (define @t692 () (@var "A__questionmark_t1u0_425" tptp.c_type)) % 0.43/0.82 (define @t693 () (@var "A__questionmark_mu504_426" tptp.c_unsorted)) % 0.43/0.82 (define @t694 () (@var "A__questionmark_v_4_230" tptp.c_sorted)) % 0.43/0.82 (define @t695 () (@var "A__questionmark_v_3_231" tptp.c_sorted)) % 0.43/0.82 (define @t696 () (@var "A__questionmark_s2u507_440" Int)) % 0.43/0.82 (define @t697 () (@var "A__questionmark_s1u509_438" Int)) % 0.43/0.82 (define @t698 () (@var "A__questionmark_o2u508_439" Int)) % 0.43/0.82 (define @t699 () (@var "A__questionmark_v_1_229" tptp.c_sorted)) % 0.43/0.82 (define @t700 () (@var "A__questionmark_v_2_228" tptp.c_sorted)) % 0.43/0.82 (define @t701 () (@var "A__questionmark_v_0_227" tptp.c_type)) % 0.43/0.82 (define @t702 () (@var "A__questionmark_o1u510_437" Int)) % 0.43/0.82 (define @t703 () (@var "A__questionmark_v2u505_442" tptp.c_unsorted)) % 0.43/0.82 (define @t704 () (@var "A__questionmark_v1u506_441" tptp.c_unsorted)) % 0.43/0.82 (define @t705 () (@var "A__questionmark_pu511_436" tptp.c_unsorted)) % 0.43/0.82 (define @t706 () (@var "A__questionmark_t1u0_434" tptp.c_type)) % 0.43/0.82 (define @t707 () (@var "A__questionmark_mu512_435" tptp.c_unsorted)) % 0.43/0.82 (define @t708 () (@var "A__questionmark_s2u513_449" Int)) % 0.43/0.82 (define @t709 () (@var "A__questionmark_s1u515_447" Int)) % 0.43/0.82 (define @t710 () (@var "A__questionmark_o1u516_446" Int)) % 0.43/0.82 (define @t711 () (@var "A__questionmark_v_1_233" tptp.c_sorted)) % 0.43/0.82 (define @t712 () (@var "A__questionmark_v_0_232" tptp.c_sorted)) % 0.43/0.82 (define @t713 () (@var "A__questionmark_o2u514_448" Int)) % 0.43/0.82 (define @t714 () (@var "A__questionmark_pu517_445" tptp.c_unsorted)) % 0.43/0.82 (define @t715 () (@var "A__questionmark_t1u0_443" tptp.c_type)) % 0.43/0.82 (define @t716 () (@var "A__questionmark_mu518_444" tptp.c_unsorted)) % 0.43/0.82 (define @t717 () (@var "A__questionmark_v_0_234" tptp.c_sorted)) % 0.43/0.82 (define @t718 () (tptp.pointer tptp.char_P)) % 0.43/0.82 (define @t719 () (@var "A__questionmark_xu539_450" tptp.c_unsorted)) % 0.43/0.82 (define @t720 () (@var "A__questionmark_v_0_235" tptp.c_sorted)) % 0.43/0.82 (define @t721 () (@var "A__questionmark_xu540_451" tptp.c_unsorted)) % 0.43/0.82 (define @t722 () (@var "A__questionmark_v_0_236" tptp.c_sorted)) % 0.43/0.82 (define @t723 () (@var "A__questionmark_xu541_452" tptp.c_unsorted)) % 0.43/0.82 (define @t724 () (@var "A__questionmark_v_0_237" tptp.c_sorted)) % 0.43/0.82 (define @t725 () (tptp.pointer tptp.void_P)) % 0.43/0.82 (define @t726 () (@var "A__questionmark_xu542_453" tptp.c_unsorted)) % 0.43/0.82 (define @t727 () (tptp.tag_id tptp.char_P)) % 0.43/0.82 (define @t728 () (tptp.c_sort @t727 tptp.char_P_tag)) % 0.43/0.82 (define @t729 () (@var "A__questionmark_v_1_239" tptp.c_sorted)) % 0.43/0.82 (define @t730 () (@var "A__questionmark_v_0_238" tptp.c_type)) % 0.43/0.82 (define @t731 () (@var "A__questionmark_xu543_454" tptp.c_unsorted)) % 0.43/0.82 (define @t732 () (@var "A__questionmark_v_1_241" tptp.c_sorted)) % 0.43/0.82 (define @t733 () (tptp.pointer tptp.c_unit)) % 0.43/0.82 (define @t734 () (@var "A__questionmark_v_0_240" tptp.c_type)) % 0.43/0.82 (define @t735 () (@var "A__questionmark_pu544_455" tptp.c_unsorted)) % 0.43/0.82 (define @t736 () (@var "A__questionmark_v_0_242" tptp.c_type)) % 0.43/0.82 (define @t737 () (@var "A__questionmark_xu546_456" tptp.c_unsorted)) % 0.43/0.82 (define @t738 () (@var "A__questionmark_charuPutagutableu545_457" tptp.c_unsorted)) % 0.43/0.82 (define @t739 () (@var "A__questionmark_v_1_244" tptp.c_sorted)) % 0.43/0.82 (define @t740 () (@var "A__questionmark_v_0_243" tptp.c_sorted)) % 0.43/0.82 (define @t741 () (@var "A__questionmark_yu0_459" tptp.c_unsorted)) % 0.43/0.82 (define @t742 () (@var "A__questionmark_xu0_458" tptp.c_unsorted)) % 0.43/0.82 (define @t743 () (@var "A__questionmark_v_1_246" tptp.c_sorted)) % 0.43/0.82 (define @t744 () (@var "A__questionmark_v_0_245" tptp.c_sorted)) % 0.43/0.82 (define @t745 () (@var "A__questionmark_yu0_461" tptp.c_unsorted)) % 0.43/0.82 (define @t746 () (@var "A__questionmark_xu0_460" tptp.c_unsorted)) % 0.43/0.82 (define @t747 () (@var "A__questionmark_xu547_462" Int)) % 0.43/0.82 (define @t748 () (- 2147483648)) % 0.43/0.82 (define @t749 () (@var "A__questionmark_v_0_247" tptp.c_sorted)) % 0.43/0.82 (define @t750 () (@var "A__questionmark_xu548_463" tptp.c_unsorted)) % 0.43/0.82 (define @t751 () (@var "A__questionmark_v_0_248" Int)) % 0.43/0.82 (define @t752 () (@var "A__questionmark_xu549_464" tptp.c_unsorted)) % 0.43/0.82 (define @t753 () (@var "A__questionmark_xu550_465" Int)) % 0.43/0.82 (define @t754 () (- 128)) % 0.43/0.82 (define @t755 () (@var "A__questionmark_v_0_249" tptp.c_sorted)) % 0.43/0.82 (define @t756 () (@var "A__questionmark_xu551_466" tptp.c_unsorted)) % 0.43/0.82 (define @t757 () (@var "A__questionmark_v_0_250" Int)) % 0.43/0.82 (define @t758 () (@var "A__questionmark_xu552_467" tptp.c_unsorted)) % 0.43/0.82 (define @t759 () (@var "A__questionmark_au0_469" Int)) % 0.43/0.82 (define @t760 () (@var "A__questionmark_v_1_251" tptp.c_sorted)) % 0.43/0.82 (define @t761 () (@var "A__questionmark_v_0_252" tptp.c_sorted)) % 0.43/0.82 (define @t762 () (@var "A__questionmark_charuPuallocutableu0_470" tptp.c_unsorted)) % 0.43/0.82 (define @t763 () (tptp.alloc_table tptp.char_P)) % 0.43/0.82 (define @t764 () (@var "A__questionmark_pu0_468" tptp.c_unsorted)) % 0.43/0.82 (define @t765 () (@var "A__questionmark_au0_472" Int)) % 0.43/0.82 (define @t766 () (@var "A__questionmark_v_1_253" tptp.c_sorted)) % 0.43/0.82 (define @t767 () (@var "A__questionmark_v_0_254" tptp.c_sorted)) % 0.43/0.82 (define @t768 () (@var "A__questionmark_voiduPuallocutableu0_473" tptp.c_unsorted)) % 0.43/0.82 (define @t769 () (tptp.alloc_table tptp.void_P)) % 0.43/0.82 (define @t770 () (@var "A__questionmark_pu0_471" tptp.c_unsorted)) % 0.43/0.82 (define @t771 () (@var "A__questionmark_v_1_256" tptp.c_sorted)) % 0.43/0.82 (define @t772 () (@var "A__questionmark_v_0_255" tptp.c_type)) % 0.43/0.82 (define @t773 () (@var "A__questionmark_pu553_474" tptp.c_unsorted)) % 0.43/0.82 (define @t774 () (@var "A__questionmark_v_1_258" tptp.c_sorted)) % 0.43/0.82 (define @t775 () (@var "A__questionmark_v_0_257" tptp.c_type)) % 0.43/0.82 (define @t776 () (@var "A__questionmark_pu554_475" tptp.c_unsorted)) % 0.43/0.82 (define @t777 () (@var "A__questionmark_bu0_477" Int)) % 0.43/0.82 (define @t778 () (@var "A__questionmark_v_1_259" tptp.c_sorted)) % 0.43/0.82 (define @t779 () (@var "A__questionmark_v_0_260" tptp.c_sorted)) % 0.43/0.82 (define @t780 () (@var "A__questionmark_charuPuallocutableu0_478" tptp.c_unsorted)) % 0.43/0.82 (define @t781 () (@var "A__questionmark_pu0_476" tptp.c_unsorted)) % 0.43/0.82 (define @t782 () (@var "A__questionmark_bu0_480" Int)) % 0.43/0.82 (define @t783 () (@var "A__questionmark_v_1_261" tptp.c_sorted)) % 0.43/0.82 (define @t784 () (@var "A__questionmark_v_0_262" tptp.c_sorted)) % 0.43/0.82 (define @t785 () (@var "A__questionmark_voiduPuallocutableu0_481" tptp.c_unsorted)) % 0.43/0.82 (define @t786 () (@var "A__questionmark_pu0_479" tptp.c_unsorted)) % 0.43/0.82 (define @t787 () (@var "A__questionmark_bu0_484" Int)) % 0.43/0.82 (define @t788 () (@var "A__questionmark_v_1_263" tptp.c_sorted)) % 0.43/0.82 (define @t789 () (@var "A__questionmark_v_0_264" tptp.c_sorted)) % 0.43/0.82 (define @t790 () (@var "A__questionmark_au0_483" Int)) % 0.43/0.82 (define @t791 () (@var "A__questionmark_charuPuallocutableu0_485" tptp.c_unsorted)) % 0.43/0.82 (define @t792 () (@var "A__questionmark_pu0_482" tptp.c_unsorted)) % 0.43/0.82 (define @t793 () (@var "A__questionmark_bu0_488" Int)) % 0.43/0.82 (define @t794 () (@var "A__questionmark_v_1_265" tptp.c_sorted)) % 0.43/0.82 (define @t795 () (@var "A__questionmark_v_0_266" tptp.c_sorted)) % 0.43/0.82 (define @t796 () (@var "A__questionmark_au0_487" Int)) % 0.43/0.82 (define @t797 () (@var "A__questionmark_voiduPuallocutableu0_489" tptp.c_unsorted)) % 0.43/0.82 (define @t798 () (@var "A__questionmark_pu0_486" tptp.c_unsorted)) % 0.43/0.82 (define @t799 () (@var "A__questionmark_bu0_492" Int)) % 0.43/0.82 (define @t800 () (@var "A__questionmark_v_1_267" tptp.c_sorted)) % 0.43/0.82 (define @t801 () (@var "A__questionmark_v_0_268" tptp.c_sorted)) % 0.43/0.82 (define @t802 () (@var "A__questionmark_au0_491" Int)) % 0.43/0.82 (define @t803 () (@var "A__questionmark_charuPuallocutableu0_493" tptp.c_unsorted)) % 0.43/0.82 (define @t804 () (@var "A__questionmark_pu0_490" tptp.c_unsorted)) % 0.43/0.82 (define @t805 () (@var "A__questionmark_bu0_496" Int)) % 0.43/0.82 (define @t806 () (@var "A__questionmark_v_1_269" tptp.c_sorted)) % 0.43/0.82 (define @t807 () (@var "A__questionmark_v_0_270" tptp.c_sorted)) % 0.43/0.82 (define @t808 () (@var "A__questionmark_au0_495" Int)) % 0.43/0.82 (define @t809 () (@var "A__questionmark_voiduPuallocutableu0_497" tptp.c_unsorted)) % 0.43/0.82 (define @t810 () (@var "A__questionmark_pu0_494" tptp.c_unsorted)) % 0.43/0.82 (define @t811 () (@var "A__questionmark_bu0_500" Int)) % 0.43/0.82 (define @t812 () (@var "A__questionmark_v_1_271" tptp.c_sorted)) % 0.43/0.82 (define @t813 () (@var "A__questionmark_v_0_272" tptp.c_sorted)) % 0.43/0.82 (define @t814 () (@var "A__questionmark_au0_499" Int)) % 0.43/0.82 (define @t815 () (@var "A__questionmark_bitvectoruallocutableu0_501" tptp.c_unsorted)) % 0.43/0.82 (define @t816 () (tptp.alloc_table tptp.c_unit)) % 0.43/0.82 (define @t817 () (@var "A__questionmark_pu0_498" tptp.c_unsorted)) % 0.43/0.82 (define @t818 () (@var "A__questionmark_bu0_504" Int)) % 0.43/0.82 (define @t819 () (@var "A__questionmark_v_1_273" tptp.c_sorted)) % 0.43/0.82 (define @t820 () (@var "A__questionmark_v_0_274" tptp.c_sorted)) % 0.43/0.82 (define @t821 () (@var "A__questionmark_au0_503" Int)) % 0.43/0.82 (define @t822 () (@var "A__questionmark_bitvectoruallocutableu0_505" tptp.c_unsorted)) % 0.43/0.82 (define @t823 () (@var "A__questionmark_pu0_502" tptp.c_unsorted)) % 0.43/0.82 (define @t824 () (@var "A__questionmark_bu0_508" Int)) % 0.43/0.82 (define @t825 () (@var "A__questionmark_v_1_275" tptp.c_sorted)) % 0.43/0.82 (define @t826 () (@var "A__questionmark_v_0_276" tptp.c_sorted)) % 0.43/0.82 (define @t827 () (@var "A__questionmark_au0_507" Int)) % 0.43/0.82 (define @t828 () (@var "A__questionmark_charuPuallocutableu0_509" tptp.c_unsorted)) % 0.43/0.82 (define @t829 () (@var "A__questionmark_pu0_506" tptp.c_unsorted)) % 0.43/0.82 (define @t830 () (@var "A__questionmark_bu0_512" Int)) % 0.43/0.82 (define @t831 () (@var "A__questionmark_v_1_277" tptp.c_sorted)) % 0.43/0.82 (define @t832 () (@var "A__questionmark_v_0_278" tptp.c_sorted)) % 0.43/0.82 (define @t833 () (@var "A__questionmark_au0_511" Int)) % 0.43/0.82 (define @t834 () (@var "A__questionmark_voiduPuallocutableu0_513" tptp.c_unsorted)) % 0.43/0.82 (define @t835 () (@var "A__questionmark_pu0_510" tptp.c_unsorted)) % 0.43/0.82 (define @t836 () (@var "A__questionmark_bu0_516" Int)) % 0.43/0.82 (define @t837 () (@var "A__questionmark_v_1_279" tptp.c_sorted)) % 0.43/0.82 (define @t838 () (@var "A__questionmark_v_0_280" tptp.c_sorted)) % 0.43/0.82 (define @t839 () (@var "A__questionmark_au0_515" Int)) % 0.43/0.82 (define @t840 () (@var "A__questionmark_charuPuallocutableu0_517" tptp.c_unsorted)) % 0.43/0.82 (define @t841 () (@var "A__questionmark_pu0_514" tptp.c_unsorted)) % 0.43/0.82 (define @t842 () (@var "A__questionmark_bu0_520" Int)) % 0.43/0.82 (define @t843 () (@var "A__questionmark_v_1_281" tptp.c_sorted)) % 0.43/0.82 (define @t844 () (@var "A__questionmark_v_0_282" tptp.c_sorted)) % 0.43/0.82 (define @t845 () (@var "A__questionmark_au0_519" Int)) % 0.43/0.82 (define @t846 () (@var "A__questionmark_voiduPuallocutableu0_521" tptp.c_unsorted)) % 0.43/0.82 (define @t847 () (@var "A__questionmark_pu0_518" tptp.c_unsorted)) % 0.43/0.82 (define @t848 () (tptp.tag_id tptp.void_P)) % 0.43/0.82 (define @t849 () (tptp.c_sort @t848 tptp.void_P_tag)) % 0.43/0.82 (define @t850 () (@var "A__questionmark_v_1_284" tptp.c_sorted)) % 0.43/0.82 (define @t851 () (@var "A__questionmark_v_0_283" tptp.c_type)) % 0.43/0.82 (define @t852 () (@var "A__questionmark_xu555_522" tptp.c_unsorted)) % 0.43/0.82 (define @t853 () (@var "A__questionmark_v_1_286" tptp.c_sorted)) % 0.43/0.82 (define @t854 () (@var "A__questionmark_v_0_285" tptp.c_type)) % 0.43/0.82 (define @t855 () (@var "A__questionmark_pu556_523" tptp.c_unsorted)) % 0.43/0.82 (define @t856 () (@var "A__questionmark_v_0_287" tptp.c_type)) % 0.43/0.82 (define @t857 () (@var "A__questionmark_xu558_524" tptp.c_unsorted)) % 0.43/0.82 (define @t858 () (@var "A__questionmark_voiduPutagutableu557_525" tptp.c_unsorted)) % 0.43/0.82 (define @t859 () (@var "A__questionmark_v_0_288" tptp.c_sorted)) % 0.43/0.82 (define @t860 () (= (tptp.integer_of_int32 @t859) 18)) % 0.43/0.82 (define @t861 () (@var "A__questionmark_smtlib____retres" tptp.c_unsorted)) % 0.43/0.82 (define @t862 () (tptp.c_sort tptp.int32 @t861)) % 0.43/0.82 (define @t863 () (=> (= @t859 @t862) @t860)) % 0.43/0.82 (define @t864 () (@var "A__questionmark_return" tptp.c_unsorted)) % 0.43/0.82 (define @t865 () (tptp.c_sort tptp.int32 @t864)) % 0.43/0.82 (define @t866 () (= @t859 @t865)) % 0.43/0.82 (define @t867 () (and @t866 @t863)) % 0.43/0.82 (define @t868 () (@list @t859)) % 0.43/0.82 (define @t869 () (exists @t868 @t867)) % 0.43/0.82 (define @t870 () (@list @t864)) % 0.43/0.82 (define @t871 () (forall @t870 @t869)) % 0.43/0.82 (define @t872 () (@var "A__questionmark_result" tptp.c_unsorted)) % 0.43/0.82 (define @t873 () (tptp.c_sort tptp.int32 @t872)) % 0.43/0.82 (define @t874 () (=> (= @t862 @t873) @t871)) % 0.43/0.82 (define @t875 () (@list @t861)) % 0.43/0.82 (define @t876 () (forall @t875 @t874)) % 0.43/0.82 (define @t877 () (= (tptp.integer_of_int32 @t873) 18)) % 0.43/0.82 (define @t878 () (=> @t877 @t876)) % 0.43/0.82 (define @t879 () (@list @t872)) % 0.43/0.82 (define @t880 () (forall @t879 @t878)) % 0.43/0.82 (define @t881 () (=> (= tptp.c_Boolean_true tptp.c_Boolean_true) @t880)) % 0.43/0.82 (define @t882 () (not @t881)) % 0.43/0.82 (define @t883 () (@var "BOUND_VARIABLE_18842" tptp.c_unsorted)) % 0.43/0.82 (define @t884 () (tptp.c_sort tptp.int32 @t883)) % 0.43/0.82 (define @t885 () (= (tptp.integer_of_int32 @t884) 18)) % 0.43/0.82 (define @t886 () (@var "BOUND_VARIABLE_18840" tptp.c_unsorted)) % 0.43/0.82 (define @t887 () (tptp.c_sort tptp.int32 @t886)) % 0.43/0.82 (define @t888 () (not (= @t887 @t884))) % 0.43/0.82 (define @t889 () (not (= @t873 @t887))) % 0.43/0.82 (define @t890 () (not @t877)) % 0.43/0.82 (define @t891 () (or @t890 @t889 @t888 @t885)) % 0.43/0.82 (define @t892 () (@list @t872 @t886 @t883)) % 0.43/0.82 (define @t893 () (forall @t892 @t891)) % 0.43/0.82 (define @t894 () (or @t889 @t888 @t885)) % 0.43/0.82 (define @t895 () (or @t890 @t894)) % 0.43/0.82 (define @t896 () (forall @t892 @t895)) % 0.43/0.82 (define @t897 () (@list @t886 @t883)) % 0.43/0.82 (define @t898 () (forall @t897 @t895)) % 0.43/0.82 (define @t899 () (forall @t897 @t894)) % 0.43/0.82 (define @t900 () (@var "BOUND_VARIABLE_18822" tptp.c_unsorted)) % 0.43/0.82 (define @t901 () (or @t890 @t899)) % 0.43/0.82 (define @t902 () (tptp.c_sort tptp.int32 @t900)) % 0.43/0.82 (define @t903 () (= (tptp.integer_of_int32 @t902) 18)) % 0.43/0.82 (define @t904 () (not (= @t862 @t902))) % 0.43/0.82 (define @t905 () (= @t873 @t862)) % 0.43/0.82 (define @t906 () (not @t905)) % 0.43/0.82 (define @t907 () (or @t906 @t904 @t903)) % 0.43/0.82 (define @t908 () (@list @t861 @t900)) % 0.43/0.82 (define @t909 () (forall @t908 @t907)) % 0.43/0.82 (define @t910 () (or @t904 @t903)) % 0.43/0.82 (define @t911 () (or @t906 @t910)) % 0.43/0.82 (define @t912 () (forall @t908 @t911)) % 0.43/0.82 (define @t913 () (@list @t900)) % 0.43/0.82 (define @t914 () (forall @t913 @t911)) % 0.43/0.82 (define @t915 () (forall @t913 @t910)) % 0.43/0.82 (define @t916 () (or @t906 @t915)) % 0.43/0.82 (define @t917 () (= (tptp.integer_of_int32 @t865) 18)) % 0.43/0.82 (define @t918 () (= @t862 @t865)) % 0.43/0.82 (define @t919 () (not @t918)) % 0.43/0.82 (define @t920 () (forall @t870 (or @t919 @t917))) % 0.43/0.82 (define @t921 () (not @t917)) % 0.43/0.82 (define @t922 () (and @t918 @t921)) % 0.43/0.82 (define @t923 () (not (= @t865 @t865))) % 0.43/0.82 (define @t924 () (or @t923 @t922)) % 0.43/0.82 (define @t925 () (= @t862 @t859)) % 0.43/0.82 (define @t926 () (and @t925 (not @t860))) % 0.43/0.82 (define @t927 () (not @t866)) % 0.43/0.82 (define @t928 () (or @t927 @t927 @t926)) % 0.43/0.82 (define @t929 () (or @t927 @t926)) % 0.43/0.82 (define @t930 () (=> @t925 @t860)) % 0.43/0.82 (define @t931 () (and @t866 @t930)) % 0.43/0.82 (define @t932 () (forall @t868 (not @t931))) % 0.43/0.82 (define @t933 () (not @t932)) % 0.43/0.82 (define @t934 () (tptp.c_sort tptp.int32 (@quantifiers_skolemize @t893 0))) % 0.43/0.82 (define @t935 () (tptp.integer_of_int32 @t934)) % 0.43/0.82 (define @t936 () (= @t935 18)) % 0.43/0.82 (define @t937 () (tptp.c_sort tptp.int32 (@quantifiers_skolemize @t893 2))) % 0.43/0.82 (define @t938 () (tptp.integer_of_int32 @t937)) % 0.43/0.82 (define @t939 () (= @t938 18)) % 0.43/0.82 (define @t940 () (tptp.c_sort tptp.int32 (@quantifiers_skolemize @t893 1))) % 0.43/0.82 (define @t941 () (= @t940 @t937)) % 0.43/0.82 (define @t942 () (not @t941)) % 0.43/0.82 (define @t943 () (= @t934 @t940)) % 0.43/0.82 (define @t944 () (not @t943)) % 0.43/0.82 (define @t945 () (not @t936)) % 0.43/0.82 (define @t946 () (or @t945 @t944 @t942 @t939)) % 0.43/0.82 (define @t947 () (@list true)) % 0.43/0.82 (define @t948 () (@list @t946)) % 0.43/0.82 (define @t949 () (not @t939)) % 0.43/0.82 (define @t950 () (= 18 @t938)) % 0.43/0.82 (define @t951 () (and @t950 @t949)) % 0.43/0.82 (assume @p1 (forall (@list @t1) (or (= @t1 tptp.c_Boolean_true) (= @t1 tptp.c_Boolean_false)))) % 0.43/0.82 (assume @p2 (not (= tptp.c_Boolean_true tptp.c_Boolean_false))) % 0.43/0.82 (assume @p3 (forall (@list @t2) (= (tptp.s2int (tptp.c_sort tptp.c_int (tptp.int2u @t2))) @t2))) % 0.43/0.82 (assume @p4 (forall (@list @t3) (= (tptp.s2bool (tptp.c_sort tptp.c_bool (tptp.bool2u @t3))) @t3))) % 0.43/0.82 (assume @p5 (forall (@list @t4) (= (tptp.s2real (tptp.c_sort tptp.c_real (tptp.real2u @t4))) @t4))) % 0.43/0.82 (assume @p6 (forall (@list @t5) (= (tptp.s2unit (tptp.c_sort tptp.c_unit (tptp.unit2u @t5))) @t5))) % 0.43/0.82 (assume @p7 (forall (@list @t6) (= (tptp.int2u (tptp.s2int (tptp.c_sort tptp.c_int @t6))) @t6))) % 0.43/0.82 (assume @p8 (forall (@list @t7) (= (tptp.bool2u (tptp.s2bool (tptp.c_sort tptp.c_bool @t7))) @t7))) % 0.43/0.82 (assume @p9 (forall (@list @t8) (= (tptp.real2u (tptp.s2real (tptp.c_sort tptp.c_real @t8))) @t8))) % 0.43/0.82 (assume @p10 (forall (@list @t9) (= (tptp.unit2u (tptp.s2unit (tptp.c_sort tptp.c_unit @t9))) @t9))) % 0.43/0.82 (assume @p11 (forall (@list @t11 @t10) (= @t12 @t12))) % 0.43/0.82 (assume @p12 (forall (@list @t14 @t13) (= (= (tptp.bool_and @t14 @t13) tptp.c_Boolean_true) (and (= @t14 tptp.c_Boolean_true) (= @t13 tptp.c_Boolean_true))))) % 0.43/0.82 (assume @p13 (forall (@list @t16 @t15) (= (= (tptp.bool_or @t16 @t15) tptp.c_Boolean_true) (or (= @t16 tptp.c_Boolean_true) (= @t15 tptp.c_Boolean_true))))) % 0.43/0.82 (assume @p14 (forall (@list @t18 @t17) (= (= (tptp.bool_xor @t18 @t17) tptp.c_Boolean_true) (not (= @t18 @t17))))) % 0.43/0.82 (assume @p15 (forall (@list @t19) (= (= (tptp.bool_not @t19) tptp.c_Boolean_true) (= @t19 tptp.c_Boolean_false)))) % 0.43/0.82 (assume @p16 (forall (@list @t22 @t23 @t21) (exists (@list @t20) (and (= @t20 (tptp.c_sort @t22 @t23)) (= (tptp.c_sort @t22 (tptp.smtlib__ite tptp.c_Boolean_true @t20 (tptp.c_sort @t22 @t21))) @t20))))) % 0.43/0.82 (assume @p17 (forall (@list @t26 @t25 @t27) (exists (@list @t24) (and (= @t24 (tptp.c_sort @t26 @t27)) (= (tptp.c_sort @t26 (tptp.smtlib__ite tptp.c_Boolean_false (tptp.c_sort @t26 @t25) @t24)) @t24))))) % 0.43/0.82 (assume @p18 (forall (@list @t29 @t28) (= (= (tptp.lt_int_bool @t29 @t28) tptp.c_Boolean_true) (< @t29 @t28)))) % 0.43/0.82 (assume @p19 (forall (@list @t31 @t30) (= (= (tptp.le_int_bool @t31 @t30) tptp.c_Boolean_true) (<= @t31 @t30)))) % 0.43/0.82 (assume @p20 (forall (@list @t33 @t32) (= (= (tptp.gt_int_bool @t33 @t32) tptp.c_Boolean_true) (> @t33 @t32)))) % 0.43/0.82 (assume @p21 (forall (@list @t35 @t34) (= (= (tptp.ge_int_bool @t35 @t34) tptp.c_Boolean_true) (>= @t35 @t34)))) % 0.43/0.82 (assume @p22 (forall (@list @t37 @t36) (= (= (tptp.eq_int_bool @t37 @t36) tptp.c_Boolean_true) (= @t37 @t36)))) % 0.43/0.82 (assume @p23 (forall (@list @t39 @t38) (= (= (tptp.neq_int_bool @t39 @t38) tptp.c_Boolean_true) (not (= @t39 @t38))))) % 0.43/0.82 (assume @p24 (forall (@list @t40) (=> (>= @t40 0) (= (tptp.abs_int @t40) @t40)))) % 0.43/0.82 (assume @p25 (forall (@list @t41) (=> (<= @t41 0) (= (tptp.abs_int @t41) (- @t41))))) % 0.43/0.82 (assume @p26 (forall (@list @t44 @t42) (exists (@list @t43) (and (= @t43 (tptp.int_max @t44 @t42)) (>= @t43 @t44) (>= @t43 @t42))))) % 0.43/0.82 (assume @p27 (forall (@list @t47 @t45) (exists (@list @t46) (and (= @t46 (tptp.int_max @t47 @t45)) (or (= @t46 @t47) (= @t46 @t45)))))) % 0.43/0.82 (assume @p28 (forall (@list @t50 @t48) (exists (@list @t49) (and (= @t49 (tptp.int_min @t50 @t48)) (<= @t49 @t50) (<= @t49 @t48))))) % 0.43/0.82 (assume @p29 (forall (@list @t53 @t51) (exists (@list @t52) (and (= @t52 (tptp.int_min @t53 @t51)) (or (= @t52 @t53) (= @t52 @t51)))))) % 0.43/0.82 (assume @p30 (forall (@list @t55 @t54) (= (= (tptp.lt_real_bool @t55 @t54) tptp.c_Boolean_true) (< @t55 @t54)))) % 0.43/0.82 (assume @p31 (forall (@list @t57 @t56) (= (= (tptp.le_real_bool @t57 @t56) tptp.c_Boolean_true) (<= @t57 @t56)))) % 0.43/0.82 (assume @p32 (forall (@list @t59 @t58) (= (= (tptp.gt_real_bool @t59 @t58) tptp.c_Boolean_true) (> @t59 @t58)))) % 0.43/0.82 (assume @p33 (forall (@list @t61 @t60) (= (= (tptp.ge_real_bool @t61 @t60) tptp.c_Boolean_true) (>= @t61 @t60)))) % 0.43/0.82 (assume @p34 (forall (@list @t63 @t62) (= (= (tptp.eq_real_bool @t63 @t62) tptp.c_Boolean_true) (= @t63 @t62)))) % 0.43/0.82 (assume @p35 (forall (@list @t65 @t64) (= (= (tptp.neq_real_bool @t65 @t64) tptp.c_Boolean_true) (not (= @t65 @t64))))) % 0.43/0.82 (assume @p36 (forall (@list @t68 @t66) (exists (@list @t67) (and (= @t67 (tptp.real_max @t68 @t66)) (>= @t67 @t68) (>= @t67 @t66))))) % 0.43/0.82 (assume @p37 (forall (@list @t71 @t69) (exists (@list @t70) (and (= @t70 (tptp.real_max @t71 @t69)) (or (= @t70 @t71) (= @t70 @t69)))))) % 0.43/0.82 (assume @p38 (forall (@list @t74 @t72) (exists (@list @t73) (and (= @t73 (tptp.real_min @t74 @t72)) (<= @t73 @t74) (<= @t73 @t72))))) % 0.43/0.82 (assume @p39 (forall (@list @t77 @t75) (exists (@list @t76) (and (= @t76 (tptp.real_min @t77 @t75)) (or (= @t76 @t77) (= @t76 @t75)))))) % 0.43/0.82 (assume @p40 (forall (@list @t78) (=> (>= @t78 0/1) (= (tptp.abs_real @t78) @t78)))) % 0.43/0.82 (assume @p41 (forall (@list @t79) (=> (<= @t79 0/1) (= (tptp.abs_real @t79) (- @t79))))) % 0.43/0.82 (assume @p42 (forall (@list @t80) (= (tptp.log (tptp.exp @t80)) @t80))) % 0.43/0.82 (assume @p43 (forall (@list @t84 @t85 @t83) (exists (@list @t82 @t81) (and (= @t82 (tptp.c_sort (tptp.alloc_table @t84) @t85)) (= @t81 (tptp.c_sort (tptp.pointer @t84) @t83)) (= (tptp.valid @t82 @t81) (and (<= (tptp.offset_min @t82 @t81) 0) (>= (tptp.offset_max @t82 @t81) 0))))))) % 0.43/0.82 (assume @p44 (forall (@list @t89 @t92 @t90) (exists (@list @t91) (and (= @t91 (tptp.pointer @t89)) (exists (@list @t88 @t86 @t87) (and (= @t88 (tptp.c_sort @t91 @t92)) (= @t86 (tptp.c_sort @t91 @t90)) (= @t87 (tptp.block @t89)) (= (tptp.same_block @t88 @t86) (= (tptp.c_sort @t87 (tptp.base_block @t88)) (tptp.c_sort @t87 (tptp.base_block @t86)))))))))) % 0.43/0.82 (assume @p45 (forall (@list @t98 @t97 @t95) (exists (@list @t96) (and (= @t96 (tptp.pointer @t98)) (exists (@list @t94 @t93) (and (= @t94 (tptp.c_sort @t96 @t97)) (= @t93 (tptp.c_sort @t96 @t95)) (= (= @t94 @t93) (= (tptp.address @t94) (tptp.address @t93))))))))) % 0.43/0.82 (assume @p46 (forall (@list @t99) (= (tptp.address (tptp.c_sort (tptp.pointer @t99) tptp.null)) 0))) % 0.43/0.82 (assume @p47 (forall (@list @t101 @t100) (<= 0 (tptp.address (tptp.c_sort (tptp.pointer @t101) @t100))))) % 0.43/0.82 (assume @p48 (forall (@list @t107 @t106 @t103 @t102) (exists (@list @t105) (and (= @t105 (tptp.pointer @t107)) (exists (@list @t104) (and (= @t104 (tptp.c_sort @t105 @t106)) (= (< (tptp.address (tptp.c_sort @t105 (tptp.shift @t104 @t103))) (tptp.address (tptp.c_sort @t105 (tptp.shift @t104 @t102)))) (< @t103 @t102)))))))) % 0.43/0.82 (assume @p49 (forall (@list @t113 @t112 @t109 @t108) (exists (@list @t111) (and (= @t111 (tptp.pointer @t113)) (exists (@list @t110) (and (= @t110 (tptp.c_sort @t111 @t112)) (= (<= (tptp.address (tptp.c_sort @t111 (tptp.shift @t110 @t109))) (tptp.address (tptp.c_sort @t111 (tptp.shift @t110 @t108)))) (<= @t109 @t108)))))))) % 0.43/0.82 (assume @p50 (forall (@list @t117 @t116) (exists (@list @t115) (and (= @t115 (tptp.pointer @t117)) (exists (@list @t114) (and (= @t114 (tptp.c_sort @t115 @t116)) (= (tptp.c_sort @t115 (tptp.shift @t114 0)) @t114))))))) % 0.43/0.82 (assume @p51 (forall (@list @t123 @t122 @t119 @t118) (exists (@list @t121) (and (= @t121 (tptp.pointer @t123)) (exists (@list @t120) (and (= @t120 (tptp.c_sort @t121 @t122)) (= (tptp.c_sort @t121 (tptp.shift (tptp.c_sort @t121 (tptp.shift @t120 @t119)) @t118)) (tptp.c_sort @t121 (tptp.shift @t120 (+ @t119 @t118)))))))))) % 0.43/0.82 (assume @p52 (forall (@list @t129 @t130 @t128 @t124) (exists (@list @t126 @t127) (and (= @t126 (tptp.c_sort (tptp.alloc_table @t129) @t130)) (= @t127 (tptp.pointer @t129)) (exists (@list @t125) (and (= @t125 (tptp.c_sort @t127 @t128)) (= (tptp.offset_max @t126 (tptp.c_sort @t127 (tptp.shift @t125 @t124))) (- (tptp.offset_max @t126 @t125) @t124)))))))) % 0.43/0.82 (assume @p53 (forall (@list @t136 @t137 @t135 @t131) (exists (@list @t133 @t134) (and (= @t133 (tptp.c_sort (tptp.alloc_table @t136) @t137)) (= @t134 (tptp.pointer @t136)) (exists (@list @t132) (and (= @t132 (tptp.c_sort @t134 @t135)) (= (tptp.offset_min @t133 (tptp.c_sort @t134 (tptp.shift @t132 @t131))) (- (tptp.offset_min @t133 @t132) @t131)))))))) % 0.43/0.82 (assume @p54 (forall (@list @t143 @t142 @t141 @t138) (exists (@list @t140) (and (= @t140 (tptp.pointer @t143)) (exists (@list @t139) (and (= @t139 (tptp.c_sort @t140 @t142)) (=> (not (= @t141 @t138)) (not (= (tptp.c_sort @t140 (tptp.shift @t139 @t141)) (tptp.c_sort @t140 (tptp.shift @t139 @t138))))))))))) % 0.43/0.82 (assume @p55 (forall (@list @t144 @t145) (not (tptp.valid (tptp.c_sort (tptp.alloc_table @t144) @t145) (tptp.c_sort (tptp.pointer @t144) tptp.null))))) % 0.43/0.82 (assume @p56 (forall (@list @t148 @t149) (exists (@list @t147 @t146) (and (= @t147 (tptp.c_sort (tptp.alloc_table @t148) @t149)) (= @t146 (tptp.c_sort (tptp.pointer @t148) tptp.null)) (>= (tptp.offset_min @t147 @t146) 0) (<= (tptp.offset_max @t147 @t146) (- 2)))))) % 0.43/0.82 (assume @p57 (forall (@list @t155 @t154 @t152) (exists (@list @t153) (and (= @t153 (tptp.pointer @t155)) (exists (@list @t151 @t150) (and (= @t151 (tptp.c_sort @t153 @t154)) (= @t150 (tptp.c_sort @t153 @t152)) (= (= (tptp.eq_pointer_bool @t151 @t150) tptp.c_Boolean_true) (= @t151 @t150)))))))) % 0.43/0.82 (assume @p58 (forall (@list @t161 @t160 @t158) (exists (@list @t159) (and (= @t159 (tptp.pointer @t161)) (exists (@list @t157 @t156) (and (= @t157 (tptp.c_sort @t159 @t160)) (= @t156 (tptp.c_sort @t159 @t158)) (= (= (tptp.neq_pointer_bool @t157 @t156) tptp.c_Boolean_true) (not (= @t157 @t156))))))))) % 0.43/0.82 (assume @p59 (forall (@list @t168 @t167 @t166 @t162) (exists (@list @t164) (and (= @t164 (tptp.pointer @t168)) (exists (@list @t165 @t163) (and (= @t165 (tptp.c_sort @t164 @t167)) (= @t163 (tptp.c_sort @t164 @t166)) (=> (tptp.same_block @t165 @t163) (tptp.same_block @t165 (tptp.c_sort @t164 (tptp.shift @t163 @t162)))))))))) % 0.43/0.82 (assume @p60 (forall (@list @t175 @t173 @t174 @t170) (exists (@list @t172) (and (= @t172 (tptp.pointer @t175)) (exists (@list @t171 @t169) (and (= @t171 (tptp.c_sort @t172 @t174)) (= @t169 (tptp.c_sort @t172 @t173)) (=> (tptp.same_block @t171 @t169) (tptp.same_block (tptp.c_sort @t172 (tptp.shift @t171 @t170)) @t169)))))))) % 0.43/0.82 (assume @p61 (forall (@list @t181 @t180 @t179) (exists (@list @t178) (and (= @t178 (tptp.pointer @t181)) (exists (@list @t177 @t176) (and (= @t177 (tptp.c_sort @t178 @t180)) (= @t176 (tptp.c_sort @t178 @t179)) (=> (tptp.same_block @t177 @t176) (= @t177 (tptp.c_sort @t178 (tptp.shift @t176 (tptp.sub_pointer @t177 @t176))))))))))) % 0.43/0.82 (assume @p62 (forall (@list @t184 @t183) (exists (@list @t182) (and (= @t182 (tptp.c_sort (tptp.pointer @t184) @t183)) (= (tptp.sub_pointer @t182 @t182) 0))))) % 0.43/0.82 (assume @p63 (forall (@list @t190 @t189 @t187) (exists (@list @t188) (and (= @t188 (tptp.pointer @t190)) (exists (@list @t186 @t185) (and (= @t186 (tptp.c_sort @t188 @t189)) (= @t185 (tptp.c_sort @t188 @t187)) (=> (tptp.same_block @t186 @t185) (=> (= (tptp.sub_pointer @t186 @t185) 0) (= @t186 @t185))))))))) % 0.43/0.82 (assume @p64 (forall (@list @t197 @t196 @t195 @t191) (exists (@list @t194) (and (= @t194 (tptp.pointer @t197)) (exists (@list @t193 @t192) (and (= @t193 (tptp.c_sort @t194 @t196)) (= @t192 (tptp.c_sort @t194 @t195)) (= (tptp.sub_pointer (tptp.c_sort @t194 (tptp.shift @t193 @t191)) @t192) (+ (tptp.sub_pointer @t193 @t192) @t191)))))))) % 0.43/0.82 (assume @p65 (forall (@list @t204 @t203 @t202 @t198) (exists (@list @t201) (and (= @t201 (tptp.pointer @t204)) (exists (@list @t200 @t199) (and (= @t200 (tptp.c_sort @t201 @t203)) (= @t199 (tptp.c_sort @t201 @t202)) (= (tptp.sub_pointer @t200 (tptp.c_sort @t201 (tptp.shift @t199 @t198))) (- (tptp.sub_pointer @t200 @t199) @t198)))))))) % 0.43/0.82 (assume @p66 (forall (@list @t210 @t212 @t208 @t215 @t213 @t211) (exists (@list @t214) (and (= @t214 (tptp.pointer @t212)) (exists (@list @t207 @t206 @t209 @t205) (and (= @t207 (tptp.c_sort @t214 @t215)) (= @t206 (tptp.c_sort @t214 @t213)) (= @t209 (tptp.memory @t212 @t210)) (= @t205 (tptp.c_sort @t210 @t211)) (=> (= @t207 @t206) (= (tptp.c_sort @t210 (tptp.smtlib__select (tptp.c_sort @t209 (tptp.smtlib__store (tptp.c_sort @t209 @t208) @t207 @t205)) @t206)) @t205)))))))) % 0.43/0.82 (assume @p67 (forall (@list @t218 @t223 @t222 @t226 @t224 @t219) (exists (@list @t225) (and (= @t225 (tptp.pointer @t223)) (exists (@list @t220 @t216 @t221) (and (= @t220 (tptp.c_sort @t225 @t226)) (= @t216 (tptp.c_sort @t225 @t224)) (= @t221 (tptp.memory @t223 @t218)) (exists (@list @t217) (and (= @t217 (tptp.c_sort @t221 @t222)) (=> (not (= @t220 @t216)) (= (tptp.c_sort @t218 (tptp.smtlib__select (tptp.c_sort @t221 (tptp.smtlib__store @t217 @t220 (tptp.c_sort @t218 @t219))) @t216)) (tptp.c_sort @t218 (tptp.smtlib__select @t217 @t216)))))))))))) % 0.43/0.82 (assume @p68 (forall (@list @t234 @t231 @t227) (exists (@list @t228) (and (= @t228 (tptp.pset @t234)) (= (tptp.pset_disjoint @t232 @t229) (forall (@list @t233) (exists (@list @t230) (and (= @t230 (tptp.c_sort (tptp.pointer @t234) @t233)) (not (and (tptp.in_pset @t230 @t232) (tptp.in_pset @t230 @t229))))))))))) % 0.43/0.82 (assume @p69 (forall (@list @t242 @t239 @t235) (exists (@list @t236) (and (= @t236 (tptp.pset @t242)) (= (tptp.pset_included @t240 @t237) (forall (@list @t241) (exists (@list @t238) (and (= @t238 (tptp.c_sort (tptp.pointer @t242) @t241)) (=> (tptp.in_pset @t238 @t240) (tptp.in_pset @t238 @t237)))))))))) % 0.43/0.82 (assume @p70 (forall (@list @t245 @t244) (exists (@list @t243) (and (= @t243 (tptp.c_sort (tptp.pset @t245) @t244)) (tptp.pset_included @t243 @t243))))) % 0.43/0.82 (assume @p71 (forall (@list @t253 @t252 @t251 @t250 @t247 @t246) (exists (@list @t249) (and (= @t249 (tptp.pset @t253)) (exists (@list @t248) (and (= @t248 (tptp.c_sort @t249 @t252)) (=> (and (<= @t247 @t251) (<= @t250 @t246)) (tptp.pset_included (tptp.c_sort @t249 (tptp.pset_range @t248 @t251 @t250)) (tptp.c_sort @t249 (tptp.pset_range @t248 @t247 @t246)))))))))) % 0.43/0.82 (assume @p72 (forall (@list @t259 @t258 @t257 @t256 (@var "A__questionmark_cu270_173" Int) (@var "A__questionmark_du269_174" Int)) (exists (@list @t255) (and (= @t255 (tptp.pset @t259)) (exists (@list @t254) (and (= @t254 (tptp.c_sort @t255 @t258)) (tptp.pset_included (tptp.c_sort @t255 (tptp.pset_range @t254 @t257 @t256)) (tptp.c_sort @t255 (tptp.pset_all @t254))))))))) % 0.43/0.82 (assume @p73 (forall (@list @t260 @t261) (not (tptp.in_pset (tptp.c_sort (tptp.pointer @t260) @t261) (tptp.c_sort (tptp.pset @t260) tptp.pset_empty))))) % 0.43/0.82 (assume @p74 (forall (@list @t264 @t267 @t265) (exists (@list @t266) (and (= @t266 (tptp.pointer @t264)) (exists (@list @t263 @t262) (and (= @t263 (tptp.c_sort @t266 @t267)) (= @t262 (tptp.c_sort @t266 @t265)) (= (tptp.in_pset @t263 (tptp.c_sort (tptp.pset @t264) (tptp.pset_singleton @t262))) (= @t263 @t262)))))))) % 0.43/0.82 (assume @p75 (forall (@list @t271 @t278 @t273 @t269 @t275) (exists (@list @t270) (and (= @t270 (tptp.pointer @t278)) (= (tptp.in_pset @t274 (tptp.c_sort (tptp.pset @t278) (tptp.pset_deref @t272 @t276))) (exists (@list @t277 @t268) (and (= @t268 (tptp.c_sort (tptp.pointer @t271) @t277)) (tptp.in_pset @t268 @t276) (= @t274 (tptp.c_sort @t270 (tptp.smtlib__select @t272 @t268)))))))))) % 0.43/0.82 (assume @p76 (forall (@list @t287 @t282 @t283) (exists (@list @t284) (and (= @t284 (tptp.pset @t287)) (= (tptp.in_pset (tptp.c_sort @t288 @t282) (tptp.c_sort @t284 (tptp.pset_all @t285))) (exists (@list @t279 @t286 @t281) (and (= @t281 @t288) (exists (@list @t280) (and (= @t280 (tptp.c_sort @t281 @t286)) (tptp.in_pset @t280 @t285) (= (tptp.c_sort @t281 @t282) (tptp.c_sort @t281 (tptp.shift @t280 @t279)))))))))))) % 0.43/0.82 (assume @p77 (forall (@list @t299 @t292 @t293 @t297 @t296) (exists (@list @t294) (and (= @t294 (tptp.pset @t299)) (= (tptp.in_pset (tptp.c_sort @t300 @t292) (tptp.c_sort @t294 (tptp.pset_range @t295 @t297 @t296))) (exists (@list @t289 @t298 @t291) (and (= @t291 @t300) (exists (@list @t290) (and (= @t290 (tptp.c_sort @t291 @t298)) (<= @t297 @t289) (<= @t289 @t296) (tptp.in_pset @t290 @t295) (= (tptp.c_sort @t291 @t292) (tptp.c_sort @t291 (tptp.shift @t290 @t289)))))))))))) % 0.43/0.82 (assume @p78 (forall (@list @t310 @t304 @t305 @t308) (exists (@list @t306) (and (= @t306 (tptp.pset @t310)) (= (tptp.in_pset (tptp.c_sort @t311 @t304) (tptp.c_sort @t306 (tptp.pset_range_left @t307 @t308))) (exists (@list @t301 @t309 @t303) (and (= @t303 @t311) (exists (@list @t302) (and (= @t302 (tptp.c_sort @t303 @t309)) (<= @t301 @t308) (tptp.in_pset @t302 @t307) (= (tptp.c_sort @t303 @t304) (tptp.c_sort @t303 (tptp.shift @t302 @t301)))))))))))) % 0.43/0.82 (assume @p79 (forall (@list @t321 @t315 @t316 @t319) (exists (@list @t317) (and (= @t317 (tptp.pset @t321)) (= (tptp.in_pset (tptp.c_sort @t322 @t315) (tptp.c_sort @t317 (tptp.pset_range_right @t318 @t319))) (exists (@list @t312 @t320 @t314) (and (= @t314 @t322) (exists (@list @t313) (and (= @t313 (tptp.c_sort @t314 @t320)) (<= @t319 @t312) (tptp.in_pset @t313 @t318) (= (tptp.c_sort @t314 @t315) (tptp.c_sort @t314 (tptp.shift @t313 @t312)))))))))))) % 0.43/0.82 (assume @p80 (forall (@list @t329 @t330 @t328 @t327) (exists (@list @t324 @t326) (and (= @t324 (tptp.c_sort (tptp.pointer @t329) @t330)) (= @t326 (tptp.pset @t329)) (exists (@list @t325 @t323) (and (= @t325 (tptp.c_sort @t326 @t328)) (= @t323 (tptp.c_sort @t326 @t327)) (= (tptp.in_pset @t324 (tptp.c_sort @t326 (tptp.pset_union @t325 @t323))) (or (tptp.in_pset @t324 @t325) (tptp.in_pset @t324 @t323))))))))) % 0.43/0.82 (assume @p81 (forall (@list @t331 @t332) (tptp.valid_pset (tptp.c_sort (tptp.alloc_table @t331) @t332) (tptp.c_sort (tptp.pset @t331) tptp.pset_empty)))) % 0.43/0.82 (assume @p82 (forall (@list @t335 @t337 @t336) (exists (@list @t334 @t333) (and (= @t334 (tptp.c_sort (tptp.alloc_table @t335) @t337)) (= @t333 (tptp.c_sort (tptp.pointer @t335) @t336)) (= (tptp.valid_pset @t334 (tptp.c_sort (tptp.pset @t335) (tptp.pset_singleton @t333))) (tptp.valid @t334 @t333)))))) % 0.43/0.82 (assume @p83 (forall (@list @t345 @t340 @t339 @t343 @t346) (= (tptp.valid_pset @t341 (tptp.c_sort (tptp.pset @t340) (tptp.pset_deref (tptp.c_sort (tptp.memory @t345 @t350) @t343) @t347))) (forall (@list @t349 @t348) (exists (@list @t344 @t342) (and (= @t344 @t350) (= @t342 (tptp.c_sort (tptp.pointer @t345) @t349)) (exists (@list @t338) (and (= @t338 (tptp.c_sort @t344 @t348)) (=> (and (tptp.in_pset @t342 @t347) (= @t338 (tptp.c_sort @t344 (tptp.smtlib__select (tptp.c_sort (tptp.memory @t345 @t344) @t343) @t342)))) (tptp.valid @t341 @t338)))))))))) % 0.43/0.82 (assume @p84 (forall (@list @t355 @t354 @t359 @t358 @t357) (exists (@list @t360) (and (= @t360 (tptp.pset @t355)) (= (tptp.valid_pset @t356 (tptp.c_sort @t360 (tptp.pset_range @t361 @t358 @t357))) (forall (@list @t351 @t362) (exists (@list @t353) (and (= @t353 (tptp.pointer @t355)) (exists (@list @t352) (and (= @t352 (tptp.c_sort @t353 @t362)) (=> (and (tptp.in_pset @t352 @t361) (<= @t358 @t351) (<= @t351 @t357)) (tptp.valid @t356 (tptp.c_sort @t353 (tptp.shift @t352 @t351)))))))))))))) % 0.43/0.82 (assume @p85 (forall (@list @t369 @t370 @t368 @t367) (exists (@list @t364 @t366) (and (= @t364 (tptp.c_sort (tptp.alloc_table @t369) @t370)) (= @t366 (tptp.pset @t369)) (exists (@list @t365 @t363) (and (= @t365 (tptp.c_sort @t366 @t368)) (= @t363 (tptp.c_sort @t366 @t367)) (= (tptp.valid_pset @t364 (tptp.c_sort @t366 (tptp.pset_union @t365 @t363))) (and (tptp.valid_pset @t364 @t365) (tptp.valid_pset @t364 @t363))))))))) % 0.43/0.82 (assume @p86 (forall (@list @t375 @t379 @t381 @t372 @t376 @t378) (exists (@list @t373) (and (= @t373 (tptp.memory @t379 @t375)) (= (tptp.not_assigns @t382 @t374 @t377 @t380) (forall (@list @t383) (exists (@list @t371) (and (= @t371 (tptp.c_sort (tptp.pointer @t379) @t383)) (=> (and (tptp.valid @t382 @t371) (not (tptp.in_pset @t371 @t380))) (= (tptp.c_sort @t375 (tptp.smtlib__select @t377 @t371)) (tptp.c_sort @t375 (tptp.smtlib__select @t374 @t371)))))))))))) % 0.43/0.82 (assume @p87 (forall (@list @t389 @t385 @t387 @t388 @t384) (exists (@list @t386) (and (= @t386 (tptp.c_sort (tptp.memory @t385 @t389) @t388)) (tptp.not_assigns (tptp.c_sort (tptp.alloc_table @t385) @t387) @t386 @t386 (tptp.c_sort (tptp.pset @t385) @t384)))))) % 0.43/0.82 (assume @p88 (forall (@list @t401 @t398 @t402 @t400 @t399 @t395 @t397) (exists (@list @t393 @t396) (and (= @t393 (tptp.c_sort (tptp.alloc_table @t398) @t402)) (= @t396 (tptp.memory @t398 @t401)) (exists (@list @t392 @t394 @t390 @t391) (and (= @t392 (tptp.c_sort @t396 @t400)) (= @t394 (tptp.c_sort @t396 @t399)) (= @t390 (tptp.c_sort (tptp.pset @t398) @t397)) (= @t391 (tptp.c_sort @t396 @t395)) (=> (tptp.not_assigns @t393 @t392 @t394 @t390) (=> (tptp.not_assigns @t393 @t394 @t391 @t390) (tptp.not_assigns @t393 @t392 @t391 @t390))))))))) % 0.43/0.82 (assume @p89 (forall (@list @t409 @t408 @t407 @t403) (exists (@list @t405) (and (= @t405 (tptp.pointer @t409)) (exists (@list @t406 @t404) (and (= @t406 (tptp.c_sort @t405 @t408)) (= @t404 (tptp.c_sort @t405 @t407)) (=> (tptp.full_separated @t406 @t404) (tptp.full_separated @t406 (tptp.c_sort @t405 (tptp.shift @t404 @t403)))))))))) % 0.43/0.82 (assume @p90 (forall (@list @t416 @t415 @t414 @t411) (exists (@list @t413) (and (= @t413 (tptp.pointer @t416)) (exists (@list @t410 @t412) (and (= @t410 (tptp.c_sort @t413 @t415)) (= @t412 (tptp.c_sort @t413 @t414)) (=> (tptp.full_separated @t410 @t412) (tptp.full_separated (tptp.c_sort @t413 (tptp.shift @t412 @t411)) @t410)))))))) % 0.43/0.82 (assume @p91 (forall (@list @t423 @t421 @t422 @t418) (exists (@list @t420) (and (= @t420 (tptp.pointer @t423)) (exists (@list @t419 @t417) (and (= @t419 (tptp.c_sort @t420 @t422)) (= @t417 (tptp.c_sort @t420 @t421)) (=> (tptp.full_separated @t419 @t417) (tptp.full_separated (tptp.c_sort @t420 (tptp.shift @t419 @t418)) @t417)))))))) % 0.43/0.82 (assume @p92 (forall (@list @t430 @t428 @t429 @t424) (exists (@list @t426) (and (= @t426 (tptp.pointer @t430)) (exists (@list @t425 @t427) (and (= @t425 (tptp.c_sort @t426 @t429)) (= @t427 (tptp.c_sort @t426 @t428)) (=> (tptp.full_separated @t425 @t427) (tptp.full_separated @t427 (tptp.c_sort @t426 (tptp.shift @t425 @t424)))))))))) % 0.43/0.82 (assume @p93 (forall (@list @t436 @t435 @t433) (exists (@list @t434) (and (= @t434 (tptp.tag_id @t436)) (exists (@list @t432 @t431) (and (= @t432 (tptp.c_sort @t434 @t435)) (= @t431 (tptp.c_sort @t434 @t433)) (= (= (tptp.subtag_bool @t432 @t431) tptp.c_Boolean_true) (tptp.subtag @t432 @t431)))))))) % 0.43/0.82 (assume @p94 (forall (@list @t439 @t438) (exists (@list @t437) (and (= @t437 (tptp.c_sort (tptp.tag_id @t439) @t438)) (tptp.subtag @t437 @t437))))) % 0.43/0.82 (assume @p95 (forall (@list @t447 @t446 @t445 @t443) (exists (@list @t444) (and (= @t444 (tptp.tag_id @t447)) (exists (@list @t441 @t442 @t440) (and (= @t441 (tptp.c_sort @t444 @t446)) (= @t442 (tptp.c_sort @t444 @t445)) (= @t440 (tptp.c_sort @t444 @t443)) (=> (tptp.subtag @t441 @t442) (=> (tptp.parenttag @t442 @t440) (tptp.subtag @t441 @t440))))))))) % 0.43/0.82 (assume @p96 (forall (@list @t453 @t455 @t454 @t452) (exists (@list @t450 @t449 @t451) (and (= @t450 (tptp.c_sort (tptp.tag_table @t453) @t455)) (= @t449 (tptp.c_sort (tptp.pointer @t453) @t454)) (= @t451 (tptp.tag_id @t453)) (exists (@list @t448) (and (= @t448 (tptp.c_sort @t451 @t452)) (= (tptp.instanceof @t450 @t449 @t448) (tptp.subtag (tptp.c_sort @t451 (tptp.typeof @t450 @t449)) @t448)))))))) % 0.43/0.82 (assume @p97 (forall (@list @t461 @t463 @t462 @t460) (exists (@list @t458 @t459) (and (= @t458 (tptp.c_sort (tptp.tag_table @t461) @t463)) (= @t459 (tptp.pointer @t461)) (exists (@list @t456 @t457) (and (= @t456 (tptp.c_sort @t459 @t462)) (= @t457 (tptp.c_sort (tptp.tag_id @t461) @t460)) (=> (tptp.instanceof @t458 @t456 @t457) (= (tptp.c_sort @t459 (tptp.downcast @t458 @t456 @t457)) @t456)))))))) % 0.43/0.82 (assume @p98 (forall (@list @t466 @t465) (exists (@list @t464) (and (= @t464 (tptp.tag_id @t466)) (tptp.subtag (tptp.c_sort @t464 @t465) (tptp.c_sort @t464 tptp.bottom_tag)))))) % 0.43/0.82 (assume @p99 (forall (@list @t470 @t469) (exists (@list @t467) (and (= @t467 (tptp.tag_id @t470)) (exists (@list @t468) (and (= @t468 (tptp.c_sort @t467 @t469)) (= (tptp.root_tag @t468) (tptp.parenttag @t468 (tptp.c_sort @t467 tptp.bottom_tag))))))))) % 0.43/0.82 (assume @p100 (forall (@list @t478 @t477 @t476 @t474) (exists (@list @t475) (and (= @t475 (tptp.tag_id @t478)) (exists (@list @t473 @t471 @t472) (and (= @t473 (tptp.c_sort @t475 @t477)) (= @t471 (tptp.c_sort @t475 @t476)) (= @t472 (tptp.c_sort @t475 @t474)) (=> (tptp.root_tag @t473) (=> (tptp.root_tag @t471) (=> (not (= @t473 @t471)) (=> (tptp.subtag @t472 @t473) (not (tptp.subtag @t472 @t471)))))))))))) % 0.43/0.82 (assume @p101 (forall (@list @t484 @t486 @t485 @t483) (exists (@list @t480 @t481) (and (= @t480 (tptp.c_sort (tptp.tag_table @t484) @t486)) (= @t481 (tptp.tag_id @t484)) (exists (@list @t482 @t479) (and (= @t482 (tptp.c_sort (tptp.memory @t484 @t481) @t485)) (= @t479 (tptp.c_sort (tptp.pointer @t484) @t483)) (= (tptp.fully_packed @t480 @t482 @t479) (= (tptp.c_sort @t481 (tptp.smtlib__select @t482 @t479)) (tptp.c_sort @t481 (tptp.typeof @t480 @t479)))))))))) % 0.43/0.82 (assume @p102 (forall (@list @t488 @t487) (=> (not (= (tptp.bw_and @t488 @t487) 0)) (and (not (= @t488 0)) (not (= @t487 0)))))) % 0.43/0.82 (assume @p103 (forall (@list @t490 @t489) (=> (and (<= 0 @t490) (<= 0 @t489)) (<= 0 (tptp.lsl @t490 @t489))))) % 0.43/0.82 (assume @p104 (forall (@list @t493 @t492 @t491) (=> (and (<= 0 @t493) (<= @t493 @t492) (<= 0 @t491)) (<= (tptp.lsl @t493 @t491) (tptp.lsl @t492 @t491))))) % 0.43/0.82 (assume @p105 (forall (@list @t495 @t494) (=> (and (<= 0 @t495) (<= 0 @t494)) (<= 0 (tptp.lsr @t495 @t494))))) % 0.43/0.82 (assume @p106 (forall (@list @t496 @t497) (=> (and (<= 0 @t496) (<= 0 @t497)) (<= (tptp.lsr @t496 @t497) @t496)))) % 0.43/0.82 (assume @p107 (forall (@list @t499 @t498) (=> (and (<= 0 @t499) (<= 0 @t498)) (<= 0 (tptp.asr @t499 @t498))))) % 0.43/0.82 (assume @p108 (forall (@list @t500 @t501) (=> (and (<= 0 @t500) (<= 0 @t501)) (<= (tptp.asr @t500 @t501) @t500)))) % 0.43/0.82 (assume @p109 (forall (@list @t503 @t502) (=> (and (<= 0 @t503) (<= 0 @t502)) (= (tptp.asr @t503 @t502) (tptp.lsr @t503 @t502))))) % 0.43/0.82 (assume @p110 (forall (@list @t504 @t505) (=> (and (<= 0 @t504) (<= 0 @t505)) (<= (tptp.lsl (tptp.lsr @t504 @t505) @t505) @t504)))) % 0.43/0.82 (assume @p111 (forall (@list @t506 @t507) (=> (and (<= 0 @t506) (<= 0 @t507)) (= (tptp.lsr (tptp.lsl @t506 @t507) @t507) @t506)))) % 0.43/0.82 (assume @p112 (forall (@list @t512 @t511 @t509 @t514) (= (tptp.alloc_fresh @t513 (tptp.c_sort @t515 @t509) @t514) (forall (@list @t508) (exists (@list @t510) (and (= @t510 @t515) (=> (and (<= 0 @t508) (< @t508 @t514)) (not (tptp.valid @t513 (tptp.c_sort @t510 (tptp.shift (tptp.c_sort @t510 @t509) @t508))))))))))) % 0.43/0.82 (assume @p113 (forall (@list @t522 @t523 @t517) (exists (@list @t518) (and (= @t518 (tptp.alloc_table @t522)) (=> (tptp.alloc_extends @t524 @t519) (forall (@list @t521) (exists (@list @t520 @t516) (and (= @t520 @t524) (= @t516 (tptp.c_sort (tptp.pointer @t522) @t521)) (=> (tptp.valid @t520 @t516) (= (tptp.offset_min @t520 @t516) (tptp.offset_min @t519 @t516))))))))))) % 0.43/0.82 (assume @p114 (forall (@list @t531 @t532 @t526) (exists (@list @t527) (and (= @t527 (tptp.alloc_table @t531)) (=> (tptp.alloc_extends @t533 @t528) (forall (@list @t530) (exists (@list @t529 @t525) (and (= @t529 @t533) (= @t525 (tptp.c_sort (tptp.pointer @t531) @t530)) (=> (tptp.valid @t529 @t525) (= (tptp.offset_max @t529 @t525) (tptp.offset_max @t528 @t525))))))))))) % 0.43/0.82 (assume @p115 (forall (@list @t547 @t543 @t551 @t549 @t546 @t544 @t542 @t548 @t541) (exists (@list @t550) (and (= @t550 (tptp.alloc_table @t543)) (exists (@list @t537 @t540 @t538 @t545) (and (= @t537 (tptp.c_sort @t550 @t551)) (= @t540 (tptp.c_sort @t550 @t549)) (= @t538 (tptp.c_sort (tptp.pointer @t543) @t548)) (= @t545 (tptp.memory @t543 @t547)) (exists (@list @t536 @t535 @t534) (and (= @t536 (tptp.c_sort @t545 @t546)) (= @t535 (tptp.c_sort @t545 @t544)) (= @t534 (tptp.pset @t543)) (exists (@list @t539) (and (= @t539 (tptp.c_sort @t534 @t542)) (=> (and (tptp.alloc_extends @t537 @t540) (tptp.alloc_fresh @t537 @t538 @t541) (tptp.not_assigns @t540 @t536 @t535 @t539) (tptp.pset_included @t539 (tptp.c_sort @t534 (tptp.pset_all (tptp.c_sort @t534 (tptp.pset_singleton @t538)))))) (tptp.not_assigns @t537 @t536 @t535 (tptp.c_sort @t534 tptp.pset_empty))))))))))))) % 0.43/0.82 (assume @p116 (forall (@list @t558 @t561 @t553 @t557) (exists (@list @t554) (and (= @t554 (tptp.alloc_table @t558)) (=> (tptp.alloc_extends_except @t562 @t555 @t559) (forall (@list @t560) (exists (@list @t556 @t552) (and (= @t556 @t562) (= @t552 (tptp.c_sort (tptp.pointer @t558) @t560)) (=> (and (tptp.valid @t556 @t552) (not (tptp.in_pset @t552 @t559))) (= (tptp.offset_min @t556 @t552) (tptp.offset_min @t555 @t552))))))))))) % 0.43/0.82 (assume @p117 (forall (@list @t569 @t572 @t564 @t568) (exists (@list @t565) (and (= @t565 (tptp.alloc_table @t569)) (=> (tptp.alloc_extends_except @t573 @t566 @t570) (forall (@list @t571) (exists (@list @t567 @t563) (and (= @t567 @t573) (= @t563 (tptp.c_sort (tptp.pointer @t569) @t571)) (=> (and (tptp.valid @t567 @t563) (not (tptp.in_pset @t563 @t570))) (= (tptp.offset_max @t567 @t563) (tptp.offset_max @t566 @t563))))))))))) % 0.43/0.82 (assume @p118 (forall (@list @t580 @t581 @t579 @t575) (exists (@list @t578 @t577) (and (= @t578 (tptp.c_sort (tptp.alloc_table @t580) @t581)) (= @t577 (tptp.c_sort (tptp.pointer @t580) @t579)) (exists (@list @t576 @t574) (and (= @t576 (* @t575 (tptp.offset_min_bytes @t578 @t577 @t575))) (= @t574 (tptp.offset_min @t578 @t577)) (=> (< 0 @t575) (and (<= @t574 @t576) (< (- @t576 @t575) @t574))))))))) % 0.43/0.82 (assume @p119 (forall (@list @t588 @t589 @t587 @t582) (exists (@list @t586 @t585) (and (= @t586 (tptp.c_sort (tptp.alloc_table @t588) @t589)) (= @t585 (tptp.c_sort (tptp.pointer @t588) @t587)) (exists (@list @t584 @t583) (and (= @t584 (tptp.offset_max @t586 @t585)) (= @t583 (+ (* @t582 (tptp.offset_max_bytes @t586 @t585 @t582)) @t582)) (=> (< 0 @t582) (and (<= (- @t583 1) @t584) (< @t584 (- (+ @t583 @t582) 1)))))))))) % 0.43/0.82 (assume @p120 (forall (@list @t594 @t593 @t592 @t591 @t595 @t596) (exists (@list @t590) (and (= @t590 (tptp.c_sort tptp.bitvector @t596)) (=> (and (= @t594 @t592) (= @t593 @t591)) (= (tptp.c_sort tptp.bitvector (tptp.extract_bytes (tptp.c_sort tptp.bitvector (tptp.replace_bytes (tptp.c_sort tptp.bitvector @t595) @t594 @t593 @t590)) @t592 @t591)) @t590)))))) % 0.43/0.82 (assume @p121 (forall (@list @t602 @t601 @t598 @t597 @t603 @t600) (exists (@list @t599) (and (= @t599 (tptp.c_sort tptp.bitvector @t603)) (=> (or (<= (+ @t598 @t597) @t602) (<= (+ @t602 @t597) @t598)) (= (tptp.c_sort tptp.bitvector (tptp.extract_bytes (tptp.c_sort tptp.bitvector (tptp.replace_bytes @t599 @t602 @t601 (tptp.c_sort tptp.bitvector @t600))) @t598 @t597)) (tptp.c_sort tptp.bitvector (tptp.extract_bytes @t599 @t598 @t597)))))))) % 0.43/0.82 (assume @p122 (forall (@list @t608 @t607 @t610 @t606 @t613 @t612 @t611) (exists (@list @t609 @t605 @t604) (and (= @t609 (tptp.c_sort tptp.bitvector @t613)) (= @t605 (tptp.c_sort tptp.bitvector @t612)) (= @t604 (tptp.c_sort tptp.bitvector @t611)) (=> (= (+ @t608 @t607) @t610) (= (tptp.c_sort tptp.bitvector (tptp.replace_bytes (tptp.c_sort tptp.bitvector (tptp.replace_bytes @t609 @t608 @t607 @t605)) @t610 @t606 @t604)) (tptp.c_sort tptp.bitvector (tptp.replace_bytes @t609 @t608 (+ @t607 @t606) (tptp.c_sort tptp.bitvector (tptp.concat_bitvector @t605 @t604)))))))))) % 0.43/0.82 (assume @p123 (forall (@list @t620 @t617 @t618 @t616 @t623 @t622 @t621) (exists (@list @t619 @t614 @t615) (and (= @t619 (tptp.c_sort tptp.bitvector @t623)) (= @t614 (tptp.c_sort tptp.bitvector @t622)) (= @t615 (tptp.c_sort tptp.bitvector @t621)) (=> (= (+ @t618 @t616) @t620) (= (tptp.c_sort tptp.bitvector (tptp.replace_bytes (tptp.c_sort tptp.bitvector (tptp.replace_bytes @t619 @t620 @t617 @t614)) @t618 @t616 @t615)) (tptp.c_sort tptp.bitvector (tptp.replace_bytes @t619 @t618 (+ @t617 @t616) (tptp.c_sort tptp.bitvector (tptp.concat_bitvector @t615 @t614)))))))))) % 0.43/0.82 (assume @p124 (forall (@list @t626 @t625 @t628 @t624 @t629) (exists (@list @t627) (and (= @t627 (tptp.c_sort tptp.bitvector @t629)) (=> (= (+ @t626 @t625) @t628) (= (tptp.c_sort tptp.bitvector (tptp.concat_bitvector (tptp.c_sort tptp.bitvector (tptp.extract_bytes @t627 @t626 @t625)) (tptp.c_sort tptp.bitvector (tptp.extract_bytes @t627 @t628 @t624)))) (tptp.c_sort tptp.bitvector (tptp.extract_bytes @t627 @t626 (+ @t625 @t624))))))))) % 0.43/0.82 (assume @p125 (forall (@list @t640 @t637 @t643 @t641 @t635 @t634 @t632 @t631 @t639) (exists (@list @t642) (and (= @t642 (tptp.pointer @t640)) (exists (@list @t636 @t633 @t638 @t630) (and (= @t636 (tptp.c_sort @t642 @t643)) (= @t633 (tptp.c_sort @t642 @t641)) (= @t638 (tptp.memory @t640 tptp.bitvector)) (= @t630 (tptp.c_sort tptp.bitvector @t639)) (=> (and (= @t636 @t633) (= @t635 @t632) (= @t634 @t631)) (= (tptp.c_sort tptp.bitvector (tptp.select_bytes (tptp.c_sort @t638 (tptp.store_bytes (tptp.c_sort @t638 @t637) @t636 @t635 @t634 @t630)) @t633 @t632 @t631)) @t630)))))))) % 0.43/0.82 (assume @p126 (forall (@list @t655 @t654 @t658 @t656 @t650 @t649 @t645 @t644 @t648) (exists (@list @t653 @t657) (and (= @t653 (tptp.pset @t655)) (= @t657 (tptp.pointer @t655)) (exists (@list @t651 @t646 @t652) (and (= @t651 (tptp.c_sort @t657 @t658)) (= @t646 (tptp.c_sort @t657 @t656)) (= @t652 (tptp.memory @t655 tptp.bitvector)) (exists (@list @t647) (and (= @t647 (tptp.c_sort @t652 @t654)) (=> (tptp.pset_disjoint (tptp.c_sort @t653 (tptp.pset_range (tptp.c_sort @t653 (tptp.pset_singleton @t651)) @t650 (+ @t650 @t649))) (tptp.c_sort @t653 (tptp.pset_range (tptp.c_sort @t653 (tptp.pset_singleton @t646)) @t645 (+ @t645 @t644)))) (= (tptp.c_sort tptp.bitvector (tptp.select_bytes (tptp.c_sort @t652 (tptp.store_bytes @t647 @t651 @t650 @t649 (tptp.c_sort tptp.bitvector @t648))) @t646 @t645 @t644)) (tptp.c_sort tptp.bitvector (tptp.select_bytes @t647 @t646 @t645 @t644)))))))))))) % 0.43/0.82 (assume @p127 (forall (@list @t669 @t670 @t668 @t661 @t662 @t660 @t667) (exists (@list @t665) (and (= @t665 (tptp.memory @t669 tptp.bitvector)) (exists (@list @t664 @t666) (and (= @t664 (tptp.c_sort @t665 @t670)) (= @t666 (tptp.pointer @t669)) (exists (@list @t663 @t659) (and (= @t663 (tptp.c_sort @t666 @t668)) (= @t659 (tptp.c_sort tptp.bitvector @t667)) (= (tptp.c_sort @t665 (tptp.store_bytes @t664 (tptp.c_sort @t666 (tptp.shift @t663 @t661)) @t662 @t660 @t659)) (tptp.c_sort @t665 (tptp.store_bytes @t664 @t663 (+ @t662 @t661) @t660 @t659))))))))))) % 0.43/0.82 (assume @p128 (forall (@list @t678 @t679 @t677 @t672 @t673 @t671 (@var "A__questionmark_vu491_424" tptp.c_unsorted)) (exists (@list @t675 @t676) (and (= @t675 (tptp.c_sort (tptp.memory @t678 tptp.bitvector) @t679)) (= @t676 (tptp.pointer @t678)) (exists (@list @t674) (and (= @t674 (tptp.c_sort @t676 @t677)) (= (tptp.c_sort tptp.bitvector (tptp.select_bytes @t675 (tptp.c_sort @t676 (tptp.shift @t674 @t672)) @t673 @t671)) (tptp.c_sort tptp.bitvector (tptp.select_bytes @t675 @t674 (+ @t673 @t672) @t671))))))))) % 0.43/0.82 (assume @p129 (forall (@list @t692 @t693 @t691 @t684 @t683 @t688 @t682 @t690 @t689) (exists (@list @t687) (and (= @t687 (tptp.memory @t692 tptp.bitvector)) (exists (@list @t686 @t685 @t681 @t680) (and (= @t686 (tptp.c_sort @t687 @t693)) (= @t685 (tptp.c_sort (tptp.pointer @t692) @t691)) (= @t681 (tptp.c_sort tptp.bitvector @t690)) (= @t680 (tptp.c_sort tptp.bitvector @t689)) (=> (= (+ @t684 @t683) @t688) (= (tptp.c_sort @t687 (tptp.store_bytes (tptp.c_sort @t687 (tptp.store_bytes @t686 @t685 @t684 @t683 @t681)) @t685 @t688 @t682 @t680)) (tptp.c_sort @t687 (tptp.store_bytes @t686 @t685 @t684 (+ @t683 @t682) (tptp.c_sort tptp.bitvector (tptp.concat_bitvector @t681 @t680)))))))))))) % 0.43/0.82 (assume @p130 (forall (@list @t706 @t707 @t705 @t702 @t697 @t698 @t696 @t704 @t703) (exists (@list @t701) (and (= @t701 (tptp.memory @t706 tptp.bitvector)) (exists (@list @t700 @t699 @t694 @t695) (and (= @t700 (tptp.c_sort @t701 @t707)) (= @t699 (tptp.c_sort (tptp.pointer @t706) @t705)) (= @t694 (tptp.c_sort tptp.bitvector @t704)) (= @t695 (tptp.c_sort tptp.bitvector @t703)) (=> (= (+ @t698 @t696) @t702) (= (tptp.c_sort @t701 (tptp.store_bytes (tptp.c_sort @t701 (tptp.store_bytes @t700 @t699 @t702 @t697 @t694)) @t699 @t698 @t696 @t695)) (tptp.c_sort @t701 (tptp.store_bytes @t700 @t699 @t698 (+ @t697 @t696) (tptp.c_sort tptp.bitvector (tptp.concat_bitvector @t695 @t694)))))))))))) % 0.43/0.82 (assume @p131 (forall (@list @t715 @t716 @t714 @t710 @t709 @t713 @t708) (exists (@list @t712 @t711) (and (= @t712 (tptp.c_sort (tptp.memory @t715 tptp.bitvector) @t716)) (= @t711 (tptp.c_sort (tptp.pointer @t715) @t714)) (=> (= (+ @t710 @t709) @t713) (= (tptp.c_sort tptp.bitvector (tptp.concat_bitvector (tptp.c_sort tptp.bitvector (tptp.select_bytes @t712 @t711 @t710 @t709)) (tptp.c_sort tptp.bitvector (tptp.select_bytes @t712 @t711 @t713 @t708)))) (tptp.c_sort tptp.bitvector (tptp.select_bytes @t712 @t711 @t710 (+ @t709 @t708))))))))) % 0.43/0.82 (assume @p132 (forall (@list @t719) (exists (@list @t717) (and (= @t717 (tptp.c_sort tptp.bitvector @t719)) (= (tptp.c_sort tptp.bitvector (tptp.bitvector_of_char_P (tptp.c_sort @t718 (tptp.char_P_of_bitvector @t717)))) @t717))))) % 0.43/0.82 (assume @p133 (forall (@list @t721) (exists (@list @t720) (and (= @t720 (tptp.c_sort tptp.bitvector @t721)) (= (tptp.c_sort tptp.bitvector (tptp.bitvector_of_int32 (tptp.c_sort tptp.int32 (tptp.int32_of_bitvector @t720)))) @t720))))) % 0.43/0.82 (assume @p134 (forall (@list @t723) (exists (@list @t722) (and (= @t722 (tptp.c_sort tptp.bitvector @t723)) (= (tptp.c_sort tptp.bitvector (tptp.bitvector_of_int8 (tptp.c_sort tptp.int8 (tptp.int8_of_bitvector @t722)))) @t722))))) % 0.43/0.82 (assume @p135 (forall (@list @t726) (exists (@list @t724) (and (= @t724 (tptp.c_sort tptp.bitvector @t726)) (= (tptp.c_sort tptp.bitvector (tptp.bitvector_of_void_P (tptp.c_sort @t725 (tptp.void_P_of_bitvector @t724)))) @t724))))) % 0.43/0.82 (assume @p136 (= (tptp.int_of_tag @t728) 1)) % 0.43/0.82 (assume @p137 (forall (@list @t731) (exists (@list @t730) (and (= @t730 @t718) (exists (@list @t729) (and (= @t729 (tptp.c_sort @t730 @t731)) (= (tptp.c_sort @t730 (tptp.char_P_of_bitvector (tptp.c_sort tptp.bitvector (tptp.bitvector_of_char_P @t729)))) @t729))))))) % 0.43/0.82 (assume @p138 (forall (@list @t735) (exists (@list @t734) (and (= @t734 @t718) (exists (@list @t732) (and (= @t732 (tptp.c_sort @t734 @t735)) (= @t732 (tptp.c_sort @t734 (tptp.char_P_of_pointer_address (tptp.c_sort @t733 (tptp.pointer_address @t732))))))))))) % 0.43/0.82 (assume @p139 (exists (@list @t736) (and (= @t736 @t727) (tptp.parenttag (tptp.c_sort @t736 tptp.char_P_tag) (tptp.c_sort @t736 tptp.bottom_tag))))) % 0.43/0.82 (assume @p140 (forall (@list @t737 @t738) (tptp.instanceof (tptp.c_sort (tptp.tag_table tptp.char_P) @t738) (tptp.c_sort @t718 @t737) @t728))) % 0.43/0.82 (assume @p141 (forall (@list @t742 @t741) (exists (@list @t740 @t739) (and (= @t740 (tptp.c_sort tptp.int32 @t742)) (= @t739 (tptp.c_sort tptp.int32 @t741)) (= (tptp.eq_int32 @t740 @t739) (= (tptp.integer_of_int32 @t740) (tptp.integer_of_int32 @t739))))))) % 0.43/0.82 (assume @p142 (forall (@list @t746 @t745) (exists (@list @t744 @t743) (and (= @t744 (tptp.c_sort tptp.int8 @t746)) (= @t743 (tptp.c_sort tptp.int8 @t745)) (= (tptp.eq_int8 @t744 @t743) (= (tptp.integer_of_int8 @t744) (tptp.integer_of_int8 @t743))))))) % 0.43/0.82 (assume @p143 (forall (@list @t747) (=> (and (<= @t748 @t747) (<= @t747 2147483647)) (= (tptp.integer_of_int32 (tptp.c_sort tptp.int32 (tptp.int32_of_integer @t747))) @t747)))) % 0.43/0.82 (assume @p144 (forall (@list @t750) (exists (@list @t749) (and (= @t749 (tptp.c_sort tptp.int32 @t750)) (tptp.eq_int32 (tptp.c_sort tptp.int32 (tptp.int32_of_bitvector (tptp.c_sort tptp.bitvector (tptp.bitvector_of_int32 @t749)))) @t749))))) % 0.43/0.82 (assume @p145 (forall (@list @t752) (exists (@list @t751) (and (= @t751 (tptp.integer_of_int32 (tptp.c_sort tptp.int32 @t752))) (<= @t748 @t751) (<= @t751 2147483647))))) % 0.43/0.82 (assume @p146 (forall (@list @t753) (=> (and (<= @t754 @t753) (<= @t753 127)) (= (tptp.integer_of_int8 (tptp.c_sort tptp.int8 (tptp.int8_of_integer @t753))) @t753)))) % 0.43/0.82 (assume @p147 (forall (@list @t756) (exists (@list @t755) (and (= @t755 (tptp.c_sort tptp.int8 @t756)) (tptp.eq_int8 (tptp.c_sort tptp.int8 (tptp.int8_of_bitvector (tptp.c_sort tptp.bitvector (tptp.bitvector_of_int8 @t755)))) @t755))))) % 0.43/0.82 (assume @p148 (forall (@list @t758) (exists (@list @t757) (and (= @t757 (tptp.integer_of_int8 (tptp.c_sort tptp.int8 @t758))) (<= @t754 @t757) (<= @t757 127))))) % 0.43/0.82 (assume @p149 (forall (@list @t764 @t759 @t762) (exists (@list @t760 @t761) (and (= @t760 (tptp.c_sort @t718 @t764)) (= @t761 (tptp.c_sort @t763 @t762)) (= (tptp.left_valid_struct_char_P @t760 @t759 @t761) (<= (tptp.offset_min @t761 @t760) @t759)))))) % 0.43/0.82 (assume @p150 (forall (@list @t770 @t765 @t768) (exists (@list @t766 @t767) (and (= @t766 (tptp.c_sort @t725 @t770)) (= @t767 (tptp.c_sort @t769 @t768)) (= (tptp.left_valid_struct_void_P @t766 @t765 @t767) (<= (tptp.offset_min @t767 @t766) @t765)))))) % 0.43/0.82 (assume @p151 (forall (@list @t773) (exists (@list @t772) (and (= @t772 @t733) (exists (@list @t771) (and (= @t771 (tptp.c_sort @t772 @t773)) (= @t771 (tptp.c_sort @t772 (tptp.pointer_address (tptp.c_sort @t718 (tptp.char_P_of_pointer_address @t771))))))))))) % 0.43/0.82 (assume @p152 (forall (@list @t776) (exists (@list @t775) (and (= @t775 @t733) (exists (@list @t774) (and (= @t774 (tptp.c_sort @t775 @t776)) (= @t774 (tptp.c_sort @t775 (tptp.pointer_address (tptp.c_sort @t725 (tptp.void_P_of_pointer_address @t774))))))))))) % 0.43/0.82 (assume @p153 (forall (@list @t781 @t777 @t780) (exists (@list @t778 @t779) (and (= @t778 (tptp.c_sort @t718 @t781)) (= @t779 (tptp.c_sort @t763 @t780)) (= (tptp.right_valid_struct_char_P @t778 @t777 @t779) (>= (tptp.offset_max @t779 @t778) @t777)))))) % 0.43/0.82 (assume @p154 (forall (@list @t786 @t782 @t785) (exists (@list @t783 @t784) (and (= @t783 (tptp.c_sort @t725 @t786)) (= @t784 (tptp.c_sort @t769 @t785)) (= (tptp.right_valid_struct_void_P @t783 @t782 @t784) (>= (tptp.offset_max @t784 @t783) @t782)))))) % 0.43/0.82 (assume @p155 (forall (@list @t792 @t790 @t787 @t791) (exists (@list @t788 @t789) (and (= @t788 (tptp.c_sort @t718 @t792)) (= @t789 (tptp.c_sort @t763 @t791)) (= (tptp.strict_valid_root_char_P @t788 @t790 @t787 @t789) (and (= (tptp.offset_min @t789 @t788) @t790) (= (tptp.offset_max @t789 @t788) @t787))))))) % 0.43/0.82 (assume @p156 (forall (@list @t798 @t796 @t793 @t797) (exists (@list @t794 @t795) (and (= @t794 (tptp.c_sort @t725 @t798)) (= @t795 (tptp.c_sort @t769 @t797)) (= (tptp.strict_valid_root_void_P @t794 @t796 @t793 @t795) (and (= (tptp.offset_min @t795 @t794) @t796) (= (tptp.offset_max @t795 @t794) @t793))))))) % 0.43/0.82 (assume @p157 (forall (@list @t804 @t802 @t799 @t803) (exists (@list @t800 @t801) (and (= @t800 (tptp.c_sort @t718 @t804)) (= @t801 (tptp.c_sort @t763 @t803)) (= (tptp.strict_valid_struct_char_P @t800 @t802 @t799 @t801) (and (= (tptp.offset_min @t801 @t800) @t802) (= (tptp.offset_max @t801 @t800) @t799))))))) % 0.43/0.82 (assume @p158 (forall (@list @t810 @t808 @t805 @t809) (exists (@list @t806 @t807) (and (= @t806 (tptp.c_sort @t725 @t810)) (= @t807 (tptp.c_sort @t769 @t809)) (= (tptp.strict_valid_struct_void_P @t806 @t808 @t805 @t807) (and (= (tptp.offset_min @t807 @t806) @t808) (= (tptp.offset_max @t807 @t806) @t805))))))) % 0.43/0.82 (assume @p159 (forall (@list @t817 @t814 @t811 @t815) (exists (@list @t812 @t813) (and (= @t812 (tptp.c_sort @t733 @t817)) (= @t813 (tptp.c_sort @t816 @t815)) (= (tptp.valid_bitvector_struct_char_P @t812 @t814 @t811 @t813) (and (= (tptp.offset_min @t813 @t812) @t814) (= (tptp.offset_max @t813 @t812) @t811))))))) % 0.43/0.82 (assume @p160 (forall (@list @t823 @t821 @t818 @t822) (exists (@list @t819 @t820) (and (= @t819 (tptp.c_sort @t733 @t823)) (= @t820 (tptp.c_sort @t816 @t822)) (= (tptp.valid_bitvector_struct_void_P @t819 @t821 @t818 @t820) (and (= (tptp.offset_min @t820 @t819) @t821) (= (tptp.offset_max @t820 @t819) @t818))))))) % 0.43/0.82 (assume @p161 (forall (@list @t829 @t827 @t824 @t828) (exists (@list @t825 @t826) (and (= @t825 (tptp.c_sort @t718 @t829)) (= @t826 (tptp.c_sort @t763 @t828)) (= (tptp.valid_root_char_P @t825 @t827 @t824 @t826) (and (<= (tptp.offset_min @t826 @t825) @t827) (>= (tptp.offset_max @t826 @t825) @t824))))))) % 0.43/0.82 (assume @p162 (forall (@list @t835 @t833 @t830 @t834) (exists (@list @t831 @t832) (and (= @t831 (tptp.c_sort @t725 @t835)) (= @t832 (tptp.c_sort @t769 @t834)) (= (tptp.valid_root_void_P @t831 @t833 @t830 @t832) (and (<= (tptp.offset_min @t832 @t831) @t833) (>= (tptp.offset_max @t832 @t831) @t830))))))) % 0.43/0.82 (assume @p163 (forall (@list @t841 @t839 @t836 @t840) (exists (@list @t837 @t838) (and (= @t837 (tptp.c_sort @t718 @t841)) (= @t838 (tptp.c_sort @t763 @t840)) (= (tptp.valid_struct_char_P @t837 @t839 @t836 @t838) (and (<= (tptp.offset_min @t838 @t837) @t839) (>= (tptp.offset_max @t838 @t837) @t836))))))) % 0.43/0.82 (assume @p164 (forall (@list @t847 @t845 @t842 @t846) (exists (@list @t843 @t844) (and (= @t843 (tptp.c_sort @t725 @t847)) (= @t844 (tptp.c_sort @t769 @t846)) (= (tptp.valid_struct_void_P @t843 @t845 @t842 @t844) (and (<= (tptp.offset_min @t844 @t843) @t845) (>= (tptp.offset_max @t844 @t843) @t842))))))) % 0.43/0.82 (assume @p165 (= (tptp.int_of_tag @t849) 1)) % 0.43/0.82 (assume @p166 (forall (@list @t852) (exists (@list @t851) (and (= @t851 @t725) (exists (@list @t850) (and (= @t850 (tptp.c_sort @t851 @t852)) (= (tptp.c_sort @t851 (tptp.void_P_of_bitvector (tptp.c_sort tptp.bitvector (tptp.bitvector_of_void_P @t850)))) @t850))))))) % 0.43/0.82 (assume @p167 (forall (@list @t855) (exists (@list @t854) (and (= @t854 @t725) (exists (@list @t853) (and (= @t853 (tptp.c_sort @t854 @t855)) (= @t853 (tptp.c_sort @t854 (tptp.void_P_of_pointer_address (tptp.c_sort @t733 (tptp.pointer_address @t853))))))))))) % 0.43/0.82 (assume @p168 (exists (@list @t856) (and (= @t856 @t848) (tptp.parenttag (tptp.c_sort @t856 tptp.void_P_tag) (tptp.c_sort @t856 tptp.bottom_tag))))) % 0.43/0.82 (assume @p169 (forall (@list @t857 @t858) (tptp.instanceof (tptp.c_sort (tptp.tag_table tptp.void_P) @t858) (tptp.c_sort @t725 @t857) @t849))) % 0.43/0.82 (assume @p170 @t882) % 0.43/0.82 (step @p171 :rule bool-impl-true2 :args (@t893)) % 0.43/0.82 (step @p172 :rule aci_norm :args ((= @t895 @t891))) % 0.43/0.82 (step @p173 :rule cong :premises (@p172) :args (@t896)) % 0.43/0.82 (step @p174 :rule quant-merge-prenex :args ((= (forall @t879 @t898) @t896))) % 0.43/0.82 (step @p175 :rule alpha_equiv :args (@t899 (@list @t886 @t883) (@list @t861 @t900))) % 0.43/0.82 (step @p176 :rule refl :args (@t890)) % 0.43/0.82 (step @p177 :rule nary_cong :premises (@p176 @p175) :args (@t901)) % 0.43/0.82 (step @p178 :rule quant-miniscope-or :args ((= @t898 @t901))) % 0.43/0.82 (step @p179 :rule trans :premises (@p178 @p177)) % 0.43/0.82 (step @p180 :rule symm :premises (@p179)) % 0.43/0.82 (step @p181 :rule cong :premises (@p180) :args ((forall @t879 (or @t890 @t909)))) % 0.43/0.82 (step @p182 :rule trans :premises (@p181 @p174)) % 0.43/0.82 (step @p183 :rule trans :premises (@p182 @p173)) % 0.43/0.82 (step @p184 :rule bool-impl-elim :args (@t877 @t909)) % 0.43/0.82 (step @p185 :rule cong :premises (@p184) :args ((forall @t879 (=> @t877 @t909)))) % 0.43/0.82 (step @p186 :rule trans :premises (@p185 @p183)) % 0.43/0.82 (step @p187 :rule aci_norm :args ((= @t911 @t907))) % 0.43/0.82 (step @p188 :rule cong :premises (@p187) :args (@t912)) % 0.43/0.82 (step @p189 :rule quant-merge-prenex :args ((= (forall @t875 @t914) @t912))) % 0.43/0.82 (step @p190 :rule alpha_equiv :args (@t915 (@list @t900) (@list @t864))) % 0.43/0.82 (step @p191 :rule refl :args (@t906)) % 0.43/0.82 (step @p192 :rule nary_cong :premises (@p191 @p190) :args (@t916)) % 0.43/0.82 (step @p193 :rule quant-miniscope-or :args ((= @t914 @t916))) % 0.43/0.82 (step @p194 :rule trans :premises (@p193 @p192)) % 0.43/0.82 (step @p195 :rule symm :premises (@p194)) % 0.43/0.82 (step @p196 :rule cong :premises (@p195) :args ((forall @t875 (or @t906 @t920)))) % 0.43/0.82 (step @p197 :rule trans :premises (@p196 @p189)) % 0.43/0.82 (step @p198 :rule trans :premises (@p197 @p188)) % 0.43/0.82 (step @p199 :rule bool-impl-elim :args (@t905 @t920)) % 0.43/0.82 (step @p200 :rule cong :premises (@p199) :args ((forall @t875 (=> @t905 @t920)))) % 0.43/0.82 (step @p201 :rule trans :premises (@p200 @p198)) % 0.43/0.82 (step @p202 :rule bool-double-not-elim :args (@t917)) % 0.43/0.82 (step @p203 :rule refl :args (@t919)) % 0.43/0.82 (step @p204 :rule nary_cong :premises (@p203 @p202) :args ((or @t919 (not @t921)))) % 0.43/0.82 (step @p205 :rule bool-and-de-morgan :args (@t918 @t921 true)) % 0.43/0.82 (step @p206 :rule trans :premises (@p205 @p204)) % 0.43/0.82 (step @p207 :rule cong :premises (@p206) :args ((forall @t870 (not @t922)))) % 0.43/0.82 (step @p208 :rule aci_norm :args ((= (or false @t922) @t922))) % 0.43/0.82 (step @p209 :rule refl :args (@t922)) % 0.43/0.82 (step @p210 :rule evaluate :args ((not true))) % 0.43/0.82 (step @p211 :rule eq-refl :args (@t865)) % 0.43/0.82 (step @p212 :rule cong :premises (@p211) :args (@t923)) % 0.43/0.82 (step @p213 :rule trans :premises (@p212 @p210)) % 0.43/0.82 (step @p214 :rule nary_cong :premises (@p213 @p209) :args (@t924)) % 0.43/0.82 (step @p215 :rule trans :premises (@p214 @p208)) % 0.43/0.82 (step @p216 :rule quant-var-elim-eq :args ((= (forall @t868 @t928) @t924))) % 0.43/0.82 (step @p217 :rule aci_norm :args ((= @t929 @t928))) % 0.43/0.82 (step @p218 :rule cong :premises (@p217) :args ((forall @t868 @t929))) % 0.43/0.82 (step @p219 :rule trans :premises (@p218 @p216)) % 0.43/0.82 (step @p220 :rule trans :premises (@p219 @p215)) % 0.43/0.82 (step @p221 :rule bool-implies-de-morgan :args (@t925 @t860)) % 0.43/0.82 (step @p222 :rule refl :args (@t927)) % 0.43/0.82 (step @p223 :rule nary_cong :premises (@p222 @p221) :args ((or @t927 (not @t930)))) % 0.43/0.82 (step @p224 :rule bool-and-de-morgan :args (@t866 @t930 true)) % 0.43/0.82 (step @p225 :rule trans :premises (@p224 @p223)) % 0.43/0.82 (step @p226 :rule cong :premises (@p225) :args (@t932)) % 0.43/0.82 (step @p227 :rule trans :premises (@p226 @p220)) % 0.43/0.82 (step @p228 :rule cong :premises (@p227) :args (@t933)) % 0.43/0.82 (step @p229 :rule exists-elim :args ((= (exists @t868 @t931) @t933))) % 0.43/0.82 (step @p230 :rule trans :premises (@p229 @p228)) % 0.43/0.82 (step @p231 :rule refl :args (@t860)) % 0.43/0.82 (step @p232 :rule eq-symm :args (@t859 @t862)) % 0.43/0.82 (step @p233 :rule cong :premises (@p232 @p231) :args (@t863)) % 0.43/0.82 (step @p234 :rule refl :args (@t866)) % 0.43/0.82 (step @p235 :rule nary_cong :premises (@p234 @p233) :args (@t867)) % 0.43/0.82 (step @p236 :rule cong :premises (@p235) :args (@t869)) % 0.43/0.82 (step @p237 :rule trans :premises (@p236 @p230)) % 0.43/0.82 (step @p238 :rule cong :premises (@p237) :args (@t871)) % 0.43/0.82 (step @p239 :rule trans :premises (@p238 @p207)) % 0.43/0.82 (step @p240 :rule eq-symm :args (@t862 @t873)) % 0.43/0.82 (step @p241 :rule cong :premises (@p240 @p239) :args (@t874)) % 0.43/0.82 (step @p242 :rule cong :premises (@p241) :args (@t876)) % 0.43/0.82 (step @p243 :rule trans :premises (@p242 @p201)) % 0.43/0.82 (step @p244 :rule refl :args (@t877)) % 0.43/0.82 (step @p245 :rule cong :premises (@p244 @p243) :args (@t878)) % 0.43/0.82 (step @p246 :rule cong :premises (@p245) :args (@t880)) % 0.43/0.82 (step @p247 :rule trans :premises (@p246 @p186)) % 0.43/0.82 (step @p248 :rule eq-refl :args (tptp.c_Boolean_true)) % 0.43/0.82 (step @p249 :rule cong :premises (@p248 @p247) :args (@t881)) % 0.43/0.82 (step @p250 :rule trans :premises (@p249 @p171)) % 0.43/0.82 (step @p251 :rule cong :premises (@p250) :args (@t882)) % 0.43/0.82 (step @p252 :rule eq_resolve :premises (@p170 @p251)) % 0.43/0.82 (step @p253 :rule skolemize :premises (@p252)) % 0.43/0.82 (step @p254 :rule bool-double-not-elim :args (@t936)) % 0.43/0.82 (step @p255 :rule refl :args (@t946)) % 0.43/0.82 (step @p256 :rule nary_cong :premises (@p255 @p254) :args ((or @t946 (not @t945)))) % 0.43/0.82 (step @p257 :rule cnf_or_neg :args (@t946 0)) % 0.43/0.82 (step @p258 :rule eq_resolve :premises (@p257 @p256)) % 0.43/0.82 (step @p259 :rule reordering :premises (@p258) :args ((or @t936 @t946))) % 0.43/0.82 (step @p260 :rule chain_m_resolution :premises (@p259 @p253) :args (@t936 @t947 @t948)) % 0.43/0.82 (step @p261 :rule bool-double-not-elim :args (@t943)) % 0.43/0.82 (step @p262 :rule nary_cong :premises (@p255 @p261) :args ((or @t946 (not @t944)))) % 0.43/0.82 (step @p263 :rule cnf_or_neg :args (@t946 1)) % 0.43/0.82 (step @p264 :rule eq_resolve :premises (@p263 @p262)) % 0.43/0.82 (step @p265 :rule reordering :premises (@p264) :args ((or @t943 @t946))) % 0.43/0.82 (step @p266 :rule chain_m_resolution :premises (@p265 @p253) :args (@t943 @t947 @t948)) % 0.43/0.82 (step @p267 :rule bool-double-not-elim :args (@t941)) % 0.43/0.82 (step @p268 :rule nary_cong :premises (@p255 @p267) :args ((or @t946 (not @t942)))) % 0.43/0.82 (step @p269 :rule cnf_or_neg :args (@t946 2)) % 0.43/0.82 (step @p270 :rule eq_resolve :premises (@p269 @p268)) % 0.43/0.82 (step @p271 :rule reordering :premises (@p270) :args ((or @t941 @t946))) % 0.43/0.82 (step @p272 :rule chain_m_resolution :premises (@p271 @p253) :args (@t941 @t947 @t948)) % 0.43/0.82 (step @p273 :rule cnf_or_neg :args (@t946 3)) % 0.43/0.82 (step @p274 :rule chain_m_resolution :premises (@p273 @p253) :args (@t949 @t947 @t948)) % 0.43/0.82 (step @p275 :rule bool-double-not-elim :args (@t939)) % 0.43/0.82 (step @p276 :rule refl :args (@t942)) % 0.43/0.82 (step @p277 :rule refl :args (@t944)) % 0.43/0.82 (step @p278 :rule refl :args (@t945)) % 0.43/0.82 (step @p279 :rule nary_cong :premises (@p278 @p277 @p276 @p275) :args ((or @t945 @t944 @t942 (not @t949)))) % 0.43/0.82 (assume-push @p322 @t950) % 0.43/0.82 (assume-push @p323 @t949) % 0.43/0.82 (step @p282 :rule evaluate :args ((= false true))) % 0.43/0.82 (step @p283 :rule symm :premises (@p322)) % 0.43/0.82 (step @p284 :rule true_intro :premises (@p283)) % 0.43/0.82 (step @p285 :rule false_intro :premises (@p274)) % 0.43/0.82 (step @p286 :rule symm :premises (@p285)) % 0.43/0.82 (step @p287 :rule trans :premises (@p286 @p284)) % 0.43/0.82 (step @p288 false :rule eq_resolve :premises (@p287 @p282)) % 0.43/0.82 (step-pop @p324 :rule scope :premises (@p288)) % 0.43/0.82 (step-pop @p325 :rule scope :premises (@p324)) % 0.43/0.82 (step @p289 :rule process_scope :premises (@p325) :args (false)) % 0.43/0.82 (assume-push @p326 @t936) % 0.43/0.82 (assume-push @p327 @t943) % 0.43/0.82 (assume-push @p328 @t941) % 0.43/0.82 (assume-push @p329 @t949) % 0.43/0.82 (assume-push @p330 @t941) % 0.43/0.82 (assume-push @p331 @t943) % 0.43/0.82 (assume-push @p332 (= 18 @t935)) % 0.43/0.82 (step @p299 :rule trans :premises (@p266 @p272)) % 0.43/0.82 (step @p300 :rule cong :premises (@p299) :args (@t935)) % 0.43/0.82 (step @p301 :rule chain_m_resolution :premises (@p259 @p253) :args (@t936 @t947 @t948)) % 0.43/0.82 (step @p302 :rule symm :premises (@p301)) % 0.43/0.82 (step @p303 :rule trans :premises (@p302 @p300)) % 0.43/0.82 (step-pop @p333 :rule scope :premises (@p303)) % 0.43/0.82 (step-pop @p334 :rule scope :premises (@p333)) % 0.43/0.82 (step-pop @p335 :rule scope :premises (@p334)) % 0.43/0.82 (step @p304 :rule process_scope :premises (@p335) :args (@t950)) % 0.43/0.82 (step @p308 :rule symm :premises (@p260)) % 0.43/0.82 (step @p309 :rule and_intro :premises (@p272 @p266 @p308)) % 0.43/0.82 (step @p310 :rule modus_ponens :premises (@p309 @p304)) % 0.43/0.82 (step @p311 :rule and_intro :premises (@p310 @p274)) % 0.43/0.82 (step-pop @p336 :rule scope :premises (@p311)) % 0.43/0.82 (step-pop @p337 :rule scope :premises (@p336)) % 0.43/0.82 (step-pop @p338 :rule scope :premises (@p337)) % 0.43/0.82 (step-pop @p339 :rule scope :premises (@p338)) % 0.43/0.82 (step @p312 :rule process_scope :premises (@p339) :args (@t951)) % 0.43/0.82 (step @p317 :rule implies_elim :premises (@p312)) % 0.43/0.82 (step @p318 :rule resolution :premises (@p317 @p289) :args (true @t951)) % 0.43/0.82 (step @p319 :rule not_and :premises (@p318)) % 0.43/0.82 (step @p320 :rule eq_resolve :premises (@p319 @p279)) % 0.43/0.82 (step @p321 false :rule chain_m_resolution :premises (@p320 @p274 @p272 @p266 @p260) :args (false (@list true false false false) (@list @t939 @t941 @t943 @t936))) % 0.43/0.82 ) % 0.43/0.82 % SZS output end Proof % 0.43/0.82 % cvc5 exiting %------------------------------------------------------------------------------