%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : LCL788-1 : TPTP v9.3.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 : n027.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 11:23:51 AM UTC 2026 % Result : Unsatisfiable 0.31s 0.60s % Output : Proof 0.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL788-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.36 % Computer : n027.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sun Sep 6 00:22:28 UTC 2026 % 0.09/0.36 % CPUTime : % 0.18/0.49 %----Proving TF0_NAR, FOF, or CNF % 0.18/0.50 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.31/0.60 % SZS status Unsatisfiable % 0.31/0.60 % SZS output start Proof % 0.31/0.60 ( % 0.31/0.60 (declare-sort $$unsorted 0) % 0.31/0.60 (declare-const tptp.c_fequal (-> $$unsorted $$unsorted $$unsorted Bool)) % 0.31/0.60 (declare-const tptp.c_Type_Otype_Otype__rec (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.60 (declare-const tptp.c_Type_Osko__Type__Xtype__induct__1__1 (-> $$unsorted $$unsorted)) % 0.31/0.60 (declare-const tptp.t_a $$unsorted) % 0.31/0.60 (declare-const tptp.c_Type_Otype_OAtom (-> $$unsorted $$unsorted)) % 0.31/0.60 (declare-const tptp.c_Lambda_OdB_OVar (-> $$unsorted $$unsorted)) % 0.31/0.60 (declare-const tptp.c_ListOrder_Ostep1 (-> $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 0.31/0.60 (declare-const tptp.c_List_OdropWhile (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.60 (declare-const tptp.c_List_Ofoldl (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.60 (declare-const tptp.c_Lambda_OdB_OApp $$unsorted) % 0.31/0.60 (declare-const tptp.c_Type_Otype_Otype__case (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.60 (declare-const tptp.c_List_Olistsp (-> $$unsorted $$unsorted $$unsorted Bool)) % 0.31/0.60 (declare-const tptp.c_Type_Otyping (-> $$unsorted $$unsorted $$unsorted Bool)) % 0.31/0.61 (declare-const tptp.tc_nat $$unsorted) % 0.31/0.61 (declare-const tptp.c_Lambda_Osubst (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_Type_Osko__Type__Xtypes__snocE__1__2 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_Type_Osko__Type__Xlist__app__typeD__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_HOL_Ozero__class_Ozero (-> $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.hAPP (-> $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.v_T____ $$unsorted) % 0.31/0.61 (declare-const tptp.tc_Lambda_OdB $$unsorted) % 0.31/0.61 (declare-const tptp.c_List_OtakeWhile (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.tc_Type_Otype $$unsorted) % 0.31/0.61 (declare-const tptp.c_List_Osplice (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_InductTermi_OIT $$unsorted) % 0.31/0.61 (declare-const tptp.c_List_Olist_OCons (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_Type_Oshift (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_List_Olist_ONil (-> $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.v_ea______ $$unsorted) % 0.31/0.61 (declare-const tptp.v_ua______ $$unsorted) % 0.31/0.61 (declare-const tptp.c_Type_Otypings (-> $$unsorted $$unsorted $$unsorted Bool)) % 0.31/0.61 (declare-const tptp.c_List_Osko__List__Xsplit__list__first__prop__iff__1__5 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_List_Olast (-> $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.v_T_H_H____ $$unsorted) % 0.31/0.61 (declare-const tptp.c_List_Oappend (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_Type_Osko__Type__Xtyping__elims__2__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.hBOOL (-> $$unsorted Bool)) % 0.31/0.61 (declare-const tptp.c_Lambda_OdB_OAbs (-> $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.v_u____ $$unsorted) % 0.31/0.61 (declare-const tptp.v_e____ $$unsorted) % 0.31/0.61 (declare-const tptp.c_List_Oreplicate (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_Type_Otype_OFun $$unsorted) % 0.31/0.61 (declare-const tptp.c_List_Osko__List__XCons__eq__append__conv__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_List_Osko__List__Xappend__eq__Cons__conv__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_List_Osko__List__Xsplit__list__last__prop__iff__1__5 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_List_Obutlast (-> $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.v_i____ $$unsorted) % 0.31/0.61 (declare-const tptp.c_Type_Osko__Type__Xvar__app__types__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_Type_Osko__Type__Xvar__app__typesE__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_Lambda_Olift (-> $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_List_Ofoldr (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.v_T_Ha______ $$unsorted) % 0.31/0.61 (declare-const tptp.c_List_Otl (-> $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.v_a____ $$unsorted) % 0.31/0.61 (declare-const tptp.v_rs____ $$unsorted) % 0.31/0.61 (declare-const tptp.v_n____ $$unsorted) % 0.31/0.61 (declare-const tptp.c_List_Ohd (-> $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_List_Oconcat__map (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_COMBC (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.c_List_Orotate1 (-> $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.v_ia______ $$unsorted) % 0.31/0.61 (declare-const tptp.c_Type_Osko__Type__Xlist__app__typeE__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.v_as____ $$unsorted) % 0.31/0.61 (declare-const tptp.c_List_Orev (-> $$unsorted $$unsorted $$unsorted)) % 0.31/0.61 (declare-const tptp.v_Ts____ $$unsorted) % 0.31/0.61 (declare-const tptp.v_T_H____ $$unsorted) % 0.31/0.61 (define @t1 () (tptp.c_HOL_Ozero__class_Ozero tptp.tc_nat)) % 0.31/0.61 (define @t2 () (@var "V_n" $$unsorted)) % 0.31/0.61 (define @t3 () (= @t2 @t1)) % 0.31/0.61 (define @t4 () (@var "T_a" $$unsorted)) % 0.31/0.61 (define @t5 () (@var "V_x" $$unsorted)) % 0.31/0.61 (define @t6 () (tptp.c_List_Oreplicate @t2 @t5 @t4)) % 0.31/0.61 (define @t7 () (tptp.c_List_Olist_ONil @t4)) % 0.31/0.61 (define @t8 () (@list @t2 @t5 @t4)) % 0.31/0.61 (define @t9 () (tptp.c_List_Oreplicate @t1 @t5 @t4)) % 0.31/0.61 (define @t10 () (@var "V_Ts" $$unsorted)) % 0.31/0.61 (define @t11 () (tptp.c_List_Olist_ONil tptp.tc_Lambda_OdB)) % 0.31/0.61 (define @t12 () (@var "V_t" $$unsorted)) % 0.31/0.61 (define @t13 () (@var "V_ts" $$unsorted)) % 0.31/0.61 (define @t14 () (@var "V_e" $$unsorted)) % 0.31/0.61 (define @t15 () (@var "V_y" $$unsorted)) % 0.31/0.61 (define @t16 () (@list @t5 @t4)) % 0.31/0.61 (define @t17 () (@var "V_m" $$unsorted)) % 0.31/0.61 (define @t18 () (= @t5 @t15)) % 0.31/0.61 (define @t19 () (not (= (tptp.c_List_Oreplicate @t17 @t5 @t4) (tptp.c_List_Oreplicate @t2 @t15 @t4)))) % 0.31/0.61 (define @t20 () (@list @t17 @t5 @t4 @t2 @t15)) % 0.31/0.61 (define @t21 () (@var "V_r" $$unsorted)) % 0.31/0.61 (define @t22 () (tptp.c_Lambda_OdB_OAbs @t21)) % 0.31/0.61 (define @t23 () (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t22 @t11 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB)) % 0.31/0.61 (define @t24 () (@list @t21)) % 0.31/0.61 (define @t25 () (not (tptp.hBOOL (tptp.hAPP tptp.c_InductTermi_OIT @t21)))) % 0.31/0.61 (define @t26 () (@var "V_ss" $$unsorted)) % 0.31/0.61 (define @t27 () (= @t26 @t11)) % 0.31/0.61 (define @t28 () (@var "V_s" $$unsorted)) % 0.31/0.61 (define @t29 () (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t28 @t26 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB)) % 0.31/0.61 (define @t30 () (not (= @t29 @t22))) % 0.31/0.61 (define @t31 () (@list @t28 @t26 @t21)) % 0.31/0.61 (define @t32 () (@var "V_xs" $$unsorted)) % 0.31/0.61 (define @t33 () (@var "V_P" $$unsorted)) % 0.31/0.61 (define @t34 () (tptp.c_List_OdropWhile @t33 @t32 @t4)) % 0.31/0.61 (define @t35 () (@list @t33 @t32 @t4)) % 0.31/0.61 (define @t36 () (not (= @t22 @t29))) % 0.31/0.61 (define @t37 () (@list @t21 @t28 @t26)) % 0.31/0.61 (define @t38 () (@var "V_Q" $$unsorted)) % 0.31/0.61 (define @t39 () (@var "V_R" $$unsorted)) % 0.31/0.61 (define @t40 () (@var "T_c" $$unsorted)) % 0.31/0.61 (define @t41 () (@var "T_b" $$unsorted)) % 0.31/0.61 (define @t42 () (@var "V_ys" $$unsorted)) % 0.31/0.61 (define @t43 () (tptp.c_List_Oappend @t32 @t42 @t4)) % 0.31/0.61 (define @t44 () (@var "V_A" $$unsorted)) % 0.31/0.61 (define @t45 () (tptp.c_List_Olistsp @t44 @t43 @t4)) % 0.31/0.61 (define @t46 () (not @t45)) % 0.31/0.61 (define @t47 () (tptp.c_List_Olistsp @t44 @t32 @t4)) % 0.31/0.61 (define @t48 () (tptp.c_List_Olistsp @t44 @t42 @t4)) % 0.31/0.61 (define @t49 () (@list @t33 @t4)) % 0.31/0.61 (define @t50 () (tptp.hBOOL (tptp.hAPP @t33 @t15))) % 0.31/0.61 (define @t51 () (tptp.c_List_Olist_OCons @t15 @t42 @t4)) % 0.31/0.61 (define @t52 () (= @t34 @t51)) % 0.31/0.61 (define @t53 () (not @t52)) % 0.31/0.61 (define @t54 () (@list @t33 @t32 @t4 @t15 @t42)) % 0.31/0.61 (define @t55 () (@var "V_dB_H" $$unsorted)) % 0.31/0.61 (define @t56 () (tptp.c_Lambda_OdB_OAbs @t55)) % 0.31/0.61 (define @t57 () (@var "V_nat" $$unsorted)) % 0.31/0.61 (define @t58 () (tptp.c_Lambda_OdB_OVar @t57)) % 0.31/0.61 (define @t59 () (@var "V_dB" $$unsorted)) % 0.31/0.61 (define @t60 () (tptp.c_List_Olist_OCons @t5 @t32 @t4)) % 0.31/0.61 (define @t61 () (tptp.c_List_Olist_OCons @t28 @t11 tptp.tc_Lambda_OdB)) % 0.31/0.61 (define @t62 () (@var "V_xa" $$unsorted)) % 0.31/0.61 (define @t63 () (tptp.hAPP (tptp.hAPP tptp.c_Lambda_OdB_OApp @t21) @t28)) % 0.31/0.61 (define @t64 () (tptp.hBOOL (tptp.hAPP @t33 @t5))) % 0.31/0.61 (define @t65 () (not @t64)) % 0.31/0.61 (define @t66 () (tptp.c_List_OdropWhile @t33 @t60 @t4)) % 0.31/0.61 (define @t67 () (@list @t33 @t5 @t32 @t4)) % 0.31/0.61 (define @t68 () (@var "V_rs" $$unsorted)) % 0.31/0.61 (define @t69 () (= @t68 @t26)) % 0.31/0.61 (define @t70 () (tptp.c_Lambda_OdB_OAbs @t28)) % 0.31/0.61 (define @t71 () (not (= (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t22 @t68 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB) (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t70 @t26 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB)))) % 0.31/0.61 (define @t72 () (@list @t21 @t68 @t28 @t26)) % 0.31/0.61 (define @t73 () (= @t21 @t28)) % 0.31/0.61 (define @t74 () (tptp.c_List_OtakeWhile @t33 @t32 @t4)) % 0.31/0.61 (define @t75 () (@list @t4 @t42)) % 0.31/0.61 (define @t76 () (@list @t32 @t4)) % 0.31/0.61 (define @t77 () (@var "V_dB2" $$unsorted)) % 0.31/0.61 (define @t78 () (@var "V_dB1" $$unsorted)) % 0.31/0.61 (define @t79 () (tptp.hAPP (tptp.hAPP tptp.c_Lambda_OdB_OApp @t78) @t77)) % 0.31/0.61 (define @t80 () (@var "V_u" $$unsorted)) % 0.31/0.61 (define @t81 () (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t12 @t13 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB)) % 0.31/0.61 (define @t82 () (tptp.c_List_Oappend @t5 @t61 tptp.tc_Lambda_OdB)) % 0.31/0.61 (define @t83 () (@var "V_U" $$unsorted)) % 0.31/0.61 (define @t84 () (@var "V_T" $$unsorted)) % 0.31/0.61 (define @t85 () (@var "V_env" $$unsorted)) % 0.31/0.61 (define @t86 () (tptp.hAPP (tptp.hAPP tptp.c_Type_Otype_OFun @t84) @t83)) % 0.31/0.61 (define @t87 () (@list @t5 @t32 @t4)) % 0.31/0.61 (define @t88 () (@var "V_zs" $$unsorted)) % 0.31/0.61 (define @t89 () (= @t60 @t88)) % 0.31/0.61 (define @t90 () (tptp.c_List_Osko__List__XCons__eq__append__conv__1__1 @t5 @t32 @t42 @t88 @t4)) % 0.31/0.61 (define @t91 () (= (tptp.c_List_Olist_OCons @t5 @t90 @t4) @t42)) % 0.31/0.61 (define @t92 () (tptp.c_List_Oappend @t42 @t88 @t4)) % 0.31/0.61 (define @t93 () (not (= @t60 @t92))) % 0.31/0.61 (define @t94 () (@list @t5 @t32 @t4 @t42 @t88)) % 0.31/0.61 (define @t95 () (= @t88 @t60)) % 0.31/0.61 (define @t96 () (tptp.c_List_Osko__List__Xappend__eq__Cons__conv__1__1 @t5 @t32 @t42 @t88 @t4)) % 0.31/0.61 (define @t97 () (= (tptp.c_List_Oappend @t96 @t88 @t4) @t32)) % 0.31/0.61 (define @t98 () (not (= @t92 @t60))) % 0.31/0.61 (define @t99 () (@list @t42 @t88 @t4 @t5 @t32)) % 0.31/0.61 (define @t100 () (= @t32 @t7)) % 0.31/0.61 (define @t101 () (tptp.c_List_Obutlast @t32 @t4)) % 0.31/0.61 (define @t102 () (tptp.c_List_Olist_OCons @t5 @t7 @t4)) % 0.31/0.61 (define @t103 () (= @t32 @t102)) % 0.31/0.61 (define @t104 () (tptp.c_List_Orev @t32 @t4)) % 0.31/0.61 (define @t105 () (tptp.c_List_OtakeWhile @t33 @t60 @t4)) % 0.31/0.61 (define @t106 () (tptp.c_List_Orev @t102 @t4)) % 0.31/0.61 (define @t107 () (tptp.c_List_Olast @t32 @t4)) % 0.31/0.61 (define @t108 () (@var "V_us" $$unsorted)) % 0.31/0.61 (define @t109 () (@var "V_i" $$unsorted)) % 0.31/0.61 (define @t110 () (tptp.c_Lambda_OdB_OVar @t109)) % 0.31/0.61 (define @t111 () (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t110 @t13 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB)) % 0.31/0.61 (define @t112 () (not (tptp.c_Type_Otyping @t14 (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t111 @t108 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB) @t84))) % 0.31/0.61 (define @t113 () (not (tptp.c_Type_Otypings @t14 @t13 @t10))) % 0.31/0.61 (define @t114 () (not (tptp.c_Type_Otyping @t14 @t111 @t83))) % 0.31/0.61 (define @t115 () (tptp.c_Type_Osko__Type__Xvar__app__types__1__1 @t84 @t83 @t14 @t108)) % 0.31/0.61 (define @t116 () (tptp.c_Lambda_OdB_OVar tptp.v_n____)) % 0.31/0.61 (define @t117 () (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t116 tptp.v_rs____ tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB)) % 0.31/0.61 (define @t118 () (@var "V_k" $$unsorted)) % 0.31/0.61 (define @t119 () (tptp.hAPP tptp.c_Lambda_OdB_OApp @t12)) % 0.31/0.61 (define @t120 () (tptp.hAPP @t119 @t80)) % 0.31/0.61 (define @t121 () (tptp.c_List_Orev @t7 @t4)) % 0.31/0.61 (define @t122 () (@list @t4)) % 0.31/0.61 (define @t123 () (not (tptp.c_Type_Otyping @t14 @t111 @t84))) % 0.31/0.61 (define @t124 () (tptp.c_Type_Osko__Type__Xvar__app__typesE__1__1 @t84 @t14 @t109 @t13)) % 0.31/0.61 (define @t125 () (tptp.c_ListOrder_Ostep1 @t21 @t42 @t32 @t4)) % 0.31/0.61 (define @t126 () (not @t125)) % 0.31/0.61 (define @t127 () (not (tptp.c_ListOrder_Ostep1 @t21 @t51 @t60 @t4))) % 0.31/0.61 (define @t128 () (tptp.hAPP @t21 @t15)) % 0.31/0.61 (define @t129 () (tptp.hBOOL (tptp.hAPP @t128 @t5))) % 0.31/0.61 (define @t130 () (@list @t21 @t42 @t32 @t4 @t15 @t5)) % 0.31/0.61 (define @t131 () (@var "V_j" $$unsorted)) % 0.31/0.61 (define @t132 () (tptp.c_Type_Otyping @t14 @t81 @t84)) % 0.31/0.61 (define @t133 () (not @t132)) % 0.31/0.61 (define @t134 () (tptp.c_Type_Osko__Type__Xlist__app__typeD__1__1 @t84 @t14 @t12 @t13)) % 0.31/0.61 (define @t135 () (@list @t14 @t13 @t84 @t12)) % 0.31/0.61 (define @t136 () (tptp.c_List_Orev @t32 @t41)) % 0.31/0.61 (define @t137 () (@var "V_a" $$unsorted)) % 0.31/0.61 (define @t138 () (@var "V_f" $$unsorted)) % 0.31/0.61 (define @t139 () (tptp.c_List_Ofoldr @t138 @t32 @t137 @t41 @t4)) % 0.31/0.61 (define @t140 () (= @t32 @t42)) % 0.31/0.61 (define @t141 () (tptp.c_List_Orev @t42 @t4)) % 0.31/0.61 (define @t142 () (tptp.c_List_Olist_ONil @t41)) % 0.31/0.61 (define @t143 () (tptp.c_Lambda_OdB_OVar @t2)) % 0.31/0.61 (define @t144 () (tptp.c_List_Oreplicate @t118 @t5 @t4)) % 0.31/0.61 (define @t145 () (= @t42 @t7)) % 0.31/0.61 (define @t146 () (tptp.c_List_Ohd @t42 @t4)) % 0.31/0.61 (define @t147 () (@list @t5 @t32 @t4 @t42)) % 0.31/0.61 (define @t148 () (= @t32 (tptp.c_List_Oappend @t74 @t51 @t4))) % 0.31/0.61 (define @t149 () (not (tptp.hBOOL (tptp.hAPP tptp.c_InductTermi_OIT @t12)))) % 0.31/0.61 (define @t150 () (tptp.c_Lambda_Olift @t12 @t109)) % 0.31/0.61 (define @t151 () (@list @t12 @t109)) % 0.31/0.61 (define @t152 () (tptp.c_Lambda_Olift @t12 @t118)) % 0.31/0.61 (define @t153 () (tptp.hAPP (tptp.hAPP tptp.c_Lambda_OdB_OApp @t28) @t12)) % 0.31/0.61 (define @t154 () (tptp.c_List_Orev @t104 @t4)) % 0.31/0.61 (define @t155 () (@list @t42 @t4)) % 0.31/0.61 (define @t156 () (tptp.c_List_Orotate1 @t32 @t4)) % 0.31/0.61 (define @t157 () (= @t17 @t2)) % 0.31/0.61 (define @t158 () (tptp.c_List_Ohd @t32 @t4)) % 0.31/0.61 (define @t159 () (@var "V_vs" $$unsorted)) % 0.31/0.61 (define @t160 () (tptp.c_List_Oappend @t32 @t5 @t4)) % 0.31/0.61 (define @t161 () (tptp.c_Lambda_OdB_OVar @t17)) % 0.31/0.61 (define @t162 () (tptp.c_Type_Osko__Type__Xlist__app__typeE__1__1 @t84 @t14 @t12 @t13)) % 0.31/0.61 (define @t163 () (tptp.c_List_Olist_OCons @t5 @t32 @t41)) % 0.31/0.61 (define @t164 () (tptp.c_List_Otl @t32 @t4)) % 0.31/0.61 (define @t165 () (not (= @t161 @t29))) % 0.31/0.61 (define @t166 () (@list @t17 @t28 @t26)) % 0.31/0.61 (define @t167 () (tptp.c_List_Ofoldl @t138 @t137 @t32 @t4 @t41)) % 0.31/0.61 (define @t168 () (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t143 @t26 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB)) % 0.31/0.61 (define @t169 () (@list @t32 @t42 @t4)) % 0.31/0.61 (define @t170 () (tptp.c_List_Oappend @t32 @t42 @t41)) % 0.31/0.61 (define @t171 () (not (tptp.hBOOL (tptp.hAPP @t33 @t62)))) % 0.31/0.61 (define @t172 () (@var "V_xb" $$unsorted)) % 0.31/0.61 (define @t173 () (tptp.c_List_Oappend @t5 (tptp.c_List_Olist_OCons @t62 @t172 @t4) @t4)) % 0.31/0.61 (define @t174 () (@list @t33 @t5 @t62 @t172 @t4)) % 0.31/0.61 (define @t175 () (tptp.hAPP @t138 @t5)) % 0.31/0.61 (define @t176 () (@var "V_l" $$unsorted)) % 0.31/0.61 (define @t177 () (= @t42 (tptp.c_List_Olist_OCons @t5 @t96 @t4))) % 0.31/0.61 (define @t178 () (= @t32 (tptp.c_List_Oappend @t90 @t88 @t4))) % 0.31/0.61 (define @t179 () (tptp.c_List_Oappend @t32 @t7 @t4)) % 0.31/0.61 (define @t180 () (tptp.c_List_Oappend @t7 @t42 @t4)) % 0.31/0.61 (define @t181 () (not (= (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t161 @t68 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB) @t168))) % 0.31/0.61 (define @t182 () (@list @t17 @t68 @t2 @t26)) % 0.31/0.61 (define @t183 () (not (tptp.c_Type_Otyping @t14 @t120 @t84))) % 0.31/0.61 (define @t184 () (tptp.c_Type_Osko__Type__Xtyping__elims__2__1 @t84 @t14 @t12 @t80)) % 0.31/0.61 (define @t185 () (@list @t14 @t12 @t84 @t13)) % 0.31/0.61 (define @t186 () (tptp.c_Lambda_Osubst @t12 @t80 @t109)) % 0.31/0.61 (define @t187 () (@var "V_e_H" $$unsorted)) % 0.31/0.61 (define @t188 () (@var "V_Ta" $$unsorted)) % 0.31/0.61 (define @t189 () (@var "V_T1" $$unsorted)) % 0.31/0.61 (define @t190 () (not (tptp.hBOOL (tptp.hAPP tptp.c_InductTermi_OIT @t80)))) % 0.31/0.61 (define @t191 () (tptp.hBOOL (tptp.hAPP tptp.c_InductTermi_OIT @t186))) % 0.31/0.61 (define @t192 () (@var "V_T2" $$unsorted)) % 0.31/0.61 (define @t193 () (tptp.hAPP (tptp.hAPP tptp.c_Type_Otype_OFun @t189) @t192)) % 0.31/0.61 (define @t194 () (not (= tptp.v_T____ @t193))) % 0.31/0.61 (define @t195 () (@list @t189 @t192 @t12 @t80 @t109 @t14 @t188)) % 0.31/0.61 (define @t196 () (tptp.c_List_Oreplicate @t109 @t5 @t4)) % 0.31/0.61 (define @t197 () (tptp.c_List_Oappend @t32 @t102 @t4)) % 0.31/0.61 (define @t198 () (tptp.c_List_Olist_OCons @t15 @t7 @t4)) % 0.31/0.61 (define @t199 () (tptp.c_List_Oappend @t42 @t198 @t4)) % 0.31/0.61 (define @t200 () (not (tptp.c_ListOrder_Ostep1 @t21 @t199 @t197 @t4))) % 0.31/0.61 (define @t201 () (= @t42 @t32)) % 0.31/0.61 (define @t202 () (tptp.c_List_Oappend @t141 @t198 @t4)) % 0.31/0.61 (define @t203 () (= @t15 @t5)) % 0.31/0.61 (define @t204 () (@list @t32 @t5 @t4)) % 0.31/0.61 (define @t205 () (tptp.c_Type_Oshift tptp.v_e____ tptp.v_i____ tptp.v_T____ tptp.tc_Type_Otype)) % 0.31/0.61 (define @t206 () (@var "V_dB2_H" $$unsorted)) % 0.31/0.61 (define @t207 () (@var "V_dB1_H" $$unsorted)) % 0.31/0.61 (define @t208 () (tptp.hAPP (tptp.hAPP tptp.c_Lambda_OdB_OApp @t207) @t206)) % 0.31/0.61 (define @t209 () (@var "V_f1" $$unsorted)) % 0.31/0.61 (define @t210 () (tptp.hAPP @t209 @t57)) % 0.31/0.61 (define @t211 () (tptp.c_Type_Otype_OAtom @t57)) % 0.31/0.61 (define @t212 () (@var "V_f2" $$unsorted)) % 0.31/0.61 (define @t213 () (@list @t209 @t212 @t57 @t4)) % 0.31/0.61 (define @t214 () (tptp.c_List_Oappend @t7 @t7 @t4)) % 0.31/0.61 (define @t215 () (tptp.c_List_Oappend @t7 @t60 @t4)) % 0.31/0.61 (define @t216 () (@var "V_xc" $$unsorted)) % 0.31/0.61 (define @t217 () (@var "V_list_H" $$unsorted)) % 0.31/0.61 (define @t218 () (@var "V_a_H" $$unsorted)) % 0.31/0.61 (define @t219 () (tptp.c_List_Olist_OCons @t218 @t217 @t4)) % 0.31/0.61 (define @t220 () (tptp.c_List_Olist_OCons @t5 @t62 @t4)) % 0.31/0.61 (define @t221 () (@var "V_xs1" $$unsorted)) % 0.31/0.61 (define @t222 () (tptp.c_List_Oappend @t220 @t88 @t4)) % 0.31/0.61 (define @t223 () (tptp.c_List_Olist_OCons @t5 (tptp.c_List_Oappend @t62 @t88 @t4) @t4)) % 0.31/0.61 (define @t224 () (tptp.c_Type_Osko__Type__Xtype__induct__1__1 @t33)) % 0.31/0.61 (define @t225 () (tptp.hBOOL (tptp.hAPP @t33 @t84))) % 0.31/0.61 (define @t226 () (= @t42 @t88)) % 0.31/0.61 (define @t227 () (@list @t32 @t42 @t4 @t88)) % 0.31/0.61 (define @t228 () (@var "V_nat_H" $$unsorted)) % 0.31/0.61 (define @t229 () (= @t57 @t228)) % 0.31/0.61 (define @t230 () (@list @t57 @t228)) % 0.31/0.61 (define @t231 () (not (tptp.c_Type_Otyping @t14 @t110 @t84))) % 0.31/0.61 (define @t232 () (tptp.hAPP @t14 @t109)) % 0.31/0.61 (define @t233 () (or (= @t232 @t84) @t231)) % 0.31/0.61 (define @t234 () (forall (@list @t14 @t109 @t84) @t233)) % 0.31/0.61 (define @t235 () (= tptp.v_n____ tptp.v_i____)) % 0.31/0.61 (define @t236 () (tptp.hAPP (tptp.c_Type_Oshift @t14 @t5 @t84 @t4) @t5)) % 0.31/0.61 (define @t237 () (forall (@list @t14 @t5 @t84 @t4) (= @t236 @t84))) % 0.31/0.61 (define @t238 () (not (= @t7 @t43))) % 0.31/0.61 (define @t239 () (@list @t4 @t32 @t42)) % 0.31/0.61 (define @t240 () (not (= @t43 @t7))) % 0.31/0.61 (define @t241 () (not (= @t79 @t208))) % 0.31/0.61 (define @t242 () (@list @t78 @t77 @t207 @t206)) % 0.31/0.61 (define @t243 () (@var "V_list" $$unsorted)) % 0.31/0.61 (define @t244 () (not (= (tptp.c_List_Olist_OCons @t137 @t243 @t4) @t219))) % 0.31/0.61 (define @t245 () (@list @t137 @t243 @t4 @t218 @t217)) % 0.31/0.61 (define @t246 () (not (= @t197 @t199))) % 0.31/0.61 (define @t247 () (@list @t32 @t5 @t4 @t42 @t15)) % 0.31/0.61 (define @t248 () (@var "V_type2_H" $$unsorted)) % 0.31/0.61 (define @t249 () (@var "V_type1_H" $$unsorted)) % 0.31/0.61 (define @t250 () (tptp.hAPP (tptp.hAPP tptp.c_Type_Otype_OFun @t249) @t248)) % 0.31/0.61 (define @t251 () (@var "V_type1" $$unsorted)) % 0.31/0.61 (define @t252 () (@var "V_type2" $$unsorted)) % 0.31/0.61 (define @t253 () (tptp.hAPP (tptp.hAPP tptp.c_Type_Otype_OFun @t251) @t252)) % 0.31/0.61 (define @t254 () (not (= @t253 @t250))) % 0.31/0.61 (define @t255 () (@list @t251 @t252 @t249 @t248)) % 0.31/0.61 (define @t256 () (@var "V_T1a" $$unsorted)) % 0.31/0.61 (define @t257 () (tptp.c_List_Ofoldr tptp.c_Type_Otype_OFun tptp.v_Ts____ tptp.v_T_H____ tptp.tc_Type_Otype tptp.tc_Type_Otype)) % 0.31/0.61 (define @t258 () (tptp.hAPP (tptp.hAPP tptp.c_Type_Otype_OFun tptp.v_T_H_H____) @t257)) % 0.31/0.61 (define @t259 () (tptp.c_Type_Otyping @t205 @t116 @t258)) % 0.31/0.61 (define @t260 () (tptp.hAPP (tptp.hAPP @t212 @t251) @t252)) % 0.31/0.61 (define @t261 () (@list @t209 @t212 @t251 @t252 @t4)) % 0.31/0.61 (define @t262 () (= tptp.v_T____ @t258)) % 0.31/0.61 (define @t263 () (@var "V_Y" $$unsorted)) % 0.31/0.61 (define @t264 () (@var "V_X" $$unsorted)) % 0.31/0.61 (define @t265 () (not @t259)) % 0.31/0.61 (define @t266 () (= @t258 (tptp.hAPP @t205 tptp.v_n____))) % 0.31/0.61 (define @t267 () (or @t266 @t265)) % 0.31/0.61 (define @t268 () (tptp.hAPP @t205 tptp.v_i____)) % 0.31/0.61 (define @t269 () (= tptp.v_T____ @t268)) % 0.31/0.61 (define @t270 () (and @t235 @t266 @t269)) % 0.31/0.61 (assume @p1 (forall (@list @t4 @t2 @t5) (or (not (= @t7 @t6)) @t3))) % 0.31/0.61 (assume @p2 (forall @t8 (or (not (= @t6 @t7)) @t3))) % 0.31/0.61 (assume @p3 (forall (@list @t4 @t5) (= @t7 @t9))) % 0.31/0.61 (assume @p4 (forall @t8 (or (= (tptp.c_List_Ohd @t6 @t4) @t5) @t3))) % 0.31/0.61 (assume @p5 (tptp.hBOOL (tptp.hAPP tptp.c_InductTermi_OIT tptp.v_ua______))) % 0.31/0.61 (assume @p6 (forall (@list @t14 @t12 @t10 @t13) (or (tptp.c_Type_Otyping @t14 @t12 (tptp.c_Type_Osko__Type__Xtypes__snocE__1__2 @t10 @t14 @t12 @t13)) (not (tptp.c_Type_Otypings @t14 (tptp.c_List_Oappend @t13 (tptp.c_List_Olist_OCons @t12 @t11 tptp.tc_Lambda_OdB) tptp.tc_Lambda_OdB) @t10))))) % 0.31/0.61 (assume @p7 (forall @t8 (or (= (tptp.c_List_Olast @t6 @t4) @t5) @t3))) % 0.31/0.61 (assume @p8 (forall (@list @t5 @t4 @t15) (= @t9 (tptp.c_List_Oreplicate @t1 @t15 @t4)))) % 0.31/0.61 (assume @p9 (forall @t16 (= @t9 @t7))) % 0.31/0.61 (assume @p10 (forall @t20 (or @t19 @t18 (= @t17 @t1)))) % 0.31/0.61 (assume @p11 (forall @t24 (= @t23 @t22))) % 0.31/0.61 (assume @p12 (forall @t24 (or (tptp.hBOOL (tptp.hAPP tptp.c_InductTermi_OIT @t22)) @t25))) % 0.31/0.61 (assume @p13 (forall @t31 (or @t30 @t27))) % 0.31/0.61 (assume @p14 (forall @t35 (or (not (tptp.hBOOL (tptp.hAPP @t33 (tptp.c_List_Ohd @t34 @t4)))) (= @t34 @t7)))) % 0.31/0.61 (assume @p15 (forall @t37 (or @t36 (= @t22 @t28)))) % 0.31/0.61 (assume @p16 (forall @t24 (= @t22 @t23))) % 0.31/0.61 (assume @p17 (forall (@list @t33 @t41 @t40 @t4 @t38 @t39) (= (tptp.hAPP (tptp.hAPP (tptp.c_COMBC @t33 @t41 @t40 @t4) @t38) @t39) (tptp.hAPP (tptp.hAPP @t33 @t39) @t38)))) % 0.31/0.61 (assume @p18 (forall (@list @t44 @t32 @t4 @t42) (or @t47 @t46))) % 0.31/0.61 (assume @p19 (forall (@list @t44 @t42 @t4 @t32) (or @t48 @t46))) % 0.31/0.61 (assume @p20 (forall (@list @t44 @t4) (tptp.c_List_Olistsp @t44 @t7 @t4))) % 0.31/0.61 (assume @p21 (tptp.c_Type_Otyping tptp.v_ea______ tptp.v_ua______ tptp.v_T____)) % 0.31/0.61 (assume @p22 (forall @t49 (= (tptp.c_List_OdropWhile @t33 @t7 @t4) @t7))) % 0.31/0.61 (assume @p23 (forall @t54 (or @t53 (not @t50)))) % 0.31/0.61 (assume @p24 (forall (@list @t57 @t55) (not (= @t58 @t56)))) % 0.31/0.61 (assume @p25 (forall @t37 (or (tptp.hBOOL (tptp.hAPP tptp.c_InductTermi_OIT (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp (tptp.hAPP (tptp.hAPP tptp.c_Lambda_OdB_OApp @t22) @t28) @t26 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB))) (not (tptp.hBOOL (tptp.hAPP tptp.c_InductTermi_OIT @t28))) (not (tptp.hBOOL (tptp.hAPP tptp.c_InductTermi_OIT (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp (tptp.c_Lambda_Osubst @t21 @t28 @t1) @t26 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB))))))) % 0.31/0.61 (assume @p26 (forall (@list @t59 @t55) (or (not (= (tptp.c_Lambda_OdB_OAbs @t59) @t56)) (= @t59 @t55)))) % 0.31/0.61 (assume @p27 (forall (@list @t5 @t32 @t4 @t15 @t42) (= (tptp.c_List_Osplice @t60 @t51 @t4) (tptp.c_List_Olist_OCons @t5 (tptp.c_List_Olist_OCons @t15 (tptp.c_List_Osplice @t32 @t42 @t4) @t4) @t4)))) % 0.31/0.61 (assume @p28 (forall (@list @t21 @t28 @t62) (or (not (= @t21 (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t63 @t62 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB))) (= @t63 (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t63 (tptp.c_List_Oappend @t62 @t61 tptp.tc_Lambda_OdB) tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB))))) % 0.31/0.61 (assume @p29 (forall @t37 (or @t36 @t27))) % 0.31/0.61 (assume @p30 (forall @t67 (or (= @t66 @t34) @t65))) % 0.31/0.61 (assume @p31 (forall @t67 (or (= @t66 @t60) @t64))) % 0.31/0.61 (assume @p32 (forall @t72 (or @t71 @t69))) % 0.31/0.61 (assume @p33 (forall @t72 (or @t71 @t73))) % 0.31/0.61 (assume @p34 (forall @t31 (or @t30 (= @t28 @t22)))) % 0.31/0.61 (assume @p35 (forall (@list @t21 @t28 @t12) (or (not (= @t63 (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t12 @t11 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB))) (= @t63 @t12)))) % 0.31/0.61 (assume @p36 (forall @t35 (= (tptp.c_List_Oappend @t74 @t34 @t4) @t32))) % 0.31/0.61 (assume @p37 (forall (@list @t44 @t32 @t42 @t4) (or @t45 (not @t48) (not @t47)))) % 0.31/0.61 (assume @p38 (forall @t75 (= (tptp.c_List_Osplice @t7 @t42 @t4) @t42))) % 0.31/0.61 (assume @p39 (forall @t76 (= (tptp.c_List_Osplice @t32 @t7 @t4) @t32))) % 0.31/0.61 (assume @p40 (forall (@list @t55 @t78 @t77) (not (= @t56 @t79)))) % 0.31/0.61 (assume @p41 (forall (@list @t12 @t13 @t80) (= (tptp.hAPP (tptp.hAPP tptp.c_Lambda_OdB_OApp @t81) @t80) (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t12 (tptp.c_List_Oappend @t13 (tptp.c_List_Olist_OCons @t80 @t11 tptp.tc_Lambda_OdB) tptp.tc_Lambda_OdB) tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB)))) % 0.31/0.61 (assume @p42 (forall (@list @t78 @t77 @t55) (not (= @t79 @t56)))) % 0.31/0.61 (assume @p43 (forall (@list @t55 @t57) (not (= @t56 @t58)))) % 0.31/0.61 (assume @p44 (forall (@list @t21 @t28) (= @t63 (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t63 @t11 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB)))) % 0.31/0.61 (assume @p45 (forall (@list @t5 @t28 @t12) (or (= @t82 @t11) (= (tptp.hAPP (tptp.hAPP tptp.c_Lambda_OdB_OApp (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t12 @t5 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB)) @t28) (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t12 @t82 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB))))) % 0.31/0.61 (assume @p46 (forall (@list @t85 @t12 @t84 @t83) (or (tptp.c_Type_Otyping @t85 (tptp.c_Lambda_OdB_OAbs @t12) @t86) (not (tptp.c_Type_Otyping (tptp.c_Type_Oshift @t85 @t1 @t84 tptp.tc_Type_Otype) @t12 @t83))))) % 0.31/0.61 (assume @p47 (forall @t87 (= (tptp.c_List_Osplice @t60 @t7 @t4) @t60))) % 0.31/0.61 (assume @p48 (forall @t94 (or @t93 @t91 @t89))) % 0.31/0.61 (assume @p49 (forall @t99 (or @t98 @t97 @t95))) % 0.31/0.61 (assume @p50 (forall @t87 (or (= (tptp.c_List_Obutlast @t60 @t4) (tptp.c_List_Olist_OCons @t5 @t101 @t4)) @t100))) % 0.31/0.61 (assume @p51 (forall @t16 (= (tptp.c_List_Olast @t102 @t4) @t5))) % 0.31/0.61 (assume @p52 (forall @t16 (= (tptp.c_List_Obutlast @t102 @t4) @t7))) % 0.31/0.61 (assume @p53 (forall (@list @t32 @t4 @t5) (or (not (= @t104 @t102)) @t103))) % 0.31/0.61 (assume @p54 (forall @t67 (or (= @t105 @t7) @t64))) % 0.31/0.61 (assume @p55 (forall (@list @t5 @t4 @t32) (or (not (= @t102 @t104)) @t103))) % 0.31/0.61 (assume @p56 (forall @t16 (= @t106 @t102))) % 0.31/0.61 (assume @p57 (forall @t87 (or (= (tptp.c_List_Olast @t60 @t4) @t107) @t100))) % 0.31/0.61 (assume @p58 (forall @t16 (= @t102 @t106))) % 0.31/0.61 (assume @p59 (forall (@list @t83 @t84 @t14 @t108 @t109 @t13 @t10) (or (= @t83 (tptp.c_List_Ofoldr tptp.c_Type_Otype_OFun @t115 @t84 tptp.tc_Type_Otype tptp.tc_Type_Otype)) @t114 @t113 @t112))) % 0.31/0.61 (assume @p60 (forall @t76 (or (= (tptp.c_List_Oappend @t101 (tptp.c_List_Olist_OCons @t107 @t7 @t4) @t4) @t32) @t100))) % 0.31/0.61 (assume @p61 (tptp.c_Type_Otyping (tptp.c_Type_Oshift tptp.v_ea______ tptp.v_ia______ tptp.v_T____ tptp.tc_Type_Otype) @t117 tptp.v_T_Ha______)) % 0.31/0.61 (assume @p62 (forall @t87 (= (tptp.c_List_Ohd @t60 @t4) @t5))) % 0.31/0.61 (assume @p63 (forall (@list @t12 @t80 @t28 @t118) (= (tptp.c_Lambda_Osubst @t120 @t28 @t118) (tptp.hAPP (tptp.hAPP tptp.c_Lambda_OdB_OApp (tptp.c_Lambda_Osubst @t12 @t28 @t118)) (tptp.c_Lambda_Osubst @t80 @t28 @t118))))) % 0.31/0.61 (assume @p64 (forall @t122 (= @t7 @t121))) % 0.31/0.61 (assume @p65 (forall (@list @t14 @t13 @t84 @t109) (or (tptp.c_Type_Otypings @t14 @t13 @t124) @t123))) % 0.31/0.61 (assume @p66 (forall @t122 (= (tptp.c_List_Obutlast @t7 @t4) @t7))) % 0.31/0.61 (assume @p67 (forall (@list @t21 @t5 @t42 @t4 @t32) (or (tptp.c_ListOrder_Ostep1 @t21 (tptp.c_List_Olist_OCons @t5 @t42 @t4) @t60 @t4) @t126))) % 0.31/0.61 (assume @p68 (forall @t130 (or @t125 @t129 @t127))) % 0.31/0.61 (assume @p69 (forall (@list @t118 @t80) (= (tptp.c_Lambda_Osubst (tptp.c_Lambda_OdB_OVar @t118) @t80 @t118) @t80))) % 0.31/0.61 (assume @p70 (forall @t49 (= (tptp.c_List_OtakeWhile @t33 @t7 @t4) @t7))) % 0.31/0.61 (assume @p71 (forall @t122 (= (tptp.c_List_Otl @t7 @t4) @t7))) % 0.31/0.61 (assume @p72 (forall (@list @t21 @t109 @t131) (or (tptp.hBOOL (tptp.hAPP tptp.c_InductTermi_OIT (tptp.c_Lambda_Osubst @t21 @t110 @t131))) @t25))) % 0.31/0.61 (assume @p73 (forall @t135 (or (tptp.c_Type_Otypings @t14 @t13 @t134) @t133))) % 0.31/0.61 (assume @p74 (forall (@list @t4 @t32) (or (not (= @t7 @t104)) @t100))) % 0.31/0.61 (assume @p75 (forall (@list @t138 @t32 @t137 @t41 @t4) (= @t139 (tptp.c_List_Ofoldl (tptp.c_COMBC @t138 @t41 @t4 @t4) @t137 @t136 @t4 @t41)))) % 0.31/0.61 (assume @p76 (forall (@list @t32 @t4 @t42) (or (not (= @t104 @t141)) @t140))) % 0.31/0.61 (assume @p77 (forall (@list @t138 @t41 @t4) (= (tptp.c_List_Oconcat__map @t138 @t142 @t41 @t4) @t7))) % 0.31/0.61 (assume @p78 (forall (@list @t2 @t68) (or (tptp.hBOOL (tptp.hAPP tptp.c_InductTermi_OIT (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t143 @t68 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB))) (not (tptp.c_List_Olistsp tptp.c_InductTermi_OIT @t68 tptp.tc_Lambda_OdB))))) % 0.31/0.61 (assume @p79 (forall (@list @t2 @t5 @t4 @t118) (= (tptp.c_List_Oappend @t6 @t144 @t4) (tptp.c_List_Oappend @t144 @t6 @t4)))) % 0.31/0.61 (assume @p80 (forall @t87 (= (tptp.c_List_Otl @t60 @t4) @t32))) % 0.31/0.61 (assume @p81 (forall @t130 (or @t125 @t140 @t127))) % 0.31/0.61 (assume @p82 (forall @t147 (or (= (tptp.c_List_Osplice @t60 @t42 @t4) (tptp.c_List_Olist_OCons @t5 (tptp.c_List_Olist_OCons @t146 (tptp.c_List_Osplice @t32 (tptp.c_List_Otl @t42 @t4) @t4) @t4) @t4)) @t145))) % 0.31/0.61 (assume @p83 (forall (@list @t32 @t33 @t4 @t15 @t42) (or (not @t148) @t52 @t50))) % 0.31/0.61 (assume @p84 (forall @t54 (or @t53 @t148))) % 0.31/0.61 (assume @p85 (forall (@list @t2 @t13 @t21 @t26) (not (= (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t143 @t13 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB) (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t22 @t26 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB))))) % 0.31/0.61 (assume @p86 (forall @t151 (or (tptp.hBOOL (tptp.hAPP tptp.c_InductTermi_OIT @t150)) @t149))) % 0.31/0.61 (assume @p87 (forall (@list @t138 @t137 @t41 @t4) (= (tptp.c_List_Ofoldl @t138 @t137 @t142 @t4 @t41) @t137))) % 0.31/0.61 (assume @p88 (forall (@list @t21 @t32 @t4) (not (tptp.c_ListOrder_Ostep1 @t21 @t32 @t7 @t4)))) % 0.31/0.61 (assume @p89 (forall (@list @t21 @t4 @t32) (not (tptp.c_ListOrder_Ostep1 @t21 @t7 @t32 @t4)))) % 0.31/0.61 (assume @p90 (forall @t76 (or (= (tptp.c_List_Ohd @t104 @t4) @t107) @t100))) % 0.31/0.61 (assume @p91 (forall (@list @t2) (tptp.hBOOL (tptp.hAPP tptp.c_InductTermi_OIT @t143)))) % 0.31/0.61 (assume @p92 (forall @t8 (= (tptp.c_List_Orev @t6 @t4) @t6))) % 0.31/0.61 (assume @p93 (forall (@list @t28 @t12 @t118) (= (tptp.c_Lambda_Olift @t153 @t118) (tptp.hAPP (tptp.hAPP tptp.c_Lambda_OdB_OApp (tptp.c_Lambda_Olift @t28 @t118)) @t152)))) % 0.31/0.61 (assume @p94 (forall @t76 (= @t154 @t32))) % 0.31/0.61 (assume @p95 (forall @t155 (= (tptp.c_List_Orev @t141 @t4) @t42))) % 0.31/0.61 (assume @p96 (forall @t76 (= @t32 @t154))) % 0.31/0.61 (assume @p97 (forall @t76 (or (not (= @t156 @t7)) @t100))) % 0.31/0.61 (assume @p98 (forall @t20 (or @t19 @t157))) % 0.31/0.61 (assume @p99 (forall (@list @t21 @t15 @t62 @t5 @t4) (or (not (tptp.hBOOL (tptp.hAPP @t128 @t62))) (tptp.c_ListOrder_Ostep1 @t21 (tptp.c_List_Olist_OCons @t15 @t5 @t4) (tptp.c_List_Olist_OCons @t62 @t5 @t4) @t4)))) % 0.31/0.61 (assume @p100 (forall (@list @t5 @t15 @t32 @t42 @t21 @t4) (or @t18 @t140 @t127))) % 0.31/0.61 (assume @p101 (forall @t122 (= (tptp.c_List_Orotate1 @t7 @t4) @t7))) % 0.31/0.61 (assume @p102 (forall @t76 (or (= (tptp.c_List_Olast @t104 @t4) @t158) @t100))) % 0.31/0.61 (assume @p103 (forall (@list @t21 @t5 @t159 @t4 @t108) (or (tptp.c_ListOrder_Ostep1 @t21 (tptp.c_List_Oappend @t5 @t159 @t4) (tptp.c_List_Oappend @t5 @t108 @t4) @t4) (not (tptp.c_ListOrder_Ostep1 @t21 @t159 @t108 @t4))))) % 0.31/0.61 (assume @p104 (forall (@list @t21 @t42 @t32 @t4 @t5) (or @t126 (tptp.c_ListOrder_Ostep1 @t21 (tptp.c_List_Oappend @t42 @t5 @t4) @t160 @t4)))) % 0.31/0.61 (assume @p105 (forall (@list @t17) (= @t161 (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t161 @t11 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB)))) % 0.31/0.61 (assume @p106 (forall @t135 (or (tptp.c_Type_Otypings @t14 @t13 @t162) @t133))) % 0.31/0.61 (assume @p107 (forall (@list @t138 @t137 @t5 @t32 @t41 @t4) (= (tptp.c_List_Ofoldl @t138 @t137 @t163 @t4 @t41) (tptp.c_List_Ofoldl @t138 (tptp.hAPP (tptp.hAPP @t138 @t137) @t5) @t32 @t4 @t41)))) % 0.31/0.61 (assume @p108 (forall @t76 (or (= @t156 (tptp.c_List_Oappend @t164 (tptp.c_List_Olist_OCons @t158 @t7 @t4) @t4)) @t100))) % 0.31/0.61 (assume @p109 (forall (@list @t5 @t15 @t21 @t42 @t4 @t32) (or @t18 @t129 @t127))) % 0.31/0.61 (assume @p110 (forall (@list @t21 @t13 @t28) (or (not (= (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t21 @t13 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB) (tptp.c_List_Ofoldl tptp.c_Lambda_OdB_OApp @t28 @t13 tptp.tc_Lambda_OdB tptp.tc_Lambda_OdB))) @t73))) % 0.31/0.61 (assume @p111 (forall (@list @t14 @t108 @t84 @t83 @t109 @t13 @t10) (or (tptp.c_Type_Otypings @t14 @t108 @t115) @t114 @t113 @t112))) % 0.31/0.61 (assume @p112 (tptp.hBOOL (tptp.hAPP tptp.c_InductTermi_OIT tptp.v_u____))) % 0.31/0.61 (assume @p113 (forall @t67 (or (= @t105 (tptp.c_List_Olist_OCons @t5 @t74 @t4)) @t65))) % 0.31/0.61 (assume @p114 (forall (@list @t12 @t118 @t28) (= (tptp.c_Lambda_Osubst @t152 @t28 @t118) @t12))) % 0.31/0.61 (assume @p115 (= tptp.v_rs____ (tptp.c_List_Olist_OCons tptp.v_a____ tptp.v_as____ tptp.tc_Lambda_OdB))) % 0.31/0.61 (assume @p116 (forall @t76 (or (not (= @t104 @t7)) @t100))) % 0.31/0.61 (assume @p117 (forall @t166 (or @t165 @t27))) % 0.31/0.61 (assume @p118 (forall (@list @t138 @t137 @t32 @t4 @t41) (= @t167 (tptp.c_List_Ofoldr (tptp.c_COMBC @t138 @t4 @t41 @t4) @t136 @t137 @t41 @t4)))) % 0.31/0.61 (assume @p119 (forall (@list @t28 @t12 @t2 @t26) (not (= (tptp.hAPP (tptp.hAPP tptp.c_Lambda_OdB_OApp @t70) @t12) @t168)))) % 0.31/0.61 (assume @p120 (forall @t122 (= @t121 @t7))) % 0.31/0.61 (assume @p121 (forall @t169 (= (tptp.c_List_Orev @t43 @t4) (tptp.c_List_Oappend @t141 @t104 @t4)))) % 0.31/0.61 (assume @p122 (forall (@list @t138 @t137 @t32 @t42 @t41 @t4) (= (tptp.c_List_Ofoldl @t138 @t137 @t170 @t4 @t41) (tptp.c_List_Ofoldl @t138 @t167 @t42 @t4 @t41)))) % 0.31/0.61 (assume @p123 (forall @t174 (or (tptp.hBOOL (tptp.hAPP @t33 (tptp.c_List_Osko__List__Xsplit__list__last__prop__iff__1__5 @t33 @t173 @t4))) (tptp.hBOOL (tptp.hAPP @t33 (tptp.c_List_Osko__List__Xsplit__list__last__prop__iff__1__5 @t33 @t172 @t4))) @t171))) % 0.31/0.61 (assume @p124 (forall (@list @t138 @t5 @t32 @t41 @t4) (= (tptp.c_List_Oconcat__map @t138 @t163 @t41 @t4) (tptp.c_List_Oappend @t175 (tptp.c_List_Oconcat__map @t138 @t32 @t41 @t4) @t4)))) % 0.31/0.61 (assume @p125 (forall @t174 (or (tptp.hBOOL (tptp.hAPP @t33 (tptp.c_List_Osko__List__Xsplit__list__first__prop__iff__1__5 @t33 @t173 @t4))) (tptp.hBOOL (tptp.hAPP @t33 (tptp.c_List_Osko__List__Xsplit__list__first__prop__iff__1__5 @t33 @t5 @t4))) @t171))) % 0.31/0.61 (assume @p126 (forall (@list @t33 @t32 @t5 @t176 @t4) (or (= (tptp.c_List_OtakeWhile @t33 (tptp.c_List_Oappend @t32 (tptp.c_List_Olist_OCons @t5 @t176 @t4) @t4) @t4) @t74) @t64))) % 0.31/0.61 (assume @p127 (forall @t99 (or @t98 @t177 @t95))) % 0.31/0.61 (assume @p128 (forall @t94 (or @t93 @t178 @t89))) % 0.31/0.61 (assume @p129 (forall (@list @t2 @t5 @t4 @t32) (= (tptp.c_List_Oappend @t6 @t60 @t4) (tptp.c_List_Olist_OCons @t5 (tptp.c_List_Oappend @t6 @t32 @t4) @t4)))) % 0.31/0.61 (assume @p130 (forall @t169 (or (= (tptp.c_List_Ohd @t43 @t4) @t158) @t100))) % 0.31/0.61 (assume @p131 (forall @t76 (= (tptp.c_List_Obutlast @t179 @t4) @t101))) % 0.31/0.61 (assume @p132 (forall @t169 (or (= (tptp.c_List_Otl @t43 @t4) (tptp.c_List_Oappend @t164 @t42 @t4)) @t100))) % 0.31/0.61 (assume @p133 (forall @t169 (or (= (tptp.c_List_Olast @t43 @t4) (tptp.c_List_Olast @t42 @t4)) @t145))) % 0.31/0.61 (assume @p134 (forall @t76 (= (tptp.c_List_Olast @t179 @t4) @t107))) % 0.31/0.61 (assume @p135 (forall @t75 (= (tptp.c_List_Ohd @t180 @t4) @t146))) % 0.31/0.61 (assume @p136 (forall @t169 (or (= (tptp.c_List_Obutlast @t43 @t4) (tptp.c_List_Oappend @t32 (tptp.c_List_Obutlast @t42 @t4) @t4)) @t145))) % 0.31/0.61 (assume @p137 (forall @t151 (or (tptp.hBOOL (tptp.hAPP tptp.c_InductTermi_OIT (tptp.hAPP @t119 @t110))) @t149))) % 0.31/0.61 (assume @p138 (forall @t166 (or @t165 (= @t161 @t28)))) % 0.31/0.61 (assume @p139 (forall @t182 (or @t181 @t69))) % 0.31/0.61 (assume @p140 (forall @t182 (or @t181 @t157))) % 0.31/0.61 (assume @p141 (forall (@list @t14 @t80 @t84 @t12) (or (tptp.c_Type_Otyping @t14 @t80 @t184) @t183))) % 0.31/0.61 (assume @p142 (forall @t185 (or (tptp.c_Type_Otyping @t14 @t12 (tptp.c_List_Ofoldr tptp.c_Type_Otype_OFun @t134 @t84 tptp.tc_Type_Otype tptp.tc_Type_Otype)) @t133))) % 0.31/0.61 (assume @p143 (forall (@list @t14 @t12 @t13 @t84 @t10) (or @t132 @t113 (not (tptp.c_Type_Otyping @t14 @t12 (tptp.c_List_Ofoldr tptp.c_Type_Otype_OFun @t10 @t84 tptp.tc_Type_Otype tptp.tc_Type_Otype)))))) % 0.31/0.61 (assume @p144 (forall @t185 (or (tptp.c_Type_Otyping @t14 @t12 (tptp.c_List_Ofoldr tptp.c_Type_Otype_OFun @t162 @t84 tptp.tc_Type_Otype tptp.tc_Type_Otype)) @t133))) % 0.31/0.61 (assume @p145 (forall (@list @t187 @t80 @t83 @t109 @t12 @t84) (or (not (tptp.c_Type_Otyping @t187 @t80 @t83)) (not (tptp.c_Type_Otyping (tptp.c_Type_Oshift @t187 @t109 @t83 tptp.tc_Type_Otype) @t12 @t84)) (tptp.c_Type_Otyping @t187 @t186 @t84)))) % 0.31/0.61 (assume @p146 (forall (@list @t14 @t109 @t83 @t12 @t84) (or (tptp.c_Type_Otyping (tptp.c_Type_Oshift @t14 @t109 @t83 tptp.tc_Type_Otype) @t150 @t84) (not (tptp.c_Type_Otyping @t14 @t12 @t84))))) % 0.31/0.61 (assume @p147 (forall @t195 (or @t194 @t191 (not (tptp.c_Type_Otyping @t14 @t80 @t189)) @t190 (not (tptp.c_Type_Otyping (tptp.c_Type_Oshift @t14 @t109 @t189 tptp.tc_Type_Otype) @t12 @t188)) @t149))) % 0.31/0.61 (assume @p148 (forall @t195 (or @t194 @t191 (not (tptp.c_Type_Otyping @t14 @t80 @t192)) @t190 (not (tptp.c_Type_Otyping (tptp.c_Type_Oshift @t14 @t109 @t192 tptp.tc_Type_Otype) @t12 @t188)) @t149))) % 0.31/0.61 (assume @p149 (forall (@list @t14 @t109 @t84 @t13) (or (tptp.c_Type_Otyping @t14 @t110 (tptp.c_List_Ofoldr tptp.c_Type_Otype_OFun @t124 @t84 tptp.tc_Type_Otype tptp.tc_Type_Otype)) @t123))) % 0.31/0.61 (assume @p150 (forall (@list @t109 @t5 @t4) (= (tptp.c_List_Oappend @t196 @t102 @t4) (tptp.c_List_Olist_OCons @t5 @t196 @t4)))) % 0.31/0.61 (assume @p151 (forall (@list @t42 @t32 @t21 @t4 @t15 @t5) (or @t201 @t125 @t200))) % 0.31/0.61 (assume @p152 (forall (@list @t5 @t32 @t41) (= (tptp.c_List_Orotate1 @t163 @t41) (tptp.c_List_Oappend @t32 (tptp.c_List_Olist_OCons @t5 @t142 @t41) @t41)))) % 0.31/0.61 (assume @p153 (forall (@list @t42 @t4 @t15) (= (tptp.c_List_Orev @t202 @t4) @t51))) % 0.31/0.61 (assume @p154 (forall (@list @t32 @t4 @t15 @t42) (or (not (= @t104 @t51)) (= @t32 @t202)))) % 0.31/0.61 (assume @p155 (forall (@list @t21 @t15 @t5 @t42 @t32 @t4) (or @t129 @t125 @t200))) % 0.31/0.61 (assume @p156 (forall @t87 (= (tptp.c_List_Orev @t60 @t4) (tptp.c_List_Oappend @t104 @t102 @t4)))) % 0.31/0.61 (assume @p157 (forall @t94 (or @t93 @t91 @t145))) % 0.31/0.61 (assume @p158 (forall @t99 (or @t98 @t97 @t145))) % 0.31/0.61 (assume @p159 (forall (@list @t21 @t15 @t5 @t42 @t4 @t32) (or @t129 @t203 @t200))) % 0.31/0.61 (assume @p160 (forall (@list @t42 @t32 @t15 @t5 @t21 @t4) (or @t201 @t203 @t200))) % 0.31/0.61 (assume @p161 (forall @t204 (= (tptp.c_List_Obutlast @t197 @t4) @t32))) % 0.31/0.61 (assume @p162 (forall @t204 (= (tptp.c_List_Olast @t197 @t4) @t5))) % 0.31/0.61 (assume @p163 (forall @t99 (or @t98 @t177 @t145))) % 0.31/0.61 (assume @p164 (forall @t94 (or @t93 @t178 @t145))) % 0.31/0.61 (assume @p165 (forall (@list @t84 @t83 @t14 @t109 @t13) (or (= @t84 @t83) @t114 @t123))) % 0.31/0.61 (assume @p166 (forall (@list @t14 @t12 @t84 @t80) (or (tptp.c_Type_Otyping @t14 @t12 (tptp.hAPP (tptp.hAPP tptp.c_Type_Otype_OFun @t184) @t84)) @t183))) % 0.31/0.61 (assume @p167 (tptp.c_Type_Otypings @t205 tptp.v_as____ tptp.v_Ts____)) % 0.31/0.61 (assume @p168 (tptp.c_Type_Otyping tptp.v_e____ tptp.v_u____ tptp.v_T____)) % 0.31/0.61 (assume @p169 (tptp.c_Type_Otyping @t205 @t117 tptp.v_T_H____)) % 0.31/0.61 (assume @p170 (forall (@list @t207 @t206 @t57) (not (= @t208 @t58)))) % 0.31/0.61 (assume @p171 (forall @t213 (= (tptp.c_Type_Otype_Otype__case @t209 @t212 @t211 @t4) @t210))) % 0.31/0.61 (assume @p172 (forall @t122 (= @t7 @t214))) % 0.31/0.61 (assume @p173 (forall @t87 (= @t60 @t215))) % 0.31/0.61 (assume @p174 (forall @t204 (not (= @t32 @t60)))) % 0.31/0.61 (assume @p175 (forall (@list @t5 @t12 @t4) (not (= (tptp.c_List_Olist_OCons @t5 @t12 @t4) @t12)))) % 0.31/0.61 (assume @p176 (forall (@list @t33 @t209 @t212 @t57) (or (not (tptp.hBOOL (tptp.hAPP @t33 (tptp.c_Type_Otype_Otype__case @t209 @t212 @t211 tptp.t_a)))) (tptp.hBOOL (tptp.hAPP @t33 @t210))))) % 0.31/0.61 (assume @p177 (forall (@list @t33 @t209 @t212 @t216) (or (not (tptp.hBOOL (tptp.hAPP @t33 (tptp.c_Type_Otype_Otype__case @t209 @t212 (tptp.c_Type_Otype_OAtom @t216) tptp.t_a)))) (tptp.hBOOL (tptp.hAPP @t33 (tptp.hAPP @t209 @t216)))))) % 0.31/0.61 (assume @p178 (forall (@list @t218 @t217 @t4) (not (= @t219 @t7)))) % 0.31/0.61 (assume @p179 (forall (@list @t5 @t62 @t4) (not (= @t220 @t7)))) % 0.31/0.61 (assume @p180 (forall (@list @t5 @t221 @t88 @t4) (= (tptp.c_List_Olist_OCons @t5 (tptp.c_List_Oappend @t221 @t88 @t4) @t4) (tptp.c_List_Oappend (tptp.c_List_Olist_OCons @t5 @t221 @t4) @t88 @t4)))) % 0.31/0.61 (assume @p181 (forall (@list @t5 @t62 @t88 @t4) (= @t223 @t222))) % 0.31/0.61 (assume @p182 (forall @t147 (= (tptp.c_List_Oappend @t60 @t42 @t4) (tptp.c_List_Olist_OCons @t5 @t43 @t4)))) % 0.31/0.61 (assume @p183 (forall (@list @t5 @t62 @t4 @t88) (= @t222 @t223))) % 0.31/0.61 (assume @p184 (forall (@list @t85 @t5) (tptp.c_Type_Otyping @t85 (tptp.c_Lambda_OdB_OVar @t5) (tptp.hAPP @t85 @t5)))) % 0.31/0.61 (assume @p185 (forall (@list @t33 @t84) (or @t225 (not (tptp.hBOOL (tptp.hAPP @t33 @t224)))))) % 0.31/0.61 (assume @p186 (forall (@list @t42 @t32 @t4 @t88) (or (not (= (tptp.c_List_Oappend @t42 @t32 @t4) (tptp.c_List_Oappend @t88 @t32 @t4))) @t226))) % 0.31/0.61 (assume @p187 (forall @t227 (or (not (= @t43 (tptp.c_List_Oappend @t32 @t88 @t4))) @t226))) % 0.31/0.61 (assume @p188 (forall @t76 (= @t179 @t32))) % 0.31/0.61 (assume @p189 (forall @t16 (= @t5 (tptp.c_List_Oappend @t7 @t5 @t4)))) % 0.31/0.61 (assume @p190 (forall @t76 (= @t32 @t179))) % 0.31/0.61 (assume @p191 (forall @t75 (= @t180 @t42))) % 0.31/0.61 (assume @p192 (forall @t155 (= @t42 @t180))) % 0.31/0.61 (assume @p193 (forall @t230 (or (not (= @t211 (tptp.c_Type_Otype_OAtom @t228))) @t229))) % 0.31/0.61 (assume @p194 @t234) % 0.31/0.61 (assume @p195 @t235) % 0.31/0.61 (assume @p196 @t237) % 0.31/0.61 (assume @p197 (forall @t239 (or @t238 @t100))) % 0.31/0.61 (assume @p198 (forall @t239 (or @t238 @t145))) % 0.31/0.61 (assume @p199 (forall @t169 (or @t240 @t100))) % 0.31/0.61 (assume @p200 (forall @t169 (or @t240 @t145))) % 0.31/0.61 (assume @p201 (forall (@list @t57 @t207 @t206) (not (= @t58 @t208)))) % 0.31/0.61 (assume @p202 (tptp.c_Type_Otyping @t205 tptp.v_a____ tptp.v_T_H_H____)) % 0.31/0.61 (assume @p203 (forall @t213 (= (tptp.c_Type_Otype_Otype__rec @t209 @t212 @t211 @t4) @t210))) % 0.31/0.61 (assume @p204 (forall @t242 (or @t241 (= @t77 @t206)))) % 0.31/0.61 (assume @p205 (forall @t242 (or @t241 (= @t78 @t207)))) % 0.31/0.61 (assume @p206 (forall (@list @t4 @t218 @t217) (not (= @t7 @t219)))) % 0.31/0.61 (assume @p207 (forall (@list @t85 @t28 @t12 @t83 @t84) (or (tptp.c_Type_Otyping @t85 @t153 @t83) (not (tptp.c_Type_Otyping @t85 @t12 @t84)) (not (tptp.c_Type_Otyping @t85 @t28 @t86))))) % 0.31/0.61 (assume @p208 (forall @t169 (or (not (= @t43 @t32)) @t145))) % 0.31/0.61 (assume @p209 (forall @t169 (or (not (= @t32 @t43)) @t145))) % 0.31/0.61 (assume @p210 (forall @t169 (or (not (= @t43 @t42)) @t100))) % 0.31/0.61 (assume @p211 (forall (@list @t42 @t32 @t4) (or (not (= @t42 @t43)) @t100))) % 0.31/0.61 (assume @p212 (forall (@list @t4 @t5 @t32) (= @t215 @t60))) % 0.31/0.61 (assume @p213 (forall @t245 (or @t244 (= @t137 @t218)))) % 0.31/0.61 (assume @p214 (forall @t245 (or @t244 (= @t243 @t217)))) % 0.31/0.61 (assume @p215 (forall @t230 (or (not (= @t58 (tptp.c_Lambda_OdB_OVar @t228))) @t229))) % 0.31/0.61 (assume @p216 (forall @t247 (or @t246 @t140))) % 0.31/0.61 (assume @p217 (forall @t247 (or @t246 @t18))) % 0.31/0.61 (assume @p218 (forall @t122 (= @t214 @t7))) % 0.31/0.61 (assume @p219 (forall @t227 (= (tptp.c_List_Oappend @t43 @t88 @t4) (tptp.c_List_Oappend @t32 @t92 @t4)))) % 0.31/0.61 (assume @p220 (forall (@list @t32 @t221 @t108 @t4) (= (tptp.c_List_Oappend @t32 (tptp.c_List_Oappend @t221 @t108 @t4) @t4) (tptp.c_List_Oappend (tptp.c_List_Oappend @t32 @t221 @t4) @t108 @t4)))) % 0.31/0.61 (assume @p221 (forall (@list @t88 @t5 @t4 @t42) (= (tptp.c_List_Oappend (tptp.c_List_Oappend @t88 @t5 @t4) @t42 @t4) (tptp.c_List_Oappend @t88 (tptp.c_List_Oappend @t5 @t42 @t4) @t4)))) % 0.31/0.61 (assume @p222 (forall (@list @t32 @t5 @t13 @t4) (= (tptp.c_List_Oappend @t32 (tptp.c_List_Oappend @t5 @t13 @t4) @t4) (tptp.c_List_Oappend @t160 @t13 @t4)))) % 0.31/0.61 (assume @p223 (forall (@list @t249 @t248 @t57) (not (= @t250 @t211)))) % 0.31/0.61 (assume @p224 (forall @t255 (or @t254 (= @t251 @t249)))) % 0.31/0.61 (assume @p225 (forall @t255 (or @t254 (= @t252 @t248)))) % 0.31/0.61 (assume @p226 (forall (@list @t138 @t5 @t32 @t41 @t137 @t4) (= (tptp.c_List_Ofoldr @t138 @t163 @t137 @t41 @t4) (tptp.hAPP @t175 @t139)))) % 0.31/0.61 (assume @p227 (forall (@list @t33 @t189 @t192 @t84) (or (not (= @t224 @t193)) @t225 (tptp.hBOOL (tptp.hAPP @t33 @t192))))) % 0.31/0.61 (assume @p228 (forall (@list @t33 @t256 @t5 @t84) (or (not (= @t224 (tptp.hAPP (tptp.hAPP tptp.c_Type_Otype_OFun @t256) @t5))) @t225 (tptp.hBOOL (tptp.hAPP @t33 @t256))))) % 0.31/0.61 (assume @p229 (forall (@list @t138 @t32 @t42 @t41 @t137 @t4) (= (tptp.c_List_Ofoldr @t138 @t170 @t137 @t41 @t4) (tptp.c_List_Ofoldr @t138 @t32 (tptp.c_List_Ofoldr @t138 @t42 @t137 @t41 @t4) @t41 @t4)))) % 0.31/0.61 (assume @p230 @t259) % 0.31/0.61 (assume @p231 (tptp.c_Type_Otyping @t205 (tptp.hAPP (tptp.hAPP tptp.c_Lambda_OdB_OApp @t116) tptp.v_a____) @t257)) % 0.31/0.61 (assume @p232 (forall (@list @t138 @t41 @t137 @t4) (= (tptp.c_List_Ofoldr @t138 @t142 @t137 @t41 @t4) @t137))) % 0.31/0.61 (assume @p233 (forall @t261 (= (tptp.c_Type_Otype_Otype__rec @t209 @t212 @t253 @t4) (tptp.hAPP (tptp.hAPP @t260 (tptp.c_Type_Otype_Otype__rec @t209 @t212 @t251 @t4)) (tptp.c_Type_Otype_Otype__rec @t209 @t212 @t252 @t4))))) % 0.31/0.61 (assume @p234 (forall @t261 (= (tptp.c_Type_Otype_Otype__case @t209 @t212 @t253 @t4) @t260))) % 0.31/0.61 (assume @p235 (forall (@list @t33 @t209 @t212 @t62 @t172) (or (not (tptp.hBOOL (tptp.hAPP @t33 (tptp.c_Type_Otype_Otype__case @t209 @t212 (tptp.hAPP (tptp.hAPP tptp.c_Type_Otype_OFun @t62) @t172) tptp.t_a)))) (tptp.hBOOL (tptp.hAPP @t33 (tptp.hAPP (tptp.hAPP @t212 @t62) @t172)))))) % 0.31/0.61 (assume @p236 (forall (@list @t33 @t209 @t212 @t251 @t252) (or (not (tptp.hBOOL (tptp.hAPP @t33 (tptp.c_Type_Otype_Otype__case @t209 @t212 @t253 tptp.t_a)))) (tptp.hBOOL (tptp.hAPP @t33 @t260))))) % 0.31/0.61 (assume @p237 (forall (@list @t57 @t249 @t248) (not (= @t211 @t250)))) % 0.31/0.61 (assume @p238 (not @t262)) % 0.31/0.61 (assume @p239 (forall @t16 (tptp.c_fequal @t5 @t5 @t4))) % 0.31/0.61 (assume @p240 (forall (@list @t264 @t263 @t4) (or (= @t264 @t263) (not (tptp.c_fequal @t264 @t263 @t4))))) % 0.31/0.61 (step @p241 :rule eq-symm :args (@t236 @t84)) % 0.31/0.61 (step @p242 :rule cong :premises (@p241) :args (@t237)) % 0.31/0.61 (step @p243 :rule eq_resolve :premises (@p196 @p242)) % 0.31/0.61 (step @p244 :rule instantiate :premises (@p243) :args ((@list tptp.v_e____ tptp.v_i____ tptp.v_T____ tptp.tc_Type_Otype))) % 0.31/0.61 (step @p245 :rule refl :args (@t231)) % 0.31/0.61 (step @p246 :rule eq-symm :args (@t232 @t84)) % 0.31/0.61 (step @p247 :rule nary_cong :premises (@p246 @p245) :args (@t233)) % 0.31/0.61 (step @p248 :rule cong :premises (@p247) :args (@t234)) % 0.31/0.61 (step @p249 :rule eq_resolve :premises (@p194 @p248)) % 0.31/0.61 (step @p250 :rule instantiate :premises (@p249) :args ((@list @t205 tptp.v_n____ @t258))) % 0.31/0.61 (step @p251 :rule cnf_or_pos :args (@t267)) % 0.31/0.61 (step @p252 :rule reordering :premises (@p251) :args ((or @t265 @t266 (not @t267)))) % 0.31/0.61 (step @p253 :rule chain_m_resolution :premises (@p252 @p230 @p250) :args (@t266 (@list false false) (@list @t259 @t267))) % 0.31/0.61 (assume-push @p271 @t235) % 0.31/0.61 (assume-push @p272 @t266) % 0.31/0.61 (assume-push @p273 @t269) % 0.31/0.61 (step @p257 :rule symm :premises (@p253)) % 0.31/0.61 (step @p258 :rule symm :premises (@p195)) % 0.31/0.61 (step @p259 :rule refl :args (@t205)) % 0.31/0.61 (step @p260 :rule cong :premises (@p259 @p258) :args (@t268)) % 0.31/0.61 (step @p261 :rule trans :premises (@p244 @p260 @p257)) % 0.31/0.61 (step-pop @p274 :rule scope :premises (@p261)) % 0.31/0.61 (step-pop @p275 :rule scope :premises (@p274)) % 0.31/0.61 (step-pop @p276 :rule scope :premises (@p275)) % 0.31/0.61 (step @p262 :rule process_scope :premises (@p276) :args (@t262)) % 0.31/0.61 (step @p266 :rule implies_elim :premises (@p262)) % 0.31/0.61 (step @p267 :rule cnf_and_neg :args (@t270)) % 0.31/0.61 (step @p268 :rule resolution :premises (@p267 @p266) :args (true @t270)) % 0.31/0.61 (step @p269 :rule reordering :premises (@p268) :args ((or @t262 (not @t235) (not @t266) (not @t269)))) % 0.31/0.61 (step @p270 false :rule chain_m_resolution :premises (@p269 @p253 @p244 @p238 @p195) :args (false (@list false false true false) (@list @t266 @t269 @t262 @t235))) % 0.31/0.61 ) % 0.31/0.61 % SZS output end Proof % 0.31/0.61 % cvc5 exiting %------------------------------------------------------------------------------