%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SWV849-1 : TPTP v9.2.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n009.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 Jun 3 09:02:30 AM UTC 2026 % Result : Unsatisfiable 3.02s 3.20s % Output : Proof 3.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.14 % Problem : SWV849-1 : TPTP v9.2.1. Released v4.1.0. % 0.12/0.15 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.17/0.37 % Computer : n009.cluster.edu % 0.17/0.37 % Model : x86_64 x86_64 % 0.17/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.37 % Memory : 8042.1875MB % 0.17/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.37 % CPULimit : 300 % 0.17/0.37 % WCLimit : 300 % 0.17/0.37 % DateTime : Tue Jun 2 21:16:59 EDT 2026 % 0.17/0.37 % CPUTime : % 0.38/0.65 %----Proving TF0_NAR, FOF, or CNF % 0.38/0.66 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 3.02/3.20 % SZS status Unsatisfiable % 3.02/3.20 % SZS output start Proof % 3.02/3.23 ( % 3.02/3.23 (declare-sort $$unsorted 0) % 3.02/3.23 (declare-const tptp.v_G $$unsorted) % 3.02/3.23 (declare-const tptp.v_b $$unsorted) % 3.02/3.23 (declare-const tptp.v_s2 $$unsorted) % 3.02/3.23 (declare-const tptp.v_ca $$unsorted) % 3.02/3.23 (declare-const tptp.v_na $$unsorted) % 3.02/3.23 (declare-const tptp.v_s1 $$unsorted) % 3.02/3.23 (declare-const tptp.v_ba $$unsorted) % 3.02/3.23 (declare-const tptp.v_s0 $$unsorted) % 3.02/3.23 (declare-const tptp.c_Natural_Osko__Natural__Xevaln__WHILE__case__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.v_sko__Hoare__Mirabelle__Xtriples__valid__Suc__1 (-> $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.tc_Hoare__Mirabelle_Otriple (-> $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_Hoare__Mirabelle_Ohoare__valids (-> $$unsorted $$unsorted $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.c_Hoare__Mirabelle_Otriple__valid (-> $$unsorted $$unsorted $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.c_Natural_Oevaln (-> $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.c_Com_Ocom_OWhile (-> $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.class_Lattices_Odistrib__lattice (-> $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.c_SetInterval_Oord_OlessThan (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.class_Lattices_Olattice (-> $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.c_Com_Ocom_OCall (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.class_Lattices_Olower__semilattice (-> $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.c_Lattices_Oupper__semilattice__class_Osup (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_ATP__Linkup_Osko__Set__XballE__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.v_c $$unsorted) % 3.02/3.23 (declare-const tptp.c_Complete__Lattice_Ocomplete__lattice__class_OSUPR (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_Set_Oinsert (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_ATP__Linkup_Osko__Set__XbexI__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_ATP__Linkup_Osko__Set__Xrev__bexI__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.tc_bool $$unsorted) % 3.02/3.23 (declare-const tptp.c_fequal (-> $$unsorted $$unsorted $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.v_xa $$unsorted) % 3.02/3.23 (declare-const tptp.t_a $$unsorted) % 3.02/3.23 (declare-const tptp.hAPP (-> $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_Lattices_Olower__semilattice__class_Oinf (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_COMBI (-> $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_SetInterval_Oord_OgreaterThan (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_Set_Oimage (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.v_x $$unsorted) % 3.02/3.23 (declare-const tptp.c_Com_Ocom_Ocom__rec (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_Fun_Oid (-> $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_in (-> $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_HOL_Ominus__class_Ominus (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_Com_OWT (-> $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.c_Com_Ocom_OAss (-> $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.tc_fun (-> $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.v_n (-> $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_Com_Ocom_OSemi (-> $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_Com_Ocom_OSKIP $$unsorted) % 3.02/3.23 (declare-const tptp.c_Com_Ocom_Ocom__case (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.class_OrderedGroup_Oab__group__add (-> $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.c_Suc (-> $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_Com_Ocom_OBODY (-> $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.v_sko__Hoare__Mirabelle__Xhoare__valids__def__2 (-> $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.class_Orderings_Olinorder (-> $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.class_Complete__Lattice_Ocomplete__lattice (-> $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.c_Natural_Osko__Natural__Xevaln__max2__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_Com_Ocom_OLocal (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.v_xb $$unsorted) % 3.02/3.23 (declare-const tptp.c_lessequals (-> $$unsorted $$unsorted $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.c_ATP__Linkup_Osko__Complete__Lattice__Xbex__UN__1__3 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.v_sko__Hoare__Mirabelle__Xhoare__valids__def__1 (-> $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.class_HOL_Ominus (-> $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.c_Fun_Ocomp (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.hBOOL (-> $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.class_Orderings_Obot (-> $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.c_SetInterval_Oord_OatLeastLessThan (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_Set_Ovimage (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_SetInterval_Oord_OatLeastAtMost (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_ATP__Linkup_Osko__Set__XbexE__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.class_Lattices_Obounded__lattice (-> $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.c_COMBC (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_Complete__Lattice_Ocomplete__lattice (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.class_Lattices_Oupper__semilattice (-> $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.tc_nat $$unsorted) % 3.02/3.23 (declare-const tptp.class_Orderings_Oorder (-> $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.c_Orderings_Obot__class_Obot (-> $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_ATP__Linkup_Osko__Complete__Lattice__Xball__conj__distrib__1__1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_SetInterval_Oord_OatMost (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.v_P $$unsorted) % 3.02/3.23 (declare-const tptp.c_Com_Ocom_OCond (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_ATP__Linkup_Osko__Set__Xbex__Un__1__3 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_Fun_Ofcomp (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.c_Natural_Oevalc (-> $$unsorted $$unsorted $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.class_Orderings_Opreorder (-> $$unsorted Bool)) % 3.02/3.23 (declare-const tptp.c_Hoare__Mirabelle_Otriple_Otriple (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 3.02/3.23 (declare-const tptp.class_OrderedGroup_Opordered__ab__group__add (-> $$unsorted Bool)) % 3.02/3.23 (define @t1 () (@var "V_pname_H" $$unsorted)) % 3.02/3.23 (define @t2 () (@var "V_pname" $$unsorted)) % 3.02/3.23 (define @t3 () (= @t2 @t1)) % 3.02/3.23 (define @t4 () (@var "V_fun_H" $$unsorted)) % 3.02/3.23 (define @t5 () (@var "V_vname_H" $$unsorted)) % 3.02/3.23 (define @t6 () (tptp.c_Com_Ocom_OCall @t5 @t1 @t4)) % 3.02/3.23 (define @t7 () (@var "V_fun" $$unsorted)) % 3.02/3.23 (define @t8 () (@var "V_vname" $$unsorted)) % 3.02/3.23 (define @t9 () (tptp.c_Com_Ocom_OCall @t8 @t2 @t7)) % 3.02/3.23 (define @t10 () (not (= @t9 @t6))) % 3.02/3.23 (define @t11 () (@list @t8 @t2 @t7 @t5 @t1 @t4)) % 3.02/3.23 (define @t12 () (= @t7 @t4)) % 3.02/3.23 (define @t13 () (@var "V_Y" $$unsorted)) % 3.02/3.23 (define @t14 () (@var "T_a" $$unsorted)) % 3.02/3.23 (define @t15 () (tptp.c_COMBI @t14)) % 3.02/3.23 (define @t16 () (@list @t14 @t13)) % 3.02/3.23 (define @t17 () (@var "V_com" $$unsorted)) % 3.02/3.23 (define @t18 () (@var "V_f8" $$unsorted)) % 3.02/3.23 (define @t19 () (@var "V_f7" $$unsorted)) % 3.02/3.23 (define @t20 () (@var "V_f6" $$unsorted)) % 3.02/3.23 (define @t21 () (@var "V_f5" $$unsorted)) % 3.02/3.23 (define @t22 () (@var "V_f4" $$unsorted)) % 3.02/3.23 (define @t23 () (@var "V_f3" $$unsorted)) % 3.02/3.23 (define @t24 () (@var "V_f2" $$unsorted)) % 3.02/3.23 (define @t25 () (@var "V_f1" $$unsorted)) % 3.02/3.23 (define @t26 () (tptp.c_Com_Ocom_Ocom__rec @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t17 @t14)) % 3.02/3.23 (define @t27 () (@var "V_loc" $$unsorted)) % 3.02/3.23 (define @t28 () (tptp.hAPP (tptp.hAPP (tptp.hAPP @t23 @t27) @t7) @t17)) % 3.02/3.23 (define @t29 () (tptp.c_Com_Ocom_OLocal @t27 @t7 @t17)) % 3.02/3.23 (define @t30 () (@list @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t27 @t7 @t17 @t14)) % 3.02/3.23 (define @t31 () (@var "V_com2_H" $$unsorted)) % 3.02/3.23 (define @t32 () (@var "V_com1_H" $$unsorted)) % 3.02/3.23 (define @t33 () (tptp.c_Com_Ocom_OSemi @t32 @t31)) % 3.02/3.23 (define @t34 () (tptp.c_Com_Ocom_OAss @t8 @t7)) % 3.02/3.23 (define @t35 () (@list @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t14)) % 3.02/3.23 (define @t36 () (tptp.c_Com_Ocom_OBODY @t2)) % 3.02/3.23 (define @t37 () (tptp.c_Com_Ocom_OCond @t4 @t32 @t31)) % 3.02/3.23 (define @t38 () (@var "V_B" $$unsorted)) % 3.02/3.23 (define @t39 () (@var "V_x" $$unsorted)) % 3.02/3.23 (define @t40 () (tptp.c_in @t14)) % 3.02/3.23 (define @t41 () (tptp.hAPP @t40 @t39)) % 3.02/3.23 (define @t42 () (tptp.hBOOL (tptp.hAPP @t41 @t38))) % 3.02/3.23 (define @t43 () (not @t42)) % 3.02/3.23 (define @t44 () (tptp.tc_fun @t14 tptp.tc_bool)) % 3.02/3.23 (define @t45 () (@var "V_A" $$unsorted)) % 3.02/3.23 (define @t46 () (tptp.c_HOL_Ominus__class_Ominus @t45 @t38 @t44)) % 3.02/3.23 (define @t47 () (tptp.c_Set_Oinsert @t39 @t45 @t14)) % 3.02/3.23 (define @t48 () (tptp.c_HOL_Ominus__class_Ominus @t47 @t38 @t44)) % 3.02/3.23 (define @t49 () (@list @t39 @t45 @t14 @t38)) % 3.02/3.23 (define @t50 () (@var "V_i" $$unsorted)) % 3.02/3.23 (define @t51 () (tptp.hAPP @t40 @t50)) % 3.02/3.23 (define @t52 () (@var "T_b" $$unsorted)) % 3.02/3.23 (define @t53 () (@var "V_M" $$unsorted)) % 3.02/3.23 (define @t54 () (@var "V_com2" $$unsorted)) % 3.02/3.23 (define @t55 () (@var "V_com1" $$unsorted)) % 3.02/3.23 (define @t56 () (tptp.c_Com_Ocom_OCond @t7 @t55 @t54)) % 3.02/3.23 (define @t57 () (tptp.c_Com_Ocom_OSemi @t55 @t54)) % 3.02/3.23 (define @t58 () (tptp.c_Com_Ocom_OBODY @t1)) % 3.02/3.23 (define @t59 () (tptp.c_Orderings_Obot__class_Obot @t44)) % 3.02/3.23 (define @t60 () (@var "V_a" $$unsorted)) % 3.02/3.23 (define @t61 () (tptp.c_Set_Oinsert @t60 @t59 @t14)) % 3.02/3.23 (define @t62 () (@var "V_b" $$unsorted)) % 3.02/3.23 (define @t63 () (tptp.hAPP @t40 @t62)) % 3.02/3.23 (define @t64 () (tptp.c_Lattices_Olower__semilattice__class_Oinf @t45 @t38 @t44)) % 3.02/3.23 (define @t65 () (not (= @t64 @t59))) % 3.02/3.23 (define @t66 () (@list @t45 @t38 @t14)) % 3.02/3.23 (define @t67 () (@var "V_g" $$unsorted)) % 3.02/3.23 (define @t68 () (tptp.hAPP @t67 tptp.v_x)) % 3.02/3.23 (define @t69 () (@var "V_f" $$unsorted)) % 3.02/3.23 (define @t70 () (tptp.hAPP @t69 tptp.v_x)) % 3.02/3.23 (define @t71 () (tptp.tc_fun tptp.t_a @t52)) % 3.02/3.23 (define @t72 () (not (tptp.class_Lattices_Olattice @t52))) % 3.02/3.23 (define @t73 () (@list @t52 @t69 @t67)) % 3.02/3.23 (define @t74 () (@var "V_C" $$unsorted)) % 3.02/3.23 (define @t75 () (tptp.c_Lattices_Olower__semilattice__class_Oinf @t74 @t45 @t44)) % 3.02/3.23 (define @t76 () (tptp.c_Lattices_Olower__semilattice__class_Oinf @t38 @t45 @t44)) % 3.02/3.23 (define @t77 () (tptp.c_Lattices_Oupper__semilattice__class_Osup @t38 @t74 @t44)) % 3.02/3.23 (define @t78 () (@list @t38 @t74 @t14 @t45)) % 3.02/3.23 (define @t79 () (tptp.c_Lattices_Olower__semilattice__class_Oinf @t45 @t74 @t44)) % 3.02/3.23 (define @t80 () (@list @t45 @t38 @t74 @t14)) % 3.02/3.23 (define @t81 () (@var "V_z" $$unsorted)) % 3.02/3.23 (define @t82 () (tptp.c_Lattices_Olower__semilattice__class_Oinf @t39 @t81 @t14)) % 3.02/3.23 (define @t83 () (@var "V_y" $$unsorted)) % 3.02/3.23 (define @t84 () (tptp.c_Lattices_Olower__semilattice__class_Oinf @t39 @t83 @t14)) % 3.02/3.23 (define @t85 () (tptp.c_Lattices_Oupper__semilattice__class_Osup @t84 @t82 @t14)) % 3.02/3.23 (define @t86 () (tptp.c_Lattices_Oupper__semilattice__class_Osup @t83 @t81 @t14)) % 3.02/3.23 (define @t87 () (tptp.c_Lattices_Olower__semilattice__class_Oinf @t39 @t86 @t14)) % 3.02/3.23 (define @t88 () (not (tptp.class_Lattices_Odistrib__lattice @t14))) % 3.02/3.23 (define @t89 () (@list @t14 @t39 @t83 @t81)) % 3.02/3.23 (define @t90 () (tptp.c_Lattices_Olower__semilattice__class_Oinf @t83 @t39 @t14)) % 3.02/3.23 (define @t91 () (@list @t14 @t83 @t81 @t39)) % 3.02/3.23 (define @t92 () (tptp.c_Fun_Oid @t14)) % 3.02/3.23 (define @t93 () (tptp.c_Fun_Oid @t52)) % 3.02/3.23 (define @t94 () (@list @t45 @t14)) % 3.02/3.23 (define @t95 () (not (tptp.class_Lattices_Oupper__semilattice @t14))) % 3.02/3.23 (define @t96 () (@list @t14 @t39)) % 3.02/3.23 (define @t97 () (tptp.hAPP (tptp.hAPP (tptp.hAPP @t18 @t8) @t2) @t7)) % 3.02/3.23 (define @t98 () (@list @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t8 @t2 @t7 @t14)) % 3.02/3.23 (define @t99 () (tptp.c_Set_Oinsert @t83 @t45 @t14)) % 3.02/3.23 (define @t100 () (tptp.tc_fun @t52 tptp.tc_bool)) % 3.02/3.23 (define @t101 () (tptp.c_Orderings_Obot__class_Obot @t100)) % 3.02/3.23 (define @t102 () (tptp.c_Complete__Lattice_Ocomplete__lattice__class_OSUPR @t101 @t38 @t52 @t44)) % 3.02/3.23 (define @t103 () (@list @t45 @t52 @t38 @t14)) % 3.02/3.23 (define @t104 () (@var "V_Q" $$unsorted)) % 3.02/3.23 (define @t105 () (@var "V_R" $$unsorted)) % 3.02/3.23 (define @t106 () (@var "V_P" $$unsorted)) % 3.02/3.23 (define @t107 () (@var "T_c" $$unsorted)) % 3.02/3.23 (define @t108 () (tptp.hAPP (tptp.hAPP @t24 @t8) @t7)) % 3.02/3.23 (define @t109 () (@list @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t8 @t7 @t14)) % 3.02/3.23 (define @t110 () (@var "V_xa" $$unsorted)) % 3.02/3.23 (define @t111 () (tptp.c_Set_Oinsert @t39 @t59 @t14)) % 3.02/3.23 (define @t112 () (tptp.c_HOL_Ominus__class_Ominus @t39 @t39 @t14)) % 3.02/3.23 (define @t113 () (not (tptp.class_OrderedGroup_Oab__group__add @t14))) % 3.02/3.23 (define @t114 () (@var "V_y_H" $$unsorted)) % 3.02/3.23 (define @t115 () (@var "V_x_H" $$unsorted)) % 3.02/3.23 (define @t116 () (tptp.c_HOL_Ominus__class_Ominus @t115 @t114 @t14)) % 3.02/3.23 (define @t117 () (tptp.c_Set_Oimage @t69 @t101 @t52 @t14)) % 3.02/3.23 (define @t118 () (@list @t69 @t52 @t14)) % 3.02/3.23 (define @t119 () (@var "V_s" $$unsorted)) % 3.02/3.23 (define @t120 () (tptp.hBOOL (tptp.hAPP @t62 @t119))) % 3.02/3.23 (define @t121 () (not @t120)) % 3.02/3.23 (define @t122 () (@var "V_s1" $$unsorted)) % 3.02/3.23 (define @t123 () (@var "V_c0" $$unsorted)) % 3.02/3.23 (define @t124 () (@var "V_c1" $$unsorted)) % 3.02/3.23 (define @t125 () (tptp.c_Com_Ocom_OCond @t62 @t123 @t124)) % 3.02/3.23 (define @t126 () (tptp.c_Natural_Oevalc @t125 @t119 @t122)) % 3.02/3.23 (define @t127 () (@list @t62 @t123 @t124 @t119 @t122)) % 3.02/3.23 (define @t128 () (@var "V_t" $$unsorted)) % 3.02/3.23 (define @t129 () (@var "V_c2" $$unsorted)) % 3.02/3.23 (define @t130 () (tptp.c_Com_Ocom_OCond @t62 @t124 @t129)) % 3.02/3.23 (define @t131 () (not (tptp.c_Natural_Oevalc @t130 @t119 @t128))) % 3.02/3.23 (define @t132 () (tptp.c_Natural_Oevalc @t124 @t119 @t128)) % 3.02/3.23 (define @t133 () (@var "V_s0" $$unsorted)) % 3.02/3.23 (define @t134 () (@var "V_s2" $$unsorted)) % 3.02/3.23 (define @t135 () (tptp.c_Com_Ocom_OSemi @t123 @t124)) % 3.02/3.23 (define @t136 () (@var "V_X" $$unsorted)) % 3.02/3.23 (define @t137 () (tptp.c_Lattices_Oupper__semilattice__class_Osup @t45 @t74 @t44)) % 3.02/3.23 (define @t138 () (tptp.c_Lattices_Oupper__semilattice__class_Osup @t45 @t77 @t44)) % 3.02/3.23 (define @t139 () (tptp.c_Lattices_Oupper__semilattice__class_Osup @t45 @t38 @t44)) % 3.02/3.23 (define @t140 () (@list @t45 @t38 @t14 @t74)) % 3.02/3.23 (define @t141 () (tptp.c_Lattices_Oupper__semilattice__class_Osup @t39 @t86 @t14)) % 3.02/3.23 (define @t142 () (tptp.c_Lattices_Oupper__semilattice__class_Osup @t39 @t83 @t14)) % 3.02/3.23 (define @t143 () (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t142 @t81 @t14) @t141)) % 3.02/3.23 (define @t144 () (tptp.c_Lattices_Oupper__semilattice__class_Osup @t39 @t81 @t14)) % 3.02/3.23 (define @t145 () (= @t141 (tptp.c_Lattices_Oupper__semilattice__class_Osup @t83 @t144 @t14))) % 3.02/3.23 (define @t146 () (not (tptp.class_Lattices_Olattice @t14))) % 3.02/3.23 (define @t147 () (tptp.c_lessequals @t39 @t83 @t14)) % 3.02/3.23 (define @t148 () (not @t147)) % 3.02/3.23 (define @t149 () (= @t84 @t39)) % 3.02/3.23 (define @t150 () (not (tptp.class_Lattices_Olower__semilattice @t14))) % 3.02/3.23 (define @t151 () (@list @t14 @t39 @t83)) % 3.02/3.23 (define @t152 () (tptp.c_lessequals @t83 @t39 @t14)) % 3.02/3.23 (define @t153 () (not @t152)) % 3.02/3.23 (define @t154 () (@var "V_pn" $$unsorted)) % 3.02/3.23 (define @t155 () (tptp.c_lessequals @t60 @t39 @t14)) % 3.02/3.23 (define @t156 () (not @t155)) % 3.02/3.23 (define @t157 () (tptp.c_lessequals @t62 @t39 @t14)) % 3.02/3.23 (define @t158 () (not @t157)) % 3.02/3.23 (define @t159 () (tptp.c_Lattices_Oupper__semilattice__class_Osup @t60 @t62 @t14)) % 3.02/3.23 (define @t160 () (tptp.c_lessequals @t159 @t39 @t14)) % 3.02/3.23 (define @t161 () (@list @t14 @t60 @t62 @t39)) % 3.02/3.23 (define @t162 () (tptp.c_lessequals @t39 @t142 @t14)) % 3.02/3.23 (define @t163 () (tptp.c_lessequals @t83 @t142 @t14)) % 3.02/3.23 (define @t164 () (@list @t14 @t83 @t39)) % 3.02/3.23 (define @t165 () (tptp.c_lessequals @t81 @t39 @t14)) % 3.02/3.23 (define @t166 () (tptp.c_lessequals @t39 @t81 @t14)) % 3.02/3.23 (define @t167 () (not @t166)) % 3.02/3.23 (define @t168 () (tptp.c_lessequals @t83 @t81 @t14)) % 3.02/3.23 (define @t169 () (not @t168)) % 3.02/3.23 (define @t170 () (tptp.c_lessequals @t142 @t81 @t14)) % 3.02/3.23 (define @t171 () (= @t8 @t5)) % 3.02/3.23 (define @t172 () (tptp.c_Com_Ocom_Ocom__rec @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t54 @t14)) % 3.02/3.23 (define @t173 () (tptp.c_Com_Ocom_Ocom__rec @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t55 @t14)) % 3.02/3.23 (define @t174 () (tptp.hAPP (tptp.hAPP @t22 @t55) @t54)) % 3.02/3.23 (define @t175 () (@list @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t55 @t54 @t14)) % 3.02/3.23 (define @t176 () (= @t45 @t101)) % 3.02/3.23 (define @t177 () (tptp.c_Set_Oimage @t69 @t45 @t52 @t14)) % 3.02/3.23 (define @t178 () (tptp.c_Set_Oinsert @t60 @t38 @t14)) % 3.02/3.23 (define @t179 () (@list @t60 @t38 @t14 @t74)) % 3.02/3.23 (define @t180 () (@list @t45 @t60 @t38 @t14)) % 3.02/3.23 (define @t181 () (tptp.c_Set_Ovimage @t69 @t38 @t14 @t52)) % 3.02/3.23 (define @t182 () (tptp.c_Set_Ovimage @t69 @t45 @t14 @t52)) % 3.02/3.23 (define @t183 () (@list @t69 @t45 @t38 @t52 @t14)) % 3.02/3.23 (define @t184 () (tptp.c_Orderings_Obot__class_Obot @t14)) % 3.02/3.23 (define @t185 () (= @t54 @t31)) % 3.02/3.23 (define @t186 () (not (= @t57 @t33))) % 3.02/3.23 (define @t187 () (@list @t55 @t54 @t32 @t31)) % 3.02/3.23 (define @t188 () (= @t55 @t32)) % 3.02/3.23 (define @t189 () (tptp.c_HOL_Ominus__class_Ominus @t45 @t178 @t44)) % 3.02/3.23 (define @t190 () (tptp.c_HOL_Ominus__class_Ominus @t45 @t61 @t44)) % 3.02/3.23 (define @t191 () (tptp.c_Set_Oinsert @t60 @t45 @t14)) % 3.02/3.23 (define @t192 () (@list @t60 @t45 @t14)) % 3.02/3.23 (define @t193 () (@var "T_aa" $$unsorted)) % 3.02/3.23 (define @t194 () (tptp.hAPP @t69 @t60)) % 3.02/3.23 (define @t195 () (tptp.c_in @t193)) % 3.02/3.23 (define @t196 () (tptp.c_Set_Oinsert @t60 @t64 @t14)) % 3.02/3.23 (define @t197 () (@list @t39 @t45 @t14)) % 3.02/3.23 (define @t198 () (@var "V_com_H" $$unsorted)) % 3.02/3.23 (define @t199 () (@var "V_loc_H" $$unsorted)) % 3.02/3.23 (define @t200 () (tptp.c_Com_Ocom_OLocal @t199 @t4 @t198)) % 3.02/3.23 (define @t201 () (tptp.hBOOL (tptp.hAPP @t99 @t39))) % 3.02/3.23 (define @t202 () (tptp.hBOOL (tptp.hAPP @t45 @t39))) % 3.02/3.23 (define @t203 () (tptp.c_in @t52)) % 3.02/3.23 (define @t204 () (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t203 @t39) @t45)))) % 3.02/3.23 (define @t205 () (tptp.hAPP @t38 @t39)) % 3.02/3.23 (define @t206 () (= @t205 @t59)) % 3.02/3.23 (define @t207 () (tptp.c_Complete__Lattice_Ocomplete__lattice__class_OSUPR @t45 @t38 @t52 @t44)) % 3.02/3.23 (define @t208 () (not (tptp.class_Lattices_Obounded__lattice @t14))) % 3.02/3.23 (define @t209 () (@list @t14 @t38)) % 3.02/3.23 (define @t210 () (@var "V_I" $$unsorted)) % 3.02/3.23 (define @t211 () (@var "V_k" $$unsorted)) % 3.02/3.23 (define @t212 () (tptp.c_Complete__Lattice_Ocomplete__lattice__class_OSUPR @t210 @t45 @t14 @t100)) % 3.02/3.23 (define @t213 () (@var "V_top" $$unsorted)) % 3.02/3.23 (define @t214 () (@var "V_bot" $$unsorted)) % 3.02/3.23 (define @t215 () (@var "V_sup" $$unsorted)) % 3.02/3.23 (define @t216 () (@var "V_inf" $$unsorted)) % 3.02/3.23 (define @t217 () (@var "V_less" $$unsorted)) % 3.02/3.23 (define @t218 () (@var "V_less__eq" $$unsorted)) % 3.02/3.23 (define @t219 () (@var "V_Sup" $$unsorted)) % 3.02/3.23 (define @t220 () (@var "V_Inf" $$unsorted)) % 3.02/3.23 (define @t221 () (not (tptp.c_Complete__Lattice_Ocomplete__lattice @t220 @t219 @t218 @t217 @t216 @t215 @t214 @t213 @t14))) % 3.02/3.23 (define @t222 () (tptp.hAPP @t215 @t60)) % 3.02/3.23 (define @t223 () (tptp.c_Set_Oinsert @t62 @t59 @t14)) % 3.02/3.23 (define @t224 () (tptp.c_Set_Oinsert @t60 @t223 @t14)) % 3.02/3.23 (define @t225 () (tptp.hAPP @t216 @t60)) % 3.02/3.23 (define @t226 () (not (= @t56 @t37))) % 3.02/3.23 (define @t227 () (@list @t7 @t55 @t54 @t4 @t32 @t31)) % 3.02/3.23 (define @t228 () (tptp.hAPP @t69 (tptp.hAPP @t67 @t39))) % 3.02/3.23 (define @t229 () (tptp.hAPP (tptp.c_Fun_Ocomp @t69 @t67 @t52 @t14 @t107) @t39)) % 3.02/3.23 (define @t230 () (@var "V_v" $$unsorted)) % 3.02/3.23 (define @t231 () (tptp.c_Fun_Ocomp @t60 @t62 @t107 @t52 @t14)) % 3.02/3.23 (define @t232 () (tptp.hAPP @t60 (tptp.hAPP @t62 @t230))) % 3.02/3.23 (define @t233 () (= @t39 @t83)) % 3.02/3.23 (define @t234 () (@var "V_nat_H" $$unsorted)) % 3.02/3.23 (define @t235 () (@var "V_nat" $$unsorted)) % 3.02/3.23 (define @t236 () (tptp.hBOOL (tptp.hAPP @t139 @t39))) % 3.02/3.23 (define @t237 () (tptp.hBOOL @t205)) % 3.02/3.23 (define @t238 () (@list @t38 @t39 @t45 @t14)) % 3.02/3.23 (define @t239 () (not @t237)) % 3.02/3.23 (define @t240 () (@list @t45 @t38 @t14 @t39)) % 3.02/3.23 (define @t241 () (not @t202)) % 3.02/3.23 (define @t242 () (not (tptp.c_Com_OWT @t123))) % 3.02/3.23 (define @t243 () (tptp.c_Com_OWT @t124)) % 3.02/3.23 (define @t244 () (not @t243)) % 3.02/3.23 (define @t245 () (tptp.c_Lattices_Olower__semilattice__class_Oinf @t83 @t81 @t14)) % 3.02/3.23 (define @t246 () (tptp.c_Lattices_Olower__semilattice__class_Oinf @t39 @t245 @t14)) % 3.02/3.23 (define @t247 () (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t84 @t81 @t14) @t246)) % 3.02/3.23 (define @t248 () (= @t246 (tptp.c_Lattices_Olower__semilattice__class_Oinf @t83 @t82 @t14))) % 3.02/3.23 (define @t249 () (tptp.c_Lattices_Olower__semilattice__class_Oinf @t38 @t74 @t44)) % 3.02/3.23 (define @t250 () (tptp.c_Lattices_Olower__semilattice__class_Oinf @t45 @t249 @t44)) % 3.02/3.23 (define @t251 () (@list @t14 @t45)) % 3.02/3.23 (define @t252 () (tptp.c_HOL_Ominus__class_Ominus @t79 @t249 @t44)) % 3.02/3.23 (define @t253 () (@list @t199 @t4 @t198)) % 3.02/3.23 (define @t254 () (tptp.hBOOL (tptp.hAPP @t41 @t45))) % 3.02/3.23 (define @t255 () (not @t254)) % 3.02/3.23 (define @t256 () (tptp.c_Lattices_Olower__semilattice__class_Oinf @t142 @t144 @t14)) % 3.02/3.23 (define @t257 () (tptp.c_Lattices_Oupper__semilattice__class_Osup @t39 @t245 @t14)) % 3.02/3.23 (define @t258 () (@var "V_n" $$unsorted)) % 3.02/3.23 (define @t259 () (@var "V_m" $$unsorted)) % 3.02/3.23 (define @t260 () (tptp.c_lessequals @t259 @t258 tptp.tc_nat)) % 3.02/3.23 (define @t261 () (not @t260)) % 3.02/3.23 (define @t262 () (tptp.c_lessequals @t258 @t259 tptp.tc_nat)) % 3.02/3.23 (define @t263 () (not @t262)) % 3.02/3.23 (define @t264 () (@list @t259 @t258)) % 3.02/3.23 (define @t265 () (@var "V_c" $$unsorted)) % 3.02/3.23 (define @t266 () (tptp.c_Natural_Oevalc @t265 @t119 @t128)) % 3.02/3.23 (define @t267 () (@var "V_u" $$unsorted)) % 3.02/3.23 (define @t268 () (not (tptp.class_Orderings_Oorder @t14))) % 3.02/3.23 (define @t269 () (= @t142 @t83)) % 3.02/3.23 (define @t270 () (= @t60 @t265)) % 3.02/3.23 (define @t271 () (@var "V_d" $$unsorted)) % 3.02/3.23 (define @t272 () (= @t60 @t271)) % 3.02/3.23 (define @t273 () (not (= @t224 (tptp.c_Set_Oinsert @t265 (tptp.c_Set_Oinsert @t271 @t59 @t14) @t14)))) % 3.02/3.23 (define @t274 () (@list @t60 @t62 @t14 @t265 @t271)) % 3.02/3.23 (define @t275 () (= @t62 @t265)) % 3.02/3.23 (define @t276 () (= @t62 @t271)) % 3.02/3.23 (define @t277 () (tptp.c_Natural_Oevalc @t129 @t119 @t128)) % 3.02/3.23 (define @t278 () (tptp.c_Com_Ocom_OAss @t5 @t4)) % 3.02/3.23 (define @t279 () (@list @t5 @t4)) % 3.02/3.23 (define @t280 () (tptp.hAPP @t38 @t60)) % 3.02/3.23 (define @t281 () (@var "V_fun1_H" $$unsorted)) % 3.02/3.23 (define @t282 () (@var "V_fun1" $$unsorted)) % 3.02/3.23 (define @t283 () (@var "V_fun2_H" $$unsorted)) % 3.02/3.23 (define @t284 () (@var "V_fun2" $$unsorted)) % 3.02/3.23 (define @t285 () (not (= (tptp.c_Hoare__Mirabelle_Otriple_Otriple @t282 @t17 @t284 @t14) (tptp.c_Hoare__Mirabelle_Otriple_Otriple @t281 @t198 @t283 @t14)))) % 3.02/3.23 (define @t286 () (@list @t282 @t17 @t284 @t14 @t281 @t198 @t283)) % 3.02/3.23 (define @t287 () (= @t17 @t198)) % 3.02/3.23 (define @t288 () (not (tptp.c_Com_OWT (tptp.c_Com_Ocom_OSemi @t124 @t129)))) % 3.02/3.23 (define @t289 () (tptp.c_Com_OWT @t129)) % 3.02/3.23 (define @t290 () (= @t84 @t90)) % 3.02/3.23 (define @t291 () (@list @t4 @t32 @t31)) % 3.02/3.23 (define @t292 () (tptp.c_Set_Oinsert @t60 @t190 @t14)) % 3.02/3.23 (define @t293 () (= @t60 @t62)) % 3.02/3.23 (define @t294 () (tptp.c_Lattices_Oupper__semilattice__class_Osup @t74 @t45 @t44)) % 3.02/3.23 (define @t295 () (tptp.c_Suc @t258)) % 3.02/3.23 (define @t296 () (tptp.c_lessequals @t295 @t259 tptp.tc_nat)) % 3.02/3.23 (define @t297 () (@list @t258 @t259)) % 3.02/3.23 (define @t298 () (tptp.c_Set_Oimage @t69 @t45 @t14 @t52)) % 3.02/3.23 (define @t299 () (tptp.hAPP @t69 @t39)) % 3.02/3.23 (define @t300 () (tptp.hAPP @t40 @t60)) % 3.02/3.23 (define @t301 () (tptp.hBOOL (tptp.hAPP @t300 @t45))) % 3.02/3.23 (define @t302 () (tptp.c_Lattices_Olower__semilattice__class_Oinf @t45 @t178 @t44)) % 3.02/3.23 (define @t303 () (tptp.hBOOL (tptp.hAPP @t300 @t74))) % 3.02/3.23 (define @t304 () (tptp.c_Lattices_Olower__semilattice__class_Oinf @t178 @t74 @t44)) % 3.02/3.23 (define @t305 () (not (= @t139 @t59))) % 3.02/3.23 (define @t306 () (not (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t45 @t38 @t14) @t184))) % 3.02/3.23 (define @t307 () (@list @t14 @t45 @t38)) % 3.02/3.23 (define @t308 () (tptp.c_Lattices_Oupper__semilattice__class_Osup @t38 @t45 @t44)) % 3.02/3.23 (define @t309 () (tptp.c_HOL_Ominus__class_Ominus @t38 @t45 @t44)) % 3.02/3.23 (define @t310 () (tptp.c_Lattices_Olower__semilattice__class_Oinf @t60 @t62 @t14)) % 3.02/3.23 (define @t311 () (tptp.c_lessequals @t39 @t310 @t14)) % 3.02/3.23 (define @t312 () (not @t311)) % 3.02/3.23 (define @t313 () (tptp.c_lessequals @t39 @t60 @t14)) % 3.02/3.23 (define @t314 () (@list @t14 @t39 @t60 @t62)) % 3.02/3.23 (define @t315 () (tptp.c_lessequals @t39 @t62 @t14)) % 3.02/3.23 (define @t316 () (tptp.c_lessequals @t310 @t39 @t14)) % 3.02/3.23 (define @t317 () (tptp.c_lessequals @t39 @t245 @t14)) % 3.02/3.23 (define @t318 () (not @t317)) % 3.02/3.23 (define @t319 () (@list @t14 @t39 @t81 @t83)) % 3.02/3.23 (define @t320 () (tptp.c_HOL_Ominus__class_Ominus @t38 @t74 @t44)) % 3.02/3.23 (define @t321 () (tptp.c_HOL_Ominus__class_Ominus @t45 @t74 @t44)) % 3.02/3.23 (define @t322 () (tptp.c_Lattices_Oupper__semilattice__class_Osup @t83 @t39 @t14)) % 3.02/3.23 (define @t323 () (= @t142 @t322)) % 3.02/3.23 (define @t324 () (@list @t258)) % 3.02/3.23 (define @t325 () (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t39 @t142 @t14) @t142)) % 3.02/3.23 (define @t326 () (tptp.c_Com_OWT @t265)) % 3.02/3.23 (define @t327 () (not @t326)) % 3.02/3.23 (define @t328 () (tptp.c_Com_OWT (tptp.c_Com_Ocom_OLocal @t13 @t60 @t265))) % 3.02/3.23 (define @t329 () (tptp.hAPP @t19 @t2)) % 3.02/3.23 (define @t330 () (@list @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t2 @t14)) % 3.02/3.23 (define @t331 () (tptp.c_Lattices_Oupper__semilattice__class_Osup @t45 @t38 @t100)) % 3.02/3.23 (define @t332 () (tptp.c_lessequals @t259 @t295 tptp.tc_nat)) % 3.02/3.23 (define @t333 () (@list @t1)) % 3.02/3.23 (define @t334 () (tptp.hBOOL (tptp.hAPP @t64 @t39))) % 3.02/3.23 (define @t335 () (not @t334)) % 3.02/3.23 (define @t336 () (tptp.hAPP (tptp.hAPP (tptp.hAPP @t21 @t7) @t55) @t54)) % 3.02/3.23 (define @t337 () (@list @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t7 @t55 @t54 @t14)) % 3.02/3.23 (define @t338 () (= @t128 @t119)) % 3.02/3.23 (define @t339 () (tptp.hAPP @t40 @t265)) % 3.02/3.23 (define @t340 () (tptp.hBOOL (tptp.hAPP @t339 @t45))) % 3.02/3.23 (define @t341 () (not @t340)) % 3.02/3.23 (define @t342 () (tptp.hBOOL (tptp.hAPP @t339 @t38))) % 3.02/3.23 (define @t343 () (not @t342)) % 3.02/3.23 (define @t344 () (tptp.hBOOL (tptp.hAPP @t339 @t64))) % 3.02/3.23 (define @t345 () (@list @t14 @t265 @t45 @t38)) % 3.02/3.23 (define @t346 () (@var "V_l" $$unsorted)) % 3.02/3.23 (define @t347 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t218 @t346) @t50))) % 3.02/3.23 (define @t348 () (not @t347)) % 3.02/3.23 (define @t349 () (tptp.hAPP @t217 @t50)) % 3.02/3.23 (define @t350 () (tptp.hBOOL (tptp.hAPP @t349 @t267))) % 3.02/3.23 (define @t351 () (tptp.hBOOL (tptp.hAPP @t51 (tptp.c_SetInterval_Oord_OatLeastLessThan @t218 @t217 @t346 @t267 @t14)))) % 3.02/3.23 (define @t352 () (not @t301)) % 3.02/3.23 (define @t353 () (tptp.hBOOL (tptp.hAPP @t300 (tptp.c_Set_Oinsert @t62 @t45 @t14)))) % 3.02/3.23 (define @t354 () (tptp.hAPP @t218 @t50)) % 3.02/3.23 (define @t355 () (tptp.hBOOL (tptp.hAPP @t354 @t267))) % 3.02/3.23 (define @t356 () (tptp.hBOOL (tptp.hAPP @t51 (tptp.c_SetInterval_Oord_OatLeastAtMost @t218 @t346 @t267 @t14)))) % 3.02/3.23 (define @t357 () (tptp.hBOOL (tptp.hAPP @t339 @t139))) % 3.02/3.23 (define @t358 () (not (tptp.hBOOL (tptp.hAPP @t41 @t59)))) % 3.02/3.23 (define @t359 () (tptp.hBOOL (tptp.hAPP @t106 @t39))) % 3.02/3.23 (define @t360 () (@list @t106 @t39 @t14)) % 3.02/3.23 (define @t361 () (@list @t14 @t265 @t38 @t45)) % 3.02/3.23 (define @t362 () (tptp.hBOOL (tptp.hAPP @t339 @t46))) % 3.02/3.23 (define @t363 () (not @t362)) % 3.02/3.23 (define @t364 () (not @t359)) % 3.02/3.23 (define @t365 () (tptp.c_ATP__Linkup_Osko__Set__XbexI__1__1 @t45 @t106 @t14)) % 3.02/3.23 (define @t366 () (@list @t106 @t45 @t14 @t39)) % 3.02/3.23 (define @t367 () (tptp.c_ATP__Linkup_Osko__Set__XbexE__1__1 @t45 @t106 @t14)) % 3.02/3.23 (define @t368 () (tptp.c_Set_Oinsert @t39 @t38 @t14)) % 3.02/3.23 (define @t369 () (tptp.c_ATP__Linkup_Osko__Complete__Lattice__Xball__conj__distrib__1__1 @t45 @t106 @t104 @t14)) % 3.02/3.23 (define @t370 () (not (tptp.hBOOL (tptp.hAPP @t106 @t369)))) % 3.02/3.23 (define @t371 () (not (tptp.hBOOL (tptp.hAPP @t104 @t369)))) % 3.02/3.23 (define @t372 () (@var "V_xf" $$unsorted)) % 3.02/3.23 (define @t373 () (@var "V_xg" $$unsorted)) % 3.02/3.23 (define @t374 () (tptp.c_ATP__Linkup_Osko__Set__XballE__1__1 @t45 @t106 @t14)) % 3.02/3.23 (define @t375 () (@list @t14 @t39 @t45 @t106)) % 3.02/3.23 (define @t376 () (not @t344)) % 3.02/3.23 (define @t377 () (@var "V_S" $$unsorted)) % 3.02/3.23 (define @t378 () (tptp.c_COMBC @t40 @t14 @t44 tptp.tc_bool)) % 3.02/3.23 (define @t379 () (tptp.hBOOL (tptp.hAPP @t354 @t211))) % 3.02/3.23 (define @t380 () (tptp.hBOOL (tptp.hAPP @t51 (tptp.c_SetInterval_Oord_OatMost @t218 @t211 @t14)))) % 3.02/3.23 (define @t381 () (tptp.hAPP @t40 @t110)) % 3.02/3.23 (define @t382 () (not (tptp.hBOOL (tptp.hAPP @t381 @t45)))) % 3.02/3.23 (define @t383 () (not (tptp.hBOOL (tptp.hAPP @t106 @t110)))) % 3.02/3.23 (define @t384 () (tptp.c_ATP__Linkup_Osko__Set__Xbex__Un__1__3 @t45 @t38 @t106 @t14)) % 3.02/3.23 (define @t385 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t40 @t384) @t139))) % 3.02/3.23 (define @t386 () (tptp.hAPP @t219 @t45)) % 3.02/3.23 (define @t387 () (tptp.hAPP @t220 @t45)) % 3.02/3.23 (define @t388 () (not (tptp.hBOOL (tptp.hAPP @t381 @t205)))) % 3.02/3.23 (define @t389 () (tptp.c_ATP__Linkup_Osko__Complete__Lattice__Xbex__UN__1__3 @t45 @t38 @t106 @t52 @t14)) % 3.02/3.23 (define @t390 () (tptp.c_Set_Oimage @t69 @t38 @t52 @t14)) % 3.02/3.23 (define @t391 () (tptp.c_Set_Oinsert @t60 @t38 @t52)) % 3.02/3.23 (define @t392 () (@list @t69 @t60 @t38 @t52 @t14)) % 3.02/3.23 (define @t393 () (tptp.c_lessequals @t84 @t39 @t14)) % 3.02/3.23 (define @t394 () (tptp.c_lessequals @t84 @t83 @t14)) % 3.02/3.23 (define @t395 () (not @t313)) % 3.02/3.23 (define @t396 () (not @t315)) % 3.02/3.23 (define @t397 () (@var "T_d" $$unsorted)) % 3.02/3.23 (define @t398 () (@var "V_h" $$unsorted)) % 3.02/3.23 (define @t399 () (not (= @t34 @t278))) % 3.02/3.23 (define @t400 () (@list @t8 @t7 @t5 @t4)) % 3.02/3.23 (define @t401 () (@list @t32 @t31)) % 3.02/3.23 (define @t402 () (tptp.c_Suc @t259)) % 3.02/3.23 (define @t403 () (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t39 @t84 @t14) @t84)) % 3.02/3.23 (define @t404 () (not (= @t29 @t200))) % 3.02/3.23 (define @t405 () (@list @t27 @t7 @t17 @t199 @t4 @t198)) % 3.02/3.23 (define @t406 () (@list @t5 @t1 @t4)) % 3.02/3.23 (define @t407 () (@var "V_r" $$unsorted)) % 3.02/3.23 (define @t408 () (not @t170)) % 3.02/3.23 (define @t409 () (tptp.c_lessequals @t39 @t159 @t14)) % 3.02/3.23 (define @t410 () (not @t160)) % 3.02/3.23 (define @t411 () (not (tptp.class_Orderings_Opreorder @t14))) % 3.02/3.23 (define @t412 () (@var "V_j" $$unsorted)) % 3.02/3.23 (define @t413 () (@list @t39)) % 3.02/3.23 (define @t414 () (tptp.c_lessequals @t39 @t39 @t14)) % 3.02/3.23 (define @t415 () (@var "T_e" $$unsorted)) % 3.02/3.23 (define @t416 () (@var "V_g_H" $$unsorted)) % 3.02/3.23 (define @t417 () (@var "V_f_H" $$unsorted)) % 3.02/3.23 (define @t418 () (tptp.hBOOL (tptp.hAPP @t182 @t39))) % 3.02/3.23 (define @t419 () (tptp.hBOOL (tptp.hAPP @t45 @t299))) % 3.02/3.23 (define @t420 () (tptp.c_lessequals @t114 @t115 @t14)) % 3.02/3.23 (define @t421 () (not (= (tptp.c_HOL_Ominus__class_Ominus @t39 @t83 @t14) @t116))) % 3.02/3.23 (define @t422 () (not (tptp.class_OrderedGroup_Opordered__ab__group__add @t14))) % 3.02/3.23 (define @t423 () (@list @t14 @t39 @t83 @t115 @t114)) % 3.02/3.23 (define @t424 () (tptp.c_lessequals @t295 @t402 tptp.tc_nat)) % 3.02/3.23 (define @t425 () (not (tptp.c_Com_OWT @t130))) % 3.02/3.23 (define @t426 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t40 @t369) @t45))) % 3.02/3.23 (define @t427 () (@var "V_xd" $$unsorted)) % 3.02/3.23 (define @t428 () (@var "V_xe" $$unsorted)) % 3.02/3.23 (define @t429 () (@list @t14 @t45 @t106 @t39)) % 3.02/3.23 (define @t430 () (tptp.hAPP @t203 @t62)) % 3.02/3.23 (define @t431 () (tptp.c_Complete__Lattice_Ocomplete__lattice__class_OSUPR @t45 @t38 @t14 @t100)) % 3.02/3.23 (define @t432 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t217 @t211) @t50))) % 3.02/3.23 (define @t433 () (tptp.hBOOL (tptp.hAPP @t51 (tptp.c_SetInterval_Oord_OgreaterThan @t217 @t211 @t14)))) % 3.02/3.23 (define @t434 () (@list @t14 @t50 @t217 @t211)) % 3.02/3.23 (define @t435 () (tptp.hAPP @t203 @t194)) % 3.02/3.23 (define @t436 () (tptp.hBOOL (tptp.hAPP @t435 @t38))) % 3.02/3.23 (define @t437 () (tptp.hBOOL (tptp.hAPP @t300 @t181))) % 3.02/3.23 (define @t438 () (tptp.hAPP @t40 @t194)) % 3.02/3.23 (define @t439 () (tptp.hAPP @t203 @t60)) % 3.02/3.23 (define @t440 () (not @t356)) % 3.02/3.23 (define @t441 () (tptp.hBOOL (tptp.hAPP @t106 @t384))) % 3.02/3.23 (define @t442 () (tptp.hBOOL (tptp.hAPP @t349 @t211))) % 3.02/3.23 (define @t443 () (tptp.hBOOL (tptp.hAPP @t51 (tptp.c_SetInterval_Oord_OlessThan @t217 @t211 @t14)))) % 3.02/3.23 (define @t444 () (tptp.hAPP @t205 @t62)) % 3.02/3.23 (define @t445 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.c_Complete__Lattice_Ocomplete__lattice__class_OSUPR @t45 @t38 @t14 (tptp.tc_fun @t52 (tptp.tc_fun @t107 tptp.tc_bool))) @t62) @t265))) % 3.02/3.23 (define @t446 () (tptp.hBOOL (tptp.hAPP @t431 @t62))) % 3.02/3.23 (define @t447 () (tptp.hAPP @t280 @t62)) % 3.02/3.23 (define @t448 () (not @t351)) % 3.02/3.23 (define @t449 () (tptp.c_ATP__Linkup_Osko__Set__Xrev__bexI__1__1 @t45 @t106 @t14)) % 3.02/3.23 (define @t450 () (tptp.hAPP @t40 @t299)) % 3.02/3.23 (define @t451 () (tptp.hBOOL (tptp.hAPP @t450 @t177))) % 3.02/3.23 (define @t452 () (tptp.tc_fun tptp.t_a tptp.tc_bool)) % 3.02/3.23 (define @t453 () (tptp.c_in tptp.t_a)) % 3.02/3.23 (define @t454 () (tptp.hAPP @t453 tptp.v_x)) % 3.02/3.23 (define @t455 () (tptp.c_COMBC @t453 tptp.t_a @t452 tptp.tc_bool)) % 3.02/3.23 (define @t456 () (tptp.hAPP @t455 @t377)) % 3.02/3.23 (define @t457 () (tptp.hAPP @t455 @t105)) % 3.02/3.23 (define @t458 () (@list @t105 @t377)) % 3.02/3.23 (define @t459 () (@list @t69 @t67 @t107 @t52)) % 3.02/3.23 (define @t460 () (tptp.c_Com_Ocom_OWhile @t7 @t17)) % 3.02/3.23 (define @t461 () (tptp.c_Com_Ocom_OWhile @t62 @t265)) % 3.02/3.23 (define @t462 () (tptp.c_Com_Ocom_OWhile @t4 @t198)) % 3.02/3.23 (define @t463 () (tptp.hAPP (tptp.hAPP @t20 @t7) @t17)) % 3.02/3.23 (define @t464 () (@list @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t7 @t17 @t14)) % 3.02/3.23 (define @t465 () (@list @t4 @t198)) % 3.02/3.23 (define @t466 () (not (tptp.hBOOL (tptp.hAPP @t62 @t133)))) % 3.02/3.23 (define @t467 () (tptp.c_Com_OWT @t461)) % 3.02/3.23 (define @t468 () (not (tptp.c_Natural_Oevaln @t130 @t119 @t258 @t128))) % 3.02/3.23 (define @t469 () (tptp.c_Natural_Oevaln @t124 @t119 @t258 @t128)) % 3.02/3.23 (define @t470 () (tptp.c_Natural_Oevaln @t129 @t119 @t258 @t128)) % 3.02/3.23 (define @t471 () (not (tptp.c_Natural_Oevaln @t265 @t119 @t258 @t128))) % 3.02/3.23 (define @t472 () (tptp.c_Natural_Oevaln @t125 @t119 @t258 @t122)) % 3.02/3.23 (define @t473 () (@list @t62 @t123 @t124 @t119 @t258 @t122)) % 3.02/3.23 (define @t474 () (@var "V_s_H" $$unsorted)) % 3.02/3.23 (define @t475 () (not (tptp.c_Natural_Oevaln @t265 @t119 @t258 @t474))) % 3.02/3.23 (define @t476 () (@var "V_t1" $$unsorted)) % 3.02/3.23 (define @t477 () (@var "V_n1" $$unsorted)) % 3.02/3.23 (define @t478 () (not (tptp.c_Natural_Oevaln @t124 @t122 @t477 @t476))) % 3.02/3.23 (define @t479 () (@var "V_t2" $$unsorted)) % 3.02/3.23 (define @t480 () (@var "V_n2" $$unsorted)) % 3.02/3.23 (define @t481 () (not (tptp.c_Natural_Oevaln @t129 @t134 @t480 @t479))) % 3.02/3.23 (define @t482 () (tptp.c_Natural_Osko__Natural__Xevaln__max2__1__1 @t124 @t129 @t122 @t134 @t476 @t479)) % 3.02/3.23 (define @t483 () (@var "V_ts" $$unsorted)) % 3.02/3.23 (define @t484 () (@var "V_G" $$unsorted)) % 3.02/3.23 (define @t485 () (tptp.c_Hoare__Mirabelle_Ohoare__valids @t484 @t483 tptp.t_a)) % 3.02/3.23 (define @t486 () (not @t485)) % 3.02/3.23 (define @t487 () (tptp.v_sko__Hoare__Mirabelle__Xhoare__valids__def__1 @t484 @t258)) % 3.02/3.23 (define @t488 () (tptp.c_in (tptp.tc_Hoare__Mirabelle_Otriple tptp.t_a))) % 3.02/3.23 (define @t489 () (@var "V_na" $$unsorted)) % 3.02/3.23 (define @t490 () (tptp.v_sko__Hoare__Mirabelle__Xtriples__valid__Suc__1 @t258 @t483)) % 3.02/3.23 (define @t491 () (tptp.hAPP @t488 @t39)) % 3.02/3.23 (define @t492 () (@var "V_nb" $$unsorted)) % 3.02/3.23 (define @t493 () (tptp.c_Orderings_Obot__class_Obot @t452)) % 3.02/3.23 (define @t494 () (not (tptp.c_Natural_Oevaln @t461 @t119 @t258 @t128))) % 3.02/3.23 (define @t495 () (tptp.c_Natural_Osko__Natural__Xevaln__WHILE__case__1__1 @t62 @t265 @t258 @t119 @t128)) % 3.02/3.23 (define @t496 () (tptp.c_Natural_Oevaln @t461 @t495 @t258 @t128)) % 3.02/3.23 (define @t497 () (@list @t62 @t265 @t258 @t119 @t128)) % 3.02/3.23 (define @t498 () (tptp.c_Natural_Oevaln @t265 @t119 @t258 @t495)) % 3.02/3.23 (define @t499 () (@list @t265 @t119 @t258 @t62 @t128)) % 3.02/3.23 (define @t500 () (@var "V_Z" $$unsorted)) % 3.02/3.23 (define @t501 () (tptp.hBOOL (tptp.hAPP @t377 @t39))) % 3.02/3.23 (define @t502 () (tptp.hBOOL (tptp.hAPP @t41 @t377))) % 3.02/3.23 (define @t503 () (not (= @t460 @t462))) % 3.02/3.23 (define @t504 () (@list @t7 @t17 @t4 @t198)) % 3.02/3.23 (define @t505 () (tptp.c_Com_Ocom_OWhile tptp.v_ba tptp.v_ca)) % 3.02/3.23 (define @t506 () (tptp.hAPP tptp.v_P tptp.v_xb)) % 3.02/3.23 (define @t507 () (tptp.hBOOL (tptp.hAPP @t506 tptp.v_s0))) % 3.02/3.23 (define @t508 () (tptp.hBOOL (tptp.hAPP @t506 tptp.v_s2))) % 3.02/3.23 (define @t509 () (tptp.hBOOL (tptp.hAPP tptp.v_b tptp.v_s2))) % 3.02/3.23 (define @t510 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t488 tptp.v_x) tptp.v_G))) % 3.02/3.23 (define @t511 () (tptp.hAPP tptp.v_P @t500)) % 3.02/3.23 (define @t512 () (not (tptp.hBOOL (tptp.hAPP @t511 tptp.v_s0)))) % 3.02/3.23 (define @t513 () (tptp.hBOOL (tptp.hAPP @t511 tptp.v_s1))) % 3.02/3.23 (define @t514 () (tptp.c_Com_Ocom_OWhile tptp.v_b tptp.v_c)) % 3.02/3.23 (define @t515 () (not (= tptp.v_ca @t514))) % 3.02/3.23 (define @t516 () (@list @t500)) % 3.02/3.23 (define @t517 () (not (tptp.hBOOL (tptp.hAPP tptp.v_b tptp.v_s1)))) % 3.02/3.23 (define @t518 () (not (tptp.c_Hoare__Mirabelle_Otriple__valid tptp.v_na tptp.v_x tptp.t_a))) % 3.02/3.23 (define @t519 () (@var "V_Za" $$unsorted)) % 3.02/3.23 (define @t520 () (tptp.hAPP tptp.v_P @t519)) % 3.02/3.23 (define @t521 () (not (tptp.hBOOL (tptp.hAPP @t520 tptp.v_s0)))) % 3.02/3.23 (define @t522 () (tptp.hBOOL (tptp.hAPP @t520 tptp.v_s1))) % 3.02/3.23 (define @t523 () (@list @t519)) % 3.02/3.23 (define @t524 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t488 tptp.v_xa) tptp.v_G))) % 3.02/3.23 (define @t525 () (not @t513)) % 3.02/3.23 (define @t526 () (tptp.hBOOL (tptp.hAPP @t511 tptp.v_s2))) % 3.02/3.23 (define @t527 () (= @t505 @t514)) % 3.02/3.23 (define @t528 () (not @t527)) % 3.02/3.23 (define @t529 () (or @t528 @t526 @t525 @t524)) % 3.02/3.23 (define @t530 () (forall @t516 @t529)) % 3.02/3.23 (define @t531 () (not @t509)) % 3.02/3.23 (define @t532 () (or @t528 @t531 @t525 @t524)) % 3.02/3.23 (define @t533 () (forall @t516 @t532)) % 3.02/3.23 (define @t534 () (tptp.c_Hoare__Mirabelle_Otriple__valid tptp.v_na tptp.v_xa tptp.t_a)) % 3.02/3.23 (define @t535 () (not @t534)) % 3.02/3.23 (define @t536 () (not @t522)) % 3.02/3.23 (define @t537 () (tptp.hBOOL (tptp.hAPP @t520 tptp.v_s2))) % 3.02/3.23 (define @t538 () (or @t528 @t537 @t536 @t535)) % 3.02/3.23 (define @t539 () (forall @t523 @t538)) % 3.02/3.23 (define @t540 () (or @t528 @t531 @t536 @t535)) % 3.02/3.23 (define @t541 () (forall @t523 @t540)) % 3.02/3.23 (define @t542 () (tptp.v_n @t489)) % 3.02/3.23 (define @t543 () (@var "V_sa" $$unsorted)) % 3.02/3.23 (define @t544 () (@var "V_s_Ha" $$unsorted)) % 3.02/3.23 (define @t545 () (@var "T_1" $$unsorted)) % 3.02/3.23 (define @t546 () (@var "T_2" $$unsorted)) % 3.02/3.23 (define @t547 () (tptp.tc_fun @t546 @t545)) % 3.02/3.23 (define @t548 () (@list @t546 @t545)) % 3.02/3.23 (define @t549 () (not (tptp.class_Lattices_Olattice @t545))) % 3.02/3.23 (define @t550 () (tptp.v_n tptp.v_na)) % 3.02/3.23 (define @t551 () (@list tptp.v_xb tptp.v_s1 tptp.v_s0 tptp.v_na)) % 3.02/3.23 (define @t552 () (tptp.hAPP tptp.v_b tptp.v_s0)) % 3.02/3.23 (define @t553 () (tptp.hBOOL @t552)) % 3.02/3.23 (define @t554 () (tptp.c_Natural_Oevaln tptp.v_c tptp.v_s0 tptp.v_na tptp.v_s1)) % 3.02/3.23 (define @t555 () (or @t526 @t525)) % 3.02/3.23 (define @t556 () (forall @t516 @t555)) % 3.02/3.23 (define @t557 () (@list @t500)) % 3.02/3.23 (define @t558 () (@list @t519)) % 3.02/3.23 (define @t559 () (or @t537 @t536)) % 3.02/3.23 (define @t560 () (forall @t523 @t559)) % 3.02/3.23 (define @t561 () (or @t528 @t535 @t559)) % 3.02/3.23 (define @t562 () (or @t528 @t524 @t555)) % 3.02/3.23 (define @t563 () (not @t524)) % 3.02/3.23 (define @t564 () (or @t534 @t563)) % 3.02/3.23 (define @t565 () (@list tptp.v_xb)) % 3.02/3.23 (define @t566 () (tptp.hBOOL (tptp.hAPP @t506 tptp.v_s1))) % 3.02/3.23 (define @t567 () (not @t566)) % 3.02/3.23 (define @t568 () (or @t508 @t567)) % 3.02/3.23 (define @t569 () (forall @t516 @t525)) % 3.02/3.23 (define @t570 () (or @t528 @t531 @t524 @t525)) % 3.02/3.23 (define @t571 () (forall @t523 @t536)) % 3.02/3.23 (define @t572 () (or @t528 @t531 @t535 @t536)) % 3.02/3.23 (define @t573 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t488 @t550) tptp.v_G))) % 3.02/3.23 (define @t574 () (not @t507)) % 3.02/3.23 (define @t575 () (not @t553)) % 3.02/3.23 (define @t576 () (not @t554)) % 3.02/3.23 (define @t577 () (or @t566 @t576 @t575 @t574 @t573)) % 3.02/3.23 (define @t578 () (@list false true false false false)) % 3.02/3.23 (define @t579 () (tptp.c_Hoare__Mirabelle_Otriple__valid tptp.v_na @t550 tptp.t_a)) % 3.02/3.23 (define @t580 () (not @t579)) % 3.02/3.23 (define @t581 () (or @t566 @t576 @t575 @t574 @t580)) % 3.02/3.23 (define @t582 () (not @t573)) % 3.02/3.23 (define @t583 () (or @t579 @t582)) % 3.02/3.23 (assume @p1 (forall @t11 (or @t10 @t3))) % 3.02/3.23 (assume @p2 (forall @t11 (or @t10 @t12))) % 3.02/3.23 (assume @p3 (forall @t16 (= (tptp.c_Set_Oimage @t15 @t13 @t14 @t14) @t13))) % 3.02/3.23 (assume @p4 (forall @t30 (= (tptp.c_Com_Ocom_Ocom__rec @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t29 @t14) (tptp.hAPP @t28 @t26)))) % 3.02/3.23 (assume @p5 (forall (@list @t8 @t7 @t32 @t31) (not (= @t34 @t33)))) % 3.02/3.23 (assume @p6 (forall @t35 (= (tptp.c_Com_Ocom_Ocom__rec @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 tptp.c_Com_Ocom_OSKIP @t14) @t25))) % 3.02/3.23 (assume @p7 (forall (@list @t5 @t1 @t4 @t2) (not (= @t6 @t36)))) % 3.02/3.23 (assume @p8 (forall (@list @t27 @t7 @t17 @t4 @t32 @t31) (not (= @t29 @t37)))) % 3.02/3.23 (assume @p9 (forall @t49 (or (= @t48 @t46) @t43))) % 3.02/3.23 (assume @p10 (forall (@list @t52 @t53 @t50 @t45 @t14) (or (not (tptp.class_Complete__Lattice_Ocomplete__lattice @t52)) (tptp.c_lessequals (tptp.hAPP @t53 @t50) (tptp.c_Complete__Lattice_Ocomplete__lattice__class_OSUPR @t45 @t53 @t14 @t52) @t52) (not (tptp.hBOOL (tptp.hAPP @t51 @t45)))))) % 3.02/3.23 (assume @p11 (forall (@list @t7 @t55 @t54 @t5 @t1 @t4) (not (= @t56 @t6)))) % 3.02/3.23 (assume @p12 (forall (@list @t1 @t55 @t54) (not (= @t58 @t57)))) % 3.02/3.23 (assume @p13 (forall (@list @t62 @t60 @t14) (or (= @t62 @t60) (not (tptp.hBOOL (tptp.hAPP @t63 @t61)))))) % 3.02/3.23 (assume @p14 (forall @t66 (or @t65 (= @t46 @t45)))) % 3.02/3.23 (assume @p15 (forall @t73 (or @t72 (= (tptp.hAPP (tptp.c_Lattices_Oupper__semilattice__class_Osup @t69 @t67 @t71) tptp.v_x) (tptp.c_Lattices_Oupper__semilattice__class_Osup @t70 @t68 @t52))))) % 3.02/3.23 (assume @p16 (forall @t78 (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t77 @t45 @t44) (tptp.c_Lattices_Oupper__semilattice__class_Osup @t76 @t75 @t44)))) % 3.02/3.23 (assume @p17 (forall @t80 (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t45 @t77 @t44) (tptp.c_Lattices_Oupper__semilattice__class_Osup @t64 @t79 @t44)))) % 3.02/3.23 (assume @p18 (forall @t89 (or @t88 (= @t87 @t85)))) % 3.02/3.23 (assume @p19 (forall @t91 (or @t88 (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t86 @t39 @t14) (tptp.c_Lattices_Oupper__semilattice__class_Osup @t90 (tptp.c_Lattices_Olower__semilattice__class_Oinf @t81 @t39 @t14) @t14))))) % 3.02/3.23 (assume @p20 (forall (@list @t69 @t14 @t52) (= (tptp.c_Fun_Ocomp @t69 @t92 @t14 @t52 @t14) @t69))) % 3.02/3.23 (assume @p21 (forall (@list @t52 @t67 @t14) (= (tptp.c_Fun_Ocomp @t93 @t67 @t52 @t52 @t14) @t67))) % 3.02/3.23 (assume @p22 (forall @t94 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t45 @t45 @t44) @t45))) % 3.02/3.23 (assume @p23 (forall @t96 (or @t95 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t39 @t39 @t14) @t39)))) % 3.02/3.23 (assume @p24 (forall (@list @t5 @t1 @t4 @t55 @t54) (not (= @t6 @t57)))) % 3.02/3.23 (assume @p25 (forall @t98 (= (tptp.c_Com_Ocom_Ocom__case @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t9 @t14) @t97))) % 3.02/3.23 (assume @p26 (forall (@list @t39 @t83 @t45 @t14) (= (tptp.c_Set_Oinsert @t39 @t99 @t14) (tptp.c_Set_Oinsert @t83 @t47 @t14)))) % 3.02/3.23 (assume @p27 (forall @t103 (= (tptp.c_HOL_Ominus__class_Ominus @t45 @t102 @t44) @t45))) % 3.02/3.23 (assume @p28 (forall (@list @t106 @t52 @t107 @t14 @t104 @t105) (= (tptp.hAPP (tptp.hAPP (tptp.c_COMBC @t106 @t52 @t107 @t14) @t104) @t105) (tptp.hAPP (tptp.hAPP @t106 @t105) @t104)))) % 3.02/3.23 (assume @p29 (forall (@list @t14 @t106) (= (tptp.hAPP @t15 @t106) @t106))) % 3.02/3.23 (assume @p30 (forall (@list @t55 @t54 @t1) (not (= @t57 @t58)))) % 3.02/3.23 (assume @p31 (forall @t66 (= (tptp.c_HOL_Ominus__class_Ominus @t46 @t38 @t44) @t46))) % 3.02/3.23 (assume @p32 (forall @t109 (= (tptp.c_Com_Ocom_Ocom__case @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t34 @t14) @t108))) % 3.02/3.23 (assume @p33 (forall (@list @t110 @t39 @t14) (= (tptp.c_Set_Oinsert @t110 @t111 @t14) (tptp.c_Set_Oinsert @t39 (tptp.c_Set_Oinsert @t110 @t59 @t14) @t14)))) % 3.02/3.23 (assume @p34 (forall (@list @t14 @t110 @t83 @t39) (or @t113 (not (= (tptp.c_HOL_Ominus__class_Ominus @t110 @t83 @t14) @t112)) (= @t110 @t83)))) % 3.02/3.23 (assume @p35 (forall (@list @t14 @t39 @t115 @t114) (or @t113 (not (= @t112 @t116)) (= @t115 @t114)))) % 3.02/3.23 (assume @p36 (tptp.c_Com_OWT tptp.c_Com_Ocom_OSKIP)) % 3.02/3.23 (assume @p37 (forall @t118 (= @t117 @t59))) % 3.02/3.23 (assume @p38 (forall @t127 (or @t126 (not (tptp.c_Natural_Oevalc @t123 @t119 @t122)) @t121))) % 3.02/3.23 (assume @p39 (forall (@list @t62 @t119 @t124 @t128 @t129) (or @t121 @t132 @t131))) % 3.02/3.23 (assume @p40 (forall (@list @t123 @t124 @t133 @t134 @t122) (or (tptp.c_Natural_Oevalc @t135 @t133 @t134) (not (tptp.c_Natural_Oevalc @t124 @t122 @t134)) (not (tptp.c_Natural_Oevalc @t123 @t133 @t122))))) % 3.02/3.23 (assume @p41 (forall (@list @t136 @t60) (tptp.c_Com_OWT (tptp.c_Com_Ocom_OAss @t136 @t60)))) % 3.02/3.23 (assume @p42 (forall @t80 (= @t138 (tptp.c_Lattices_Oupper__semilattice__class_Osup @t38 @t137 @t44)))) % 3.02/3.23 (assume @p43 (forall @t140 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t139 @t74 @t44) @t138))) % 3.02/3.23 (assume @p44 (forall @t89 (or @t95 @t143))) % 3.02/3.23 (assume @p45 (forall @t89 (or @t95 @t145))) % 3.02/3.23 (assume @p46 (forall @t89 (or @t146 @t145))) % 3.02/3.23 (assume @p47 (forall @t89 (or @t146 @t143))) % 3.02/3.23 (assume @p48 (forall @t151 (or @t150 @t149 @t148))) % 3.02/3.23 (assume @p49 (forall @t151 (or @t150 (not @t149) @t147))) % 3.02/3.23 (assume @p50 (forall @t151 (or @t150 (= @t84 @t83) @t153))) % 3.02/3.23 (assume @p51 (forall (@list @t136 @t154 @t60) (or (tptp.c_Com_OWT (tptp.c_Com_Ocom_OCall @t136 @t154 @t60)) (not (tptp.c_Com_OWT (tptp.c_Com_Ocom_OBODY @t154)))))) % 3.02/3.23 (assume @p52 (forall (@list @t106 @t136 @t60) (or (tptp.c_Com_OWT (tptp.c_Com_Ocom_OBODY @t106)) (not (tptp.c_Com_OWT (tptp.c_Com_Ocom_OCall @t136 @t106 @t60)))))) % 3.02/3.23 (assume @p53 (forall @t161 (or @t95 @t160 @t158 @t156))) % 3.02/3.23 (assume @p54 (forall @t151 (or @t95 @t162))) % 3.02/3.23 (assume @p55 (forall @t164 (or @t95 @t163))) % 3.02/3.23 (assume @p56 (forall @t91 (or @t95 (tptp.c_lessequals @t86 @t39 @t14) (not @t165) @t153))) % 3.02/3.23 (assume @p57 (forall @t89 (or @t95 @t170 @t169 @t167))) % 3.02/3.23 (assume @p58 (forall @t164 (or @t146 @t163))) % 3.02/3.23 (assume @p59 (forall @t11 (or @t10 @t171))) % 3.02/3.23 (assume @p60 (forall @t175 (= (tptp.c_Com_Ocom_Ocom__rec @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t57 @t14) (tptp.hAPP (tptp.hAPP @t174 @t173) @t172)))) % 3.02/3.23 (assume @p61 (forall (@list @t52) (or (not (tptp.class_Orderings_Obot @t52)) (= (tptp.hAPP (tptp.c_Orderings_Obot__class_Obot @t71) tptp.v_x) (tptp.c_Orderings_Obot__class_Obot @t52))))) % 3.02/3.23 (assume @p62 (forall (@list @t1 @t27 @t7 @t17) (not (= @t58 @t29)))) % 3.02/3.23 (assume @p63 (forall (@list @t14 @t69 @t45 @t52) (or (not (= @t59 @t177)) @t176))) % 3.02/3.23 (assume @p64 (forall @t179 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t178 @t74 @t44) (tptp.c_Set_Oinsert @t60 @t77 @t14)))) % 3.02/3.23 (assume @p65 (forall @t180 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t45 @t178 @t44) (tptp.c_Set_Oinsert @t60 @t139 @t14)))) % 3.02/3.23 (assume @p66 (forall @t183 (= (tptp.c_Set_Ovimage @t69 (tptp.c_HOL_Ominus__class_Ominus @t45 @t38 @t100) @t14 @t52) (tptp.c_HOL_Ominus__class_Ominus @t182 @t181 @t44)))) % 3.02/3.23 (assume @p67 (forall (@list @t8 @t7 @t1) (not (= @t34 @t58)))) % 3.02/3.23 (assume @p68 (forall @t96 (or (not (tptp.class_Orderings_Obot @t14)) (tptp.c_lessequals @t184 @t39 @t14)))) % 3.02/3.23 (assume @p69 (forall @t187 (or @t186 @t185))) % 3.02/3.23 (assume @p70 (forall @t187 (or @t186 @t188))) % 3.02/3.23 (assume @p71 (forall @t180 (= @t189 (tptp.c_HOL_Ominus__class_Ominus @t46 @t61 @t44)))) % 3.02/3.23 (assume @p72 (forall @t180 (= @t189 (tptp.c_HOL_Ominus__class_Ominus @t190 @t38 @t44)))) % 3.02/3.23 (assume @p73 (forall (@list @t55 @t54 @t4 @t32 @t31) (not (= @t57 @t37)))) % 3.02/3.23 (assume @p74 (forall @t192 (not (= @t191 @t59)))) % 3.02/3.23 (assume @p75 (forall (@list @t32 @t31 @t27 @t7 @t17) (not (= @t33 @t29)))) % 3.02/3.23 (assume @p76 (forall (@list @t193 @t60 @t69 @t14) (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t195 @t60) (tptp.c_Set_Ovimage @t69 (tptp.c_Set_Oinsert @t194 @t59 @t14) @t193 @t14))))) % 3.02/3.23 (assume @p77 (forall (@list @t60 @t45 @t14 @t38) (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t191 @t178 @t44) @t196))) % 3.02/3.23 (assume @p78 (forall @t197 (= (tptp.c_Set_Oinsert @t39 @t47 @t14) @t47))) % 3.02/3.23 (assume @p79 (forall (@list @t199 @t4 @t198 @t8 @t7) (not (= @t200 @t34)))) % 3.02/3.23 (assume @p80 (forall (@list @t45 @t39 @t83 @t14) (or @t202 (= @t83 @t39) (not @t201)))) % 3.02/3.23 (assume @p81 (forall (@list @t45 @t38 @t52 @t14 @t39) (or (not (= @t207 @t59)) @t206 @t204))) % 3.02/3.23 (assume @p82 (forall (@list @t1 @t8 @t7) (not (= @t58 @t34)))) % 3.02/3.23 (assume @p83 (forall (@list @t4 @t32 @t31 @t27 @t7 @t17) (not (= @t37 @t29)))) % 3.02/3.23 (assume @p84 (forall @t96 (or @t208 (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t39 @t184 @t14) @t184)))) % 3.02/3.23 (assume @p85 (forall @t96 (or @t208 (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t184 @t39 @t14) @t184)))) % 3.02/3.23 (assume @p86 (forall @t209 (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t59 @t38 @t44) @t59))) % 3.02/3.23 (assume @p87 (forall @t94 (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t45 @t59 @t44) @t59))) % 3.02/3.23 (assume @p88 (forall (@list @t4 @t32 @t31 @t55 @t54) (not (= @t37 @t57)))) % 3.02/3.23 (assume @p89 (forall (@list @t45 @t211 @t210 @t14 @t52) (or (= (tptp.c_Lattices_Oupper__semilattice__class_Osup (tptp.hAPP @t45 @t211) @t212 @t100) @t212) (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t40 @t211) @t210)))))) % 3.02/3.23 (assume @p90 (forall (@list @t219 @t60 @t62 @t14 @t215 @t220 @t218 @t217 @t216 @t214 @t213) (or (= (tptp.hAPP @t219 @t224) (tptp.hAPP @t222 @t62)) @t221))) % 3.02/3.23 (assume @p91 (forall (@list @t220 @t60 @t62 @t14 @t216 @t219 @t218 @t217 @t215 @t214 @t213) (or (= (tptp.hAPP @t220 @t224) (tptp.hAPP @t225 @t62)) @t221))) % 3.02/3.23 (assume @p92 (forall @t227 (or @t226 @t185))) % 3.02/3.23 (assume @p93 (forall @t227 (or @t226 @t188))) % 3.02/3.23 (assume @p94 (forall @t227 (or @t226 @t12))) % 3.02/3.23 (assume @p95 (forall (@list @t5 @t1 @t4 @t7 @t55 @t54) (not (= @t6 @t56)))) % 3.02/3.23 (assume @p96 (forall @t94 (= (tptp.c_HOL_Ominus__class_Ominus @t45 @t59 @t44) @t45))) % 3.02/3.23 (assume @p97 (forall @t94 (= (tptp.c_HOL_Ominus__class_Ominus @t45 @t45 @t44) @t59))) % 3.02/3.23 (assume @p98 (forall (@list @t69 @t67 @t52 @t14 @t107 @t39) (= @t229 @t228))) % 3.02/3.23 (assume @p99 (forall (@list @t60 @t62 @t230 @t107 @t52 @t14) (= @t232 (tptp.hAPP @t231 @t230)))) % 3.02/3.23 (assume @p100 (forall (@list @t39 @t83) (or (not (= (tptp.c_Suc @t39) (tptp.c_Suc @t83))) @t233))) % 3.02/3.23 (assume @p101 (forall (@list @t235 @t234) (or (not (= (tptp.c_Suc @t235) (tptp.c_Suc @t234))) (= @t235 @t234)))) % 3.02/3.23 (assume @p102 (forall (@list @t8 @t7 @t199 @t4 @t198) (not (= @t34 @t200)))) % 3.02/3.23 (assume @p103 (forall @t238 (or @t237 @t202 (not @t236)))) % 3.02/3.23 (assume @p104 (forall @t240 (or @t236 @t239))) % 3.02/3.23 (assume @p105 (forall @t240 (or @t236 @t241))) % 3.02/3.23 (assume @p106 (forall (@list @t62 @t123 @t124) (or (tptp.c_Com_OWT @t125) @t244 @t242))) % 3.02/3.23 (assume @p107 (forall @t35 (= (tptp.c_Com_Ocom_Ocom__case @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 tptp.c_Com_Ocom_OSKIP @t14) @t25))) % 3.02/3.23 (assume @p108 (forall @t16 (= (tptp.c_Set_Ovimage @t15 @t13 @t14 @t14) @t13))) % 3.02/3.23 (assume @p109 (forall (@list @t7 @t55 @t54 @t1) (not (= @t56 @t58)))) % 3.02/3.23 (assume @p110 (forall (@list @t1 @t7 @t55 @t54) (not (= @t58 @t56)))) % 3.02/3.23 (assume @p111 (forall @t89 (or @t146 @t247))) % 3.02/3.23 (assume @p112 (forall @t89 (or @t146 @t248))) % 3.02/3.23 (assume @p113 (forall @t89 (or @t150 @t248))) % 3.02/3.23 (assume @p114 (forall @t89 (or @t150 @t247))) % 3.02/3.23 (assume @p115 (forall @t140 (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t64 @t74 @t44) @t250))) % 3.02/3.23 (assume @p116 (forall @t80 (= @t250 (tptp.c_Lattices_Olower__semilattice__class_Oinf @t38 @t79 @t44)))) % 3.02/3.23 (assume @p117 (forall (@list @t14 @t45 @t38 @t52 @t39) (or (not (= @t59 @t207)) @t206 @t204))) % 3.02/3.23 (assume @p118 (forall @t96 (or @t208 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t39 @t184 @t14) @t39)))) % 3.02/3.23 (assume @p119 (forall @t96 (or @t208 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t184 @t39 @t14) @t39)))) % 3.02/3.23 (assume @p120 (forall @t209 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t59 @t38 @t44) @t38))) % 3.02/3.23 (assume @p121 (forall @t94 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t45 @t59 @t44) @t45))) % 3.02/3.23 (assume @p122 (forall @t251 (= (tptp.c_HOL_Ominus__class_Ominus @t59 @t45 @t44) @t59))) % 3.02/3.23 (assume @p123 (forall (@list @t52 @t45 @t14 @t38) (= (tptp.c_Lattices_Oupper__semilattice__class_Osup (tptp.c_Complete__Lattice_Ocomplete__lattice__class_OSUPR @t101 @t45 @t52 @t44) @t38 @t44) @t38))) % 3.02/3.23 (assume @p124 (forall @t103 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t45 @t102 @t44) @t45))) % 3.02/3.23 (assume @p125 (forall (@list @t8 @t7 @t4 @t32 @t31) (not (= @t34 @t37)))) % 3.02/3.23 (assume @p126 (forall @t96 (not (tptp.hBOOL (tptp.hAPP @t59 @t39))))) % 3.02/3.23 (assume @p127 (forall (@list @t74 @t45 @t38 @t14) (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t74 @t46 @t44) (tptp.c_HOL_Ominus__class_Ominus @t75 (tptp.c_Lattices_Olower__semilattice__class_Oinf @t74 @t38 @t44) @t44)))) % 3.02/3.23 (assume @p128 (forall @t140 (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t46 @t74 @t44) @t252))) % 3.02/3.23 (assume @p129 (forall @t253 (not (= tptp.c_Com_Ocom_OSKIP @t200)))) % 3.02/3.23 (assume @p130 (forall (@list @t14 @t39 @t38 @t45) (or @t43 @t255 @t65))) % 3.02/3.23 (assume @p131 (forall @t89 (or @t146 (tptp.c_lessequals @t257 @t256 @t14)))) % 3.02/3.23 (assume @p132 (forall (@list @t45 @t74 @t14 @t38) (= @t252 (tptp.c_HOL_Ominus__class_Ominus @t79 @t38 @t44)))) % 3.02/3.23 (assume @p133 (forall @t151 (or @t146 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t39 @t84 @t14) @t39)))) % 3.02/3.23 (assume @p134 (forall (@list @t119) (tptp.c_Natural_Oevalc tptp.c_Com_Ocom_OSKIP @t119 @t119))) % 3.02/3.23 (assume @p135 (forall (@list @t32 @t31 @t8 @t7) (not (= @t33 @t34)))) % 3.02/3.23 (assume @p136 (forall @t264 (or (= @t259 @t258) @t263 @t261))) % 3.02/3.23 (assume @p137 (forall (@list @t267 @t128 @t265 @t119) (or (= @t267 @t128) (not (tptp.c_Natural_Oevalc @t265 @t119 @t267)) (not @t266)))) % 3.02/3.23 (assume @p138 (forall @t151 (or @t268 @t233 @t153 @t148))) % 3.02/3.23 (assume @p139 (forall @t151 (or @t268 @t233 @t148 @t153))) % 3.02/3.23 (assume @p140 (forall @t253 (not (= @t200 tptp.c_Com_Ocom_OSKIP)))) % 3.02/3.23 (assume @p141 (forall @t151 (or @t146 (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t39 @t142 @t14) @t39)))) % 3.02/3.23 (assume @p142 (forall @t66 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t46 @t64 @t44) @t45))) % 3.02/3.23 (assume @p143 (forall @t151 (or @t95 (= @t142 @t39) @t153))) % 3.02/3.23 (assume @p144 (forall @t151 (or @t95 (not @t269) @t147))) % 3.02/3.23 (assume @p145 (forall @t151 (or @t95 @t269 @t148))) % 3.02/3.23 (assume @p146 (forall @t274 (or @t273 @t272 @t270))) % 3.02/3.23 (assume @p147 (forall @t274 (or @t273 @t275 @t270))) % 3.02/3.23 (assume @p148 (forall @t274 (or @t273 @t272 @t276))) % 3.02/3.23 (assume @p149 (forall @t274 (or @t273 @t275 @t276))) % 3.02/3.23 (assume @p150 (forall (@list @t129 @t119 @t128 @t62 @t124) (or @t277 @t120 @t131))) % 3.02/3.23 (assume @p151 (forall @t127 (or @t126 (not (tptp.c_Natural_Oevalc @t124 @t119 @t122)) @t120))) % 3.02/3.23 (assume @p152 (forall @t279 (not (= tptp.c_Com_Ocom_OSKIP @t278)))) % 3.02/3.23 (assume @p153 (forall (@list @t60 @t45 @t52 @t38 @t14) (= (tptp.c_Complete__Lattice_Ocomplete__lattice__class_OSUPR (tptp.c_Set_Oinsert @t60 @t45 @t52) @t38 @t52 @t44) (tptp.c_Lattices_Oupper__semilattice__class_Osup @t280 @t207 @t44)))) % 3.02/3.23 (assume @p154 (forall @t286 (or @t285 (= @t282 @t281)))) % 3.02/3.23 (assume @p155 (forall @t286 (or @t285 @t287))) % 3.02/3.23 (assume @p156 (forall @t286 (or @t285 (= @t284 @t283)))) % 3.02/3.23 (assume @p157 (forall (@list @t129 @t124) (or @t289 @t288))) % 3.02/3.23 (assume @p158 (forall @t151 (or @t146 @t162))) % 3.02/3.23 (assume @p159 (forall @t66 (= @t64 @t76))) % 3.02/3.23 (assume @p160 (forall @t151 (or @t150 @t290))) % 3.02/3.23 (assume @p161 (forall @t151 (or @t146 @t290))) % 3.02/3.23 (assume @p162 (forall (@list @t219 @t220 @t218 @t14 @t217 @t215 @t216 @t213 @t214) (or (tptp.c_Complete__Lattice_Ocomplete__lattice @t219 @t220 (tptp.c_COMBC @t218 @t14 @t14 tptp.tc_bool) (tptp.c_COMBC @t217 @t14 @t14 tptp.tc_bool) @t215 @t216 @t213 @t214 @t14) @t221))) % 3.02/3.23 (assume @p163 (forall @t291 (not (= tptp.c_Com_Ocom_OSKIP @t37)))) % 3.02/3.23 (assume @p164 (forall @t89 (or @t146 (tptp.c_lessequals @t85 @t87 @t14)))) % 3.02/3.23 (assume @p165 (forall (@list @t8 @t7 @t5 @t1 @t4) (not (= @t34 @t6)))) % 3.02/3.23 (assume @p166 (forall @t192 (= @t292 @t191))) % 3.02/3.23 (assume @p167 (forall (@list @t60 @t14 @t62) (or (not (= @t61 @t223)) @t293))) % 3.02/3.23 (assume @p168 (forall @t140 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup (tptp.c_Lattices_Oupper__semilattice__class_Osup @t64 @t249 @t44) @t75 @t44) (tptp.c_Lattices_Olower__semilattice__class_Oinf (tptp.c_Lattices_Olower__semilattice__class_Oinf @t139 @t77 @t44) @t294 @t44)))) % 3.02/3.23 (assume @p169 (forall (@list @t39 @t110 @t14) (or (not (= (tptp.c_Set_Oinsert @t39 @t110 @t14) @t59)) (tptp.hBOOL (tptp.hAPP @t41 @t110))))) % 3.02/3.23 (assume @p170 (forall (@list @t27 @t7 @t17 @t1) (not (= @t29 @t58)))) % 3.02/3.23 (assume @p171 (forall (@list @t2 @t5 @t1 @t4) (not (= @t36 @t6)))) % 3.02/3.23 (assume @p172 (forall (@list @t5 @t1 @t4 @t27 @t7 @t17) (not (= @t6 @t29)))) % 3.02/3.23 (assume @p173 (forall @t264 (or @t261 (not @t296)))) % 3.02/3.23 (assume @p174 (forall @t297 (or @t296 @t260))) % 3.02/3.23 (assume @p175 (forall (@list @t83 @t45 @t14 @t39) (or @t201 @t241))) % 3.02/3.23 (assume @p176 (forall (@list @t69 @t39 @t45 @t14 @t52) (or (= (tptp.c_Set_Oinsert @t299 @t298 @t52) @t298) @t255))) % 3.02/3.23 (assume @p177 (forall @t180 (or (= @t302 @t64) @t301))) % 3.02/3.23 (assume @p178 (forall @t179 (or (= @t304 @t249) @t303))) % 3.02/3.23 (assume @p179 (forall @t66 (or @t305 (= @t38 @t59)))) % 3.02/3.23 (assume @p180 (forall @t66 (or @t305 (= @t45 @t59)))) % 3.02/3.23 (assume @p181 (forall @t307 (or @t208 @t306 (= @t45 @t184)))) % 3.02/3.23 (assume @p182 (forall @t307 (or @t208 @t306 (= @t38 @t184)))) % 3.02/3.23 (assume @p183 (forall (@list @t60 @t62 @t107 @t52 @t14 @t265 @t230) (or (not (= @t231 (tptp.c_Fun_Ocomp @t93 @t265 @t52 @t52 @t14))) (= @t232 (tptp.hAPP @t265 @t230))))) % 3.02/3.23 (assume @p184 (forall (@list @t38 @t45 @t14) (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t309 @t45 @t44) @t308))) % 3.02/3.23 (assume @p185 (forall @t66 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t45 @t309 @t44) @t139))) % 3.02/3.23 (assume @p186 (forall (@list @t52 @t45 @t38) (or (not (tptp.class_HOL_Ominus @t52)) (= (tptp.hAPP (tptp.c_HOL_Ominus__class_Ominus @t45 @t38 @t71) tptp.v_x) (tptp.c_HOL_Ominus__class_Ominus (tptp.hAPP @t45 tptp.v_x) (tptp.hAPP @t38 tptp.v_x) @t52))))) % 3.02/3.23 (assume @p187 (forall @t314 (or @t150 @t313 @t312))) % 3.02/3.23 (assume @p188 (forall (@list @t14 @t39 @t62 @t60) (or @t150 @t315 @t312))) % 3.02/3.23 (assume @p189 (forall @t161 (or @t150 @t316 @t156))) % 3.02/3.23 (assume @p190 (forall @t161 (or @t150 @t316 @t158))) % 3.02/3.23 (assume @p191 (forall @t89 (or @t150 @t147 @t318))) % 3.02/3.23 (assume @p192 (forall @t319 (or @t150 @t166 @t318))) % 3.02/3.23 (assume @p193 (forall @t251 (= (tptp.c_Set_Ovimage @t92 @t45 @t14 @t14) @t45))) % 3.02/3.23 (assume @p194 (forall @t140 (= (tptp.c_HOL_Ominus__class_Ominus @t139 @t74 @t44) (tptp.c_Lattices_Oupper__semilattice__class_Osup @t321 @t320 @t44)))) % 3.02/3.23 (assume @p195 (forall @t175 (= (tptp.c_Com_Ocom_Ocom__case @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t57 @t14) @t174))) % 3.02/3.23 (assume @p196 (forall (@list @t27 @t7 @t17 @t32 @t31) (not (= @t29 @t33)))) % 3.02/3.23 (assume @p197 (forall (@list @t67 @t69 @t107 @t52 @t14 @t39) (= (tptp.c_Set_Ovimage (tptp.c_Fun_Ocomp @t67 @t69 @t107 @t52 @t14) @t39 @t14 @t52) (tptp.c_Set_Ovimage @t69 (tptp.c_Set_Ovimage @t67 @t39 @t107 @t52) @t14 @t107)))) % 3.02/3.23 (assume @p198 (forall @t66 (= @t139 @t308))) % 3.02/3.23 (assume @p199 (forall @t151 (or @t95 @t323))) % 3.02/3.23 (assume @p200 (forall @t151 (or @t146 @t323))) % 3.02/3.23 (assume @p201 (forall @t16 (= (tptp.c_Set_Oimage @t92 @t13 @t14 @t14) @t13))) % 3.02/3.23 (assume @p202 (forall (@list @t2 @t1) (or (not (= @t36 @t58)) @t3))) % 3.02/3.23 (assume @p203 (forall @t98 (= (tptp.c_Com_Ocom_Ocom__rec @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t9 @t14) @t97))) % 3.02/3.23 (assume @p204 (forall @t192 (= @t191 (tptp.c_Lattices_Oupper__semilattice__class_Osup @t61 @t45 @t44)))) % 3.02/3.23 (assume @p205 (forall @t324 (tptp.c_lessequals @t295 @t295 tptp.tc_nat))) % 3.02/3.23 (assume @p206 (forall @t66 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t45 @t139 @t44) @t139))) % 3.02/3.23 (assume @p207 (forall @t151 (or @t95 @t325))) % 3.02/3.23 (assume @p208 (forall @t151 (or @t146 @t325))) % 3.02/3.23 (assume @p209 (forall (@list @t14 @t69 @t52) (= @t59 @t117))) % 3.02/3.23 (assume @p210 (forall (@list @t13 @t60 @t265) (or @t328 @t327))) % 3.02/3.23 (assume @p211 (forall (@list @t265 @t13 @t60) (or @t326 (not @t328)))) % 3.02/3.23 (assume @p212 (forall @t291 (not (= @t37 tptp.c_Com_Ocom_OSKIP)))) % 3.02/3.23 (assume @p213 (forall @t66 (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t45 @t309 @t44) @t59))) % 3.02/3.23 (assume @p214 (forall @t330 (= (tptp.c_Com_Ocom_Ocom__case @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t36 @t14) @t329))) % 3.02/3.23 (assume @p215 (forall @t183 (= (tptp.c_Set_Ovimage @t69 @t331 @t14 @t52) (tptp.c_Lattices_Oupper__semilattice__class_Osup @t182 @t181 @t44)))) % 3.02/3.23 (assume @p216 (forall (@list @t55 @t54 @t5 @t1 @t4) (not (= @t57 @t6)))) % 3.02/3.23 (assume @p217 (forall @t264 (or (= @t259 @t295) @t260 (not @t332)))) % 3.02/3.23 (assume @p218 (forall @t109 (= (tptp.c_Com_Ocom_Ocom__rec @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t34 @t14) @t108))) % 3.02/3.23 (assume @p219 (forall (@list @t4 @t32 @t31 @t8 @t7) (not (= @t37 @t34)))) % 3.02/3.23 (assume @p220 (forall @t333 (not (= tptp.c_Com_Ocom_OSKIP @t58)))) % 3.02/3.23 (assume @p221 (forall @t49 (or (= @t48 (tptp.c_Set_Oinsert @t39 @t46 @t14)) @t42))) % 3.02/3.23 (assume @p222 (forall @t238 (or @t237 @t335))) % 3.02/3.23 (assume @p223 (forall (@list @t45 @t39 @t38 @t14) (or @t202 @t335))) % 3.02/3.23 (assume @p224 (forall @t197 (or (= (tptp.c_HOL_Ominus__class_Ominus @t47 @t111 @t44) @t45) @t254))) % 3.02/3.23 (assume @p225 (forall @t96 (= (tptp.hAPP @t92 @t39) @t39))) % 3.02/3.23 (assume @p226 (forall @t337 (= (tptp.c_Com_Ocom_Ocom__rec @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t56 @t14) (tptp.hAPP (tptp.hAPP @t336 @t173) @t172)))) % 3.02/3.23 (assume @p227 (forall @t183 (= (tptp.c_Set_Ovimage @t69 (tptp.c_Lattices_Olower__semilattice__class_Oinf @t45 @t38 @t100) @t14 @t52) (tptp.c_Lattices_Olower__semilattice__class_Oinf @t182 @t181 @t44)))) % 3.02/3.23 (assume @p228 (forall (@list @t128 @t119) (or @t338 (not (tptp.c_Natural_Oevalc tptp.c_Com_Ocom_OSKIP @t119 @t128))))) % 3.02/3.23 (assume @p229 (forall @t345 (or @t344 @t343 @t341))) % 3.02/3.23 (assume @p230 (forall (@list @t14 @t50 @t218 @t217 @t346 @t267) (or @t351 (not @t350) @t348))) % 3.02/3.23 (assume @p231 (forall (@list @t14 @t60 @t62 @t45) (or @t353 @t352))) % 3.02/3.23 (assume @p232 (forall (@list @t14 @t60 @t62 @t38) (or (tptp.hBOOL (tptp.hAPP @t300 (tptp.c_Set_Oinsert @t62 @t38 @t14))) (not (tptp.hBOOL (tptp.hAPP @t300 @t38)))))) % 3.02/3.23 (assume @p233 (forall (@list @t14 @t50 @t218 @t346 @t267) (or @t356 (not @t355) @t348))) % 3.02/3.23 (assume @p234 (forall @t345 (or @t357 @t341))) % 3.02/3.23 (assume @p235 (forall @t345 (or @t357 @t343))) % 3.02/3.23 (assume @p236 (forall @t96 @t358)) % 3.02/3.23 (assume @p237 (forall @t360 (or @t359 @t358))) % 3.02/3.23 (assume @p238 (forall (@list @t14 @t265) (not (tptp.hBOOL (tptp.hAPP @t339 @t59))))) % 3.02/3.23 (assume @p239 (forall (@list @t14 @t60) (not (tptp.hBOOL (tptp.hAPP @t300 @t59))))) % 3.02/3.23 (assume @p240 (forall (@list @t14 @t60 @t45 @t62) (or @t301 @t293 (not @t353)))) % 3.02/3.23 (assume @p241 (forall @t361 (or @t342 @t340 (not @t357)))) % 3.02/3.23 (assume @p242 (forall @t361 (or @t343 @t363))) % 3.02/3.23 (assume @p243 (forall @t345 (or @t340 @t363))) % 3.02/3.23 (assume @p244 (forall @t366 (or (tptp.hBOOL (tptp.hAPP @t106 @t365)) @t255 @t364))) % 3.02/3.23 (assume @p245 (forall @t366 (or (tptp.hBOOL (tptp.hAPP @t106 @t367)) @t364 @t255))) % 3.02/3.23 (assume @p246 (forall (@list @t14 @t39 @t45) (tptp.hBOOL (tptp.hAPP @t41 @t47)))) % 3.02/3.23 (assume @p247 (forall (@list @t14 @t60 @t38) (tptp.hBOOL (tptp.hAPP @t300 @t178)))) % 3.02/3.23 (assume @p248 (forall (@list @t14 @t39 @t38) (tptp.hBOOL (tptp.hAPP @t41 @t368)))) % 3.02/3.23 (assume @p249 (forall (@list @t104 @t372 @t14 @t45 @t106) (or (tptp.hBOOL (tptp.hAPP @t104 @t372)) (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t40 @t372) @t45))) @t371 @t370))) % 3.02/3.23 (assume @p250 (forall (@list @t106 @t373 @t14 @t45 @t104) (or (tptp.hBOOL (tptp.hAPP @t106 @t373)) (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t40 @t373) @t45))) @t371 @t370))) % 3.02/3.23 (assume @p251 (forall @t375 (or @t255 @t359 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t40 @t374) @t45))))) % 3.02/3.23 (assume @p252 (forall @t361 (or @t342 @t376))) % 3.02/3.23 (assume @p253 (forall @t345 (or @t340 @t376))) % 3.02/3.23 (assume @p254 (forall @t360 (or @t364 @t358))) % 3.02/3.23 (assume @p255 (forall (@list @t14 @t105 @t377) (or (not (= (tptp.hAPP @t378 @t105) (tptp.hAPP @t378 @t377))) (= @t105 @t377)))) % 3.02/3.23 (assume @p256 (forall (@list @t14 @t50 @t218 @t211) (or @t380 (not @t379)))) % 3.02/3.23 (assume @p257 (forall (@list @t124 @t129) (or @t243 @t288))) % 3.02/3.23 (assume @p258 (forall (@list @t14 @t45 @t38 @t106 @t110) (or @t385 @t383 @t382))) % 3.02/3.23 (assume @p259 (forall (@list @t14 @t45 @t38 @t106 @t39) (or @t385 @t364 @t43))) % 3.02/3.23 (assume @p260 (forall (@list @t219 @t60 @t45 @t14 @t215 @t220 @t218 @t217 @t216 @t214 @t213) (or (= (tptp.hAPP @t219 @t191) (tptp.hAPP @t222 @t386)) @t221))) % 3.02/3.23 (assume @p261 (forall (@list @t220 @t60 @t45 @t14 @t216 @t219 @t218 @t217 @t215 @t214 @t213) (or (= (tptp.hAPP @t220 @t191) (tptp.hAPP @t225 @t387)) @t221))) % 3.02/3.23 (assume @p262 (forall (@list @t14 @t45 @t38 @t106 @t52 @t110 @t39) (or (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t40 @t389) @t207)) @t383 @t388 @t204))) % 3.02/3.23 (assume @p263 (forall (@list @t14 @t60 @t45) (not (= @t59 @t191)))) % 3.02/3.23 (assume @p264 (forall @t30 (= (tptp.c_Com_Ocom_Ocom__case @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t29 @t14) @t28))) % 3.02/3.23 (assume @p265 (forall @t179 (or (= @t304 (tptp.c_Set_Oinsert @t60 @t249 @t14)) (not @t303)))) % 3.02/3.23 (assume @p266 (forall @t180 (or (= @t302 @t196) @t352))) % 3.02/3.23 (assume @p267 (forall @t392 (= (tptp.c_Set_Oimage @t69 @t391 @t52 @t14) (tptp.c_Set_Oinsert @t194 @t390 @t14)))) % 3.02/3.23 (assume @p268 (forall (@list @t69 @t67 @t52 @t107 @t14 @t39) (= (tptp.hAPP (tptp.c_Fun_Ofcomp @t69 @t67 @t52 @t107 @t14) @t39) (tptp.hAPP @t67 @t299)))) % 3.02/3.23 (assume @p269 (forall (@list @t69 @t60 @t62 @t14 @t52) (or (= @t194 @t62) (not (tptp.hBOOL (tptp.hAPP @t300 (tptp.c_Set_Ovimage @t69 (tptp.c_Set_Oinsert @t62 @t101 @t52) @t14 @t52))))))) % 3.02/3.23 (assume @p270 (forall @t151 (or @t146 @t393))) % 3.02/3.23 (assume @p271 (forall @t151 (or @t146 @t394))) % 3.02/3.23 (assume @p272 (forall @t89 (or @t150 @t317 @t167 @t148))) % 3.02/3.23 (assume @p273 (forall @t314 (or @t150 @t311 @t396 @t395))) % 3.02/3.23 (assume @p274 (forall @t151 (or @t150 @t394))) % 3.02/3.23 (assume @p275 (forall @t151 (or @t150 @t393))) % 3.02/3.23 (assume @p276 (forall (@list @t69 @t67 @t398 @t397 @t107 @t14 @t52) (= (tptp.c_Fun_Ocomp @t69 (tptp.c_Fun_Ocomp @t67 @t398 @t397 @t107 @t14) @t107 @t52 @t14) (tptp.c_Fun_Ocomp (tptp.c_Fun_Ocomp @t69 @t67 @t107 @t52 @t397) @t398 @t397 @t52 @t14)))) % 3.02/3.23 (assume @p277 (forall @t400 (or @t399 @t12))) % 3.02/3.23 (assume @p278 (forall @t400 (or @t399 @t171))) % 3.02/3.23 (assume @p279 (forall (@list @t5 @t1 @t4 @t8 @t7) (not (= @t6 @t34)))) % 3.02/3.23 (assume @p280 (forall (@list @t60 @t52 @t38 @t14) (= (tptp.c_Set_Oinsert @t60 @t102 @t14) @t61))) % 3.02/3.23 (assume @p281 (forall @t401 (not (= @t33 tptp.c_Com_Ocom_OSKIP)))) % 3.02/3.23 (assume @p282 (forall @t264 (or @t260 (not (tptp.c_lessequals @t402 @t258 tptp.tc_nat))))) % 3.02/3.23 (assume @p283 (forall @t264 (or @t332 @t261))) % 3.02/3.23 (assume @p284 (forall @t91 (or @t88 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t245 @t39 @t14) (tptp.c_Lattices_Olower__semilattice__class_Oinf @t322 (tptp.c_Lattices_Oupper__semilattice__class_Osup @t81 @t39 @t14) @t14))))) % 3.02/3.23 (assume @p285 (forall @t89 (or @t88 (= @t257 @t256)))) % 3.02/3.23 (assume @p286 (forall @t80 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t45 @t249 @t44) (tptp.c_Lattices_Olower__semilattice__class_Oinf @t139 @t137 @t44)))) % 3.02/3.23 (assume @p287 (forall @t78 (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t249 @t45 @t44) (tptp.c_Lattices_Olower__semilattice__class_Oinf @t308 @t294 @t44)))) % 3.02/3.23 (assume @p288 (forall @t197 (tptp.hBOOL (tptp.hAPP @t47 @t39)))) % 3.02/3.23 (assume @p289 (forall @t324 (not (tptp.c_lessequals @t295 @t258 tptp.tc_nat)))) % 3.02/3.23 (assume @p290 (forall @t151 (or @t146 @t403))) % 3.02/3.23 (assume @p291 (forall @t151 (or @t150 @t403))) % 3.02/3.23 (assume @p292 (forall @t66 (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t45 @t64 @t44) @t64))) % 3.02/3.23 (assume @p293 (forall @t405 (or @t404 @t287))) % 3.02/3.23 (assume @p294 (forall @t405 (or @t404 @t12))) % 3.02/3.23 (assume @p295 (forall @t405 (or @t404 (= @t27 @t199)))) % 3.02/3.23 (assume @p296 (forall (@list @t123 @t124) (or (tptp.c_Com_OWT @t135) @t244 @t242))) % 3.02/3.23 (assume @p297 (forall @t406 (not (= tptp.c_Com_Ocom_OSKIP @t6)))) % 3.02/3.23 (assume @p298 (forall @t118 (= (tptp.c_Fun_Ofcomp @t69 @t93 @t14 @t52 @t52) @t69))) % 3.02/3.23 (assume @p299 (forall (@list @t14 @t67 @t52) (= (tptp.c_Fun_Ofcomp @t92 @t67 @t14 @t14 @t52) @t67))) % 3.02/3.23 (assume @p300 (forall (@list @t69 @t67 @t107 @t14 @t52 @t407) (= (tptp.c_Set_Oimage (tptp.c_Fun_Ocomp @t69 @t67 @t107 @t14 @t52) @t407 @t52 @t14) (tptp.c_Set_Oimage @t69 (tptp.c_Set_Oimage @t67 @t407 @t52 @t107) @t107 @t14)))) % 3.02/3.23 (assume @p301 (forall (@list @t219 @t14 @t214 @t220 @t218 @t217 @t216 @t215 @t213) (or (= (tptp.hAPP @t219 @t59) @t214) @t221))) % 3.02/3.23 (assume @p302 (forall (@list @t220 @t14 @t213 @t219 @t218 @t217 @t216 @t215 @t214) (or (= (tptp.hAPP @t220 @t59) @t213) @t221))) % 3.02/3.23 (assume @p303 (forall @t324 (not (= @t295 @t258)))) % 3.02/3.23 (assume @p304 (forall @t324 (not (= @t258 @t295)))) % 3.02/3.23 (assume @p305 (forall @t192 (or (= @t292 @t45) @t352))) % 3.02/3.23 (assume @p306 (forall @t96 (or @t150 (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t39 @t39 @t14) @t39)))) % 3.02/3.23 (assume @p307 (forall @t94 (= (tptp.c_Lattices_Olower__semilattice__class_Oinf @t45 @t45 @t44) @t45))) % 3.02/3.23 (assume @p308 (forall @t91 (or @t95 @t168 @t408))) % 3.02/3.23 (assume @p309 (forall @t319 (or @t95 @t166 @t408))) % 3.02/3.23 (assume @p310 (forall @t314 (or @t95 @t409 @t396))) % 3.02/3.23 (assume @p311 (forall @t314 (or @t95 @t409 @t395))) % 3.02/3.23 (assume @p312 (forall (@list @t14 @t62 @t39 @t60) (or @t95 @t157 @t410))) % 3.02/3.23 (assume @p313 (forall (@list @t14 @t60 @t39 @t62) (or @t95 @t155 @t410))) % 3.02/3.23 (assume @p314 (forall @t73 (or @t72 (= (tptp.hAPP (tptp.c_Lattices_Olower__semilattice__class_Oinf @t69 @t67 @t71) tptp.v_x) (tptp.c_Lattices_Olower__semilattice__class_Oinf @t70 @t68 @t52))))) % 3.02/3.23 (assume @p315 (forall (@list @t14 @t81 @t39 @t83) (or @t268 @t165 (not (tptp.c_lessequals @t81 @t83 @t14)) @t153))) % 3.02/3.23 (assume @p316 (forall @t319 (or @t411 @t166 @t169 @t148))) % 3.02/3.23 (assume @p317 (forall @t324 (tptp.c_lessequals @t258 @t258 tptp.tc_nat))) % 3.02/3.23 (assume @p318 (forall (@list @t50 @t211 @t412) (or (tptp.c_lessequals @t50 @t211 tptp.tc_nat) (not (tptp.c_lessequals @t412 @t211 tptp.tc_nat)) (not (tptp.c_lessequals @t50 @t412 tptp.tc_nat))))) % 3.02/3.23 (assume @p319 (forall @t413 (tptp.c_lessequals @t39 @t39 tptp.tc_nat))) % 3.02/3.23 (assume @p320 (forall @t96 (or @t268 @t414))) % 3.02/3.23 (assume @p321 (forall @t96 (or @t411 @t414))) % 3.02/3.23 (assume @p322 (forall @t406 (not (= @t6 tptp.c_Com_Ocom_OSKIP)))) % 3.02/3.23 (assume @p323 (forall (@list @t69 @t45 @t52 @t14) (or (not (= @t177 @t59)) @t176))) % 3.02/3.23 (assume @p324 (forall @t330 (= (tptp.c_Com_Ocom_Ocom__rec @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t36 @t14) @t329))) % 3.02/3.23 (assume @p325 (forall @t80 (= (tptp.c_HOL_Ominus__class_Ominus @t45 @t77 @t44) (tptp.c_Lattices_Olower__semilattice__class_Oinf @t46 @t321 @t44)))) % 3.02/3.23 (assume @p326 (forall @t140 (= (tptp.c_HOL_Ominus__class_Ominus @t64 @t74 @t44) (tptp.c_Lattices_Olower__semilattice__class_Oinf @t45 @t320 @t44)))) % 3.02/3.23 (assume @p327 (forall (@list @t219 @t60 @t14 @t220 @t218 @t217 @t216 @t215 @t214 @t213) (or (= (tptp.hAPP @t219 @t61) @t60) @t221))) % 3.02/3.23 (assume @p328 (forall (@list @t220 @t60 @t14 @t219 @t218 @t217 @t216 @t215 @t214 @t213) (or (= (tptp.hAPP @t220 @t61) @t60) @t221))) % 3.02/3.23 (assume @p329 (forall @t96 (tptp.hBOOL (tptp.hAPP @t41 @t111)))) % 3.02/3.23 (assume @p330 (forall @t337 (= (tptp.c_Com_Ocom_Ocom__case @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t56 @t14) @t336))) % 3.02/3.23 (assume @p331 (forall @t333 (not (= @t58 tptp.c_Com_Ocom_OSKIP)))) % 3.02/3.23 (assume @p332 (forall (@list @t60 @t62 @t107 @t52 @t14 @t265 @t271 @t397 @t230) (or (not (= @t231 (tptp.c_Fun_Ocomp @t265 @t271 @t397 @t52 @t14))) (= @t232 (tptp.hAPP @t265 (tptp.hAPP @t271 @t230)))))) % 3.02/3.23 (assume @p333 (forall (@list @t69 @t67 @t39 @t417 @t416 @t115 @t52 @t14 @t107 @t397 @t415) (or (not (= @t228 (tptp.hAPP @t417 (tptp.hAPP @t416 @t115)))) (= @t229 (tptp.hAPP (tptp.c_Fun_Ocomp @t417 @t416 @t397 @t14 @t415) @t115))))) % 3.02/3.23 (assume @p334 (forall @t392 (= (tptp.c_Set_Ovimage @t69 @t391 @t14 @t52) (tptp.c_Lattices_Oupper__semilattice__class_Osup (tptp.c_Set_Ovimage @t69 (tptp.c_Set_Oinsert @t60 @t101 @t52) @t14 @t52) @t181 @t44)))) % 3.02/3.23 (assume @p335 (forall @t80 (= (tptp.c_HOL_Ominus__class_Ominus @t45 @t249 @t44) (tptp.c_Lattices_Oupper__semilattice__class_Osup @t46 @t321 @t44)))) % 3.02/3.23 (assume @p336 (forall (@list @t45 @t38 @t52 @t53 @t14) (= (tptp.c_Complete__Lattice_Ocomplete__lattice__class_OSUPR @t331 @t53 @t52 @t44) (tptp.c_Lattices_Oupper__semilattice__class_Osup (tptp.c_Complete__Lattice_Ocomplete__lattice__class_OSUPR @t45 @t53 @t52 @t44) (tptp.c_Complete__Lattice_Ocomplete__lattice__class_OSUPR @t38 @t53 @t52 @t44) @t44)))) % 3.02/3.23 (assume @p337 (forall (@list @t45 @t69 @t39 @t14 @t52) (or @t419 (not @t418)))) % 3.02/3.23 (assume @p338 (forall (@list @t69 @t45 @t14 @t52 @t39) (or @t418 (not @t419)))) % 3.02/3.23 (assume @p339 (forall @t240 (or @t334 @t239 @t241))) % 3.02/3.23 (assume @p340 (forall @t423 (or @t422 @t421 @t420 @t153))) % 3.02/3.23 (assume @p341 (forall @t423 (or @t422 @t421 @t152 (not @t420)))) % 3.02/3.23 (assume @p342 (forall @t279 (not (= @t278 tptp.c_Com_Ocom_OSKIP)))) % 3.02/3.23 (assume @p343 (forall (@list @t14) (= (tptp.c_Lattices_Oupper__semilattice__class_Osup @t59 @t59 @t44) @t59))) % 3.02/3.23 (assume @p344 (forall @t183 (= (tptp.c_Set_Oimage @t69 @t331 @t52 @t14) (tptp.c_Lattices_Oupper__semilattice__class_Osup @t177 @t390 @t44)))) % 3.02/3.23 (assume @p345 (forall @t118 (= (tptp.c_Set_Ovimage @t69 @t101 @t14 @t52) @t59))) % 3.02/3.23 (assume @p346 (forall (@list @t27 @t7 @t17 @t5 @t1 @t4) (not (= @t29 @t6)))) % 3.02/3.23 (assume @p347 (forall (@list @t129 @t119 @t128 @t124 @t62) (or @t277 @t132 @t131))) % 3.02/3.23 (assume @p348 (forall @t297 (or @t262 (not @t424)))) % 3.02/3.23 (assume @p349 (forall @t297 (or @t424 @t263))) % 3.02/3.23 (assume @p350 (forall (@list @t129 @t62 @t124) (or @t289 @t425))) % 3.02/3.23 (assume @p351 (forall (@list @t124 @t62 @t129) (or @t243 @t425))) % 3.02/3.23 (assume @p352 (forall (@list @t69 @t67 @t14 @t397 @t107 @t398 @t52) (= (tptp.c_Fun_Ofcomp (tptp.c_Fun_Ofcomp @t69 @t67 @t14 @t397 @t107) @t398 @t14 @t107 @t52) (tptp.c_Fun_Ofcomp @t69 (tptp.c_Fun_Ofcomp @t67 @t398 @t397 @t107 @t52) @t14 @t397 @t52)))) % 3.02/3.23 (assume @p353 (forall @t401 (not (= tptp.c_Com_Ocom_OSKIP @t33)))) % 3.02/3.23 (assume @p354 (forall @t297 (or @t262 @t260))) % 3.02/3.23 (assume @p355 (forall @t164 (or (not (tptp.class_Orderings_Olinorder @t14)) @t152 @t147))) % 3.02/3.23 (assume @p356 (forall (@list @t218 @t50 @t211 @t14) (or @t379 (not @t380)))) % 3.02/3.23 (assume @p357 (forall @t345 (or @t362 @t342 @t341))) % 3.02/3.23 (assume @p358 (forall (@list @t104 @t427 @t14 @t45 @t106) (or (tptp.hBOOL (tptp.hAPP @t104 @t427)) (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t40 @t427) @t45))) @t426))) % 3.02/3.23 (assume @p359 (forall (@list @t106 @t428 @t14 @t45 @t104) (or (tptp.hBOOL (tptp.hAPP @t106 @t428)) (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t40 @t428) @t45))) @t426))) % 3.02/3.23 (assume @p360 (forall @t375 (or @t255 @t359 (not (tptp.hBOOL (tptp.hAPP @t106 @t374)))))) % 3.02/3.23 (assume @p361 (forall @t49 (or (not (= @t47 @t368)) @t42 @t254 (= @t45 @t38)))) % 3.02/3.23 (assume @p362 (forall @t429 (or (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t40 @t365) @t45)) @t255 @t364))) % 3.02/3.23 (assume @p363 (forall (@list @t14 @t62 @t45 @t38 @t52 @t39) (or (tptp.hBOOL (tptp.hAPP @t63 @t207)) (not (tptp.hBOOL (tptp.hAPP @t63 @t205))) @t204))) % 3.02/3.23 (assume @p364 (forall (@list @t52 @t62 @t45 @t38 @t14 @t60) (or (tptp.hBOOL (tptp.hAPP @t430 @t431)) (not (tptp.hBOOL (tptp.hAPP @t430 @t280))) @t352))) % 3.02/3.23 (assume @p365 (forall @t434 (or @t433 (not @t432)))) % 3.02/3.23 (assume @p366 (forall (@list @t217 @t211 @t50 @t14) (or @t432 (not @t433)))) % 3.02/3.23 (assume @p367 (forall (@list @t106 @t45 @t38 @t52 @t14 @t110 @t39) (or (tptp.hBOOL (tptp.hAPP @t106 @t389)) @t383 @t388 @t204))) % 3.02/3.23 (assume @p368 (forall (@list @t14 @t60 @t69 @t38 @t52) (or @t437 (not @t436)))) % 3.02/3.23 (assume @p369 (forall (@list @t52 @t60 @t69 @t45 @t14) (or (tptp.hBOOL (tptp.hAPP @t439 (tptp.c_Set_Ovimage @t69 @t45 @t52 @t14))) (not (tptp.hBOOL (tptp.hAPP @t438 @t45)))))) % 3.02/3.23 (assume @p370 (forall (@list @t52 @t60 @t69 @t38 @t14) (or (tptp.hBOOL (tptp.hAPP @t439 (tptp.c_Set_Ovimage @t69 @t38 @t52 @t14))) (not (tptp.hBOOL (tptp.hAPP @t438 @t38)))))) % 3.02/3.23 (assume @p371 (forall (@list @t52 @t69 @t60 @t38 @t14) (or @t436 (not @t437)))) % 3.02/3.23 (assume @p372 (forall (@list @t52 @t69 @t60 @t45 @t14) (or (tptp.hBOOL (tptp.hAPP @t435 @t45)) (not (tptp.hBOOL (tptp.hAPP @t300 @t182)))))) % 3.02/3.23 (assume @p373 (forall (@list @t218 @t220 @t45 @t39 @t14 @t219 @t217 @t216 @t215 @t214 @t213) (or (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t218 @t387) @t39)) @t255 @t221))) % 3.02/3.23 (assume @p374 (forall (@list @t218 @t39 @t219 @t45 @t14 @t220 @t217 @t216 @t215 @t214 @t213) (or (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t218 @t39) @t386)) @t255 @t221))) % 3.02/3.23 (assume @p375 (forall (@list @t218 @t50 @t267 @t14 @t346) (or @t355 @t440))) % 3.02/3.23 (assume @p376 (forall (@list @t218 @t346 @t50 @t14 @t267) (or @t347 @t440))) % 3.02/3.23 (assume @p377 (forall (@list @t106 @t45 @t38 @t14 @t39) (or @t441 @t364 @t43))) % 3.02/3.23 (assume @p378 (forall (@list @t106 @t45 @t38 @t14 @t110) (or @t441 @t383 @t382))) % 3.02/3.23 (assume @p379 (forall @t429 (or (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t40 @t367) @t45)) @t364 @t255))) % 3.02/3.23 (assume @p380 (forall @t192 (or (= @t191 @t45) @t352))) % 3.02/3.23 (assume @p381 (forall @t434 (or @t443 (not @t442)))) % 3.02/3.23 (assume @p382 (forall (@list @t217 @t50 @t211 @t14) (or @t442 (not @t443)))) % 3.02/3.23 (assume @p383 (forall (@list @t45 @t38 @t14 @t52 @t107 @t62 @t265 @t39) (or @t445 (not (tptp.hBOOL (tptp.hAPP @t444 @t265))) @t255))) % 3.02/3.23 (assume @p384 (forall (@list @t45 @t38 @t14 @t52 @t62 @t39) (or @t446 (not (tptp.hBOOL @t444)) @t255))) % 3.02/3.23 (assume @p385 (forall (@list @t45 @t38 @t14 @t52 @t107 @t62 @t265 @t60) (or @t445 (not (tptp.hBOOL (tptp.hAPP @t447 @t265))) @t352))) % 3.02/3.23 (assume @p386 (forall (@list @t45 @t38 @t14 @t52 @t62 @t60) (or @t446 (not (tptp.hBOOL @t447)) @t352))) % 3.02/3.23 (assume @p387 (forall (@list @t217 @t50 @t267 @t14 @t218 @t346) (or @t350 @t448))) % 3.02/3.23 (assume @p388 (forall (@list @t218 @t346 @t50 @t14 @t217 @t267) (or @t347 @t448))) % 3.02/3.23 (assume @p389 (forall @t429 (or (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t40 @t449) @t45)) @t364 @t255))) % 3.02/3.23 (assume @p390 (forall @t366 (or (tptp.hBOOL (tptp.hAPP @t106 @t449)) @t364 @t255))) % 3.02/3.23 (assume @p391 (forall (@list @t193 @t39 @t45 @t14 @t69) (or (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t195 @t39) @t45))) (tptp.hBOOL (tptp.hAPP @t450 (tptp.c_Set_Oimage @t69 @t45 @t193 @t14)))))) % 3.02/3.23 (assume @p392 (forall (@list @t52 @t39 @t45 @t14 @t69) (or @t204 @t451))) % 3.02/3.23 (assume @p393 (forall (@list @t14 @t69 @t39 @t45 @t52) (or @t451 @t204))) % 3.02/3.23 (assume @p394 (forall (@list @t52 @t69 @t39 @t45 @t14) (or (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t203 @t299) @t298)) @t255))) % 3.02/3.23 (assume @p395 (forall @t458 (= (tptp.hAPP (tptp.c_Lattices_Olower__semilattice__class_Oinf @t457 @t456 @t452) tptp.v_x) (tptp.hAPP @t454 (tptp.c_Lattices_Olower__semilattice__class_Oinf @t105 @t377 @t452))))) % 3.02/3.23 (assume @p396 (forall @t458 (= (tptp.hAPP (tptp.c_Lattices_Oupper__semilattice__class_Osup @t457 @t456 @t452) tptp.v_x) (tptp.hAPP @t454 (tptp.c_Lattices_Oupper__semilattice__class_Osup @t105 @t377 @t452))))) % 3.02/3.23 (assume @p397 (forall @t459 (= (tptp.hAPP (tptp.c_Fun_Ocomp @t69 @t67 @t107 @t52 tptp.t_a) tptp.v_x) (tptp.hAPP @t69 @t68)))) % 3.02/3.23 (assume @p398 (= (tptp.hAPP (tptp.c_Fun_Oid tptp.t_a) tptp.v_x) tptp.v_x)) % 3.02/3.23 (assume @p399 (forall @t459 (= (tptp.hAPP (tptp.c_Fun_Ofcomp @t69 @t67 tptp.t_a @t107 @t52) tptp.v_x) (tptp.hAPP @t67 @t70)))) % 3.02/3.23 (assume @p400 (forall (@list @t7 @t17 @t1) (not (= @t460 @t58)))) % 3.02/3.23 (assume @p401 (forall (@list @t62 @t119 @t128 @t265) (or @t120 @t338 (not (tptp.c_Natural_Oevalc @t461 @t119 @t128))))) % 3.02/3.23 (assume @p402 (forall (@list @t4 @t198 @t55 @t54) (not (= @t462 @t57)))) % 3.02/3.23 (assume @p403 (forall @t464 (= (tptp.c_Com_Ocom_Ocom__case @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t460 @t14) @t463))) % 3.02/3.23 (assume @p404 (forall (@list @t4 @t198 @t8 @t7) (not (= @t462 @t34)))) % 3.02/3.23 (assume @p405 (forall (@list @t7 @t17 @t5 @t1 @t4) (not (= @t460 @t6)))) % 3.02/3.23 (assume @p406 (forall @t465 (not (= tptp.c_Com_Ocom_OSKIP @t462)))) % 3.02/3.23 (assume @p407 (forall (@list @t27 @t7 @t17 @t4 @t198) (not (= @t29 @t462)))) % 3.02/3.23 (assume @p408 (forall (@list @t8 @t7 @t4 @t198) (not (= @t34 @t462)))) % 3.02/3.23 (assume @p409 (forall (@list @t7 @t55 @t54 @t4 @t198) (not (= @t56 @t462)))) % 3.02/3.23 (assume @p410 (forall (@list @t55 @t54 @t4 @t198) (not (= @t57 @t462)))) % 3.02/3.23 (assume @p411 (forall (@list @t62 @t265 @t119) (or (tptp.c_Natural_Oevalc @t461 @t119 @t119) @t120))) % 3.02/3.23 (assume @p412 (forall (@list @t4 @t198 @t27 @t7 @t17) (not (= @t462 @t29)))) % 3.02/3.23 (assume @p413 (forall (@list @t1 @t7 @t17) (not (= @t58 @t460)))) % 3.02/3.23 (assume @p414 (forall @t465 (not (= @t462 tptp.c_Com_Ocom_OSKIP)))) % 3.02/3.23 (assume @p415 (forall (@list @t62 @t265 @t133 @t134 @t122) (or (tptp.c_Natural_Oevalc @t461 @t133 @t134) (not (tptp.c_Natural_Oevalc @t461 @t122 @t134)) (not (tptp.c_Natural_Oevalc @t265 @t133 @t122)) @t466))) % 3.02/3.23 (assume @p416 (forall (@list @t5 @t1 @t4 @t7 @t17) (not (= @t6 @t460)))) % 3.02/3.23 (assume @p417 (forall (@list @t62 @t265) (or @t467 @t327))) % 3.02/3.23 (assume @p418 (forall (@list @t265 @t62) (or @t326 (not @t467)))) % 3.02/3.23 (assume @p419 (forall (@list @t4 @t198 @t7 @t55 @t54) (not (= @t462 @t56)))) % 3.02/3.23 (assume @p420 (forall @t464 (= (tptp.c_Com_Ocom_Ocom__rec @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t460 @t14) (tptp.hAPP @t463 @t26)))) % 3.02/3.23 (assume @p421 (forall (@list @t129 @t119 @t258 @t128 @t124 @t62) (or @t470 @t469 @t468))) % 3.02/3.23 (assume @p422 (forall (@list @t265 @t119 @t259 @t128 @t258) (or (tptp.c_Natural_Oevaln @t265 @t119 @t259 @t128) @t263 @t471))) % 3.02/3.23 (assume @p423 (forall (@list @t119 @t258) (tptp.c_Natural_Oevaln tptp.c_Com_Ocom_OSKIP @t119 @t258 @t119))) % 3.02/3.23 (assume @p424 (forall @t473 (or @t472 (not (tptp.c_Natural_Oevaln @t124 @t119 @t258 @t122)) @t120))) % 3.02/3.23 (assume @p425 (forall (@list @t129 @t119 @t258 @t128 @t62 @t124) (or @t470 @t120 @t468))) % 3.02/3.23 (assume @p426 (forall (@list @t265 @t119 @t258 @t474) (or (tptp.c_Natural_Oevaln @t265 @t119 @t295 @t474) @t475))) % 3.02/3.23 (assume @p427 (forall (@list @t129 @t134 @t124 @t122 @t476 @t479 @t480 @t477) (or (tptp.c_Natural_Oevaln @t129 @t134 @t482 @t479) @t481 @t478))) % 3.02/3.23 (assume @p428 (forall (@list @t124 @t122 @t129 @t134 @t476 @t479 @t480 @t477) (or (tptp.c_Natural_Oevaln @t124 @t122 @t482 @t476) @t481 @t478))) % 3.02/3.23 (assume @p429 (forall @t473 (or @t472 (not (tptp.c_Natural_Oevaln @t123 @t119 @t258 @t122)) @t121))) % 3.02/3.23 (assume @p430 (forall (@list @t62 @t119 @t124 @t258 @t128 @t129) (or @t121 @t469 @t468))) % 3.02/3.23 (assume @p431 (forall (@list @t123 @t124 @t133 @t258 @t134 @t122) (or (tptp.c_Natural_Oevaln @t135 @t133 @t258 @t134) (not (tptp.c_Natural_Oevaln @t124 @t122 @t258 @t134)) (not (tptp.c_Natural_Oevaln @t123 @t133 @t258 @t122))))) % 3.02/3.24 (assume @p432 (forall (@list @t128 @t119 @t258) (or @t338 (not (tptp.c_Natural_Oevaln tptp.c_Com_Ocom_OSKIP @t119 @t258 @t128))))) % 3.02/3.24 (assume @p433 (forall (@list @t265 @t119 @t128 @t258) (or @t266 @t471))) % 3.02/3.24 (assume @p434 (forall (@list @t265 @t119 @t128 @t39) (or @t266 (not (tptp.c_Natural_Oevaln @t265 @t119 @t39 @t128))))) % 3.02/3.24 (assume @p435 (= (tptp.hAPP (tptp.c_COMBI tptp.t_a) tptp.v_P) tptp.v_P)) % 3.02/3.24 (assume @p436 (forall (@list @t258 @t128 @t14) (or (tptp.c_Hoare__Mirabelle_Otriple__valid @t258 @t128 @t14) (not (tptp.c_Hoare__Mirabelle_Otriple__valid @t295 @t128 @t14))))) % 3.02/3.24 (assume @p437 (forall (@list @t258 @t489 @t483 @t484) (or (tptp.c_Hoare__Mirabelle_Otriple__valid @t258 @t489 tptp.t_a) (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t488 @t489) @t483))) (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t488 @t487) @t484)) @t486))) % 3.02/3.24 (assume @p438 (forall (@list @t258 @t110 @t483) (or (tptp.c_Hoare__Mirabelle_Otriple__valid @t258 @t110 tptp.t_a) (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t488 @t110) @t483))) (not (tptp.c_Hoare__Mirabelle_Otriple__valid @t295 @t490 tptp.t_a))))) % 3.02/3.24 (assume @p439 (forall (@list @t484 @t483 @t39) (or @t485 (tptp.c_Hoare__Mirabelle_Otriple__valid (tptp.v_sko__Hoare__Mirabelle__Xhoare__valids__def__2 @t484 @t483) @t39 tptp.t_a) (not (tptp.hBOOL (tptp.hAPP @t491 @t484)))))) % 3.02/3.24 (assume @p440 (forall (@list @t258 @t492 @t483 @t484) (or (tptp.c_Hoare__Mirabelle_Otriple__valid @t258 @t492 tptp.t_a) (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t488 @t492) @t483))) (not (tptp.c_Hoare__Mirabelle_Otriple__valid @t258 @t487 tptp.t_a)) @t486))) % 3.02/3.24 (assume @p441 (= (tptp.hAPP @t493 tptp.v_x) (tptp.hAPP @t454 @t493))) % 3.02/3.24 (assume @p442 (forall @t497 (or @t496 @t121 @t494))) % 3.02/3.24 (assume @p443 (forall @t499 (or @t498 @t338 @t494))) % 3.02/3.24 (assume @p444 (forall @t497 (or @t496 @t338 @t494))) % 3.02/3.24 (assume @p445 (forall @t499 (or @t498 @t121 @t494))) % 3.02/3.24 (assume @p446 (forall (@list @t104 @t500 @t474 @t265 @t119 @t258 @t106) (or (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t104 @t500) @t474)) @t475 (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t106 @t500) @t119))) (not (tptp.c_Hoare__Mirabelle_Otriple__valid @t258 (tptp.c_Hoare__Mirabelle_Otriple_Otriple @t106 @t265 @t104 tptp.t_a) tptp.t_a))))) % 3.02/3.24 (assume @p447 (forall (@list @t258 @t39 @t483) (or (tptp.c_Hoare__Mirabelle_Otriple__valid @t258 @t39 tptp.t_a) (not (tptp.hBOOL (tptp.hAPP @t491 @t483))) (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t488 @t490) @t483))))) % 3.02/3.24 (assume @p448 (forall (@list @t62 @t119 @t128 @t265 @t258) (or @t120 @t338 @t494))) % 3.02/3.24 (assume @p449 (forall (@list @t62 @t265 @t119 @t258) (or (tptp.c_Natural_Oevaln @t461 @t119 @t258 @t119) @t120))) % 3.02/3.24 (assume @p450 (forall (@list @t14 @t39 @t377) (or @t502 (not @t501)))) % 3.02/3.24 (assume @p451 (forall (@list @t377 @t39 @t14) (or @t501 (not @t502)))) % 3.02/3.24 (assume @p452 (forall (@list @t62 @t265 @t133 @t258 @t134 @t122) (or (tptp.c_Natural_Oevaln @t461 @t133 @t258 @t134) (not (tptp.c_Natural_Oevaln @t461 @t122 @t258 @t134)) (not (tptp.c_Natural_Oevaln @t265 @t133 @t258 @t122)) @t466))) % 3.02/3.24 (assume @p453 (forall @t504 (or @t503 @t12))) % 3.02/3.24 (assume @p454 (forall @t504 (or @t503 @t287))) % 3.02/3.24 (assume @p455 (tptp.hBOOL (tptp.hAPP tptp.v_ba tptp.v_s0))) % 3.02/3.24 (assume @p456 (tptp.c_Natural_Oevaln tptp.v_ca tptp.v_s0 tptp.v_na tptp.v_s1)) % 3.02/3.24 (assume @p457 (tptp.c_Natural_Oevaln @t505 tptp.v_s1 tptp.v_na tptp.v_s2)) % 3.02/3.24 (assume @p458 (= tptp.v_ba tptp.v_b)) % 3.02/3.24 (assume @p459 (= tptp.v_ca tptp.v_c)) % 3.02/3.24 (assume @p460 @t507) % 3.02/3.24 (assume @p461 (forall @t413 (or (tptp.c_Hoare__Mirabelle_Otriple__valid tptp.v_na @t39 tptp.t_a) (not (tptp.hBOOL (tptp.hAPP @t491 tptp.v_G)))))) % 3.02/3.24 (assume @p462 (or @t509 (not @t508))) % 3.02/3.24 (assume @p463 (forall @t516 (or @t515 @t513 @t512 @t510))) % 3.02/3.24 (assume @p464 (forall @t516 (or @t515 @t517 @t512 @t510))) % 3.02/3.24 (assume @p465 (forall @t523 (or @t515 @t522 @t521 @t518))) % 3.02/3.24 (assume @p466 (forall @t523 (or @t515 @t517 @t521 @t518))) % 3.02/3.24 (assume @p467 @t530) % 3.02/3.24 (assume @p468 @t533) % 3.02/3.24 (assume @p469 @t539) % 3.02/3.24 (assume @p470 @t541) % 3.02/3.24 (assume @p471 (forall (@list @t500 @t474 @t119 @t489) (or (tptp.hBOOL (tptp.hAPP @t511 @t474)) (not (tptp.c_Natural_Oevaln tptp.v_c @t119 @t489 @t474)) (not (tptp.hBOOL (tptp.hAPP tptp.v_b @t119))) (not (tptp.hBOOL (tptp.hAPP @t511 @t119))) (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t488 @t542) tptp.v_G))))) % 3.02/3.24 (assume @p472 (forall (@list @t519 @t544 @t543 @t489) (or (tptp.hBOOL (tptp.hAPP @t520 @t544)) (not (tptp.c_Natural_Oevaln tptp.v_c @t543 @t489 @t544)) (not (tptp.hBOOL (tptp.hAPP tptp.v_b @t543))) (not (tptp.hBOOL (tptp.hAPP @t520 @t543))) (not (tptp.c_Hoare__Mirabelle_Otriple__valid @t489 @t542 tptp.t_a))))) % 3.02/3.24 (assume @p473 (forall @t548 (or (tptp.class_Complete__Lattice_Ocomplete__lattice @t547) (not (tptp.class_Complete__Lattice_Ocomplete__lattice @t545))))) % 3.02/3.24 (assume @p474 (forall @t548 (or (tptp.class_Lattices_Oupper__semilattice @t547) @t549))) % 3.02/3.24 (assume @p475 (forall @t548 (or (tptp.class_Lattices_Olower__semilattice @t547) @t549))) % 3.02/3.24 (assume @p476 (forall @t548 (or (tptp.class_Lattices_Odistrib__lattice @t547) (not (tptp.class_Lattices_Odistrib__lattice @t545))))) % 3.02/3.24 (assume @p477 (forall @t548 (or (tptp.class_Lattices_Obounded__lattice @t547) (not (tptp.class_Lattices_Obounded__lattice @t545))))) % 3.02/3.24 (assume @p478 (forall @t548 (or (tptp.class_Orderings_Opreorder @t547) (not (tptp.class_Orderings_Opreorder @t545))))) % 3.02/3.24 (assume @p479 (forall @t548 (or (tptp.class_Lattices_Olattice @t547) @t549))) % 3.02/3.24 (assume @p480 (forall @t548 (or (tptp.class_Orderings_Oorder @t547) (not (tptp.class_Orderings_Oorder @t545))))) % 3.02/3.24 (assume @p481 (forall @t548 (or (tptp.class_Orderings_Obot @t547) (not (tptp.class_Orderings_Obot @t545))))) % 3.02/3.24 (assume @p482 (forall @t548 (or (tptp.class_HOL_Ominus @t547) (not (tptp.class_HOL_Ominus @t545))))) % 3.02/3.24 (assume @p483 (tptp.class_Lattices_Oupper__semilattice tptp.tc_nat)) % 3.02/3.24 (assume @p484 (tptp.class_Lattices_Olower__semilattice tptp.tc_nat)) % 3.02/3.24 (assume @p485 (tptp.class_Lattices_Odistrib__lattice tptp.tc_nat)) % 3.02/3.24 (assume @p486 (tptp.class_Orderings_Opreorder tptp.tc_nat)) % 3.02/3.24 (assume @p487 (tptp.class_Orderings_Olinorder tptp.tc_nat)) % 3.02/3.24 (assume @p488 (tptp.class_Lattices_Olattice tptp.tc_nat)) % 3.02/3.24 (assume @p489 (tptp.class_Orderings_Oorder tptp.tc_nat)) % 3.02/3.24 (assume @p490 (tptp.class_Orderings_Obot tptp.tc_nat)) % 3.02/3.24 (assume @p491 (tptp.class_HOL_Ominus tptp.tc_nat)) % 3.02/3.24 (assume @p492 (tptp.class_Complete__Lattice_Ocomplete__lattice tptp.tc_bool)) % 3.02/3.24 (assume @p493 (tptp.class_Lattices_Oupper__semilattice tptp.tc_bool)) % 3.02/3.24 (assume @p494 (tptp.class_Lattices_Olower__semilattice tptp.tc_bool)) % 3.02/3.24 (assume @p495 (tptp.class_Lattices_Odistrib__lattice tptp.tc_bool)) % 3.02/3.24 (assume @p496 (tptp.class_Lattices_Obounded__lattice tptp.tc_bool)) % 3.02/3.24 (assume @p497 (tptp.class_Orderings_Opreorder tptp.tc_bool)) % 3.02/3.24 (assume @p498 (tptp.class_Lattices_Olattice tptp.tc_bool)) % 3.02/3.24 (assume @p499 (tptp.class_Orderings_Oorder tptp.tc_bool)) % 3.02/3.24 (assume @p500 (tptp.class_Orderings_Obot tptp.tc_bool)) % 3.02/3.24 (assume @p501 (tptp.class_HOL_Ominus tptp.tc_bool)) % 3.02/3.24 (assume @p502 (forall (@list @t39 @t14) (tptp.c_fequal @t39 @t39 @t14))) % 3.02/3.24 (assume @p503 (forall (@list @t136 @t13 @t14) (or (= @t136 @t13) (not (tptp.c_fequal @t136 @t13 @t14))))) % 3.02/3.24 (step @p504 :rule instantiate :premises (@p461) :args ((@list @t550))) % 3.02/3.24 (step @p505 :rule instantiate :premises (@p471) :args (@t551)) % 3.02/3.24 (step @p506 :rule true_intro :premises (@p455)) % 3.02/3.24 (step @p507 :rule refl :args (tptp.v_s0)) % 3.02/3.24 (step @p508 :rule symm :premises (@p458)) % 3.02/3.24 (step @p509 :rule cong :premises (@p508 @p507) :args (@t552)) % 3.02/3.24 (step @p510 :rule cong :premises (@p509) :args (@t553)) % 3.02/3.24 (step @p511 :rule trans :premises (@p510 @p506)) % 3.02/3.24 (step @p512 :rule true_elim :premises (@p511)) % 3.02/3.24 (step @p513 :rule true_intro :premises (@p456)) % 3.02/3.24 (step @p514 :rule refl :args (tptp.v_s1)) % 3.02/3.24 (step @p515 :rule refl :args (tptp.v_na)) % 3.02/3.24 (step @p516 :rule symm :premises (@p459)) % 3.02/3.24 (step @p517 :rule cong :premises (@p516 @p507 @p515 @p514) :args (@t554)) % 3.02/3.24 (step @p518 :rule trans :premises (@p517 @p513)) % 3.02/3.24 (step @p519 :rule true_elim :premises (@p518)) % 3.02/3.24 (step @p520 :rule alpha_equiv :args (@t556 @t557 @t558)) % 3.02/3.24 (step @p521 :rule equiv_elim1 :premises (@p520)) % 3.02/3.24 (step @p522 :rule reordering :premises (@p521) :args ((or @t560 (not @t556)))) % 3.02/3.24 (step @p523 :rule cong :premises (@p458 @p459) :args (@t505)) % 3.02/3.24 (step @p524 :rule quant-miniscope-or :args ((= (forall @t523 @t561) (or @t528 @t535 @t560)))) % 3.02/3.24 (step @p525 :rule aci_norm :args ((= @t538 @t561))) % 3.02/3.24 (step @p526 :rule cong :premises (@p525) :args (@t539)) % 3.02/3.24 (step @p527 :rule trans :premises (@p526 @p524)) % 3.02/3.24 (step @p528 :rule eq_resolve :premises (@p469 @p527)) % 3.02/3.24 (step @p529 :rule quant-miniscope-or :args ((= (forall @t516 @t562) (or @t528 @t524 @t556)))) % 3.02/3.24 (step @p530 :rule aci_norm :args ((= @t529 @t562))) % 3.02/3.24 (step @p531 :rule cong :premises (@p530) :args (@t530)) % 3.02/3.24 (step @p532 :rule trans :premises (@p531 @p529)) % 3.02/3.24 (step @p533 :rule eq_resolve :premises (@p467 @p532)) % 3.02/3.24 (step @p534 :rule instantiate :premises (@p461) :args ((@list tptp.v_xa))) % 3.02/3.24 (step @p535 :rule cnf_or_pos :args (@t564)) % 3.02/3.24 (step @p536 :rule reordering :premises (@p535) :args ((or @t534 @t563 (not @t564)))) % 3.02/3.24 (step @p537 :rule chain_m_resolution :premises (@p536 @p534 @p533 @p523 @p528 @p523 @p522) :args (@t560 (@list false false false true false true) (@list @t564 @t524 @t527 @t534 @t527 @t556))) % 3.02/3.24 (step @p538 :rule equiv_elim2 :premises (@p520)) % 3.02/3.24 (step @p539 :rule chain_m_resolution :premises (@p538 @p537) :args (@t556 (@list false) (@list @t560))) % 3.02/3.24 (step @p540 :rule instantiate :premises (@p539) :args (@t565)) % 3.02/3.24 (step @p541 :rule cnf_or_pos :args (@t568)) % 3.02/3.24 (step @p542 :rule reordering :premises (@p541) :args ((or @t508 @t567 (not @t568)))) % 3.02/3.24 (assume-push @p572 @t569) % 3.02/3.24 (step @p544 :rule instantiate :premises (@p572) :args (@t565)) % 3.02/3.24 (step-pop @p573 :rule scope :premises (@p544)) % 3.02/3.24 (step @p545 :rule process_scope :premises (@p573) :args (@t567)) % 3.02/3.24 (step @p547 :rule implies_elim :premises (@p545)) % 3.02/3.24 (step @p548 :rule alpha_equiv :args (@t569 @t557 @t558)) % 3.02/3.24 (step @p549 :rule equiv_elim2 :premises (@p548)) % 3.02/3.24 (step @p550 :rule quant-miniscope-or :args ((= (forall @t516 @t570) (or @t528 @t531 @t524 @t569)))) % 3.02/3.24 (step @p551 :rule aci_norm :args ((= @t532 @t570))) % 3.02/3.24 (step @p552 :rule cong :premises (@p551) :args (@t533)) % 3.02/3.24 (step @p553 :rule trans :premises (@p552 @p550)) % 3.02/3.24 (step @p554 :rule eq_resolve :premises (@p468 @p553)) % 3.02/3.24 (step @p555 :rule reordering :premises (@p554) :args ((or @t528 @t524 @t531 @t569))) % 3.02/3.24 (step @p556 :rule quant-miniscope-or :args ((= (forall @t523 @t572) (or @t528 @t531 @t535 @t571)))) % 3.02/3.24 (step @p557 :rule aci_norm :args ((= @t540 @t572))) % 3.02/3.24 (step @p558 :rule cong :premises (@p557) :args (@t541)) % 3.02/3.24 (step @p559 :rule trans :premises (@p558 @p556)) % 3.02/3.24 (step @p560 :rule eq_resolve :premises (@p470 @p559)) % 3.02/3.24 (step @p561 :rule chain_m_resolution :premises (@p536 @p534 @p560 @p523 @p555 @p523 @p549 @p462 @p547 @p542 @p540) :args (@t567 (@list false true false false false true false true false false) (@list @t564 @t534 @t527 @t524 @t527 @t571 @t509 @t569 @t508 @t568))) % 3.02/3.24 (step @p562 :rule cnf_or_pos :args (@t577)) % 3.02/3.24 (step @p563 :rule reordering :premises (@p562) :args ((or @t574 @t566 @t576 @t575 @t573 (not @t577)))) % 3.02/3.24 (step @p564 :rule chain_m_resolution :premises (@p563 @p460 @p561 @p519 @p512 @p505) :args (@t573 @t578 (@list @t507 @t566 @t554 @t553 @t577))) % 3.02/3.24 (step @p565 :rule instantiate :premises (@p472) :args (@t551)) % 3.02/3.24 (step @p566 :rule cnf_or_pos :args (@t581)) % 3.02/3.24 (step @p567 :rule reordering :premises (@p566) :args ((or @t574 @t566 @t576 @t575 @t580 (not @t581)))) % 3.02/3.24 (step @p568 :rule chain_m_resolution :premises (@p567 @p460 @p561 @p519 @p512 @p565) :args (@t580 @t578 (@list @t507 @t566 @t554 @t553 @t581))) % 3.02/3.24 (step @p569 :rule cnf_or_pos :args (@t583)) % 3.02/3.24 (step @p570 :rule reordering :premises (@p569) :args ((or @t579 @t582 (not @t583)))) % 3.02/3.24 (step @p571 false :rule chain_m_resolution :premises (@p570 @p568 @p564 @p504) :args (false (@list true false false) (@list @t579 @t573 @t583))) % 3.02/3.24 ) % 3.02/3.24 % SZS output end Proof % 3.02/3.24 % cvc5 exiting %------------------------------------------------------------------------------