%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWW941+1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n020.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:12 EDT 2022 % Result : Unknown 2.70s 2.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWW941+1 : TPTP v8.1.0. Released v7.3.0. % 0.13/0.13 % Command : otter-tptp-script %s % 0.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Jul 27 03:02:38 EDT 2022 % 0.13/0.34 % CPUTime : % 2.52/2.70 ----- Otter 3.3f, August 2004 ----- % 2.52/2.70 The process was started by sandbox on n020.cluster.edu, % 2.52/2.70 Wed Jul 27 03:02:38 2022 % 2.52/2.70 The command was "./otter". The process ID is 22871. % 2.52/2.70 % 2.52/2.70 set(prolog_style_variables). % 2.52/2.70 set(auto). % 2.52/2.70 dependent: set(auto1). % 2.52/2.70 dependent: set(process_input). % 2.52/2.70 dependent: clear(print_kept). % 2.52/2.70 dependent: clear(print_new_demod). % 2.52/2.70 dependent: clear(print_back_demod). % 2.52/2.70 dependent: clear(print_back_sub). % 2.52/2.70 dependent: set(control_memory). % 2.52/2.70 dependent: assign(max_mem, 12000). % 2.52/2.70 dependent: assign(pick_given_ratio, 4). % 2.52/2.70 dependent: assign(stats_level, 1). % 2.52/2.70 dependent: assign(max_seconds, 10800). % 2.52/2.70 clear(print_given). % 2.52/2.70 % 2.52/2.70 formula_list(usable). % 2.52/2.70 all A (A=A). % 2.52/2.70 p__01(s__02(cbool__00,cT__00)). % 2.52/2.70 -p__01(s__02(cbool__00,cF__00)). % 2.52/2.70 all Vt (s__02(cbool__00,Vt)=s__02(cbool__00,cT__00)|s__02(cbool__00,Vt)=s__02(cbool__00,cF__00)). % 2.52/2.70 all V_3f2384 V_3f2380 Vf Vg ((all Vx (s__02(V_3f2380,chapp__02(s__02(cfun__02(V_3f2384,V_3f2380),Vf),s__02(V_3f2384,Vx)))=s__02(V_3f2380,chapp__02(s__02(cfun__02(V_3f2384,V_3f2380),Vg),s__02(V_3f2384,Vx)))))->s__02(cfun__02(V_3f2384,V_3f2380),Vf)=s__02(cfun__02(V_3f2384,V_3f2380),Vg)). % 2.52/2.70 p__01(s__02(cbool__00,cT__00)). % 2.52/2.70 all V_27t1_27 V_27t2_27 ((p__01(s__02(cbool__00,V_27t1_27))->p__01(s__02(cbool__00,V_27t2_27)))-> ((p__01(s__02(cbool__00,V_27t2_27))->p__01(s__02(cbool__00,V_27t1_27)))->s__02(cbool__00,V_27t1_27)=s__02(cbool__00,V_27t2_27))). % 2.52/2.70 all V_27t_27 (p__01(s__02(cbool__00,cF__00))->p__01(s__02(cbool__00,V_27t_27))). % 2.52/2.70 all V_27A_27 V_27t_27 ((all V_27x_27 p__01(s__02(cbool__00,V_27t_27)))<->p__01(s__02(cbool__00,V_27t_27))). % 2.52/2.70 all V_27A_27 V_27t_27 ((exists V_27x_27 p__01(s__02(cbool__00,V_27t_27)))<->p__01(s__02(cbool__00,V_27t_27))). % 2.52/2.70 all 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)))). % 2.52/2.70 all V_27t_27 ((p__01(s__02(cbool__00,cT__00))&p__01(s__02(cbool__00,V_27t_27))<->p__01(s__02(cbool__00,V_27t_27)))& (p__01(s__02(cbool__00,V_27t_27))&p__01(s__02(cbool__00,cT__00))<->p__01(s__02(cbool__00,V_27t_27)))& (p__01(s__02(cbool__00,cF__00))&p__01(s__02(cbool__00,V_27t_27))<->p__01(s__02(cbool__00,cF__00)))& (p__01(s__02(cbool__00,V_27t_27))&p__01(s__02(cbool__00,cF__00))<->p__01(s__02(cbool__00,cF__00)))& (p__01(s__02(cbool__00,V_27t_27))&p__01(s__02(cbool__00,V_27t_27))<->p__01(s__02(cbool__00,V_27t_27)))). % 2.52/2.70 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)))). % 2.52/2.70 all V_27t_27 (((p__01(s__02(cbool__00,cT__00))->p__01(s__02(cbool__00,V_27t_27)))<->p__01(s__02(cbool__00,V_27t_27)))& ((p__01(s__02(cbool__00,V_27t_27))->p__01(s__02(cbool__00,cT__00)))<->p__01(s__02(cbool__00,cT__00)))& ((p__01(s__02(cbool__00,cF__00))->p__01(s__02(cbool__00,V_27t_27)))<->p__01(s__02(cbool__00,cT__00)))& ((p__01(s__02(cbool__00,V_27t_27))->p__01(s__02(cbool__00,V_27t_27)))<->p__01(s__02(cbool__00,cT__00)))& ((p__01(s__02(cbool__00,V_27t_27))->p__01(s__02(cbool__00,cF__00)))<-> -p__01(s__02(cbool__00,V_27t_27)))). % 2.52/2.70 all V_27t_27 (-(-p__01(s__02(cbool__00,V_27t_27)))<->p__01(s__02(cbool__00,V_27t_27))). % 2.52/2.70 -p__01(s__02(cbool__00,cT__00))<->p__01(s__02(cbool__00,cF__00)). % 2.52/2.70 -p__01(s__02(cbool__00,cF__00))<->p__01(s__02(cbool__00,cT__00)). % 2.52/2.70 all V_27A_27 V_27x_27 (s__02(V_27A_27,V_27x_27)=s__02(V_27A_27,V_27x_27)<->p__01(s__02(cbool__00,cT__00))). % 2.52/2.70 all V_27A_27 V_27x_27 V_27y_27 (s__02(V_27A_27,V_27x_27)=s__02(V_27A_27,V_27y_27)<->s__02(V_27A_27,V_27y_27)=s__02(V_27A_27,V_27x_27)). % 2.52/2.70 all V_27t_27 ((s__02(cbool__00,cT__00)=s__02(cbool__00,V_27t_27)<->p__01(s__02(cbool__00,V_27t_27)))& (s__02(cbool__00,V_27t_27)=s__02(cbool__00,cT__00)<->p__01(s__02(cbool__00,V_27t_27)))& (s__02(cbool__00,cF__00)=s__02(cbool__00,V_27t_27)<-> -p__01(s__02(cbool__00,V_27t_27)))& (s__02(cbool__00,V_27t_27)=s__02(cbool__00,cF__00)<-> -p__01(s__02(cbool__00,V_27t_27)))). % 2.52/2.70 all V_27A_270 V_27B_270 V_27C_27 (p__01(s__02(cbool__00,V_27A_270))|p__01(s__02(cbool__00,V_27B_270))|p__01(s__02(cbool__00,V_27C_27))<->p__01(s__02(cbool__00,V_27A_270))|p__01(s__02(cbool__00,V_27B_270))|p__01(s__02(cbool__00,V_27C_27))). % 2.52/2.70 all V_27A_270 V_27B_270 (p__01(s__02(cbool__00,V_27A_270))|p__01(s__02(cbool__00,V_27B_270))<->p__01(s__02(cbool__00,V_27B_270))|p__01(s__02(cbool__00,V_27A_270))). % 2.52/2.70 all V_27A_270 V_27B_270 ((p__01(s__02(cbool__00,V_27A_270))->p__01(s__02(cbool__00,V_27B_270)))<-> -p__01(s__02(cbool__00,V_27A_270))|p__01(s__02(cbool__00,V_27B_270))). % 2.52/2.70 all V_27t1_27 V_27t2_27 V_27t3_27 ((p__01(s__02(cbool__00,V_27t1_27))-> (p__01(s__02(cbool__00,V_27t2_27))->p__01(s__02(cbool__00,V_27t3_27))))<-> (p__01(s__02(cbool__00,V_27t1_27))&p__01(s__02(cbool__00,V_27t2_27))->p__01(s__02(cbool__00,V_27t3_27)))). % 2.52/2.70 all V_27x_27 V_27x_7c39_7c_27 V_27y_27 V_27y_7c39_7c_27 (s__02(cbool__00,V_27x_27)=s__02(cbool__00,V_27x_7c39_7c_27)& (p__01(s__02(cbool__00,V_27x_7c39_7c_27))->s__02(cbool__00,V_27y_27)=s__02(cbool__00,V_27y_7c39_7c_27))-> ((p__01(s__02(cbool__00,V_27x_27))->p__01(s__02(cbool__00,V_27y_27)))<-> (p__01(s__02(cbool__00,V_27x_7c39_7c_27))->p__01(s__02(cbool__00,V_27y_7c39_7c_27))))). % 2.52/2.70 all V_27A_27 V_27a_27 exists V_27x_27 (s__02(V_27A_27,V_27x_27)=s__02(V_27A_27,V_27a_27)). % 2.52/2.70 all V_27A_27 V_27P_27 V_27a_27 ((exists V_27x_27 (s__02(V_27A_27,V_27x_27)=s__02(V_27A_27,V_27a_27)&p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,V_27x_27))))))<->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,V_27a_27))))). % 2.52/2.70 all V_27A_27 V_27f_27 V_27v_27 ((all V_27x_27 (s__02(V_27A_27,V_27x_27)=s__02(V_27A_27,V_27v_27)->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27f_27),s__02(V_27A_27,V_27x_27))))))<->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27f_27),s__02(V_27A_27,V_27v_27))))). % 2.52/2.70 all V_27K_27 V_27V_27 V_27a0_27 V_27a1_27 V_27a2_27 V_27a3_27 V_27a4_27 V_27a0_7c39_7c_27 V_27a1_7c39_7c_27 V_27a2_7c39_7c_27 V_27a3_7c39_7c_27 V_27a4_7c39_7c_27 (s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27a0_27),s__02(V_27K_27,V_27a1_27),s__02(V_27V_27,V_27a2_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_27)))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27a0_7c39_7c_27),s__02(V_27K_27,V_27a1_7c39_7c_27),s__02(V_27V_27,V_27a2_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_7c39_7c_27)))<->s__02(c_27type_2enum_2enum_27__00,V_27a0_27)=s__02(c_27type_2enum_2enum_27__00,V_27a0_7c39_7c_27)&s__02(V_27K_27,V_27a1_27)=s__02(V_27K_27,V_27a1_7c39_7c_27)&s__02(V_27V_27,V_27a2_27)=s__02(V_27V_27,V_27a2_7c39_7c_27)&s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_7c39_7c_27)&s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_7c39_7c_27)). % 2.52/2.70 all V_27K_27 V_27V_27 V_27a4_27 V_27a3_27 V_27a2_27 V_27a1_27 V_27a0_27 (s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eTip_27__00)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27a0_27),s__02(V_27K_27,V_27a1_27),s__02(V_27V_27,V_27a2_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_27)))). % 2.52/2.70 all V_27A_27 V_27B_27 V_27P_27 ((all V_27s_27 V_27k_27 V_27x_27 V_27l_27 p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),cbool__00),V_27P_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27s_27),s__02(V_27A_27,V_27k_27),s__02(V_27B_27,V_27x_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27l_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)))))))& (all V_27s_27 V_27k_27 V_27x_27 V_27l_27 V_27v5_27 V_27v6_27 V_27v7_27 V_27v8_27 V_27v9_27 (p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),cbool__00),V_27P_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27v5_27),s__02(V_27A_27,V_27v6_27),s__02(V_27B_27,V_27v7_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27v8_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27v9_27))))))->p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),cbool__00),V_27P_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27s_27),s__02(V_27A_27,V_27k_27),s__02(V_27B_27,V_27x_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27l_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27v5_27),s__02(V_27A_27,V_27v6_27),s__02(V_27B_27,V_27v7_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27v8_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27v9_27))))))))))&p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),cbool__00),V_27P_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00))))-> (all V_27v_27 p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),cbool__00),V_27P_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27v_27)))))). % 2.52/2.70 all V_27A_27 V_27B_27 V_27a0_27 (p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))<-> ((exists V_27x3_27 V_27x2_27 V_27x_7c39_7c_27 V_27x1_27 (s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x3_27),s__02(V_27A_27,V_27x2_27),s__02(V_27B_27,V_27x_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x1_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)))))| (exists V_27x11_27 V_27x10_27 V_27x_7c39_7c_27 V_27x9_27 V_27x8_27 V_27x7_27 V_27x6_27 V_27x5_27 V_27x4_27 (s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x11_27),s__02(V_27A_27,V_27x10_27),s__02(V_27B_27,V_27x_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x9_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x8_27),s__02(V_27A_27,V_27x7_27),s__02(V_27B_27,V_27x6_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x5_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x4_27)))))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00))& (all V_27x21_27 V_27x20_27 V_27x19_27 V_27x18_27 V_27x17_27 ((s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)->p__01(s__02(cbool__00,cF__00)))& (s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x21_27),s__02(V_27A_27,V_27x20_27),s__02(V_27B_27,V_27x19_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x18_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x17_27)))-> (all V_27x16_27 V_27x15_27 V_27x14_27 V_27x13_27 V_27x12_27 (s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x17_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x16_27),s__02(V_27A_27,V_27x15_27),s__02(V_27B_27,V_27x14_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x13_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x12_27)))->p__01(s__02(cbool__00,cT__00))&p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x16_27),s__02(V_27A_27,V_27x15_27),s__02(V_27B_27,V_27x14_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x13_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x12_27)))))))))))). % 2.52/2.70 -(all V_27A_27 V_27B_27 V_27m_27 (s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27m_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)->p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27m_27)))))). % 2.52/2.70 end_of_list. % 2.52/2.70 % 2.52/2.70 -------> usable clausifies to: % 2.52/2.70 % 2.52/2.70 list(usable). % 2.52/2.70 0 [] A=A. % 2.52/2.70 0 [] p__01(s__02(cbool__00,cT__00)). % 2.52/2.70 0 [] -p__01(s__02(cbool__00,cF__00)). % 2.52/2.70 0 [] s__02(cbool__00,Vt)=s__02(cbool__00,cT__00)|s__02(cbool__00,Vt)=s__02(cbool__00,cF__00). % 2.52/2.70 0 [] s__02(V_3f2380,chapp__02(s__02(cfun__02(V_3f2384,V_3f2380),Vf),s__02(V_3f2384,$f1(V_3f2384,V_3f2380,Vf,Vg))))!=s__02(V_3f2380,chapp__02(s__02(cfun__02(V_3f2384,V_3f2380),Vg),s__02(V_3f2384,$f1(V_3f2384,V_3f2380,Vf,Vg))))|s__02(cfun__02(V_3f2384,V_3f2380),Vf)=s__02(cfun__02(V_3f2384,V_3f2380),Vg). % 2.52/2.70 0 [] p__01(s__02(cbool__00,cT__00)). % 2.52/2.70 0 [] p__01(s__02(cbool__00,V_27t1_27))|p__01(s__02(cbool__00,V_27t2_27))|s__02(cbool__00,V_27t1_27)=s__02(cbool__00,V_27t2_27). % 2.52/2.70 0 [] -p__01(s__02(cbool__00,V_27t2_27))| -p__01(s__02(cbool__00,V_27t1_27))|s__02(cbool__00,V_27t1_27)=s__02(cbool__00,V_27t2_27). % 2.52/2.70 0 [] -p__01(s__02(cbool__00,cF__00))|p__01(s__02(cbool__00,V_27t_27)). % 2.52/2.70 0 [] p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,V_27t_27)). % 2.52/2.70 0 [] p__01(s__02(cbool__00,V_27t_27))| -p__01(s__02(cbool__00,cF__00)). % 2.52/2.70 0 [] -p__01(s__02(cbool__00,V_27t_27))|p__01(s__02(cbool__00,cT__00)). % 2.52/2.70 0 [] -p__01(s__02(cbool__00,cF__00))|p__01(s__02(cbool__00,V_27t_27)). % 2.52/2.70 0 [] -p__01(s__02(cbool__00,cF__00))|p__01(s__02(cbool__00,V_27t_27))| -p__01(s__02(cbool__00,cT__00)). % 2.52/2.70 0 [] p__01(s__02(cbool__00,cT__00)). % 2.52/2.70 0 [] -p__01(s__02(cbool__00,cF__00))| -p__01(s__02(cbool__00,V_27t_27)). % 2.52/2.70 0 [] p__01(s__02(cbool__00,cT__00))|p__01(s__02(cbool__00,cF__00)). % 2.52/2.70 0 [] -p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,cF__00)). % 2.52/2.70 0 [] p__01(s__02(cbool__00,cF__00))|p__01(s__02(cbool__00,cT__00)). % 2.52/2.70 0 [] -p__01(s__02(cbool__00,cF__00))| -p__01(s__02(cbool__00,cT__00)). % 2.52/2.70 0 [] s__02(V_27A_27,V_27x_27)!=s__02(V_27A_27,V_27x_27)|p__01(s__02(cbool__00,cT__00)). % 2.52/2.70 0 [] s__02(V_27A_27,V_27x_27)=s__02(V_27A_27,V_27x_27)| -p__01(s__02(cbool__00,cT__00)). % 2.52/2.70 0 [] s__02(V_27A_27,V_27x_27)!=s__02(V_27A_27,V_27y_27)|s__02(V_27A_27,V_27y_27)=s__02(V_27A_27,V_27x_27). % 2.52/2.70 0 [] s__02(V_27A_27,V_27x_27)=s__02(V_27A_27,V_27y_27)|s__02(V_27A_27,V_27y_27)!=s__02(V_27A_27,V_27x_27). % 2.52/2.70 0 [] s__02(cbool__00,cT__00)!=s__02(cbool__00,V_27t_27)|p__01(s__02(cbool__00,V_27t_27)). % 2.52/2.70 0 [] s__02(cbool__00,cT__00)=s__02(cbool__00,V_27t_27)| -p__01(s__02(cbool__00,V_27t_27)). % 2.52/2.70 0 [] s__02(cbool__00,V_27t_27)!=s__02(cbool__00,cT__00)|p__01(s__02(cbool__00,V_27t_27)). % 2.52/2.70 0 [] s__02(cbool__00,V_27t_27)=s__02(cbool__00,cT__00)| -p__01(s__02(cbool__00,V_27t_27)). % 2.52/2.70 0 [] s__02(cbool__00,cF__00)!=s__02(cbool__00,V_27t_27)| -p__01(s__02(cbool__00,V_27t_27)). % 2.52/2.70 0 [] s__02(cbool__00,cF__00)=s__02(cbool__00,V_27t_27)|p__01(s__02(cbool__00,V_27t_27)). % 2.52/2.70 0 [] s__02(cbool__00,V_27t_27)!=s__02(cbool__00,cF__00)| -p__01(s__02(cbool__00,V_27t_27)). % 2.52/2.70 0 [] s__02(cbool__00,V_27t_27)=s__02(cbool__00,cF__00)|p__01(s__02(cbool__00,V_27t_27)). % 2.52/2.70 0 [] s__02(cbool__00,V_27x_27)!=s__02(cbool__00,V_27x_7c39_7c_27)|p__01(s__02(cbool__00,V_27x_7c39_7c_27))| -p__01(s__02(cbool__00,V_27x_27))|p__01(s__02(cbool__00,V_27y_27)). % 2.52/2.70 0 [] s__02(cbool__00,V_27x_27)!=s__02(cbool__00,V_27x_7c39_7c_27)|s__02(cbool__00,V_27y_27)!=s__02(cbool__00,V_27y_7c39_7c_27)|p__01(s__02(cbool__00,V_27x_27))| -p__01(s__02(cbool__00,V_27x_7c39_7c_27))|p__01(s__02(cbool__00,V_27y_7c39_7c_27)). % 2.52/2.70 0 [] s__02(cbool__00,V_27x_27)!=s__02(cbool__00,V_27x_7c39_7c_27)|s__02(cbool__00,V_27y_27)!=s__02(cbool__00,V_27y_7c39_7c_27)| -p__01(s__02(cbool__00,V_27y_27))| -p__01(s__02(cbool__00,V_27x_7c39_7c_27))|p__01(s__02(cbool__00,V_27y_7c39_7c_27)). % 2.52/2.70 0 [] s__02(cbool__00,V_27x_27)!=s__02(cbool__00,V_27x_7c39_7c_27)|s__02(cbool__00,V_27y_27)!=s__02(cbool__00,V_27y_7c39_7c_27)| -p__01(s__02(cbool__00,V_27x_27))|p__01(s__02(cbool__00,V_27y_27))| -p__01(s__02(cbool__00,V_27y_7c39_7c_27)). % 2.52/2.70 0 [] s__02(V_27A_27,$f4(V_27A_27,V_27a_27))=s__02(V_27A_27,V_27a_27). % 2.52/2.70 0 [] s__02(V_27A_27,V_27x_27)!=s__02(V_27A_27,V_27a_27)| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,V_27x_27))))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,V_27a_27)))). % 2.52/2.70 0 [] s__02(V_27A_27,$f5(V_27A_27,V_27P_27,V_27a_27))=s__02(V_27A_27,V_27a_27)| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,V_27a_27)))). % 2.52/2.70 0 [] p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,$f5(V_27A_27,V_27P_27,V_27a_27)))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27P_27),s__02(V_27A_27,V_27a_27)))). % 2.52/2.70 0 [] s__02(V_27A_27,$f6(V_27A_27,V_27f_27,V_27v_27))=s__02(V_27A_27,V_27v_27)|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27f_27),s__02(V_27A_27,V_27v_27)))). % 2.52/2.70 0 [] -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27f_27),s__02(V_27A_27,$f6(V_27A_27,V_27f_27,V_27v_27)))))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27f_27),s__02(V_27A_27,V_27v_27)))). % 2.52/2.70 0 [] s__02(V_27A_27,V_27x_27)!=s__02(V_27A_27,V_27v_27)|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27f_27),s__02(V_27A_27,V_27x_27))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(V_27A_27,cbool__00),V_27f_27),s__02(V_27A_27,V_27v_27)))). % 2.52/2.70 0 [] s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27a0_27),s__02(V_27K_27,V_27a1_27),s__02(V_27V_27,V_27a2_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_27)))!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27a0_7c39_7c_27),s__02(V_27K_27,V_27a1_7c39_7c_27),s__02(V_27V_27,V_27a2_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_7c39_7c_27)))|s__02(c_27type_2enum_2enum_27__00,V_27a0_27)=s__02(c_27type_2enum_2enum_27__00,V_27a0_7c39_7c_27). % 2.52/2.70 0 [] s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27a0_27),s__02(V_27K_27,V_27a1_27),s__02(V_27V_27,V_27a2_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_27)))!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27a0_7c39_7c_27),s__02(V_27K_27,V_27a1_7c39_7c_27),s__02(V_27V_27,V_27a2_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_7c39_7c_27)))|s__02(V_27K_27,V_27a1_27)=s__02(V_27K_27,V_27a1_7c39_7c_27). % 2.52/2.70 0 [] s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27a0_27),s__02(V_27K_27,V_27a1_27),s__02(V_27V_27,V_27a2_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_27)))!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27a0_7c39_7c_27),s__02(V_27K_27,V_27a1_7c39_7c_27),s__02(V_27V_27,V_27a2_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_7c39_7c_27)))|s__02(V_27V_27,V_27a2_27)=s__02(V_27V_27,V_27a2_7c39_7c_27). % 2.52/2.70 0 [] s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27a0_27),s__02(V_27K_27,V_27a1_27),s__02(V_27V_27,V_27a2_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_27)))!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27a0_7c39_7c_27),s__02(V_27K_27,V_27a1_7c39_7c_27),s__02(V_27V_27,V_27a2_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_7c39_7c_27)))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_7c39_7c_27). % 2.52/2.70 0 [] s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27a0_27),s__02(V_27K_27,V_27a1_27),s__02(V_27V_27,V_27a2_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_27)))!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27a0_7c39_7c_27),s__02(V_27K_27,V_27a1_7c39_7c_27),s__02(V_27V_27,V_27a2_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_7c39_7c_27)))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_7c39_7c_27). % 2.52/2.70 0 [] s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27a0_27),s__02(V_27K_27,V_27a1_27),s__02(V_27V_27,V_27a2_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_27)))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27a0_7c39_7c_27),s__02(V_27K_27,V_27a1_7c39_7c_27),s__02(V_27V_27,V_27a2_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_7c39_7c_27)))|s__02(c_27type_2enum_2enum_27__00,V_27a0_27)!=s__02(c_27type_2enum_2enum_27__00,V_27a0_7c39_7c_27)|s__02(V_27K_27,V_27a1_27)!=s__02(V_27K_27,V_27a1_7c39_7c_27)|s__02(V_27V_27,V_27a2_27)!=s__02(V_27V_27,V_27a2_7c39_7c_27)|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_7c39_7c_27)|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_7c39_7c_27). % 2.52/2.70 0 [] s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eTip_27__00)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27a0_27),s__02(V_27K_27,V_27a1_27),s__02(V_27V_27,V_27a2_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a3_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27K_27,V_27V_27),V_27a4_27))). % 2.52/2.70 0 [] -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),cbool__00),V_27P_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f10(V_27A_27,V_27B_27,V_27P_27)),s__02(V_27A_27,$f9(V_27A_27,V_27B_27,V_27P_27)),s__02(V_27B_27,$f8(V_27A_27,V_27B_27,V_27P_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f7(V_27A_27,V_27B_27,V_27P_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00))))))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),cbool__00),V_27P_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V_27P_27)),s__02(V_27A_27,$f14(V_27A_27,V_27B_27,V_27P_27)),s__02(V_27B_27,$f13(V_27A_27,V_27B_27,V_27P_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f12(V_27A_27,V_27B_27,V_27P_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f11(V_27A_27,V_27B_27,V_27P_27)))))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),cbool__00),V_27P_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00))))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),cbool__00),V_27P_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27v_27)))). % 2.52/2.70 0 [] -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),cbool__00),V_27P_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f10(V_27A_27,V_27B_27,V_27P_27)),s__02(V_27A_27,$f9(V_27A_27,V_27B_27,V_27P_27)),s__02(V_27B_27,$f8(V_27A_27,V_27B_27,V_27P_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f7(V_27A_27,V_27B_27,V_27P_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00))))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),cbool__00),V_27P_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f19(V_27A_27,V_27B_27,V_27P_27)),s__02(V_27A_27,$f18(V_27A_27,V_27B_27,V_27P_27)),s__02(V_27B_27,$f17(V_27A_27,V_27B_27,V_27P_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f16(V_27A_27,V_27B_27,V_27P_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f15(V_27A_27,V_27B_27,V_27P_27)),s__02(V_27A_27,$f14(V_27A_27,V_27B_27,V_27P_27)),s__02(V_27B_27,$f13(V_27A_27,V_27B_27,V_27P_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f12(V_27A_27,V_27B_27,V_27P_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f11(V_27A_27,V_27B_27,V_27P_27)))))))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),cbool__00),V_27P_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00))))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),cbool__00),V_27P_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27v_27)))). % 2.52/2.70 0 [] -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f23(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f22(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f21(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f20(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f32(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f31(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f30(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f29(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f28(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f27(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f26(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f25(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f24(V_27A_27,V_27B_27,V_27a0_27))))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00). % 2.52/2.70 0 [] -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)|p__01(s__02(cbool__00,cF__00)). % 2.52/2.70 0 [] -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x21_27),s__02(V_27A_27,V_27x20_27),s__02(V_27B_27,V_27x19_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x18_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x17_27)))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x17_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x16_27),s__02(V_27A_27,V_27x15_27),s__02(V_27B_27,V_27x14_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x13_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x12_27)))|p__01(s__02(cbool__00,cT__00)). % 2.52/2.70 0 [] -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x21_27),s__02(V_27A_27,V_27x20_27),s__02(V_27B_27,V_27x19_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x18_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x17_27)))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x17_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x16_27),s__02(V_27A_27,V_27x15_27),s__02(V_27B_27,V_27x14_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x13_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x12_27)))|p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x16_27),s__02(V_27A_27,V_27x15_27),s__02(V_27B_27,V_27x14_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x13_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x12_27)))))). % 2.52/2.70 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x3_27),s__02(V_27A_27,V_27x2_27),s__02(V_27B_27,V_27x_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x1_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f42(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f41(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f40(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f39(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f38(V_27A_27,V_27B_27,V_27a0_27)))). % 2.52/2.70 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x3_27),s__02(V_27A_27,V_27x2_27),s__02(V_27B_27,V_27x_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x1_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f38(V_27A_27,V_27B_27,V_27a0_27))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f36(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f35(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f34(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f33(V_27A_27,V_27B_27,V_27a0_27)))). % 2.52/2.70 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x3_27),s__02(V_27A_27,V_27x2_27),s__02(V_27B_27,V_27x_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x1_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)| -p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f36(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f35(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f34(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f33(V_27A_27,V_27B_27,V_27a0_27))))))). % 2.52/2.70 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x3_27),s__02(V_27A_27,V_27x2_27),s__02(V_27B_27,V_27x_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x1_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)))| -p__01(s__02(cbool__00,cF__00))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f42(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f41(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f40(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f39(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f38(V_27A_27,V_27B_27,V_27a0_27)))). % 2.52/2.70 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x3_27),s__02(V_27A_27,V_27x2_27),s__02(V_27B_27,V_27x_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x1_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)))| -p__01(s__02(cbool__00,cF__00))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f38(V_27A_27,V_27B_27,V_27a0_27))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f36(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f35(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f34(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f33(V_27A_27,V_27B_27,V_27a0_27)))). % 2.52/2.70 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x3_27),s__02(V_27A_27,V_27x2_27),s__02(V_27B_27,V_27x_7c39_7c_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x1_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)))| -p__01(s__02(cbool__00,cF__00))| -p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f36(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f35(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f34(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f33(V_27A_27,V_27B_27,V_27a0_27))))))). % 2.52/2.70 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x11_27),s__02(V_27A_27,V_27x10_27),s__02(V_27B_27,X1),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x9_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x8_27),s__02(V_27A_27,V_27x7_27),s__02(V_27B_27,V_27x6_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x5_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x4_27)))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f42(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f41(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f40(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f39(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f38(V_27A_27,V_27B_27,V_27a0_27)))). % 2.52/2.70 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x11_27),s__02(V_27A_27,V_27x10_27),s__02(V_27B_27,X1),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x9_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x8_27),s__02(V_27A_27,V_27x7_27),s__02(V_27B_27,V_27x6_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x5_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x4_27)))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f38(V_27A_27,V_27B_27,V_27a0_27))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f36(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f35(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f34(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f33(V_27A_27,V_27B_27,V_27a0_27)))). % 2.52/2.70 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x11_27),s__02(V_27A_27,V_27x10_27),s__02(V_27B_27,X1),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x9_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x8_27),s__02(V_27A_27,V_27x7_27),s__02(V_27B_27,V_27x6_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x5_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x4_27)))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)| -p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f36(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f35(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f34(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f33(V_27A_27,V_27B_27,V_27a0_27))))))). % 2.52/2.70 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x11_27),s__02(V_27A_27,V_27x10_27),s__02(V_27B_27,X1),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x9_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x8_27),s__02(V_27A_27,V_27x7_27),s__02(V_27B_27,V_27x6_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x5_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x4_27)))))| -p__01(s__02(cbool__00,cF__00))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f42(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f41(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f40(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f39(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f38(V_27A_27,V_27B_27,V_27a0_27)))). % 2.52/2.70 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x11_27),s__02(V_27A_27,V_27x10_27),s__02(V_27B_27,X1),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x9_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x8_27),s__02(V_27A_27,V_27x7_27),s__02(V_27B_27,V_27x6_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x5_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x4_27)))))| -p__01(s__02(cbool__00,cF__00))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f38(V_27A_27,V_27B_27,V_27a0_27))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f36(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f35(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f34(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f33(V_27A_27,V_27B_27,V_27a0_27)))). % 2.52/2.70 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x11_27),s__02(V_27A_27,V_27x10_27),s__02(V_27B_27,X1),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x9_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,V_27x8_27),s__02(V_27A_27,V_27x7_27),s__02(V_27B_27,V_27x6_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x5_27),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27x4_27)))))| -p__01(s__02(cbool__00,cF__00))| -p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f36(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f35(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f34(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f33(V_27A_27,V_27B_27,V_27a0_27))))))). % 2.52/2.70 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)| -p__01(s__02(cbool__00,cF__00))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f42(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f41(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f40(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f39(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f38(V_27A_27,V_27B_27,V_27a0_27)))). % 2.52/2.70 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)| -p__01(s__02(cbool__00,cF__00))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f38(V_27A_27,V_27B_27,V_27a0_27))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f36(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f35(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f34(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f33(V_27A_27,V_27B_27,V_27a0_27)))). % 2.52/2.70 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),V_27a0_27)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eTip_27__00)| -p__01(s__02(cbool__00,cF__00))| -p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27A_27,$f36(V_27A_27,V_27B_27,V_27a0_27)),s__02(V_27B_27,$f35(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f34(V_27A_27,V_27B_27,V_27a0_27)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(V_27A_27,V_27B_27),$f33(V_27A_27,V_27B_27,V_27a0_27))))))). % 2.52/2.70 0 [] s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02($c3,$c2),$c1)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02($c3,$c2),c_27const_2ebalanced__map_2eTip_27__00). % 2.52/2.70 0 [] -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02($c3,$c2),$c1)))). % 2.52/2.70 end_of_list. % 2.52/2.70 % 2.52/2.70 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=6. % 2.52/2.70 % 2.52/2.70 This ia a non-Horn set with equality. The strategy will be % 2.52/2.70 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.52/2.70 deletion, with positive clauses in sos and nonpositive % 2.52/2.70 clauses in usable. % 2.52/2.70 % 2.52/2.70 dependent: set(knuth_bendix). % 2.52/2.70 dependent: set(anl_eq). % 2.52/2.70 dependent: set(para_from). % 2.52/2.70 dependent: set(para_into). % 2.52/2.70 dependent: clear(para_from_right). % 2.52/2.70 dependent: clear(para_into_right). % 2.52/2.70 dependent: set(para_from_vars). % 2.52/2.70 dependent: set(eq_units_both_ways). % 2.52/2.70 dependent: set(dynamic_demod_all). % 2.52/2.70 dependent: set(dynamic_demod). % 2.52/2.70 dependent: set(order_eq). % 2.52/2.70 dependent: set(back_demod). % 2.52/2.70 dependent: set(lrpo). % 2.52/2.70 dependent: set(hyper_res). % 2.52/2.70 dependent: set(unit_deletion). % 2.52/2.70 dependent: set(factor). % 2.52/2.70 % 2.52/2.70 ------------> process usable: % 2.52/2.70 ** KEPT (pick-wt=4): 1 [] -p__01(s__02(cbool__00,cF__00)). % 2.52/2.70 ** KEPT (pick-wt=42): 2 [] s__02(A,chapp__02(s__02(cfun__02(B,A),C),s__02(B,$f1(B,A,C,D))))!=s__02(A,chapp__02(s__02(cfun__02(B,A),D),s__02(B,$f1(B,A,C,D))))|s__02(cfun__02(B,A),C)=s__02(cfun__02(B,A),D). % 2.52/2.70 ** KEPT (pick-wt=15): 3 [] -p__01(s__02(cbool__00,A))| -p__01(s__02(cbool__00,B))|s__02(cbool__00,B)=s__02(cbool__00,A). % 2.52/2.70 Following clause subsumed by 1 during input processing: 0 [] -p__01(s__02(cbool__00,cF__00))|p__01(s__02(cbool__00,A)). % 2.52/2.70 ** KEPT (pick-wt=8): 4 [] p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,A)). % 2.52/2.70 Following clause subsumed by 1 during input processing: 0 [] p__01(s__02(cbool__00,A))| -p__01(s__02(cbool__00,cF__00)). % 2.52/2.70 Following clause subsumed by 4 during input processing: 0 [] -p__01(s__02(cbool__00,A))|p__01(s__02(cbool__00,cT__00)). % 2.52/2.70 Following clause subsumed by 1 during input processing: 0 [] -p__01(s__02(cbool__00,cF__00))|p__01(s__02(cbool__00,A)). % 2.52/2.70 Following clause subsumed by 1 during input processing: 0 [] -p__01(s__02(cbool__00,cF__00))|p__01(s__02(cbool__00,A))| -p__01(s__02(cbool__00,cT__00)). % 2.52/2.70 Following clause subsumed by 1 during input processing: 0 [factor_simp] -p__01(s__02(cbool__00,cF__00)). % 2.52/2.70 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)). % 2.52/2.70 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)). % 2.52/2.70 ** KEPT (pick-wt=11): 5 [] s__02(A,B)!=s__02(A,B)|p__01(s__02(cbool__00,cT__00)). % 2.52/2.70 ** KEPT (pick-wt=11): 6 [] s__02(A,B)=s__02(A,B)| -p__01(s__02(cbool__00,cT__00)). % 2.52/2.70 ** KEPT (pick-wt=14): 7 [] s__02(A,B)!=s__02(A,C)|s__02(A,C)=s__02(A,B). % 2.52/2.70 Following clause subsumed by 7 during input processing: 0 [] s__02(A,B)=s__02(A,C)|s__02(A,C)!=s__02(A,B). % 2.52/2.70 ** KEPT (pick-wt=11): 8 [] s__02(cbool__00,cT__00)!=s__02(cbool__00,A)|p__01(s__02(cbool__00,A)). % 2.52/2.70 ** KEPT (pick-wt=11): 9 [] s__02(cbool__00,cT__00)=s__02(cbool__00,A)| -p__01(s__02(cbool__00,A)). % 2.52/2.70 ** KEPT (pick-wt=11): 10 [] s__02(cbool__00,A)!=s__02(cbool__00,cT__00)|p__01(s__02(cbool__00,A)). % 2.52/2.70 ** KEPT (pick-wt=11): 11 [] s__02(cbool__00,A)=s__02(cbool__00,cT__00)| -p__01(s__02(cbool__00,A)). % 2.52/2.70 ** KEPT (pick-wt=11): 12 [] s__02(cbool__00,cF__00)!=s__02(cbool__00,A)| -p__01(s__02(cbool__00,A)). % 2.52/2.70 ** KEPT (pick-wt=11): 13 [] s__02(cbool__00,A)!=s__02(cbool__00,cF__00)| -p__01(s__02(cbool__00,A)). % 2.52/2.70 ** KEPT (pick-wt=15): 15 [copy,14,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)). % 2.52/2.70 ** 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,B))|p__01(s__02(cbool__00,D)). % 2.52/2.70 Following clause subsumed by 15 during input processing: 0 [] s__02(cbool__00,A)!=s__02(cbool__00,B)|s__02(cbool__00,C)!=s__02(cbool__00,D)| -p__01(s__02(cbool__00,C))| -p__01(s__02(cbool__00,B))|p__01(s__02(cbool__00,D)). % 2.52/2.70 ** KEPT (pick-wt=26): 17 [] s__02(cbool__00,A)!=s__02(cbool__00,B)|s__02(cbool__00,C)!=s__02(cbool__00,D)| -p__01(s__02(cbool__00,A))|p__01(s__02(cbool__00,C))| -p__01(s__02(cbool__00,D)). % 2.52/2.70 ** KEPT (pick-wt=31): 18 [] s__02(A,B)!=s__02(A,C)| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),D),s__02(A,B))))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),D),s__02(A,C)))). % 2.52/2.70 ** KEPT (pick-wt=22): 19 [] s__02(A,$f5(A,B,C))=s__02(A,C)| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,C)))). % 2.52/2.70 ** KEPT (pick-wt=27): 20 [] p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,$f5(A,B,C)))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,C)))). % 2.52/2.70 ** KEPT (pick-wt=27): 21 [] -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,$f6(A,B,C)))))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,C)))). % 2.52/2.70 ** KEPT (pick-wt=31): 22 [] s__02(A,B)!=s__02(A,C)|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),D),s__02(A,B))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),D),s__02(A,C)))). % 2.52/2.71 ** KEPT (pick-wt=56): 23 [] s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,C),s__02(A,D),s__02(B,E),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G)))!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,H),s__02(A,I),s__02(B,J),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),K),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),L)))|s__02(c_27type_2enum_2enum_27__00,C)=s__02(c_27type_2enum_2enum_27__00,H). % 2.52/2.71 ** KEPT (pick-wt=56): 24 [] s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,C),s__02(A,D),s__02(B,E),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G)))!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,H),s__02(A,I),s__02(B,J),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),K),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),L)))|s__02(A,D)=s__02(A,I). % 2.52/2.71 ** KEPT (pick-wt=56): 25 [] s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,C),s__02(A,D),s__02(B,E),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G)))!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,H),s__02(A,I),s__02(B,J),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),K),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),L)))|s__02(B,E)=s__02(B,J). % 2.52/2.71 ** KEPT (pick-wt=60): 26 [] s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,C),s__02(A,D),s__02(B,E),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G)))!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,H),s__02(A,I),s__02(B,J),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),K),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),L)))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),F)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),K). % 2.52/2.71 ** KEPT (pick-wt=60): 27 [] s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,C),s__02(A,D),s__02(B,E),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G)))!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,H),s__02(A,I),s__02(B,J),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),K),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),L)))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),L). % 2.52/2.71 ** KEPT (pick-wt=92): 28 [] s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,C),s__02(A,D),s__02(B,E),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G)))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,H),s__02(A,I),s__02(B,J),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),K),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),L)))|s__02(c_27type_2enum_2enum_27__00,C)!=s__02(c_27type_2enum_2enum_27__00,H)|s__02(A,D)!=s__02(A,I)|s__02(B,E)!=s__02(B,J)|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),F)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),K)|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),L). % 2.52/2.71 ** KEPT (pick-wt=30): 30 [copy,29,flip.1] s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,C),s__02(A,D),s__02(B,E),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G)))!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00). % 2.52/2.71 ** KEPT (pick-wt=113): 32 [copy,31,factor_simp] -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),cbool__00),C),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f10(A,B,C)),s__02(A,$f9(A,B,C)),s__02(B,$f8(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f7(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00))))))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),cbool__00),C),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f15(A,B,C)),s__02(A,$f14(A,B,C)),s__02(B,$f13(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f12(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f11(A,B,C)))))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),cbool__00),C),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00)))). % 2.52/2.71 ** KEPT (pick-wt=160): 33 [] -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),cbool__00),C),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f10(A,B,C)),s__02(A,$f9(A,B,C)),s__02(B,$f8(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f7(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00))))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),cbool__00),C),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f19(A,B,C)),s__02(A,$f18(A,B,C)),s__02(B,$f17(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f16(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f15(A,B,C)),s__02(A,$f14(A,B,C)),s__02(B,$f13(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f12(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f11(A,B,C)))))))))| -p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),cbool__00),C),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00))))|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),cbool__00),C),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),D)))). % 2.52/2.71 ** KEPT (pick-wt=138): 35 [copy,34,flip.2,flip.3] -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f23(A,B,C)),s__02(A,$f22(A,B,C)),s__02(B,$f21(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f20(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00)))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f32(A,B,C)),s__02(A,$f31(A,B,C)),s__02(B,$f30(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f29(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f28(A,B,C)),s__02(A,$f27(A,B,C)),s__02(B,$f26(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f25(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f24(A,B,C))))))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00). % 2.52/2.71 ** KEPT (pick-wt=20): 37 [copy,36,unit_del,1] -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00). % 2.52/2.71 Following clause subsumed by 4 during input processing: 0 [] -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,D),s__02(A,E),s__02(B,F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),H)))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),H)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,I),s__02(A,J),s__02(B,K),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),L),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),M)))|p__01(s__02(cbool__00,cT__00)). % 2.52/2.71 ** KEPT (pick-wt=97): 38 [] -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,D),s__02(A,E),s__02(B,F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),H)))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),H)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,I),s__02(A,J),s__02(B,K),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),L),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),M)))|p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,I),s__02(A,J),s__02(B,K),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),L),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),M)))))). % 2.52/2.71 ** KEPT (pick-wt=95): 40 [copy,39,flip.4] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,D),s__02(A,E),s__02(B,F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00)))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00)|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f42(A,B,C)),s__02(A,$f41(A,B,C)),s__02(B,$f40(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f39(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f38(A,B,C))))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C). % 2.52/2.71 ** KEPT (pick-wt=98): 42 [copy,41,flip.4] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,D),s__02(A,E),s__02(B,F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00)))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00)|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(A,B,C)),s__02(A,$f36(A,B,C)),s__02(B,$f35(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f34(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f33(A,B,C))))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f38(A,B,C)). % 2.52/2.71 ** KEPT (pick-wt=97): 43 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,D),s__02(A,E),s__02(B,F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00)))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00)| -p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(A,B,C)),s__02(A,$f36(A,B,C)),s__02(B,$f35(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f34(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f33(A,B,C))))))). % 2.52/2.71 Following clause subsumed by 1 during input processing: 0 [flip.4] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,D),s__02(A,E),s__02(B,F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00)))| -p__01(s__02(cbool__00,cF__00))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f42(A,B,C)),s__02(A,$f41(A,B,C)),s__02(B,$f40(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f39(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f38(A,B,C))))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C). % 2.52/2.71 Following clause subsumed by 1 during input processing: 0 [flip.4] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,D),s__02(A,E),s__02(B,F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00)))| -p__01(s__02(cbool__00,cF__00))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(A,B,C)),s__02(A,$f36(A,B,C)),s__02(B,$f35(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f34(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f33(A,B,C))))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f38(A,B,C)). % 2.52/2.71 Following clause subsumed by 1 during input processing: 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,D),s__02(A,E),s__02(B,F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00)))| -p__01(s__02(cbool__00,cF__00))| -p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(A,B,C)),s__02(A,$f36(A,B,C)),s__02(B,$f35(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f34(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f33(A,B,C))))))). % 2.52/2.71 ** KEPT (pick-wt=114): 45 [copy,44,flip.4] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,D),s__02(A,E),s__02(B,F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,H),s__02(A,I),s__02(B,J),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),K),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),L)))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00)|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f42(A,B,C)),s__02(A,$f41(A,B,C)),s__02(B,$f40(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f39(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f38(A,B,C))))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C). % 2.52/2.71 ** KEPT (pick-wt=117): 47 [copy,46,flip.4] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,D),s__02(A,E),s__02(B,F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,H),s__02(A,I),s__02(B,J),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),K),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),L)))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00)|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(A,B,C)),s__02(A,$f36(A,B,C)),s__02(B,$f35(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f34(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f33(A,B,C))))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f38(A,B,C)). % 2.52/2.71 ** KEPT (pick-wt=116): 48 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,D),s__02(A,E),s__02(B,F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,H),s__02(A,I),s__02(B,J),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),K),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),L)))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00)| -p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(A,B,C)),s__02(A,$f36(A,B,C)),s__02(B,$f35(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f34(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f33(A,B,C))))))). % 2.52/2.71 Following clause subsumed by 1 during input processing: 0 [flip.4] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,D),s__02(A,E),s__02(B,F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,H),s__02(A,I),s__02(B,J),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),K),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),L)))))| -p__01(s__02(cbool__00,cF__00))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f42(A,B,C)),s__02(A,$f41(A,B,C)),s__02(B,$f40(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f39(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f38(A,B,C))))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C). % 2.52/2.71 Following clause subsumed by 1 during input processing: 0 [flip.4] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,D),s__02(A,E),s__02(B,F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,H),s__02(A,I),s__02(B,J),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),K),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),L)))))| -p__01(s__02(cbool__00,cF__00))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(A,B,C)),s__02(A,$f36(A,B,C)),s__02(B,$f35(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f34(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f33(A,B,C))))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f38(A,B,C)). % 2.52/2.71 Following clause subsumed by 1 during input processing: 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,D),s__02(A,E),s__02(B,F),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),G),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,H),s__02(A,I),s__02(B,J),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),K),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),L)))))| -p__01(s__02(cbool__00,cF__00))| -p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(A,B,C)),s__02(A,$f36(A,B,C)),s__02(B,$f35(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f34(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f33(A,B,C))))))). % 2.52/2.71 Following clause subsumed by 1 during input processing: 0 [flip.4] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00)| -p__01(s__02(cbool__00,cF__00))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f42(A,B,C)),s__02(A,$f41(A,B,C)),s__02(B,$f40(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f39(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f38(A,B,C))))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C). % 2.52/2.71 Following clause subsumed by 1 during input processing: 0 [flip.4] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00)| -p__01(s__02(cbool__00,cF__00))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(A,B,C)),s__02(A,$f36(A,B,C)),s__02(B,$f35(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f34(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f33(A,B,C))))=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f38(A,B,C)). % 2.52/2.71 Following clause subsumed by 1 during input processing: 0 [] p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C))))|s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),C)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eTip_27__00)| -p__01(s__02(cbool__00,cF__00))| -p__01(s__02(cbool__00,cT__00))| -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),c_27const_2ebalanced__map_2eBin_27__05(s__02(c_27type_2enum_2enum_27__00,$f37(A,B,C)),s__02(A,$f36(A,B,C)),s__02(B,$f35(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f34(A,B,C)),s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02(A,B),$f33(A,B,C))))))). % 2.52/2.71 ** KEPT (pick-wt=11): 50 [copy,49,flip.1] s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02($c3,$c2),c_27const_2ebalanced__map_2eTip_27__00)!=s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02($c3,$c2),$c1). % 2.52/2.71 ** KEPT (pick-wt=9): 51 [] -p__01(s__02(cbool__00,c_27const_2eMapProg_2edeletefindmax__side_27__01(s__02(c_27type_2ebalanced__map_2ebalanced__map_27__02($c3,$c2),$c1)))). % 2.52/2.71 % 2.52/2.71 ------------> process sos: % 2.52/2.71 ** KEPT (pick-wt=3): 65 [] A=A. % 2.52/2.71 ** KEPT (pick-wt=4): 66 [] p__01(s__02(cbool__00,cT__00)). % 2.66/2.83 ** KEPT (pick-wt=14): 67 [] s__02(cbool__00,A)=s__02(cbool__00,cT__00)|s__02(cbool__00,A)=s__02(cbool__00,cF__00). % 2.66/2.83 Following clause subsumed by 66 during input processing: 0 [] p__01(s__02(cbool__00,cT__00)). % 2.66/2.83 ** KEPT (pick-wt=15): 68 [] p__01(s__02(cbool__00,A))|p__01(s__02(cbool__00,B))|s__02(cbool__00,A)=s__02(cbool__00,B). % 2.66/2.83 Following clause subsumed by 66 during input processing: 0 [] p__01(s__02(cbool__00,cT__00)). % 2.66/2.83 Following clause subsumed by 66 during input processing: 0 [unit_del,1] p__01(s__02(cbool__00,cT__00)). % 2.66/2.83 Following clause subsumed by 66 during input processing: 0 [unit_del,1] p__01(s__02(cbool__00,cT__00)). % 2.66/2.83 ** KEPT (pick-wt=11): 69 [] s__02(cbool__00,cF__00)=s__02(cbool__00,A)|p__01(s__02(cbool__00,A)). % 2.66/2.83 ** KEPT (pick-wt=11): 70 [] s__02(cbool__00,A)=s__02(cbool__00,cF__00)|p__01(s__02(cbool__00,A)). % 2.66/2.83 ** KEPT (pick-wt=9): 71 [] s__02(A,$f4(A,B))=s__02(A,B). % 2.66/2.83 ---> New Demodulator: 72 [new_demod,71] s__02(A,$f4(A,B))=s__02(A,B). % 2.66/2.83 ** KEPT (pick-wt=22): 73 [] s__02(A,$f6(A,B,C))=s__02(A,C)|p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(A,cbool__00),B),s__02(A,C)))). % 2.66/2.83 Following clause subsumed by 65 during input processing: 0 [copy,65,flip.1] A=A. % 2.66/2.83 65 back subsumes 52. % 2.66/2.83 65 back subsumes 6. % 2.66/2.83 66 back subsumes 5. % 2.66/2.83 66 back subsumes 4. % 2.66/2.83 >>>> Starting back demodulation with 72. % 2.66/2.83 % 2.66/2.83 ======= end of input processing ======= % 2.66/2.83 % 2.66/2.83 =========== start of search =========== % 2.66/2.83 % 2.66/2.83 % 2.66/2.83 Resetting weight limit to 4. % 2.66/2.83 % 2.66/2.83 % 2.66/2.83 Resetting weight limit to 4. % 2.66/2.83 % 2.66/2.83 sos_size=7 % 2.66/2.83 % 2.66/2.83 Search stopped because sos empty. % 2.66/2.83 % 2.66/2.83 % 2.66/2.83 Search stopped because sos empty. % 2.66/2.83 % 2.66/2.83 ============ end of search ============ % 2.66/2.83 % 2.66/2.83 -------------- statistics ------------- % 2.66/2.83 clauses given 8 % 2.66/2.83 clauses generated 3361 % 2.66/2.83 clauses kept 62 % 2.66/2.83 clauses forward subsumed 58 % 2.66/2.83 clauses back subsumed 4 % 2.66/2.83 Kbytes malloced 6835 % 2.66/2.83 % 2.66/2.83 ----------- times (seconds) ----------- % 2.66/2.83 user CPU time 0.14 (0 hr, 0 min, 0 sec) % 2.66/2.83 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 2.66/2.83 wall-clock time 3 (0 hr, 0 min, 3 sec) % 2.66/2.83 % 2.66/2.83 Process 22871 finished Wed Jul 27 03:02:41 2022 % 2.66/2.83 Otter interrupted % 2.66/2.83 PROOF NOT FOUND %------------------------------------------------------------------------------