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