%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWW924+1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jul 27 13:23:11 EDT 2022 % Result : Unknown 3.18s 3.33s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SWW924+1 : TPTP v8.1.0. Released v7.3.0. % 0.06/0.12 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n006.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 02:58:17 EDT 2022 % 0.12/0.33 % CPUTime : % 3.01/3.17 ----- Otter 3.3f, August 2004 ----- % 3.01/3.17 The process was started by sandbox on n006.cluster.edu, % 3.01/3.17 Wed Jul 27 02:58:17 2022 % 3.01/3.17 The command was "./otter". The process ID is 796. % 3.01/3.17 % 3.01/3.17 set(prolog_style_variables). % 3.01/3.17 set(auto). % 3.01/3.17 dependent: set(auto1). % 3.01/3.17 dependent: set(process_input). % 3.01/3.17 dependent: clear(print_kept). % 3.01/3.17 dependent: clear(print_new_demod). % 3.01/3.17 dependent: clear(print_back_demod). % 3.01/3.17 dependent: clear(print_back_sub). % 3.01/3.17 dependent: set(control_memory). % 3.01/3.17 dependent: assign(max_mem, 12000). % 3.01/3.17 dependent: assign(pick_given_ratio, 4). % 3.01/3.17 dependent: assign(stats_level, 1). % 3.01/3.17 dependent: assign(max_seconds, 10800). % 3.01/3.17 clear(print_given). % 3.01/3.17 % 3.01/3.17 formula_list(usable). % 3.01/3.17 all A (A=A). % 3.01/3.17 p__01(s__02(cbool__00,cT__00)). % 3.01/3.17 -p__01(s__02(cbool__00,cF__00)). % 3.01/3.17 all Vt (s__02(cbool__00,Vt)=s__02(cbool__00,cT__00)|s__02(cbool__00,Vt)=s__02(cbool__00,cF__00)). % 3.01/3.17 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)). % 3.01/3.17 p__01(s__02(cbool__00,cT__00)). % 3.01/3.17 all V_27B_27 V_27A_27 V_27M_27 Vx (s__02(V_27B_27,chapp__02(s__02(cfun__02(V_27A_27,V_27B_27),V_27M_27),s__02(V_27A_27,Vx)))=s__02(V_27B_27,chapp__02(s__02(cfun__02(V_27A_27,V_27B_27),V_27M_27),s__02(V_27A_27,Vx)))). % 3.01/3.17 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))). % 3.01/3.17 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))). % 3.01/3.17 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)))). % 3.01/3.17 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,cT__00)))& (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,V_27t_27)))& (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,V_27t_27))|p__01(s__02(cbool__00,V_27t_27))<->p__01(s__02(cbool__00,V_27t_27)))). % 3.01/3.17 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)))). % 3.01/3.17 all V_27t_27 (-(-p__01(s__02(cbool__00,V_27t_27)))<->p__01(s__02(cbool__00,V_27t_27))). % 3.01/3.17 -p__01(s__02(cbool__00,cT__00))<->p__01(s__02(cbool__00,cF__00)). % 3.01/3.17 -p__01(s__02(cbool__00,cF__00))<->p__01(s__02(cbool__00,cT__00)). % 3.01/3.17 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))). % 3.01/3.17 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)). % 3.01/3.17 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)))). % 3.01/3.17 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))). % 3.01/3.17 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)))& (-(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)))). % 3.01/3.17 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))). % 3.01/3.17 all V_27t_27 ((p__01(s__02(cbool__00,V_27t_27))->p__01(s__02(cbool__00,cF__00)))<->s__02(cbool__00,V_27t_27)=s__02(cbool__00,cF__00)). % 3.01/3.17 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)))). % 3.01/3.17 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))))). % 3.01/3.17 all V_27t_27 (-(-p__01(s__02(cbool__00,V_27t_27)))<->p__01(s__02(cbool__00,V_27t_27))). % 3.01/3.17 all V_27A_270 (p__01(s__02(cbool__00,V_27A_270))-> (-p__01(s__02(cbool__00,V_27A_270))->p__01(s__02(cbool__00,cF__00)))). % 3.01/3.17 all V_27B_270 V_27A_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,cF__00)))<-> ((p__01(s__02(cbool__00,V_27A_270))->p__01(s__02(cbool__00,cF__00)))-> (-p__01(s__02(cbool__00,V_27B_270))->p__01(s__02(cbool__00,cF__00))))). % 3.01/3.17 all V_27B_270 V_27A_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,cF__00)))<-> (p__01(s__02(cbool__00,V_27A_270))-> (-p__01(s__02(cbool__00,V_27B_270))->p__01(s__02(cbool__00,cF__00))))). % 3.01/3.17 all V_27A_270 ((-p__01(s__02(cbool__00,V_27A_270))->p__01(s__02(cbool__00,cF__00)))-> ((p__01(s__02(cbool__00,V_27A_270))->p__01(s__02(cbool__00,cF__00)))->p__01(s__02(cbool__00,cF__00)))). % 3.01/3.17 all V_27r_27 V_27q_27 V_27p_27 ((p__01(s__02(cbool__00,V_27p_27))<->s__02(cbool__00,V_27q_27)=s__02(cbool__00,V_27r_27))<-> (p__01(s__02(cbool__00,V_27p_27))|p__01(s__02(cbool__00,V_27q_27))|p__01(s__02(cbool__00,V_27r_27)))& (p__01(s__02(cbool__00,V_27p_27))| -p__01(s__02(cbool__00,V_27r_27))| -p__01(s__02(cbool__00,V_27q_27)))& (p__01(s__02(cbool__00,V_27q_27))| -p__01(s__02(cbool__00,V_27r_27))| -p__01(s__02(cbool__00,V_27p_27)))& (p__01(s__02(cbool__00,V_27r_27))| -p__01(s__02(cbool__00,V_27q_27))| -p__01(s__02(cbool__00,V_27p_27)))). % 3.01/3.17 all V_27r_27 V_27q_27 V_27p_27 ((p__01(s__02(cbool__00,V_27p_27))<->p__01(s__02(cbool__00,V_27q_27))&p__01(s__02(cbool__00,V_27r_27)))<-> (p__01(s__02(cbool__00,V_27p_27))| -p__01(s__02(cbool__00,V_27q_27))| -p__01(s__02(cbool__00,V_27r_27)))& (p__01(s__02(cbool__00,V_27q_27))| -p__01(s__02(cbool__00,V_27p_27)))& (p__01(s__02(cbool__00,V_27r_27))| -p__01(s__02(cbool__00,V_27p_27)))). % 3.01/3.17 all V_27r_27 V_27q_27 V_27p_27 ((p__01(s__02(cbool__00,V_27p_27))<->p__01(s__02(cbool__00,V_27q_27))|p__01(s__02(cbool__00,V_27r_27)))<-> (p__01(s__02(cbool__00,V_27p_27))| -p__01(s__02(cbool__00,V_27q_27)))& (p__01(s__02(cbool__00,V_27p_27))| -p__01(s__02(cbool__00,V_27r_27)))& (p__01(s__02(cbool__00,V_27q_27))|p__01(s__02(cbool__00,V_27r_27))| -p__01(s__02(cbool__00,V_27p_27)))). % 3.01/3.17 all V_27r_27 V_27q_27 V_27p_27 ((p__01(s__02(cbool__00,V_27p_27))<-> (p__01(s__02(cbool__00,V_27q_27))->p__01(s__02(cbool__00,V_27r_27))))<-> (p__01(s__02(cbool__00,V_27p_27))|p__01(s__02(cbool__00,V_27q_27)))& (p__01(s__02(cbool__00,V_27p_27))| -p__01(s__02(cbool__00,V_27r_27)))& (-p__01(s__02(cbool__00,V_27q_27))|p__01(s__02(cbool__00,V_27r_27))| -p__01(s__02(cbool__00,V_27p_27)))). % 3.01/3.17 all V_27q_27 V_27p_27 ((p__01(s__02(cbool__00,V_27p_27))<-> -p__01(s__02(cbool__00,V_27q_27)))<-> (p__01(s__02(cbool__00,V_27p_27))|p__01(s__02(cbool__00,V_27q_27)))& (-p__01(s__02(cbool__00,V_27q_27))| -p__01(s__02(cbool__00,V_27p_27)))). % 3.01/3.17 all V_27q_27 V_27p_27 (-(p__01(s__02(cbool__00,V_27p_27))->p__01(s__02(cbool__00,V_27q_27)))->p__01(s__02(cbool__00,V_27p_27))). % 3.01/3.17 all V_27q_27 V_27p_27 (-(p__01(s__02(cbool__00,V_27p_27))->p__01(s__02(cbool__00,V_27q_27)))-> -p__01(s__02(cbool__00,V_27q_27))). % 3.01/3.17 all V_27q_27 V_27p_27 (-(p__01(s__02(cbool__00,V_27p_27))|p__01(s__02(cbool__00,V_27q_27)))-> -p__01(s__02(cbool__00,V_27p_27))). % 3.01/3.17 all V_27q_27 V_27p_27 (-(p__01(s__02(cbool__00,V_27p_27))|p__01(s__02(cbool__00,V_27q_27)))-> -p__01(s__02(cbool__00,V_27q_27))). % 3.01/3.17 all V_27p_27 (-(-p__01(s__02(cbool__00,V_27p_27)))->p__01(s__02(cbool__00,V_27p_27))). % 3.01/3.17 all V_27A_27 V_27B_27 V_27x_27 V_27y_27 V_27a_27 V_27b_27 (s__02(c_27type_2epair_2eprod_27__02(V_27A_27,V_27B_27),c_27const_2epair_2e_2c_27__02(s__02(V_27A_27,V_27x_27),s__02(V_27B_27,V_27y_27)))=s__02(c_27type_2epair_2eprod_27__02(V_27A_27,V_27B_27),c_27const_2epair_2e_2c_27__02(s__02(V_27A_27,V_27a_27),s__02(V_27B_27,V_27b_27)))<->s__02(V_27A_27,V_27x_27)=s__02(V_27A_27,V_27a_27)&s__02(V_27B_27,V_27y_27)=s__02(V_27B_27,V_27b_27)). % 3.01/3.17 all 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_27m_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,V_27m_27)). % 3.01/3.17 all V_27n_27 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,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))=s__02(c_27type_2enum_2enum_27__00,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_27m_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,V_27m_27)&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_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27))),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(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_27m_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(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)))))). % 3.01/3.17 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)))). % 3.01/3.17 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)))). % 3.01/3.17 all V_27n_27 p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))). % 3.01/3.17 all V_27m_27 V_27n_27 p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,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)))))). % 3.01/3.17 all V_27m_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)&s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,V_27m_27)). % 3.01/3.17 all V_27m_27 V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)&s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)&s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))=s__02(c_27type_2enum_2enum_27__00,V_27m_27)&s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))=s__02(c_27type_2enum_2enum_27__00,V_27m_27)&s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(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,c_27const_2earithmetic_2e_2a_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_27n_27)))&s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(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_27m_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))). % 3.01/3.17 all V_27m_27 V_27n_27 V_27p_27 (p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))))&p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27p_27))))->p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27p_27))))). % 3.01/3.17 all V_27m_27 V_27n_27 (s__02(c_27type_2enum_2enum_27__00,V_27m_27)=s__02(c_27type_2enum_2enum_27__00,V_27n_27)<->p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))))&p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27))))). % 3.01/3.17 all V_27m_27 V_27n_27 V_27p_27 (s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_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,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_27p_27)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27p_27)))). % 3.01/3.17 all V_27m_27 V_27n_27 (s__02(c_27type_2enum_2enum_27__00,V_27m_27)!=s__02(c_27type_2enum_2enum_27__00,V_27n_27)<->p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27))),s__02(c_27type_2enum_2enum_27__00,V_27n_27))))|p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,V_27m_27))))). % 3.01/3.17 all V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(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,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))). % 3.01/3.17 all V_27b_27 V_27a_27 V_27P_27 (p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),V_27P_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27a_27),s__02(c_27type_2enum_2enum_27__00,V_27b_27))))))<-> (all V_27d_27 ((s__02(c_27type_2enum_2enum_27__00,V_27b_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_27a_27),s__02(c_27type_2enum_2enum_27__00,V_27d_27)))->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),V_27P_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))))& (s__02(c_27type_2enum_2enum_27__00,V_27a_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_27b_27),s__02(c_27type_2enum_2enum_27__00,V_27d_27)))->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27d_27)))))))). % 3.01/3.17 all 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,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(c_27type_2enum_2enum_27__00,V_27n_27)). % 3.01/3.17 all 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,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,V_27n_27)). % 3.01/3.17 all V_27n_27 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,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enumeral_2eiZ_27__01(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)))))))). % 3.01/3.17 all V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)). % 3.01/3.17 all V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)). % 3.01/3.17 all V_27n_27 V_27m_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))). % 3.01/3.17 all V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)). % 3.01/3.17 all V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,V_27n_27)). % 3.01/3.17 all V_27n_27 V_27m_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))). % 3.01/3.17 all V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)). % 3.01/3.17 all V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)). % 3.01/3.17 all V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))). % 3.01/3.17 all V_27n_27 V_27m_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))). % 3.01/3.17 s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))). % 3.01/3.17 all V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))). % 3.01/3.17 s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.17 all V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))). % 3.01/3.17 all V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)<->s__02(c_27type_2enum_2enum_27__00,V_27n_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)). % 3.01/3.17 all V_27n_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))<->s__02(c_27type_2enum_2enum_27__00,V_27n_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)). % 3.01/3.17 all V_27n_27 V_27m_27 (s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))<->s__02(c_27type_2enum_2enum_27__00,V_27n_27)=s__02(c_27type_2enum_2enum_27__00,V_27m_27)). % 3.01/3.17 all V_27n_27 (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_2enum_2e0_27__00)))=s__02(cbool__00,cF__00)). % 3.01/3.17 all V_27n_27 (s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))=s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))). % 3.01/3.17 all V_27n_27 V_27m_27 (s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=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,V_27m_27)))). % 3.01/3.17 all V_27n_27 (s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(cbool__00,cF__00)). % 3.01/3.17 all V_27n_27 (s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))). % 3.01/3.17 all V_27n_27 V_27m_27 (s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))). % 3.01/3.17 all V_27n_27 (s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(cbool__00,cT__00)). % 3.01/3.17 all V_27n_27 (s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))). % 3.01/3.17 all V_27n_27 V_27m_27 (s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))). % 3.01/3.17 all V_27n_27 (s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(cbool__00,cT__00)). % 3.01/3.17 all V_27n_27 (p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27))))<->s__02(c_27type_2enum_2enum_27__00,V_27n_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)). % 3.01/3.17 all V_27n_27 V_27m_27 (s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))). % 3.01/3.17 all V_27n_27 (s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))=s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))). % 3.01/3.17 all V_27n_27 (s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))=s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))). % 3.01/3.17 -p__01(s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))). % 3.01/3.17 p__01(s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))). % 3.01/3.17 all V_27n_27 V_27m_27 (s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(cbool__00,cT__00)&s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))=s__02(cbool__00,cF__00)&s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))=s__02(cbool__00,cF__00)&s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))&s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))& (p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27))))))<-> -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))&s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))). % 3.01/3.17 all V_27A_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),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l2_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_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_27A_27),V_27l2_27)))))). % 3.01/3.17 all V_27A_27 V_27l_27 (s__02(c_27type_2elist_2elist_27__01(V_27A_27),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l_27)))=s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l_27)). % 3.01/3.17 all V_27A_27 V_27n_27 V_27l_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),c_27const_2elist_2eDROP_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)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l_27))),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))). % 3.01/3.17 all V_27A_27 V_27l1_27 V_27l2_27 (s__02(c_27type_2elist_2elist_27__01(V_27A_27),c_27const_2elist_2eTAKE_27__02(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_2elist_2elist_27__01(V_27A_27),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l2_27)))))=s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27)). % 3.01/3.17 all V_27A_27 V_27B_27 ((all V_27a_27 V_27a_7c39_7c_27 (s__02(c_27type_2esemanticPrimitives_2eresult_27__02(V_27A_27,V_27B_27),c_27const_2esemanticPrimitives_2eRval_27__01(s__02(V_27A_27,V_27a_27)))=s__02(c_27type_2esemanticPrimitives_2eresult_27__02(V_27A_27,V_27B_27),c_27const_2esemanticPrimitives_2eRval_27__01(s__02(V_27A_27,V_27a_7c39_7c_27)))<->s__02(V_27A_27,V_27a_27)=s__02(V_27A_27,V_27a_7c39_7c_27)))& (all V_27a_27 V_27a_7c39_7c_27 (s__02(c_27type_2esemanticPrimitives_2eresult_27__02(V_27A_27,V_27B_27),c_27const_2esemanticPrimitives_2eRerr_27__01(s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(V_27B_27),V_27a_27)))=s__02(c_27type_2esemanticPrimitives_2eresult_27__02(V_27A_27,V_27B_27),c_27const_2esemanticPrimitives_2eRerr_27__01(s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(V_27B_27),V_27a_7c39_7c_27)))<->s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(V_27B_27),V_27a_27)=s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(V_27B_27),V_27a_7c39_7c_27)))). % 3.01/3.17 all V_27A_27 V__0 ((all V_27skip_27 V_27arg_27 (s__02(c_27type_2ebvl_2eexp_27__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00)),V__0),s__02(c_27type_2enum_2enum_27__00,V_27skip_27))),s__02(c_27type_2enum_2enum_27__00,V_27arg_27)))=s__02(c_27type_2ebvl_2eexp_27__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00),c_27const_2ebvl_2eVar_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,V_27arg_27),s__02(c_27type_2enum_2enum_27__00,V_27skip_27)))))))-> (all V_27skip_27 V_27env_27 V_27n_27 V_27st_27 (p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_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_27skip_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),V_27env_27))))))->s__02(c_27type_2epair_2eprod_27__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01(V_27A_27)),c_27const_2ebvlSem_2eevaluate_27__01(s__02(c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01(V_27A_27))),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eGENLIST_27__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00)),V__0),s__02(c_27type_2enum_2enum_27__00,V_27skip_27))),s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01(V_27A_27)),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),V_27env_27),s__02(c_27type_2ebvlSem_2estate_27__01(V_27A_27),V_27st_27)))))))=s__02(c_27type_2epair_2eprod_27__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01(V_27A_27)),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27const_2esemanticPrimitives_2eRval_27__01(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,V_27skip_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),V_27env_27))))))),s__02(c_27type_2ebvlSem_2estate_27__01(V_27A_27),V_27st_27)))))). % 3.01/3.18 -(all V_27A_27 V_27num__args_27 V_27args_7c39_7c_27 V_27stuff_27 V_27t1_27 (p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27num__args_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),V_27args_7c39_7c_27))))))->s__02(c_27type_2epair_2eprod_27__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01(V_27A_27)),c_27const_2ebvlSem_2eevaluate_27__01(s__02(c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01(V_27A_27))),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eGENLIST_27__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00),c_27const_2ebvl_2eVar_27__00),s__02(c_27type_2enum_2enum_27__00,V_27num__args_27))),s__02(c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01(V_27A_27)),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),V_27args_7c39_7c_27))),s__02(c_27type_2enum_2enum_27__00,V_27num__args_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),V_27args_7c39_7c_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),V_27stuff_27))),s__02(c_27type_2ebvlSem_2estate_27__01(V_27A_27),V_27t1_27)))))))=s__02(c_27type_2epair_2eprod_27__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01(V_27A_27)),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27const_2esemanticPrimitives_2eRval_27__01(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),V_27args_7c39_7c_27))),s__02(c_27type_2enum_2enum_27__00,V_27num__args_27))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),V_27args_7c39_7c_27))))),s__02(c_27type_2ebvlSem_2estate_27__01(V_27A_27),V_27t1_27))))). % 3.01/3.18 end_of_list. % 3.01/3.18 % 3.01/3.18 -------> usable clausifies to: % 3.01/3.18 % 3.01/3.18 list(usable). % 3.01/3.18 0 [] A=A. % 3.01/3.18 0 [] p__01(s__02(cbool__00,cT__00)). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,cF__00)). % 3.01/3.18 0 [] s__02(cbool__00,Vt)=s__02(cbool__00,cT__00)|s__02(cbool__00,Vt)=s__02(cbool__00,cF__00). % 3.01/3.18 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). % 3.01/3.18 0 [] p__01(s__02(cbool__00,cT__00)). % 3.01/3.18 0 [] s__02(V_27B_27,chapp__02(s__02(cfun__02(V_27A_27,V_27B_27),V_27M_27),s__02(V_27A_27,Vx)))=s__02(V_27B_27,chapp__02(s__02(cfun__02(V_27A_27,V_27B_27),V_27M_27),s__02(V_27A_27,Vx))). % 3.01/3.18 0 [] p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,V_27t_27)). % 3.01/3.18 0 [] p__01(s__02(cbool__00,V_27t_27))| -p__01(s__02(cbool__00,cF__00)). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,V_27t_27))|p__01(s__02(cbool__00,cT__00)). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,cF__00))|p__01(s__02(cbool__00,V_27t_27)). % 3.01/3.18 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)). % 3.01/3.18 0 [] p__01(s__02(cbool__00,cT__00)). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,cF__00))| -p__01(s__02(cbool__00,V_27t_27)). % 3.01/3.18 0 [] p__01(s__02(cbool__00,cT__00))|p__01(s__02(cbool__00,cF__00)). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,cF__00)). % 3.01/3.18 0 [] p__01(s__02(cbool__00,cF__00))|p__01(s__02(cbool__00,cT__00)). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,cF__00))| -p__01(s__02(cbool__00,cT__00)). % 3.01/3.18 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)). % 3.01/3.18 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)). % 3.01/3.18 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). % 3.01/3.18 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). % 3.01/3.18 0 [] s__02(cbool__00,cT__00)!=s__02(cbool__00,V_27t_27)|p__01(s__02(cbool__00,V_27t_27)). % 3.01/3.18 0 [] s__02(cbool__00,cT__00)=s__02(cbool__00,V_27t_27)| -p__01(s__02(cbool__00,V_27t_27)). % 3.01/3.18 0 [] s__02(cbool__00,V_27t_27)!=s__02(cbool__00,cT__00)|p__01(s__02(cbool__00,V_27t_27)). % 3.01/3.18 0 [] s__02(cbool__00,V_27t_27)=s__02(cbool__00,cT__00)| -p__01(s__02(cbool__00,V_27t_27)). % 3.01/3.18 0 [] s__02(cbool__00,cF__00)!=s__02(cbool__00,V_27t_27)| -p__01(s__02(cbool__00,V_27t_27)). % 3.01/3.18 0 [] s__02(cbool__00,cF__00)=s__02(cbool__00,V_27t_27)|p__01(s__02(cbool__00,V_27t_27)). % 3.01/3.18 0 [] s__02(cbool__00,V_27t_27)!=s__02(cbool__00,cF__00)| -p__01(s__02(cbool__00,V_27t_27)). % 3.01/3.18 0 [] s__02(cbool__00,V_27t_27)=s__02(cbool__00,cF__00)|p__01(s__02(cbool__00,V_27t_27)). % 3.01/3.18 0 [] p__01(s__02(cbool__00,V_27t_27))|s__02(cbool__00,V_27t_27)=s__02(cbool__00,cF__00). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,cF__00))|s__02(cbool__00,V_27t_27)=s__02(cbool__00,cF__00). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,V_27t_27))|p__01(s__02(cbool__00,cF__00))|s__02(cbool__00,V_27t_27)!=s__02(cbool__00,cF__00). % 3.01/3.18 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)). % 3.01/3.18 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)). % 3.01/3.18 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)). % 3.01/3.18 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)). % 3.01/3.18 0 [] p__01(s__02(cbool__00,V_27p_27))|s__02(cbool__00,V_27q_27)=s__02(cbool__00,V_27r_27)|p__01(s__02(cbool__00,V_27q_27))|p__01(s__02(cbool__00,V_27r_27)). % 3.01/3.18 0 [] p__01(s__02(cbool__00,V_27p_27))|s__02(cbool__00,V_27q_27)=s__02(cbool__00,V_27r_27)| -p__01(s__02(cbool__00,V_27r_27))| -p__01(s__02(cbool__00,V_27q_27)). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,V_27p_27))|s__02(cbool__00,V_27q_27)!=s__02(cbool__00,V_27r_27)|p__01(s__02(cbool__00,V_27q_27))| -p__01(s__02(cbool__00,V_27r_27)). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,V_27p_27))|s__02(cbool__00,V_27q_27)!=s__02(cbool__00,V_27r_27)|p__01(s__02(cbool__00,V_27r_27))| -p__01(s__02(cbool__00,V_27q_27)). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,V_27p_27))|s__02(cbool__00,V_27q_27)=s__02(cbool__00,V_27r_27)| -p__01(s__02(cbool__00,V_27q_27))| -p__01(s__02(cbool__00,V_27r_27)). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,V_27p_27))|s__02(cbool__00,V_27q_27)=s__02(cbool__00,V_27r_27)|p__01(s__02(cbool__00,V_27r_27))|p__01(s__02(cbool__00,V_27q_27)). % 3.01/3.18 0 [] p__01(s__02(cbool__00,V_27p_27))|s__02(cbool__00,V_27q_27)!=s__02(cbool__00,V_27r_27)| -p__01(s__02(cbool__00,V_27q_27))|p__01(s__02(cbool__00,V_27r_27)). % 3.01/3.18 0 [] p__01(s__02(cbool__00,V_27p_27))|s__02(cbool__00,V_27q_27)!=s__02(cbool__00,V_27r_27)| -p__01(s__02(cbool__00,V_27r_27))|p__01(s__02(cbool__00,V_27q_27)). % 3.01/3.18 0 [] s__02(c_27type_2epair_2eprod_27__02(V_27A_27,V_27B_27),c_27const_2epair_2e_2c_27__02(s__02(V_27A_27,V_27x_27),s__02(V_27B_27,V_27y_27)))!=s__02(c_27type_2epair_2eprod_27__02(V_27A_27,V_27B_27),c_27const_2epair_2e_2c_27__02(s__02(V_27A_27,V_27a_27),s__02(V_27B_27,V_27b_27)))|s__02(V_27A_27,V_27x_27)=s__02(V_27A_27,V_27a_27). % 3.01/3.18 0 [] s__02(c_27type_2epair_2eprod_27__02(V_27A_27,V_27B_27),c_27const_2epair_2e_2c_27__02(s__02(V_27A_27,V_27x_27),s__02(V_27B_27,V_27y_27)))!=s__02(c_27type_2epair_2eprod_27__02(V_27A_27,V_27B_27),c_27const_2epair_2e_2c_27__02(s__02(V_27A_27,V_27a_27),s__02(V_27B_27,V_27b_27)))|s__02(V_27B_27,V_27y_27)=s__02(V_27B_27,V_27b_27). % 3.01/3.18 0 [] s__02(c_27type_2epair_2eprod_27__02(V_27A_27,V_27B_27),c_27const_2epair_2e_2c_27__02(s__02(V_27A_27,V_27x_27),s__02(V_27B_27,V_27y_27)))=s__02(c_27type_2epair_2eprod_27__02(V_27A_27,V_27B_27),c_27const_2epair_2e_2c_27__02(s__02(V_27A_27,V_27a_27),s__02(V_27B_27,V_27b_27)))|s__02(V_27A_27,V_27x_27)!=s__02(V_27A_27,V_27a_27)|s__02(V_27B_27,V_27y_27)!=s__02(V_27B_27,V_27b_27). % 3.01/3.18 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_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,V_27m_27). % 3.01/3.18 0 [] 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_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))=s__02(c_27type_2enum_2enum_27__00,V_27m_27). % 3.01/3.18 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_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,V_27m_27). % 3.01/3.18 0 [] 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_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27))),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(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))))). % 3.01/3.18 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_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(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))))). % 3.01/3.18 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))). % 3.01/3.18 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))). % 3.01/3.18 0 [] p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))). % 3.01/3.18 0 [] p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,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)))))). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,V_27m_27). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))=s__02(c_27type_2enum_2enum_27__00,V_27m_27). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))=s__02(c_27type_2enum_2enum_27__00,V_27m_27). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(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,c_27const_2earithmetic_2e_2a_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_27n_27))). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(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_27m_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))))). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))))| -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27p_27))))|p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27p_27)))). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,V_27m_27)!=s__02(c_27type_2enum_2enum_27__00,V_27n_27)|p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,V_27m_27)!=s__02(c_27type_2enum_2enum_27__00,V_27n_27)|p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,V_27m_27)=s__02(c_27type_2enum_2enum_27__00,V_27n_27)| -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))))| -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_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,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_27p_27)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27p_27))). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,V_27m_27)=s__02(c_27type_2enum_2enum_27__00,V_27n_27)|p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27))),s__02(c_27type_2enum_2enum_27__00,V_27n_27))))|p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,V_27m_27)!=s__02(c_27type_2enum_2enum_27__00,V_27n_27)| -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27))),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,V_27m_27)!=s__02(c_27type_2enum_2enum_27__00,V_27n_27)| -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,V_27m_27)))). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(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,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,V_27n_27))). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),V_27P_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27a_27),s__02(c_27type_2enum_2enum_27__00,V_27b_27))))))|s__02(c_27type_2enum_2enum_27__00,V_27b_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_27a_27),s__02(c_27type_2enum_2enum_27__00,V_27d_27)))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),V_27P_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),V_27P_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27a_27),s__02(c_27type_2enum_2enum_27__00,V_27b_27))))))|s__02(c_27type_2enum_2enum_27__00,V_27a_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_27b_27),s__02(c_27type_2enum_2enum_27__00,V_27d_27)))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),V_27P_27),s__02(c_27type_2enum_2enum_27__00,V_27d_27)))). % 3.01/3.18 0 [] p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),V_27P_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27a_27),s__02(c_27type_2enum_2enum_27__00,V_27b_27))))))|s__02(c_27type_2enum_2enum_27__00,V_27b_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_27a_27),s__02(c_27type_2enum_2enum_27__00,$f3(V_27b_27,V_27a_27,V_27P_27))))|s__02(c_27type_2enum_2enum_27__00,V_27a_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_27b_27),s__02(c_27type_2enum_2enum_27__00,$f3(V_27b_27,V_27a_27,V_27P_27)))). % 3.01/3.18 0 [] p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),V_27P_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27a_27),s__02(c_27type_2enum_2enum_27__00,V_27b_27))))))|s__02(c_27type_2enum_2enum_27__00,V_27b_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_27a_27),s__02(c_27type_2enum_2enum_27__00,$f3(V_27b_27,V_27a_27,V_27P_27))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),V_27P_27),s__02(c_27type_2enum_2enum_27__00,$f3(V_27b_27,V_27a_27,V_27P_27))))). % 3.01/3.18 0 [] p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),V_27P_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27a_27),s__02(c_27type_2enum_2enum_27__00,V_27b_27))))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),V_27P_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))))|s__02(c_27type_2enum_2enum_27__00,V_27a_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_27b_27),s__02(c_27type_2enum_2enum_27__00,$f3(V_27b_27,V_27a_27,V_27P_27)))). % 3.01/3.18 0 [] p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),V_27P_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27a_27),s__02(c_27type_2enum_2enum_27__00,V_27b_27))))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),V_27P_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),V_27P_27),s__02(c_27type_2enum_2enum_27__00,$f3(V_27b_27,V_27a_27,V_27P_27))))). % 3.01/3.18 0 [] 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_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(c_27type_2enum_2enum_27__00,V_27n_27). % 3.01/3.18 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_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,V_27n_27). % 3.01/3.18 0 [] 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_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enumeral_2eiZ_27__01(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))))))). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27))))). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,V_27n_27). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27))))). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27))))). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))))). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))))). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)|s__02(c_27type_2enum_2enum_27__00,V_27n_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)|s__02(c_27type_2enum_2enum_27__00,V_27n_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))|s__02(c_27type_2enum_2enum_27__00,V_27n_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))|s__02(c_27type_2enum_2enum_27__00,V_27n_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))!=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))|s__02(c_27type_2enum_2enum_27__00,V_27n_27)=s__02(c_27type_2enum_2enum_27__00,V_27m_27). % 3.01/3.18 0 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))|s__02(c_27type_2enum_2enum_27__00,V_27n_27)!=s__02(c_27type_2enum_2enum_27__00,V_27m_27). % 3.01/3.18 0 [] 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_2enum_2e0_27__00)))=s__02(cbool__00,cF__00). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))=s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27))). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=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,V_27m_27))). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(cbool__00,cF__00). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27))). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(cbool__00,cT__00). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27))). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(cbool__00,cT__00). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27))))|s__02(c_27type_2enum_2enum_27__00,V_27n_27)=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 0 [] p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27))))|s__02(c_27type_2enum_2enum_27__00,V_27n_27)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27))). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))=s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27)))))=s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))). % 3.01/3.18 0 [] p__01(s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))=s__02(cbool__00,cT__00). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))=s__02(cbool__00,cF__00). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))=s__02(cbool__00,cF__00). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27))). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27))). % 3.01/3.18 0 [] -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27))))))| -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))). % 3.01/3.18 0 [] p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27))))))|p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27m_27),s__02(c_27type_2enum_2enum_27__00,V_27n_27)))). % 3.01/3.18 0 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,V_27m_27)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2enum_2enum_27__00,V_27m_27))). % 3.01/3.18 0 [] 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),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l2_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_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_27A_27),V_27l2_27))))). % 3.01/3.18 0 [] s__02(c_27type_2elist_2elist_27__01(V_27A_27),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l_27)))=s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l_27). % 3.01/3.18 0 [] 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),c_27const_2elist_2eDROP_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)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l_27))),s__02(c_27type_2enum_2enum_27__00,V_27n_27))). % 3.01/3.18 0 [] s__02(c_27type_2elist_2elist_27__01(V_27A_27),c_27const_2elist_2eTAKE_27__02(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_2elist_2elist_27__01(V_27A_27),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27),s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l2_27)))))=s__02(c_27type_2elist_2elist_27__01(V_27A_27),V_27l1_27). % 3.01/3.18 0 [] s__02(c_27type_2esemanticPrimitives_2eresult_27__02(V_27A_27,V_27B_27),c_27const_2esemanticPrimitives_2eRval_27__01(s__02(V_27A_27,V_27a_27)))!=s__02(c_27type_2esemanticPrimitives_2eresult_27__02(V_27A_27,V_27B_27),c_27const_2esemanticPrimitives_2eRval_27__01(s__02(V_27A_27,V_27a_7c39_7c_27)))|s__02(V_27A_27,V_27a_27)=s__02(V_27A_27,V_27a_7c39_7c_27). % 3.01/3.18 0 [] s__02(c_27type_2esemanticPrimitives_2eresult_27__02(V_27A_27,V_27B_27),c_27const_2esemanticPrimitives_2eRval_27__01(s__02(V_27A_27,V_27a_27)))=s__02(c_27type_2esemanticPrimitives_2eresult_27__02(V_27A_27,V_27B_27),c_27const_2esemanticPrimitives_2eRval_27__01(s__02(V_27A_27,V_27a_7c39_7c_27)))|s__02(V_27A_27,V_27a_27)!=s__02(V_27A_27,V_27a_7c39_7c_27). % 3.01/3.18 0 [] s__02(c_27type_2esemanticPrimitives_2eresult_27__02(V_27A_27,V_27B_27),c_27const_2esemanticPrimitives_2eRerr_27__01(s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(V_27B_27),X1)))!=s__02(c_27type_2esemanticPrimitives_2eresult_27__02(V_27A_27,V_27B_27),c_27const_2esemanticPrimitives_2eRerr_27__01(s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(V_27B_27),X2)))|s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(V_27B_27),X1)=s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(V_27B_27),X2). % 3.01/3.18 0 [] s__02(c_27type_2esemanticPrimitives_2eresult_27__02(V_27A_27,V_27B_27),c_27const_2esemanticPrimitives_2eRerr_27__01(s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(V_27B_27),X1)))=s__02(c_27type_2esemanticPrimitives_2eresult_27__02(V_27A_27,V_27B_27),c_27const_2esemanticPrimitives_2eRerr_27__01(s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(V_27B_27),X2)))|s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(V_27B_27),X1)!=s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(V_27B_27),X2). % 3.01/3.18 0 [] s__02(c_27type_2ebvl_2eexp_27__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00)),V__0),s__02(c_27type_2enum_2enum_27__00,$f5(V_27A_27,V__0)))),s__02(c_27type_2enum_2enum_27__00,$f4(V_27A_27,V__0))))!=s__02(c_27type_2ebvl_2eexp_27__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00),c_27const_2ebvl_2eVar_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f4(V_27A_27,V__0)),s__02(c_27type_2enum_2enum_27__00,$f5(V_27A_27,V__0))))))| -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_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_27skip_27))),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),V_27env_27))))))|s__02(c_27type_2epair_2eprod_27__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01(V_27A_27)),c_27const_2ebvlSem_2eevaluate_27__01(s__02(c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01(V_27A_27))),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eGENLIST_27__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00)),V__0),s__02(c_27type_2enum_2enum_27__00,V_27skip_27))),s__02(c_27type_2enum_2enum_27__00,V_27n_27))),s__02(c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01(V_27A_27)),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),V_27env_27),s__02(c_27type_2ebvlSem_2estate_27__01(V_27A_27),V_27st_27)))))))=s__02(c_27type_2epair_2eprod_27__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01(V_27A_27)),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27const_2esemanticPrimitives_2eRval_27__01(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,V_27n_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,V_27skip_27),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),V_27env_27))))))),s__02(c_27type_2ebvlSem_2estate_27__01(V_27A_27),V_27st_27))). % 3.01/3.18 0 [] p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,$c4),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),$c3)))))). % 3.01/3.18 0 [] s__02(c_27type_2epair_2eprod_27__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01($c5)),c_27const_2ebvlSem_2eevaluate_27__01(s__02(c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01($c5))),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eGENLIST_27__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00),c_27const_2ebvl_2eVar_27__00),s__02(c_27type_2enum_2enum_27__00,$c4))),s__02(c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01($c5)),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),$c3))),s__02(c_27type_2enum_2enum_27__00,$c4))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),$c3))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),$c2))),s__02(c_27type_2ebvlSem_2estate_27__01($c5),$c1)))))))!=s__02(c_27type_2epair_2eprod_27__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01($c5)),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27const_2esemanticPrimitives_2eRval_27__01(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),$c3))),s__02(c_27type_2enum_2enum_27__00,$c4))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),$c3))))),s__02(c_27type_2ebvlSem_2estate_27__01($c5),$c1))). % 3.01/3.18 end_of_list. % 3.01/3.18 % 3.01/3.18 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=5. % 3.01/3.18 % 3.01/3.18 This ia a non-Horn set with equality. The strategy will be % 3.01/3.18 Knuth-Bendix, ordered hyper_res, factoring, and unit % 3.01/3.18 deletion, with positive clauses in sos and nonpositive % 3.01/3.18 clauses in usable. % 3.01/3.18 % 3.01/3.18 dependent: set(knuth_bendix). % 3.01/3.18 dependent: set(anl_eq). % 3.01/3.18 dependent: set(para_from). % 3.01/3.18 dependent: set(para_into). % 3.01/3.18 dependent: clear(para_from_right). % 3.01/3.18 dependent: clear(para_into_right). % 3.01/3.18 dependent: set(para_from_vars). % 3.01/3.18 dependent: set(eq_units_both_ways). % 3.01/3.18 dependent: set(dynamic_demod_all). % 3.01/3.18 dependent: set(dynamic_demod). % 3.01/3.18 dependent: set(order_eq). % 3.01/3.18 dependent: set(back_demod). % 3.01/3.18 dependent: set(lrpo). % 3.01/3.18 dependent: set(hyper_res). % 3.01/3.18 dependent: set(unit_deletion). % 3.01/3.18 dependent: set(factor). % 3.01/3.18 % 3.01/3.18 ------------> process usable: % 3.01/3.18 ** KEPT (pick-wt=4): 1 [] -p__01(s__02(cbool__00,cF__00)). % 3.01/3.18 ** 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). % 3.01/3.18 ** KEPT (pick-wt=8): 3 [] p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,A)). % 3.01/3.18 Following clause subsumed by 1 during input processing: 0 [] p__01(s__02(cbool__00,A))| -p__01(s__02(cbool__00,cF__00)). % 3.01/3.18 Following clause subsumed by 3 during input processing: 0 [] -p__01(s__02(cbool__00,A))|p__01(s__02(cbool__00,cT__00)). % 3.01/3.18 Following clause subsumed by 1 during input processing: 0 [] -p__01(s__02(cbool__00,cF__00))|p__01(s__02(cbool__00,A)). % 3.01/3.18 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)). % 3.01/3.18 Following clause subsumed by 1 during input processing: 0 [factor_simp] -p__01(s__02(cbool__00,cF__00)). % 3.01/3.18 Following clause subsumed by 1 during input processing: 0 [] -p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,cF__00)). % 3.01/3.18 Following clause subsumed by 1 during input processing: 0 [] -p__01(s__02(cbool__00,cF__00))| -p__01(s__02(cbool__00,cT__00)). % 3.01/3.18 ** KEPT (pick-wt=11): 4 [] s__02(A,B)!=s__02(A,B)|p__01(s__02(cbool__00,cT__00)). % 3.01/3.18 ** KEPT (pick-wt=11): 5 [] s__02(A,B)=s__02(A,B)| -p__01(s__02(cbool__00,cT__00)). % 3.01/3.18 ** KEPT (pick-wt=14): 6 [] s__02(A,B)!=s__02(A,C)|s__02(A,C)=s__02(A,B). % 3.01/3.18 Following clause subsumed by 6 during input processing: 0 [] s__02(A,B)=s__02(A,C)|s__02(A,C)!=s__02(A,B). % 3.01/3.18 ** KEPT (pick-wt=11): 7 [] s__02(cbool__00,cT__00)!=s__02(cbool__00,A)|p__01(s__02(cbool__00,A)). % 3.01/3.18 ** KEPT (pick-wt=11): 8 [] s__02(cbool__00,cT__00)=s__02(cbool__00,A)| -p__01(s__02(cbool__00,A)). % 3.01/3.18 ** KEPT (pick-wt=11): 9 [] s__02(cbool__00,A)!=s__02(cbool__00,cT__00)|p__01(s__02(cbool__00,A)). % 3.01/3.18 ** KEPT (pick-wt=11): 10 [] s__02(cbool__00,A)=s__02(cbool__00,cT__00)| -p__01(s__02(cbool__00,A)). % 3.01/3.18 ** KEPT (pick-wt=11): 11 [] s__02(cbool__00,cF__00)!=s__02(cbool__00,A)| -p__01(s__02(cbool__00,A)). % 3.01/3.18 ** KEPT (pick-wt=11): 12 [] s__02(cbool__00,A)!=s__02(cbool__00,cF__00)| -p__01(s__02(cbool__00,A)). % 3.01/3.18 Following clause subsumed by 1 during input processing: 0 [] -p__01(s__02(cbool__00,cF__00))|s__02(cbool__00,A)=s__02(cbool__00,cF__00). % 3.01/3.18 Following clause subsumed by 12 during input processing: 0 [unit_del,1] -p__01(s__02(cbool__00,A))|s__02(cbool__00,A)!=s__02(cbool__00,cF__00). % 3.01/3.18 ** KEPT (pick-wt=15): 14 [copy,13,factor_simp] s__02(cbool__00,A)!=s__02(cbool__00,B)|p__01(s__02(cbool__00,B))| -p__01(s__02(cbool__00,A)). % 3.01/3.18 ** KEPT (pick-wt=26): 15 [] 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)). % 3.01/3.18 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)). % 3.01/3.18 ** KEPT (pick-wt=26): 16 [] 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)). % 3.01/3.18 ** KEPT (pick-wt=19): 17 [] p__01(s__02(cbool__00,A))|s__02(cbool__00,B)=s__02(cbool__00,C)| -p__01(s__02(cbool__00,C))| -p__01(s__02(cbool__00,B)). % 3.01/3.18 ** KEPT (pick-wt=15): 19 [copy,18,factor_simp] -p__01(s__02(cbool__00,A))|s__02(cbool__00,B)!=s__02(cbool__00,A)|p__01(s__02(cbool__00,B)). % 3.01/3.18 Following clause subsumed by 14 during input processing: 0 [factor_simp] -p__01(s__02(cbool__00,B))|s__02(cbool__00,B)!=s__02(cbool__00,C)|p__01(s__02(cbool__00,C)). % 3.01/3.18 ** KEPT (pick-wt=15): 21 [copy,20,factor_simp] -p__01(s__02(cbool__00,A))|s__02(cbool__00,A)=s__02(cbool__00,B)| -p__01(s__02(cbool__00,B)). % 3.01/3.18 ** KEPT (pick-wt=19): 22 [] -p__01(s__02(cbool__00,A))|s__02(cbool__00,B)=s__02(cbool__00,C)|p__01(s__02(cbool__00,C))|p__01(s__02(cbool__00,B)). % 3.01/3.18 Following clause subsumed by 14 during input processing: 0 [factor_simp] p__01(s__02(cbool__00,C))|s__02(cbool__00,B)!=s__02(cbool__00,C)| -p__01(s__02(cbool__00,B)). % 3.01/3.18 Following clause subsumed by 19 during input processing: 0 [factor_simp] p__01(s__02(cbool__00,B))|s__02(cbool__00,B)!=s__02(cbool__00,C)| -p__01(s__02(cbool__00,C)). % 3.01/3.18 ** KEPT (pick-wt=30): 23 [] s__02(c_27type_2epair_2eprod_27__02(A,B),c_27const_2epair_2e_2c_27__02(s__02(A,C),s__02(B,D)))!=s__02(c_27type_2epair_2eprod_27__02(A,B),c_27const_2epair_2e_2c_27__02(s__02(A,E),s__02(B,F)))|s__02(A,C)=s__02(A,E). % 3.01/3.18 ** KEPT (pick-wt=30): 24 [] s__02(c_27type_2epair_2eprod_27__02(A,B),c_27const_2epair_2e_2c_27__02(s__02(A,C),s__02(B,D)))!=s__02(c_27type_2epair_2eprod_27__02(A,B),c_27const_2epair_2e_2c_27__02(s__02(A,E),s__02(B,F)))|s__02(B,D)=s__02(B,F). % 3.01/3.18 ** KEPT (pick-wt=37): 25 [] s__02(c_27type_2epair_2eprod_27__02(A,B),c_27const_2epair_2e_2c_27__02(s__02(A,C),s__02(B,D)))=s__02(c_27type_2epair_2eprod_27__02(A,B),c_27const_2epair_2e_2c_27__02(s__02(A,E),s__02(B,F)))|s__02(A,C)!=s__02(A,E)|s__02(B,D)!=s__02(B,F). % 3.01/3.18 ** KEPT (pick-wt=30): 26 [] -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B))))| -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,C))))|p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,C)))). % 3.01/3.18 ** KEPT (pick-wt=17): 27 [] s__02(c_27type_2enum_2enum_27__00,A)!=s__02(c_27type_2enum_2enum_27__00,B)|p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B)))). % 3.01/3.18 ** KEPT (pick-wt=17): 28 [] s__02(c_27type_2enum_2enum_27__00,A)!=s__02(c_27type_2enum_2enum_27__00,B)|p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,A)))). % 3.01/3.18 ** KEPT (pick-wt=27): 29 [] s__02(c_27type_2enum_2enum_27__00,A)=s__02(c_27type_2enum_2enum_27__00,B)| -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B))))| -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,A)))). % 3.01/3.18 ** KEPT (pick-wt=20): 30 [] s__02(c_27type_2enum_2enum_27__00,A)!=s__02(c_27type_2enum_2enum_27__00,B)| -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,B)))). % 3.01/3.18 ** KEPT (pick-wt=20): 31 [] s__02(c_27type_2enum_2enum_27__00,A)!=s__02(c_27type_2enum_2enum_27__00,B)| -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,B))),s__02(c_27type_2enum_2enum_27__00,A)))). % 3.01/3.18 ** KEPT (pick-wt=43): 32 [] -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),A),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_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)!=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,D)))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),A),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))). % 3.01/3.18 ** KEPT (pick-wt=43): 33 [] -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),A),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_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,B)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,C),s__02(c_27type_2enum_2enum_27__00,D)))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),A),s__02(c_27type_2enum_2enum_27__00,D)))). % 3.01/3.18 ** KEPT (pick-wt=49): 35 [copy,34,flip.2] p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),A),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_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,B),s__02(c_27type_2enum_2enum_27__00,$f3(C,B,A))))=s__02(c_27type_2enum_2enum_27__00,C)| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),A),s__02(c_27type_2enum_2enum_27__00,$f3(C,B,A))))). % 3.01/3.18 ** KEPT (pick-wt=46): 37 [copy,36,flip.3] p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),A),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,C))))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),A),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))))|s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,C),s__02(c_27type_2enum_2enum_27__00,$f3(C,B,A))))=s__02(c_27type_2enum_2enum_27__00,B). % 3.01/3.18 ** KEPT (pick-wt=45): 38 [] p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),A),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,C))))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),A),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),A),s__02(c_27type_2enum_2enum_27__00,$f3(C,B,A))))). % 3.01/3.18 ** KEPT (pick-wt=17): 39 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A)))!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)|s__02(c_27type_2enum_2enum_27__00,A)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00). % 3.01/3.18 ** KEPT (pick-wt=17): 40 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)|s__02(c_27type_2enum_2enum_27__00,A)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00). % 3.01/3.18 Following clause subsumed by 39 during input processing: 0 [flip.1] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A)))!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)|s__02(c_27type_2enum_2enum_27__00,A)=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00). % 3.01/3.18 Following clause subsumed by 40 during input processing: 0 [flip.1] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)|s__02(c_27type_2enum_2enum_27__00,A)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00). % 3.01/3.18 ** KEPT (pick-wt=20): 41 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A)))!=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B)))|s__02(c_27type_2enum_2enum_27__00,A)=s__02(c_27type_2enum_2enum_27__00,B). % 3.01/3.18 ** KEPT (pick-wt=20): 42 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B)))|s__02(c_27type_2enum_2enum_27__00,A)!=s__02(c_27type_2enum_2enum_27__00,B). % 3.01/3.18 ** KEPT (pick-wt=17): 43 [] -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,A))))|s__02(c_27type_2enum_2enum_27__00,A)=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 ** KEPT (pick-wt=17): 44 [] p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,A))))|s__02(c_27type_2enum_2enum_27__00,A)!=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 ** KEPT (pick-wt=7): 45 [] -p__01(s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))). % 3.01/3.18 ** KEPT (pick-wt=26): 46 [] -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,B))))))| -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,A)))). % 3.01/3.18 ** KEPT (pick-wt=24): 47 [] s__02(c_27type_2esemanticPrimitives_2eresult_27__02(A,B),c_27const_2esemanticPrimitives_2eRval_27__01(s__02(A,C)))!=s__02(c_27type_2esemanticPrimitives_2eresult_27__02(A,B),c_27const_2esemanticPrimitives_2eRval_27__01(s__02(A,D)))|s__02(A,C)=s__02(A,D). % 3.01/3.18 ** KEPT (pick-wt=24): 48 [] s__02(c_27type_2esemanticPrimitives_2eresult_27__02(A,B),c_27const_2esemanticPrimitives_2eRval_27__01(s__02(A,C)))=s__02(c_27type_2esemanticPrimitives_2eresult_27__02(A,B),c_27const_2esemanticPrimitives_2eRval_27__01(s__02(A,D)))|s__02(A,C)!=s__02(A,D). % 3.01/3.18 ** KEPT (pick-wt=28): 49 [] s__02(c_27type_2esemanticPrimitives_2eresult_27__02(A,B),c_27const_2esemanticPrimitives_2eRerr_27__01(s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(B),C)))!=s__02(c_27type_2esemanticPrimitives_2eresult_27__02(A,B),c_27const_2esemanticPrimitives_2eRerr_27__01(s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(B),D)))|s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(B),C)=s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(B),D). % 3.01/3.18 ** KEPT (pick-wt=28): 50 [] s__02(c_27type_2esemanticPrimitives_2eresult_27__02(A,B),c_27const_2esemanticPrimitives_2eRerr_27__01(s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(B),C)))=s__02(c_27type_2esemanticPrimitives_2eresult_27__02(A,B),c_27const_2esemanticPrimitives_2eRerr_27__01(s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(B),D)))|s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(B),C)!=s__02(c_27type_2esemanticPrimitives_2eerror__result_27__01(B),D). % 3.01/3.18 ** KEPT (pick-wt=161): 51 [] s__02(c_27type_2ebvl_2eexp_27__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00)),A),s__02(c_27type_2enum_2enum_27__00,$f5(B,A)))),s__02(c_27type_2enum_2enum_27__00,$f4(B,A))))!=s__02(c_27type_2ebvl_2eexp_27__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00),c_27const_2ebvl_2eVar_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,$f4(B,A)),s__02(c_27type_2enum_2enum_27__00,$f5(B,A))))))| -p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_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),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(c_27type_2ebvlSem_2ev_27__00),E))))))|s__02(c_27type_2epair_2eprod_27__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01(B)),c_27const_2ebvlSem_2eevaluate_27__01(s__02(c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01(B))),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eGENLIST_27__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00),chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00)),A),s__02(c_27type_2enum_2enum_27__00,D))),s__02(c_27type_2enum_2enum_27__00,C))),s__02(c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01(B)),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),E),s__02(c_27type_2ebvlSem_2estate_27__01(B),F)))))))=s__02(c_27type_2epair_2eprod_27__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01(B)),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27const_2esemanticPrimitives_2eRval_27__01(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,C),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,D),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),E))))))),s__02(c_27type_2ebvlSem_2estate_27__01(B),F))). % 3.01/3.18 ** KEPT (pick-wt=112): 52 [] s__02(c_27type_2epair_2eprod_27__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01($c5)),c_27const_2ebvlSem_2eevaluate_27__01(s__02(c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01($c5))),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvl_2eexp_27__00),c_27const_2elist_2eGENLIST_27__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,c_27type_2ebvl_2eexp_27__00),c_27const_2ebvl_2eVar_27__00),s__02(c_27type_2enum_2enum_27__00,$c4))),s__02(c_27type_2epair_2eprod_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01($c5)),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),$c3))),s__02(c_27type_2enum_2enum_27__00,$c4))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),$c3))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),$c2))),s__02(c_27type_2ebvlSem_2estate_27__01($c5),$c1)))))))!=s__02(c_27type_2epair_2eprod_27__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2estate_27__01($c5)),c_27const_2epair_2e_2c_27__02(s__02(c_27type_2esemanticPrimitives_2eresult_27__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27type_2ebvlSem_2ev_27__00),c_27const_2esemanticPrimitives_2eRval_27__01(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),$c3))),s__02(c_27type_2enum_2enum_27__00,$c4))),s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),$c3))))),s__02(c_27type_2ebvlSem_2estate_27__01($c5),$c1))). % 3.01/3.18 19 back subsumes 16. % 3.01/3.18 19 back subsumes 15. % 3.01/3.18 21 back subsumes 17. % 3.01/3.18 % 3.01/3.18 ------------> process sos: % 3.01/3.18 ** KEPT (pick-wt=3): 57 [] A=A. % 3.01/3.18 ** KEPT (pick-wt=4): 58 [] p__01(s__02(cbool__00,cT__00)). % 3.01/3.18 ** 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). % 3.01/3.18 Following clause subsumed by 58 during input processing: 0 [] p__01(s__02(cbool__00,cT__00)). % 3.01/3.18 Following clause subsumed by 57 during input processing: 0 [] s__02(A,chapp__02(s__02(cfun__02(B,A),C),s__02(B,D)))=s__02(A,chapp__02(s__02(cfun__02(B,A),C),s__02(B,D))). % 3.01/3.18 Following clause subsumed by 58 during input processing: 0 [] p__01(s__02(cbool__00,cT__00)). % 3.01/3.18 Following clause subsumed by 58 during input processing: 0 [unit_del,1] p__01(s__02(cbool__00,cT__00)). % 3.01/3.18 Following clause subsumed by 58 during input processing: 0 [unit_del,1] p__01(s__02(cbool__00,cT__00)). % 3.01/3.18 ** KEPT (pick-wt=11): 60 [] s__02(cbool__00,cF__00)=s__02(cbool__00,A)|p__01(s__02(cbool__00,A)). % 3.01/3.18 ** KEPT (pick-wt=11): 61 [] s__02(cbool__00,A)=s__02(cbool__00,cF__00)|p__01(s__02(cbool__00,A)). % 3.01/3.18 Following clause subsumed by 61 during input processing: 0 [] p__01(s__02(cbool__00,A))|s__02(cbool__00,A)=s__02(cbool__00,cF__00). % 3.01/3.18 ** KEPT (pick-wt=15): 63 [copy,62,factor_simp] p__01(s__02(cbool__00,A))|s__02(cbool__00,A)=s__02(cbool__00,B)|p__01(s__02(cbool__00,B)). % 3.01/3.18 ** KEPT (pick-wt=13): 64 [] 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_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,A). % 3.01/3.18 ---> New Demodulator: 65 [new_demod,64] 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_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,A). % 3.01/3.18 ** KEPT (pick-wt=13): 66 [] 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_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,A)))=s__02(c_27type_2enum_2enum_27__00,A). % 3.01/3.18 ---> New Demodulator: 67 [new_demod,66] 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_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,A)))=s__02(c_27type_2enum_2enum_27__00,A). % 3.01/3.18 Following clause subsumed by 57 during input processing: 0 [demod,65] s__02(c_27type_2enum_2enum_27__00,A)=s__02(c_27type_2enum_2enum_27__00,A). % 3.01/3.18 ** KEPT (pick-wt=25): 69 [copy,68,flip.1] s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(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,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,B))). % 3.01/3.18 ---> New Demodulator: 70 [new_demod,69] s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(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,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,B))). % 3.01/3.18 ** KEPT (pick-wt=25): 72 [copy,71,demod,70] 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_2enum_2eSUC_27__01(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,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,B))). % 3.01/3.18 ** KEPT (pick-wt=19): 73 [] 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))). % 3.01/3.18 ** KEPT (pick-wt=31): 74 [] 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))). % 3.01/3.18 ** KEPT (pick-wt=10): 75 [] p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,A)))). % 3.01/3.18 ** KEPT (pick-wt=16): 76 [] p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_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,A),s__02(c_27type_2enum_2enum_27__00,B)))))). % 3.01/3.18 ** KEPT (pick-wt=13): 77 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,A)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 ---> New Demodulator: 78 [new_demod,77] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,A)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 ** KEPT (pick-wt=13): 79 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,A). % 3.01/3.18 ---> New Demodulator: 80 [new_demod,79] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,A). % 3.01/3.18 ** KEPT (pick-wt=13): 81 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,A)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 ---> New Demodulator: 82 [new_demod,81] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,A)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 ** KEPT (pick-wt=13): 83 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 ---> New Demodulator: 84 [new_demod,83] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 ** KEPT (pick-wt=19): 85 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,A)))=s__02(c_27type_2enum_2enum_27__00,A). % 3.01/3.18 ---> New Demodulator: 86 [new_demod,85] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,A)))=s__02(c_27type_2enum_2enum_27__00,A). % 3.01/3.18 ** KEPT (pick-wt=19): 87 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))=s__02(c_27type_2enum_2enum_27__00,A). % 3.01/3.18 ---> New Demodulator: 88 [new_demod,87] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))))=s__02(c_27type_2enum_2enum_27__00,A). % 3.01/3.18 ** KEPT (pick-wt=28): 89 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(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,c_27const_2earithmetic_2e_2a_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,B))). % 3.01/3.18 ** KEPT (pick-wt=28): 90 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(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,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B))))). % 3.01/3.18 ** KEPT (pick-wt=31): 91 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_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_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,C)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,C))). % 3.01/3.18 ---> New Demodulator: 92 [new_demod,91] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_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_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,C)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,C))). % 3.01/3.18 ** KEPT (pick-wt=33): 93 [] s__02(c_27type_2enum_2enum_27__00,A)=s__02(c_27type_2enum_2enum_27__00,B)|p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,B))))|p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(s__02(c_27type_2enum_2enum_27__00,B))),s__02(c_27type_2enum_2enum_27__00,A)))). % 3.01/3.18 ** KEPT (pick-wt=22): 94 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(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,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,A))). % 3.01/3.18 ---> New Demodulator: 95 [new_demod,94] s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2eSUC_27__01(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,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,A))). % 3.01/3.18 ** KEPT (pick-wt=50): 97 [copy,96,flip.2,flip.3] p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2enum_2enum_27__00,cbool__00),A),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_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,B),s__02(c_27type_2enum_2enum_27__00,$f3(C,B,A))))=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),s__02(c_27type_2enum_2enum_27__00,$f3(C,B,A))))=s__02(c_27type_2enum_2enum_27__00,B). % 3.01/3.18 Following clause subsumed by 57 during input processing: 0 [demod,67] s__02(c_27type_2enum_2enum_27__00,A)=s__02(c_27type_2enum_2enum_27__00,A). % 3.01/3.18 Following clause subsumed by 57 during input processing: 0 [demod,65] s__02(c_27type_2enum_2enum_27__00,A)=s__02(c_27type_2enum_2enum_27__00,A). % 3.01/3.18 ** KEPT (pick-wt=31): 99 [copy,98,flip.1] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enumeral_2eiZ_27__01(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,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B))))). % 3.01/3.18 ---> New Demodulator: 100 [new_demod,99] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enumeral_2eiZ_27__01(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,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B))))). % 3.01/3.18 Following clause subsumed by 57 during input processing: 0 [demod,82] s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 Following clause subsumed by 57 during input processing: 0 [demod,84] s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 ** KEPT (pick-wt=28): 102 [copy,101,flip.1] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_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_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B))))). % 3.01/3.18 ---> New Demodulator: 103 [new_demod,102] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_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_2a_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B))))). % 3.01/3.18 Following clause subsumed by 57 during input processing: 0 [demod,78] s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 Following clause subsumed by 57 during input processing: 0 [demod,80] s__02(c_27type_2enum_2enum_27__00,A)=s__02(c_27type_2enum_2enum_27__00,A). % 3.01/3.18 ** KEPT (pick-wt=28): 105 [copy,104,flip.1] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_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_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B))))). % 3.01/3.18 ---> New Demodulator: 106 [new_demod,105] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_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_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B))))). % 3.01/3.18 ** KEPT (pick-wt=19): 107 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,A)))))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 ---> New Demodulator: 108 [new_demod,107] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,A)))))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 ** KEPT (pick-wt=19): 109 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,A)))))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 ---> New Demodulator: 110 [new_demod,109] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,A)))))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 ** KEPT (pick-wt=19): 111 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))). % 3.01/3.18 ** KEPT (pick-wt=28): 113 [copy,112,flip.1] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_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_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B))))). % 3.01/3.18 ---> New Demodulator: 114 [new_demod,113] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_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_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B))))). % 3.01/3.18 Following clause subsumed by 57 during input processing: 0 [demod,95,65] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))). % 3.01/3.18 ** KEPT (pick-wt=37): 116 [copy,115,demod,95,95,flip.1] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,A)))))=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_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))))). % 3.01/3.18 ---> New Demodulator: 117 [new_demod,116] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2b_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,A)))))=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_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))))). % 3.01/3.18 ** KEPT (pick-wt=10): 118 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 ---> New Demodulator: 119 [new_demod,118] s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00). % 3.01/3.18 ** KEPT (pick-wt=19): 120 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,A))))). % 3.01/3.18 ---> New Demodulator: 121 [new_demod,120] s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2eprim__rec_2ePRE_27__01(s__02(c_27type_2enum_2enum_27__00,A))))). % 3.01/3.18 ** KEPT (pick-wt=13): 122 [] s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(cbool__00,cF__00). % 3.01/3.18 ---> New Demodulator: 123 [new_demod,122] s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(cbool__00,cF__00). % 3.01/3.18 ** KEPT (pick-wt=22): 124 [] s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A)))))=s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,A))). % 3.01/3.18 ---> New Demodulator: 125 [new_demod,124] s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A)))))=s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,A))). % 3.01/3.18 ** KEPT (pick-wt=25): 126 [] s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B)))))=s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B))). % 3.01/3.18 ---> New Demodulator: 127 [new_demod,126] s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B)))))=s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B))). % 3.01/3.18 ** KEPT (pick-wt=13): 128 [] s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,A)))=s__02(cbool__00,cF__00). % 3.01/3.18 ---> New Demodulator: 129 [new_demod,128] s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,A)))=s__02(cbool__00,cF__00). % 3.01/3.18 ** KEPT (pick-wt=22): 130 [] s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,A))). % 3.01/3.18 ---> New Demodulator: 131 [new_demod,130] s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,A))). % 3.01/3.18 ** KEPT (pick-wt=25): 132 [] s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B)))))=s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,A))). % 3.01/3.18 ** KEPT (pick-wt=13): 133 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,A)))=s__02(cbool__00,cT__00). % 3.01/3.18 ---> New Demodulator: 134 [new_demod,133] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2enum_2enum_27__00,A)))=s__02(cbool__00,cT__00). % 3.01/3.18 ** KEPT (pick-wt=22): 135 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))). % 3.01/3.18 ---> New Demodulator: 136 [new_demod,135] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))). % 3.01/3.18 ** KEPT (pick-wt=25): 137 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B))). % 3.01/3.18 ---> New Demodulator: 138 [new_demod,137] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B))). % 3.01/3.18 ** KEPT (pick-wt=13): 139 [] s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(cbool__00,cT__00). % 3.01/3.18 ---> New Demodulator: 140 [new_demod,139] s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(cbool__00,cT__00). % 3.01/3.18 ** KEPT (pick-wt=25): 141 [] s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,A))). % 3.01/3.18 ---> New Demodulator: 142 [new_demod,141] s__02(cbool__00,c_27const_2earithmetic_2e_3e_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,A))). % 3.01/3.18 ** KEPT (pick-wt=16): 143 [] s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A)))))=s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,A))). % 3.01/3.18 ---> New Demodulator: 144 [new_demod,143] s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A)))))=s__02(cbool__00,c_27const_2earithmetic_2eODD_27__01(s__02(c_27type_2enum_2enum_27__00,A))). % 3.01/3.18 ** KEPT (pick-wt=16): 145 [] s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A)))))=s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,A))). % 3.01/3.18 ---> New Demodulator: 146 [new_demod,145] s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A)))))=s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,A))). % 3.01/3.18 ** KEPT (pick-wt=7): 147 [] p__01(s__02(cbool__00,c_27const_2earithmetic_2eEVEN_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))). % 3.01/3.18 ** KEPT (pick-wt=13): 148 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,A)))=s__02(cbool__00,cT__00). % 3.01/3.18 ---> New Demodulator: 149 [new_demod,148] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00),s__02(c_27type_2enum_2enum_27__00,A)))=s__02(cbool__00,cT__00). % 3.01/3.18 ** KEPT (pick-wt=16): 150 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))=s__02(cbool__00,cF__00). % 3.01/3.18 ---> New Demodulator: 151 [new_demod,150] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))=s__02(cbool__00,cF__00). % 3.01/3.18 ** KEPT (pick-wt=16): 152 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))=s__02(cbool__00,cF__00). % 3.01/3.18 ---> New Demodulator: 153 [new_demod,152] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))=s__02(cbool__00,cF__00). % 3.01/3.18 ** KEPT (pick-wt=25): 154 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,B)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B))). % 3.01/3.18 ---> New Demodulator: 155 [new_demod,154] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,B)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B))). % 3.01/3.18 ** KEPT (pick-wt=25): 156 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,B)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B))). % 3.01/3.18 ---> New Demodulator: 157 [new_demod,156] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,B)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B))). % 3.01/3.18 ** KEPT (pick-wt=26): 158 [] p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,B))))))|p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,A)))). % 3.01/3.18 ** KEPT (pick-wt=25): 159 [] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,B)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B))). % 3.01/3.18 ---> New Demodulator: 160 [new_demod,159] s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT2_27__01(s__02(c_27type_2enum_2enum_27__00,B)))))=s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B))). % 3.01/3.18 ** KEPT (pick-wt=33): 161 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(A),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(A),B),s__02(c_27type_2elist_2elist_27__01(A),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_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(A),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))))). % 3.01/3.18 ---> New Demodulator: 162 [new_demod,161] s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(A),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(A),B),s__02(c_27type_2elist_2elist_27__01(A),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_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(A),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))))). % 3.01/3.18 ** KEPT (pick-wt=16): 163 [] s__02(c_27type_2elist_2elist_27__01(A),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2elist_2elist_27__01(A),B)))=s__02(c_27type_2elist_2elist_27__01(A),B). % 3.01/3.18 ---> New Demodulator: 164 [new_demod,163] s__02(c_27type_2elist_2elist_27__01(A),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00),s__02(c_27type_2elist_2elist_27__01(A),B)))=s__02(c_27type_2elist_2elist_27__01(A),B). % 3.01/3.18 ** KEPT (pick-wt=28): 165 [] s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(A),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2elist_2elist_27__01(A),C)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(A),C))),s__02(c_27type_2enum_2enum_27__00,B))). % 3.01/3.18 ---> New Demodulator: 166 [new_demod,165] s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(A),c_27const_2elist_2eDROP_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2elist_2elist_27__01(A),C)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2d_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(A),C))),s__02(c_27type_2enum_2enum_27__00,B))). % 3.01/3.18 ** KEPT (pick-wt=28): 167 [] s__02(c_27type_2elist_2elist_27__01(A),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(A),B))),s__02(c_27type_2elist_2elist_27__01(A),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(A),B),s__02(c_27type_2elist_2elist_27__01(A),C)))))=s__02(c_27type_2elist_2elist_27__01(A),B). % 3.01/3.18 ---> New Demodulator: 168 [new_demod,167] s__02(c_27type_2elist_2elist_27__01(A),c_27const_2elist_2eTAKE_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(A),B))),s__02(c_27type_2elist_2elist_27__01(A),c_27const_2elist_2eAPPEND_27__02(s__02(c_27type_2elist_2elist_27__01(A),B),s__02(c_27type_2elist_2elist_27__01(A),C)))))=s__02(c_27type_2elist_2elist_27__01(A),B). % 3.01/3.18 ** KEPT (pick-wt=14): 169 [] p__01(s__02(cbool__00,c_27const_2earithmetic_2e_3c_3d_27__02(s__02(c_27type_2enum_2enum_27__00,$c4),s__02(c_27type_2enum_2enum_27__00,c_27const_2elist_2eLENGTH_27__01(s__02(c_27type_2elist_2elist_27__01(c_27type_2ebvlSem_2ev_27__00),$c3)))))). % 3.01/3.18 Following clause subsumed by 57 during input processing: 0 [copy,57,flip.1] A=A. % 3.01/3.18 57 back subsumes 56. % 3.01/3.18 57 back subsumes 54. % 3.01/3.18 57 back subsumes 53. % 3.01/3.18 57 back subsumes 5. % 3.01/3.18 58 back subsumes 4. % 3.01/3.18 58 back subsumes 3. % 3.01/3.18 63 back subsumes 22. % 3.01/3.18 >>>> Starting back demodulation with 65. % 3.01/3.18 >>>> Starting back demodulation with 67. % 3.01/3.18 >>>> Starting back demodulation with 70. % 3.01/3.18 ** KEPT (pick-wt=43): 170 [copy,72,flip.1,demod,95,95] 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,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,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,A),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_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,B))))). % 3.01/3.18 Following clause subsumed by 73 during input processing: 0 [copy,73,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))). % 3.01/3.18 ** KEPT (pick-wt=31): 171 [copy,74,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))))). % 3.01/3.18 >>>> Starting back demodulation with 78. % 3.01/3.18 >>>> Starting back demodulation with 80. % 3.01/3.18 >>>> Starting back demodulation with 82. % 3.01/3.18 >>>> Starting back demodulation with 84. % 3.01/3.18 >>>> Starting back demodulation with 86. % 3.01/3.18 >>>> Starting back demodulation with 88. % 3.01/3.18 ** KEPT (pick-wt=37): 172 [copy,89,flip.1,demod,95] 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_2a_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,B)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_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_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,B))). % 3.01/3.18 ** KEPT (pick-wt=37): 173 [copy,90,flip.1,demod,95] 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_2a_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_2a_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,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,B))))). % 3.01/3.18 >>>> Starting back demodulation with 92. % 3.01/3.18 >>>> Starting back demodulation with 95. % 3.01/3.18 >> back demodulating 93 with 95. % 3.01/3.18 >> back demodulating 90 with 95. % 3.01/3.18 >> back demodulating 89 with 95. % 3.01/3.18 >> back demodulating 72 with 95. % 3.01/3.18 >> back demodulating 69 with 95. % 3.01/3.18 >> back demodulating 31 with 95. % 3.01/3.18 >> back demodulating 30 with 95. % 3.01/3.18 >>>> Starting back demodulation with 100. % 3.01/3.18 >>>> Starting back demodulation with 103. % 3.01/3.18 >>>> Starting back demodulation with 106. % 3.01/3.18 >>>> Starting back demodulation with 108. % 3.01/3.18 >>>> Starting back demodulation with 110. % 3.01/3.18 ** KEPT (pick-wt=19): 181 [copy,111,flip.1] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00)))))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00))). % 3.01/3.18 >>>> Starting back demodulation with 114. % 3.01/3.18 >>>> Starting back demodulation with 117. % 3.01/3.18 >>>> Starting back demodulation with 119. % 3.01/3.18 >>>> Starting back demodulation with 121. % 3.01/3.18 >>>> Starting back demodulation with 123. % 3.01/3.18 >>>> Starting back demodulation with 125. % 3.01/3.18 >>>> Starting back demodulation with 127. % 3.01/3.18 >>>> Starting back demodulation with 129. % 3.01/3.18 >>>> Starting back demodulation with 131. % 3.01/3.18 ** KEPT (pick-wt=25): 182 [copy,132,flip.1] s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B)))=s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))))). % 3.01/3.18 >>>> Starting back demodulation with 134. % 3.01/3.18 >> back demodulating 75 with 134. % 3.01/3.18 >>>> Starting back demodulation with 136. % 3.01/3.18 >>>> Starting back demodulation with 138. % 3.01/3.18 >>>> Starting back demodulation with 140. % 3.01/3.18 >>>> Starting back demodulation with 142. % 3.01/3.18 >>>> Starting back demodulation with 144. % 3.01/3.18 >>>> Starting back demodulation with 146. % 3.01/3.18 >>>> Starting back demodulation with 149. % 3.01/3.18 >>>> Starting back demodulation with 151. % 3.01/3.18 >>>> Starting back demodulation with 153. % 3.01/3.18 >>>> Starting back demodulation with 155. % 3.01/3.18 >>>> Starting back demodulation with 157. % 3.01/3.18 >>>> Starting back demodulation with 160. % 3.01/3.18 >>>> Starting back demodulation with 162. % 3.01/3.18 >>>> Starting back demodulation with 164. % 3.01/3.18 >>>> Starting back demodulation with 166. % 3.01/3.18 >>>> Starting back demodulation with 168. % 3.01/3.18 Following clause subsumed by 177 during input processing: 0 [copy,170,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,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,B)))))=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,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,B))). % 3.01/3.18 Following clause subsumed by 74 during input processing: 0 [copy,171,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))). % 3.01/3.18 Following clause subsumed by 176 during input processing: 0 [copy,172,flip.1] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_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_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,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,c_27const_2earithmetic_2e_2a_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,B))). % 3.01/3.18 Following clause subsumed by 175 during input processing: 0 [copy,173,flip.1] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_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,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,B)))))=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_2a_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,B))))). % 3.18/3.32 Following clause subsumed by 173 during input processing: 0 [copy,175,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_2a_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_2a_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,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,B))))). % 3.18/3.32 Following clause subsumed by 172 during input processing: 0 [copy,176,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_2a_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,B)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2e_2a_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_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,B))). % 3.18/3.32 Following clause subsumed by 170 during input processing: 0 [copy,177,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,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,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,A),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_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))),s__02(c_27type_2enum_2enum_27__00,B))))). % 3.18/3.32 Following clause subsumed by 111 during input processing: 0 [copy,181,flip.1] s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eEXP_27__02(s__02(c_27type_2enum_2enum_27__00,A),s__02(c_27type_2enum_2enum_27__00,c_27const_2enum_2e0_27__00)))=s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eBIT1_27__01(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eZERO_27__00))))). % 3.18/3.32 Following clause subsumed by 132 during input processing: 0 [copy,182,flip.1] s__02(cbool__00,c_27const_2earithmetic_2e_3e_27__02(s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,A))),s__02(c_27type_2enum_2enum_27__00,c_27const_2earithmetic_2eNUMERAL_27__01(s__02(c_27type_2enum_2enum_27__00,B)))))=s__02(cbool__00,c_27const_2eprim__rec_2e_3c_27__02(s__02(c_27type_2enum_2enum_27__00,B),s__02(c_27type_2enum_2enum_27__00,A))). % 3.18/3.32 % 3.18/3.32 ======= end of input processing ======= % 3.18/3.32 % 3.18/3.32 =========== start of search =========== % 3.18/3.32 % 3.18/3.32 % 3.18/3.32 Resetting weight limit to 11. % 3.18/3.32 % 3.18/3.32 % 3.18/3.32 Resetting weight limit to 11. % 3.18/3.32 % 3.18/3.32 sos_size=68 % 3.18/3.32 % 3.18/3.32 Search stopped because sos empty. % 3.18/3.32 % 3.18/3.32 % 3.18/3.32 Search stopped because sos empty. % 3.18/3.32 % 3.18/3.32 ============ end of search ============ % 3.18/3.32 % 3.18/3.32 -------------- statistics ------------- % 3.18/3.32 clauses given 78 % 3.18/3.32 clauses generated 17867 % 3.18/3.32 clauses kept 135 % 3.18/3.32 clauses forward subsumed 1604 % 3.18/3.32 clauses back subsumed 10 % 3.18/3.32 Kbytes malloced 9765 % 3.18/3.32 % 3.18/3.32 ----------- times (seconds) ----------- % 3.18/3.32 user CPU time 0.15 (0 hr, 0 min, 0 sec) % 3.18/3.32 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 3.18/3.32 wall-clock time 3 (0 hr, 0 min, 3 sec) % 3.18/3.32 % 3.18/3.32 Process 796 finished Wed Jul 27 02:58:20 2022 % 3.18/3.32 Otter interrupted % 3.18/3.32 PROOF NOT FOUND %------------------------------------------------------------------------------