|
95a654bfff554e647800fe77ff2ba30347402e24 9 0
unsat
(assume a0 (! (not true) :named @p_1))
(step t2 (cl (! (= @p_1 false) :named @p_2)) :rule not_simplify)
(step t3 (cl (! (not @p_2) :named @p_4) (! (not @p_1) :named @p_3) false) :rule equiv_pos2)
(step t4 (cl (not @p_3) true) :rule not_not)
(step t5 (cl @p_4 true false) :rule th_resolution :premises (t4 t3))
(step t6 (cl false) :rule th_resolution :premises (a0 t2 t5))
(step t7 (cl (not false)) :rule false)
(step t8 (cl) :rule resolution :premises (t6 t7))
064ce4a7bbfaa11e79501270fc838c420c703181 12 0
unsat
(assume a0 (! (not (! (or p$ (not p$)) :named @p_1)) :named @p_2))
(step t2 (cl (= @p_1 true)) :rule or_simplify)
(step t3 (cl (= @p_2 (! (not true) :named @p_3))) :rule cong :premises (t2))
(step t4 (cl (= @p_3 false)) :rule not_simplify)
(step t5 (cl (! (= @p_2 false) :named @p_4)) :rule trans :premises (t3 t4))
(step t6 (cl (! (not @p_4) :named @p_6) (! (not @p_2) :named @p_5) false) :rule equiv_pos2)
(step t7 (cl (not @p_5) @p_1) :rule not_not)
(step t8 (cl @p_6 @p_1 false) :rule th_resolution :premises (t7 t6))
(step t9 (cl false) :rule th_resolution :premises (a0 t5 t8))
(step t10 (cl (not false)) :rule false)
(step t11 (cl) :rule resolution :premises (t9 t10))
d4888d8ad473d347e6ab6d509244a7583a7babd4 17 0
unsat
(assume a0 (! (not (! (= (! (and p$ true) :named @p_1) p$) :named @p_3)) :named @p_5))
(step t2 (cl (= @p_1 (! (and p$) :named @p_2))) :rule and_simplify)
(step t3 (cl (= @p_2 p$)) :rule and_simplify)
(step t4 (cl @p_3) :rule trans :premises (t2 t3))
(step t5 (cl (= @p_3 (! (= p$ p$) :named @p_4))) :rule cong :premises (t4))
(step t6 (cl (= @p_4 true)) :rule equiv_simplify)
(step t7 (cl (= @p_3 true)) :rule trans :premises (t5 t6))
(step t8 (cl (= @p_5 (! (not true) :named @p_6))) :rule cong :premises (t7))
(step t9 (cl (= @p_6 false)) :rule not_simplify)
(step t10 (cl (! (= @p_5 false) :named @p_7)) :rule trans :premises (t8 t9))
(step t11 (cl (! (not @p_7) :named @p_9) (! (not @p_5) :named @p_8) false) :rule equiv_pos2)
(step t12 (cl (not @p_8) @p_3) :rule not_not)
(step t13 (cl @p_9 @p_3 false) :rule th_resolution :premises (t12 t11))
(step t14 (cl false) :rule th_resolution :premises (a0 t10 t13))
(step t15 (cl (not false)) :rule false)
(step t16 (cl) :rule resolution :premises (t14 t15))
337e2bffaa7ce02e1ab772f593ffdbb243d5e449 15 0
unsat
(assume a0 (! (not (! (=> (! (and (! (or p$ q$) :named @p_8) (! (not p$) :named @p_9)) :named @p_2) q$) :named @p_6)) :named @p_1))
(step t2 (cl (! (= @p_1 (! (and @p_2 (! (not q$) :named @p_10)) :named @p_4)) :named @p_3)) :rule bool_simplify)
(step t3 (cl (! (not @p_3) :named @p_7) (! (not @p_1) :named @p_5) @p_4) :rule equiv_pos2)
(step t4 (cl (not @p_5) @p_6) :rule not_not)
(step t5 (cl @p_7 @p_6 @p_4) :rule th_resolution :premises (t4 t3))
(step t6 (cl @p_4) :rule th_resolution :premises (a0 t2 t5))
(step t7 (cl (! (= @p_4 (! (and @p_8 @p_9 @p_10) :named @p_12)) :named @p_11)) :rule ac_simp)
(step t8 (cl (not @p_11) (not @p_4) @p_12) :rule equiv_pos2)
(step t9 (cl @p_12) :rule th_resolution :premises (t6 t7 t8))
(step t10 (cl @p_8) :rule and :premises (t9))
(step t11 (cl p$ q$) :rule or :premises (t10))
(step t12 (cl @p_9) :rule and :premises (t9))
(step t13 (cl @p_10) :rule and :premises (t9))
(step t14 (cl) :rule resolution :premises (t11 t12 t13))
10d84ea161ad298d0be18624997ac708a1f26ba1 12 0
unsat
(assume a0 (! (not (! (=> (! (or (and a$ b$) (and c$ d$)) :named @p_1) @p_1) :named @p_6)) :named @p_2))
(step t2 (cl (! (= @p_2 (! (and @p_1 (not @p_1)) :named @p_4)) :named @p_3)) :rule bool_simplify)
(step t3 (cl (! (not @p_3) :named @p_7) (! (not @p_2) :named @p_5) @p_4) :rule equiv_pos2)
(step t4 (cl (not @p_5) @p_6) :rule not_not)
(step t5 (cl @p_7 @p_6 @p_4) :rule th_resolution :premises (t4 t3))
(step t6 (cl @p_4) :rule th_resolution :premises (a0 t2 t5))
(step t7 (cl (! (= @p_4 false) :named @p_8)) :rule and_simplify)
(step t8 (cl (not @p_8) (not @p_4) false) :rule equiv_pos2)
(step t9 (cl false) :rule th_resolution :premises (t6 t7 t8))
(step t10 (cl (not false)) :rule false)
(step t11 (cl) :rule resolution :premises (t9 t10))
9edc95cdafbdeeaebc87884ea4bcc53a0e812967 12 0
unsat
(assume a0 (! (not (! (=> (! (or (and p1$ p2$) p3$) :named @p_2) (! (or (! (=> p1$ (or (and p3$ p2$) (and p1$ p3$))) :named @p_10) p1$) :named @p_3)) :named @p_7)) :named @p_1))
(step t2 (cl (! (= @p_1 (! (and @p_2 (! (not @p_3) :named @p_9)) :named @p_5)) :named @p_4)) :rule bool_simplify)
(step t3 (cl (! (not @p_4) :named @p_8) (! (not @p_1) :named @p_6) @p_5) :rule equiv_pos2)
(step t4 (cl (not @p_6) @p_7) :rule not_not)
(step t5 (cl @p_8 @p_7 @p_5) :rule th_resolution :premises (t4 t3))
(step t6 (cl @p_5) :rule th_resolution :premises (a0 t2 t5))
(step t7 (cl @p_9) :rule and :premises (t6))
(step t8 (cl (not @p_10)) :rule not_or :premises (t7))
(step t9 (cl p1$) :rule not_implies1 :premises (t8))
(step t10 (cl (not p1$)) :rule not_or :premises (t7))
(step t11 (cl) :rule resolution :premises (t10 t9))
f8dcc171fd9ab79494da2e1c5e4771e075fd9d51 29 0
unsat
(assume a0 (! (not (! (= (! (= (! (= (! (= (! (= (! (= (! (= (! (= (! (= p$ p$) :named @p_1) p$) :named @p_2) p$) :named @p_4) p$) :named @p_5) p$) :named @p_6) p$) :named @p_7) p$) :named @p_8) p$) :named @p_9) p$) :named @p_10)) :named @p_11))
(step t2 (cl (= @p_1 true)) :rule equiv_simplify)
(step t3 (cl (= @p_2 (! (= true p$) :named @p_3))) :rule cong :premises (t2))
(step t4 (cl (= @p_3 p$)) :rule equiv_simplify)
(step t5 (cl @p_4) :rule trans :premises (t3 t4))
(step t6 (cl (= @p_4 @p_1)) :rule cong :premises (t5))
(step t7 (cl (= @p_4 true)) :rule trans :premises (t6 t2))
(step t8 (cl (= @p_5 @p_3)) :rule cong :premises (t7))
(step t9 (cl @p_6) :rule trans :premises (t8 t4))
(step t10 (cl (= @p_6 @p_1)) :rule cong :premises (t9))
(step t11 (cl (= @p_6 true)) :rule trans :premises (t10 t2))
(step t12 (cl (= @p_7 @p_3)) :rule cong :premises (t11))
(step t13 (cl @p_8) :rule trans :premises (t12 t4))
(step t14 (cl (= @p_8 @p_1)) :rule cong :premises (t13))
(step t15 (cl (= @p_8 true)) :rule trans :premises (t14 t2))
(step t16 (cl (= @p_9 @p_3)) :rule cong :premises (t15))
(step t17 (cl @p_10) :rule trans :premises (t16 t4))
(step t18 (cl (= @p_10 @p_1)) :rule cong :premises (t17))
(step t19 (cl (= @p_10 true)) :rule trans :premises (t18 t2))
(step t20 (cl (= @p_11 (! (not true) :named @p_12))) :rule cong :premises (t19))
(step t21 (cl (= @p_12 false)) :rule not_simplify)
(step t22 (cl (! (= @p_11 false) :named @p_13)) :rule trans :premises (t20 t21))
(step t23 (cl (! (not @p_13) :named @p_15) (! (not @p_11) :named @p_14) false) :rule equiv_pos2)
(step t24 (cl (not @p_14) @p_10) :rule not_not)
(step t25 (cl @p_15 @p_10 false) :rule th_resolution :premises (t24 t23))
(step t26 (cl false) :rule th_resolution :premises (a0 t22 t25))
(step t27 (cl (not false)) :rule false)
(step t28 (cl) :rule resolution :premises (t26 t27))
ef250e7a4e9499952e8416cff69ed029a37c7aa3 59 0
unsat
(assume a0 (! (or a$ (or b$ (or c$ d$))) :named @p_1))
(assume a2 (! (or (! (not (! (or a$ (! (and c$ (! (not c$) :named @p_40)) :named @p_4)) :named @p_5)) :named @p_8) b$) :named @p_9))
(assume a3 (! (or (! (not (! (and b$ (! (or x$ (not x$)) :named @p_13)) :named @p_14)) :named @p_17) c$) :named @p_18))
(assume a4 (! (or (! (not (! (or d$ false) :named @p_22)) :named @p_24) c$) :named @p_25))
(assume a5 (! (not (! (or c$ (! (and (! (not p$) :named @p_34) (! (or p$ (! (and q$ (not q$)) :named @p_29)) :named @p_30)) :named @p_33)) :named @p_36)) :named @p_39))
(step t6 (cl (! (= @p_1 (! (or a$ b$ c$ d$) :named @p_3)) :named @p_2)) :rule ac_simp)
(step t7 (cl (not @p_2) (not @p_1) @p_3) :rule equiv_pos2)
(step t8 (cl @p_3) :rule th_resolution :premises (a0 t6 t7))
(step t9 (cl (= @p_4 false)) :rule and_simplify)
(step t10 (cl (= @p_5 (! (or a$ false) :named @p_6))) :rule cong :premises (t9))
(step t11 (cl (= @p_6 (! (or a$) :named @p_7))) :rule or_simplify)
(step t12 (cl (= @p_7 a$)) :rule or_simplify)
(step t13 (cl (= @p_5 a$)) :rule trans :premises (t10 t11 t12))
(step t14 (cl (= @p_8 (! (not a$) :named @p_10))) :rule cong :premises (t13))
(step t15 (cl (! (= @p_9 (! (or @p_10 b$) :named @p_12)) :named @p_11)) :rule cong :premises (t14))
(step t16 (cl (not @p_11) (not @p_9) @p_12) :rule equiv_pos2)
(step t17 (cl @p_12) :rule th_resolution :premises (a2 t15 t16))
(step t18 (cl (= @p_13 true)) :rule or_simplify)
(step t19 (cl (= @p_14 (! (and b$ true) :named @p_15))) :rule cong :premises (t18))
(step t20 (cl (= @p_15 (! (and b$) :named @p_16))) :rule and_simplify)
(step t21 (cl (= @p_16 b$)) :rule and_simplify)
(step t22 (cl (= @p_14 b$)) :rule trans :premises (t19 t20 t21))
(step t23 (cl (= @p_17 (! (not b$) :named @p_19))) :rule cong :premises (t22))
(step t24 (cl (! (= @p_18 (! (or @p_19 c$) :named @p_21)) :named @p_20)) :rule cong :premises (t23))
(step t25 (cl (not @p_20) (not @p_18) @p_21) :rule equiv_pos2)
(step t26 (cl @p_21) :rule th_resolution :premises (a3 t24 t25))
(step t27 (cl (= @p_22 (! (or d$) :named @p_23))) :rule or_simplify)
(step t28 (cl (= @p_23 d$)) :rule or_simplify)
(step t29 (cl (= @p_22 d$)) :rule trans :premises (t27 t28))
(step t30 (cl (= @p_24 (! (not d$) :named @p_26))) :rule cong :premises (t29))
(step t31 (cl (! (= @p_25 (! (or @p_26 c$) :named @p_28)) :named @p_27)) :rule cong :premises (t30))
(step t32 (cl (not @p_27) (not @p_25) @p_28) :rule equiv_pos2)
(step t33 (cl @p_28) :rule th_resolution :premises (a4 t31 t32))
(step t34 (cl (= @p_29 false)) :rule and_simplify)
(step t35 (cl (= @p_30 (! (or p$ false) :named @p_31))) :rule cong :premises (t34))
(step t36 (cl (= @p_31 (! (or p$) :named @p_32))) :rule or_simplify)
(step t37 (cl (= @p_32 p$)) :rule or_simplify)
(step t38 (cl (= @p_30 p$)) :rule trans :premises (t35 t36 t37))
(step t39 (cl (= @p_33 (! (and @p_34 p$) :named @p_35))) :rule cong :premises (t38))
(step t40 (cl (= @p_35 false)) :rule and_simplify)
(step t41 (cl (= @p_33 false)) :rule trans :premises (t39 t40))
(step t42 (cl (= @p_36 (! (or c$ false) :named @p_37))) :rule cong :premises (t41))
(step t43 (cl (= @p_37 (! (or c$) :named @p_38))) :rule or_simplify)
(step t44 (cl (= @p_38 c$)) :rule or_simplify)
(step t45 (cl (= @p_36 c$)) :rule trans :premises (t42 t43 t44))
(step t46 (cl (! (= @p_39 @p_40) :named @p_41)) :rule cong :premises (t45))
(step t47 (cl (! (not @p_41) :named @p_43) (! (not @p_39) :named @p_42) @p_40) :rule equiv_pos2)
(step t48 (cl (not @p_42) @p_36) :rule not_not)
(step t49 (cl @p_43 @p_36 @p_40) :rule th_resolution :premises (t48 t47))
(step t50 (cl @p_40) :rule th_resolution :premises (a5 t46 t49))
(step t51 (cl a$ b$ c$ d$) :rule or :premises (t8))
(step t52 (cl @p_10 b$) :rule or :premises (t17))
(step t53 (cl @p_19 c$) :rule or :premises (t26))
(step t54 (cl @p_26 c$) :rule or :premises (t33))
(step t55 (cl @p_19) :rule resolution :premises (t53 t50))
(step t56 (cl @p_26) :rule resolution :premises (t54 t50))
(step t57 (cl a$) :rule resolution :premises (t51 t55 t50 t56))
(step t58 (cl) :rule resolution :premises (t52 t55 t57))
a331481eed4f18a666baadda4e1010ca7a295ccf 38 0
unsat
(assume a0 (! (forall ((?v0 A$) (?v1 A$)) (! (= (! (symm_f$ ?v0 ?v1) :named @p_2) (! (symm_f$ ?v1 ?v0) :named @p_6)) :named @p_8)) :named @p_1))
(assume a1 (! (not (! (and (! (= a$ a$) :named @p_19) (! (= (symm_f$ a$ b$) (symm_f$ b$ a$)) :named @p_21)) :named @p_20)) :named @p_24))
(anchor :step t3 :args ((:= (?v0 A$) veriT_vr0) (:= (?v1 A$) veriT_vr1)))
(step t3.t1 (cl (! (= ?v0 veriT_vr0) :named @p_5)) :rule refl)
(step t3.t2 (cl (! (= ?v1 veriT_vr1) :named @p_4)) :rule refl)
(step t3.t3 (cl (= @p_2 (! (symm_f$ veriT_vr0 veriT_vr1) :named @p_3))) :rule cong :premises (t3.t1 t3.t2))
(step t3.t4 (cl @p_4) :rule refl)
(step t3.t5 (cl @p_5) :rule refl)
(step t3.t6 (cl (= @p_6 (! (symm_f$ veriT_vr1 veriT_vr0) :named @p_7))) :rule cong :premises (t3.t4 t3.t5))
(step t3.t7 (cl (= @p_8 (! (= @p_3 @p_7) :named @p_9))) :rule cong :premises (t3.t3 t3.t6))
(step t3 (cl (! (= @p_1 (! (forall ((veriT_vr0 A$) (veriT_vr1 A$)) @p_9) :named @p_11)) :named @p_10)) :rule bind)
(step t4 (cl (not @p_10) (not @p_1) @p_11) :rule equiv_pos2)
(step t5 (cl @p_11) :rule th_resolution :premises (a0 t3 t4))
(anchor :step t6 :args ((:= (veriT_vr0 A$) veriT_vr2) (:= (veriT_vr1 A$) veriT_vr3)))
(step t6.t1 (cl (! (= veriT_vr0 veriT_vr2) :named @p_14)) :rule refl)
(step t6.t2 (cl (! (= veriT_vr1 veriT_vr3) :named @p_13)) :rule refl)
(step t6.t3 (cl (= @p_3 (! (symm_f$ veriT_vr2 veriT_vr3) :named @p_12))) :rule cong :premises (t6.t1 t6.t2))
(step t6.t4 (cl @p_13) :rule refl)
(step t6.t5 (cl @p_14) :rule refl)
(step t6.t6 (cl (= @p_7 (! (symm_f$ veriT_vr3 veriT_vr2) :named @p_15))) :rule cong :premises (t6.t4 t6.t5))
(step t6.t7 (cl (= @p_9 (! (= @p_12 @p_15) :named @p_16))) :rule cong :premises (t6.t3 t6.t6))
(step t6 (cl (! (= @p_11 (! (forall ((veriT_vr2 A$) (veriT_vr3 A$)) @p_16) :named @p_18)) :named @p_17)) :rule bind)
(step t7 (cl (not @p_17) (not @p_11) @p_18) :rule equiv_pos2)
(step t8 (cl @p_18) :rule th_resolution :premises (t5 t6 t7))
(step t9 (cl (= @p_19 true)) :rule eq_simplify)
(step t10 (cl (= @p_20 (! (and true @p_21) :named @p_22))) :rule cong :premises (t9))
(step t11 (cl (= @p_22 (! (and @p_21) :named @p_23))) :rule and_simplify)
(step t12 (cl (= @p_23 @p_21)) :rule and_simplify)
(step t13 (cl (= @p_20 @p_21)) :rule trans :premises (t10 t11 t12))
(step t14 (cl (! (= @p_24 (! (not @p_21) :named @p_26)) :named @p_25)) :rule cong :premises (t13))
(step t15 (cl (! (not @p_25) :named @p_28) (! (not @p_24) :named @p_27) @p_26) :rule equiv_pos2)
(step t16 (cl (not @p_27) @p_20) :rule not_not)
(step t17 (cl @p_28 @p_20 @p_26) :rule th_resolution :premises (t16 t15))
(step t18 (cl @p_26) :rule th_resolution :premises (a1 t14 t17))
(step t19 (cl (or (! (not @p_18) :named @p_29) @p_21)) :rule forall_inst :args ((:= veriT_vr2 a$) (:= veriT_vr3 b$)))
(step t20 (cl @p_29 @p_21) :rule or :premises (t19))
(step t21 (cl) :rule resolution :premises (t20 t8 t18))
a5b152c08be1e0a4da353f094af8f11f36a16f52 333 0
unsat
(assume a0 (not x0$))
(assume a1 (not x30$))
(assume a2 (not x29$))
(assume a3 (not x59$))
(assume a4 (! (or x1$ (or x31$ x0$)) :named @p_57))
(assume a6 (! (or x3$ (or x33$ x2$)) :named @p_60))
(assume a7 (! (or x4$ (or x34$ x3$)) :named @p_63))
(assume a8 (or x35$ x4$))
(assume a9 (! (or x5$ (or x36$ x30$)) :named @p_66))
(assume a11 (! (or x7$ (or x38$ (or x6$ x32$))) :named @p_69))
(assume a13 (! (or x9$ (or x40$ (or x8$ x34$))) :named @p_72))
(assume a16 (! (or x11$ (or x43$ (or x10$ x37$))) :named @p_75))
(assume a18 (! (or x13$ (or x45$ (or x12$ x39$))) :named @p_78))
(assume a20 (! (or x47$ (or x14$ x41$)) :named @p_81))
(assume a21 (! (or x15$ (or x48$ x42$)) :named @p_84))
(assume a23 (! (or x17$ (or x50$ (or x16$ x44$))) :named @p_87))
(assume a25 (! (or x19$ (or x52$ (or x18$ x46$))) :named @p_90))
(assume a28 (! (or x21$ (or x55$ (or x20$ x49$))) :named @p_93))
(assume a30 (! (or x23$ (or x57$ (or x22$ x51$))) :named @p_96))
(assume a32 (! (or x59$ (or x24$ x53$)) :named @p_99))
(assume a33 (or x25$ x54$))
(assume a35 (! (or x27$ (or x26$ x56$)) :named @p_102))
(assume a37 (! (or x29$ (or x28$ x58$)) :named @p_105))
(assume a41 (or (! (not x2$) :named @p_1) (! (not x32$) :named @p_2)))
(assume a42 (or @p_1 (! (not x1$) :named @p_3)))
(assume a43 (or @p_2 @p_3))
(assume a47 (or (! (not x4$) :named @p_4) (! (not x34$) :named @p_5)))
(assume a48 (or @p_4 (! (not x3$) :named @p_6)))
(assume a49 (or @p_5 @p_6))
(assume a54 (or (! (not x6$) :named @p_7) (! (not x37$) :named @p_8)))
(assume a55 (or @p_7 (! (not x5$) :named @p_9)))
(assume a56 (or @p_7 (! (not x31$) :named @p_10)))
(assume a57 (or @p_8 @p_9))
(assume a58 (or @p_8 @p_10))
(assume a59 (or @p_9 @p_10))
(assume a63 (or (! (not x38$) :named @p_11) @p_7))
(assume a64 (or @p_11 @p_2))
(assume a66 (or (! (not x8$) :named @p_12) (! (not x39$) :named @p_13)))
(assume a67 (or @p_12 (! (not x7$) :named @p_14)))
(assume a68 (or @p_12 (! (not x33$) :named @p_15)))
(assume a69 (or @p_13 @p_14))
(assume a70 (or @p_13 @p_15))
(assume a71 (or @p_14 @p_15))
(assume a78 (or (! (not x41$) :named @p_16) (! (not x9$) :named @p_17)))
(assume a79 (or @p_16 (! (not x35$) :named @p_18)))
(assume a80 (or @p_17 @p_18))
(assume a81 (or (! (not x10$) :named @p_19) (! (not x42$) :named @p_20)))
(assume a82 (or @p_19 (! (not x36$) :named @p_21)))
(assume a83 (or @p_20 @p_21))
(assume a90 (or (! (not x12$) :named @p_22) (! (not x44$) :named @p_23)))
(assume a91 (or @p_22 (! (not x11$) :named @p_24)))
(assume a92 (or @p_22 @p_11))
(assume a93 (or @p_23 @p_24))
(assume a94 (or @p_23 @p_11))
(assume a95 (or @p_24 @p_11))
(assume a99 (or (! (not x45$) :named @p_25) @p_22))
(assume a100 (or @p_25 @p_13))
(assume a102 (or (! (not x14$) :named @p_26) (! (not x46$) :named @p_27)))
(assume a103 (or @p_26 (! (not x13$) :named @p_28)))
(assume a104 (or @p_26 (! (not x40$) :named @p_29)))
(assume a105 (or @p_27 @p_28))
(assume a106 (or @p_27 @p_29))
(assume a107 (or @p_28 @p_29))
(assume a113 (or (! (not x48$) :named @p_41) @p_20))
(assume a114 (or (! (not x16$) :named @p_30) (! (not x49$) :named @p_31)))
(assume a115 (or @p_30 (! (not x15$) :named @p_32)))
(assume a116 (or @p_30 (! (not x43$) :named @p_33)))
(assume a117 (or @p_31 @p_32))
(assume a118 (or @p_31 @p_33))
(assume a119 (or @p_32 @p_33))
(assume a126 (or (! (not x18$) :named @p_34) (! (not x51$) :named @p_35)))
(assume a127 (or @p_34 (! (not x17$) :named @p_36)))
(assume a128 (or @p_34 @p_25))
(assume a129 (or @p_35 @p_36))
(assume a130 (or @p_35 @p_25))
(assume a131 (or @p_36 @p_25))
(assume a134 (or (! (not x19$) :named @p_37) @p_27))
(assume a138 (or (! (not x53$) :named @p_38) @p_37))
(assume a139 (or @p_38 (! (not x47$) :named @p_39)))
(assume a140 (or @p_37 @p_39))
(assume a141 (or (! (not x20$) :named @p_40) (! (not x54$) :named @p_42)))
(assume a142 (or @p_40 @p_41))
(assume a143 (or @p_42 @p_41))
(assume a150 (or (! (not x22$) :named @p_43) (! (not x56$) :named @p_44)))
(assume a151 (or @p_43 (! (not x21$) :named @p_45)))
(assume a152 (or @p_43 (! (not x50$) :named @p_46)))
(assume a153 (or @p_44 @p_45))
(assume a154 (or @p_44 @p_46))
(assume a155 (or @p_45 @p_46))
(assume a162 (or (! (not x24$) :named @p_47) (! (not x58$) :named @p_48)))
(assume a163 (or @p_47 (! (not x23$) :named @p_49)))
(assume a164 (or @p_47 (! (not x52$) :named @p_50)))
(assume a165 (or @p_48 @p_49))
(assume a166 (or @p_48 @p_50))
(assume a167 (or @p_49 @p_50))
(assume a172 (or (! (not x26$) :named @p_51) (! (not x25$) :named @p_52)))
(assume a173 (or @p_51 (! (not x55$) :named @p_53)))
(assume a174 (or @p_52 @p_53))
(assume a178 (or (! (not x28$) :named @p_54) (! (not x27$) :named @p_55)))
(assume a179 (or @p_54 (! (not x57$) :named @p_56)))
(assume a180 (or @p_55 @p_56))
(step t102 (cl (! (= @p_57 (! (or x1$ x31$ x0$) :named @p_59)) :named @p_58)) :rule ac_simp)
(step t103 (cl (not @p_58) (not @p_57) @p_59) :rule equiv_pos2)
(step t104 (cl @p_59) :rule th_resolution :premises (a4 t102 t103))
(step t105 (cl (! (= @p_60 (! (or x3$ x33$ x2$) :named @p_62)) :named @p_61)) :rule ac_simp)
(step t106 (cl (not @p_61) (not @p_60) @p_62) :rule equiv_pos2)
(step t107 (cl @p_62) :rule th_resolution :premises (a6 t105 t106))
(step t108 (cl (! (= @p_63 (! (or x4$ x34$ x3$) :named @p_65)) :named @p_64)) :rule ac_simp)
(step t109 (cl (not @p_64) (not @p_63) @p_65) :rule equiv_pos2)
(step t110 (cl @p_65) :rule th_resolution :premises (a7 t108 t109))
(step t111 (cl (! (= @p_66 (! (or x5$ x36$ x30$) :named @p_68)) :named @p_67)) :rule ac_simp)
(step t112 (cl (not @p_67) (not @p_66) @p_68) :rule equiv_pos2)
(step t113 (cl @p_68) :rule th_resolution :premises (a9 t111 t112))
(step t114 (cl (! (= @p_69 (! (or x7$ x38$ x6$ x32$) :named @p_71)) :named @p_70)) :rule ac_simp)
(step t115 (cl (not @p_70) (not @p_69) @p_71) :rule equiv_pos2)
(step t116 (cl @p_71) :rule th_resolution :premises (a11 t114 t115))
(step t117 (cl (! (= @p_72 (! (or x9$ x40$ x8$ x34$) :named @p_74)) :named @p_73)) :rule ac_simp)
(step t118 (cl (not @p_73) (not @p_72) @p_74) :rule equiv_pos2)
(step t119 (cl @p_74) :rule th_resolution :premises (a13 t117 t118))
(step t120 (cl (! (= @p_75 (! (or x11$ x43$ x10$ x37$) :named @p_77)) :named @p_76)) :rule ac_simp)
(step t121 (cl (not @p_76) (not @p_75) @p_77) :rule equiv_pos2)
(step t122 (cl @p_77) :rule th_resolution :premises (a16 t120 t121))
(step t123 (cl (! (= @p_78 (! (or x13$ x45$ x12$ x39$) :named @p_80)) :named @p_79)) :rule ac_simp)
(step t124 (cl (not @p_79) (not @p_78) @p_80) :rule equiv_pos2)
(step t125 (cl @p_80) :rule th_resolution :premises (a18 t123 t124))
(step t126 (cl (! (= @p_81 (! (or x47$ x14$ x41$) :named @p_83)) :named @p_82)) :rule ac_simp)
(step t127 (cl (not @p_82) (not @p_81) @p_83) :rule equiv_pos2)
(step t128 (cl @p_83) :rule th_resolution :premises (a20 t126 t127))
(step t129 (cl (! (= @p_84 (! (or x15$ x48$ x42$) :named @p_86)) :named @p_85)) :rule ac_simp)
(step t130 (cl (not @p_85) (not @p_84) @p_86) :rule equiv_pos2)
(step t131 (cl @p_86) :rule th_resolution :premises (a21 t129 t130))
(step t132 (cl (! (= @p_87 (! (or x17$ x50$ x16$ x44$) :named @p_89)) :named @p_88)) :rule ac_simp)
(step t133 (cl (not @p_88) (not @p_87) @p_89) :rule equiv_pos2)
(step t134 (cl @p_89) :rule th_resolution :premises (a23 t132 t133))
(step t135 (cl (! (= @p_90 (! (or x19$ x52$ x18$ x46$) :named @p_92)) :named @p_91)) :rule ac_simp)
(step t136 (cl (not @p_91) (not @p_90) @p_92) :rule equiv_pos2)
(step t137 (cl @p_92) :rule th_resolution :premises (a25 t135 t136))
(step t138 (cl (! (= @p_93 (! (or x21$ x55$ x20$ x49$) :named @p_95)) :named @p_94)) :rule ac_simp)
(step t139 (cl (not @p_94) (not @p_93) @p_95) :rule equiv_pos2)
(step t140 (cl @p_95) :rule th_resolution :premises (a28 t138 t139))
(step t141 (cl (! (= @p_96 (! (or x23$ x57$ x22$ x51$) :named @p_98)) :named @p_97)) :rule ac_simp)
(step t142 (cl (not @p_97) (not @p_96) @p_98) :rule equiv_pos2)
(step t143 (cl @p_98) :rule th_resolution :premises (a30 t141 t142))
(step t144 (cl (! (= @p_99 (! (or x59$ x24$ x53$) :named @p_101)) :named @p_100)) :rule ac_simp)
(step t145 (cl (not @p_100) (not @p_99) @p_101) :rule equiv_pos2)
(step t146 (cl @p_101) :rule th_resolution :premises (a32 t144 t145))
(step t147 (cl (! (= @p_102 (! (or x27$ x26$ x56$) :named @p_104)) :named @p_103)) :rule ac_simp)
(step t148 (cl (not @p_103) (not @p_102) @p_104) :rule equiv_pos2)
(step t149 (cl @p_104) :rule th_resolution :premises (a35 t147 t148))
(step t150 (cl (! (= @p_105 (! (or x29$ x28$ x58$) :named @p_107)) :named @p_106)) :rule ac_simp)
(step t151 (cl (not @p_106) (not @p_105) @p_107) :rule equiv_pos2)
(step t152 (cl @p_107) :rule th_resolution :premises (a37 t150 t151))
(step t153 (cl x1$ x31$ x0$) :rule or :premises (t104))
(step t154 (cl x1$ x31$) :rule resolution :premises (t153 a0))
(step t155 (cl x3$ x33$ x2$) :rule or :premises (t107))
(step t156 (cl x4$ x34$ x3$) :rule or :premises (t110))
(step t157 (cl x35$ x4$) :rule or :premises (a8))
(step t158 (cl x5$ x36$ x30$) :rule or :premises (t113))
(step t159 (cl x5$ x36$) :rule resolution :premises (t158 a1))
(step t160 (cl x7$ x38$ x6$ x32$) :rule or :premises (t116))
(step t161 (cl x9$ x40$ x8$ x34$) :rule or :premises (t119))
(step t162 (cl x11$ x43$ x10$ x37$) :rule or :premises (t122))
(step t163 (cl x13$ x45$ x12$ x39$) :rule or :premises (t125))
(step t164 (cl x47$ x14$ x41$) :rule or :premises (t128))
(step t165 (cl x15$ x48$ x42$) :rule or :premises (t131))
(step t166 (cl x17$ x50$ x16$ x44$) :rule or :premises (t134))
(step t167 (cl x19$ x52$ x18$ x46$) :rule or :premises (t137))
(step t168 (cl x21$ x55$ x20$ x49$) :rule or :premises (t140))
(step t169 (cl x23$ x57$ x22$ x51$) :rule or :premises (t143))
(step t170 (cl x59$ x24$ x53$) :rule or :premises (t146))
(step t171 (cl x24$ x53$) :rule resolution :premises (t170 a3))
(step t172 (cl x25$ x54$) :rule or :premises (a33))
(step t173 (cl x27$ x26$ x56$) :rule or :premises (t149))
(step t174 (cl x29$ x28$ x58$) :rule or :premises (t152))
(step t175 (cl x28$ x58$) :rule resolution :premises (t174 a2))
(step t176 (cl @p_1 @p_2) :rule or :premises (a41))
(step t177 (cl @p_1 @p_3) :rule or :premises (a42))
(step t178 (cl @p_2 @p_3) :rule or :premises (a43))
(step t179 (cl @p_4 @p_5) :rule or :premises (a47))
(step t180 (cl @p_4 @p_6) :rule or :premises (a48))
(step t181 (cl @p_5 @p_6) :rule or :premises (a49))
(step t182 (cl @p_7 @p_8) :rule or :premises (a54))
(step t183 (cl @p_7 @p_9) :rule or :premises (a55))
(step t184 (cl @p_7 @p_10) :rule or :premises (a56))
(step t185 (cl @p_8 @p_9) :rule or :premises (a57))
(step t186 (cl @p_8 @p_10) :rule or :premises (a58))
(step t187 (cl @p_9 @p_10) :rule or :premises (a59))
(step t188 (cl @p_11 @p_7) :rule or :premises (a63))
(step t189 (cl @p_11 @p_2) :rule or :premises (a64))
(step t190 (cl @p_12 @p_13) :rule or :premises (a66))
(step t191 (cl @p_12 @p_14) :rule or :premises (a67))
(step t192 (cl @p_12 @p_15) :rule or :premises (a68))
(step t193 (cl @p_13 @p_14) :rule or :premises (a69))
(step t194 (cl @p_13 @p_15) :rule or :premises (a70))
(step t195 (cl @p_14 @p_15) :rule or :premises (a71))
(step t196 (cl @p_16 @p_17) :rule or :premises (a78))
(step t197 (cl @p_16 @p_18) :rule or :premises (a79))
(step t198 (cl @p_17 @p_18) :rule or :premises (a80))
(step t199 (cl @p_19 @p_20) :rule or :premises (a81))
(step t200 (cl @p_19 @p_21) :rule or :premises (a82))
(step t201 (cl @p_20 @p_21) :rule or :premises (a83))
(step t202 (cl @p_22 @p_23) :rule or :premises (a90))
(step t203 (cl @p_22 @p_24) :rule or :premises (a91))
(step t204 (cl @p_22 @p_11) :rule or :premises (a92))
(step t205 (cl @p_23 @p_24) :rule or :premises (a93))
(step t206 (cl @p_23 @p_11) :rule or :premises (a94))
(step t207 (cl @p_24 @p_11) :rule or :premises (a95))
(step t208 (cl @p_25 @p_22) :rule or :premises (a99))
(step t209 (cl @p_25 @p_13) :rule or :premises (a100))
(step t210 (cl @p_26 @p_27) :rule or :premises (a102))
(step t211 (cl @p_26 @p_28) :rule or :premises (a103))
(step t212 (cl @p_26 @p_29) :rule or :premises (a104))
(step t213 (cl @p_27 @p_28) :rule or :premises (a105))
(step t214 (cl @p_27 @p_29) :rule or :premises (a106))
(step t215 (cl @p_28 @p_29) :rule or :premises (a107))
(step t216 (cl @p_41 @p_20) :rule or :premises (a113))
(step t217 (cl @p_30 @p_31) :rule or :premises (a114))
(step t218 (cl @p_30 @p_32) :rule or :premises (a115))
(step t219 (cl @p_30 @p_33) :rule or :premises (a116))
(step t220 (cl @p_31 @p_32) :rule or :premises (a117))
(step t221 (cl @p_31 @p_33) :rule or :premises (a118))
(step t222 (cl @p_32 @p_33) :rule or :premises (a119))
(step t223 (cl @p_34 @p_35) :rule or :premises (a126))
(step t224 (cl @p_34 @p_36) :rule or :premises (a127))
(step t225 (cl @p_34 @p_25) :rule or :premises (a128))
(step t226 (cl @p_35 @p_36) :rule or :premises (a129))
(step t227 (cl @p_35 @p_25) :rule or :premises (a130))
(step t228 (cl @p_36 @p_25) :rule or :premises (a131))
(step t229 (cl @p_37 @p_27) :rule or :premises (a134))
(step t230 (cl @p_38 @p_37) :rule or :premises (a138))
(step t231 (cl @p_38 @p_39) :rule or :premises (a139))
(step t232 (cl @p_37 @p_39) :rule or :premises (a140))
(step t233 (cl @p_40 @p_42) :rule or :premises (a141))
(step t234 (cl @p_40 @p_41) :rule or :premises (a142))
(step t235 (cl @p_42 @p_41) :rule or :premises (a143))
(step t236 (cl @p_43 @p_44) :rule or :premises (a150))
(step t237 (cl @p_43 @p_45) :rule or :premises (a151))
(step t238 (cl @p_43 @p_46) :rule or :premises (a152))
(step t239 (cl @p_44 @p_45) :rule or :premises (a153))
(step t240 (cl @p_44 @p_46) :rule or :premises (a154))
(step t241 (cl @p_45 @p_46) :rule or :premises (a155))
(step t242 (cl @p_47 @p_48) :rule or :premises (a162))
(step t243 (cl @p_47 @p_49) :rule or :premises (a163))
(step t244 (cl @p_47 @p_50) :rule or :premises (a164))
(step t245 (cl @p_48 @p_49) :rule or :premises (a165))
(step t246 (cl @p_48 @p_50) :rule or :premises (a166))
(step t247 (cl @p_49 @p_50) :rule or :premises (a167))
(step t248 (cl @p_51 @p_52) :rule or :premises (a172))
(step t249 (cl @p_51 @p_53) :rule or :premises (a173))
(step t250 (cl @p_52 @p_53) :rule or :premises (a174))
(step t251 (cl @p_54 @p_55) :rule or :premises (a178))
(step t252 (cl @p_54 @p_56) :rule or :premises (a179))
(step t253 (cl @p_55 @p_56) :rule or :premises (a180))
(step t254 (cl x48$ x47$ @p_27) :rule resolution :premises (t222 t165 t162 t201 t200 t207 t159 t160 t187 t186 t184 t154 t177 t176 t155 t192 t191 t161 t180 t179 t157 t197 t196 t164 t214 t210))
(step t255 (cl x47$ x45$ x12$ x38$ @p_9) :rule resolution :premises (t196 t161 t164 t181 t215 t211 t155 t163 t195 t193 t191 t160 t178 t177 t154 t187 t183))
(step t256 (cl x47$ x45$ x17$ x50$ @p_32) :rule resolution :premises (t196 t161 t164 t181 t215 t211 t155 t163 t195 t193 t191 t160 t178 t177 t154 t186 t182 t162 t200 t159 t255 t206 t205 t202 t166 t222 t218))
(step t257 (cl x6$ x32$ x45$ x2$ x47$ @p_17) :rule resolution :premises (t204 t160 t163 t195 t194 t155 t180 t211 t157 t164 t198 t196))
(step t258 (cl x10$ x37$ x17$ x50$ @p_11) :rule resolution :premises (t219 t162 t166 t207 t206))
(step t259 (cl x50$ x47$ x48$ x19$ x52$) :rule resolution :premises (t219 t162 t166 t203 t202 t255 t258 t185 t159 t201 t199 t165 t256 t225 t224 t167 t254))
(step t260 (cl x47$ x38$ @p_9) :rule resolution :premises (t212 t161 t164 t198 t197 t157 t181 t180 t155 t195 t191 t160 t178 t177 t154 t187 t183))
(step t261 (cl x50$ x16$ x9$ x19$ x52$ x47$ @p_6) :rule resolution :premises (t202 t163 t166 t190 t225 t224 t161 t167 t212 t211 t210 t164 t197 t157 t181 t180))
(step t262 (cl x38$ x3$ x43$ x10$ x50$ x16$ x19$ x52$ @p_26) :rule resolution :premises (t176 t160 t155 t182 t194 t193 t162 t163 t205 t202 t166 t225 t224 t167 t211 t210))
(step t263 (cl x45$ x12$ x9$ x34$ @p_15) :rule resolution :premises (t215 t163 t161 t194 t192))
(step t264 (cl x45$ x12$ x9$ x34$ x38$ x3$) :rule resolution :premises (t215 t163 t161 t193 t191 t160 t184 t154 t177 t176 t155 t263))
(step t265 (cl x38$ x9$ x34$ x19$ x52$ x43$ x10$ x50$ x16$ @p_22) :rule resolution :premises (t191 t160 t161 t178 t214 t154 t167 t186 t182 t224 t162 t166 t203 t202))
(step t266 (cl x38$ x43$ x10$ x9$ x50$ x16$ x19$ x52$ x47$) :rule resolution :premises (t176 t155 t160 t182 t192 t191 t162 t161 t205 t214 t166 t167 t228 t225 t264 t265 t179 t157 t197 t164 t262 t261))
(step t267 (cl x38$ x43$ x50$ x16$ x19$ x52$ x47$) :rule resolution :premises (t180 t262 t157 t164 t198 t196 t266 t200 t159 t260))
(step t268 (cl x47$ x19$ x52$ @p_44) :rule resolution :premises (t179 t161 t157 t190 t197 t196 t163 t164 t214 t213 t210 t167 t228 t224 t166 t206 t204 t267 t221 t217 t168 t250 t172 t235 t234 t259 t240 t239))
(step t269 (cl x56$ x23$ x11$ @p_11 x12$ x19$ x52$ x47$ @p_5) :rule resolution :premises (t248 t172 t173 t235 t253 t165 t169 t222 t238 t162 t258 t201 t200 t159 t187 t186 t154 t177 t155 t194 t163 t225 t224 t223 t167 t211 t210 t164 t197 t157 t181 t179))
(step t270 (cl x9$ x34$ x45$ x12$ @p_26) :rule resolution :premises (t190 t161 t163 t212 t211))
(step t271 (cl x44$ x23$ x56$ x11$ @p_10) :rule resolution :premises (t226 t166 t169 t241 t237 t253 t168 t173 t250 t248 t172 t235 t234 t165 t222 t221 t219 t162 t201 t200 t159 t187 t186))
(step t272 (cl x47$ x2$ x9$ x34$ x45$ x12$) :rule resolution :premises (t157 t197 t180 t164 t155 t270 t263))
(step t273 (cl x2$ x9$ x34$ x47$ x19$ x52$ x12$) :rule resolution :premises (t180 t155 t157 t192 t197 t161 t164 t214 t210 t167 t225 t272))
(step t274 (cl x19$ x52$ x47$ x23$ x56$ @p_11) :rule resolution :premises (t167 t210 t225 t164 t257 t196 t273 t177 t154 t271 t269 t207 t206 t204 t189 t188))
(step t275 (cl x38$ x12$ x19$ x52$ x47$ @p_17) :rule resolution :premises (t184 t154 t160 t177 t176 t155 t194 t193 t163 t225 t167 t180 t211 t210 t157 t164 t198 t196))
(step t276 (cl x38$ x45$ x12$ x9$ @p_26) :rule resolution :premises (t184 t154 t160 t177 t176 t155 t194 t193 t181 t163 t270 t211))
(step t277 (cl x45$ x12$ x9$ x38$ x47$) :rule resolution :premises (t264 t180 t179 t157 t197 t164 t276))
(step t278 (cl x38$ x47$ x19$ x52$ x12$) :rule resolution :premises (t184 t154 t160 t191 t177 t176 t161 t273 t179 t157 t197 t164 t214 t210 t167 t225 t277 t275))
(step t279 (cl x42$ x44$ x11$ x10$ x19$ x52$ x38$ x32$ x9$ x2$ @p_4) :rule resolution :premises (t250 t172 t168 t235 t234 t241 t165 t166 t222 t221 t219 t224 t162 t167 t182 t214 t160 t161 t195 t192 t155 t180 t179))
(step t280 (cl x42$ x9$ x19$ x52$ x47$ x11$ x10$ x38$ x32$ x40$ x34$ x4$) :rule resolution :premises (t250 t172 t168 t235 t234 t241 t165 t261 t222 t221 t219 t162 t182 t160 t191 t161 t156))
(step t281 (cl x42$ x44$ x11$ x10$ x38$ x32$ x2$ x9$ x19$ x52$ x47$) :rule resolution :premises (t250 t172 t168 t235 t234 t241 t165 t166 t222 t221 t219 t162 t182 t160 t195 t155 t181 t280 t224 t167 t212 t210 t164 t197 t157 t279))
(step t282 (cl @p_48) :rule resolution :premises (t250 t172 t168 t235 t234 t241 t165 t166 t224 t222 t221 t219 t167 t162 t210 t182 t164 t257 t196 t281 t178 t177 t154 t271 t208 t203 t202 t278 t201 t200 t159 t260 t274 t268 t231 t230 t171 t246 t245 t242))
(step t283 (cl x28$) :rule resolution :premises (t175 t282))
(step t284 (cl @p_55) :rule resolution :premises (t251 t283))
(step t285 (cl @p_56) :rule resolution :premises (t252 t283))
(step t286 (cl x42$ x47$ x19$ x52$) :rule resolution :premises (t168 t220 t241 t165 t259 t235 t233 t172 t249 t248 t173 t268 t284))
(step t287 (cl x42$ @p_33) :rule resolution :premises (t239 t168 t173 t250 t248 t172 t235 t234 t165 t222 t221 t284))
(step t288 (cl x47$ @p_17 x43$ x10$ @p_22) :rule resolution :premises (t257 t178 t177 t154 t186 t182 t162 t208 t203))
(step t289 (cl x38$ x3$ @p_13) :rule resolution :premises (t184 t154 t160 t177 t176 t155 t194 t193))
(step t290 (cl x17$ x44$ @p_43) :rule resolution :premises (t233 t168 t172 t217 t249 t248 t166 t173 t238 t237 t236 t284))
(step t291 (cl x18$ x46$ @p_49) :rule resolution :premises (t230 t167 t171 t247 t243))
(step t292 (cl x39$ x47$ @p_17 x38$ x41$) :rule resolution :premises (t220 t165 t168 t235 t233 t172 t249 t248 t173 t237 t236 t169 t291 t227 t225 t163 t288 t287 t201 t200 t159 t211 t210 t260 t164 t284 t285))
(step t293 (cl x23$ @p_25) :rule resolution :premises (t185 t159 t162 t201 t199 t165 t221 t220 t168 t235 t233 t172 t249 t248 t205 t173 t290 t237 t236 t169 t228 t227 t284 t285))
(step t294 (cl x23$ @p_34) :rule resolution :premises (t185 t159 t162 t201 t199 t165 t221 t220 t168 t235 t233 t172 t249 t248 t205 t173 t290 t237 t236 t169 t224 t223 t284 t285))
(step t295 (cl x38$ x3$ @p_8) :rule resolution :premises (t195 t160 t155 t178 t177 t154 t186 t182))
(step t296 (cl x38$ x3$ @p_9) :rule resolution :premises (t195 t160 t155 t178 t177 t154 t187 t183))
(step t297 (cl x38$ x3$ @p_17 x41$) :rule resolution :premises (t287 t162 t201 t200 t159 t296 t295 t203 t163 t213 t167 t294 t293 t244 t243 t171 t232 t231 t292 t289))
(step t298 (cl x12$ x39$ @p_39) :rule resolution :premises (t213 t167 t163 t294 t293 t244 t243 t171 t232 t231))
(step t299 (cl x6$ x32$ @p_17 x12$ x3$ @p_20) :rule resolution :premises (t291 t293 t225 t257 t254 t298 t194 t155 t177 t154 t187 t159 t216 t201))
(step t300 (cl x46$ @p_25) :rule resolution :premises (t291 t293 t225))
(step t301 (cl x11$ x43$ @p_10) :rule resolution :premises (t200 t159 t162 t187 t186))
(step t302 (cl @p_17) :rule resolution :premises (t300 t210 t257 t164 t298 t194 t155 t177 t154 t301 t287 t299 t207 t204 t189 t188 t297 t180 t157 t198 t196))
(step t303 (cl @p_25) :rule resolution :premises (t216 t286 t254 t229 t247 t298 t300 t293 t209 t208))
(step t304 (cl x12$ x47$ x2$) :rule resolution :premises (t211 t163 t164 t194 t197 t155 t157 t181 t179 t272 t303 t302))
(step t305 (cl x12$ x47$) :rule resolution :premises (t201 t287 t159 t301 t187 t154 t177 t304 t207 t277 t302 t303))
(step t306 (cl x47$) :rule resolution :premises (t212 t164 t161 t197 t191 t157 t160 t181 t180 t178 t295 t182 t154 t162 t301 t287 t201 t200 t159 t260 t204 t203 t305 t302))
(step t307 (cl @p_38) :rule resolution :premises (t231 t306))
(step t308 (cl @p_37) :rule resolution :premises (t232 t306))
(step t309 (cl x24$) :rule resolution :premises (t171 t307))
(step t310 (cl @p_49) :rule resolution :premises (t243 t309))
(step t311 (cl @p_50) :rule resolution :premises (t244 t309))
(step t312 (cl @p_34) :rule resolution :premises (t294 t310))
(step t313 (cl x46$) :rule resolution :premises (t167 t312 t308 t311))
(step t314 (cl @p_29) :rule resolution :premises (t214 t313))
(step t315 (cl x11$ x43$ @p_7) :rule resolution :premises (t200 t159 t162 t183 t182))
(step t316 (cl x38$ x11$ x43$) :rule resolution :premises (t181 t155 t161 t195 t191 t160 t315 t178 t177 t154 t301 t302 t314))
(step t317 (cl @p_22) :rule resolution :premises (t191 t160 t161 t178 t181 t154 t296 t187 t183 t159 t201 t287 t316 t204 t203 t302 t314))
(step t318 (cl x39$) :rule resolution :premises (t298 t317 t306))
(step t319 (cl @p_12) :rule resolution :premises (t190 t318))
(step t320 (cl @p_15) :rule resolution :premises (t194 t318))
(step t321 (cl x34$) :rule resolution :premises (t161 t319 t302 t314))
(step t322 (cl @p_6) :rule resolution :premises (t181 t321))
(step t323 (cl x2$) :rule resolution :premises (t155 t322 t320))
(step t324 (cl x38$) :rule resolution :premises (t289 t322 t318))
(step t325 (cl @p_3) :rule resolution :premises (t177 t323))
(step t326 (cl @p_24) :rule resolution :premises (t207 t324))
(step t327 (cl x31$) :rule resolution :premises (t154 t325))
(step t328 (cl @p_9) :rule resolution :premises (t187 t327))
(step t329 (cl x43$) :rule resolution :premises (t301 t327 t326))
(step t330 (cl x36$) :rule resolution :premises (t159 t328))
(step t331 (cl x42$) :rule resolution :premises (t287 t329))
(step t332 (cl) :rule resolution :premises (t201 t330 t331))
a73b15b00e6e103b31fc48e963d878be9038a417 64 0
unsat
(define-fun veriT_sk0 () Int (! (choice ((veriT_vr2 Int)) (not (! (=> (! (p$ veriT_vr2) :named @p_20) (! (forall ((veriT_vr3 Int)) (! (or @p_20 (! (p$ veriT_vr3) :named @p_24)) :named @p_25)) :named @p_21)) :named @p_26))) :named @p_33))
(define-fun veriT_sk1 () Int (! (choice ((veriT_vr3 Int)) (not (or (p$ @p_33) @p_24))) :named @p_37))
(assume a0 (! (not (! (forall ((?v0 Int)) (! (=> (! (p$ ?v0) :named @p_1) (! (forall ((?v1 Int)) (! (or @p_1 (! (p$ ?v1) :named @p_8)) :named @p_10)) :named @p_4)) :named @p_12)) :named @p_2)) :named @p_14))
(anchor :step t2 :args ((:= (?v0 Int) veriT_vr0)))
(step t2.t1 (cl (! (= ?v0 veriT_vr0) :named @p_6)) :rule refl)
(step t2.t2 (cl (! (= @p_1 (! (p$ veriT_vr0) :named @p_3)) :named @p_7)) :rule cong :premises (t2.t1))
(anchor :step t2.t3 :args ((:= (?v1 Int) veriT_vr1)))
(step t2.t3.t1 (cl @p_6) :rule refl)
(step t2.t3.t2 (cl @p_7) :rule cong :premises (t2.t3.t1))
(step t2.t3.t3 (cl (= ?v1 veriT_vr1)) :rule refl)
(step t2.t3.t4 (cl (= @p_8 (! (p$ veriT_vr1) :named @p_9))) :rule cong :premises (t2.t3.t3))
(step t2.t3.t5 (cl (= @p_10 (! (or @p_3 @p_9) :named @p_11))) :rule cong :premises (t2.t3.t2 t2.t3.t4))
(step t2.t3 (cl (= @p_4 (! (forall ((veriT_vr1 Int)) @p_11) :named @p_5))) :rule bind)
(step t2.t4 (cl (= @p_12 (! (=> @p_3 @p_5) :named @p_13))) :rule cong :premises (t2.t2 t2.t3))
(step t2 (cl (= @p_2 (! (forall ((veriT_vr0 Int)) @p_13) :named @p_15))) :rule bind)
(step t3 (cl (! (= @p_14 (! (not @p_15) :named @p_17)) :named @p_16)) :rule cong :premises (t2))
(step t4 (cl (! (not @p_16) :named @p_19) (! (not @p_14) :named @p_18) @p_17) :rule equiv_pos2)
(step t5 (cl (not @p_18) @p_2) :rule not_not)
(step t6 (cl @p_19 @p_2 @p_17) :rule th_resolution :premises (t5 t4))
(step t7 (cl @p_17) :rule th_resolution :premises (a0 t3 t6))
(anchor :step t8 :args ((:= (veriT_vr0 Int) veriT_vr2)))
(step t8.t1 (cl (! (= veriT_vr0 veriT_vr2) :named @p_22)) :rule refl)
(step t8.t2 (cl (! (= @p_3 @p_20) :named @p_23)) :rule cong :premises (t8.t1))
(anchor :step t8.t3 :args ((:= (veriT_vr1 Int) veriT_vr3)))
(step t8.t3.t1 (cl @p_22) :rule refl)
(step t8.t3.t2 (cl @p_23) :rule cong :premises (t8.t3.t1))
(step t8.t3.t3 (cl (= veriT_vr1 veriT_vr3)) :rule refl)
(step t8.t3.t4 (cl (= @p_9 @p_24)) :rule cong :premises (t8.t3.t3))
(step t8.t3.t5 (cl (= @p_11 @p_25)) :rule cong :premises (t8.t3.t2 t8.t3.t4))
(step t8.t3 (cl (= @p_5 @p_21)) :rule bind)
(step t8.t4 (cl (= @p_13 @p_26)) :rule cong :premises (t8.t2 t8.t3))
(step t8 (cl (= @p_15 (! (forall ((veriT_vr2 Int)) @p_26) :named @p_27))) :rule bind)
(step t9 (cl (! (= @p_17 (! (not @p_27) :named @p_29)) :named @p_28)) :rule cong :premises (t8))
(step t10 (cl (! (not @p_28) :named @p_31) (! (not @p_17) :named @p_30) @p_29) :rule equiv_pos2)
(step t11 (cl (not @p_30) @p_15) :rule not_not)
(step t12 (cl @p_31 @p_15 @p_29) :rule th_resolution :premises (t11 t10))
(step t13 (cl @p_29) :rule th_resolution :premises (t7 t9 t12))
(anchor :step t14 :args ((:= (veriT_vr2 Int) veriT_sk0)))
(step t14.t1 (cl (! (= veriT_vr2 veriT_sk0) :named @p_35)) :rule refl)
(step t14.t2 (cl (! (= @p_20 (! (p$ veriT_sk0) :named @p_32)) :named @p_36)) :rule cong :premises (t14.t1))
(anchor :step t14.t3 :args ((:= (veriT_vr3 Int) veriT_sk1)))
(step t14.t3.t1 (cl @p_35) :rule refl)
(step t14.t3.t2 (cl @p_36) :rule cong :premises (t14.t3.t1))
(step t14.t3.t3 (cl (= veriT_vr3 veriT_sk1)) :rule refl)
(step t14.t3.t4 (cl (= @p_24 (! (p$ veriT_sk1) :named @p_38))) :rule cong :premises (t14.t3.t3))
(step t14.t3.t5 (cl (= @p_25 (! (or @p_32 @p_38) :named @p_34))) :rule cong :premises (t14.t3.t2 t14.t3.t4))
(step t14.t3 (cl (= @p_21 @p_34)) :rule sko_forall)
(step t14.t4 (cl (= @p_26 (! (=> @p_32 @p_34) :named @p_39))) :rule cong :premises (t14.t2 t14.t3))
(step t14 (cl (= @p_27 @p_39)) :rule sko_forall)
(step t15 (cl (! (= @p_29 (! (not @p_39) :named @p_41)) :named @p_40)) :rule cong :premises (t14))
(step t16 (cl (! (not @p_40) :named @p_43) (! (not @p_29) :named @p_42) @p_41) :rule equiv_pos2)
(step t17 (cl (not @p_42) @p_27) :rule not_not)
(step t18 (cl @p_43 @p_27 @p_41) :rule th_resolution :premises (t17 t16))
(step t19 (cl @p_41) :rule th_resolution :premises (t13 t15 t18))
(step t20 (cl (! (= @p_41 (! (and @p_32 (! (not @p_34) :named @p_48)) :named @p_45)) :named @p_44)) :rule bool_simplify)
(step t21 (cl (! (not @p_44) :named @p_47) (! (not @p_41) :named @p_46) @p_45) :rule equiv_pos2)
(step t22 (cl (not @p_46) @p_39) :rule not_not)
(step t23 (cl @p_47 @p_39 @p_45) :rule th_resolution :premises (t22 t21))
(step t24 (cl @p_45) :rule th_resolution :premises (t19 t20 t23))
(step t25 (cl @p_32) :rule and :premises (t24))
(step t26 (cl @p_48) :rule and :premises (t24))
(step t27 (cl (not @p_32)) :rule not_or :premises (t26))
(step t28 (cl) :rule resolution :premises (t27 t25))
9024ca3fa3536be727200e6a5ffc1df778e7e505 155 0
unsat
(define-fun veriT_sk0 () A$ (! (choice ((veriT_vr3 A$)) (! (ite x$ (! (p$ true veriT_vr3) :named @p_48) (! (p$ false veriT_vr3) :named @p_50)) :named @p_51)) :named @p_62))
(assume a0 (forall ((?v0 Bool) (?v1 A$)) (= (p$ ?v0 ?v1) ?v0)))
(assume a1 (not (= (exists ((?v0 A$)) (p$ x$ ?v0)) (p$ x$ c$))))
(step t3 (cl (! (forall ((?v1 A$)) (! (and (! (= (! (p$ false ?v1) :named @p_2) false) :named @p_4) (! (= (! (p$ true ?v1) :named @p_7) true) :named @p_9)) :named @p_11)) :named @p_1)) :rule bfun_elim :premises (a0))
(step t4 (cl (! (not (! (= (! (exists ((?v0 A$)) (! (ite x$ (! (p$ true ?v0) :named @p_27) (! (p$ false ?v0) :named @p_30)) :named @p_32)) :named @p_26) (! (ite x$ (! (p$ true c$) :named @p_91) (! (p$ false c$) :named @p_93)) :named @p_36)) :named @p_34)) :named @p_37)) :rule bfun_elim :premises (a1))
(anchor :step t5 :args ((:= (?v1 A$) veriT_vr0)))
(step t5.t1 (cl (! (= ?v1 veriT_vr0) :named @p_6)) :rule refl)
(step t5.t2 (cl (= @p_2 (! (p$ false veriT_vr0) :named @p_3))) :rule cong :premises (t5.t1))
(step t5.t3 (cl (= @p_4 (! (= @p_3 false) :named @p_5))) :rule cong :premises (t5.t2))
(step t5.t4 (cl @p_6) :rule refl)
(step t5.t5 (cl (= @p_7 (! (p$ true veriT_vr0) :named @p_8))) :rule cong :premises (t5.t4))
(step t5.t6 (cl (= @p_9 (! (= @p_8 true) :named @p_10))) :rule cong :premises (t5.t5))
(step t5.t7 (cl (= @p_11 (! (and @p_5 @p_10) :named @p_12))) :rule cong :premises (t5.t3 t5.t6))
(step t5 (cl (! (= @p_1 (! (forall ((veriT_vr0 A$)) @p_12) :named @p_14)) :named @p_13)) :rule bind)
(step t6 (cl (not @p_13) (not @p_1) @p_14) :rule equiv_pos2)
(step t7 (cl @p_14) :rule th_resolution :premises (t3 t5 t6))
(anchor :step t8 :args ((veriT_vr0 A$)))
(step t8.t1 (cl (= @p_5 (! (not @p_3) :named @p_15))) :rule equiv_simplify)
(step t8.t2 (cl (= @p_10 @p_8)) :rule equiv_simplify)
(step t8.t3 (cl (= @p_12 (! (and @p_15 @p_8) :named @p_16))) :rule cong :premises (t8.t1 t8.t2))
(step t8 (cl (! (= @p_14 (! (forall ((veriT_vr0 A$)) @p_16) :named @p_18)) :named @p_17)) :rule bind)
(step t9 (cl (not @p_17) (not @p_14) @p_18) :rule equiv_pos2)
(step t10 (cl @p_18) :rule th_resolution :premises (t7 t8 t9))
(anchor :step t11 :args ((:= (veriT_vr0 A$) veriT_vr1)))
(step t11.t1 (cl (! (= veriT_vr0 veriT_vr1) :named @p_21)) :rule refl)
(step t11.t2 (cl (= @p_3 (! (p$ false veriT_vr1) :named @p_19))) :rule cong :premises (t11.t1))
(step t11.t3 (cl (= @p_15 (! (not @p_19) :named @p_20))) :rule cong :premises (t11.t2))
(step t11.t4 (cl @p_21) :rule refl)
(step t11.t5 (cl (= @p_8 (! (p$ true veriT_vr1) :named @p_22))) :rule cong :premises (t11.t4))
(step t11.t6 (cl (= @p_16 (! (and @p_20 @p_22) :named @p_23))) :rule cong :premises (t11.t3 t11.t5))
(step t11 (cl (! (= @p_18 (! (forall ((veriT_vr1 A$)) @p_23) :named @p_25)) :named @p_24)) :rule bind)
(step t12 (cl (not @p_24) (not @p_18) @p_25) :rule equiv_pos2)
(step t13 (cl @p_25) :rule th_resolution :premises (t10 t11 t12))
(anchor :step t14 :args ((:= (?v0 A$) veriT_vr2)))
(step t14.t1 (cl (! (= ?v0 veriT_vr2) :named @p_29)) :rule refl)
(step t14.t2 (cl (= @p_27 (! (p$ true veriT_vr2) :named @p_28))) :rule cong :premises (t14.t1))
(step t14.t3 (cl @p_29) :rule refl)
(step t14.t4 (cl (= @p_30 (! (p$ false veriT_vr2) :named @p_31))) :rule cong :premises (t14.t3))
(step t14.t5 (cl (= @p_32 (! (ite x$ @p_28 @p_31) :named @p_33))) :rule cong :premises (t14.t2 t14.t4))
(step t14 (cl (= @p_26 (! (exists ((veriT_vr2 A$)) @p_33) :named @p_35))) :rule bind)
(step t15 (cl (= @p_34 (! (= @p_35 @p_36) :named @p_38))) :rule cong :premises (t14))
(step t16 (cl (! (= @p_37 (! (not @p_38) :named @p_40)) :named @p_39)) :rule cong :premises (t15))
(step t17 (cl (! (not @p_39) :named @p_42) (! (not @p_37) :named @p_41) @p_40) :rule equiv_pos2)
(step t18 (cl (not @p_41) @p_34) :rule not_not)
(step t19 (cl @p_42 @p_34 @p_40) :rule th_resolution :premises (t18 t17))
(step t20 (cl @p_40) :rule th_resolution :premises (t4 t16 t19))
(step t21 (cl (= @p_38 (! (and (! (=> @p_35 @p_36) :named @p_52) (! (=> @p_36 @p_35) :named @p_54)) :named @p_43))) :rule connective_def)
(step t22 (cl (! (= @p_40 (! (not @p_43) :named @p_45)) :named @p_44)) :rule cong :premises (t21))
(step t23 (cl (! (not @p_44) :named @p_47) (! (not @p_40) :named @p_46) @p_45) :rule equiv_pos2)
(step t24 (cl (not @p_46) @p_38) :rule not_not)
(step t25 (cl @p_47 @p_38 @p_45) :rule th_resolution :premises (t24 t23))
(step t26 (cl @p_45) :rule th_resolution :premises (t20 t22 t25))
(anchor :step t27 :args ((:= (veriT_vr2 A$) veriT_vr3)))
(step t27.t1 (cl (! (= veriT_vr2 veriT_vr3) :named @p_49)) :rule refl)
(step t27.t2 (cl (= @p_28 @p_48)) :rule cong :premises (t27.t1))
(step t27.t3 (cl @p_49) :rule refl)
(step t27.t4 (cl (= @p_31 @p_50)) :rule cong :premises (t27.t3))
(step t27.t5 (cl (= @p_33 @p_51)) :rule cong :premises (t27.t2 t27.t4))
(step t27 (cl (= @p_35 (! (exists ((veriT_vr3 A$)) @p_51) :named @p_53))) :rule bind)
(step t28 (cl (= @p_52 (! (=> @p_53 @p_36) :named @p_55))) :rule cong :premises (t27))
(step t29 (cl (= @p_54 (! (=> @p_36 @p_53) :named @p_56))) :rule cong :premises (t27))
(step t30 (cl (= @p_43 (! (and @p_55 @p_56) :named @p_57))) :rule cong :premises (t28 t29))
(step t31 (cl (! (= @p_45 (! (not @p_57) :named @p_59)) :named @p_58)) :rule cong :premises (t30))
(step t32 (cl (! (not @p_58) :named @p_61) (! (not @p_45) :named @p_60) @p_59) :rule equiv_pos2)
(step t33 (cl (not @p_60) @p_43) :rule not_not)
(step t34 (cl @p_61 @p_43 @p_59) :rule th_resolution :premises (t33 t32))
(step t35 (cl @p_59) :rule th_resolution :premises (t26 t31 t34))
(anchor :step t36 :args ((:= (veriT_vr3 A$) veriT_sk0)))
(step t36.t1 (cl (! (= veriT_vr3 veriT_sk0) :named @p_64)) :rule refl)
(step t36.t2 (cl (= @p_48 (! (p$ true veriT_sk0) :named @p_63))) :rule cong :premises (t36.t1))
(step t36.t3 (cl @p_64) :rule refl)
(step t36.t4 (cl (= @p_50 (! (p$ false veriT_sk0) :named @p_65))) :rule cong :premises (t36.t3))
(step t36.t5 (cl (= @p_51 (! (ite x$ @p_63 @p_65) :named @p_66))) :rule cong :premises (t36.t2 t36.t4))
(step t36 (cl (= @p_53 @p_66)) :rule sko_ex)
(step t37 (cl (= @p_55 (! (=> @p_66 @p_36) :named @p_67))) :rule cong :premises (t36))
(step t38 (cl (= @p_57 (! (and @p_67 @p_56) :named @p_68))) :rule cong :premises (t37))
(step t39 (cl (! (= @p_59 (! (not @p_68) :named @p_70)) :named @p_69)) :rule cong :premises (t38))
(step t40 (cl (! (not @p_69) :named @p_72) (! (not @p_59) :named @p_71) @p_70) :rule equiv_pos2)
(step t41 (cl (not @p_71) @p_57) :rule not_not)
(step t42 (cl @p_72 @p_57 @p_70) :rule th_resolution :premises (t41 t40))
(step t43 (cl @p_70) :rule th_resolution :premises (t35 t39 t42))
(anchor :step t44 :args ((:= (veriT_vr3 A$) veriT_vr4)))
(step t44.t1 (cl (! (= veriT_vr3 veriT_vr4) :named @p_74)) :rule refl)
(step t44.t2 (cl (= @p_48 (! (p$ true veriT_vr4) :named @p_73))) :rule cong :premises (t44.t1))
(step t44.t3 (cl @p_74) :rule refl)
(step t44.t4 (cl (= @p_50 (! (p$ false veriT_vr4) :named @p_75))) :rule cong :premises (t44.t3))
(step t44.t5 (cl (= @p_51 (! (ite x$ @p_73 @p_75) :named @p_76))) :rule cong :premises (t44.t2 t44.t4))
(step t44 (cl (= @p_53 (! (exists ((veriT_vr4 A$)) @p_76) :named @p_77))) :rule bind)
(step t45 (cl (= @p_56 (! (=> @p_36 @p_77) :named @p_78))) :rule cong :premises (t44))
(step t46 (cl (= @p_68 (! (and @p_67 @p_78) :named @p_79))) :rule cong :premises (t45))
(step t47 (cl (! (= @p_70 (! (not @p_79) :named @p_81)) :named @p_80)) :rule cong :premises (t46))
(step t48 (cl (! (not @p_80) :named @p_83) (! (not @p_70) :named @p_82) @p_81) :rule equiv_pos2)
(step t49 (cl (not @p_82) @p_68) :rule not_not)
(step t50 (cl @p_83 @p_68 @p_81) :rule th_resolution :premises (t49 t48))
(step t51 (cl @p_81) :rule th_resolution :premises (t43 t47 t50))
(step t52 (cl (= @p_77 (! (not (! (forall ((veriT_vr4 A$)) (not @p_76)) :named @p_95)) :named @p_84))) :rule connective_def)
(step t53 (cl (= @p_78 (! (=> @p_36 @p_84) :named @p_85))) :rule cong :premises (t52))
(step t54 (cl (= @p_79 (! (and @p_67 @p_85) :named @p_86))) :rule cong :premises (t53))
(step t55 (cl (! (= @p_81 (! (not @p_86) :named @p_88)) :named @p_87)) :rule cong :premises (t54))
(step t56 (cl (! (not @p_87) :named @p_90) (! (not @p_81) :named @p_89) @p_88) :rule equiv_pos2)
(step t57 (cl (not @p_89) @p_79) :rule not_not)
(step t58 (cl @p_90 @p_79 @p_88) :rule th_resolution :premises (t57 t56))
(step t59 (cl @p_88) :rule th_resolution :premises (t51 t55 t58))
(step t60 (cl (not @p_66) x$ @p_65) :rule ite_pos1)
(step t61 (cl @p_67 @p_66) :rule implies_neg1)
(step t62 (cl @p_36 (not x$) (! (not @p_91) :named @p_109)) :rule ite_neg2)
(step t63 (cl @p_67 (! (not @p_36) :named @p_92)) :rule implies_neg2)
(step t64 (cl @p_92 x$ @p_93) :rule ite_pos1)
(step t65 (cl @p_85 @p_36) :rule implies_neg1)
(step t66 (cl @p_85 (! (not @p_84) :named @p_94)) :rule implies_neg2)
(step t67 (cl (not @p_94) @p_95) :rule not_not)
(step t68 (cl @p_85 @p_95) :rule th_resolution :premises (t67 t66))
(step t69 (cl (not @p_67) (! (not @p_85) :named @p_110)) :rule not_and :premises (t59))
(step t70 (cl (or (! (not @p_25) :named @p_96) (! (forall ((veriT_vr1 A$)) @p_20) :named @p_97))) :rule qnt_cnf)
(step t71 (cl (or @p_96 (! (forall ((veriT_vr1 A$)) @p_22) :named @p_106))) :rule qnt_cnf)
(step t72 (cl @p_96 @p_97) :rule or :premises (t70))
(step t73 (cl (or (! (not @p_97) :named @p_98) (! (not @p_65) :named @p_99))) :rule forall_inst :args ((:= veriT_vr1 veriT_sk0)))
(step t74 (cl @p_98 @p_99) :rule or :premises (t73))
(step t75 (cl (! (or @p_96 @p_99) :named @p_101) (! (not @p_96) :named @p_100)) :rule or_neg)
(step t76 (cl (not @p_100) @p_25) :rule not_not)
(step t77 (cl @p_101 @p_25) :rule th_resolution :premises (t76 t75))
(step t78 (cl @p_101 (! (not @p_99) :named @p_102)) :rule or_neg)
(step t79 (cl (not @p_102) @p_65) :rule not_not)
(step t80 (cl @p_101 @p_65) :rule th_resolution :premises (t79 t78))
(step t81 (cl @p_101) :rule th_resolution :premises (t72 t74 t77 t80))
(step t82 (cl @p_96 @p_99) :rule or :premises (t81))
(step t83 (cl @p_99) :rule resolution :premises (t82 t13))
(step t84 (cl (or @p_98 (! (not @p_93) :named @p_103))) :rule forall_inst :args ((:= veriT_vr1 c$)))
(step t85 (cl @p_98 @p_103) :rule or :premises (t84))
(step t86 (cl (! (or @p_96 @p_103) :named @p_104) @p_100) :rule or_neg)
(step t87 (cl @p_104 @p_25) :rule th_resolution :premises (t76 t86))
(step t88 (cl @p_104 (! (not @p_103) :named @p_105)) :rule or_neg)
(step t89 (cl (not @p_105) @p_93) :rule not_not)
(step t90 (cl @p_104 @p_93) :rule th_resolution :premises (t89 t88))
(step t91 (cl @p_104) :rule th_resolution :premises (t72 t85 t87 t90))
(step t92 (cl @p_96 @p_103) :rule or :premises (t91))
(step t93 (cl @p_103) :rule resolution :premises (t92 t13))
(step t94 (cl x$) :rule resolution :premises (t69 t65 t61 t64 t60 t93 t83))
(step t95 (cl @p_96 @p_106) :rule or :premises (t71))
(step t96 (cl (or (! (not @p_106) :named @p_107) @p_91)) :rule forall_inst :args ((:= veriT_vr1 c$)))
(step t97 (cl @p_107 @p_91) :rule or :premises (t96))
(step t98 (cl (! (or @p_96 @p_91) :named @p_108) @p_100) :rule or_neg)
(step t99 (cl @p_108 @p_25) :rule th_resolution :premises (t76 t98))
(step t100 (cl @p_108 @p_109) :rule or_neg)
(step t101 (cl @p_108) :rule th_resolution :premises (t95 t97 t99 t100))
(step t102 (cl @p_96 @p_91) :rule or :premises (t101))
(step t103 (cl @p_91) :rule resolution :premises (t102 t13))
(step t104 (cl @p_36) :rule resolution :premises (t62 t103 t94))
(step t105 (cl @p_67) :rule resolution :premises (t63 t104))
(step t106 (cl @p_110) :rule resolution :premises (t69 t105))
(step t107 (cl @p_95) :rule resolution :premises (t68 t106))
(step t108 (cl (or @p_84 @p_92)) :rule forall_inst :args ((:= veriT_vr4 c$)))
(step t109 (cl @p_84 @p_92) :rule or :premises (t108))
(step t110 (cl) :rule resolution :premises (t109 t104 t107))
6388f32213a8f0cba4b8bfe24dbcf79d47d5c156 143 0
unsat
(define-fun veriT_sk2 () A$ (! (choice ((veriT_vr9 A$)) (! (ite x$ (! (p$ true veriT_vr9) :named @p_48) (! (p$ false veriT_vr9) :named @p_50)) :named @p_51)) :named @p_62))
(assume a0 (forall ((?v0 Bool) (?v1 A$)) (= (p$ ?v0 ?v1) ?v0)))
(assume a2 (not (= (exists ((?v0 A$)) (p$ x$ ?v0)) (p$ x$ c$))))
(step t3 (cl (! (forall ((?v1 A$)) (! (and (! (= (! (p$ false ?v1) :named @p_2) false) :named @p_4) (! (= (! (p$ true ?v1) :named @p_7) true) :named @p_9)) :named @p_11)) :named @p_1)) :rule bfun_elim :premises (a0))
(step t4 (cl (! (not (! (= (! (exists ((?v0 A$)) (! (ite x$ (! (p$ true ?v0) :named @p_27) (! (p$ false ?v0) :named @p_30)) :named @p_32)) :named @p_26) (! (ite x$ (! (p$ true c$) :named @p_91) (p$ false c$)) :named @p_36)) :named @p_34)) :named @p_37)) :rule bfun_elim :premises (a2))
(anchor :step t5 :args ((:= (?v1 A$) veriT_vr0)))
(step t5.t1 (cl (! (= ?v1 veriT_vr0) :named @p_6)) :rule refl)
(step t5.t2 (cl (= @p_2 (! (p$ false veriT_vr0) :named @p_3))) :rule cong :premises (t5.t1))
(step t5.t3 (cl (= @p_4 (! (= @p_3 false) :named @p_5))) :rule cong :premises (t5.t2))
(step t5.t4 (cl @p_6) :rule refl)
(step t5.t5 (cl (= @p_7 (! (p$ true veriT_vr0) :named @p_8))) :rule cong :premises (t5.t4))
(step t5.t6 (cl (= @p_9 (! (= @p_8 true) :named @p_10))) :rule cong :premises (t5.t5))
(step t5.t7 (cl (= @p_11 (! (and @p_5 @p_10) :named @p_12))) :rule cong :premises (t5.t3 t5.t6))
(step t5 (cl (! (= @p_1 (! (forall ((veriT_vr0 A$)) @p_12) :named @p_14)) :named @p_13)) :rule bind)
(step t6 (cl (not @p_13) (not @p_1) @p_14) :rule equiv_pos2)
(step t7 (cl @p_14) :rule th_resolution :premises (t3 t5 t6))
(anchor :step t8 :args ((veriT_vr0 A$)))
(step t8.t1 (cl (= @p_5 (! (not @p_3) :named @p_15))) :rule equiv_simplify)
(step t8.t2 (cl (= @p_10 @p_8)) :rule equiv_simplify)
(step t8.t3 (cl (= @p_12 (! (and @p_15 @p_8) :named @p_16))) :rule cong :premises (t8.t1 t8.t2))
(step t8 (cl (! (= @p_14 (! (forall ((veriT_vr0 A$)) @p_16) :named @p_18)) :named @p_17)) :rule bind)
(step t9 (cl (not @p_17) (not @p_14) @p_18) :rule equiv_pos2)
(step t10 (cl @p_18) :rule th_resolution :premises (t7 t8 t9))
(anchor :step t11 :args ((:= (veriT_vr0 A$) veriT_vr1)))
(step t11.t1 (cl (! (= veriT_vr0 veriT_vr1) :named @p_21)) :rule refl)
(step t11.t2 (cl (= @p_3 (! (p$ false veriT_vr1) :named @p_19))) :rule cong :premises (t11.t1))
(step t11.t3 (cl (= @p_15 (! (not @p_19) :named @p_20))) :rule cong :premises (t11.t2))
(step t11.t4 (cl @p_21) :rule refl)
(step t11.t5 (cl (= @p_8 (! (p$ true veriT_vr1) :named @p_22))) :rule cong :premises (t11.t4))
(step t11.t6 (cl (= @p_16 (! (and @p_20 @p_22) :named @p_23))) :rule cong :premises (t11.t3 t11.t5))
(step t11 (cl (! (= @p_18 (! (forall ((veriT_vr1 A$)) @p_23) :named @p_25)) :named @p_24)) :rule bind)
(step t12 (cl (not @p_24) (not @p_18) @p_25) :rule equiv_pos2)
(step t13 (cl @p_25) :rule th_resolution :premises (t10 t11 t12))
(anchor :step t14 :args ((:= (?v0 A$) veriT_vr8)))
(step t14.t1 (cl (! (= ?v0 veriT_vr8) :named @p_29)) :rule refl)
(step t14.t2 (cl (= @p_27 (! (p$ true veriT_vr8) :named @p_28))) :rule cong :premises (t14.t1))
(step t14.t3 (cl @p_29) :rule refl)
(step t14.t4 (cl (= @p_30 (! (p$ false veriT_vr8) :named @p_31))) :rule cong :premises (t14.t3))
(step t14.t5 (cl (= @p_32 (! (ite x$ @p_28 @p_31) :named @p_33))) :rule cong :premises (t14.t2 t14.t4))
(step t14 (cl (= @p_26 (! (exists ((veriT_vr8 A$)) @p_33) :named @p_35))) :rule bind)
(step t15 (cl (= @p_34 (! (= @p_35 @p_36) :named @p_38))) :rule cong :premises (t14))
(step t16 (cl (! (= @p_37 (! (not @p_38) :named @p_40)) :named @p_39)) :rule cong :premises (t15))
(step t17 (cl (! (not @p_39) :named @p_42) (! (not @p_37) :named @p_41) @p_40) :rule equiv_pos2)
(step t18 (cl (not @p_41) @p_34) :rule not_not)
(step t19 (cl @p_42 @p_34 @p_40) :rule th_resolution :premises (t18 t17))
(step t20 (cl @p_40) :rule th_resolution :premises (t4 t16 t19))
(step t21 (cl (= @p_38 (! (and (! (=> @p_35 @p_36) :named @p_52) (! (=> @p_36 @p_35) :named @p_54)) :named @p_43))) :rule connective_def)
(step t22 (cl (! (= @p_40 (! (not @p_43) :named @p_45)) :named @p_44)) :rule cong :premises (t21))
(step t23 (cl (! (not @p_44) :named @p_47) (! (not @p_40) :named @p_46) @p_45) :rule equiv_pos2)
(step t24 (cl (not @p_46) @p_38) :rule not_not)
(step t25 (cl @p_47 @p_38 @p_45) :rule th_resolution :premises (t24 t23))
(step t26 (cl @p_45) :rule th_resolution :premises (t20 t22 t25))
(anchor :step t27 :args ((:= (veriT_vr8 A$) veriT_vr9)))
(step t27.t1 (cl (! (= veriT_vr8 veriT_vr9) :named @p_49)) :rule refl)
(step t27.t2 (cl (= @p_28 @p_48)) :rule cong :premises (t27.t1))
(step t27.t3 (cl @p_49) :rule refl)
(step t27.t4 (cl (= @p_31 @p_50)) :rule cong :premises (t27.t3))
(step t27.t5 (cl (= @p_33 @p_51)) :rule cong :premises (t27.t2 t27.t4))
(step t27 (cl (= @p_35 (! (exists ((veriT_vr9 A$)) @p_51) :named @p_53))) :rule bind)
(step t28 (cl (= @p_52 (! (=> @p_53 @p_36) :named @p_55))) :rule cong :premises (t27))
(step t29 (cl (= @p_54 (! (=> @p_36 @p_53) :named @p_56))) :rule cong :premises (t27))
(step t30 (cl (= @p_43 (! (and @p_55 @p_56) :named @p_57))) :rule cong :premises (t28 t29))
(step t31 (cl (! (= @p_45 (! (not @p_57) :named @p_59)) :named @p_58)) :rule cong :premises (t30))
(step t32 (cl (! (not @p_58) :named @p_61) (! (not @p_45) :named @p_60) @p_59) :rule equiv_pos2)
(step t33 (cl (not @p_60) @p_43) :rule not_not)
(step t34 (cl @p_61 @p_43 @p_59) :rule th_resolution :premises (t33 t32))
(step t35 (cl @p_59) :rule th_resolution :premises (t26 t31 t34))
(anchor :step t36 :args ((:= (veriT_vr9 A$) veriT_sk2)))
(step t36.t1 (cl (! (= veriT_vr9 veriT_sk2) :named @p_64)) :rule refl)
(step t36.t2 (cl (= @p_48 (! (p$ true veriT_sk2) :named @p_63))) :rule cong :premises (t36.t1))
(step t36.t3 (cl @p_64) :rule refl)
(step t36.t4 (cl (= @p_50 (! (p$ false veriT_sk2) :named @p_65))) :rule cong :premises (t36.t3))
(step t36.t5 (cl (= @p_51 (! (ite x$ @p_63 @p_65) :named @p_66))) :rule cong :premises (t36.t2 t36.t4))
(step t36 (cl (= @p_53 @p_66)) :rule sko_ex)
(step t37 (cl (= @p_55 (! (=> @p_66 @p_36) :named @p_67))) :rule cong :premises (t36))
(step t38 (cl (= @p_57 (! (and @p_67 @p_56) :named @p_68))) :rule cong :premises (t37))
(step t39 (cl (! (= @p_59 (! (not @p_68) :named @p_70)) :named @p_69)) :rule cong :premises (t38))
(step t40 (cl (! (not @p_69) :named @p_72) (! (not @p_59) :named @p_71) @p_70) :rule equiv_pos2)
(step t41 (cl (not @p_71) @p_57) :rule not_not)
(step t42 (cl @p_72 @p_57 @p_70) :rule th_resolution :premises (t41 t40))
(step t43 (cl @p_70) :rule th_resolution :premises (t35 t39 t42))
(anchor :step t44 :args ((:= (veriT_vr9 A$) veriT_vr10)))
(step t44.t1 (cl (! (= veriT_vr9 veriT_vr10) :named @p_74)) :rule refl)
(step t44.t2 (cl (= @p_48 (! (p$ true veriT_vr10) :named @p_73))) :rule cong :premises (t44.t1))
(step t44.t3 (cl @p_74) :rule refl)
(step t44.t4 (cl (= @p_50 (! (p$ false veriT_vr10) :named @p_75))) :rule cong :premises (t44.t3))
(step t44.t5 (cl (= @p_51 (! (ite x$ @p_73 @p_75) :named @p_76))) :rule cong :premises (t44.t2 t44.t4))
(step t44 (cl (= @p_53 (! (exists ((veriT_vr10 A$)) @p_76) :named @p_77))) :rule bind)
(step t45 (cl (= @p_56 (! (=> @p_36 @p_77) :named @p_78))) :rule cong :premises (t44))
(step t46 (cl (= @p_68 (! (and @p_67 @p_78) :named @p_79))) :rule cong :premises (t45))
(step t47 (cl (! (= @p_70 (! (not @p_79) :named @p_81)) :named @p_80)) :rule cong :premises (t46))
(step t48 (cl (! (not @p_80) :named @p_83) (! (not @p_70) :named @p_82) @p_81) :rule equiv_pos2)
(step t49 (cl (not @p_82) @p_68) :rule not_not)
(step t50 (cl @p_83 @p_68 @p_81) :rule th_resolution :premises (t49 t48))
(step t51 (cl @p_81) :rule th_resolution :premises (t43 t47 t50))
(step t52 (cl (= @p_77 (! (not (! (forall ((veriT_vr10 A$)) (not @p_76)) :named @p_93)) :named @p_84))) :rule connective_def)
(step t53 (cl (= @p_78 (! (=> @p_36 @p_84) :named @p_85))) :rule cong :premises (t52))
(step t54 (cl (= @p_79 (! (and @p_67 @p_85) :named @p_86))) :rule cong :premises (t53))
(step t55 (cl (! (= @p_81 (! (not @p_86) :named @p_88)) :named @p_87)) :rule cong :premises (t54))
(step t56 (cl (! (not @p_87) :named @p_90) (! (not @p_81) :named @p_89) @p_88) :rule equiv_pos2)
(step t57 (cl (not @p_89) @p_79) :rule not_not)
(step t58 (cl @p_90 @p_79 @p_88) :rule th_resolution :premises (t57 t56))
(step t59 (cl @p_88) :rule th_resolution :premises (t51 t55 t58))
(step t60 (cl (not @p_66) x$ @p_65) :rule ite_pos1)
(step t61 (cl @p_67 @p_66) :rule implies_neg1)
(step t62 (cl @p_36 (not x$) (! (not @p_91) :named @p_104)) :rule ite_neg2)
(step t63 (cl @p_67 (! (not @p_36) :named @p_106)) :rule implies_neg2)
(step t64 (cl @p_85 @p_36) :rule implies_neg1)
(step t65 (cl @p_85 (! (not @p_84) :named @p_92)) :rule implies_neg2)
(step t66 (cl (not @p_92) @p_93) :rule not_not)
(step t67 (cl @p_85 @p_93) :rule th_resolution :premises (t66 t65))
(step t68 (cl (not @p_67) (! (not @p_85) :named @p_105)) :rule not_and :premises (t59))
(step t69 (cl (or (! (not @p_25) :named @p_94) (! (forall ((veriT_vr1 A$)) @p_20) :named @p_95))) :rule qnt_cnf)
(step t70 (cl (or @p_94 (! (forall ((veriT_vr1 A$)) @p_22) :named @p_101))) :rule qnt_cnf)
(step t71 (cl @p_94 @p_95) :rule or :premises (t69))
(step t72 (cl (or (! (not @p_95) :named @p_96) (! (not @p_65) :named @p_97))) :rule forall_inst :args ((:= veriT_vr1 veriT_sk2)))
(step t73 (cl @p_96 @p_97) :rule or :premises (t72))
(step t74 (cl (! (or @p_94 @p_97) :named @p_99) (! (not @p_94) :named @p_98)) :rule or_neg)
(step t75 (cl (not @p_98) @p_25) :rule not_not)
(step t76 (cl @p_99 @p_25) :rule th_resolution :premises (t75 t74))
(step t77 (cl @p_99 (! (not @p_97) :named @p_100)) :rule or_neg)
(step t78 (cl (not @p_100) @p_65) :rule not_not)
(step t79 (cl @p_99 @p_65) :rule th_resolution :premises (t78 t77))
(step t80 (cl @p_99) :rule th_resolution :premises (t71 t73 t76 t79))
(step t81 (cl @p_94 @p_97) :rule or :premises (t80))
(step t82 (cl @p_97) :rule resolution :premises (t81 t13))
(step t83 (cl @p_94 @p_101) :rule or :premises (t70))
(step t84 (cl (or (! (not @p_101) :named @p_102) @p_91)) :rule forall_inst :args ((:= veriT_vr1 c$)))
(step t85 (cl @p_102 @p_91) :rule or :premises (t84))
(step t86 (cl (! (or @p_94 @p_91) :named @p_103) @p_98) :rule or_neg)
(step t87 (cl @p_103 @p_25) :rule th_resolution :premises (t75 t86))
(step t88 (cl @p_103 @p_104) :rule or_neg)
(step t89 (cl @p_103) :rule th_resolution :premises (t83 t85 t87 t88))
(step t90 (cl @p_94 @p_91) :rule or :premises (t89))
(step t91 (cl @p_91) :rule resolution :premises (t90 t13))
(step t92 (cl @p_67) :rule resolution :premises (t62 t60 t63 t61 t91 t82))
(step t93 (cl @p_105) :rule resolution :premises (t68 t92))
(step t94 (cl @p_36) :rule resolution :premises (t64 t93))
(step t95 (cl @p_93) :rule resolution :premises (t67 t93))
(step t96 (cl (or @p_84 @p_106)) :rule forall_inst :args ((:= veriT_vr10 c$)))
(step t97 (cl @p_84 @p_106) :rule or :premises (t96))
(step t98 (cl) :rule resolution :premises (t97 t94 t95))
8a6f5819f9bec363751118815580748c0df0e998 57 0
unsat
--> --------------------
--> maximum size reached
--> --------------------
[ Dauer der Verarbeitung: 0.9 Sekunden
(vorverarbeitet)
]
|
