%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWW897+1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n027.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:09 EDT 2022 % Result : Unknown 2.18s 2.35s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SWW897+1 : TPTP v8.1.0. Released v7.3.0. % 0.03/0.12 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n027.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Wed Jul 27 03:06:06 EDT 2022 % 0.12/0.33 % CPUTime : % 2.01/2.21 ----- Otter 3.3f, August 2004 ----- % 2.01/2.21 The process was started by sandbox on n027.cluster.edu, % 2.01/2.21 Wed Jul 27 03:06:06 2022 % 2.01/2.21 The command was "./otter". The process ID is 32563. % 2.01/2.21 % 2.01/2.21 set(prolog_style_variables). % 2.01/2.21 set(auto). % 2.01/2.21 dependent: set(auto1). % 2.01/2.21 dependent: set(process_input). % 2.01/2.21 dependent: clear(print_kept). % 2.01/2.21 dependent: clear(print_new_demod). % 2.01/2.21 dependent: clear(print_back_demod). % 2.01/2.21 dependent: clear(print_back_sub). % 2.01/2.21 dependent: set(control_memory). % 2.01/2.21 dependent: assign(max_mem, 12000). % 2.01/2.21 dependent: assign(pick_given_ratio, 4). % 2.01/2.21 dependent: assign(stats_level, 1). % 2.01/2.21 dependent: assign(max_seconds, 10800). % 2.01/2.21 clear(print_given). % 2.01/2.21 % 2.01/2.21 formula_list(usable). % 2.01/2.21 all A (A=A). % 2.01/2.21 p__01(s__02(cbool__00,cT__00)). % 2.01/2.21 -p__01(s__02(cbool__00,cF__00)). % 2.01/2.21 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.01/2.21 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.01/2.21 p__01(s__02(cbool__00,cT__00)). % 2.01/2.21 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.01/2.21 all V_27t_27 (p__01(s__02(cbool__00,cF__00))->p__01(s__02(cbool__00,V_27t_27))). % 2.01/2.21 all V_27t_27 (p__01(s__02(cbool__00,V_27t_27))| -p__01(s__02(cbool__00,V_27t_27))). % 2.01/2.21 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.01/2.21 all V_27t_27 ((p__01(s__02(cbool__00,cT__00))&p__01(s__02(cbool__00,V_27t_27))<->p__01(s__02(cbool__00,V_27t_27)))& (p__01(s__02(cbool__00,V_27t_27))&p__01(s__02(cbool__00,cT__00))<->p__01(s__02(cbool__00,V_27t_27)))& (p__01(s__02(cbool__00,cF__00))&p__01(s__02(cbool__00,V_27t_27))<->p__01(s__02(cbool__00,cF__00)))& (p__01(s__02(cbool__00,V_27t_27))&p__01(s__02(cbool__00,cF__00))<->p__01(s__02(cbool__00,cF__00)))& (p__01(s__02(cbool__00,V_27t_27))&p__01(s__02(cbool__00,V_27t_27))<->p__01(s__02(cbool__00,V_27t_27)))). % 2.01/2.21 all V_27t_27 (((p__01(s__02(cbool__00,cT__00))->p__01(s__02(cbool__00,V_27t_27)))<->p__01(s__02(cbool__00,V_27t_27)))& ((p__01(s__02(cbool__00,V_27t_27))->p__01(s__02(cbool__00,cT__00)))<->p__01(s__02(cbool__00,cT__00)))& ((p__01(s__02(cbool__00,cF__00))->p__01(s__02(cbool__00,V_27t_27)))<->p__01(s__02(cbool__00,cT__00)))& ((p__01(s__02(cbool__00,V_27t_27))->p__01(s__02(cbool__00,V_27t_27)))<->p__01(s__02(cbool__00,cT__00)))& ((p__01(s__02(cbool__00,V_27t_27))->p__01(s__02(cbool__00,cF__00)))<-> -p__01(s__02(cbool__00,V_27t_27)))). % 2.01/2.21 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.01/2.21 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.01/2.21 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.01/2.21 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.01/2.21 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.01/2.21 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.01/2.21 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.01/2.21 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.01/2.21 all V_27t1_27 V_27t2_27 (s__02(cbool__00,V_27t1_27)=s__02(cbool__00,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)))). % 2.01/2.21 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.01/2.21 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.01/2.21 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.01/2.21 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.01/2.21 all V_27A_27 V_27P_27 V_27Q_27 ((((exists V_27x_27 p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,V_27x_27)))))->p__01(s__02(cbool__00,V_27Q_27)))<-> (all V_27x_27 (p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,V_27x_27))))->p__01(s__02(cbool__00,V_27Q_27)))))& ((exists V_27x_27 p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,V_27x_27)))))&p__01(s__02(cbool__00,V_27Q_27))<-> (exists V_27x_27 (p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,V_27x_27))))&p__01(s__02(cbool__00,V_27Q_27)))))& (p__01(s__02(cbool__00,V_27Q_27))& (exists V_27x_27 p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,V_27x_27)))))<-> (exists V_27x_27 (p__01(s__02(cbool__00,V_27Q_27))&p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,V_27x_27)))))))). % 2.01/2.21 all V_27m_27 V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_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_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))). % 2.01/2.21 all V_27m_27 V_27n_27 V_27p_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27p_27)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_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,V_27p_27)))). % 2.01/2.21 all V_27A_27 V_27B_27 V_27R_27 V_27l1_27 V_27l2_27 (p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27),s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27l2_27))))<->s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27l2_27)))& (all V_27n_27 (p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27))))))->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27B_27,cbool__00),chapp__02(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_27),s__02(V_27A_27,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27))))),s__02(V_27B_27,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27l2_27))))))))). % 2.01/2.21 all V_27A_27 V_27l_27 V_27x_27 (p__01(s__02(cbool__00,c_27const_2ebool_2eIN_27__02(s__02(V_27A_27,V_27x_27),s__02(cfun__02(V_27A_27,cbool__00),c_27const_2elist_2eLIST__TO__SET_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l_27))))))<-> (exists V_27n_27 (p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l_27))))))&s__02(V_27A_27,V_27x_27)=s__02(V_27A_27,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l_27)))))). % 2.01/2.21 all V_27A_27 V_27B_27 V__1 ((all V_27n_27 V_27a_27 V_27x_27 V_27p_27 (s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,V_27a_27))),s__02(c_27type_2enum_2enum_27__00,V_27x_27))),s__02(c_27type_2eclosLang_2eexp_27__00,V_27p_27)))=s__02(cbool__00,c_27const_2eclosProps_2efv1_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27a_27))),s__02(c_27type_2enum_2enum_27__00,V_27x_27))),s__02(c_27type_2eclosLang_2eexp_27__00,V_27p_27)))))-> (all V__0 ((all V_27a_27 V_27x_27 V_27n_27 (s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__0),s__02(c_27type_2enum_2enum_27__00,V_27a_27))),s__02(c_27type_2enum_2enum_27__00,V_27x_27))),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,V_27a_27))),s__02(c_27type_2enum_2enum_27__00,V_27x_27)))))-> (all V_27R_27 V_27env1_27 V_27env2_27 V_27a_27 V_27es_27 exists Vv ((p__01(s__02(cbool__00,Vv))<-> (all V_27x_27 (p__01(s__02(cbool__00,c_27const_2elist_2eEXISTS_27__02(s__02(cfun__02(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00),cbool__00),c_27const_2epair_2eUNCURRY_27__01(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__0),s__02(c_27type_2enum_2enum_27__00,V_27a_27))),s__02(c_27type_2enum_2enum_27__00,V_27x_27))))),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),V_27es_27))))->p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,V_27x_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27env1_27))))))&p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,V_27x_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27env2_27))))))&p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27B_27,cbool__00),chapp__02(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_27),s__02(V_27A_27,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,V_27x_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27env1_27))))),s__02(V_27B_27,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,V_27x_27),s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27env2_27)))))))))& (exists Vv_27 ((p__01(s__02(cbool__00,Vv_27))<->s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27env1_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27env2_27))))&s__02(cbool__00,c_27const_2eclos__callProof_2eenv__rel_27__05(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27env1_27),s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27env2_27),s__02(c_27type_2enum_2enum_27__00,V_27a_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),V_27es_27)))=s__02(cbool__00,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,Vv_27),s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27env1_27),s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27env2_27))),s__02(cbool__00,Vv)))))))))). % 2.01/2.22 -(all V_27A_27 V_27B_27 V_27env1_27 V_27env2_27 V_27R_27 V_27R_7c39_7c_27 V_27a_27 V_27es_27 ((all V_27x_27 V_27y_27 (p__01(s__02(cbool__00,c_27const_2ebool_2eIN_27__02(s__02(V_27A_27,V_27x_27),s__02(cfun__02(V_27A_27,cbool__00),c_27const_2elist_2eLIST__TO__SET_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27env1_27))))))&p__01(s__02(cbool__00,c_27const_2ebool_2eIN_27__02(s__02(V_27B_27,V_27y_27),s__02(cfun__02(V_27B_27,cbool__00),c_27const_2elist_2eLIST__TO__SET_27__01(s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27env2_27))))))->s__02(cbool__00,chapp__02(s__02(cfun__02(V_27B_27,cbool__00),chapp__02(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_27),s__02(V_27A_27,V_27x_27))),s__02(V_27B_27,V_27y_27)))=s__02(cbool__00,chapp__02(s__02(cfun__02(V_27B_27,cbool__00),chapp__02(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_7c39_7c_27),s__02(V_27A_27,V_27x_27))),s__02(V_27B_27,V_27y_27)))))->s__02(cbool__00,c_27const_2eclos__callProof_2eenv__rel_27__05(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27env1_27),s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27env2_27),s__02(c_27type_2enum_2enum_27__00,V_27a_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),V_27es_27)))=s__02(cbool__00,c_27const_2eclos__callProof_2eenv__rel_27__05(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_7c39_7c_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27env1_27),s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27env2_27),s__02(c_27type_2enum_2enum_27__00,V_27a_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),V_27es_27))))). % 2.01/2.22 end_of_list. % 2.01/2.22 % 2.01/2.22 -------> usable clausifies to: % 2.01/2.22 % 2.01/2.22 list(usable). % 2.01/2.22 0 [] A=A. % 2.01/2.22 0 [] p__01(s__02(cbool__00,cT__00)). % 2.01/2.22 0 [] -p__01(s__02(cbool__00,cF__00)). % 2.01/2.22 0 [] s__02(cbool__00,Vt)=s__02(cbool__00,cT__00)|s__02(cbool__00,Vt)=s__02(cbool__00,cF__00). % 2.01/2.22 0 [] s__02(V_3f2380,chapp__02(s__02(cfun__02(V_3f2384,V_3f2380),Vf),s__02(V_3f2384,$f1(V_3f2384,V_3f2380,Vf,Vg))))!=s__02(V_3f2380,chapp__02(s__02(cfun__02(V_3f2384,V_3f2380),Vg),s__02(V_3f2384,$f1(V_3f2384,V_3f2380,Vf,Vg))))|s__02(cfun__02(V_3f2384,V_3f2380),Vf)=s__02(cfun__02(V_3f2384,V_3f2380),Vg). % 2.01/2.22 0 [] p__01(s__02(cbool__00,cT__00)). % 2.01/2.22 0 [] p__01(s__02(cbool__00,V_27t1_27))|p__01(s__02(cbool__00,V_27t2_27))|s__02(cbool__00,V_27t1_27)=s__02(cbool__00,V_27t2_27). % 2.01/2.22 0 [] -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.01/2.22 0 [] -p__01(s__02(cbool__00,cF__00))|p__01(s__02(cbool__00,V_27t_27)). % 2.01/2.22 0 [] p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,V_27t_27)). % 2.01/2.22 0 [] p__01(s__02(cbool__00,V_27t_27))| -p__01(s__02(cbool__00,cF__00)). % 2.01/2.22 0 [] -p__01(s__02(cbool__00,cF__00))|p__01(s__02(cbool__00,V_27t_27))| -p__01(s__02(cbool__00,cT__00)). % 2.01/2.22 0 [] p__01(s__02(cbool__00,cT__00)). % 2.01/2.22 0 [] -p__01(s__02(cbool__00,cF__00))| -p__01(s__02(cbool__00,V_27t_27)). % 2.01/2.22 0 [] 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.01/2.22 0 [] 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.01/2.22 0 [] 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.01/2.22 0 [] 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.01/2.22 0 [] s__02(cbool__00,cT__00)!=s__02(cbool__00,V_27t_27)|p__01(s__02(cbool__00,V_27t_27)). % 2.01/2.22 0 [] s__02(cbool__00,cT__00)=s__02(cbool__00,V_27t_27)| -p__01(s__02(cbool__00,V_27t_27)). % 2.01/2.22 0 [] s__02(cbool__00,V_27t_27)!=s__02(cbool__00,cT__00)|p__01(s__02(cbool__00,V_27t_27)). % 2.01/2.22 0 [] s__02(cbool__00,V_27t_27)=s__02(cbool__00,cT__00)| -p__01(s__02(cbool__00,V_27t_27)). % 2.01/2.22 0 [] s__02(cbool__00,cF__00)!=s__02(cbool__00,V_27t_27)| -p__01(s__02(cbool__00,V_27t_27)). % 2.01/2.22 0 [] s__02(cbool__00,cF__00)=s__02(cbool__00,V_27t_27)|p__01(s__02(cbool__00,V_27t_27)). % 2.01/2.22 0 [] s__02(cbool__00,V_27t_27)!=s__02(cbool__00,cF__00)| -p__01(s__02(cbool__00,V_27t_27)). % 2.01/2.22 0 [] s__02(cbool__00,V_27t_27)=s__02(cbool__00,cF__00)|p__01(s__02(cbool__00,V_27t_27)). % 2.01/2.22 0 [] 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). % 2.01/2.22 0 [] 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.01/2.22 0 [] s__02(cbool__00,V_27t1_27)!=s__02(cbool__00,V_27t2_27)| -p__01(s__02(cbool__00,V_27t1_27))|p__01(s__02(cbool__00,V_27t2_27)). % 2.01/2.22 0 [] s__02(cbool__00,V_27t1_27)!=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)). % 2.01/2.22 0 [] s__02(cbool__00,V_27t1_27)=s__02(cbool__00,V_27t2_27)|p__01(s__02(cbool__00,V_27t1_27))|p__01(s__02(cbool__00,V_27t2_27)). % 2.01/2.22 0 [] s__02(cbool__00,V_27t1_27)=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)). % 2.01/2.22 0 [] 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))| -p__01(s__02(cbool__00,V_27x_27))|p__01(s__02(cbool__00,V_27y_27)). % 2.01/2.22 0 [] s__02(cbool__00,V_27x_27)!=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_27x_7c39_7c_27))|p__01(s__02(cbool__00,V_27y_7c39_7c_27)). % 2.01/2.22 0 [] s__02(cbool__00,V_27x_27)!=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_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.01/2.22 0 [] s__02(cbool__00,V_27x_27)!=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_27y_7c39_7c_27)). % 2.01/2.22 0 [] 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_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.01/2.22 0 [] s__02(cbool__00,V_27P_27)!=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,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.01/2.22 0 [] s__02(cbool__00,V_27P_27)!=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)|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.01/2.22 0 [] s__02(V_27A_27,$f3(V_27A_27,V_27f_27,V_27v_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_27v_27)))). % 2.01/2.22 0 [] -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,$f3(V_27A_27,V_27f_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_27v_27)))). % 2.01/2.22 0 [] 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.01/2.22 0 [] 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). % 2.01/2.22 0 [] s__02(V_27A_27,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cF__00),s__02(V_27A_27,X1),s__02(V_27A_27,X2)))=s__02(V_27A_27,X2). % 2.01/2.22 0 [] p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,$f4(V_27A_27,V_27P_27,V_27Q_27)))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,V_27x_27))))|p__01(s__02(cbool__00,V_27Q_27)). % 2.01/2.22 0 [] -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,X3))))|p__01(s__02(cbool__00,V_27Q_27))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,$f5(V_27A_27,V_27P_27,V_27Q_27))))). % 2.01/2.22 0 [] -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,X4))))| -p__01(s__02(cbool__00,V_27Q_27))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,$f6(V_27A_27,V_27P_27,V_27Q_27))))). % 2.01/2.22 0 [] p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,$f7(V_27A_27,V_27P_27,V_27Q_27)))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,X5))))| -p__01(s__02(cbool__00,V_27Q_27)). % 2.01/2.22 0 [] -p__01(s__02(cbool__00,V_27Q_27))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,X6))))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,$f8(V_27A_27,V_27P_27,V_27Q_27))))). % 2.01/2.22 0 [] p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,$f9(V_27A_27,V_27P_27,V_27Q_27)))))| -p__01(s__02(cbool__00,V_27Q_27))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,X7)))). % 2.01/2.22 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_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_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27))). % 2.01/2.22 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27p_27)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_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,V_27p_27))). % 2.01/2.22 0 [] -p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27),s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27l2_27))))|s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27l2_27))). % 2.01/2.22 0 [] -p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27),s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27l2_27))))| -p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27))))))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27B_27,cbool__00),chapp__02(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_27),s__02(V_27A_27,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27))))),s__02(V_27B_27,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27l2_27)))))). % 2.01/2.22 0 [] p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27),s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27l2_27))))|s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27)))!=s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27l2_27)))|p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,$f10(V_27A_27,V_27B_27,V_27R_27,V_27l1_27,V_27l2_27)),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27)))))). % 2.01/2.22 0 [] p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27),s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27l2_27))))|s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27)))!=s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27l2_27)))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27B_27,cbool__00),chapp__02(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_27),s__02(V_27A_27,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,$f10(V_27A_27,V_27B_27,V_27R_27,V_27l1_27,V_27l2_27)),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27))))),s__02(V_27B_27,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,$f10(V_27A_27,V_27B_27,V_27R_27,V_27l1_27,V_27l2_27)),s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27l2_27)))))). % 2.01/2.22 0 [] -p__01(s__02(cbool__00,c_27const_2ebool_2eIN_27__02(s__02(V_27A_27,V_27x_27),s__02(cfun__02(V_27A_27,cbool__00),c_27const_2elist_2eLIST__TO__SET_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l_27))))))|p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,$f11(V_27A_27,V_27l_27,V_27x_27)),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l_27)))))). % 2.01/2.22 0 [] -p__01(s__02(cbool__00,c_27const_2ebool_2eIN_27__02(s__02(V_27A_27,V_27x_27),s__02(cfun__02(V_27A_27,cbool__00),c_27const_2elist_2eLIST__TO__SET_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l_27))))))|s__02(V_27A_27,V_27x_27)=s__02(V_27A_27,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,$f11(V_27A_27,V_27l_27,V_27x_27)),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l_27))). % 2.01/2.22 0 [] p__01(s__02(cbool__00,c_27const_2ebool_2eIN_27__02(s__02(V_27A_27,V_27x_27),s__02(cfun__02(V_27A_27,cbool__00),c_27const_2elist_2eLIST__TO__SET_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l_27))))))| -p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l_27))))))|s__02(V_27A_27,V_27x_27)!=s__02(V_27A_27,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l_27))). % 2.01/2.22 0 [] s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f14(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f13(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(V_27A_27,V_27B_27,V__1))))!=s__02(cbool__00,c_27const_2eclosProps_2efv1_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V__1)),s__02(c_27type_2enum_2enum_27__00,$f14(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f13(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(V_27A_27,V_27B_27,V__1))))|s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__0),s__02(c_27type_2enum_2enum_27__00,$f18(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f17(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f16(V_27A_27,V_27B_27,V__1,V__0))))!=s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,$f16(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f18(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f17(V_27A_27,V_27B_27,V__1,V__0))))| -p__01(s__02(cbool__00,$f21(V_27A_27,V_27B_27,V__1,V__0,V_27R_27,V_27env1_27,V_27env2_27,V_27a_27,V_27es_27)))| -p__01(s__02(cbool__00,c_27const_2elist_2eEXISTS_27__02(s__02(cfun__02(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00),cbool__00),c_27const_2epair_2eUNCURRY_27__01(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__0),s__02(c_27type_2enum_2enum_27__00,V_27a_27))),s__02(c_27type_2enum_2enum_27__00,V_27x_27))))),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),V_27es_27))))|p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,V_27x_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27env1_27)))))). % 2.01/2.22 0 [] s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f14(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f13(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(V_27A_27,V_27B_27,V__1))))!=s__02(cbool__00,c_27const_2eclosProps_2efv1_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V__1)),s__02(c_27type_2enum_2enum_27__00,$f14(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f13(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(V_27A_27,V_27B_27,V__1))))|s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__0),s__02(c_27type_2enum_2enum_27__00,$f18(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f17(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f16(V_27A_27,V_27B_27,V__1,V__0))))!=s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,$f16(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f18(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f17(V_27A_27,V_27B_27,V__1,V__0))))| -p__01(s__02(cbool__00,$f21(V_27A_27,V_27B_27,V__1,V__0,V_27R_27,V_27env1_27,V_27env2_27,V_27a_27,V_27es_27)))| -p__01(s__02(cbool__00,c_27const_2elist_2eEXISTS_27__02(s__02(cfun__02(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00),cbool__00),c_27const_2epair_2eUNCURRY_27__01(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__0),s__02(c_27type_2enum_2enum_27__00,V_27a_27))),s__02(c_27type_2enum_2enum_27__00,V_27x_27))))),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),V_27es_27))))|p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,V_27x_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27env2_27)))))). % 2.01/2.22 0 [] s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f14(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f13(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(V_27A_27,V_27B_27,V__1))))!=s__02(cbool__00,c_27const_2eclosProps_2efv1_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V__1)),s__02(c_27type_2enum_2enum_27__00,$f14(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f13(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(V_27A_27,V_27B_27,V__1))))|s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__0),s__02(c_27type_2enum_2enum_27__00,$f18(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f17(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f16(V_27A_27,V_27B_27,V__1,V__0))))!=s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,$f16(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f18(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f17(V_27A_27,V_27B_27,V__1,V__0))))| -p__01(s__02(cbool__00,$f21(V_27A_27,V_27B_27,V__1,V__0,V_27R_27,V_27env1_27,V_27env2_27,V_27a_27,V_27es_27)))| -p__01(s__02(cbool__00,c_27const_2elist_2eEXISTS_27__02(s__02(cfun__02(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00),cbool__00),c_27const_2epair_2eUNCURRY_27__01(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__0),s__02(c_27type_2enum_2enum_27__00,V_27a_27))),s__02(c_27type_2enum_2enum_27__00,V_27x_27))))),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),V_27es_27))))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27B_27,cbool__00),chapp__02(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_27),s__02(V_27A_27,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,V_27x_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27env1_27))))),s__02(V_27B_27,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,V_27x_27),s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27env2_27)))))). % 2.01/2.22 0 [] s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f14(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f13(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(V_27A_27,V_27B_27,V__1))))!=s__02(cbool__00,c_27const_2eclosProps_2efv1_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V__1)),s__02(c_27type_2enum_2enum_27__00,$f14(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f13(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(V_27A_27,V_27B_27,V__1))))|s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__0),s__02(c_27type_2enum_2enum_27__00,$f18(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f17(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f16(V_27A_27,V_27B_27,V__1,V__0))))!=s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,$f16(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f18(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f17(V_27A_27,V_27B_27,V__1,V__0))))|p__01(s__02(cbool__00,$f21(V_27A_27,V_27B_27,V__1,V__0,V_27R_27,V_27env1_27,V_27env2_27,V_27a_27,V_27es_27)))|p__01(s__02(cbool__00,c_27const_2elist_2eEXISTS_27__02(s__02(cfun__02(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00),cbool__00),c_27const_2epair_2eUNCURRY_27__01(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__0),s__02(c_27type_2enum_2enum_27__00,V_27a_27))),s__02(c_27type_2enum_2enum_27__00,$f19(V_27A_27,V_27B_27,V__1,V__0,V_27R_27,V_27env1_27,V_27env2_27,V_27a_27,V_27es_27)))))),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),V_27es_27)))). % 2.01/2.22 0 [] s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f14(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f13(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(V_27A_27,V_27B_27,V__1))))!=s__02(cbool__00,c_27const_2eclosProps_2efv1_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V__1)),s__02(c_27type_2enum_2enum_27__00,$f14(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f13(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(V_27A_27,V_27B_27,V__1))))|s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__0),s__02(c_27type_2enum_2enum_27__00,$f18(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f17(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f16(V_27A_27,V_27B_27,V__1,V__0))))!=s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,$f16(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f18(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f17(V_27A_27,V_27B_27,V__1,V__0))))|p__01(s__02(cbool__00,$f21(V_27A_27,V_27B_27,V__1,V__0,V_27R_27,V_27env1_27,V_27env2_27,V_27a_27,V_27es_27)))| -p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,$f19(V_27A_27,V_27B_27,V__1,V__0,V_27R_27,V_27env1_27,V_27env2_27,V_27a_27,V_27es_27)),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27env1_27))))))| -p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,$f19(V_27A_27,V_27B_27,V__1,V__0,V_27R_27,V_27env1_27,V_27env2_27,V_27a_27,V_27es_27)),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27env2_27))))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27B_27,cbool__00),chapp__02(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_27),s__02(V_27A_27,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,$f19(V_27A_27,V_27B_27,V__1,V__0,V_27R_27,V_27env1_27,V_27env2_27,V_27a_27,V_27es_27)),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27env1_27))))),s__02(V_27B_27,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,$f19(V_27A_27,V_27B_27,V__1,V__0,V_27R_27,V_27env1_27,V_27env2_27,V_27a_27,V_27es_27)),s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27env2_27)))))). % 2.01/2.22 0 [] s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f14(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f13(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(V_27A_27,V_27B_27,V__1))))!=s__02(cbool__00,c_27const_2eclosProps_2efv1_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V__1)),s__02(c_27type_2enum_2enum_27__00,$f14(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f13(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(V_27A_27,V_27B_27,V__1))))|s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__0),s__02(c_27type_2enum_2enum_27__00,$f18(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f17(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f16(V_27A_27,V_27B_27,V__1,V__0))))!=s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,$f16(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f18(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f17(V_27A_27,V_27B_27,V__1,V__0))))| -p__01(s__02(cbool__00,$f20(V_27A_27,V_27B_27,V__1,V__0,V_27R_27,V_27env1_27,V_27env2_27,V_27a_27,V_27es_27)))|s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27env1_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27env2_27))). % 2.01/2.22 0 [] s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f14(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f13(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(V_27A_27,V_27B_27,V__1))))!=s__02(cbool__00,c_27const_2eclosProps_2efv1_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V__1)),s__02(c_27type_2enum_2enum_27__00,$f14(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f13(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(V_27A_27,V_27B_27,V__1))))|s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__0),s__02(c_27type_2enum_2enum_27__00,$f18(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f17(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f16(V_27A_27,V_27B_27,V__1,V__0))))!=s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,$f16(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f18(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f17(V_27A_27,V_27B_27,V__1,V__0))))|p__01(s__02(cbool__00,$f20(V_27A_27,V_27B_27,V__1,V__0,V_27R_27,V_27env1_27,V_27env2_27,V_27a_27,V_27es_27)))|s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27env1_27)))!=s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27env2_27))). % 2.01/2.22 0 [] s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f14(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f13(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(V_27A_27,V_27B_27,V__1))))!=s__02(cbool__00,c_27const_2eclosProps_2efv1_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V__1)),s__02(c_27type_2enum_2enum_27__00,$f14(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2enum_2enum_27__00,$f13(V_27A_27,V_27B_27,V__1)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(V_27A_27,V_27B_27,V__1))))|s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__0),s__02(c_27type_2enum_2enum_27__00,$f18(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f17(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f16(V_27A_27,V_27B_27,V__1,V__0))))!=s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),V__1),s__02(c_27type_2enum_2enum_27__00,$f16(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f18(V_27A_27,V_27B_27,V__1,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f17(V_27A_27,V_27B_27,V__1,V__0))))|s__02(cbool__00,c_27const_2eclos__callProof_2eenv__rel_27__05(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27env1_27),s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27env2_27),s__02(c_27type_2enum_2enum_27__00,V_27a_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),V_27es_27)))=s__02(cbool__00,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,$f20(V_27A_27,V_27B_27,V__1,V__0,V_27R_27,V_27env1_27,V_27env2_27,V_27a_27,V_27es_27)),s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(V_27A_27,cfun__02(V_27B_27,cbool__00)),V_27R_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27env1_27),s__02(c_27type_2elist_2elist_27__01(V_27B_27),V_27env2_27))),s__02(cbool__00,$f21(V_27A_27,V_27B_27,V__1,V__0,V_27R_27,V_27env1_27,V_27env2_27,V_27a_27,V_27es_27)))). % 2.01/2.22 0 [] -p__01(s__02(cbool__00,c_27const_2ebool_2eIN_27__02(s__02($c8,V_27x_27),s__02(cfun__02($c8,cbool__00),c_27const_2elist_2eLIST__TO__SET_27__01(s__02(c_27type_2elist_2elist_27__01($c8),$c6))))))| -p__01(s__02(cbool__00,c_27const_2ebool_2eIN_27__02(s__02($c7,V_27y_27),s__02(cfun__02($c7,cbool__00),c_27const_2elist_2eLIST__TO__SET_27__01(s__02(c_27type_2elist_2elist_27__01($c7),$c5))))))|s__02(cbool__00,chapp__02(s__02(cfun__02($c7,cbool__00),chapp__02(s__02(cfun__02($c8,cfun__02($c7,cbool__00)),$c4),s__02($c8,V_27x_27))),s__02($c7,V_27y_27)))=s__02(cbool__00,chapp__02(s__02(cfun__02($c7,cbool__00),chapp__02(s__02(cfun__02($c8,cfun__02($c7,cbool__00)),$c3),s__02($c8,V_27x_27))),s__02($c7,V_27y_27))). % 2.01/2.22 0 [] s__02(cbool__00,c_27const_2eclos__callProof_2eenv__rel_27__05(s__02(cfun__02($c8,cfun__02($c7,cbool__00)),$c4),s__02(c_27type_2elist_2elist_27__01($c8),$c6),s__02(c_27type_2elist_2elist_27__01($c7),$c5),s__02(c_27type_2enum_2enum_27__00,$c2),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),$c1)))!=s__02(cbool__00,c_27const_2eclos__callProof_2eenv__rel_27__05(s__02(cfun__02($c8,cfun__02($c7,cbool__00)),$c3),s__02(c_27type_2elist_2elist_27__01($c8),$c6),s__02(c_27type_2elist_2elist_27__01($c7),$c5),s__02(c_27type_2enum_2enum_27__00,$c2),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),$c1))). % 2.01/2.22 end_of_list. % 2.01/2.22 % 2.01/2.22 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=6. % 2.01/2.22 % 2.01/2.22 This ia a non-Horn set with equality. The strategy will be % 2.01/2.22 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.01/2.22 deletion, with positive clauses in sos and nonpositive % 2.01/2.22 clauses in usable. % 2.01/2.22 % 2.01/2.22 dependent: set(knuth_bendix). % 2.01/2.22 dependent: set(anl_eq). % 2.01/2.22 dependent: set(para_from). % 2.01/2.22 dependent: set(para_into). % 2.01/2.22 dependent: clear(para_from_right). % 2.01/2.22 dependent: clear(para_into_right). % 2.01/2.22 dependent: set(para_from_vars). % 2.01/2.22 dependent: set(eq_units_both_ways). % 2.01/2.22 dependent: set(dynamic_demod_all). % 2.01/2.22 dependent: set(dynamic_demod). % 2.01/2.22 dependent: set(order_eq). % 2.01/2.22 dependent: set(back_demod). % 2.01/2.22 dependent: set(lrpo). % 2.01/2.22 dependent: set(hyper_res). % 2.01/2.22 dependent: set(unit_deletion). % 2.01/2.22 dependent: set(factor). % 2.01/2.22 % 2.01/2.22 ------------> process usable: % 2.01/2.22 ** KEPT (pick-wt=4): 1 [] -p__01(s__02(cbool__00,cF__00)). % 2.01/2.22 ** KEPT (pick-wt=42): 2 [] s__02(A,chapp__02(s__02(cfun__02(B,A),C),s__02(B,$f1(B,A,C,D))))!=s__02(A,chapp__02(s__02(cfun__02(B,A),D),s__02(B,$f1(B,A,C,D))))|s__02(cfun__02(B,A),C)=s__02(cfun__02(B,A),D). % 2.01/2.22 ** KEPT (pick-wt=15): 3 [] -p__01(s__02(cbool__00,A))| -p__01(s__02(cbool__00,B))|s__02(cbool__00,B)=s__02(cbool__00,A). % 2.01/2.22 Following clause subsumed by 1 during input processing: 0 [] -p__01(s__02(cbool__00,cF__00))|p__01(s__02(cbool__00,A)). % 2.01/2.22 ** KEPT (pick-wt=8): 4 [] p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,A)). % 2.01/2.22 Following clause subsumed by 1 during input processing: 0 [] p__01(s__02(cbool__00,A))| -p__01(s__02(cbool__00,cF__00)). % 2.01/2.22 Following clause subsumed by 1 during input processing: 0 [] -p__01(s__02(cbool__00,cF__00))|p__01(s__02(cbool__00,A))| -p__01(s__02(cbool__00,cT__00)). % 2.01/2.22 Following clause subsumed by 1 during input processing: 0 [factor_simp] -p__01(s__02(cbool__00,cF__00)). % 2.01/2.22 ** KEPT (pick-wt=11): 5 [] s__02(A,B)!=s__02(A,B)|p__01(s__02(cbool__00,cT__00)). % 2.01/2.22 ** KEPT (pick-wt=11): 6 [] s__02(A,B)=s__02(A,B)| -p__01(s__02(cbool__00,cT__00)). % 2.01/2.22 ** KEPT (pick-wt=14): 7 [] s__02(A,B)!=s__02(A,C)|s__02(A,C)=s__02(A,B). % 2.01/2.22 Following clause subsumed by 7 during input processing: 0 [] s__02(A,B)=s__02(A,C)|s__02(A,C)!=s__02(A,B). % 2.01/2.22 ** KEPT (pick-wt=11): 8 [] s__02(cbool__00,cT__00)!=s__02(cbool__00,A)|p__01(s__02(cbool__00,A)). % 2.01/2.22 ** KEPT (pick-wt=11): 9 [] s__02(cbool__00,cT__00)=s__02(cbool__00,A)| -p__01(s__02(cbool__00,A)). % 2.01/2.22 ** KEPT (pick-wt=11): 10 [] s__02(cbool__00,A)!=s__02(cbool__00,cT__00)|p__01(s__02(cbool__00,A)). % 2.01/2.22 ** KEPT (pick-wt=11): 11 [] s__02(cbool__00,A)=s__02(cbool__00,cT__00)| -p__01(s__02(cbool__00,A)). % 2.01/2.22 ** KEPT (pick-wt=11): 12 [] s__02(cbool__00,cF__00)!=s__02(cbool__00,A)| -p__01(s__02(cbool__00,A)). % 2.01/2.22 ** KEPT (pick-wt=11): 13 [] s__02(cbool__00,A)!=s__02(cbool__00,cF__00)| -p__01(s__02(cbool__00,A)). % 2.01/2.22 ** KEPT (pick-wt=15): 14 [] s__02(cbool__00,A)!=s__02(cbool__00,B)| -p__01(s__02(cbool__00,A))|p__01(s__02(cbool__00,B)). % 2.01/2.22 ** KEPT (pick-wt=15): 15 [] s__02(cbool__00,A)!=s__02(cbool__00,B)| -p__01(s__02(cbool__00,B))|p__01(s__02(cbool__00,A)). % 2.01/2.22 Following clause subsumed by 3 during input processing: 0 [] s__02(cbool__00,A)=s__02(cbool__00,B)| -p__01(s__02(cbool__00,B))| -p__01(s__02(cbool__00,A)). % 2.01/2.22 Following clause subsumed by 14 during input processing: 0 [factor_simp] s__02(cbool__00,A)!=s__02(cbool__00,C)|p__01(s__02(cbool__00,C))| -p__01(s__02(cbool__00,A)). % 2.01/2.22 Following clause subsumed by 15 during input processing: 0 [] s__02(cbool__00,A)!=s__02(cbool__00,B)|s__02(cbool__00,C)!=s__02(cbool__00,D)|p__01(s__02(cbool__00,A))| -p__01(s__02(cbool__00,B))|p__01(s__02(cbool__00,D)). % 2.01/2.22 Following clause subsumed by 14 during input processing: 0 [] s__02(cbool__00,A)!=s__02(cbool__00,B)|s__02(cbool__00,C)!=s__02(cbool__00,D)| -p__01(s__02(cbool__00,C))| -p__01(s__02(cbool__00,B))|p__01(s__02(cbool__00,D)). % 2.01/2.22 Following clause subsumed by 15 during input processing: 0 [] s__02(cbool__00,A)!=s__02(cbool__00,B)|s__02(cbool__00,C)!=s__02(cbool__00,D)| -p__01(s__02(cbool__00,A))|p__01(s__02(cbool__00,C))| -p__01(s__02(cbool__00,D)). % 2.01/2.22 ** KEPT (pick-wt=43): 16 [] s__02(cbool__00,A)!=s__02(cbool__00,B)|p__01(s__02(cbool__00,B))|s__02(C,D)!=s__02(C,E)|s__02(C,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,A),s__02(C,F),s__02(C,D)))=s__02(C,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,B),s__02(C,G),s__02(C,E))). % 2.01/2.22 ** KEPT (pick-wt=43): 17 [] s__02(cbool__00,A)!=s__02(cbool__00,B)|s__02(C,D)!=s__02(C,E)| -p__01(s__02(cbool__00,B))|s__02(C,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,A),s__02(C,D),s__02(C,F)))=s__02(C,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,B),s__02(C,E),s__02(C,G))). % 2.01/2.22 ** KEPT (pick-wt=46): 18 [] s__02(cbool__00,A)!=s__02(cbool__00,B)|s__02(C,D)!=s__02(C,E)|s__02(C,F)!=s__02(C,G)|s__02(C,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,A),s__02(C,D),s__02(C,F)))=s__02(C,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,B),s__02(C,E),s__02(C,G))). % 2.01/2.22 ** KEPT (pick-wt=27): 19 [] -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,$f3(A,B,C)))))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,C)))). % 2.01/2.22 ** KEPT (pick-wt=31): 20 [] s__02(A,B)!=s__02(A,C)|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),D),s__02(A,B))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),D),s__02(A,C)))). % 2.01/2.22 ** KEPT (pick-wt=31): 21 [] p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,$f4(A,B,C)))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,D))))|p__01(s__02(cbool__00,C)). % 2.01/2.22 ** KEPT (pick-wt=31): 22 [] -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,C))))|p__01(s__02(cbool__00,D))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,$f5(A,B,D))))). % 2.01/2.22 ** KEPT (pick-wt=31): 23 [] -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,C))))| -p__01(s__02(cbool__00,D))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,$f6(A,B,D))))). % 2.01/2.22 ** KEPT (pick-wt=31): 24 [] p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,$f7(A,B,C)))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,D))))| -p__01(s__02(cbool__00,C)). % 2.01/2.22 ** KEPT (pick-wt=31): 25 [] -p__01(s__02(cbool__00,A))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(B,cbool__00),C),s__02(B,D))))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(B,cbool__00),C),s__02(B,$f8(B,C,A))))). % 2.01/2.22 ** KEPT (pick-wt=31): 26 [] p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,$f9(A,B,C)))))| -p__01(s__02(cbool__00,C))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,D)))). % 2.01/2.22 ** KEPT (pick-wt=34): 27 [] -p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(A,cfun__02(B,cbool__00)),C),s__02(c_27type_2elist_2elist_27__01(A),D),s__02(c_27type_2elist_2elist_27__01(B),E))))|s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(A),D)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(B),E))). % 2.01/2.22 ** KEPT (pick-wt=69): 28 [] -p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(A,cfun__02(B,cbool__00)),C),s__02(c_27type_2elist_2elist_27__01(A),D),s__02(c_27type_2elist_2elist_27__01(B),E))))| -p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,F),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(A),D))))))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(B,cbool__00),chapp__02(s__02(cfun__02(A,cfun__02(B,cbool__00)),C),s__02(A,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,F),s__02(c_27type_2elist_2elist_27__01(A),D))))),s__02(B,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,F),s__02(c_27type_2elist_2elist_27__01(B),E)))))). % 2.01/2.22 ** KEPT (pick-wt=53): 29 [] p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(A,cfun__02(B,cbool__00)),C),s__02(c_27type_2elist_2elist_27__01(A),D),s__02(c_27type_2elist_2elist_27__01(B),E))))|s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(A),D)))!=s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(B),E)))|p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,$f10(A,B,C,D,E)),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(A),D)))))). % 2.01/2.22 ** KEPT (pick-wt=80): 30 [] p__01(s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(A,cfun__02(B,cbool__00)),C),s__02(c_27type_2elist_2elist_27__01(A),D),s__02(c_27type_2elist_2elist_27__01(B),E))))|s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(A),D)))!=s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(B),E)))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(B,cbool__00),chapp__02(s__02(cfun__02(A,cfun__02(B,cbool__00)),C),s__02(A,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,$f10(A,B,C,D,E)),s__02(c_27type_2elist_2elist_27__01(A),D))))),s__02(B,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,$f10(A,B,C,D,E)),s__02(c_27type_2elist_2elist_27__01(B),E)))))). % 2.01/2.22 ** KEPT (pick-wt=33): 31 [] -p__01(s__02(cbool__00,c_27const_2ebool_2eIN_27__02(s__02(A,B),s__02(cfun__02(A,cbool__00),c_27const_2elist_2eLIST__TO__SET_27__01(s__02(c_27type_2elist_2elist_27__01(A),C))))))|p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,$f11(A,C,B)),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(A),C)))))). % 2.01/2.22 ** KEPT (pick-wt=33): 33 [copy,32,flip.2] -p__01(s__02(cbool__00,c_27const_2ebool_2eIN_27__02(s__02(A,B),s__02(cfun__02(A,cbool__00),c_27const_2elist_2eLIST__TO__SET_27__01(s__02(c_27type_2elist_2elist_27__01(A),C))))))|s__02(A,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,$f11(A,C,B)),s__02(c_27type_2elist_2elist_27__01(A),C)))=s__02(A,B). % 2.01/2.22 ** KEPT (pick-wt=44): 34 [] p__01(s__02(cbool__00,c_27const_2ebool_2eIN_27__02(s__02(A,B),s__02(cfun__02(A,cbool__00),c_27const_2elist_2eLIST__TO__SET_27__01(s__02(c_27type_2elist_2elist_27__01(A),C))))))| -p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,D),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(A),C))))))|s__02(A,B)!=s__02(A,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,D),s__02(c_27type_2elist_2elist_27__01(A),C))). % 2.01/2.22 ** KEPT (pick-wt=277): 35 [] s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),A),s__02(c_27type_2enum_2enum_27__00,$f15(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f14(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f13(B,C,A)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(B,C,A))))!=s__02(cbool__00,c_27const_2eclosProps_2efv1_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f15(B,C,A)),s__02(c_27type_2enum_2enum_27__00,$f14(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f13(B,C,A)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(B,C,A))))|s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),D),s__02(c_27type_2enum_2enum_27__00,$f18(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f17(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f16(B,C,A,D))))!=s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),A),s__02(c_27type_2enum_2enum_27__00,$f16(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f18(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f17(B,C,A,D))))| -p__01(s__02(cbool__00,$f21(B,C,A,D,E,F,G,H,I)))| -p__01(s__02(cbool__00,c_27const_2elist_2eEXISTS_27__02(s__02(cfun__02(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00),cbool__00),c_27const_2epair_2eUNCURRY_27__01(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),D),s__02(c_27type_2enum_2enum_27__00,H))),s__02(c_27type_2enum_2enum_27__00,J))))),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),I))))|p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,J),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(B),F)))))). % 2.01/2.23 ** KEPT (pick-wt=277): 36 [] s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),A),s__02(c_27type_2enum_2enum_27__00,$f15(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f14(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f13(B,C,A)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(B,C,A))))!=s__02(cbool__00,c_27const_2eclosProps_2efv1_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f15(B,C,A)),s__02(c_27type_2enum_2enum_27__00,$f14(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f13(B,C,A)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(B,C,A))))|s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),D),s__02(c_27type_2enum_2enum_27__00,$f18(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f17(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f16(B,C,A,D))))!=s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),A),s__02(c_27type_2enum_2enum_27__00,$f16(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f18(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f17(B,C,A,D))))| -p__01(s__02(cbool__00,$f21(B,C,A,D,E,F,G,H,I)))| -p__01(s__02(cbool__00,c_27const_2elist_2eEXISTS_27__02(s__02(cfun__02(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00),cbool__00),c_27const_2epair_2eUNCURRY_27__01(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),D),s__02(c_27type_2enum_2enum_27__00,H))),s__02(c_27type_2enum_2enum_27__00,J))))),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),I))))|p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,J),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(C),G)))))). % 2.01/2.23 ** KEPT (pick-wt=299): 37 [] s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),A),s__02(c_27type_2enum_2enum_27__00,$f15(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f14(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f13(B,C,A)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(B,C,A))))!=s__02(cbool__00,c_27const_2eclosProps_2efv1_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f15(B,C,A)),s__02(c_27type_2enum_2enum_27__00,$f14(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f13(B,C,A)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(B,C,A))))|s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),D),s__02(c_27type_2enum_2enum_27__00,$f18(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f17(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f16(B,C,A,D))))!=s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),A),s__02(c_27type_2enum_2enum_27__00,$f16(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f18(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f17(B,C,A,D))))| -p__01(s__02(cbool__00,$f21(B,C,A,D,E,F,G,H,I)))| -p__01(s__02(cbool__00,c_27const_2elist_2eEXISTS_27__02(s__02(cfun__02(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00),cbool__00),c_27const_2epair_2eUNCURRY_27__01(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),D),s__02(c_27type_2enum_2enum_27__00,H))),s__02(c_27type_2enum_2enum_27__00,J))))),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),I))))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(C,cbool__00),chapp__02(s__02(cfun__02(B,cfun__02(C,cbool__00)),E),s__02(B,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,J),s__02(c_27type_2elist_2elist_27__01(B),F))))),s__02(C,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,J),s__02(c_27type_2elist_2elist_27__01(C),G)))))). % 2.01/2.23 ** KEPT (pick-wt=272): 38 [] s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),A),s__02(c_27type_2enum_2enum_27__00,$f15(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f14(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f13(B,C,A)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(B,C,A))))!=s__02(cbool__00,c_27const_2eclosProps_2efv1_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f15(B,C,A)),s__02(c_27type_2enum_2enum_27__00,$f14(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f13(B,C,A)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(B,C,A))))|s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),D),s__02(c_27type_2enum_2enum_27__00,$f18(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f17(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f16(B,C,A,D))))!=s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),A),s__02(c_27type_2enum_2enum_27__00,$f16(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f18(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f17(B,C,A,D))))|p__01(s__02(cbool__00,$f21(B,C,A,D,E,F,G,H,I)))|p__01(s__02(cbool__00,c_27const_2elist_2eEXISTS_27__02(s__02(cfun__02(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00),cbool__00),c_27const_2epair_2eUNCURRY_27__01(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),D),s__02(c_27type_2enum_2enum_27__00,H))),s__02(c_27type_2enum_2enum_27__00,$f19(B,C,A,D,E,F,G,H,I)))))),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),I)))). % 2.01/2.23 ** KEPT (pick-wt=313): 39 [] s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),A),s__02(c_27type_2enum_2enum_27__00,$f15(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f14(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f13(B,C,A)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(B,C,A))))!=s__02(cbool__00,c_27const_2eclosProps_2efv1_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f15(B,C,A)),s__02(c_27type_2enum_2enum_27__00,$f14(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f13(B,C,A)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(B,C,A))))|s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),D),s__02(c_27type_2enum_2enum_27__00,$f18(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f17(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f16(B,C,A,D))))!=s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),A),s__02(c_27type_2enum_2enum_27__00,$f16(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f18(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f17(B,C,A,D))))|p__01(s__02(cbool__00,$f21(B,C,A,D,E,F,G,H,I)))| -p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,$f19(B,C,A,D,E,F,G,H,I)),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(B),F))))))| -p__01(s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,$f19(B,C,A,D,E,F,G,H,I)),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(C),G))))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(C,cbool__00),chapp__02(s__02(cfun__02(B,cfun__02(C,cbool__00)),E),s__02(B,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,$f19(B,C,A,D,E,F,G,H,I)),s__02(c_27type_2elist_2elist_27__01(B),F))))),s__02(C,c_27const_2elist_2eEL_27__02(s__02(c_27type_2enum_2enum_27__00,$f19(B,C,A,D,E,F,G,H,I)),s__02(c_27type_2elist_2elist_27__01(C),G)))))). % 2.01/2.23 ** KEPT (pick-wt=228): 40 [] s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),A),s__02(c_27type_2enum_2enum_27__00,$f15(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f14(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f13(B,C,A)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(B,C,A))))!=s__02(cbool__00,c_27const_2eclosProps_2efv1_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f15(B,C,A)),s__02(c_27type_2enum_2enum_27__00,$f14(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f13(B,C,A)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(B,C,A))))|s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),D),s__02(c_27type_2enum_2enum_27__00,$f18(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f17(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f16(B,C,A,D))))!=s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),A),s__02(c_27type_2enum_2enum_27__00,$f16(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f18(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f17(B,C,A,D))))| -p__01(s__02(cbool__00,$f20(B,C,A,D,E,F,G,H,I)))|s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(B),F)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(C),G))). % 2.01/2.23 ** KEPT (pick-wt=228): 41 [] s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),A),s__02(c_27type_2enum_2enum_27__00,$f15(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f14(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f13(B,C,A)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(B,C,A))))!=s__02(cbool__00,c_27const_2eclosProps_2efv1_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f15(B,C,A)),s__02(c_27type_2enum_2enum_27__00,$f14(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f13(B,C,A)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(B,C,A))))|s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),D),s__02(c_27type_2enum_2enum_27__00,$f18(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f17(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f16(B,C,A,D))))!=s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),A),s__02(c_27type_2enum_2enum_27__00,$f16(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f18(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f17(B,C,A,D))))|p__01(s__02(cbool__00,$f20(B,C,A,D,E,F,G,H,I)))|s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(B),F)))!=s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(C),G))). % 2.01/2.23 ** KEPT (pick-wt=273): 42 [] s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),A),s__02(c_27type_2enum_2enum_27__00,$f15(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f14(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f13(B,C,A)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(B,C,A))))!=s__02(cbool__00,c_27const_2eclosProps_2efv1_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f15(B,C,A)),s__02(c_27type_2enum_2enum_27__00,$f14(B,C,A)))),s__02(c_27type_2enum_2enum_27__00,$f13(B,C,A)))),s__02(c_27type_2eclosLang_2eexp_27__00,$f12(B,C,A))))|s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),D),s__02(c_27type_2enum_2enum_27__00,$f18(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f17(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f16(B,C,A,D))))!=s__02(cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00))),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2eclosLang_2eexp_27__00,cbool__00)))),A),s__02(c_27type_2enum_2enum_27__00,$f16(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f18(B,C,A,D)))),s__02(c_27type_2enum_2enum_27__00,$f17(B,C,A,D))))|s__02(cbool__00,c_27const_2eclos__callProof_2eenv__rel_27__05(s__02(cfun__02(B,cfun__02(C,cbool__00)),E),s__02(c_27type_2elist_2elist_27__01(B),F),s__02(c_27type_2elist_2elist_27__01(C),G),s__02(c_27type_2enum_2enum_27__00,H),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),I)))=s__02(cbool__00,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,$f20(B,C,A,D,E,F,G,H,I)),s__02(cbool__00,c_27const_2elist_2eLIST__REL_27__03(s__02(cfun__02(B,cfun__02(C,cbool__00)),E),s__02(c_27type_2elist_2elist_27__01(B),F),s__02(c_27type_2elist_2elist_27__01(C),G))),s__02(cbool__00,$f21(B,C,A,D,E,F,G,H,I)))). % 2.01/2.23 ** KEPT (pick-wt=75): 43 [] -p__01(s__02(cbool__00,c_27const_2ebool_2eIN_27__02(s__02($c8,A),s__02(cfun__02($c8,cbool__00),c_27const_2elist_2eLIST__TO__SET_27__01(s__02(c_27type_2elist_2elist_27__01($c8),$c6))))))| -p__01(s__02(cbool__00,c_27const_2ebool_2eIN_27__02(s__02($c7,B),s__02(cfun__02($c7,cbool__00),c_27const_2elist_2eLIST__TO__SET_27__01(s__02(c_27type_2elist_2elist_27__01($c7),$c5))))))|s__02(cbool__00,chapp__02(s__02(cfun__02($c7,cbool__00),chapp__02(s__02(cfun__02($c8,cfun__02($c7,cbool__00)),$c4),s__02($c8,A))),s__02($c7,B)))=s__02(cbool__00,chapp__02(s__02(cfun__02($c7,cbool__00),chapp__02(s__02(cfun__02($c8,cfun__02($c7,cbool__00)),$c3),s__02($c8,A))),s__02($c7,B))). % 2.01/2.23 ** KEPT (pick-wt=55): 44 [] s__02(cbool__00,c_27const_2eclos__callProof_2eenv__rel_27__05(s__02(cfun__02($c8,cfun__02($c7,cbool__00)),$c4),s__02(c_27type_2elist_2elist_27__01($c8),$c6),s__02(c_27type_2elist_2elist_27__01($c7),$c5),s__02(c_27type_2enum_2enum_27__00,$c2),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),$c1)))!=s__02(cbool__00,c_27const_2eclos__callProof_2eenv__rel_27__05(s__02(cfun__02($c8,cfun__02($c7,cbool__00)),$c3),s__02(c_27type_2elist_2elist_27__01($c8),$c6),s__02(c_27type_2elist_2elist_27__01($c7),$c5),s__02(c_27type_2enum_2enum_27__00,$c2),s__02(c_27type_2elist_2elist_27__01(c_27type_2epair_2eprod_27__02(c_27type_2enum_2enum_27__00,c_27type_2eclosLang_2eexp_27__00)),$c1))). % 2.01/2.23 % 2.01/2.23 ------------> process sos: % 2.01/2.23 ** KEPT (pick-wt=3): 57 [] A=A. % 2.01/2.23 ** KEPT (pick-wt=4): 58 [] p__01(s__02(cbool__00,cT__00)). % 2.01/2.23 ** KEPT (pick-wt=14): 59 [] s__02(cbool__00,A)=s__02(cbool__00,cT__00)|s__02(cbool__00,A)=s__02(cbool__00,cF__00). % 2.01/2.23 Following clause subsumed by 58 during input processing: 0 [] p__01(s__02(cbool__00,cT__00)). % 2.01/2.23 ** KEPT (pick-wt=15): 60 [] p__01(s__02(cbool__00,A))|p__01(s__02(cbool__00,B))|s__02(cbool__00,A)=s__02(cbool__00,B). % 2.01/2.23 Following clause subsumed by 58 during input processing: 0 [] p__01(s__02(cbool__00,cT__00)). % 2.01/2.23 ** KEPT (pick-wt=11): 61 [] s__02(cbool__00,cF__00)=s__02(cbool__00,A)|p__01(s__02(cbool__00,A)). % 2.01/2.23 ** KEPT (pick-wt=11): 62 [] s__02(cbool__00,A)=s__02(cbool__00,cF__00)|p__01(s__02(cbool__00,A)). % 2.01/2.23 ** KEPT (pick-wt=16): 63 [] s__02(A,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cT__00),s__02(A,B),s__02(A,C)))=s__02(A,B). % 2.01/2.23 ---> New Demodulator: 64 [new_demod,63] s__02(A,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cT__00),s__02(A,B),s__02(A,C)))=s__02(A,B). % 2.01/2.23 ** KEPT (pick-wt=16): 65 [] s__02(A,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cF__00),s__02(A,B),s__02(A,C)))=s__02(A,C). % 2.01/2.23 ---> New Demodulator: 66 [new_demod,65] s__02(A,c_27const_2ebool_2eCOND_27__03(s__02(cbool__00,cF__00),s__02(A,B),s__02(A,C)))=s__02(A,C). % 2.01/2.23 Following clause subsumed by 60 during input processing: 0 [] s__02(cbool__00,A)=s__02(cbool__00,B)|p__01(s__02(cbool__00,A))|p__01(s__02(cbool__00,B)). % 2.01/2.23 ** KEPT (pick-wt=22): 67 [] s__02(A,$f3(A,B,C))=s__02(A,C)|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,C)))). % 2.01/2.23 Following clause subsumed by 57 during input processing: 0 [demod,64] s__02(A,B)=s__02(A,B). % 2.01/2.23 Following clause subsumed by 57 during input processing: 0 [demod,66] s__02(A,C)=s__02(A,C). % 2.01/2.23 ** KEPT (pick-wt=19): 68 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,A))). % 2.01/2.23 ** KEPT (pick-wt=31): 69 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,C)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B))),s__02(c_27type_2enum_2enum_27__00,C))). % 2.18/2.35 Following clause subsumed by 57 during input processing: 0 [copy,57,flip.1] A=A. % 2.18/2.35 57 back subsumes 45. % 2.18/2.35 57 back subsumes 6. % 2.18/2.35 58 back subsumes 5. % 2.18/2.35 58 back subsumes 4. % 2.18/2.35 >>>> Starting back demodulation with 64. % 2.18/2.35 >>>> Starting back demodulation with 66. % 2.18/2.35 Following clause subsumed by 68 during input processing: 0 [copy,68,flip.1] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,A))). % 2.18/2.35 ** KEPT (pick-wt=31): 70 [copy,69,flip.1] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B))),s__02(c_27type_2enum_2enum_27__00,C)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,C))))). % 2.18/2.35 Following clause subsumed by 69 during input processing: 0 [copy,70,flip.1] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,C)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B))),s__02(c_27type_2enum_2enum_27__00,C))). % 2.18/2.35 % 2.18/2.35 ======= end of input processing ======= % 2.18/2.35 % 2.18/2.35 =========== start of search =========== % 2.18/2.35 % 2.18/2.35 % 2.18/2.35 Resetting weight limit to 4. % 2.18/2.35 % 2.18/2.35 % 2.18/2.35 Resetting weight limit to 4. % 2.18/2.35 % 2.18/2.35 sos_size=11 % 2.18/2.35 % 2.18/2.35 Search stopped because sos empty. % 2.18/2.35 % 2.18/2.35 % 2.18/2.35 Search stopped because sos empty. % 2.18/2.35 % 2.18/2.35 ============ end of search ============ % 2.18/2.35 % 2.18/2.35 -------------- statistics ------------- % 2.18/2.35 clauses given 12 % 2.18/2.35 clauses generated 3582 % 2.18/2.35 clauses kept 67 % 2.18/2.35 clauses forward subsumed 33 % 2.18/2.35 clauses back subsumed 4 % 2.18/2.35 Kbytes malloced 8789 % 2.18/2.35 % 2.18/2.35 ----------- times (seconds) ----------- % 2.18/2.35 user CPU time 0.13 (0 hr, 0 min, 0 sec) % 2.18/2.35 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 2.18/2.35 wall-clock time 2 (0 hr, 0 min, 2 sec) % 2.18/2.35 % 2.18/2.35 Process 32563 finished Wed Jul 27 03:06:08 2022 % 2.18/2.35 Otter interrupted % 2.18/2.35 PROOF NOT FOUND %------------------------------------------------------------------------------