%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SWV966-1 : TPTP v9.2.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n022.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 09:02:41 AM UTC 2026 % Result : Unsatisfiable 16.51s 16.70s % Output : Proof 16.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWV966-1 : TPTP v9.2.1. Released v4.1.0. % 0.13/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.16/0.34 % Computer : n022.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Jun 2 21:27:08 EDT 2026 % 0.16/0.35 % CPUTime : % 0.38/0.57 %----Proving TF0_NAR, FOF, or CNF % 0.38/0.58 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 15.41/15.68 --- Run --no-e-matching --full-saturate-quant at 6... % 16.51/16.70 % SZS status Unsatisfiable % 16.51/16.70 % SZS output start Proof % 16.51/16.72 ( % 16.51/16.72 (declare-sort $$unsorted 0) % 16.51/16.72 (declare-const tptp.v_M____ $$unsorted) % 16.51/16.72 (declare-const tptp.c_Expr_Oexp_Oexp__case (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.tc_Type_Oty $$unsorted) % 16.51/16.72 (declare-const tptp.t_a $$unsorted) % 16.51/16.72 (declare-const tptp.c_DefAss_O_092_060D_062 (-> $$unsorted $$unsorted $$unsorted Bool)) % 16.51/16.72 (declare-const tptp.hAPP (-> $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_Map_Omap__le (-> $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 16.51/16.72 (declare-const tptp.tc_nat $$unsorted) % 16.51/16.72 (declare-const tptp.hBOOL (-> $$unsorted Bool)) % 16.51/16.72 (declare-const tptp.c_Expr_Oexp_OCast (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_TypeRel_Owiden (-> $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.tc_Expr_Oexp (-> $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_Expr_Oexp_OCond (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.tc_List_Olist (-> $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_Expr_Oexp_OBlock (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_Expr_Oexp_OLAss (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.v_esa____ $$unsorted) % 16.51/16.72 (declare-const tptp.tc_String_Ochar $$unsorted) % 16.51/16.72 (declare-const tptp.c_TypeSafe__Mirabelle_Osconf (-> $$unsorted $$unsorted $$unsorted Bool)) % 16.51/16.72 (declare-const tptp.c_SmallStep_Oredp (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 16.51/16.72 (declare-const tptp.c_WellTypeRT_OWTrts (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 16.51/16.72 (declare-const tptp.tc_prod (-> $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_Expr_Oexp_OFAss (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_COMBI (-> $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_Progress_OWTrt_H (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 16.51/16.72 (declare-const tptp.v_ea____ $$unsorted) % 16.51/16.72 (declare-const tptp.v_la____ $$unsorted) % 16.51/16.72 (declare-const tptp.c_Expr_Oexp_OTryCatch (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.v_ha____ $$unsorted) % 16.51/16.72 (declare-const tptp.v_sko__local__XCallObj__2__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_Expr_Oexp_Othrow (-> $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_Expr_Oexp_OVar (-> $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_WellType_OWT (-> $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 16.51/16.72 (declare-const tptp.c_Expr_Oexp_OWhile (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_Expr_Oexp_OFAcc (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_List_Olist__all2 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 16.51/16.72 (declare-const tptp.c_Expr_Oexp_OVal (-> $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_Expr_Oexp_Onew (-> $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_Expr_Oexp_OBinOp (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.v_sko__local__XIH__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_Type_Oty_ONT $$unsorted) % 16.51/16.72 (declare-const tptp.c_fequal (-> $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_Type_Oty_OBoolean $$unsorted) % 16.51/16.72 (declare-const tptp.c_Objects_Ohext (-> $$unsorted $$unsorted Bool)) % 16.51/16.72 (declare-const tptp.c_Expr_Oexp_OSeq (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_WellTypeRT_OWTrt (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 16.51/16.72 (declare-const tptp.c_Conform_Oconf (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 16.51/16.72 (declare-const tptp.c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__5__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.tc_Value_Oval $$unsorted) % 16.51/16.72 (declare-const tptp.tc_Option_Ooption (-> $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_Expr_Oexp_OCall (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.tc_fun (-> $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.c_Pair (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.v_E____ $$unsorted) % 16.51/16.72 (declare-const tptp.v_h_Ha____ $$unsorted) % 16.51/16.72 (declare-const tptp.v_P $$unsorted) % 16.51/16.72 (declare-const tptp.v_e_Ha____ $$unsorted) % 16.51/16.72 (declare-const tptp.v_sko__local__XCallObj__Xhyps__2__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 16.51/16.72 (declare-const tptp.v_Ts____ $$unsorted) % 16.51/16.72 (declare-const tptp.v_T____ $$unsorted) % 16.51/16.72 (define @t1 () (@var "T_a" $$unsorted)) % 16.51/16.72 (define @t2 () (@var "V_exp" $$unsorted)) % 16.51/16.72 (define @t3 () (@var "V_list" $$unsorted)) % 16.51/16.72 (define @t4 () (tptp.c_Expr_Oexp_OCast @t3 @t2 @t1)) % 16.51/16.72 (define @t5 () (@var "V_exp3_H" $$unsorted)) % 16.51/16.72 (define @t6 () (@var "V_exp2_H" $$unsorted)) % 16.51/16.72 (define @t7 () (@var "V_exp1_H" $$unsorted)) % 16.51/16.72 (define @t8 () (tptp.c_Expr_Oexp_OCond @t7 @t6 @t5 @t1)) % 16.51/16.72 (define @t9 () (@var "V_list2_H" $$unsorted)) % 16.51/16.72 (define @t10 () (@var "V_list1_H" $$unsorted)) % 16.51/16.72 (define @t11 () (tptp.c_Expr_Oexp_OFAss @t7 @t10 @t9 @t6 @t1)) % 16.51/16.72 (define @t12 () (@var "V_a_H" $$unsorted)) % 16.51/16.72 (define @t13 () (@var "V_list_H" $$unsorted)) % 16.51/16.72 (define @t14 () (tptp.c_Expr_Oexp_OTryCatch @t7 @t13 @t12 @t6 @t1)) % 16.51/16.72 (define @t15 () (@var "V_exp3" $$unsorted)) % 16.51/16.72 (define @t16 () (@var "V_exp2" $$unsorted)) % 16.51/16.72 (define @t17 () (@var "V_exp1" $$unsorted)) % 16.51/16.72 (define @t18 () (tptp.c_Expr_Oexp_OCond @t17 @t16 @t15 @t1)) % 16.51/16.72 (define @t19 () (tptp.c_Expr_Oexp_OWhile @t7 @t6 @t1)) % 16.51/16.72 (define @t20 () (@var "V_a" $$unsorted)) % 16.51/16.72 (define @t21 () (tptp.c_Expr_Oexp_OLAss @t20 @t2 @t1)) % 16.51/16.72 (define @t22 () (@var "V_exp_H" $$unsorted)) % 16.51/16.72 (define @t23 () (tptp.c_Expr_Oexp_OFAcc @t22 @t10 @t9 @t1)) % 16.51/16.72 (define @t24 () (@list @t22 @t10 @t9 @t1 @t20 @t2)) % 16.51/16.72 (define @t25 () (tptp.c_Expr_Oexp_OSeq @t17 @t16 @t1)) % 16.51/16.72 (define @t26 () (= @t2 @t22)) % 16.51/16.72 (define @t27 () (tptp.c_Expr_Oexp_Othrow @t22 @t1)) % 16.51/16.72 (define @t28 () (tptp.c_Expr_Oexp_Othrow @t2 @t1)) % 16.51/16.72 (define @t29 () (@var "V_list2" $$unsorted)) % 16.51/16.72 (define @t30 () (@var "V_list1" $$unsorted)) % 16.51/16.72 (define @t31 () (tptp.c_Expr_Oexp_OFAss @t17 @t30 @t29 @t16 @t1)) % 16.51/16.72 (define @t32 () (@var "V_val" $$unsorted)) % 16.51/16.72 (define @t33 () (tptp.c_Expr_Oexp_OVal @t32 @t1)) % 16.51/16.72 (define @t34 () (@var "V_bop_H" $$unsorted)) % 16.51/16.72 (define @t35 () (tptp.c_Expr_Oexp_OBinOp @t7 @t34 @t6 @t1)) % 16.51/16.72 (define @t36 () (tptp.c_Expr_Oexp_OVar @t12 @t1)) % 16.51/16.72 (define @t37 () (@var "V_bop" $$unsorted)) % 16.51/16.72 (define @t38 () (tptp.c_Expr_Oexp_OBinOp @t17 @t37 @t16 @t1)) % 16.51/16.72 (define @t39 () (tptp.c_Expr_Oexp_Onew @t3 @t1)) % 16.51/16.72 (define @t40 () (tptp.c_Expr_Oexp_OCast @t13 @t22 @t1)) % 16.51/16.72 (define @t41 () (tptp.c_Expr_Oexp_OWhile @t17 @t16 @t1)) % 16.51/16.72 (define @t42 () (@list @t7 @t13 @t12 @t6 @t1 @t17 @t16)) % 16.51/16.72 (define @t43 () (tptp.c_Expr_Oexp_OLAss @t12 @t22 @t1)) % 16.51/16.72 (define @t44 () (@list @t17 @t37 @t16 @t1 @t22 @t10 @t9)) % 16.51/16.72 (define @t45 () (tptp.c_Expr_Oexp_OSeq @t7 @t6 @t1)) % 16.51/16.72 (define @t46 () (@list @t20 @t2 @t1 @t7 @t6)) % 16.51/16.72 (define @t47 () (@var "V_s_H" $$unsorted)) % 16.51/16.72 (define @t48 () (@var "V_e_H" $$unsorted)) % 16.51/16.72 (define @t49 () (@var "V_s" $$unsorted)) % 16.51/16.72 (define @t50 () (@var "V_e" $$unsorted)) % 16.51/16.72 (define @t51 () (@var "V_P" $$unsorted)) % 16.51/16.72 (define @t52 () (not (tptp.c_SmallStep_Oredp @t51 @t50 @t49 @t48 @t47))) % 16.51/16.72 (define @t53 () (tptp.tc_List_Olist tptp.tc_String_Ochar)) % 16.51/16.72 (define @t54 () (@var "V_e_092_060_094isub_0622" $$unsorted)) % 16.51/16.72 (define @t55 () (@var "V_e_092_060_094isub_0621" $$unsorted)) % 16.51/16.72 (define @t56 () (tptp.c_Expr_Oexp_OCond @t50 @t55 @t54 @t53)) % 16.51/16.72 (define @t57 () (@var "V_x" $$unsorted)) % 16.51/16.72 (define @t58 () (@var "V_E" $$unsorted)) % 16.51/16.72 (define @t59 () (tptp.c_WellType_OWT @t51 @t58 @t56 @t57)) % 16.51/16.72 (define @t60 () (tptp.c_WellType_OWT @t51 @t58 @t50 tptp.c_Type_Oty_OBoolean)) % 16.51/16.72 (define @t61 () (not @t60)) % 16.51/16.72 (define @t62 () (not (tptp.c_WellType_OWT @t51 @t58 @t55 @t57))) % 16.51/16.72 (define @t63 () (not (tptp.c_WellType_OWT @t51 @t58 @t54 @t57))) % 16.51/16.72 (define @t64 () (tptp.tc_prod (tptp.tc_List_Olist @t53) (tptp.tc_Expr_Oexp @t53))) % 16.51/16.72 (define @t65 () (tptp.c_TypeRel_Owiden @t51 @t64)) % 16.51/16.72 (define @t66 () (tptp.hAPP @t65 @t57)) % 16.51/16.72 (define @t67 () (not (tptp.hBOOL (tptp.hAPP @t66 @t57)))) % 16.51/16.72 (define @t68 () (@var "T_b" $$unsorted)) % 16.51/16.72 (define @t69 () (@var "V_f" $$unsorted)) % 16.51/16.72 (define @t70 () (@var "V_m2" $$unsorted)) % 16.51/16.72 (define @t71 () (@var "V_m1" $$unsorted)) % 16.51/16.72 (define @t72 () (@var "V_m3" $$unsorted)) % 16.51/16.72 (define @t73 () (@var "V_T" $$unsorted)) % 16.51/16.72 (define @t74 () (not (tptp.c_WellType_OWT @t51 @t58 @t50 @t73))) % 16.51/16.72 (define @t75 () (@var "V_E_H" $$unsorted)) % 16.51/16.72 (define @t76 () (not (tptp.c_Map_Omap__le @t58 @t75 @t53 tptp.tc_Type_Oty))) % 16.51/16.72 (define @t77 () (@var "V_A" $$unsorted)) % 16.51/16.72 (define @t78 () (tptp.c_DefAss_O_092_060D_062 @t50 @t77 @t1)) % 16.51/16.72 (define @t79 () (@list @t17 @t16 @t1 @t7 @t6)) % 16.51/16.72 (define @t80 () (tptp.c_DefAss_O_092_060D_062 @t55 @t77 @t1)) % 16.51/16.72 (define @t81 () (@list @t17 @t37 @t16 @t1 @t7 @t6)) % 16.51/16.72 (define @t82 () (@list @t7 @t6 @t1 @t17 @t37 @t16)) % 16.51/16.72 (define @t83 () (@var "V_val_H" $$unsorted)) % 16.51/16.72 (define @t84 () (tptp.c_Expr_Oexp_OVal @t83 @t1)) % 16.51/16.72 (define @t85 () (@var "V_ty_H" $$unsorted)) % 16.51/16.72 (define @t86 () (tptp.c_Expr_Oexp_OBlock @t12 @t85 @t22 @t1)) % 16.51/16.72 (define @t87 () (tptp.c_Expr_Oexp_OFAcc @t2 @t30 @t29 @t1)) % 16.51/16.72 (define @t88 () (@list @t2 @t30 @t29 @t1 @t7 @t6)) % 16.51/16.72 (define @t89 () (@var "V_ty" $$unsorted)) % 16.51/16.72 (define @t90 () (@var "V_f10" $$unsorted)) % 16.51/16.72 (define @t91 () (@var "V_f15" $$unsorted)) % 16.51/16.72 (define @t92 () (@var "V_f14" $$unsorted)) % 16.51/16.72 (define @t93 () (@var "V_f13" $$unsorted)) % 16.51/16.72 (define @t94 () (@var "V_f12" $$unsorted)) % 16.51/16.72 (define @t95 () (@var "V_f11" $$unsorted)) % 16.51/16.72 (define @t96 () (@var "V_f9" $$unsorted)) % 16.51/16.72 (define @t97 () (@var "V_f8" $$unsorted)) % 16.51/16.72 (define @t98 () (@var "V_f7" $$unsorted)) % 16.51/16.72 (define @t99 () (@var "V_f6" $$unsorted)) % 16.51/16.72 (define @t100 () (@var "V_f5" $$unsorted)) % 16.51/16.72 (define @t101 () (@var "V_f4" $$unsorted)) % 16.51/16.72 (define @t102 () (@var "V_f3" $$unsorted)) % 16.51/16.72 (define @t103 () (@var "V_f2" $$unsorted)) % 16.51/16.72 (define @t104 () (@var "V_f1" $$unsorted)) % 16.51/16.72 (define @t105 () (= @t29 @t9)) % 16.51/16.72 (define @t106 () (not (= @t87 @t23))) % 16.51/16.72 (define @t107 () (@list @t2 @t30 @t29 @t1 @t22 @t10 @t9)) % 16.51/16.72 (define @t108 () (= @t30 @t10)) % 16.51/16.72 (define @t109 () (= @t16 @t6)) % 16.51/16.72 (define @t110 () (not (= @t31 @t11))) % 16.51/16.72 (define @t111 () (@list @t17 @t30 @t29 @t16 @t1 @t7 @t10 @t9 @t6)) % 16.51/16.72 (define @t112 () (= @t17 @t7)) % 16.51/16.72 (define @t113 () (tptp.c_Expr_Oexp_OBlock @t20 @t89 @t2 @t1)) % 16.51/16.72 (define @t114 () (@list @t20 @t89 @t2 @t1 @t7 @t6)) % 16.51/16.72 (define @t115 () (@var "V_h" $$unsorted)) % 16.51/16.72 (define @t116 () (tptp.c_Progress_OWTrt_H @t51 @t115 @t58 @t56 @t57)) % 16.51/16.72 (define @t117 () (not (tptp.c_Progress_OWTrt_H @t51 @t115 @t58 @t50 tptp.c_Type_Oty_OBoolean))) % 16.51/16.72 (define @t118 () (not (tptp.c_Progress_OWTrt_H @t51 @t115 @t58 @t55 @t57))) % 16.51/16.72 (define @t119 () (not (tptp.c_Progress_OWTrt_H @t51 @t115 @t58 @t54 @t57))) % 16.51/16.72 (define @t120 () (@list @t51 @t57 @t115 @t58 @t54 @t55 @t50)) % 16.51/16.72 (define @t121 () (@var "V_V" $$unsorted)) % 16.51/16.72 (define @t122 () (@var "V_C" $$unsorted)) % 16.51/16.72 (define @t123 () (tptp.c_Expr_Oexp_OTryCatch @t55 @t122 @t121 @t54 @t53)) % 16.51/16.72 (define @t124 () (@list @t2 @t30 @t29 @t1 @t7 @t13 @t12 @t6)) % 16.51/16.72 (define @t125 () (@list @t17 @t16 @t1 @t22)) % 16.51/16.72 (define @t126 () (tptp.c_Expr_Oexp_OVar @t20 @t1)) % 16.51/16.72 (define @t127 () (@list @t7 @t6 @t1 @t20 @t2)) % 16.51/16.72 (define @t128 () (@list @t32 @t1 @t7 @t6)) % 16.51/16.72 (define @t129 () (@list @t17 @t30 @t29 @t16 @t1 @t7 @t6)) % 16.51/16.72 (define @t130 () (@list @t7 @t6 @t1 @t3)) % 16.51/16.72 (define @t131 () (@list @t7 @t6 @t1 @t20 @t89 @t2)) % 16.51/16.72 (define @t132 () (@list @t3 @t2 @t1 @t7 @t6)) % 16.51/16.72 (define @t133 () (@list @t7 @t13 @t12 @t6 @t1 @t2 @t30 @t29)) % 16.51/16.72 (define @t134 () (@list @t7 @t6 @t5 @t1 @t2 @t30 @t29)) % 16.51/16.72 (define @t135 () (@list @t22 @t1 @t17 @t16)) % 16.51/16.72 (define @t136 () (@list @t20 @t2 @t1 @t22 @t10 @t9)) % 16.51/16.72 (define @t137 () (@list @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 @t2 @t30 @t29 @t68 @t1)) % 16.51/16.72 (define @t138 () (@list @t3 @t2 @t1 @t22 @t10 @t9)) % 16.51/16.72 (define @t139 () (@var "V_ys" $$unsorted)) % 16.51/16.72 (define @t140 () (@var "V_xs" $$unsorted)) % 16.51/16.72 (define @t141 () (tptp.c_fequal @t1)) % 16.51/16.72 (define @t142 () (@list @t22 @t10 @t9 @t1 @t20)) % 16.51/16.72 (define @t143 () (@list @t22 @t10 @t9 @t1 @t32)) % 16.51/16.72 (define @t144 () (@list @t12 @t85 @t22 @t1 @t2 @t30 @t29)) % 16.51/16.72 (define @t145 () (@var "V_Ts" $$unsorted)) % 16.51/16.72 (define @t146 () (@var "V_es" $$unsorted)) % 16.51/16.72 (define @t147 () (not (tptp.c_WellTypeRT_OWTrts @t51 @t115 @t58 @t146 @t145))) % 16.51/16.72 (define @t148 () (@var "V_h_H" $$unsorted)) % 16.51/16.72 (define @t149 () (not (tptp.c_Objects_Ohext @t115 @t148))) % 16.51/16.72 (define @t150 () (@var "V_h_H_H" $$unsorted)) % 16.51/16.72 (define @t151 () (@var "V_v" $$unsorted)) % 16.51/16.72 (define @t152 () (not (tptp.c_Conform_Oconf @t51 @t115 @t151 @t73 @t1))) % 16.51/16.72 (define @t153 () (@list @t20 @t1 @t22 @t10 @t9)) % 16.51/16.72 (define @t154 () (@var "V_T_092_060_094isub_0621" $$unsorted)) % 16.51/16.72 (define @t155 () (tptp.hBOOL (tptp.hAPP @t66 @t154))) % 16.51/16.72 (define @t156 () (not (tptp.c_Progress_OWTrt_H @t51 @t115 @t58 @t55 @t154))) % 16.51/16.72 (define @t157 () (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t65 @t154) @t57)))) % 16.51/16.72 (define @t158 () (@list @t51 @t154 @t57 @t115 @t58 @t54 @t55 @t50)) % 16.51/16.72 (define @t159 () (@var "V_T_092_060_094isub_0622" $$unsorted)) % 16.51/16.72 (define @t160 () (not (tptp.c_Progress_OWTrt_H @t51 @t115 @t58 @t54 @t159))) % 16.51/16.72 (define @t161 () (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t65 @t159) @t57)))) % 16.51/16.72 (define @t162 () (tptp.hBOOL (tptp.hAPP @t66 @t159))) % 16.51/16.72 (define @t163 () (@list @t51 @t57 @t159 @t115 @t58 @t54 @t55 @t50)) % 16.51/16.72 (define @t164 () (@list @t22 @t1 @t2 @t30 @t29)) % 16.51/16.72 (define @t165 () (= @t3 @t13)) % 16.51/16.72 (define @t166 () (@list @t2 @t30 @t29 @t1 @t7 @t6 @t5)) % 16.51/16.72 (define @t167 () (= @t20 @t12)) % 16.51/16.72 (define @t168 () (@list @t3 @t1 @t22 @t10 @t9)) % 16.51/16.72 (define @t169 () (not (tptp.c_WellTypeRT_OWTrt @t51 @t115 @t58 @t123 @t73))) % 16.51/16.72 (define @t170 () (tptp.c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__5__1 @t122 @t58 @t51 @t73 @t121 @t55 @t54 @t115)) % 16.51/16.72 (define @t171 () (not (= @t4 @t40))) % 16.51/16.72 (define @t172 () (@list @t3 @t2 @t1 @t13 @t22)) % 16.51/16.72 (define @t173 () (not (= @t41 @t19))) % 16.51/16.72 (define @t174 () (@list @t22 @t10 @t9 @t1 @t3)) % 16.51/16.72 (define @t175 () (@list @t2 @t30 @t29 @t1 @t12 @t85 @t22)) % 16.51/16.72 (define @t176 () (@list @t7 @t6 @t1 @t20)) % 16.51/16.72 (define @t177 () (@list @t7 @t6 @t1 @t32)) % 16.51/16.72 (define @t178 () (not (= @t25 @t45))) % 16.51/16.72 (define @t179 () (@list @t7 @t6 @t1 @t17 @t30 @t29 @t16)) % 16.51/16.72 (define @t180 () (@list @t2 @t30 @t29 @t1 @t22)) % 16.51/16.72 (define @t181 () (@list @t7 @t6 @t1 @t3 @t2)) % 16.51/16.72 (define @t182 () (@var "V_g" $$unsorted)) % 16.51/16.72 (define @t183 () (@var "V_c" $$unsorted)) % 16.51/16.72 (define @t184 () (@list @t20 @t1 @t7 @t6)) % 16.51/16.72 (define @t185 () (not @t78)) % 16.51/16.72 (define @t186 () (tptp.c_DefAss_O_092_060D_062 (tptp.c_Expr_Oexp_OLAss @t121 @t50 @t1) @t77 @t1)) % 16.51/16.72 (define @t187 () (not (= @t21 @t43))) % 16.51/16.72 (define @t188 () (@list @t20 @t2 @t1 @t12 @t22)) % 16.51/16.72 (define @t189 () (@list @t17 @t16 @t1 @t7 @t13 @t12 @t6)) % 16.51/16.72 (define @t190 () (@var "V_D" $$unsorted)) % 16.51/16.72 (define @t191 () (@var "V_F" $$unsorted)) % 16.51/16.72 (define @t192 () (not (tptp.c_WellType_OWT @t51 @t58 @t55 @t154))) % 16.51/16.72 (define @t193 () (not (tptp.c_WellType_OWT @t51 @t58 @t54 @t159))) % 16.51/16.72 (define @t194 () (@list @t22 @t10 @t9 @t1 @t3 @t2)) % 16.51/16.72 (define @t195 () (tptp.c_Expr_Oexp_OSeq @t55 @t54 @t53)) % 16.51/16.72 (define @t196 () (@list @t51 @t115 @t58 @t55 @t54 @t159 @t154)) % 16.51/16.72 (define @t197 () (tptp.c_DefAss_O_092_060D_062 (tptp.c_Expr_Oexp_OFAcc @t50 @t191 @t190 @t1) @t77 @t1)) % 16.51/16.72 (define @t198 () (tptp.tc_Option_Ooption tptp.tc_Value_Oval)) % 16.51/16.72 (define @t199 () (tptp.c_Pair tptp.v_ha____ tptp.v_la____ (tptp.tc_fun tptp.tc_nat (tptp.tc_Option_Ooption (tptp.tc_prod @t53 (tptp.tc_fun (tptp.tc_prod @t53 @t53) @t198)))) (tptp.tc_fun @t53 @t198))) % 16.51/16.72 (define @t200 () (tptp.c_WellTypeRT_OWTrt @t51 @t115 @t58 @t50 tptp.c_Type_Oty_OBoolean)) % 16.51/16.72 (define @t201 () (@list @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 @t17 @t16 @t68 @t1)) % 16.51/16.72 (define @t202 () (tptp.c_DefAss_O_092_060D_062 (tptp.c_Expr_Oexp_OCast @t122 @t50 @t1) @t77 @t1)) % 16.51/16.72 (define @t203 () (@list @t3 @t1 @t7 @t6)) % 16.51/16.72 (define @t204 () (@list @t32 @t1 @t22 @t10 @t9)) % 16.51/16.72 (define @t205 () (@var "V_b_H" $$unsorted)) % 16.51/16.72 (define @t206 () (@var "V_b" $$unsorted)) % 16.51/16.72 (define @t207 () (not (= (tptp.c_Pair @t20 @t206 @t1 @t68) (tptp.c_Pair @t12 @t205 @t1 @t68)))) % 16.51/16.72 (define @t208 () (@list @t20 @t206 @t1 @t68 @t12 @t205)) % 16.51/16.72 (define @t209 () (not (= @t113 @t86))) % 16.51/16.72 (define @t210 () (@list @t20 @t89 @t2 @t1 @t12 @t85 @t22)) % 16.51/16.72 (define @t211 () (not (= @t18 @t8))) % 16.51/16.72 (define @t212 () (@list @t17 @t16 @t15 @t1 @t7 @t6 @t5)) % 16.51/16.72 (define @t213 () (tptp.c_DefAss_O_092_060D_062 (tptp.c_Expr_Oexp_Othrow @t50 @t1) @t77 @t1)) % 16.51/16.72 (define @t214 () (not (= (tptp.c_Expr_Oexp_OTryCatch @t17 @t3 @t20 @t16 @t1) @t14))) % 16.51/16.72 (define @t215 () (@list @t17 @t3 @t20 @t16 @t1 @t7 @t13 @t12 @t6)) % 16.51/16.72 (define @t216 () (@list @t1 @t57)) % 16.51/16.72 (define @t217 () (not (= @t38 @t35))) % 16.51/16.72 (define @t218 () (@list @t17 @t37 @t16 @t1 @t7 @t34 @t6)) % 16.51/16.72 (define @t219 () (@list @t7 @t6 @t1 @t2 @t30 @t29)) % 16.51/16.72 (define @t220 () (@list @t22 @t10 @t9 @t1 @t17 @t37 @t16)) % 16.51/16.72 (define @t221 () (tptp.c_Expr_Oexp_OCall @t2 @t30 @t29 @t1)) % 16.51/16.72 (define @t222 () (tptp.c_Expr_Oexp_OCall @t22 @t10 @t9 @t1)) % 16.51/16.72 (define @t223 () (not (tptp.c_TypeSafe__Mirabelle_Osconf tptp.v_P @t58 @t199))) % 16.51/16.72 (define @t224 () (not (tptp.c_WellTypeRT_OWTrt tptp.v_P tptp.v_ha____ @t58 tptp.v_ea____ @t73))) % 16.51/16.72 (define @t225 () (tptp.v_sko__local__XCallObj__2__1 @t58 tptp.v_P @t73 tptp.v_e_Ha____ tptp.v_h_Ha____)) % 16.51/16.72 (define @t226 () (tptp.c_TypeRel_Owiden tptp.v_P @t64)) % 16.51/16.72 (define @t227 () (@list @t58 @t73)) % 16.51/16.72 (define @t228 () (@var "V_M" $$unsorted)) % 16.51/16.72 (define @t229 () (not (tptp.c_WellTypeRT_OWTrt @t51 @t115 @t58 @t55 @t154))) % 16.51/16.72 (define @t230 () (not (tptp.c_WellTypeRT_OWTrt @t51 @t115 @t58 @t54 @t159))) % 16.51/16.72 (define @t231 () (tptp.c_Expr_Oexp_OCall @t50 @t228 @t146 @t53)) % 16.51/16.72 (define @t232 () (forall (@list @t51 @t115 @t58 @t50 @t228 @t146 @t73 @t145) (or (tptp.c_WellTypeRT_OWTrt @t51 @t115 @t58 @t231 @t73) @t147 (not (tptp.c_WellTypeRT_OWTrt @t51 @t115 @t58 @t50 tptp.c_Type_Oty_ONT))))) % 16.51/16.72 (define @t233 () (@var "V_Ea" $$unsorted)) % 16.51/16.72 (define @t234 () (not (tptp.c_TypeSafe__Mirabelle_Osconf tptp.v_P @t233 @t199))) % 16.51/16.72 (define @t235 () (@var "V_Ta" $$unsorted)) % 16.51/16.72 (define @t236 () (not (tptp.c_WellTypeRT_OWTrt tptp.v_P tptp.v_ha____ @t233 tptp.v_ea____ @t235))) % 16.51/16.72 (define @t237 () (tptp.v_sko__local__XIH__1 @t233 tptp.v_P @t235 tptp.v_e_Ha____ tptp.v_h_Ha____)) % 16.51/16.72 (define @t238 () (@list @t233 @t235)) % 16.51/16.72 (define @t239 () (tptp.c_WellTypeRT_OWTrt @t51 @t115 @t58 @t56 @t57)) % 16.51/16.72 (define @t240 () (not @t200)) % 16.51/16.72 (define @t241 () (not (tptp.c_WellTypeRT_OWTrt @t51 @t115 @t58 @t55 @t57))) % 16.51/16.72 (define @t242 () (not (tptp.c_WellTypeRT_OWTrt @t51 @t115 @t58 @t54 @t57))) % 16.51/16.72 (define @t243 () (tptp.c_WellTypeRT_OWTrt @t51 @t115 @t58 @t50 @t73)) % 16.51/16.72 (define @t244 () (not @t243)) % 16.51/16.72 (define @t245 () (tptp.c_Progress_OWTrt_H @t51 @t115 @t58 @t50 @t73)) % 16.51/16.72 (define @t246 () (@list @t51 @t115 @t58 @t50 @t73)) % 16.51/16.72 (define @t247 () (tptp.v_sko__local__XCallObj__Xhyps__2__1 @t58 tptp.v_P @t73 tptp.v_e_Ha____ tptp.v_h_Ha____)) % 16.51/16.72 (define @t248 () (not (= @t221 @t222))) % 16.51/16.72 (define @t249 () (tptp.c_TypeRel_Owiden @t51 @t1)) % 16.51/16.72 (define @t250 () (tptp.hAPP @t249 @t73)) % 16.51/16.72 (define @t251 () (@var "V_U" $$unsorted)) % 16.51/16.72 (define @t252 () (@var "V_S" $$unsorted)) % 16.51/16.72 (define @t253 () (tptp.hAPP @t249 @t252)) % 16.51/16.72 (define @t254 () (@var "V_T_H" $$unsorted)) % 16.51/16.72 (define @t255 () (@var "V_Ss" $$unsorted)) % 16.51/16.72 (define @t256 () (@var "V_Us" $$unsorted)) % 16.51/16.72 (define @t257 () (tptp.c_WellTypeRT_OWTrts tptp.v_P tptp.v_h_Ha____ tptp.v_E____ tptp.v_esa____ tptp.v_Ts____)) % 16.51/16.72 (define @t258 () (tptp.c_WellTypeRT_OWTrt tptp.v_P tptp.v_h_Ha____ tptp.v_E____ tptp.v_e_Ha____ tptp.c_Type_Oty_ONT)) % 16.51/16.72 (define @t259 () (tptp.c_Expr_Oexp_OCall tptp.v_e_Ha____ tptp.v_M____ tptp.v_esa____ @t53)) % 16.51/16.72 (define @t260 () (@var "V_Y" $$unsorted)) % 16.51/16.72 (define @t261 () (@var "V_X" $$unsorted)) % 16.51/16.72 (define @t262 () (tptp.c_WellTypeRT_OWTrt tptp.v_P tptp.v_h_Ha____ tptp.v_E____ @t259 tptp.v_T____)) % 16.51/16.72 (define @t263 () (not @t262)) % 16.51/16.72 (define @t264 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t226 tptp.v_T____) tptp.v_T____))) % 16.51/16.72 (define @t265 () (not @t264)) % 16.51/16.72 (define @t266 () (or @t265 @t263)) % 16.51/16.72 (define @t267 () (not @t258)) % 16.51/16.72 (define @t268 () (not @t257)) % 16.51/16.72 (define @t269 () (or @t262 @t268 @t267)) % 16.51/16.72 (define @t270 () (not @t269)) % 16.51/16.72 (assume @p1 (forall (@list @t7 @t6 @t5 @t1 @t3 @t2) (not (= @t8 @t4)))) % 16.51/16.72 (assume @p2 (forall (@list @t3 @t2 @t1 @t7 @t10 @t9 @t6) (not (= @t4 @t11)))) % 16.51/16.72 (assume @p3 (forall (@list @t7 @t13 @t12 @t6 @t1 @t3 @t2) (not (= @t14 @t4)))) % 16.51/16.72 (assume @p4 (forall (@list @t7 @t6 @t1 @t17 @t16 @t15) (not (= @t19 @t18)))) % 16.51/16.72 (assume @p5 (forall (@list @t20 @t2 @t1 @t7 @t10 @t9 @t6) (not (= @t21 @t11)))) % 16.51/16.72 (assume @p6 (forall @t24 (not (= @t23 @t21)))) % 16.51/16.72 (assume @p7 (forall (@list @t17 @t16 @t1 @t7 @t6 @t5) (not (= @t25 @t8)))) % 16.51/16.72 (assume @p8 (forall (@list @t2 @t1 @t22) (or (not (= @t28 @t27)) @t26))) % 16.51/16.72 (assume @p9 (forall (@list @t7 @t6 @t5 @t1 @t17 @t30 @t29 @t16) (not (= @t8 @t31)))) % 16.51/16.72 (assume @p10 (forall (@list @t7 @t34 @t6 @t1 @t32) (not (= @t35 @t33)))) % 16.51/16.72 (assume @p11 (forall (@list @t17 @t37 @t16 @t1 @t12) (not (= @t38 @t36)))) % 16.51/16.72 (assume @p12 (forall (@list @t7 @t13 @t12 @t6 @t1 @t17 @t30 @t29 @t16) (not (= @t14 @t31)))) % 16.51/16.72 (assume @p13 (forall (@list @t12 @t1 @t32) (not (= @t36 @t33)))) % 16.51/16.72 (assume @p14 (forall (@list @t13 @t22 @t1 @t3) (not (= @t40 @t39)))) % 16.51/16.72 (assume @p15 (forall @t42 (not (= @t14 @t41)))) % 16.51/16.72 (assume @p16 (forall (@list @t12 @t22 @t1 @t17 @t37 @t16) (not (= @t43 @t38)))) % 16.51/16.72 (assume @p17 (forall @t44 (not (= @t38 @t23)))) % 16.51/16.72 (assume @p18 (forall @t46 (not (= @t21 @t45)))) % 16.51/16.72 (assume @p19 (forall (@list @t51 @t50 @t55 @t54 @t49 @t48 @t47) (or (tptp.c_SmallStep_Oredp @t51 @t56 @t49 (tptp.c_Expr_Oexp_OCond @t48 @t55 @t54 @t53) @t47) @t52))) % 16.51/16.72 (assume @p20 (forall (@list @t51 @t57 @t58 @t54 @t55 @t50) (or @t67 @t63 @t62 @t61 @t59))) % 16.51/16.72 (assume @p21 (forall (@list @t7 @t34 @t6 @t1 @t3 @t2) (not (= @t35 @t4)))) % 16.51/16.72 (assume @p22 (forall (@list @t69 @t1 @t68) (tptp.c_Map_Omap__le @t69 @t69 @t1 @t68))) % 16.51/16.72 (assume @p23 (forall (@list @t71 @t72 @t1 @t68 @t70) (or (tptp.c_Map_Omap__le @t71 @t72 @t1 @t68) (not (tptp.c_Map_Omap__le @t70 @t72 @t1 @t68)) (not (tptp.c_Map_Omap__le @t71 @t70 @t1 @t68))))) % 16.51/16.72 (assume @p24 (forall (@list @t51 @t75 @t50 @t73 @t58) (or (tptp.c_WellType_OWT @t51 @t75 @t50 @t73) @t76 @t74))) % 16.51/16.72 (assume @p25 (forall (@list @t50 @t77 @t1 @t55 @t54) (or @t78 (not (tptp.c_DefAss_O_092_060D_062 (tptp.c_Expr_Oexp_OCond @t50 @t55 @t54 @t1) @t77 @t1))))) % 16.51/16.72 (assume @p26 (forall (@list @t20 @t2 @t1 @t22) (not (= @t21 @t27)))) % 16.51/16.72 (assume @p27 (forall (@list @t7 @t6 @t5 @t1 @t17 @t37 @t16) (not (= @t8 @t38)))) % 16.51/16.72 (assume @p28 (forall (@list @t17 @t30 @t29 @t16 @t1 @t7 @t13 @t12 @t6) (not (= @t31 @t14)))) % 16.51/16.72 (assume @p29 (forall @t79 (not (= @t25 @t19)))) % 16.51/16.72 (assume @p30 (forall (@list @t55 @t77 @t1 @t37 @t54) (or @t80 (not (tptp.c_DefAss_O_092_060D_062 (tptp.c_Expr_Oexp_OBinOp @t55 @t37 @t54 @t1) @t77 @t1))))) % 16.51/16.72 (assume @p31 (forall @t81 (not (= @t38 @t19)))) % 16.51/16.72 (assume @p32 (forall (@list @t17 @t37 @t16 @t1 @t7 @t10 @t9 @t6) (not (= @t38 @t11)))) % 16.51/16.72 (assume @p33 (forall (@list @t32 @t1 @t12 @t22) (not (= @t33 @t43)))) % 16.51/16.72 (assume @p34 (forall @t82 (not (= @t19 @t38)))) % 16.51/16.72 (assume @p35 (forall (@list @t83 @t1 @t3) (not (= @t84 @t39)))) % 16.51/16.72 (assume @p36 (forall (@list @t3 @t1 @t7 @t6 @t5) (not (= @t39 @t8)))) % 16.51/16.72 (assume @p37 (forall (@list @t7 @t13 @t12 @t6 @t1 @t3) (not (= @t14 @t39)))) % 16.51/16.72 (assume @p38 (forall (@list @t12 @t85 @t22 @t1 @t17 @t37 @t16) (not (= @t86 @t38)))) % 16.51/16.72 (assume @p39 (forall (@list @t3 @t2 @t1 @t7 @t34 @t6) (not (= @t4 @t35)))) % 16.51/16.72 (assume @p40 (forall (@list @t20 @t2 @t1 @t12 @t85 @t22) (not (= @t21 @t86)))) % 16.51/16.72 (assume @p41 (forall (@list @t17 @t16 @t15 @t1 @t22) (not (= @t18 @t27)))) % 16.51/16.72 (assume @p42 (forall @t88 (not (= @t87 @t45)))) % 16.51/16.72 (assume @p43 (forall (@list @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 @t20 @t89 @t2 @t68 @t1) (= (tptp.c_Expr_Oexp_Oexp__case @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 (tptp.c_Expr_Oexp_OBlock @t20 @t89 @t2 @t68) @t1 @t68) (tptp.hAPP (tptp.hAPP (tptp.hAPP @t90 @t20) @t89) @t2)))) % 16.51/16.72 (assume @p44 (forall @t107 (or @t106 @t105))) % 16.51/16.72 (assume @p45 (forall @t107 (or @t106 @t108))) % 16.51/16.72 (assume @p46 (forall @t107 (or @t106 @t26))) % 16.51/16.72 (assume @p47 (forall @t111 (or @t110 @t109))) % 16.51/16.72 (assume @p48 (forall @t111 (or @t110 @t105))) % 16.51/16.72 (assume @p49 (forall @t111 (or @t110 @t108))) % 16.51/16.72 (assume @p50 (forall @t111 (or @t110 @t112))) % 16.51/16.72 (assume @p51 (forall @t114 (not (= @t113 @t45)))) % 16.51/16.72 (assume @p52 (forall (@list @t51 @t50 @t54 @t49 @t48 @t47) (or (tptp.c_SmallStep_Oredp @t51 (tptp.c_Expr_Oexp_OSeq @t50 @t54 @t53) @t49 (tptp.c_Expr_Oexp_OSeq @t48 @t54 @t53) @t47) @t52))) % 16.51/16.72 (assume @p53 (forall @t120 (or @t67 @t119 @t118 @t117 @t116))) % 16.51/16.72 (assume @p54 (forall (@list @t51 @t58 @t55 @t73 @t122 @t121 @t54) (or (tptp.c_WellType_OWT @t51 @t58 @t55 @t73) (not (tptp.c_WellType_OWT @t51 @t58 @t123 @t73))))) % 16.51/16.72 (assume @p55 (forall @t124 (not (= @t87 @t14)))) % 16.51/16.72 (assume @p56 (forall (@list @t3 @t1 @t83) (not (= @t39 @t84)))) % 16.51/16.72 (assume @p57 (forall (@list @t3 @t1 @t12) (not (= @t39 @t36)))) % 16.51/16.72 (assume @p58 (forall (@list @t22 @t1 @t17 @t16 @t15) (not (= @t27 @t18)))) % 16.51/16.72 (assume @p59 (forall @t125 (not (= @t41 @t27)))) % 16.51/16.72 (assume @p60 (forall (@list @t20 @t89 @t2 @t1 @t22) (not (= @t113 @t27)))) % 16.51/16.72 (assume @p61 (forall (@list @t20 @t1 @t7 @t6 @t5) (not (= @t126 @t8)))) % 16.51/16.72 (assume @p62 (forall (@list @t3 @t2 @t1 @t22) (not (= @t4 @t27)))) % 16.51/16.72 (assume @p63 (forall (@list @t7 @t6 @t5 @t1 @t20 @t89 @t2) (not (= @t8 @t113)))) % 16.51/16.72 (assume @p64 (forall @t127 (not (= @t19 @t21)))) % 16.51/16.72 (assume @p65 (forall (@list @t3 @t2 @t1 @t83) (not (= @t4 @t84)))) % 16.51/16.72 (assume @p66 (forall (@list @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 @t2 @t68 @t1) (= (tptp.c_Expr_Oexp_Oexp__case @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 (tptp.c_Expr_Oexp_Othrow @t2 @t68) @t1 @t68) (tptp.hAPP @t92 @t2)))) % 16.51/16.72 (assume @p67 (forall (@list @t3 @t2 @t1 @t12) (not (= @t4 @t36)))) % 16.51/16.72 (assume @p68 (forall @t128 (not (= @t33 @t19)))) % 16.51/16.72 (assume @p69 (forall @t129 (not (= @t31 @t45)))) % 16.51/16.72 (assume @p70 (forall @t130 (not (= @t19 @t39)))) % 16.51/16.72 (assume @p71 (forall @t127 (not (= @t45 @t21)))) % 16.51/16.72 (assume @p72 (forall (@list @t7 @t6 @t5 @t1 @t17 @t16) (not (= @t8 @t25)))) % 16.51/16.72 (assume @p73 (forall @t131 (not (= @t19 @t113)))) % 16.51/16.72 (assume @p74 (forall (@list @t7 @t13 @t12 @t6 @t1 @t17 @t37 @t16) (not (= @t14 @t38)))) % 16.51/16.72 (assume @p75 (forall (@list @t20 @t89 @t2 @t1 @t7 @t6 @t5) (not (= @t113 @t8)))) % 16.51/16.72 (assume @p76 (forall (@list @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 @t3 @t68 @t1) (= (tptp.c_Expr_Oexp_Oexp__case @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 (tptp.c_Expr_Oexp_Onew @t3 @t68) @t1 @t68) (tptp.hAPP @t104 @t3)))) % 16.51/16.72 (assume @p77 (forall @t132 (not (= @t4 @t19)))) % 16.51/16.72 (assume @p78 (forall (@list @t12 @t22 @t1 @t3 @t2) (not (= @t43 @t4)))) % 16.51/16.72 (assume @p79 (forall (@list @t51 @t50 @t122 @t121 @t54 @t49 @t48 @t47) (or (tptp.c_SmallStep_Oredp @t51 (tptp.c_Expr_Oexp_OTryCatch @t50 @t122 @t121 @t54 @t53) @t49 (tptp.c_Expr_Oexp_OTryCatch @t48 @t122 @t121 @t54 @t53) @t47) @t52))) % 16.51/16.72 (assume @p80 (forall @t114 (not (= @t113 @t19)))) % 16.51/16.72 (assume @p81 (forall @t133 (not (= @t14 @t87)))) % 16.51/16.72 (assume @p82 (forall @t134 (not (= @t8 @t87)))) % 16.51/16.72 (assume @p83 (forall @t135 (not (= @t27 @t25)))) % 16.51/16.72 (assume @p84 (forall (@list @t7 @t6 @t5 @t1 @t20) (not (= @t8 @t126)))) % 16.51/16.72 (assume @p85 (forall (@list @t7 @t6 @t5 @t1 @t32) (not (= @t8 @t33)))) % 16.51/16.72 (assume @p86 (forall (@list @t7 @t10 @t9 @t6 @t1 @t20 @t2) (not (= @t11 @t21)))) % 16.51/16.72 (assume @p87 (forall (@list @t7 @t10 @t9 @t6 @t1 @t20) (not (= @t11 @t126)))) % 16.51/16.72 (assume @p88 (forall (@list @t7 @t10 @t9 @t6 @t1 @t32) (not (= @t11 @t33)))) % 16.51/16.72 (assume @p89 (forall @t136 (not (= @t21 @t23)))) % 16.51/16.72 (assume @p90 (forall @t137 (= (tptp.c_Expr_Oexp_Oexp__case @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 (tptp.c_Expr_Oexp_OFAcc @t2 @t30 @t29 @t68) @t1 @t68) (tptp.hAPP (tptp.hAPP (tptp.hAPP @t98 @t2) @t30) @t29)))) % 16.51/16.72 (assume @p91 (forall (@list @t20 @t1 @t7 @t13 @t12 @t6) (not (= @t126 @t14)))) % 16.51/16.72 (assume @p92 (forall (@list @t17 @t16 @t15 @t1 @t7 @t6) (not (= @t18 @t19)))) % 16.51/16.72 (assume @p93 (forall @t138 (not (= @t4 @t23)))) % 16.51/16.72 (assume @p94 (forall (@list @t51 @t1) (= (tptp.c_COMBI @t51 @t1) @t51))) % 16.51/16.72 (assume @p95 (forall (@list @t12 @t85 @t22 @t1 @t17 @t30 @t29 @t16) (not (= @t86 @t31)))) % 16.51/16.72 (assume @p96 (forall (@list @t3 @t1 @t12 @t85 @t22) (not (= @t39 @t86)))) % 16.51/16.72 (assume @p97 (not (= tptp.c_Type_Oty_ONT tptp.c_Type_Oty_OBoolean))) % 16.51/16.72 (assume @p98 (forall (@list @t32 @t1 @t7 @t6 @t5) (not (= @t33 @t8)))) % 16.51/16.72 (assume @p99 (forall (@list @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 @t3 @t2 @t68 @t1) (= (tptp.c_Expr_Oexp_Oexp__case @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 (tptp.c_Expr_Oexp_OCast @t3 @t2 @t68) @t1 @t68) (tptp.hAPP (tptp.hAPP @t103 @t3) @t2)))) % 16.51/16.72 (assume @p100 (forall (@list @t2 @t1 @t7 @t13 @t12 @t6) (not (= @t28 @t14)))) % 16.51/16.72 (assume @p101 (forall (@list @t12 @t85 @t22 @t1 @t20) (not (= @t86 @t126)))) % 16.51/16.72 (assume @p102 (forall (@list @t12 @t85 @t22 @t1 @t32) (not (= @t86 @t33)))) % 16.51/16.72 (assume @p103 (forall (@list @t140 @t139 @t1) (or (= @t140 @t139) (not (tptp.c_List_Olist__all2 @t141 @t140 @t139 @t1 @t1))))) % 16.51/16.72 (assume @p104 (forall @t142 (not (= @t23 @t126)))) % 16.51/16.72 (assume @p105 (forall @t143 (not (= @t23 @t33)))) % 16.51/16.72 (assume @p106 (forall (@list @t17 @t16 @t15 @t1 @t7 @t13 @t12 @t6) (not (= @t18 @t14)))) % 16.51/16.72 (assume @p107 (forall (@list @t12 @t85 @t22 @t1 @t3 @t2) (not (= @t86 @t4)))) % 16.51/16.72 (assume @p108 (forall @t46 (not (= @t21 @t19)))) % 16.51/16.72 (assume @p109 (forall (@list @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 @t17 @t30 @t29 @t16 @t68 @t1) (= (tptp.c_Expr_Oexp_Oexp__case @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 (tptp.c_Expr_Oexp_OFAss @t17 @t30 @t29 @t16 @t68) @t1 @t68) (tptp.hAPP (tptp.hAPP (tptp.hAPP (tptp.hAPP @t97 @t17) @t30) @t29) @t16)))) % 16.51/16.72 (assume @p110 (forall (@list @t20 @t1 @t7 @t10 @t9 @t6) (not (= @t126 @t11)))) % 16.51/16.72 (assume @p111 (forall (@list @t12 @t1 @t3) (not (= @t36 @t39)))) % 16.51/16.72 (assume @p112 (forall (@list @t3 @t1 @t22) (not (= @t39 @t27)))) % 16.51/16.72 (assume @p113 (forall (@list @t22 @t1 @t17 @t30 @t29 @t16) (not (= @t27 @t31)))) % 16.51/16.72 (assume @p114 (forall (@list @t7 @t34 @t6 @t1 @t3) (not (= @t35 @t39)))) % 16.51/16.72 (assume @p115 (forall @t144 (not (= @t86 @t87)))) % 16.51/16.72 (assume @p116 (forall (@list @t51 @t58 @t50 @t55 @t54 @t73) (or @t60 (not (tptp.c_WellType_OWT @t51 @t58 @t56 @t73))))) % 16.51/16.72 (assume @p117 (forall (@list @t22 @t1 @t20 @t89 @t2) (not (= @t27 @t113)))) % 16.51/16.72 (assume @p118 (forall (@list @t12 @t1 @t3 @t2) (not (= @t36 @t4)))) % 16.51/16.72 (assume @p119 (forall (@list @t22 @t1 @t3 @t2) (not (= @t27 @t4)))) % 16.51/16.72 (assume @p120 (forall (@list @t51 @t148 @t58 @t146 @t145 @t115) (or (tptp.c_WellTypeRT_OWTrts @t51 @t148 @t58 @t146 @t145) @t149 @t147))) % 16.51/16.72 (assume @p121 (forall (@list @t115 @t150 @t148) (or (tptp.c_Objects_Ohext @t115 @t150) (not (tptp.c_Objects_Ohext @t148 @t150)) @t149))) % 16.51/16.72 (assume @p122 (forall (@list @t115) (tptp.c_Objects_Ohext @t115 @t115))) % 16.51/16.72 (assume @p123 (forall (@list @t51 @t148 @t151 @t73 @t1 @t115) (or (tptp.c_Conform_Oconf @t51 @t148 @t151 @t73 @t1) @t152 @t149))) % 16.51/16.72 (assume @p124 (forall (@list @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 @t32 @t68 @t1) (= (tptp.c_Expr_Oexp_Oexp__case @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 (tptp.c_Expr_Oexp_OVal @t32 @t68) @t1 @t68) (tptp.hAPP @t102 @t32)))) % 16.51/16.72 (assume @p125 (forall (@list @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 @t20 @t68 @t1) (= (tptp.c_Expr_Oexp_Oexp__case @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 (tptp.c_Expr_Oexp_OVar @t20 @t68) @t1 @t68) (tptp.hAPP @t100 @t20)))) % 16.51/16.72 (assume @p126 (forall (@list @t3 @t1 @t7 @t10 @t9 @t6) (not (= @t39 @t11)))) % 16.51/16.72 (assume @p127 (forall @t153 (not (= @t126 @t23)))) % 16.51/16.72 (assume @p128 (forall (@list @t3 @t1 @t7 @t34 @t6) (not (= @t39 @t35)))) % 16.51/16.72 (assume @p129 (forall @t158 (or @t157 @t119 @t156 @t117 @t116 @t155))) % 16.51/16.72 (assume @p130 (forall @t163 (or @t162 @t161 @t160 @t118 @t117 @t116))) % 16.51/16.72 (assume @p131 (forall (@list @t12 @t22 @t1 @t20) (not (= @t43 @t126)))) % 16.51/16.72 (assume @p132 (forall (@list @t12 @t22 @t1 @t32) (not (= @t43 @t33)))) % 16.51/16.72 (assume @p133 (forall @t164 (not (= @t27 @t87)))) % 16.51/16.72 (assume @p134 (forall (@list @t7 @t6 @t5 @t1 @t3) (not (= @t8 @t39)))) % 16.51/16.72 (assume @p135 (forall (@list @t3 @t1 @t13) (or (not (= @t39 (tptp.c_Expr_Oexp_Onew @t13 @t1))) @t165))) % 16.51/16.72 (assume @p136 (forall @t166 (not (= @t87 @t8)))) % 16.51/16.72 (assume @p137 (forall (@list @t7 @t10 @t9 @t6 @t1 @t3) (not (= @t11 @t39)))) % 16.51/16.72 (assume @p138 (forall (@list @t3 @t1 @t13 @t22) (not (= @t39 @t40)))) % 16.51/16.72 (assume @p139 (forall (@list @t20 @t1 @t12) (or (not (= @t126 @t36)) @t167))) % 16.51/16.72 (assume @p140 (forall (@list @t122 @t1 @t77) (tptp.c_DefAss_O_092_060D_062 (tptp.c_Expr_Oexp_Onew @t122 @t1) @t77 @t1))) % 16.51/16.72 (assume @p141 (forall (@list @t17 @t30 @t29 @t16 @t1 @t12 @t85 @t22) (not (= @t31 @t86)))) % 16.51/16.72 (assume @p142 (forall (@list @t3 @t1 @t7 @t13 @t12 @t6) (not (= @t39 @t14)))) % 16.51/16.72 (assume @p143 (forall (@list @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 @t17 @t3 @t20 @t16 @t68 @t1) (= (tptp.c_Expr_Oexp_Oexp__case @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 (tptp.c_Expr_Oexp_OTryCatch @t17 @t3 @t20 @t16 @t68) @t1 @t68) (tptp.hAPP (tptp.hAPP (tptp.hAPP (tptp.hAPP @t91 @t17) @t3) @t20) @t16)))) % 16.51/16.72 (assume @p144 (forall @t168 (not (= @t39 @t23)))) % 16.51/16.72 (assume @p145 (forall (@list @t22 @t1 @t17 @t37 @t16) (not (= @t27 @t38)))) % 16.51/16.72 (assume @p146 (forall (@list @t51 @t115 @t58 @t55 @t122 @t73 @t121 @t54) (or (tptp.c_WellTypeRT_OWTrt @t51 @t115 @t58 @t55 @t170) @t169))) % 16.51/16.72 (assume @p147 (forall @t172 (or @t171 @t165))) % 16.51/16.72 (assume @p148 (forall @t172 (or @t171 @t26))) % 16.51/16.72 (assume @p149 (forall (@list @t12 @t85 @t22 @t1 @t3) (not (= @t86 @t39)))) % 16.51/16.72 (assume @p150 (forall (@list @t17 @t30 @t29 @t16 @t1 @t7 @t6 @t5) (not (= @t31 @t8)))) % 16.51/16.72 (assume @p151 (forall @t79 (or @t173 @t112))) % 16.51/16.72 (assume @p152 (forall @t79 (or @t173 @t109))) % 16.51/16.72 (assume @p153 (not (= tptp.c_Type_Oty_OBoolean tptp.c_Type_Oty_ONT))) % 16.51/16.72 (assume @p154 (forall (@list @t17 @t30 @t29 @t16 @t1 @t22) (not (= @t31 @t27)))) % 16.51/16.72 (assume @p155 (forall @t174 (not (= @t23 @t39)))) % 16.51/16.72 (assume @p156 (forall (@list @t17 @t37 @t16 @t1 @t7 @t13 @t12 @t6) (not (= @t38 @t14)))) % 16.51/16.72 (assume @p157 (forall (@list @t17 @t37 @t16 @t1 @t12 @t22) (not (= @t38 @t43)))) % 16.51/16.72 (assume @p158 (forall @t175 (not (= @t87 @t86)))) % 16.51/16.72 (assume @p159 (forall (@list @t7 @t6 @t1 @t17 @t16) (not (= @t19 @t25)))) % 16.51/16.72 (assume @p160 (forall @t176 (not (= @t45 @t126)))) % 16.51/16.72 (assume @p161 (forall @t177 (not (= @t45 @t33)))) % 16.51/16.72 (assume @p162 (forall (@list @t20 @t1 @t12 @t85 @t22) (not (= @t126 @t86)))) % 16.51/16.72 (assume @p163 (forall @t79 (or @t178 @t112))) % 16.51/16.72 (assume @p164 (forall @t79 (or @t178 @t109))) % 16.51/16.72 (assume @p165 (forall @t179 (not (= @t45 @t31)))) % 16.51/16.72 (assume @p166 (forall (@list @t22 @t1 @t20) (not (= @t27 @t126)))) % 16.51/16.72 (assume @p167 (forall (@list @t22 @t1 @t32) (not (= @t27 @t33)))) % 16.51/16.72 (assume @p168 (forall (@list @t7 @t10 @t9 @t6 @t1 @t17 @t37 @t16) (not (= @t11 @t38)))) % 16.51/16.72 (assume @p169 (forall (@list @t20 @t2 @t1 @t7 @t13 @t12 @t6) (not (= @t21 @t14)))) % 16.51/16.72 (assume @p170 (forall @t179 (not (= @t19 @t31)))) % 16.51/16.72 (assume @p171 (forall @t180 (not (= @t87 @t27)))) % 16.51/16.72 (assume @p172 (forall (@list @t20 @t1 @t22) (not (= @t126 @t27)))) % 16.51/16.72 (assume @p173 (forall @t181 (not (= @t45 @t4)))) % 16.51/16.72 (assume @p174 (forall (@list @t12 @t22 @t1 @t3) (not (= @t43 @t39)))) % 16.51/16.72 (assume @p175 (forall @t181 (not (= @t19 @t4)))) % 16.51/16.72 (assume @p176 (forall (@list @t3 @t2 @t1 @t12 @t85 @t22) (not (= @t4 @t86)))) % 16.51/16.72 (assume @p177 (forall (@list @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 @t17 @t37 @t16 @t68 @t1) (= (tptp.c_Expr_Oexp_Oexp__case @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 (tptp.c_Expr_Oexp_OBinOp @t17 @t37 @t16 @t68) @t1 @t68) (tptp.hAPP (tptp.hAPP (tptp.hAPP @t101 @t17) @t37) @t16)))) % 16.51/16.72 (assume @p178 (forall (@list @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 @t20 @t2 @t68 @t1) (= (tptp.c_Expr_Oexp_Oexp__case @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 (tptp.c_Expr_Oexp_OLAss @t20 @t2 @t68) @t1 @t68) (tptp.hAPP (tptp.hAPP @t99 @t20) @t2)))) % 16.51/16.72 (assume @p179 (forall (@list @t7 @t13 @t12 @t6 @t1 @t2) (not (= @t14 @t28)))) % 16.51/16.72 (assume @p180 (forall (@list @t3 @t2 @t1 @t7 @t13 @t12 @t6) (not (= @t4 @t14)))) % 16.51/16.72 (assume @p181 (forall @t81 (not (= @t38 @t45)))) % 16.51/16.72 (assume @p182 (forall (@list @t32 @t1 @t12) (not (= @t33 @t36)))) % 16.51/16.72 (assume @p183 (forall (@list @t7 @t10 @t9 @t6 @t1 @t2 @t30 @t29) (not (= @t11 @t87)))) % 16.51/16.72 (assume @p184 (forall (@list @t69 @t182 @t1 @t68) (or (= @t69 @t182) (not (tptp.c_Map_Omap__le @t182 @t69 @t1 @t68)) (not (tptp.c_Map_Omap__le @t69 @t182 @t1 @t68))))) % 16.51/16.72 (assume @p185 (forall @t82 (not (= @t45 @t38)))) % 16.51/16.72 (assume @p186 (forall (@list @t50 @t77 @t1 @t183) (or @t78 (not (tptp.c_DefAss_O_092_060D_062 (tptp.c_Expr_Oexp_OWhile @t50 @t183 @t1) @t77 @t1))))) % 16.51/16.72 (assume @p187 (forall (@list @t7 @t13 @t12 @t6 @t1 @t32) (not (= @t14 @t33)))) % 16.51/16.72 (assume @p188 (forall (@list @t7 @t13 @t12 @t6 @t1 @t20) (not (= @t14 @t126)))) % 16.51/16.72 (assume @p189 (forall @t184 (not (= @t126 @t45)))) % 16.51/16.72 (assume @p190 (forall (@list @t3 @t2 @t1 @t7 @t6 @t5) (not (= @t4 @t8)))) % 16.51/16.72 (assume @p191 (forall (@list @t121 @t50 @t1 @t77) (or @t186 @t185))) % 16.51/16.72 (assume @p192 (forall (@list @t50 @t77 @t1 @t121) (or @t78 (not @t186)))) % 16.51/16.72 (assume @p193 (forall @t188 (or @t187 @t26))) % 16.51/16.72 (assume @p194 (forall @t188 (or @t187 @t167))) % 16.51/16.72 (assume @p195 (forall (@list @t20 @t2 @t1 @t7 @t6 @t5) (not (= @t21 @t8)))) % 16.51/16.72 (assume @p196 (forall (@list @t7 @t10 @t9 @t6 @t1 @t3 @t2) (not (= @t11 @t4)))) % 16.51/16.72 (assume @p197 (forall (@list @t7 @t13 @t12 @t6 @t1 @t20 @t89 @t2) (not (= @t14 @t113)))) % 16.51/16.72 (assume @p198 (forall (@list @t7 @t13 @t12 @t6 @t1 @t17 @t16 @t15) (not (= @t14 @t18)))) % 16.51/16.72 (assume @p199 (forall @t125 (not (= @t25 @t27)))) % 16.51/16.72 (assume @p200 (forall @t189 (not (= @t41 @t14)))) % 16.51/16.72 (assume @p201 (forall (@list @t17 @t37 @t16 @t1 @t22) (not (= @t38 @t27)))) % 16.51/16.72 (assume @p202 (forall (@list @t3 @t1 @t12 @t22) (not (= @t39 @t43)))) % 16.51/16.72 (assume @p203 (forall (@list @t55 @t77 @t1 @t191 @t190 @t54) (or @t80 (not (tptp.c_DefAss_O_092_060D_062 (tptp.c_Expr_Oexp_OFAss @t55 @t191 @t190 @t54 @t1) @t77 @t1))))) % 16.51/16.72 (assume @p204 (forall (@list @t51 @t154 @t57 @t58 @t54 @t55 @t50) (or @t157 @t63 @t192 @t61 @t59 @t155))) % 16.51/16.72 (assume @p205 (forall (@list @t51 @t57 @t159 @t58 @t54 @t55 @t50) (or @t162 @t161 @t193 @t62 @t61 @t59))) % 16.51/16.72 (assume @p206 (forall @t184 (not (= @t126 @t19)))) % 16.51/16.72 (assume @p207 (forall @t194 (not (= @t23 @t4)))) % 16.51/16.72 (assume @p208 (forall @t88 (not (= @t87 @t19)))) % 16.51/16.72 (assume @p209 (forall @t177 (not (= @t19 @t33)))) % 16.51/16.72 (assume @p210 (forall @t176 (not (= @t19 @t126)))) % 16.51/16.72 (assume @p211 (forall @t196 (or (tptp.c_Progress_OWTrt_H @t51 @t115 @t58 @t195 @t159) @t160 @t156))) % 16.51/16.72 (assume @p212 (forall (@list @t32 @t1 @t7 @t34 @t6) (not (= @t33 @t35)))) % 16.51/16.72 (assume @p213 (forall @t131 (not (= @t45 @t113)))) % 16.51/16.72 (assume @p214 (forall (@list @t22 @t1 @t20 @t2) (not (= @t27 @t21)))) % 16.51/16.72 (assume @p215 (forall (@list @t17 @t37 @t16 @t1 @t12 @t85 @t22) (not (= @t38 @t86)))) % 16.51/16.72 (assume @p216 (forall (@list @t20 @t1 @t12 @t22) (not (= @t126 @t43)))) % 16.51/16.72 (assume @p217 (forall (@list @t2 @t30 @t29 @t1 @t7 @t10 @t9 @t6) (not (= @t87 @t11)))) % 16.51/16.72 (assume @p218 (forall (@list @t50 @t191 @t190 @t1 @t77) (or @t197 @t185))) % 16.51/16.72 (assume @p219 (forall (@list @t50 @t77 @t1 @t191 @t190) (or @t78 (not @t197)))) % 16.51/16.72 (assume @p220 (tptp.c_TypeSafe__Mirabelle_Osconf tptp.v_P tptp.v_E____ @t199)) % 16.51/16.72 (assume @p221 (forall (@list @t51 @t115 @t58 @t50 @t55 @t54 @t73) (or @t200 (not (tptp.c_WellTypeRT_OWTrt @t51 @t115 @t58 @t56 @t73))))) % 16.51/16.72 (assume @p222 (forall @t201 (= (tptp.c_Expr_Oexp_Oexp__case @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 (tptp.c_Expr_Oexp_OWhile @t17 @t16 @t68) @t1 @t68) (tptp.hAPP (tptp.hAPP @t93 @t17) @t16)))) % 16.51/16.72 (assume @p223 (forall @t129 (not (= @t31 @t19)))) % 16.51/16.72 (assume @p224 (forall (@list @t17 @t37 @t16 @t1 @t7 @t6 @t5) (not (= @t38 @t8)))) % 16.51/16.72 (assume @p225 (forall (@list @t32 @t1 @t22) (not (= @t33 @t27)))) % 16.51/16.72 (assume @p226 (forall (@list @t122 @t50 @t1 @t77) (or @t202 @t185))) % 16.51/16.72 (assume @p227 (forall (@list @t50 @t77 @t1 @t122) (or @t78 (not @t202)))) % 16.51/16.72 (assume @p228 (forall (@list @t12 @t85 @t22 @t1 @t20 @t2) (not (= @t86 @t21)))) % 16.51/16.72 (assume @p229 (forall @t203 (not (= @t39 @t45)))) % 16.51/16.72 (assume @p230 (forall (@list @t22 @t1 @t3) (not (= @t27 @t39)))) % 16.51/16.72 (assume @p231 (forall @t204 (not (= @t33 @t23)))) % 16.51/16.72 (assume @p232 (forall @t132 (not (= @t4 @t45)))) % 16.51/16.72 (assume @p233 (forall (@list @t32 @t1 @t12 @t85 @t22) (not (= @t33 @t86)))) % 16.51/16.72 (assume @p234 (forall @t201 (= (tptp.c_Expr_Oexp_Oexp__case @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 (tptp.c_Expr_Oexp_OSeq @t17 @t16 @t68) @t1 @t68) (tptp.hAPP (tptp.hAPP @t95 @t17) @t16)))) % 16.51/16.72 (assume @p235 (forall @t130 (not (= @t45 @t39)))) % 16.51/16.72 (assume @p236 (forall @t208 (or @t207 @t167))) % 16.51/16.72 (assume @p237 (forall @t208 (or @t207 (= @t206 @t205)))) % 16.51/16.72 (assume @p238 (forall (@list @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 @t17 @t16 @t15 @t68 @t1) (= (tptp.c_Expr_Oexp_Oexp__case @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 (tptp.c_Expr_Oexp_OCond @t17 @t16 @t15 @t68) @t1 @t68) (tptp.hAPP (tptp.hAPP (tptp.hAPP @t94 @t17) @t16) @t15)))) % 16.51/16.72 (assume @p239 (forall (@list @t83 @t1 @t3 @t2) (not (= @t84 @t4)))) % 16.51/16.72 (assume @p240 (forall (@list @t32 @t1 @t7 @t13 @t12 @t6) (not (= @t33 @t14)))) % 16.51/16.72 (assume @p241 (forall (@list @t51 @t58 @t55 @t54 @t159 @t154) (or (tptp.c_WellType_OWT @t51 @t58 @t195 @t159) @t193 @t192))) % 16.51/16.72 (assume @p242 (forall @t135 (not (= @t27 @t41)))) % 16.51/16.72 (assume @p243 (forall @t210 (or @t209 @t26))) % 16.51/16.72 (assume @p244 (forall @t210 (or @t209 (= @t89 @t85)))) % 16.51/16.72 (assume @p245 (forall @t210 (or @t209 @t167))) % 16.51/16.72 (assume @p246 (forall @t212 (or @t211 (= @t15 @t5)))) % 16.51/16.72 (assume @p247 (forall @t212 (or @t211 @t109))) % 16.51/16.72 (assume @p248 (forall @t212 (or @t211 @t112))) % 16.51/16.72 (assume @p249 (forall (@list @t3 @t2 @t1 @t12 @t22) (not (= @t4 @t43)))) % 16.51/16.72 (assume @p250 (forall (@list @t50 @t1 @t77) (or @t213 @t185))) % 16.51/16.72 (assume @p251 (forall (@list @t50 @t77 @t1) (or @t78 (not @t213)))) % 16.51/16.72 (assume @p252 (forall (@list @t32 @t1 @t7 @t10 @t9 @t6) (not (= @t33 @t11)))) % 16.51/16.72 (assume @p253 (forall (@list @t20 @t89 @t2 @t1 @t7 @t13 @t12 @t6) (not (= @t113 @t14)))) % 16.51/16.72 (assume @p254 (forall @t215 (or @t214 @t109))) % 16.51/16.72 (assume @p255 (forall @t215 (or @t214 @t167))) % 16.51/16.72 (assume @p256 (forall @t215 (or @t214 @t165))) % 16.51/16.72 (assume @p257 (forall @t215 (or @t214 @t112))) % 16.51/16.72 (assume @p258 (forall @t216 (tptp.c_List_Olist__all2 @t141 @t57 @t57 @t1 @t1))) % 16.51/16.72 (assume @p259 (forall (@list @t7 @t6 @t5 @t1 @t20 @t2) (not (= @t8 @t21)))) % 16.51/16.72 (assume @p260 (forall (@list @t55 @t77 @t1 @t122 @t121 @t54) (or @t80 (not (tptp.c_DefAss_O_092_060D_062 (tptp.c_Expr_Oexp_OTryCatch @t55 @t122 @t121 @t54 @t1) @t77 @t1))))) % 16.51/16.72 (assume @p261 (forall @t218 (or @t217 @t109))) % 16.51/16.72 (assume @p262 (forall @t218 (or @t217 (= @t37 @t34)))) % 16.51/16.72 (assume @p263 (forall @t218 (or @t217 @t112))) % 16.51/16.72 (assume @p264 (forall (@list @t7 @t13 @t12 @t6 @t1 @t20 @t2) (not (= @t14 @t21)))) % 16.51/16.72 (assume @p265 (forall (@list @t12 @t1 @t17 @t37 @t16) (not (= @t36 @t38)))) % 16.51/16.72 (assume @p266 (forall @t219 (not (= @t19 @t87)))) % 16.51/16.72 (assume @p267 (forall (@list @t151 @t1 @t77) (tptp.c_DefAss_O_092_060D_062 (tptp.c_Expr_Oexp_OVal @t151 @t1) @t77 @t1))) % 16.51/16.72 (assume @p268 (forall @t220 (not (= @t23 @t38)))) % 16.51/16.72 (assume @p269 (forall @t128 (not (= @t33 @t45)))) % 16.51/16.72 (assume @p270 (forall @t42 (not (= @t14 @t25)))) % 16.51/16.72 (assume @p271 (forall @t219 (not (= @t45 @t87)))) % 16.51/16.72 (assume @p272 (forall @t189 (not (= @t25 @t14)))) % 16.51/16.72 (assume @p273 (forall (@list @t55 @t77 @t1 @t54) (or @t80 (not (tptp.c_DefAss_O_092_060D_062 (tptp.c_Expr_Oexp_OSeq @t55 @t54 @t1) @t77 @t1))))) % 16.51/16.72 (assume @p274 (forall (@list @t32 @t1 @t83) (or (not (= @t33 @t84)) (= @t32 @t83)))) % 16.51/16.72 (assume @p275 (forall @t203 (not (= @t39 @t19)))) % 16.51/16.72 (assume @p276 (forall @t219 (not (= @t45 @t221)))) % 16.51/16.72 (assume @p277 (forall @t219 (not (= @t19 @t221)))) % 16.51/16.72 (assume @p278 (forall @t174 (not (= @t222 @t39)))) % 16.51/16.72 (assume @p279 (forall @t227 (or (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t226 @t225) @t73)) @t224 @t223))) % 16.51/16.72 (assume @p280 (forall @t124 (not (= @t221 @t14)))) % 16.51/16.72 (assume @p281 (forall @t204 (not (= @t33 @t222)))) % 16.51/16.72 (assume @p282 (forall (@list @t50 @t77 @t1 @t228 @t146) (or @t78 (not (tptp.c_DefAss_O_092_060D_062 (tptp.c_Expr_Oexp_OCall @t50 @t228 @t146 @t1) @t77 @t1))))) % 16.51/16.72 (assume @p283 (forall @t227 (or (tptp.c_WellTypeRT_OWTrt tptp.v_P tptp.v_h_Ha____ @t58 tptp.v_e_Ha____ @t225) @t224 @t223))) % 16.51/16.72 (assume @p284 (forall @t107 (not (= @t87 @t222)))) % 16.51/16.72 (assume @p285 (forall @t196 (or (tptp.c_WellTypeRT_OWTrt @t51 @t115 @t58 @t195 @t159) @t230 @t229))) % 16.51/16.72 (assume @p286 (forall (@list @t17 @t30 @t29 @t16 @t1 @t22 @t10 @t9) (not (= @t31 @t222)))) % 16.51/16.72 (assume @p287 @t232) % 16.51/16.72 (assume @p288 (forall (@list @t51 @t50 @t228 @t146 @t49 @t48 @t47) (or (tptp.c_SmallStep_Oredp @t51 @t231 @t49 (tptp.c_Expr_Oexp_OCall @t48 @t228 @t146 @t53) @t47) @t52))) % 16.51/16.72 (assume @p289 (forall @t238 (or (tptp.c_WellTypeRT_OWTrt tptp.v_P tptp.v_h_Ha____ @t233 tptp.v_e_Ha____ @t237) @t236 @t234))) % 16.51/16.72 (assume @p290 (forall @t24 (not (= @t222 @t21)))) % 16.51/16.72 (assume @p291 (forall @t120 (or @t67 @t242 @t241 @t240 @t239))) % 16.51/16.72 (assume @p292 (forall (@list @t51 @t115 @t75 @t50 @t73 @t58) (or (tptp.c_WellTypeRT_OWTrt @t51 @t115 @t75 @t50 @t73) @t76 @t244))) % 16.51/16.72 (assume @p293 (forall @t44 (not (= @t38 @t222)))) % 16.51/16.72 (assume @p294 (forall @t166 (not (= @t221 @t8)))) % 16.51/16.72 (assume @p295 (forall @t175 (not (= @t221 @t86)))) % 16.51/16.72 (assume @p296 (forall @t88 (not (= @t221 @t45)))) % 16.51/16.72 (assume @p297 (forall @t246 (or @t245 @t244))) % 16.51/16.72 (assume @p298 (forall @t246 (or @t243 (not @t245)))) % 16.51/16.72 (assume @p299 (forall @t180 (not (= @t221 @t27)))) % 16.51/16.72 (assume @p300 (forall @t133 (not (= @t14 @t221)))) % 16.51/16.72 (assume @p301 (forall @t134 (not (= @t8 @t221)))) % 16.51/16.72 (assume @p302 (forall @t136 (not (= @t21 @t222)))) % 16.51/16.72 (assume @p303 (forall @t227 (or (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t226 @t247) @t73)) @t224 @t223))) % 16.51/16.72 (assume @p304 (forall @t220 (not (= @t222 @t38)))) % 16.51/16.72 (assume @p305 (forall @t137 (= (tptp.c_Expr_Oexp_Oexp__case @t104 @t103 @t102 @t101 @t100 @t99 @t98 @t97 @t96 @t90 @t95 @t94 @t93 @t92 @t91 (tptp.c_Expr_Oexp_OCall @t2 @t30 @t29 @t68) @t1 @t68) (tptp.hAPP (tptp.hAPP (tptp.hAPP @t96 @t2) @t30) @t29)))) % 16.51/16.72 (assume @p306 (forall @t138 (not (= @t4 @t222)))) % 16.51/16.72 (assume @p307 (tptp.c_WellTypeRT_OWTrts tptp.v_P tptp.v_ha____ tptp.v_E____ tptp.v_esa____ tptp.v_Ts____)) % 16.51/16.72 (assume @p308 (forall (@list @t51 @t122 @t58 @t73 @t121 @t55 @t54 @t115) (or (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t65 @t170) @t73)) @t169))) % 16.51/16.72 (assume @p309 (forall @t107 (or @t248 @t26))) % 16.51/16.72 (assume @p310 (forall @t107 (or @t248 @t108))) % 16.51/16.72 (assume @p311 (forall @t107 (or @t248 @t105))) % 16.51/16.72 (assume @p312 (forall (@list @t51 @t1 @t73) (tptp.hBOOL (tptp.hAPP @t250 @t73)))) % 16.51/16.72 (assume @p313 (forall (@list @t51 @t1 @t252 @t73 @t251) (or (tptp.hBOOL (tptp.hAPP @t253 @t73)) (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t249 @t251) @t73))) (not (tptp.hBOOL (tptp.hAPP @t253 @t251)))))) % 16.51/16.72 (assume @p314 (forall (@list @t51 @t115 @t151 @t254 @t1 @t73) (or (tptp.c_Conform_Oconf @t51 @t115 @t151 @t254 @t1) (not (tptp.hBOOL (tptp.hAPP @t250 @t254))) @t152))) % 16.51/16.72 (assume @p315 (forall @t238 (or (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t226 @t237) @t235)) @t236 @t234))) % 16.51/16.72 (assume @p316 (forall @t144 (not (= @t86 @t221)))) % 16.51/16.72 (assume @p317 (forall @t246 (or @t243 @t74))) % 16.51/16.72 (assume @p318 (forall (@list @t51 @t148 @t58 @t50 @t73 @t115) (or (tptp.c_WellTypeRT_OWTrt @t51 @t148 @t58 @t50 @t73) @t149 @t244))) % 16.51/16.72 (assume @p319 (forall @t153 (not (= @t126 @t222)))) % 16.51/16.72 (assume @p320 (forall @t164 (not (= @t27 @t221)))) % 16.51/16.72 (assume @p321 (forall @t163 (or @t162 @t161 @t230 @t241 @t240 @t239))) % 16.51/16.72 (assume @p322 (forall @t158 (or @t157 @t242 @t229 @t240 @t239 @t155))) % 16.51/16.72 (assume @p323 (forall @t168 (not (= @t39 @t222)))) % 16.51/16.72 (assume @p324 (forall @t88 (not (= @t221 @t19)))) % 16.51/16.72 (assume @p325 (forall @t142 (not (= @t222 @t126)))) % 16.51/16.72 (assume @p326 (forall @t143 (not (= @t222 @t33)))) % 16.51/16.72 (assume @p327 (= (tptp.c_COMBI tptp.v_P tptp.t_a) tptp.v_P)) % 16.51/16.72 (assume @p328 (forall (@list @t22 @t10 @t9 @t1 @t17 @t30 @t29 @t16) (not (= @t222 @t31)))) % 16.51/16.72 (assume @p329 (tptp.c_WellTypeRT_OWTrt tptp.v_P tptp.v_ha____ tptp.v_E____ (tptp.c_Expr_Oexp_OCall tptp.v_ea____ tptp.v_M____ tptp.v_esa____ @t53) tptp.v_T____)) % 16.51/16.72 (assume @p330 (forall @t194 (not (= @t222 @t4)))) % 16.51/16.72 (assume @p331 (forall @t227 (or (tptp.c_WellTypeRT_OWTrt tptp.v_P tptp.v_h_Ha____ @t58 tptp.v_e_Ha____ @t247) @t224 @t223))) % 16.51/16.72 (assume @p332 (forall (@list @t51 @t1 @t255 @t256 @t145) (or (tptp.c_List_Olist__all2 @t249 @t255 @t256 tptp.tc_Type_Oty tptp.tc_Type_Oty) (not (tptp.c_List_Olist__all2 @t249 @t145 @t256 tptp.tc_Type_Oty tptp.tc_Type_Oty)) (not (tptp.c_List_Olist__all2 @t249 @t255 @t145 tptp.tc_Type_Oty tptp.tc_Type_Oty))))) % 16.51/16.72 (assume @p333 (forall (@list @t51 @t1 @t140) (tptp.c_List_Olist__all2 @t249 @t140 @t140 tptp.tc_Type_Oty tptp.tc_Type_Oty))) % 16.51/16.72 (assume @p334 (forall (@list @t22 @t10 @t9 @t1 @t2 @t30 @t29) (not (= @t222 @t87)))) % 16.51/16.72 (assume @p335 @t257) % 16.51/16.72 (assume @p336 @t258) % 16.51/16.72 (assume @p337 (forall (@list @t57) (or (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t226 @t57) tptp.v_T____))) (not (tptp.c_WellTypeRT_OWTrt tptp.v_P tptp.v_h_Ha____ tptp.v_E____ @t259 @t57))))) % 16.51/16.72 (assume @p338 (forall @t216 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t141 @t57) @t57)))) % 16.51/16.72 (assume @p339 (forall (@list @t261 @t260 @t1) (or (= @t261 @t260) (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t141 @t261) @t260)))))) % 16.51/16.72 (step @p340 :rule instantiate :premises (@p337) :args ((@list tptp.v_T____))) % 16.51/16.72 (step @p341 :rule instantiate :premises (@p312) :args ((@list tptp.v_P @t64 tptp.v_T____))) % 16.51/16.72 (step @p342 :rule cnf_or_pos :args (@t266)) % 16.51/16.72 (step @p343 :rule reordering :premises (@p342) :args ((or @t265 @t263 (not @t266)))) % 16.51/16.72 (step @p344 :rule chain_m_resolution :premises (@p343 @p341 @p340) :args (@t263 (@list false false) (@list @t264 @t266))) % 16.51/16.72 (step @p345 :rule cnf_or_pos :args (@t269)) % 16.51/16.72 (step @p346 :rule reordering :premises (@p345) :args ((or @t268 @t267 @t262 @t270))) % 16.51/16.72 (step @p347 :rule chain_m_resolution :premises (@p346 @p335 @p336 @p344) :args (@t270 (@list false false true) (@list @t257 @t258 @t262))) % 16.51/16.72 (assume-push @p354 @t232) % 16.51/16.72 (step @p349 :rule instantiate :premises (@p287) :args ((@list tptp.v_P tptp.v_h_Ha____ tptp.v_E____ tptp.v_e_Ha____ tptp.v_M____ tptp.v_esa____ tptp.v_T____ tptp.v_Ts____))) % 16.51/16.72 (step-pop @p355 :rule scope :premises (@p349)) % 16.51/16.72 (step @p350 :rule process_scope :premises (@p355) :args (@t269)) % 16.51/16.72 (step @p352 :rule implies_elim :premises (@p350)) % 16.51/16.72 (step @p353 false :rule chain_m_resolution :premises (@p352 @p347 @p287) :args (false (@list true false) (@list @t269 @t232))) % 16.51/16.72 ) % 16.51/16.73 % SZS output end Proof % 16.51/16.73 % cvc5 exiting %------------------------------------------------------------------------------