%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWW929+1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n004.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 Jul 27 13:23:11 EDT 2022 % Result : Unknown 3.38s 3.57s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW929+1 : TPTP v8.1.0. Released v7.3.0. % 0.12/0.13 % Command : otter-tptp-script %s % 0.13/0.34 % Computer : n004.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Jul 27 02:54:06 EDT 2022 % 0.13/0.34 % CPUTime : % 2.66/2.79 ----- Otter 3.3f, August 2004 ----- % 2.66/2.79 The process was started by sandbox2 on n004.cluster.edu, % 2.66/2.79 Wed Jul 27 02:54:06 2022 % 2.66/2.79 The command was "./otter". The process ID is 10090. % 2.66/2.79 % 2.66/2.79 set(prolog_style_variables). % 2.66/2.79 set(auto). % 2.66/2.79 dependent: set(auto1). % 2.66/2.79 dependent: set(process_input). % 2.66/2.79 dependent: clear(print_kept). % 2.66/2.79 dependent: clear(print_new_demod). % 2.66/2.79 dependent: clear(print_back_demod). % 2.66/2.79 dependent: clear(print_back_sub). % 2.66/2.79 dependent: set(control_memory). % 2.66/2.79 dependent: assign(max_mem, 12000). % 2.66/2.79 dependent: assign(pick_given_ratio, 4). % 2.66/2.79 dependent: assign(stats_level, 1). % 2.66/2.79 dependent: assign(max_seconds, 10800). % 2.66/2.79 clear(print_given). % 2.66/2.79 % 2.66/2.79 formula_list(usable). % 2.66/2.79 all A (A=A). % 2.66/2.79 p__01(s__02(cbool__00,cT__00)). % 2.66/2.79 -p__01(s__02(cbool__00,cF__00)). % 2.66/2.79 all Vt (s__02(cbool__00,Vt)=s__02(cbool__00,cT__00)|s__02(cbool__00,Vt)=s__02(cbool__00,cF__00)). % 2.66/2.79 all V_3f2384 V_3f2380 Vf Vg ((all Vx (s__02(V_3f2380,chapp__02(s__02(cfun__02(V_3f2384,V_3f2380),Vf),s__02(V_3f2384,Vx)))=s__02(V_3f2380,chapp__02(s__02(cfun__02(V_3f2384,V_3f2380),Vg),s__02(V_3f2384,Vx)))))->s__02(cfun__02(V_3f2384,V_3f2380),Vf)=s__02(cfun__02(V_3f2384,V_3f2380),Vg)). % 2.66/2.80 all V_27B_27 V_27A_27 V_27t_27 Vx (s__02(V_27B_27,chapp__02(s__02(cfun__02(V_27A_27,V_27B_27),V_27t_27),s__02(V_27A_27,Vx)))=s__02(V_27B_27,chapp__02(s__02(cfun__02(V_27A_27,V_27B_27),V_27t_27),s__02(V_27A_27,Vx)))). % 2.66/2.80 p__01(s__02(cbool__00,cT__00)). % 2.66/2.80 all V_27t1_27 V_27t2_27 ((p__01(s__02(cbool__00,V_27t1_27))->p__01(s__02(cbool__00,V_27t2_27)))-> ((p__01(s__02(cbool__00,V_27t2_27))->p__01(s__02(cbool__00,V_27t1_27)))->s__02(cbool__00,V_27t1_27)=s__02(cbool__00,V_27t2_27))). % 2.66/2.80 all V_27t_27 (p__01(s__02(cbool__00,cF__00))->p__01(s__02(cbool__00,V_27t_27))). % 2.66/2.80 all V_27t_27 (p__01(s__02(cbool__00,V_27t_27))| -p__01(s__02(cbool__00,V_27t_27))). % 2.66/2.80 all V_27B_27 V_27A_27 V_27f_27 V_27x_27 (s__02(V_27B_27,c_27const_2ebool_2eLET_27__02(s__02(cfun__02(V_27A_27,V_27B_27),V_27f_27),s__02(V_27A_27,V_27x_27)))=s__02(V_27B_27,chapp__02(s__02(cfun__02(V_27A_27,V_27B_27),V_27f_27),s__02(V_27A_27,V_27x_27)))). % 2.66/2.80 all V_27A_27 V_27t_27 ((all V_27x_27 p__01(s__02(cbool__00,V_27t_27)))<->p__01(s__02(cbool__00,V_27t_27))). % 2.66/2.80 all V_27t_27 (-(-p__01(s__02(cbool__00,V_27t_27)))<->p__01(s__02(cbool__00,V_27t_27))). % 2.66/2.80 -p__01(s__02(cbool__00,cT__00))<->p__01(s__02(cbool__00,cF__00)). % 2.66/2.80 -p__01(s__02(cbool__00,cF__00))<->p__01(s__02(cbool__00,cT__00)). % 2.66/2.80 all V_27A_27 V_27x_27 (s__02(V_27A_27,V_27x_27)=s__02(V_27A_27,V_27x_27)<->p__01(s__02(cbool__00,cT__00))). % 2.66/2.80 all V_27A_27 V_27x_27 V_27y_27 (s__02(V_27A_27,V_27x_27)=s__02(V_27A_27,V_27y_27)<->s__02(V_27A_27,V_27y_27)=s__02(V_27A_27,V_27x_27)). % 2.66/2.80 all V_27t_27 ((s__02(cbool__00,cT__00)=s__02(cbool__00,V_27t_27)<->p__01(s__02(cbool__00,V_27t_27)))& (s__02(cbool__00,V_27t_27)=s__02(cbool__00,cT__00)<->p__01(s__02(cbool__00,V_27t_27)))& (s__02(cbool__00,cF__00)=s__02(cbool__00,V_27t_27)<-> -p__01(s__02(cbool__00,V_27t_27)))& (s__02(cbool__00,V_27t_27)=s__02(cbool__00,cF__00)<-> -p__01(s__02(cbool__00,V_27t_27)))). % 2.66/2.80 all V_27A_27 V_27t1_27 V_27t2_27 (s__02(V_27A_27,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cT__00),s__02(V_27A_27,V_27t1_27),s__02(V_27A_27,V_27t2_27)))=s__02(V_27A_27,V_27t1_27)&s__02(V_27A_27,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cF__00),s__02(V_27A_27,V_27t1_27),s__02(V_27A_27,V_27t2_27)))=s__02(V_27A_27,V_27t2_27)). % 2.66/2.80 all V_27A_270 V_27B_270 V_27C_27 (p__01(s__02(cbool__00,V_27A_270))|p__01(s__02(cbool__00,V_27B_270))|p__01(s__02(cbool__00,V_27C_27))<->p__01(s__02(cbool__00,V_27A_270))|p__01(s__02(cbool__00,V_27B_270))|p__01(s__02(cbool__00,V_27C_27))). % 2.66/2.80 all V_27A_270 V_27B_270 (p__01(s__02(cbool__00,V_27A_270))|p__01(s__02(cbool__00,V_27B_270))<->p__01(s__02(cbool__00,V_27B_270))|p__01(s__02(cbool__00,V_27A_270))). % 2.66/2.80 all V_27A_270 V_27B_270 ((p__01(s__02(cbool__00,V_27A_270))->p__01(s__02(cbool__00,V_27B_270)))<-> -p__01(s__02(cbool__00,V_27A_270))|p__01(s__02(cbool__00,V_27B_270))). % 2.66/2.80 all V_27t1_27 V_27t2_27 V_27t3_27 ((p__01(s__02(cbool__00,V_27t1_27))-> (p__01(s__02(cbool__00,V_27t2_27))->p__01(s__02(cbool__00,V_27t3_27))))<-> (p__01(s__02(cbool__00,V_27t1_27))&p__01(s__02(cbool__00,V_27t2_27))->p__01(s__02(cbool__00,V_27t3_27)))). % 2.66/2.80 all V_27x_27 V_27x_7c39_7c_27 V_27y_27 V_27y_7c39_7c_27 (s__02(cbool__00,V_27x_27)=s__02(cbool__00,V_27x_7c39_7c_27)& (p__01(s__02(cbool__00,V_27x_7c39_7c_27))->s__02(cbool__00,V_27y_27)=s__02(cbool__00,V_27y_7c39_7c_27))-> ((p__01(s__02(cbool__00,V_27x_27))->p__01(s__02(cbool__00,V_27y_27)))<-> (p__01(s__02(cbool__00,V_27x_7c39_7c_27))->p__01(s__02(cbool__00,V_27y_7c39_7c_27))))). % 2.66/2.80 all V_27A_27 V_27P_27 V_27Q_27 V_27x_27 V_27x_7c39_7c_27 V_27y_27 V_27y_7c39_7c_27 (s__02(cbool__00,V_27P_27)=s__02(cbool__00,V_27Q_27)& (p__01(s__02(cbool__00,V_27Q_27))->s__02(V_27A_27,V_27x_27)=s__02(V_27A_27,V_27x_7c39_7c_27))& (-p__01(s__02(cbool__00,V_27Q_27))->s__02(V_27A_27,V_27y_27)=s__02(V_27A_27,V_27y_7c39_7c_27))->s__02(V_27A_27,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,V_27P_27),s__02(V_27A_27,V_27x_27),s__02(V_27A_27,V_27y_27)))=s__02(V_27A_27,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,V_27Q_27),s__02(V_27A_27,V_27x_7c39_7c_27),s__02(V_27A_27,V_27y_7c39_7c_27)))). % 2.66/2.80 all V_27A_27 V_27f_27 V_27v_27 ((all V_27x_27 (s__02(V_27A_27,V_27x_27)=s__02(V_27A_27,V_27v_27)->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27f_27),s__02(V_27A_27,V_27x_27))))))<->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27f_27),s__02(V_27A_27,V_27v_27))))). % 2.66/2.80 all V_27A_27 ((all V_27t1_27 V_27t2_27 (s__02(V_27A_27,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cT__00),s__02(V_27A_27,V_27t1_27),s__02(V_27A_27,V_27t2_27)))=s__02(V_27A_27,V_27t1_27)))& (all V_27t1_27 V_27t2_27 (s__02(V_27A_27,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cF__00),s__02(V_27A_27,V_27t1_27),s__02(V_27A_27,V_27t2_27)))=s__02(V_27A_27,V_27t2_27)))). % 2.66/2.80 all V_27A_27 V_27x_27 (s__02(V_27A_27,c_27const_2ecombin_2eI_27__01(s__02(V_27A_27,V_27x_27)))=s__02(V_27A_27,V_27x_27)). % 2.66/2.80 all V_27m_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)&s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,V_27m_27)). % 2.66/2.80 all V_27m_27 V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)<->p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))))). % 2.66/2.80 all V_27A_27 V_27P_27 (p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(V_27A_27),cbool__00),V_27P_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),c_27const_2elist_2eNIL_27__00))))& (all V_27t_27 (p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(V_27A_27),cbool__00),V_27P_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27t_27))))-> (all V_27h_27 p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(V_27A_27),cbool__00),V_27P_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),c_27const_2elist_2eCONS_27__02(s__02(V_27A_27,V_27h_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27t_27)))))))))-> (all V_27l_27 p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(V_27A_27),cbool__00),V_27P_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l_27)))))). % 2.66/2.80 all V_27ee_27 ((exists V_27n_27 (s__02(c_27type_2ebvl_2eexp_27__00,V_27ee_27)=s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eVar_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))| (exists V_27e_27 V_27e0_27 V_27e1_27 (s__02(c_27type_2ebvl_2eexp_27__00,V_27ee_27)=s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eIf_27__03(s__02(c_27type_2ebvl_2eexp_27__00,V_27e_27),s__02(c_27type_2ebvl_2eexp_27__00,V_27e0_27),s__02(c_27type_2ebvl_2eexp_27__00,V_27e1_27)))))| (exists V_27l_27 V_27e_27 (s__02(c_27type_2ebvl_2eexp_27__00,V_27ee_27)=s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eLet_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27l_27),s__02(c_27type_2ebvl_2eexp_27__00,V_27e_27)))))| (exists V_27e_27 (s__02(c_27type_2ebvl_2eexp_27__00,V_27ee_27)=s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eRaise_27__01(s__02(c_27type_2ebvl_2eexp_27__00,V_27e_27)))))| (exists V_27e_27 V_27e0_27 (s__02(c_27type_2ebvl_2eexp_27__00,V_27ee_27)=s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eHandle_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27e_27),s__02(c_27type_2ebvl_2eexp_27__00,V_27e0_27)))))| (exists V_27e_27 (s__02(c_27type_2ebvl_2eexp_27__00,V_27ee_27)=s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eTick_27__01(s__02(c_27type_2ebvl_2eexp_27__00,V_27e_27)))))| (exists V_27n_27 V_27o_7c39_7c_27 V_27l_27 (s__02(c_27type_2ebvl_2eexp_27__00,V_27ee_27)=s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eCall_27__03(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2eoption_2eoption_27__01(c_27type_2enum_2enum_27__00),V_27o_7c39_7c_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27l_27)))))| (exists V_27o_7c39_7c_27 V_27l_27 (s__02(c_27type_2ebvl_2eexp_27__00,V_27ee_27)=s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eOp_27__02(s__02(c_27type_2eclosLang_2eop_27__00,V_27o_7c39_7c_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27l_27)))))). % 2.66/2.80 all V_27P_27 ((all V_27n_27 p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))& (all V_27n_27 V_27x_27 V_27y_27 V_27xs_27 ((all V_27n_7c39_7c_27 (s__02(c_27type_2enum_2enum_27__00,V_27n_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27y_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27))))))))& (s__02(c_27type_2enum_2enum_27__00,V_27n_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))))->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27y_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27))))))))))& (all V_27n_27 V_27v_27 p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eVar_27__01(s__02(c_27type_2enum_2enum_27__00,V_27v_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))))& (all V_27n_27 V_27x1_27 V_27x2_27 V_27x3_27 ((all V_27n_7c39_7c_27 V_27n_7c39_7c_7c39_7c_27 V_27n_7c39_7c_7c39_7c_7c39_7c_27 (s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x1_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_7c39_7c_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_7c39_7c_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x3_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00))))))))& (all V_27n_7c39_7c_27 V_27n_7c39_7c_7c39_7c_27 (s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x1_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00))))))))& (all V_27n_7c39_7c_27 (s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x1_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00))))))))->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eIf_27__03(s__02(c_27type_2ebvl_2eexp_27__00,V_27x1_27),s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27),s__02(c_27type_2ebvl_2eexp_27__00,V_27x3_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00))))))))& (all V_27n_27 V_27xs_27 V_27x2_27 ((all V_27n_7c39_7c_27 V_27n_7c39_7c_7c39_7c_27 (s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27)))&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00))))))))& (all V_27n_7c39_7c_27 (s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27))))))->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eLet_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27),s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00))))))))& (all V_27n_27 V_27x1_27 ((all V_27n_7c39_7c_27 (s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x1_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00))))))))->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eRaise_27__01(s__02(c_27type_2ebvl_2eexp_27__00,V_27x1_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00))))))))& (all V_27n_27 V_27x1_27 V_27x2_27 ((all V_27n_7c39_7c_27 V_27n_7c39_7c_7c39_7c_27 (s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x1_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00))))))))& (all V_27n_7c39_7c_27 (s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x1_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00))))))))->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eHandle_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x1_27),s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00))))))))& (all V_27n_27 V_27op_27 V_27xs_27 ((all V_27n_7c39_7c_27 (s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27))))))->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eOp_27__02(s__02(c_27type_2eclosLang_2eop_27__00,V_27op_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00))))))))& (all V_27n_27 V_27x_27 (p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00))))))->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eTick_27__01(s__02(c_27type_2ebvl_2eexp_27__00,V_27x_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00))))))))& (all V_27n_27 V_27ticks_27 V_27dest_27 V_27xs_27 ((all V_27n_7c39_7c_27 (s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))&s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27))))))->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eCall_27__03(s__02(c_27type_2enum_2enum_27__00,V_27ticks_27),s__02(c_27type_2eoption_2eoption_27__01(c_27type_2enum_2enum_27__00),V_27dest_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00))))))))-> (all V_27v_27 V_27v1_27 p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cbool__00)),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27v_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27v1_27)))))). % 3.38/3.56 all V__5 ((all V_27xs_27 V_27n_7c39_7c_27 exists Vv ((p__01(s__02(cbool__00,Vv))<->s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))&s__02(c_27type_2enum_2enum_27__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),V__5),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27))),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,Vv),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27)))))))-> (all V__4 ((all V__3 V_27x2_27 V_27xs_27 V_27n_7c39_7c_27 exists Vv ((p__01(s__02(cbool__00,Vv))<->s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))&s__02(c_27type_2enum_2enum_27__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00))),chapp__02(s__02(cfun__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)))),V__4),s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),V__3))),s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27))),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,Vv),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eLET_27__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),V__3),s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27)))))))))-> (all V__3 ((all V_27x3_27 V_27n_7c39_7c_7c39_7c_7c39_7c_27 exists Vv ((p__01(s__02(cbool__00,Vv))<->s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))&s__02(c_27type_2enum_2enum_27__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),V__3),s__02(c_27type_2ebvl_2eexp_27__00,V_27x3_27))),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_7c39_7c_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,Vv),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_7c39_7c_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x3_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))))))-> (all V__2 ((all V_27x3_27 V_27x2_27 V_27n_7c39_7c_7c39_7c_27 exists Vv ((p__01(s__02(cbool__00,Vv))<->s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))&s__02(c_27type_2enum_2enum_27__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00))),V__2),s__02(c_27type_2ebvl_2eexp_27__00,V_27x3_27))),s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27))),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,Vv),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eLET_27__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),V__3),s__02(c_27type_2ebvl_2eexp_27__00,V_27x3_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_7c39_7c_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))))))))-> (all V__1 ((all V_27x3_27 V_27x2_27 V_27x1_27 V_27n_7c39_7c_27 exists Vv ((p__01(s__02(cbool__00,Vv))<->s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))&s__02(c_27type_2enum_2enum_27__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00))),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)))),V__1),s__02(c_27type_2ebvl_2eexp_27__00,V_27x3_27))),s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27))),s__02(c_27type_2ebvl_2eexp_27__00,V_27x1_27))),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,Vv),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eLET_27__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00))),V__2),s__02(c_27type_2ebvl_2eexp_27__00,V_27x3_27))),s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x1_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))))))))-> (all V__0 ((all V_27y_27 V_27xs_27 V_27n_7c39_7c_27 exists Vv ((p__01(s__02(cbool__00,Vv))<->s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))&s__02(c_27type_2enum_2enum_27__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00))),V__0),s__02(c_27type_2ebvl_2eexp_27__00,V_27y_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27))),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,Vv),s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_7c39_7c_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27y_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27)))))))))-> (all V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))=s__02(c_27type_2enum_2enum_27__00,V_27n_27)))& (all V_27y_27 V_27xs_27 V_27x_27 V_27n_27 exists Vv ((p__01(s__02(cbool__00,Vv))<->s__02(c_27type_2enum_2enum_27__00,V_27n_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))&s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27y_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27)))))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,Vv),s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eLET_27__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00))),V__0),s__02(c_27type_2ebvl_2eexp_27__00,V_27y_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))))))))& (all V_27v_27 V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eVar_27__01(s__02(c_27type_2enum_2enum_27__00,V_27v_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))=s__02(c_27type_2enum_2enum_27__00,V_27n_27)))& (all V_27x3_27 V_27x2_27 V_27x1_27 V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eIf_27__03(s__02(c_27type_2ebvl_2eexp_27__00,V_27x1_27),s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27),s__02(c_27type_2ebvl_2eexp_27__00,V_27x3_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eLET_27__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00))),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)))),V__1),s__02(c_27type_2ebvl_2eexp_27__00,V_27x3_27))),s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27))),s__02(c_27type_2ebvl_2eexp_27__00,V_27x1_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))))))& (all V_27xs_27 V_27x2_27 V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eLet_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27),s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eLET_27__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00))),chapp__02(s__02(cfun__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)))),V__4),s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),V__3))),s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))))))& (all V_27x1_27 V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eRaise_27__01(s__02(c_27type_2ebvl_2eexp_27__00,V_27x1_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eLET_27__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),V__3),s__02(c_27type_2ebvl_2eexp_27__00,V_27x1_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))))))& (all V_27x2_27 V_27x1_27 V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eHandle_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x1_27),s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eLET_27__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),chapp__02(s__02(cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2ebvl_2eexp_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00))),V__2),s__02(c_27type_2ebvl_2eexp_27__00,V_27x2_27))),s__02(c_27type_2ebvl_2eexp_27__00,V_27x1_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))))))& (all V_27xs_27 V_27op_27 V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eOp_27__02(s__02(c_27type_2eclosLang_2eop_27__00,V_27op_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eLET_27__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),V__5),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))))))& (all V_27x_27 V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eTick_27__01(s__02(c_27type_2ebvl_2eexp_27__00,V_27x_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))))& (all V_27xs_27 V_27ticks_27 V_27n_27 V_27dest_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,c_27const_2ebvl_2eCall_27__03(s__02(c_27type_2enum_2enum_27__00,V_27ticks_27),s__02(c_27type_2eoption_2eoption_27__01(c_27type_2enum_2enum_27__00),V_27dest_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eLET_27__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),V__5),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_2 % 3.38/3.56 Search stopped in tp_alloc by max_mem option. % 3.38/3.56 7__00),V_27xs_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))))))))))))))))). % 3.38/3.56 -(all V__0 ((all V_27xs_27 V_27n0_27 exists Vv ((p__01(s__02(cbool__00,Vv))<->s__02(c_27type_2enum_2enum_27__00,V_27n0_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))&s__02(c_27type_2enum_2enum_27__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),V__0),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27))),s__02(c_27type_2enum_2enum_27__00,V_27n0_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,Vv),s__02(c_27type_2enum_2enum_27__00,V_27n0_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n0_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27)))))))-> (all V_27n_27 V_27x_27 V_27xs_27 exists Vv ((p__01(s__02(cbool__00,Vv))<->s__02(c_27type_2enum_2enum_27__00,V_27n_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))&s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,Vv),s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2ebool_2eLET_27__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00),chapp__02(s__02(cfun__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),cfun__02(c_27type_2enum_2enum_27__00,c_27type_2enum_2enum_27__00)),V__0),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),V_27xs_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2ebvl__inline_2eis__small__aux_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eCONS_27__02(s__02(c_27type_2ebvl_2eexp_27__00,V_27x_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eNIL_27__00))))))))))))). % 3.38/3.56 end_of_list. % 3.38/3.56 % 3.38/3.56 Search stopped in tp_alloc by max_mem option. % 3.38/3.56 % 3.38/3.56 ============ end of search ============ % 3.38/3.56 % 3.38/3.56 -------------- statistics ------------- % 3.38/3.56 clauses given 0 % 3.38/3.56 clauses generated 0 % 3.38/3.56 clauses kept 0 % 3.38/3.56 clauses forward subsumed 0 % 3.38/3.56 clauses back subsumed 0 % 3.38/3.56 Kbytes malloced 11718 % 3.38/3.56 % 3.38/3.56 ----------- times (seconds) ----------- % 3.38/3.56 user CPU time 0.77 (0 hr, 0 min, 0 sec) % 3.38/3.56 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 3.38/3.56 wall-clock time 3 (0 hr, 0 min, 3 sec) % 3.38/3.56 % 3.38/3.56 Process 10090 finished Wed Jul 27 02:54:09 2022 % 3.38/3.57 Otter interrupted % 3.38/3.57 PROOF NOT FOUND %------------------------------------------------------------------------------