%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SYO063^4 : TPTP v9.2.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n007.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:11:55 AM UTC 2026 % Result : Theorem 52.56s 52.85s % Output : Proof 52.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SYO063^4 : TPTP v9.2.1. Released v4.0.0. % 0.12/0.14 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.19/0.35 % Computer : n007.cluster.edu % 0.19/0.35 % Model : x86_64 x86_64 % 0.19/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.19/0.35 % Memory : 8042.1875MB % 0.19/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.19/0.35 % CPULimit : 300 % 0.19/0.35 % WCLimit : 300 % 0.19/0.35 % DateTime : Tue Jun 2 23:52:26 EDT 2026 % 0.19/0.35 % CPUTime : % 0.29/0.51 %----Proving TH0 % 52.56/52.85 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 52.56/52.85 % SZS status Theorem % 52.56/52.85 % SZS output start Proof % 52.56/52.85 ( % 52.56/52.85 (declare-sort $$unsorted 0) % 52.56/52.85 (declare-const tptp.irel (-> $$unsorted $$unsorted Bool)) % 52.56/52.85 (declare-const tptp.q (-> $$unsorted Bool)) % 52.56/52.85 (declare-const tptp.r (-> $$unsorted Bool)) % 52.56/52.85 (declare-const tptp.p (-> $$unsorted Bool)) % 52.56/52.85 (declare-const tptp.s (-> $$unsorted Bool)) % 52.56/52.85 (declare-const tptp.t (-> $$unsorted Bool)) % 52.56/52.85 (declare-const tptp.ifalse (-> $$unsorted Bool)) % 52.56/52.85 (define tptp.mnot () (let ((_let_1 (@var "U" $$unsorted))) (let ((_let_2 (@var "X" (-> $$unsorted Bool)))) (lambda (@list _let_2 _let_1) (not (_ _let_2 _let_1)))))) % 52.56/52.85 (define tptp.mor () (let ((_let_1 (@var "U" $$unsorted))) (let ((_let_2 (@var "Y" (-> $$unsorted Bool)))) (let ((_let_3 (@var "X" (-> $$unsorted Bool)))) (lambda (@list _let_3 _let_2 _let_1) (or (_ _let_3 _let_1) (_ _let_2 _let_1))))))) % 52.56/52.85 (define tptp.mand () (let ((_let_1 (@var "U" $$unsorted))) (let ((_let_2 (@var "Y" (-> $$unsorted Bool)))) (let ((_let_3 (@var "X" (-> $$unsorted Bool)))) (lambda (@list _let_3 _let_2 _let_1) (and (_ _let_3 _let_1) (_ _let_2 _let_1))))))) % 52.56/52.85 (define tptp.mimplies () (let ((_let_1 (@var "__flatten_var_0" $$unsorted))) (let ((_let_2 (@var "V" (-> $$unsorted Bool)))) (let ((_let_3 (@var "U" (-> $$unsorted Bool)))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ (_ tptp.mor (_ tptp.mnot _let_3)) _let_2) _let_1)))))) % 52.56/52.85 (define tptp.mbox_s4 () (let ((_let_1 (@var "Y" $$unsorted))) (let ((_let_2 (@var "P" (-> $$unsorted Bool)))) (let ((_let_3 (@var "X" $$unsorted))) (lambda (@list _let_2 _let_3) (forall (@list _let_1) (=> (_ (_ tptp.irel _let_3) _let_1) (_ _let_2 _let_1)))))))) % 52.56/52.85 (define tptp.iatom () (let ((_let_1 (@var "__flatten_var_0" $$unsorted))) (let ((_let_2 (@var "P" (-> $$unsorted Bool)))) (lambda (@list _let_2 _let_1) (_ _let_2 _let_1))))) % 52.56/52.85 (define tptp.inot () (let ((_let_1 (@var "__flatten_var_0" $$unsorted))) (let ((_let_2 (@var "P" (-> $$unsorted Bool)))) (lambda (@list _let_2 _let_1) (_ (_ tptp.mnot (_ tptp.mbox_s4 _let_2)) _let_1))))) % 52.56/52.85 (define tptp.itrue () (lambda (@list (@var "W" $$unsorted)) true)) % 52.56/52.85 (define tptp.iand () (let ((_let_1 (@var "__flatten_var_0" $$unsorted))) (let ((_let_2 (@var "Q" (-> $$unsorted Bool)))) (let ((_let_3 (@var "P" (-> $$unsorted Bool)))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ (_ tptp.mand _let_3) _let_2) _let_1)))))) % 52.56/52.85 (define tptp.ior () (let ((_let_1 (@var "__flatten_var_0" $$unsorted))) (let ((_let_2 (@var "Q" (-> $$unsorted Bool)))) (let ((_let_3 (@var "P" (-> $$unsorted Bool)))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ (_ tptp.mor (_ tptp.mbox_s4 _let_3)) (_ tptp.mbox_s4 _let_2)) _let_1)))))) % 52.56/52.85 (define tptp.iimplies () (let ((_let_1 (@var "__flatten_var_0" $$unsorted))) (let ((_let_2 (@var "Q" (-> $$unsorted Bool)))) (let ((_let_3 (@var "P" (-> $$unsorted Bool)))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ (_ tptp.mimplies (_ tptp.mbox_s4 _let_3)) (_ tptp.mbox_s4 _let_2)) _let_1)))))) % 52.56/52.85 (define tptp.iimplied () (let ((_let_1 (@var "__flatten_var_0" $$unsorted))) (let ((_let_2 (@var "P" (-> $$unsorted Bool)))) (let ((_let_3 (@var "Q" (-> $$unsorted Bool)))) (lambda (@list _let_2 _let_3 _let_1) (_ (_ (_ tptp.iimplies _let_3) _let_2) _let_1)))))) % 52.56/52.85 (define tptp.iequiv () (let ((_let_1 (@var "__flatten_var_0" $$unsorted))) (let ((_let_2 (@var "P" (-> $$unsorted Bool)))) (let ((_let_3 (@var "Q" (-> $$unsorted Bool)))) (lambda (@list _let_2 _let_3 _let_1) (_ (_ (_ tptp.iand (_ (_ tptp.iimplies _let_2) _let_3)) (_ (_ tptp.iimplies _let_3) _let_2)) _let_1)))))) % 52.56/52.85 (define tptp.ixor () (let ((_let_1 (@var "__flatten_var_0" $$unsorted))) (let ((_let_2 (@var "Q" (-> $$unsorted Bool)))) (let ((_let_3 (@var "P" (-> $$unsorted Bool)))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ tptp.inot (_ (_ tptp.iequiv _let_3) _let_2)) _let_1)))))) % 52.56/52.85 (define tptp.ivalid () (let ((_let_1 (@var "W" $$unsorted))) (let ((_let_2 (@var "Phi" (-> $$unsorted Bool)))) (lambda (@list _let_2) (forall (@list _let_1) (_ _let_2 _let_1)))))) % 52.56/52.85 (define tptp.isatisfiable () (let ((_let_1 (@var "W" $$unsorted))) (let ((_let_2 (@var "Phi" (-> $$unsorted Bool)))) (lambda (@list _let_2) (exists (@list _let_1) (_ _let_2 _let_1)))))) % 52.56/52.85 (define tptp.icountersatisfiable () (let ((_let_1 (@var "W" $$unsorted))) (let ((_let_2 (@var "Phi" (-> $$unsorted Bool)))) (lambda (@list _let_2) (exists (@list _let_1) (not (_ _let_2 _let_1))))))) % 52.56/52.85 (define tptp.iinvalid () (let ((_let_1 (@var "W" $$unsorted))) (let ((_let_2 (@var "Phi" (-> $$unsorted Bool)))) (lambda (@list _let_2) (forall (@list _let_1) (not (_ _let_2 _let_1))))))) % 52.56/52.85 (define @t1 () (@var "X" $$unsorted)) % 52.56/52.85 (define @t2 () (_ tptp.irel @t1)) % 52.56/52.85 (define @t3 () (@list @t1)) % 52.56/52.85 (define @t4 () (@var "Z" $$unsorted)) % 52.56/52.85 (define @t5 () (_ @t2 @t4)) % 52.56/52.85 (define @t6 () (@var "Y" $$unsorted)) % 52.56/52.85 (define @t7 () (_ (_ tptp.irel @t6) @t4)) % 52.56/52.85 (define @t8 () (_ @t2 @t6)) % 52.56/52.85 (define @t9 () (and @t8 @t7)) % 52.56/52.85 (define @t10 () (@list @t1 @t6 @t4)) % 52.56/52.85 (define @t11 () (forall @t10 (=> @t9 @t5))) % 52.56/52.85 (define @t12 () (_ tptp.iatom tptp.s)) % 52.56/52.85 (define @t13 () (_ tptp.iatom tptp.p)) % 52.56/52.85 (define @t14 () (_ (_ tptp.iimplies (_ tptp.iatom tptp.t)) (_ tptp.iatom tptp.r))) % 52.56/52.85 (define @t15 () (not (_ tptp.ivalid (_ (_ tptp.iimplies (_ tptp.inot (_ (_ tptp.iand (_ (_ tptp.iimplies @t13) (_ tptp.iatom tptp.q))) @t14))) (_ (_ tptp.iand (_ tptp.inot (_ tptp.inot @t13))) (_ (_ tptp.iand @t12) @t12)))))) % 52.56/52.85 (define @t16 () (@var "U" $$unsorted)) % 52.56/52.85 (define @t17 () (@var "X" (-> $$unsorted Bool))) % 52.56/52.85 (define @t18 () (_ @t17 @t16)) % 52.56/52.85 (define @t19 () (lambda (@list @t17 @t16) (not @t18))) % 52.56/52.85 (define @t20 () (@var "Y" (-> $$unsorted Bool))) % 52.56/52.85 (define @t21 () (_ @t20 @t16)) % 52.56/52.85 (define @t22 () (@list @t17 @t20 @t16)) % 52.56/52.85 (define @t23 () (lambda @t22 (or @t18 @t21))) % 52.56/52.85 (define @t24 () (lambda @t22 (and @t18 @t21))) % 52.56/52.85 (define @t25 () (@var "__flatten_var_0" $$unsorted)) % 52.56/52.85 (define @t26 () (@var "V" (-> $$unsorted Bool))) % 52.56/52.85 (define @t27 () (@var "U" (-> $$unsorted Bool))) % 52.56/52.85 (define @t28 () (@list @t27 @t26 @t25)) % 52.56/52.85 (define @t29 () (lambda @t28 (_ (_ (_ tptp.mor (_ tptp.mnot @t27)) @t26) @t25))) % 52.56/52.85 (define @t30 () (@var "P" (-> $$unsorted Bool))) % 52.56/52.85 (define @t31 () (_ @t30 @t6)) % 52.56/52.85 (define @t32 () (@list @t6)) % 52.56/52.85 (define @t33 () (forall @t32 (=> @t8 @t31))) % 52.56/52.85 (define @t34 () (@list @t30 @t1)) % 52.56/52.85 (define @t35 () (lambda @t34 @t33)) % 52.56/52.85 (define @t36 () (_ @t30 @t25)) % 52.56/52.85 (define @t37 () (@list @t30 @t25)) % 52.56/52.85 (define @t38 () (lambda @t37 @t36)) % 52.56/52.85 (define @t39 () (_ tptp.mbox_s4 @t30)) % 52.56/52.85 (define @t40 () (lambda @t37 (_ (_ tptp.mnot @t39) @t25))) % 52.56/52.85 (define @t41 () (@var "W" $$unsorted)) % 52.56/52.85 (define @t42 () (@list @t41)) % 52.56/52.85 (define @t43 () (lambda @t42 true)) % 52.56/52.85 (define @t44 () (@var "Q" (-> $$unsorted Bool))) % 52.56/52.85 (define @t45 () (@list @t30 @t44 @t25)) % 52.56/52.85 (define @t46 () (lambda @t45 (_ (_ (_ tptp.mand @t30) @t44) @t25))) % 52.56/52.85 (define @t47 () (_ tptp.mbox_s4 @t44)) % 52.56/52.85 (define @t48 () (lambda @t45 (_ (_ (_ tptp.mor @t39) @t47) @t25))) % 52.56/52.85 (define @t49 () (lambda @t45 (_ (_ (_ tptp.mimplies @t39) @t47) @t25))) % 52.56/52.85 (define @t50 () (_ (_ tptp.iimplies @t44) @t30)) % 52.56/52.85 (define @t51 () (lambda @t45 (_ @t50 @t25))) % 52.56/52.85 (define @t52 () (lambda @t45 (_ (_ (_ tptp.iand (_ (_ tptp.iimplies @t30) @t44)) @t50) @t25))) % 52.56/52.85 (define @t53 () (lambda @t45 (_ (_ tptp.inot (_ (_ tptp.iequiv @t30) @t44)) @t25))) % 52.56/52.85 (define @t54 () (@var "Phi" (-> $$unsorted Bool))) % 52.56/52.85 (define @t55 () (_ @t54 @t41)) % 52.56/52.85 (define @t56 () (forall @t42 @t55)) % 52.56/52.85 (define @t57 () (@list @t54)) % 52.56/52.85 (define @t58 () (lambda @t57 @t56)) % 52.56/52.85 (define @t59 () (lambda @t57 (exists @t42 @t55))) % 52.56/52.85 (define @t60 () (not @t55)) % 52.56/52.85 (define @t61 () (lambda @t57 (exists @t42 @t60))) % 52.56/52.85 (define @t62 () (lambda @t57 (forall @t42 @t60))) % 52.56/52.85 (define @t63 () (tptp.s @t41)) % 52.56/52.85 (define @t64 () (_ tptp.s @t41)) % 52.56/52.85 (define @t65 () (_ tptp.s @t25)) % 52.56/52.85 (define @t66 () (@list @t25)) % 52.56/52.85 (define @t67 () (lambda @t66 @t65)) % 52.56/52.85 (define @t68 () (_ @t67 @t41)) % 52.56/52.85 (define @t69 () (forall @t42 @t68)) % 52.56/52.85 (define @t70 () (_ @t54 @t41)) % 52.56/52.85 (define @t71 () (lambda @t57 (forall @t42 @t70))) % 52.56/52.85 (define @t72 () (_ @t38 tptp.s)) % 52.56/52.85 (define @t73 () (@var "BOUND_VARIABLE_8506" $$unsorted)) % 52.56/52.85 (define @t74 () (@var "BOUND_VARIABLE_8415" $$unsorted)) % 52.56/52.85 (define @t75 () (tptp.p @t74)) % 52.56/52.85 (define @t76 () (@var "BOUND_VARIABLE_8465" $$unsorted)) % 52.56/52.85 (define @t77 () (@list @t74)) % 52.56/52.85 (define @t78 () (not (forall @t77 (or (not (tptp.irel @t76 @t74)) @t75)))) % 52.56/52.85 (define @t79 () (@list @t76)) % 52.56/52.85 (define @t80 () (and (not (forall @t79 (or (not (tptp.irel @t73 @t76)) @t78))) (tptp.s @t73))) % 52.56/52.85 (define @t81 () (not (tptp.irel @t41 @t73))) % 52.56/52.85 (define @t82 () (@var "BOUND_VARIABLE_8344" $$unsorted)) % 52.56/52.85 (define @t83 () (tptp.r @t82)) % 52.56/52.85 (define @t84 () (@var "BOUND_VARIABLE_8369" $$unsorted)) % 52.56/52.85 (define @t85 () (@var "BOUND_VARIABLE_8283" $$unsorted)) % 52.56/52.85 (define @t86 () (tptp.t @t85)) % 52.56/52.85 (define @t87 () (@list @t85)) % 52.56/52.85 (define @t88 () (@var "BOUND_VARIABLE_8337" $$unsorted)) % 52.56/52.85 (define @t89 () (tptp.q @t88)) % 52.56/52.85 (define @t90 () (@var "BOUND_VARIABLE_8301" $$unsorted)) % 52.56/52.85 (define @t91 () (tptp.p @t90)) % 52.56/52.85 (define @t92 () (@list @t90)) % 52.56/52.85 (define @t93 () (and (or (not (forall @t92 (or (not (tptp.irel @t84 @t90)) @t91))) (not (tptp.irel @t84 @t88)) @t89) (or (not (forall @t87 (or (not (tptp.irel @t84 @t85)) @t86))) (not (tptp.irel @t84 @t82)) @t83))) % 52.56/52.85 (define @t94 () (@list @t84 @t88 @t82)) % 52.56/52.85 (define @t95 () (not (forall @t94 (or (not (tptp.irel @t6 @t84)) @t93)))) % 52.56/52.85 (define @t96 () (not (tptp.irel @t41 @t6))) % 52.56/52.85 (define @t97 () (not (forall @t32 (or @t96 @t95)))) % 52.56/52.85 (define @t98 () (or @t97 @t81 @t80)) % 52.56/52.85 (define @t99 () (or @t81 @t80)) % 52.56/52.85 (define @t100 () (or @t97 @t99)) % 52.56/52.85 (define @t101 () (@list @t41 @t73)) % 52.56/52.85 (define @t102 () (forall @t101 @t100)) % 52.56/52.85 (define @t103 () (@list @t73)) % 52.56/52.85 (define @t104 () (forall @t103 @t100)) % 52.56/52.85 (define @t105 () (forall @t103 @t99)) % 52.56/52.85 (define @t106 () (@list @t6)) % 52.56/52.85 (define @t107 () (or @t97 @t105)) % 52.56/52.85 (define @t108 () (tptp.s @t6)) % 52.56/52.85 (define @t109 () (not (forall @t79 (or (not (tptp.irel @t6 @t76)) @t78)))) % 52.56/52.85 (define @t110 () (and @t109 @t108)) % 52.56/52.85 (define @t111 () (or @t97 (forall @t32 (or @t96 @t110)))) % 52.56/52.85 (define @t112 () (not (tptp.irel @t25 @t6))) % 52.56/52.85 (define @t113 () (not (forall @t32 (or @t112 @t95)))) % 52.56/52.85 (define @t114 () (lambda @t66 (or @t113 (forall @t32 (or @t112 @t110))))) % 52.56/52.85 (define @t115 () (_ @t114 @t41)) % 52.56/52.85 (define @t116 () (forall @t42 @t115)) % 52.56/52.85 (define @t117 () (_ tptp.s @t6)) % 52.56/52.85 (define @t118 () (and @t109 @t117)) % 52.56/52.85 (define @t119 () (or @t112 @t118)) % 52.56/52.85 (define @t120 () (not (forall @t77 (or (not (tptp.irel @t6 @t74)) @t75)))) % 52.56/52.85 (define @t121 () (forall @t32 (or @t112 @t120))) % 52.56/52.85 (define @t122 () (not @t121)) % 52.56/52.85 (define @t123 () (and @t122 @t65)) % 52.56/52.85 (define @t124 () (lambda @t66 @t123)) % 52.56/52.85 (define @t125 () (or @t112 (_ @t124 @t6))) % 52.56/52.85 (define @t126 () (forall @t32 @t125)) % 52.56/52.85 (define @t127 () (or @t113 @t126)) % 52.56/52.85 (define @t128 () (lambda @t66 @t127)) % 52.56/52.85 (define @t129 () (_ @t44 @t6)) % 52.56/52.85 (define @t130 () (forall @t32 (or @t112 @t129))) % 52.56/52.85 (define @t131 () (@list @t44 @t25)) % 52.56/52.85 (define @t132 () (_ @t67 @t25)) % 52.56/52.85 (define @t133 () (and @t122 @t132)) % 52.56/52.85 (define @t134 () (lambda @t66 @t133)) % 52.56/52.85 (define @t135 () (_ @t44 @t25)) % 52.56/52.85 (define @t136 () (and @t65 @t132)) % 52.56/52.85 (define @t137 () (lambda @t66 @t136)) % 52.56/52.85 (define @t138 () (and @t132 @t135)) % 52.56/52.85 (define @t139 () (lambda @t131 @t138)) % 52.56/52.85 (define @t140 () (and @t36 @t135)) % 52.56/52.85 (define @t141 () (lambda @t45 @t140)) % 52.56/52.85 (define @t142 () (lambda @t66 @t122)) % 52.56/52.85 (define @t143 () (_ @t142 @t25)) % 52.56/52.85 (define @t144 () (and @t143 @t135)) % 52.56/52.85 (define @t145 () (lambda @t131 @t144)) % 52.56/52.85 (define @t146 () (tptp.p @t6)) % 52.56/52.85 (define @t147 () (forall @t32 (or @t112 @t146))) % 52.56/52.85 (define @t148 () (@list @t74)) % 52.56/52.85 (define @t149 () (not @t147)) % 52.56/52.85 (define @t150 () (lambda @t66 @t149)) % 52.56/52.85 (define @t151 () (or @t112 (_ @t150 @t6))) % 52.56/52.85 (define @t152 () (forall @t32 @t151)) % 52.56/52.85 (define @t153 () (not @t152)) % 52.56/52.85 (define @t154 () (lambda @t66 @t153)) % 52.56/52.85 (define @t155 () (_ @t30 @t6)) % 52.56/52.85 (define @t156 () (forall @t32 (or @t112 @t155))) % 52.56/52.85 (define @t157 () (not @t156)) % 52.56/52.85 (define @t158 () (lambda @t37 @t157)) % 52.56/52.85 (define @t159 () (_ tptp.p @t6)) % 52.56/52.85 (define @t160 () (or @t112 @t159)) % 52.56/52.85 (define @t161 () (lambda @t66 (_ tptp.p @t25))) % 52.56/52.85 (define @t162 () (_ @t161 @t6)) % 52.56/52.85 (define @t163 () (or @t112 @t162)) % 52.56/52.85 (define @t164 () (forall @t32 @t163)) % 52.56/52.85 (define @t165 () (not @t164)) % 52.56/52.85 (define @t166 () (lambda @t66 @t165)) % 52.56/52.85 (define @t167 () (_ @t38 tptp.p)) % 52.56/52.85 (define @t168 () (not (tptp.irel @t6 @t82))) % 52.56/52.85 (define @t169 () (not (forall @t87 (or (not (tptp.irel @t6 @t85)) @t86)))) % 52.56/52.85 (define @t170 () (or @t169 @t168 @t83)) % 52.56/52.85 (define @t171 () (not (tptp.irel @t6 @t88))) % 52.56/52.85 (define @t172 () (not (forall @t92 (or (not (tptp.irel @t6 @t90)) @t91)))) % 52.56/52.85 (define @t173 () (or @t172 @t171 @t89)) % 52.56/52.85 (define @t174 () (@list @t6 @t88 @t82)) % 52.56/52.85 (define @t175 () (forall @t174 (or @t112 (and @t173 @t170)))) % 52.56/52.85 (define @t176 () (not @t175)) % 52.56/52.85 (define @t177 () (lambda @t66 @t176)) % 52.56/52.85 (define @t178 () (or @t112 (_ @t177 @t6))) % 52.56/52.85 (define @t179 () (forall @t32 @t178)) % 52.56/52.85 (define @t180 () (not @t179)) % 52.56/52.85 (define @t181 () (or @t180 @t130)) % 52.56/52.85 (define @t182 () (lambda @t131 @t181)) % 52.56/52.85 (define @t183 () (or @t157 @t130)) % 52.56/52.85 (define @t184 () (lambda @t45 @t183)) % 52.56/52.85 (define @t185 () (or @t168 @t83)) % 52.56/52.85 (define @t186 () (or @t169 @t185)) % 52.56/52.85 (define @t187 () (or @t171 @t89)) % 52.56/52.85 (define @t188 () (or @t172 @t187)) % 52.56/52.85 (define @t189 () (and @t188 @t186)) % 52.56/52.85 (define @t190 () (or @t112 @t189)) % 52.56/52.85 (define @t191 () (forall @t174 @t190)) % 52.56/52.85 (define @t192 () (@list @t88 @t82)) % 52.56/52.85 (define @t193 () (forall @t192 @t190)) % 52.56/52.85 (define @t194 () (@list @t82)) % 52.56/52.85 (define @t195 () (forall @t194 @t185)) % 52.56/52.85 (define @t196 () (@var "BOUND_VARIABLE_8275" $$unsorted)) % 52.56/52.85 (define @t197 () (@list @t196)) % 52.56/52.85 (define @t198 () (or @t169 @t195)) % 52.56/52.85 (define @t199 () (forall @t194 @t186)) % 52.56/52.85 (define @t200 () (forall @t192 @t186)) % 52.56/52.85 (define @t201 () (@list @t88)) % 52.56/52.85 (define @t202 () (forall @t201 @t187)) % 52.56/52.85 (define @t203 () (@var "BOUND_VARIABLE_8293" $$unsorted)) % 52.56/52.85 (define @t204 () (@list @t203)) % 52.56/52.85 (define @t205 () (or @t172 @t202)) % 52.56/52.85 (define @t206 () (forall @t201 @t188)) % 52.56/52.85 (define @t207 () (forall @t192 @t188)) % 52.56/52.85 (define @t208 () (and @t207 @t200)) % 52.56/52.85 (define @t209 () (forall @t192 @t189)) % 52.56/52.85 (define @t210 () (or @t112 @t209)) % 52.56/52.85 (define @t211 () (tptp.r @t196)) % 52.56/52.85 (define @t212 () (@list @t196)) % 52.56/52.85 (define @t213 () (tptp.q @t203)) % 52.56/52.85 (define @t214 () (@list @t203)) % 52.56/52.85 (define @t215 () (and (or @t172 (forall @t214 (or (not (tptp.irel @t6 @t203)) @t213))) (or @t169 (forall @t212 (or (not (tptp.irel @t6 @t196)) @t211))))) % 52.56/52.85 (define @t216 () (tptp.r @t6)) % 52.56/52.85 (define @t217 () (forall @t32 (or @t112 @t216))) % 52.56/52.85 (define @t218 () (tptp.t @t6)) % 52.56/52.85 (define @t219 () (forall @t32 (or @t112 @t218))) % 52.56/52.85 (define @t220 () (@list @t85)) % 52.56/52.85 (define @t221 () (not @t219)) % 52.56/52.85 (define @t222 () (or @t221 @t217)) % 52.56/52.85 (define @t223 () (tptp.q @t6)) % 52.56/52.85 (define @t224 () (forall @t32 (or @t112 @t223))) % 52.56/52.85 (define @t225 () (@list @t90)) % 52.56/52.85 (define @t226 () (or @t149 @t224)) % 52.56/52.85 (define @t227 () (and @t226 @t222)) % 52.56/52.85 (define @t228 () (lambda @t66 @t227)) % 52.56/52.85 (define @t229 () (or @t112 (_ @t228 @t6))) % 52.56/52.85 (define @t230 () (forall @t32 @t229)) % 52.56/52.85 (define @t231 () (not @t230)) % 52.56/52.85 (define @t232 () (lambda @t66 @t231)) % 52.56/52.85 (define @t233 () (lambda @t66 @t222)) % 52.56/52.85 (define @t234 () (_ @t233 @t25)) % 52.56/52.85 (define @t235 () (and @t226 @t234)) % 52.56/52.85 (define @t236 () (lambda @t66 @t235)) % 52.56/52.85 (define @t237 () (_ tptp.r @t6)) % 52.56/52.85 (define @t238 () (or @t112 @t237)) % 52.56/52.85 (define @t239 () (lambda @t66 (_ tptp.r @t25))) % 52.56/52.85 (define @t240 () (_ @t239 @t6)) % 52.56/52.85 (define @t241 () (or @t112 @t240)) % 52.56/52.85 (define @t242 () (forall @t32 @t241)) % 52.56/52.85 (define @t243 () (or @t221 @t242)) % 52.56/52.85 (define @t244 () (lambda @t66 @t243)) % 52.56/52.85 (define @t245 () (_ @t38 tptp.r)) % 52.56/52.85 (define @t246 () (_ tptp.t @t6)) % 52.56/52.85 (define @t247 () (or @t112 @t246)) % 52.56/52.85 (define @t248 () (lambda @t66 (_ tptp.t @t25))) % 52.56/52.85 (define @t249 () (_ @t248 @t6)) % 52.56/52.85 (define @t250 () (or @t112 @t249)) % 52.56/52.85 (define @t251 () (forall @t32 @t250)) % 52.56/52.85 (define @t252 () (not @t251)) % 52.56/52.85 (define @t253 () (or @t252 @t130)) % 52.56/52.85 (define @t254 () (lambda @t131 @t253)) % 52.56/52.85 (define @t255 () (_ @t38 tptp.t)) % 52.56/52.85 (define @t256 () (lambda @t66 @t226)) % 52.56/52.85 (define @t257 () (_ @t256 @t25)) % 52.56/52.85 (define @t258 () (and @t257 @t135)) % 52.56/52.85 (define @t259 () (lambda @t131 @t258)) % 52.56/52.85 (define @t260 () (_ tptp.q @t6)) % 52.56/52.85 (define @t261 () (or @t112 @t260)) % 52.56/52.85 (define @t262 () (lambda @t66 (_ tptp.q @t25))) % 52.56/52.85 (define @t263 () (_ @t262 @t6)) % 52.56/52.85 (define @t264 () (or @t112 @t263)) % 52.56/52.85 (define @t265 () (forall @t32 @t264)) % 52.56/52.85 (define @t266 () (or @t149 @t265)) % 52.56/52.85 (define @t267 () (lambda @t66 @t266)) % 52.56/52.85 (define @t268 () (_ @t38 tptp.q)) % 52.56/52.85 (define @t269 () (or @t165 @t130)) % 52.56/52.85 (define @t270 () (lambda @t131 @t269)) % 52.56/52.85 (define @t271 () (_ @t30 @t16)) % 52.56/52.85 (define @t272 () (@list @t16)) % 52.56/52.85 (define @t273 () (lambda @t272 (and @t271 (_ @t44 @t16)))) % 52.56/52.85 (define @t274 () (@list @t20 @t16)) % 52.56/52.85 (define @t275 () (lambda @t274 (and @t271 @t21))) % 52.56/52.85 (define @t276 () (forall @t32 (or (not (tptp.irel @t16 @t6)) @t155))) % 52.56/52.85 (define @t277 () (tptp.irel @t1 @t6)) % 52.56/52.85 (define @t278 () (not @t277)) % 52.56/52.85 (define @t279 () (forall @t32 (or @t278 @t155))) % 52.56/52.85 (define @t280 () (lambda @t3 @t279)) % 52.56/52.85 (define @t281 () (_ @t280 @t16)) % 52.56/52.85 (define @t282 () (not @t281)) % 52.56/52.85 (define @t283 () (lambda @t272 @t282)) % 52.56/52.85 (define @t284 () (lambda @t34 @t279)) % 52.56/52.85 (define @t285 () (not @t8)) % 52.56/52.85 (define @t286 () (or @t285 @t31)) % 52.56/52.85 (define @t287 () (lambda @t3 (forall @t32 (or @t278 @t129)))) % 52.56/52.85 (define @t288 () (_ @t287 @t25)) % 52.56/52.85 (define @t289 () (or @t157 @t288)) % 52.56/52.85 (define @t290 () (lambda @t66 @t289)) % 52.56/52.85 (define @t291 () (_ @t26 @t25)) % 52.56/52.85 (define @t292 () (@list @t26 @t25)) % 52.56/52.85 (define @t293 () (_ @t280 @t25)) % 52.56/52.85 (define @t294 () (not @t293)) % 52.56/52.85 (define @t295 () (or @t294 @t291)) % 52.56/52.85 (define @t296 () (lambda @t292 @t295)) % 52.56/52.85 (define @t297 () (or (not (_ @t27 @t25)) @t291)) % 52.56/52.85 (define @t298 () (lambda @t28 @t297)) % 52.56/52.85 (define @t299 () (not (_ @t27 @t16))) % 52.56/52.85 (define @t300 () (lambda @t272 (or @t299 (_ @t26 @t16)))) % 52.56/52.85 (define @t301 () (lambda @t272 @t299)) % 52.56/52.85 (define @t302 () (_ @t301 @t16)) % 52.56/52.85 (define @t303 () (or @t302 @t21)) % 52.56/52.85 (define @t304 () (lambda @t274 @t303)) % 52.56/52.85 (define @t305 () (forall @t101 @t98)) % 52.56/52.85 (define @t306 () (@quantifiers_skolemize @t305 1)) % 52.56/52.85 (define @t307 () (tptp.s @t306)) % 52.56/52.85 (define @t308 () (forall @t79 (or (not (tptp.irel @t306 @t76)) @t78))) % 52.56/52.85 (define @t309 () (not @t308)) % 52.56/52.85 (define @t310 () (and @t309 @t307)) % 52.56/52.85 (define @t311 () (@quantifiers_skolemize @t305 0)) % 52.56/52.85 (define @t312 () (tptp.irel @t311 @t306)) % 52.56/52.85 (define @t313 () (not @t312)) % 52.56/52.85 (define @t314 () (forall @t32 (or (not (tptp.irel @t311 @t6)) @t95))) % 52.56/52.85 (define @t315 () (not @t314)) % 52.56/52.85 (define @t316 () (or @t315 @t313 @t310)) % 52.56/52.85 (define @t317 () (@list true)) % 52.56/52.85 (define @t318 () (@list @t316)) % 52.56/52.85 (define @t319 () (forall @t94 (or (not (tptp.irel @t306 @t84)) @t93))) % 52.56/52.85 (define @t320 () (@quantifiers_skolemize @t319 0)) % 52.56/52.85 (define @t321 () (forall @t77 (or (not (tptp.irel @t320 @t74)) @t75))) % 52.56/52.85 (define @t322 () (not @t321)) % 52.56/52.85 (define @t323 () (tptp.irel @t306 @t320)) % 52.56/52.85 (define @t324 () (not @t323)) % 52.56/52.85 (define @t325 () (or @t324 @t322)) % 52.56/52.85 (define @t326 () (@var "BOUND_VARIABLE_8128" $$unsorted)) % 52.56/52.85 (define @t327 () (tptp.r @t326)) % 52.56/52.85 (define @t328 () (@var "BOUND_VARIABLE_8148" $$unsorted)) % 52.56/52.85 (define @t329 () (not (tptp.irel @t328 @t326))) % 52.56/52.85 (define @t330 () (@var "BOUND_VARIABLE_8103" $$unsorted)) % 52.56/52.85 (define @t331 () (tptp.t @t330)) % 52.56/52.85 (define @t332 () (@list @t330)) % 52.56/52.85 (define @t333 () (not (forall @t332 (or (not (tptp.irel @t328 @t330)) @t331)))) % 52.56/52.85 (define @t334 () (@list @t328 @t326)) % 52.56/52.85 (define @t335 () (not (forall @t334 (or (not (tptp.irel @t6 @t328)) @t333 @t329 @t327)))) % 52.56/52.85 (define @t336 () (forall @t32 (or (not (tptp.irel @t306 @t6)) @t335))) % 52.56/52.85 (define @t337 () (@quantifiers_skolemize @t336 0)) % 52.56/52.85 (define @t338 () (forall @t94 (or (not (tptp.irel @t337 @t84)) @t93))) % 52.56/52.85 (define @t339 () (@quantifiers_skolemize @t338 0)) % 52.56/52.85 (define @t340 () (forall @t77 (or (not (tptp.irel @t339 @t74)) @t75))) % 52.56/52.85 (define @t341 () (not @t340)) % 52.56/52.85 (define @t342 () (tptp.irel @t306 @t339)) % 52.56/52.85 (define @t343 () (not @t342)) % 52.56/52.85 (define @t344 () (or @t343 @t341)) % 52.56/52.85 (define @t345 () (@list @t306)) % 52.56/52.85 (define @t346 () (not @t319)) % 52.56/52.85 (define @t347 () (or @t313 @t346)) % 52.56/52.85 (define @t348 () (@quantifiers_skolemize @t319 2)) % 52.56/52.85 (define @t349 () (@quantifiers_skolemize @t319 1)) % 52.56/52.85 (define @t350 () (forall @t92 (or (not (tptp.irel @t320 @t90)) @t91))) % 52.56/52.85 (define @t351 () (not @t350)) % 52.56/52.85 (define @t352 () (or @t324 (and (or @t351 (not (tptp.irel @t320 @t349)) (tptp.q @t349)) (or (not (forall @t87 (or (not (tptp.irel @t320 @t85)) @t86))) (not (tptp.irel @t320 @t348)) (tptp.r @t348))))) % 52.56/52.85 (define @t353 () (@quantifiers_skolemize @t350 0)) % 52.56/52.85 (define @t354 () (tptp.p @t353)) % 52.56/52.85 (define @t355 () (tptp.irel @t320 @t353)) % 52.56/52.85 (define @t356 () (not @t355)) % 52.56/52.85 (define @t357 () (or @t356 @t354)) % 52.56/52.85 (define @t358 () (not @t357)) % 52.56/52.85 (define @t359 () (tptp.irel @t1 @t4)) % 52.56/52.85 (define @t360 () (tptp.irel @t6 @t4)) % 52.56/52.85 (define @t361 () (not @t7)) % 52.56/52.85 (define @t362 () (or @t285 @t361 @t5)) % 52.56/52.85 (define @t363 () (tptp.irel @t306 @t353)) % 52.56/52.85 (define @t364 () (or @t324 @t356 @t363)) % 52.56/52.85 (define @t365 () (@var "BOUND_VARIABLE_8204" $$unsorted)) % 52.56/52.85 (define @t366 () (tptp.p @t365)) % 52.56/52.85 (define @t367 () (not (tptp.irel @t41 @t365))) % 52.56/52.85 (define @t368 () (not (forall @t32 (or @t96 @t335)))) % 52.56/52.85 (define @t369 () (or @t367 @t366)) % 52.56/52.85 (define @t370 () (or @t368 @t369)) % 52.56/52.85 (define @t371 () (forall (@list @t41 @t365) @t370)) % 52.56/52.85 (define @t372 () (@list @t365)) % 52.56/52.85 (define @t373 () (forall @t372 @t370)) % 52.56/52.85 (define @t374 () (forall @t372 @t369)) % 52.56/52.85 (define @t375 () (or @t368 @t374)) % 52.56/52.85 (define @t376 () (or @t368 (forall @t32 (or @t96 @t146)))) % 52.56/52.85 (define @t377 () (not (forall @t32 (or @t112 @t335)))) % 52.56/52.85 (define @t378 () (lambda @t66 (or @t377 @t147))) % 52.56/52.85 (define @t379 () (_ @t378 @t41)) % 52.56/52.85 (define @t380 () (forall @t42 @t379)) % 52.56/52.85 (define @t381 () (or @t377 @t164)) % 52.56/52.85 (define @t382 () (lambda @t66 @t381)) % 52.56/52.85 (define @t383 () (not (tptp.irel @t6 @t326))) % 52.56/52.85 (define @t384 () (not (forall @t332 (or (not (tptp.irel @t6 @t330)) @t331)))) % 52.56/52.85 (define @t385 () (or @t112 @t384 @t383 @t327)) % 52.56/52.85 (define @t386 () (@list @t6 @t326)) % 52.56/52.85 (define @t387 () (forall @t386 @t385)) % 52.56/52.85 (define @t388 () (not @t387)) % 52.56/52.85 (define @t389 () (lambda @t66 @t388)) % 52.56/52.85 (define @t390 () (or @t112 (_ @t389 @t6))) % 52.56/52.85 (define @t391 () (forall @t32 @t390)) % 52.56/52.85 (define @t392 () (not @t391)) % 52.56/52.85 (define @t393 () (or @t392 @t130)) % 52.56/52.85 (define @t394 () (lambda @t131 @t393)) % 52.56/52.85 (define @t395 () (or @t383 @t327)) % 52.56/52.85 (define @t396 () (or @t112 @t384 @t395)) % 52.56/52.85 (define @t397 () (forall @t386 @t396)) % 52.56/52.85 (define @t398 () (@list @t326)) % 52.56/52.85 (define @t399 () (forall @t398 @t396)) % 52.56/52.85 (define @t400 () (forall @t398 @t395)) % 52.56/52.85 (define @t401 () (@var "BOUND_VARIABLE_8095" $$unsorted)) % 52.56/52.85 (define @t402 () (@list @t401)) % 52.56/52.85 (define @t403 () (or @t112 @t384 @t400)) % 52.56/52.85 (define @t404 () (tptp.r @t401)) % 52.56/52.85 (define @t405 () (@list @t401)) % 52.56/52.85 (define @t406 () (forall @t405 (or (not (tptp.irel @t6 @t401)) @t404))) % 52.56/52.85 (define @t407 () (or @t112 @t384 @t406)) % 52.56/52.85 (define @t408 () (or @t384 @t406)) % 52.56/52.85 (define @t409 () (@list @t330)) % 52.56/52.85 (define @t410 () (or @t112 (_ @t233 @t6))) % 52.56/52.85 (define @t411 () (forall @t32 @t410)) % 52.56/52.85 (define @t412 () (not @t411)) % 52.56/52.85 (define @t413 () (lambda @t66 @t412)) % 52.56/52.85 (define @t414 () (not @t363)) % 52.56/52.85 (define @t415 () (not @t336)) % 52.56/52.85 (define @t416 () (or @t415 @t414 @t354)) % 52.56/52.85 (define @t417 () (forall @t334 (or (not (tptp.irel @t337 @t328)) @t333 @t329 @t327))) % 52.56/52.85 (define @t418 () (not @t417)) % 52.56/52.85 (define @t419 () (tptp.irel @t306 @t337)) % 52.56/52.85 (define @t420 () (not @t419)) % 52.56/52.85 (define @t421 () (or @t420 @t418)) % 52.56/52.85 (define @t422 () (not @t421)) % 52.56/52.85 (define @t423 () (tptp.irel @t311 @t337)) % 52.56/52.85 (define @t424 () (or @t313 @t420 @t423)) % 52.56/52.85 (define @t425 () (@quantifiers_skolemize @t338 2)) % 52.56/52.85 (define @t426 () (tptp.r @t425)) % 52.56/52.85 (define @t427 () (tptp.irel @t339 @t425)) % 52.56/52.85 (define @t428 () (not @t427)) % 52.56/52.85 (define @t429 () (forall @t332 (or (not (tptp.irel @t339 @t330)) @t331))) % 52.56/52.85 (define @t430 () (not @t429)) % 52.56/52.85 (define @t431 () (tptp.irel @t337 @t339)) % 52.56/52.85 (define @t432 () (not @t431)) % 52.56/52.85 (define @t433 () (or @t432 @t430 @t428 @t426)) % 52.56/52.85 (define @t434 () (not @t338)) % 52.56/52.85 (define @t435 () (not @t423)) % 52.56/52.85 (define @t436 () (or @t435 @t434)) % 52.56/52.85 (define @t437 () (forall @t87 (or (not (tptp.irel @t339 @t85)) @t86))) % 52.56/52.85 (define @t438 () (not @t437)) % 52.56/52.85 (define @t439 () (or @t438 @t428 @t426)) % 52.56/52.85 (define @t440 () (@quantifiers_skolemize @t338 1)) % 52.56/52.85 (define @t441 () (forall @t92 (or (not (tptp.irel @t339 @t90)) @t91))) % 52.56/52.85 (define @t442 () (not @t441)) % 52.56/52.85 (define @t443 () (or @t442 (not (tptp.irel @t339 @t440)) (tptp.q @t440))) % 52.56/52.85 (define @t444 () (and @t443 @t439)) % 52.56/52.85 (define @t445 () (or @t432 @t444)) % 52.56/52.85 (define @t446 () (not @t445)) % 52.56/52.85 (define @t447 () (or @t420 @t432 @t342)) % 52.56/52.85 (define @t448 () (not @t307)) % 52.56/52.85 (define @t449 () (forall @t42 @t63)) % 52.56/52.85 (assume @p1 (forall @t3 (_ @t2 @t1))) % 52.56/52.85 (assume @p2 @t11) % 52.56/52.85 (assume @p3 (= tptp.ifalse (_ tptp.inot tptp.itrue))) % 52.56/52.85 (assume @p4 (_ tptp.ivalid @t12)) % 52.56/52.85 (assume @p5 (_ tptp.ivalid (_ (_ tptp.iimplies (_ tptp.inot @t14)) @t13))) % 52.56/52.85 (assume @p6 @t15) % 52.56/52.85 (assume @p7 true) % 52.56/52.85 (step @p8 (= tptp.mnot @t19) :rule refl :args (@t19)) % 52.56/52.85 (step @p9 (= tptp.mor @t23) :rule refl :args (@t23)) % 52.56/52.85 (step @p10 (= tptp.mand @t24) :rule refl :args (@t24)) % 52.56/52.85 (step @p11 (= tptp.mimplies @t29) :rule refl :args (@t29)) % 52.56/52.85 (step @p12 (= tptp.mbox_s4 @t35) :rule refl :args (@t35)) % 52.56/52.85 (step @p13 (= tptp.iatom @t38) :rule refl :args (@t38)) % 52.56/52.85 (step @p14 (= tptp.inot @t40) :rule refl :args (@t40)) % 52.56/52.85 (step @p15 (= tptp.itrue @t43) :rule refl :args (@t43)) % 52.56/52.85 (step @p16 (= tptp.iand @t46) :rule refl :args (@t46)) % 52.56/52.85 (step @p17 (= tptp.ior @t48) :rule refl :args (@t48)) % 52.56/52.85 (step @p18 (= tptp.iimplies @t49) :rule refl :args (@t49)) % 52.56/52.85 (step @p19 (= tptp.iimplied @t51) :rule refl :args (@t51)) % 52.56/52.85 (step @p20 (= tptp.iequiv @t52) :rule refl :args (@t52)) % 52.56/52.85 (step @p21 (= tptp.ixor @t53) :rule refl :args (@t53)) % 52.56/52.85 (step @p22 (= tptp.ivalid @t58) :rule refl :args (@t58)) % 52.56/52.85 (step @p23 (= tptp.isatisfiable @t59) :rule refl :args (@t59)) % 52.56/52.85 (step @p24 (= tptp.icountersatisfiable @t61) :rule refl :args (@t61)) % 52.56/52.85 (step @p25 (= tptp.iinvalid @t62) :rule refl :args (@t62)) % 52.56/52.85 (step @p26 :rule refl :args (@t63)) % 52.56/52.85 (step @p27 :rule refl :args (@t64)) % 52.56/52.85 (step @p28 :rule cong :premises (@p27 @p26) :args ((= @t64 @t63))) % 52.56/52.85 (step @p29 :rule symm :premises (@p28)) % 52.56/52.85 (step @p30 :rule eq_resolve :premises (@p27 @p29)) % 52.56/52.85 (step @p31 :rule cong :premises (@p30) :args ((forall @t42 @t64))) % 52.56/52.85 (step @p32 :rule beta-reduce :args ((= @t68 @t64))) % 52.56/52.85 (step @p33 :rule cong :premises (@p32) :args (@t69)) % 52.56/52.85 (step @p34 :rule trans :premises (@p33 @p31)) % 52.56/52.85 (step @p35 :rule beta-reduce :args ((= (_ @t71 @t67) @t69))) % 52.56/52.85 (step @p36 :rule trans :premises (@p35 @p34)) % 52.56/52.85 (step @p37 :rule beta-reduce :args ((= @t72 @t67))) % 52.56/52.85 (step @p38 :rule refl :args (@t71)) % 52.56/52.85 (step @p39 :rule ho_cong :premises (@p38 @p37)) % 52.56/52.85 (step @p40 :rule trans :premises (@p39 @p36)) % 52.56/52.85 (step @p41 :rule refl :args (tptp.s)) % 52.56/52.85 (step @p42 :rule ho_cong :premises (@p13 @p41)) % 52.56/52.85 (step @p43 :rule refl :args (@t70)) % 52.56/52.85 (step @p44 :rule refl :args (@t55)) % 52.56/52.85 (step @p45 :rule cong :premises (@p44 @p43) :args ((= @t55 @t70))) % 52.56/52.85 (step @p46 :rule symm :premises (@p45)) % 52.56/52.85 (step @p47 :rule eq_resolve :premises (@p44 @p46)) % 52.56/52.85 (step @p48 :rule cong :premises (@p47) :args (@t56)) % 52.56/52.85 (step @p49 :rule cong :premises (@p48) :args (@t58)) % 52.56/52.85 (step @p50 :rule trans :premises (@p22 @p49)) % 52.56/52.85 (step @p51 :rule ho_cong :premises (@p50 @p42)) % 52.56/52.85 (step @p52 :rule trans :premises (@p51 @p40)) % 52.56/52.85 (step @p53 :rule eq_resolve :premises (@p4 @p52)) % 52.56/52.85 (step @p54 :rule aci_norm :args ((= @t100 @t98))) % 52.56/52.85 (step @p55 :rule cong :premises (@p54) :args (@t102)) % 52.56/52.85 (step @p56 :rule quant-merge-prenex :args ((= (forall @t42 @t104) @t102))) % 52.56/52.85 (step @p57 :rule alpha_equiv :args (@t105 (@list @t73) @t106)) % 52.56/52.85 (step @p58 :rule refl :args (@t97)) % 52.56/52.85 (step @p59 :rule nary_cong :premises (@p58 @p57) :args (@t107)) % 52.56/52.85 (step @p60 :rule quant-miniscope-or :args ((= @t104 @t107))) % 52.56/52.85 (step @p61 :rule trans :premises (@p60 @p59)) % 52.56/52.85 (step @p62 :rule symm :premises (@p61)) % 52.56/52.85 (step @p63 :rule cong :premises (@p62) :args ((forall @t42 @t111))) % 52.56/52.85 (step @p64 :rule trans :premises (@p63 @p56)) % 52.56/52.85 (step @p65 :rule trans :premises (@p64 @p55)) % 52.56/52.85 (step @p66 :rule beta-reduce :args ((= @t115 @t111))) % 52.56/52.85 (step @p67 :rule cong :premises (@p66) :args (@t116)) % 52.56/52.85 (step @p68 :rule trans :premises (@p67 @p65)) % 52.56/52.85 (step @p69 :rule beta-reduce :args ((= (_ @t71 @t114) @t116))) % 52.56/52.85 (step @p70 :rule trans :premises (@p69 @p68)) % 52.56/52.85 (step @p71 :rule refl :args (@t108)) % 52.56/52.85 (step @p72 :rule refl :args (@t117)) % 52.56/52.85 (step @p73 :rule cong :premises (@p72 @p71) :args ((= @t117 @t108))) % 52.56/52.85 (step @p74 :rule symm :premises (@p73)) % 52.56/52.85 (step @p75 :rule eq_resolve :premises (@p72 @p74)) % 52.56/52.85 (step @p76 :rule refl :args (@t109)) % 52.56/52.85 (step @p77 :rule nary_cong :premises (@p76 @p75) :args (@t118)) % 52.56/52.85 (step @p78 :rule refl :args (@t112)) % 52.56/52.85 (step @p79 :rule nary_cong :premises (@p78 @p77) :args (@t119)) % 52.56/52.85 (step @p80 :rule cong :premises (@p79) :args ((forall @t32 @t119))) % 52.56/52.85 (step @p81 :rule beta-reduce :args ((= (_ (lambda @t66 (and (not (forall @t79 (or (not (tptp.irel @t25 @t76)) @t78))) @t65)) @t6) @t118))) % 52.56/52.85 (step @p82 :rule refl :args (@t6)) % 52.56/52.85 (step @p83 :rule refl :args (@t65)) % 52.56/52.85 (step @p84 :rule alpha_equiv :args (@t121 @t106 (@list @t76))) % 52.56/52.85 (step @p85 :rule cong :premises (@p84) :args (@t122)) % 52.56/52.85 (step @p86 :rule nary_cong :premises (@p85 @p83) :args (@t123)) % 52.56/52.85 (step @p87 :rule cong :premises (@p86) :args (@t124)) % 52.56/52.85 (step @p88 :rule ho_cong :premises (@p87 @p82)) % 52.56/52.85 (step @p89 :rule trans :premises (@p88 @p81)) % 52.56/52.85 (step @p90 :rule refl :args (@t112)) % 52.56/52.85 (step @p91 :rule nary_cong :premises (@p90 @p89) :args (@t125)) % 52.56/52.85 (step @p92 :rule cong :premises (@p91) :args (@t126)) % 52.56/52.85 (step @p93 :rule trans :premises (@p92 @p80)) % 52.56/52.85 (step @p94 :rule refl :args (@t113)) % 52.56/52.85 (step @p95 :rule nary_cong :premises (@p94 @p93) :args (@t127)) % 52.56/52.85 (step @p96 :rule cong :premises (@p95) :args (@t128)) % 52.56/52.85 (step @p97 :rule beta-reduce :args ((= (_ (lambda @t131 (or @t113 @t130)) @t124) @t128))) % 52.56/52.85 (step @p98 :rule trans :premises (@p97 @p96)) % 52.56/52.85 (step @p99 :rule beta-reduce :args ((= @t132 @t65))) % 52.56/52.85 (step @p100 :rule refl :args (@t122)) % 52.56/52.85 (step @p101 :rule nary_cong :premises (@p100 @p99) :args (@t133)) % 52.56/52.85 (step @p102 :rule cong :premises (@p101) :args (@t134)) % 52.56/52.85 (step @p103 :rule beta-reduce :args ((= (_ (lambda @t131 (and @t122 @t135)) @t67) @t134))) % 52.56/52.85 (step @p104 :rule trans :premises (@p103 @p102)) % 52.56/52.85 (step @p105 :rule aci_norm :args ((= (and @t65 @t65) @t65))) % 52.56/52.85 (step @p106 :rule refl :args (@t65)) % 52.56/52.85 (step @p107 :rule nary_cong :premises (@p106 @p99) :args (@t136)) % 52.56/52.85 (step @p108 :rule trans :premises (@p107 @p105)) % 52.56/52.85 (step @p109 :rule cong :premises (@p108) :args (@t137)) % 52.56/52.85 (step @p110 :rule beta-reduce :args ((= (_ (lambda @t131 (and @t65 @t135)) @t67) @t137))) % 52.56/52.85 (step @p111 :rule trans :premises (@p110 @p109)) % 52.56/52.85 (step @p112 :rule refl :args (@t135)) % 52.56/52.85 (step @p113 :rule nary_cong :premises (@p99 @p112) :args (@t138)) % 52.56/52.85 (step @p114 :rule cong :premises (@p113) :args (@t139)) % 52.56/52.85 (step @p115 :rule beta-reduce :args ((= (_ @t141 @t67) @t139))) % 52.56/52.85 (step @p116 :rule trans :premises (@p115 @p114)) % 52.56/52.85 (step @p117 :rule refl :args (@t141)) % 52.56/52.85 (step @p118 :rule ho_cong :premises (@p117 @p37)) % 52.56/52.85 (step @p119 :rule trans :premises (@p118 @p116)) % 52.56/52.85 (step @p120 :rule ho_cong :premises (@p119 @p37)) % 52.56/52.85 (step @p121 :rule trans :premises (@p120 @p111)) % 52.56/52.85 (step @p122 :rule beta-reduce :args ((= @t143 @t122))) % 52.56/52.85 (step @p123 :rule nary_cong :premises (@p122 @p112) :args (@t144)) % 52.56/52.85 (step @p124 :rule cong :premises (@p123) :args (@t145)) % 52.56/52.85 (step @p125 :rule beta-reduce :args ((= (_ @t141 @t142) @t145))) % 52.56/52.85 (step @p126 :rule trans :premises (@p125 @p124)) % 52.56/52.85 (step @p127 :rule beta-reduce :args ((= (_ (lambda @t66 (not (forall @t77 (or (not (tptp.irel @t25 @t74)) @t75)))) @t6) @t120))) % 52.56/52.85 (step @p128 :rule alpha_equiv :args (@t147 @t106 @t148)) % 52.56/52.85 (step @p129 :rule cong :premises (@p128) :args (@t149)) % 52.56/52.85 (step @p130 :rule cong :premises (@p129) :args (@t150)) % 52.56/52.85 (step @p131 :rule ho_cong :premises (@p130 @p82)) % 52.56/52.85 (step @p132 :rule trans :premises (@p131 @p127)) % 52.56/52.85 (step @p133 :rule nary_cong :premises (@p90 @p132) :args (@t151)) % 52.56/52.85 (step @p134 :rule cong :premises (@p133) :args (@t152)) % 52.56/52.85 (step @p135 :rule cong :premises (@p134) :args (@t153)) % 52.56/52.85 (step @p136 :rule cong :premises (@p135) :args (@t154)) % 52.56/52.85 (step @p137 :rule beta-reduce :args ((= (_ @t158 @t150) @t154))) % 52.56/52.85 (step @p138 :rule trans :premises (@p137 @p136)) % 52.56/52.85 (step @p139 :rule refl :args (@t146)) % 52.56/52.85 (step @p140 :rule refl :args (@t159)) % 52.56/52.85 (step @p141 :rule cong :premises (@p140 @p139) :args ((= @t159 @t146))) % 52.56/52.85 (step @p142 :rule symm :premises (@p141)) % 52.56/52.85 (step @p143 :rule eq_resolve :premises (@p140 @p142)) % 52.56/52.85 (step @p144 :rule nary_cong :premises (@p78 @p143) :args (@t160)) % 52.56/52.85 (step @p145 :rule cong :premises (@p144) :args ((forall @t32 @t160))) % 52.56/52.85 (step @p146 :rule beta-reduce :args ((= @t162 @t159))) % 52.56/52.85 (step @p147 :rule nary_cong :premises (@p90 @p146) :args (@t163)) % 52.56/52.85 (step @p148 :rule cong :premises (@p147) :args (@t164)) % 52.56/52.85 (step @p149 :rule trans :premises (@p148 @p145)) % 52.56/52.85 (step @p150 :rule cong :premises (@p149) :args (@t165)) % 52.56/52.85 (step @p151 :rule cong :premises (@p150) :args (@t166)) % 52.56/52.85 (step @p152 :rule beta-reduce :args ((= (_ @t158 @t161) @t166))) % 52.56/52.85 (step @p153 :rule trans :premises (@p152 @p151)) % 52.56/52.85 (step @p154 :rule beta-reduce :args ((= @t167 @t161))) % 52.56/52.85 (step @p155 :rule refl :args (@t158)) % 52.56/52.85 (step @p156 :rule ho_cong :premises (@p155 @p154)) % 52.56/52.85 (step @p157 :rule trans :premises (@p156 @p153)) % 52.56/52.85 (step @p158 :rule ho_cong :premises (@p155 @p157)) % 52.56/52.85 (step @p159 :rule trans :premises (@p158 @p138)) % 52.56/52.85 (step @p160 :rule ho_cong :premises (@p117 @p159)) % 52.56/52.85 (step @p161 :rule trans :premises (@p160 @p126)) % 52.56/52.85 (step @p162 :rule ho_cong :premises (@p161 @p121)) % 52.56/52.85 (step @p163 :rule trans :premises (@p162 @p104)) % 52.56/52.85 (step @p164 :rule refl :args (@t130)) % 52.56/52.85 (step @p165 :rule beta-reduce :args ((= (_ (lambda @t66 (not (forall @t94 (or (not (tptp.irel @t25 @t84)) @t93)))) @t6) @t95))) % 52.56/52.85 (step @p166 :rule alpha_equiv :args (@t175 @t106 (@list @t84))) % 52.56/52.85 (step @p167 :rule cong :premises (@p166) :args (@t176)) % 52.56/52.85 (step @p168 :rule cong :premises (@p167) :args (@t177)) % 52.56/52.85 (step @p169 :rule ho_cong :premises (@p168 @p82)) % 52.56/52.85 (step @p170 :rule trans :premises (@p169 @p165)) % 52.56/52.85 (step @p171 :rule nary_cong :premises (@p90 @p170) :args (@t178)) % 52.56/52.85 (step @p172 :rule cong :premises (@p171) :args (@t179)) % 52.56/52.85 (step @p173 :rule cong :premises (@p172) :args (@t180)) % 52.56/52.85 (step @p174 :rule nary_cong :premises (@p173 @p164) :args (@t181)) % 52.56/52.85 (step @p175 :rule cong :premises (@p174) :args (@t182)) % 52.56/52.85 (step @p176 :rule beta-reduce :args ((= (_ @t184 @t177) @t182))) % 52.56/52.85 (step @p177 :rule trans :premises (@p176 @p175)) % 52.56/52.85 (step @p178 :rule aci_norm :args ((= @t186 @t170))) % 52.56/52.85 (step @p179 :rule aci_norm :args ((= @t188 @t173))) % 52.56/52.85 (step @p180 :rule nary_cong :premises (@p179 @p178) :args (@t189)) % 52.56/52.85 (step @p181 :rule nary_cong :premises (@p90 @p180) :args (@t190)) % 52.56/52.85 (step @p182 :rule cong :premises (@p181) :args (@t191)) % 52.56/52.85 (step @p183 :rule quant-merge-prenex :args ((= (forall @t32 @t193) @t191))) % 52.56/52.85 (step @p184 :rule alpha_equiv :args (@t195 (@list @t82) @t197)) % 52.56/52.85 (step @p185 :rule refl :args (@t169)) % 52.56/52.85 (step @p186 :rule nary_cong :premises (@p185 @p184) :args (@t198)) % 52.56/52.85 (step @p187 :rule quant-miniscope-or :args ((= @t199 @t198))) % 52.56/52.85 (step @p188 :rule quant-unused-vars :args ((= @t200 @t199))) % 52.56/52.85 (step @p189 :rule trans :premises (@p188 @p187)) % 52.56/52.85 (step @p190 :rule trans :premises (@p189 @p186)) % 52.56/52.85 (step @p191 :rule alpha_equiv :args (@t202 (@list @t88) @t204)) % 52.56/52.85 (step @p192 :rule refl :args (@t172)) % 52.56/52.85 (step @p193 :rule nary_cong :premises (@p192 @p191) :args (@t205)) % 52.56/52.85 (step @p194 :rule quant-miniscope-or :args ((= @t206 @t205))) % 52.56/52.85 (step @p195 :rule quant-unused-vars :args ((= @t207 @t206))) % 52.56/52.85 (step @p196 :rule trans :premises (@p195 @p194)) % 52.56/52.85 (step @p197 :rule trans :premises (@p196 @p193)) % 52.56/52.85 (step @p198 :rule nary_cong :premises (@p197 @p190) :args (@t208)) % 52.56/52.85 (step @p199 :rule quant-miniscope-and :args ((= @t209 @t208))) % 52.56/52.85 (step @p200 :rule trans :premises (@p199 @p198)) % 52.56/52.85 (step @p201 :rule nary_cong :premises (@p78 @p200) :args (@t210)) % 52.56/52.85 (step @p202 :rule quant-miniscope-or :args ((= @t193 @t210))) % 52.56/52.85 (step @p203 :rule trans :premises (@p202 @p201)) % 52.56/52.85 (step @p204 :rule symm :premises (@p203)) % 52.56/52.85 (step @p205 :rule cong :premises (@p204) :args ((forall @t32 (or @t112 @t215)))) % 52.56/52.85 (step @p206 :rule trans :premises (@p205 @p183)) % 52.56/52.85 (step @p207 :rule trans :premises (@p206 @p182)) % 52.56/52.85 (step @p208 :rule beta-reduce :args ((= (_ (lambda @t66 (and (or (not (forall @t92 (or (not (tptp.irel @t25 @t90)) @t91))) (forall @t214 (or (not (tptp.irel @t25 @t203)) @t213))) (or (not (forall @t87 (or (not (tptp.irel @t25 @t85)) @t86))) (forall @t212 (or (not (tptp.irel @t25 @t196)) @t211))))) @t6) @t215))) % 52.56/52.85 (step @p209 :rule alpha_equiv :args (@t217 @t106 @t197)) % 52.56/52.85 (step @p210 :rule alpha_equiv :args (@t219 @t106 @t220)) % 52.56/52.85 (step @p211 :rule cong :premises (@p210) :args (@t221)) % 52.56/52.85 (step @p212 :rule nary_cong :premises (@p211 @p209) :args (@t222)) % 52.56/52.85 (step @p213 :rule alpha_equiv :args (@t224 @t106 @t204)) % 52.56/52.85 (step @p214 :rule alpha_equiv :args (@t147 @t106 @t225)) % 52.56/52.85 (step @p215 :rule cong :premises (@p214) :args (@t149)) % 52.56/52.85 (step @p216 :rule nary_cong :premises (@p215 @p213) :args (@t226)) % 52.56/52.85 (step @p217 :rule nary_cong :premises (@p216 @p212) :args (@t227)) % 52.56/52.85 (step @p218 :rule cong :premises (@p217) :args (@t228)) % 52.56/52.85 (step @p219 :rule ho_cong :premises (@p218 @p82)) % 52.56/52.85 (step @p220 :rule trans :premises (@p219 @p208)) % 52.56/52.85 (step @p221 :rule nary_cong :premises (@p90 @p220) :args (@t229)) % 52.56/52.85 (step @p222 :rule cong :premises (@p221) :args (@t230)) % 52.56/52.85 (step @p223 :rule trans :premises (@p222 @p207)) % 52.56/52.85 (step @p224 :rule cong :premises (@p223) :args (@t231)) % 52.56/52.85 (step @p225 :rule cong :premises (@p224) :args (@t232)) % 52.56/52.85 (step @p226 :rule beta-reduce :args ((= (_ @t158 @t228) @t232))) % 52.56/52.85 (step @p227 :rule trans :premises (@p226 @p225)) % 52.56/52.85 (step @p228 :rule beta-reduce :args ((= @t234 @t222))) % 52.56/52.85 (step @p229 :rule refl :args (@t226)) % 52.56/52.85 (step @p230 :rule nary_cong :premises (@p229 @p228) :args (@t235)) % 52.56/52.85 (step @p231 :rule cong :premises (@p230) :args (@t236)) % 52.56/52.85 (step @p232 :rule beta-reduce :args ((= (_ (lambda @t131 (and @t226 @t135)) @t233) @t236))) % 52.56/52.85 (step @p233 :rule trans :premises (@p232 @p231)) % 52.56/52.85 (step @p234 :rule refl :args (@t216)) % 52.56/52.85 (step @p235 :rule refl :args (@t237)) % 52.56/52.85 (step @p236 :rule cong :premises (@p235 @p234) :args ((= @t237 @t216))) % 52.56/52.85 (step @p237 :rule symm :premises (@p236)) % 52.56/52.85 (step @p238 :rule eq_resolve :premises (@p235 @p237)) % 52.56/52.85 (step @p239 :rule nary_cong :premises (@p78 @p238) :args (@t238)) % 52.56/52.85 (step @p240 :rule cong :premises (@p239) :args ((forall @t32 @t238))) % 52.56/52.85 (step @p241 :rule beta-reduce :args ((= @t240 @t237))) % 52.56/52.85 (step @p242 :rule nary_cong :premises (@p90 @p241) :args (@t241)) % 52.56/52.85 (step @p243 :rule cong :premises (@p242) :args (@t242)) % 52.56/52.85 (step @p244 :rule trans :premises (@p243 @p240)) % 52.56/52.85 (step @p245 :rule refl :args (@t221)) % 52.56/52.85 (step @p246 :rule nary_cong :premises (@p245 @p244) :args (@t243)) % 52.56/52.85 (step @p247 :rule cong :premises (@p246) :args (@t244)) % 52.56/52.85 (step @p248 :rule beta-reduce :args ((= (_ (lambda @t131 (or @t221 @t130)) @t239) @t244))) % 52.56/52.85 (step @p249 :rule trans :premises (@p248 @p247)) % 52.56/52.85 (step @p250 :rule beta-reduce :args ((= @t245 @t239))) % 52.56/52.85 (step @p251 :rule refl :args (@t218)) % 52.56/52.85 (step @p252 :rule refl :args (@t246)) % 52.56/52.85 (step @p253 :rule cong :premises (@p252 @p251) :args ((= @t246 @t218))) % 52.56/52.85 (step @p254 :rule symm :premises (@p253)) % 52.56/52.85 (step @p255 :rule eq_resolve :premises (@p252 @p254)) % 52.56/52.85 (step @p256 :rule nary_cong :premises (@p78 @p255) :args (@t247)) % 52.56/52.85 (step @p257 :rule cong :premises (@p256) :args ((forall @t32 @t247))) % 52.56/52.85 (step @p258 :rule beta-reduce :args ((= @t249 @t246))) % 52.56/52.85 (step @p259 :rule nary_cong :premises (@p90 @p258) :args (@t250)) % 52.56/52.85 (step @p260 :rule cong :premises (@p259) :args (@t251)) % 52.56/52.85 (step @p261 :rule trans :premises (@p260 @p257)) % 52.56/52.85 (step @p262 :rule cong :premises (@p261) :args (@t252)) % 52.56/52.85 (step @p263 :rule nary_cong :premises (@p262 @p164) :args (@t253)) % 52.56/52.85 (step @p264 :rule cong :premises (@p263) :args (@t254)) % 52.56/52.85 (step @p265 :rule beta-reduce :args ((= (_ @t184 @t248) @t254))) % 52.56/52.85 (step @p266 :rule trans :premises (@p265 @p264)) % 52.56/52.85 (step @p267 :rule beta-reduce :args ((= @t255 @t248))) % 52.56/52.85 (step @p268 :rule refl :args (@t184)) % 52.56/52.85 (step @p269 :rule ho_cong :premises (@p268 @p267)) % 52.56/52.85 (step @p270 :rule trans :premises (@p269 @p266)) % 52.56/52.85 (step @p271 :rule ho_cong :premises (@p270 @p250)) % 52.56/52.85 (step @p272 :rule trans :premises (@p271 @p249)) % 52.56/52.85 (step @p273 :rule beta-reduce :args ((= @t257 @t226))) % 52.56/52.85 (step @p274 :rule nary_cong :premises (@p273 @p112) :args (@t258)) % 52.56/52.85 (step @p275 :rule cong :premises (@p274) :args (@t259)) % 52.56/52.85 (step @p276 :rule beta-reduce :args ((= (_ @t141 @t256) @t259))) % 52.56/52.85 (step @p277 :rule trans :premises (@p276 @p275)) % 52.56/52.85 (step @p278 :rule refl :args (@t223)) % 52.56/52.85 (step @p279 :rule refl :args (@t260)) % 52.56/52.85 (step @p280 :rule cong :premises (@p279 @p278) :args ((= @t260 @t223))) % 52.56/52.85 (step @p281 :rule symm :premises (@p280)) % 52.56/52.85 (step @p282 :rule eq_resolve :premises (@p279 @p281)) % 52.56/52.85 (step @p283 :rule nary_cong :premises (@p78 @p282) :args (@t261)) % 52.56/52.85 (step @p284 :rule cong :premises (@p283) :args ((forall @t32 @t261))) % 52.56/52.85 (step @p285 :rule beta-reduce :args ((= @t263 @t260))) % 52.56/52.85 (step @p286 :rule nary_cong :premises (@p90 @p285) :args (@t264)) % 52.56/52.85 (step @p287 :rule cong :premises (@p286) :args (@t265)) % 52.56/52.85 (step @p288 :rule trans :premises (@p287 @p284)) % 52.56/52.85 (step @p289 :rule refl :args (@t149)) % 52.56/52.85 (step @p290 :rule nary_cong :premises (@p289 @p288) :args (@t266)) % 52.56/52.85 (step @p291 :rule cong :premises (@p290) :args (@t267)) % 52.56/52.85 (step @p292 :rule beta-reduce :args ((= (_ (lambda @t131 (or @t149 @t130)) @t262) @t267))) % 52.56/52.85 (step @p293 :rule trans :premises (@p292 @p291)) % 52.56/52.85 (step @p294 :rule beta-reduce :args ((= @t268 @t262))) % 52.56/52.85 (step @p295 :rule nary_cong :premises (@p150 @p164) :args (@t269)) % 52.56/52.85 (step @p296 :rule cong :premises (@p295) :args (@t270)) % 52.56/52.85 (step @p297 :rule beta-reduce :args ((= (_ @t184 @t161) @t270))) % 52.56/52.85 (step @p298 :rule trans :premises (@p297 @p296)) % 52.56/52.85 (step @p299 :rule ho_cong :premises (@p268 @p154)) % 52.56/52.85 (step @p300 :rule trans :premises (@p299 @p298)) % 52.56/52.85 (step @p301 :rule ho_cong :premises (@p300 @p294)) % 52.56/52.85 (step @p302 :rule trans :premises (@p301 @p293)) % 52.56/52.85 (step @p303 :rule ho_cong :premises (@p117 @p302)) % 52.56/52.85 (step @p304 :rule trans :premises (@p303 @p277)) % 52.56/52.85 (step @p305 :rule ho_cong :premises (@p304 @p272)) % 52.56/52.85 (step @p306 :rule trans :premises (@p305 @p233)) % 52.56/52.85 (step @p307 :rule ho_cong :premises (@p155 @p306)) % 52.56/52.85 (step @p308 :rule trans :premises (@p307 @p227)) % 52.56/52.85 (step @p309 :rule ho_cong :premises (@p268 @p308)) % 52.56/52.85 (step @p310 :rule trans :premises (@p309 @p177)) % 52.56/52.85 (step @p311 :rule ho_cong :premises (@p310 @p163)) % 52.56/52.85 (step @p312 :rule trans :premises (@p311 @p98)) % 52.56/52.85 (step @p313 :rule ho_cong :premises (@p38 @p312)) % 52.56/52.85 (step @p314 :rule trans :premises (@p313 @p70)) % 52.56/52.85 (step @p315 :rule cong :premises (@p314) :args ((not (_ @t71 (_ (_ @t184 (_ @t158 (_ (_ @t141 (_ (_ @t184 @t167) @t268)) (_ (_ @t184 @t255) @t245)))) (_ (_ @t141 (_ @t158 (_ @t158 @t167))) (_ (_ @t141 @t72) @t72))))))) % 52.56/52.85 (step @p316 :rule beta-reduce :args ((= (_ @t273 @t25) @t140))) % 52.56/52.85 (step @p317 :rule refl :args (@t25)) % 52.56/52.85 (step @p318 :rule beta-reduce :args ((= (_ @t275 @t44) @t273))) % 52.56/52.85 (step @p319 :rule refl :args (@t44)) % 52.56/52.85 (step @p320 :rule beta-reduce :args ((= (_ @t24 @t30) @t275))) % 52.56/52.85 (step @p321 :rule ho_cong :premises (@p320 @p319)) % 52.56/52.85 (step @p322 :rule trans :premises (@p321 @p318)) % 52.56/52.85 (step @p323 :rule ho_cong :premises (@p322 @p317)) % 52.56/52.85 (step @p324 :rule trans :premises (@p323 @p316)) % 52.56/52.85 (step @p325 :rule refl :args (@t30)) % 52.56/52.85 (step @p326 :rule ho_cong :premises (@p10 @p325)) % 52.56/52.85 (step @p327 :rule ho_cong :premises (@p326 @p319)) % 52.56/52.85 (step @p328 :rule ho_cong :premises (@p327 @p317)) % 52.56/52.85 (step @p329 :rule trans :premises (@p328 @p324)) % 52.56/52.85 (step @p330 :rule cong :premises (@p329) :args (@t46)) % 52.56/52.85 (step @p331 :rule trans :premises (@p16 @p330)) % 52.56/52.85 (step @p332 :rule ho_cong :premises (@p331 @p42)) % 52.56/52.85 (step @p333 :rule ho_cong :premises (@p332 @p42)) % 52.56/52.85 (step @p334 :rule refl :args (tptp.p)) % 52.56/52.85 (step @p335 :rule ho_cong :premises (@p13 @p334)) % 52.56/52.85 (step @p336 :rule beta-reduce :args ((= (_ (lambda @t272 (not @t276)) @t25) @t157))) % 52.56/52.85 (step @p337 :rule beta-reduce :args ((= @t281 @t276))) % 52.56/52.85 (step @p338 :rule cong :premises (@p337) :args (@t282)) % 52.56/52.85 (step @p339 :rule cong :premises (@p338) :args (@t283)) % 52.56/52.85 (step @p340 :rule beta-reduce :args ((= (_ @t19 @t280) @t283))) % 52.56/52.85 (step @p341 :rule trans :premises (@p340 @p339)) % 52.56/52.85 (step @p342 :rule beta-reduce :args ((= (_ @t284 @t30) @t280))) % 52.56/52.85 (step @p343 :rule refl :args (@t19)) % 52.56/52.85 (step @p344 :rule ho_cong :premises (@p343 @p342)) % 52.56/52.85 (step @p345 :rule trans :premises (@p344 @p341)) % 52.56/52.85 (step @p346 :rule ho_cong :premises (@p345 @p317)) % 52.56/52.85 (step @p347 :rule trans :premises (@p346 @p336)) % 52.56/52.85 (step @p348 :rule refl :args (@t155)) % 52.56/52.85 (step @p349 :rule refl :args (@t31)) % 52.56/52.85 (step @p350 :rule cong :premises (@p349 @p348) :args ((= @t31 @t155))) % 52.56/52.85 (step @p351 :rule symm :premises (@p350)) % 52.56/52.85 (step @p352 :rule eq_resolve :premises (@p349 @p351)) % 52.56/52.85 (step @p353 :rule refl :args (@t277)) % 52.56/52.85 (step @p354 :rule refl :args (@t8)) % 52.56/52.85 (step @p355 :rule cong :premises (@p354 @p353) :args ((= @t8 @t277))) % 52.56/52.85 (step @p356 :rule symm :premises (@p355)) % 52.56/52.85 (step @p357 :rule eq_resolve :premises (@p354 @p356)) % 52.56/52.85 (step @p358 :rule cong :premises (@p357) :args (@t285)) % 52.56/52.85 (step @p359 :rule nary_cong :premises (@p358 @p352) :args (@t286)) % 52.56/52.85 (step @p360 :rule cong :premises (@p359) :args ((forall @t32 @t286))) % 52.56/52.85 (step @p361 :rule bool-impl-elim :args (@t8 @t31)) % 52.56/52.85 (step @p362 :rule cong :premises (@p361) :args (@t33)) % 52.56/52.85 (step @p363 :rule trans :premises (@p362 @p360)) % 52.56/52.85 (step @p364 :rule cong :premises (@p363) :args (@t35)) % 52.56/52.85 (step @p365 :rule trans :premises (@p12 @p364)) % 52.56/52.85 (step @p366 :rule ho_cong :premises (@p365 @p325)) % 52.56/52.85 (step @p367 :rule ho_cong :premises (@p8 @p366)) % 52.56/52.85 (step @p368 :rule ho_cong :premises (@p367 @p317)) % 52.56/52.85 (step @p369 :rule trans :premises (@p368 @p347)) % 52.56/52.85 (step @p370 :rule cong :premises (@p369) :args (@t40)) % 52.56/52.85 (step @p371 :rule trans :premises (@p14 @p370)) % 52.56/52.85 (step @p372 :rule ho_cong :premises (@p371 @p335)) % 52.56/52.85 (step @p373 :rule ho_cong :premises (@p371 @p372)) % 52.56/52.85 (step @p374 :rule ho_cong :premises (@p331 @p373)) % 52.56/52.85 (step @p375 :rule ho_cong :premises (@p374 @p333)) % 52.56/52.85 (step @p376 :rule refl :args (tptp.r)) % 52.56/52.85 (step @p377 :rule ho_cong :premises (@p13 @p376)) % 52.56/52.85 (step @p378 :rule refl :args (tptp.t)) % 52.56/52.85 (step @p379 :rule ho_cong :premises (@p13 @p378)) % 52.56/52.85 (step @p380 :rule beta-reduce :args ((= (_ (lambda @t66 @t183) @t25) @t183))) % 52.56/52.85 (step @p381 :rule beta-reduce :args ((= @t288 @t130))) % 52.56/52.85 (step @p382 :rule refl :args (@t157)) % 52.56/52.85 (step @p383 :rule nary_cong :premises (@p382 @p381) :args (@t289)) % 52.56/52.85 (step @p384 :rule cong :premises (@p383) :args (@t290)) % 52.56/52.85 (step @p385 :rule beta-reduce :args ((= (_ (lambda @t292 (or @t157 @t291)) @t287) @t290))) % 52.56/52.85 (step @p386 :rule trans :premises (@p385 @p384)) % 52.56/52.85 (step @p387 :rule beta-reduce :args ((= (_ @t284 @t44) @t287))) % 52.56/52.85 (step @p388 :rule refl :args (@t291)) % 52.56/52.85 (step @p389 :rule beta-reduce :args ((= @t293 @t156))) % 52.56/52.85 (step @p390 :rule cong :premises (@p389) :args (@t294)) % 52.56/52.85 (step @p391 :rule nary_cong :premises (@p390 @p388) :args (@t295)) % 52.56/52.85 (step @p392 :rule cong :premises (@p391) :args (@t296)) % 52.56/52.85 (step @p393 :rule beta-reduce :args ((= (_ @t298 @t280) @t296))) % 52.56/52.85 (step @p394 :rule trans :premises (@p393 @p392)) % 52.56/52.85 (step @p395 :rule refl :args (@t298)) % 52.56/52.85 (step @p396 :rule ho_cong :premises (@p395 @p342)) % 52.56/52.85 (step @p397 :rule trans :premises (@p396 @p394)) % 52.56/52.85 (step @p398 :rule ho_cong :premises (@p397 @p387)) % 52.56/52.85 (step @p399 :rule trans :premises (@p398 @p386)) % 52.56/52.85 (step @p400 :rule ho_cong :premises (@p399 @p317)) % 52.56/52.85 (step @p401 :rule trans :premises (@p400 @p380)) % 52.56/52.85 (step @p402 :rule ho_cong :premises (@p365 @p319)) % 52.56/52.85 (step @p403 :rule beta-reduce :args ((= (_ @t300 @t25) @t297))) % 52.56/52.85 (step @p404 :rule beta-reduce :args ((= (_ (lambda @t274 (or @t299 @t21)) @t26) @t300))) % 52.56/52.85 (step @p405 :rule refl :args (@t26)) % 52.56/52.85 (step @p406 :rule refl :args (@t21)) % 52.56/52.85 (step @p407 :rule beta-reduce :args ((= @t302 @t299))) % 52.56/52.85 (step @p408 :rule nary_cong :premises (@p407 @p406) :args (@t303)) % 52.56/52.85 (step @p409 :rule cong :premises (@p408) :args (@t304)) % 52.56/52.85 (step @p410 :rule beta-reduce :args ((= (_ @t23 @t301) @t304))) % 52.56/52.85 (step @p411 :rule trans :premises (@p410 @p409)) % 52.56/52.85 (step @p412 :rule beta-reduce :args ((= (_ @t19 @t27) @t301))) % 52.56/52.85 (step @p413 :rule refl :args (@t23)) % 52.56/52.85 (step @p414 :rule ho_cong :premises (@p413 @p412)) % 52.56/52.85 (step @p415 :rule trans :premises (@p414 @p411)) % 52.56/52.85 (step @p416 :rule ho_cong :premises (@p415 @p405)) % 52.56/52.85 (step @p417 :rule trans :premises (@p416 @p404)) % 52.56/52.85 (step @p418 :rule ho_cong :premises (@p417 @p317)) % 52.56/52.85 (step @p419 :rule trans :premises (@p418 @p403)) % 52.56/52.85 (step @p420 :rule refl :args (@t27)) % 52.56/52.85 (step @p421 :rule ho_cong :premises (@p8 @p420)) % 52.56/52.85 (step @p422 :rule ho_cong :premises (@p9 @p421)) % 52.56/52.85 (step @p423 :rule ho_cong :premises (@p422 @p405)) % 52.56/52.85 (step @p424 :rule ho_cong :premises (@p423 @p317)) % 52.56/52.85 (step @p425 :rule trans :premises (@p424 @p419)) % 52.56/52.85 (step @p426 :rule cong :premises (@p425) :args (@t29)) % 52.56/52.85 (step @p427 :rule trans :premises (@p11 @p426)) % 52.56/52.85 (step @p428 :rule ho_cong :premises (@p427 @p366)) % 52.56/52.85 (step @p429 :rule ho_cong :premises (@p428 @p402)) % 52.56/52.85 (step @p430 :rule ho_cong :premises (@p429 @p317)) % 52.56/52.85 (step @p431 :rule trans :premises (@p430 @p401)) % 52.56/52.85 (step @p432 :rule cong :premises (@p431) :args (@t49)) % 52.56/52.85 (step @p433 :rule trans :premises (@p18 @p432)) % 52.56/52.85 (step @p434 :rule ho_cong :premises (@p433 @p379)) % 52.56/52.85 (step @p435 :rule ho_cong :premises (@p434 @p377)) % 52.56/52.85 (step @p436 :rule refl :args (tptp.q)) % 52.56/52.85 (step @p437 :rule ho_cong :premises (@p13 @p436)) % 52.56/52.85 (step @p438 :rule ho_cong :premises (@p433 @p335)) % 52.56/52.85 (step @p439 :rule ho_cong :premises (@p438 @p437)) % 52.56/52.85 (step @p440 :rule ho_cong :premises (@p331 @p439)) % 52.56/52.85 (step @p441 :rule ho_cong :premises (@p440 @p435)) % 52.56/52.85 (step @p442 :rule ho_cong :premises (@p371 @p441)) % 52.56/52.85 (step @p443 :rule ho_cong :premises (@p433 @p442)) % 52.56/52.85 (step @p444 :rule ho_cong :premises (@p443 @p375)) % 52.56/52.85 (step @p445 :rule ho_cong :premises (@p50 @p444)) % 52.56/52.85 (step @p446 :rule cong :premises (@p445) :args (@t15)) % 52.56/52.85 (step @p447 :rule trans :premises (@p446 @p315)) % 52.56/52.85 (step @p448 :rule eq_resolve :premises (@p6 @p447)) % 52.56/52.85 (step @p449 :rule skolemize :premises (@p448)) % 52.56/52.85 (step @p450 :rule cnf_or_neg :args (@t316 2)) % 52.56/52.85 (step @p451 :rule chain_m_resolution :premises (@p450 @p449) :args ((not @t310) @t317 @t318)) % 52.56/52.85 (assume-push @p705 @t308) % 52.56/52.85 (step @p453 :rule instantiate :premises (@p705) :args ((@list @t320))) % 52.56/52.85 (step-pop @p706 :rule scope :premises (@p453)) % 52.56/52.85 (step @p454 :rule process_scope :premises (@p706) :args (@t325)) % 52.56/52.85 (step @p456 :rule implies_elim :premises (@p454)) % 52.56/52.85 (assume-push @p707 @t308) % 52.56/52.85 (step @p458 :rule instantiate :premises (@p707) :args ((@list @t339))) % 52.56/52.85 (step-pop @p708 :rule scope :premises (@p458)) % 52.56/52.85 (step @p459 :rule process_scope :premises (@p708) :args (@t344)) % 52.56/52.85 (step @p461 :rule implies_elim :premises (@p459)) % 52.56/52.85 (step @p462 :rule bool-double-not-elim :args (@t314)) % 52.56/52.85 (step @p463 :rule refl :args (@t316)) % 52.56/52.85 (step @p464 :rule nary_cong :premises (@p463 @p462) :args ((or @t316 (not @t315)))) % 52.56/52.85 (step @p465 :rule cnf_or_neg :args (@t316 0)) % 52.56/52.85 (step @p466 :rule eq_resolve :premises (@p465 @p464)) % 52.56/52.85 (step @p467 :rule reordering :premises (@p466) :args ((or @t314 @t316))) % 52.56/52.85 (step @p468 :rule chain_m_resolution :premises (@p467 @p449) :args (@t314 @t317 @t318)) % 52.56/52.85 (step @p469 :rule instantiate :premises (@p468) :args (@t345)) % 52.56/52.85 (step @p470 :rule bool-double-not-elim :args (@t312)) % 52.56/52.85 (step @p471 :rule nary_cong :premises (@p463 @p470) :args ((or @t316 (not @t313)))) % 52.56/52.85 (step @p472 :rule cnf_or_neg :args (@t316 1)) % 52.56/52.85 (step @p473 :rule eq_resolve :premises (@p472 @p471)) % 52.56/52.85 (step @p474 :rule reordering :premises (@p473) :args ((or @t312 @t316))) % 52.56/52.85 (step @p475 :rule chain_m_resolution :premises (@p474 @p449) :args (@t312 @t317 @t318)) % 52.56/52.85 (step @p476 :rule cnf_or_pos :args (@t347)) % 52.56/52.85 (step @p477 :rule reordering :premises (@p476) :args ((or @t313 @t346 (not @t347)))) % 52.56/52.85 (step @p478 :rule chain_m_resolution :premises (@p477 @p475 @p469) :args (@t346 (@list false false) (@list @t312 @t347))) % 52.56/52.85 (step @p479 :rule skolemize :premises (@p478)) % 52.56/52.85 (step @p480 :rule bool-double-not-elim :args (@t323)) % 52.56/52.85 (step @p481 :rule refl :args (@t352)) % 52.56/52.85 (step @p482 :rule nary_cong :premises (@p481 @p480) :args ((or @t352 (not @t324)))) % 52.56/52.85 (step @p483 :rule cnf_or_neg :args (@t352 0)) % 52.56/52.85 (step @p484 :rule eq_resolve :premises (@p483 @p482)) % 52.56/52.85 (step @p485 :rule reordering :premises (@p484) :args ((or @t323 @t352))) % 52.56/52.85 (step @p486 :rule chain_m_resolution :premises (@p485 @p479) :args (@t323 @t317 (@list @t352))) % 52.56/52.85 (step @p487 :rule cnf_or_pos :args (@t325)) % 52.56/52.85 (step @p488 :rule reordering :premises (@p487) :args ((or @t324 @t322 (not @t325)))) % 52.56/52.85 (step @p489 :rule alpha_equiv :args (@t350 @t225 @t148)) % 52.56/52.85 (step @p490 :rule equiv_elim1 :premises (@p489)) % 52.56/52.85 (step @p491 :rule refl :args (@t358)) % 52.56/52.85 (step @p492 :rule bool-double-not-elim :args (@t350)) % 52.56/52.85 (step @p493 :rule nary_cong :premises (@p492 @p491) :args ((or (not @t351) @t358))) % 52.56/52.85 (assume-push @p709 @t351) % 52.56/52.85 (step @p495 :rule skolemize :premises (@p709)) % 52.56/52.85 (step-pop @p710 :rule scope :premises (@p495)) % 52.56/52.85 (step @p496 :rule process_scope :premises (@p710) :args (@t358)) % 52.56/52.85 (step @p498 :rule implies_elim :premises (@p496)) % 52.56/52.85 (step @p499 :rule eq_resolve :premises (@p498 @p493)) % 52.56/52.85 (step @p500 :rule bool-double-not-elim :args (@t355)) % 52.56/52.85 (step @p501 :rule refl :args (@t357)) % 52.56/52.85 (step @p502 :rule nary_cong :premises (@p501 @p500) :args ((or @t357 (not @t356)))) % 52.56/52.85 (step @p503 :rule cnf_or_neg :args (@t357 0)) % 52.56/52.85 (step @p504 :rule eq_resolve :premises (@p503 @p502)) % 52.56/52.85 (step @p505 :rule reordering :premises (@p504) :args ((or @t355 @t357))) % 52.56/52.85 (step @p506 :rule cnf_or_neg :args (@t357 1)) % 52.56/52.85 (step @p507 :rule refl :args (@t359)) % 52.56/52.85 (step @p508 :rule refl :args (@t5)) % 52.56/52.85 (step @p509 :rule cong :premises (@p508 @p507) :args ((= @t5 @t359))) % 52.56/52.85 (step @p510 :rule symm :premises (@p509)) % 52.56/52.85 (step @p511 :rule eq_resolve :premises (@p508 @p510)) % 52.56/52.85 (step @p512 :rule refl :args (@t360)) % 52.56/52.85 (step @p513 :rule refl :args (@t7)) % 52.56/52.85 (step @p514 :rule cong :premises (@p513 @p512) :args ((= @t7 @t360))) % 52.56/52.85 (step @p515 :rule symm :premises (@p514)) % 52.56/52.85 (step @p516 :rule eq_resolve :premises (@p513 @p515)) % 52.56/52.85 (step @p517 :rule cong :premises (@p516) :args (@t361)) % 52.56/52.85 (step @p518 :rule nary_cong :premises (@p358 @p517 @p511) :args (@t362)) % 52.56/52.85 (step @p519 :rule cong :premises (@p518) :args ((forall @t10 @t362))) % 52.56/52.85 (step @p520 :rule aci_norm :args ((= (or (or @t285 @t361) @t5) @t362))) % 52.56/52.85 (step @p521 :rule bool-and-de-morgan :args (@t8 @t7 true)) % 52.56/52.85 (step @p522 :rule nary_cong :premises (@p521 @p508) :args ((or (not @t9) @t5))) % 52.56/52.85 (step @p523 :rule trans :premises (@p522 @p520)) % 52.56/52.85 (step @p524 :rule bool-impl-elim :args (@t9 @t5)) % 52.56/52.85 (step @p525 :rule trans :premises (@p524 @p523)) % 52.56/52.85 (step @p526 :rule cong :premises (@p525) :args (@t11)) % 52.56/52.85 (step @p527 :rule trans :premises (@p526 @p519)) % 52.56/52.85 (step @p528 :rule eq_resolve :premises (@p2 @p527)) % 52.56/52.85 (step @p529 :rule instantiate :premises (@p528) :args ((@list @t306 @t320 @t353))) % 52.56/52.85 (step @p530 :rule cnf_or_pos :args (@t364)) % 52.56/52.85 (step @p531 :rule reordering :premises (@p530) :args ((or @t324 @t356 @t363 (not @t364)))) % 52.56/52.85 (step @p532 :rule aci_norm :args ((= @t370 (or @t368 @t367 @t366)))) % 52.56/52.85 (step @p533 :rule cong :premises (@p532) :args (@t371)) % 52.56/52.85 (step @p534 :rule quant-merge-prenex :args ((= (forall @t42 @t373) @t371))) % 52.56/52.85 (step @p535 :rule alpha_equiv :args (@t374 (@list @t365) @t106)) % 52.56/52.85 (step @p536 :rule refl :args (@t368)) % 52.56/52.85 (step @p537 :rule nary_cong :premises (@p536 @p535) :args (@t375)) % 52.56/52.85 (step @p538 :rule quant-miniscope-or :args ((= @t373 @t375))) % 52.56/52.85 (step @p539 :rule trans :premises (@p538 @p537)) % 52.56/52.85 (step @p540 :rule symm :premises (@p539)) % 52.56/52.85 (step @p541 :rule cong :premises (@p540) :args ((forall @t42 @t376))) % 52.56/52.85 (step @p542 :rule trans :premises (@p541 @p534)) % 52.56/52.85 (step @p543 :rule trans :premises (@p542 @p533)) % 52.56/52.85 (step @p544 :rule beta-reduce :args ((= @t379 @t376))) % 52.56/52.85 (step @p545 :rule cong :premises (@p544) :args (@t380)) % 52.56/52.85 (step @p546 :rule trans :premises (@p545 @p543)) % 52.56/52.85 (step @p547 :rule beta-reduce :args ((= (_ @t71 @t378) @t380))) % 52.56/52.85 (step @p548 :rule trans :premises (@p547 @p546)) % 52.56/52.85 (step @p549 :rule refl :args (@t377)) % 52.56/52.85 (step @p550 :rule nary_cong :premises (@p549 @p149) :args (@t381)) % 52.56/52.85 (step @p551 :rule cong :premises (@p550) :args (@t382)) % 52.56/52.85 (step @p552 :rule beta-reduce :args ((= (_ (lambda @t131 (or @t377 @t130)) @t161) @t382))) % 52.56/52.85 (step @p553 :rule trans :premises (@p552 @p551)) % 52.56/52.85 (step @p554 :rule beta-reduce :args ((= (_ (lambda @t66 (not (forall @t334 (or (not (tptp.irel @t25 @t328)) @t333 @t329 @t327)))) @t6) @t335))) % 52.56/52.85 (step @p555 :rule alpha_equiv :args (@t387 @t106 (@list @t328))) % 52.56/52.85 (step @p556 :rule cong :premises (@p555) :args (@t388)) % 52.56/52.85 (step @p557 :rule cong :premises (@p556) :args (@t389)) % 52.56/52.85 (step @p558 :rule ho_cong :premises (@p557 @p82)) % 52.56/52.85 (step @p559 :rule trans :premises (@p558 @p554)) % 52.56/52.85 (step @p560 :rule nary_cong :premises (@p90 @p559) :args (@t390)) % 52.56/52.85 (step @p561 :rule cong :premises (@p560) :args (@t391)) % 52.56/52.85 (step @p562 :rule cong :premises (@p561) :args (@t392)) % 52.56/52.85 (step @p563 :rule nary_cong :premises (@p562 @p164) :args (@t393)) % 52.56/52.85 (step @p564 :rule cong :premises (@p563) :args (@t394)) % 52.56/52.85 (step @p565 :rule beta-reduce :args ((= (_ @t184 @t389) @t394))) % 52.56/52.85 (step @p566 :rule trans :premises (@p565 @p564)) % 52.56/52.85 (step @p567 :rule aci_norm :args ((= @t396 @t385))) % 52.56/52.85 (step @p568 :rule cong :premises (@p567) :args (@t397)) % 52.56/52.85 (step @p569 :rule quant-merge-prenex :args ((= (forall @t32 @t399) @t397))) % 52.56/52.85 (step @p570 :rule alpha_equiv :args (@t400 (@list @t326) @t402)) % 52.56/52.85 (step @p571 :rule refl :args (@t384)) % 52.56/52.85 (step @p572 :rule nary_cong :premises (@p78 @p571 @p570) :args (@t403)) % 52.56/52.85 (step @p573 :rule quant-miniscope-or :args ((= @t399 @t403))) % 52.56/52.85 (step @p574 :rule trans :premises (@p573 @p572)) % 52.56/52.85 (step @p575 :rule symm :premises (@p574)) % 52.56/52.85 (step @p576 :rule cong :premises (@p575) :args ((forall @t32 @t407))) % 52.56/52.85 (step @p577 :rule trans :premises (@p576 @p569)) % 52.56/52.85 (step @p578 :rule trans :premises (@p577 @p568)) % 52.56/52.85 (step @p579 :rule aci_norm :args ((= (or @t112 @t408) @t407))) % 52.56/52.85 (step @p580 :rule beta-reduce :args ((= (_ (lambda @t66 (or (not (forall @t332 (or (not (tptp.irel @t25 @t330)) @t331))) (forall @t405 (or (not (tptp.irel @t25 @t401)) @t404)))) @t6) @t408))) % 52.56/52.85 (step @p581 :rule alpha_equiv :args (@t217 @t106 @t402)) % 52.56/52.85 (step @p582 :rule alpha_equiv :args (@t219 @t106 @t409)) % 52.56/52.85 (step @p583 :rule cong :premises (@p582) :args (@t221)) % 52.56/52.85 (step @p584 :rule nary_cong :premises (@p583 @p581) :args (@t222)) % 52.56/52.85 (step @p585 :rule cong :premises (@p584) :args (@t233)) % 52.56/52.85 (step @p586 :rule ho_cong :premises (@p585 @p82)) % 52.56/52.85 (step @p587 :rule trans :premises (@p586 @p580)) % 52.56/52.85 (step @p588 :rule nary_cong :premises (@p90 @p587) :args (@t410)) % 52.56/52.85 (step @p589 :rule trans :premises (@p588 @p579)) % 52.56/52.85 (step @p590 :rule cong :premises (@p589) :args (@t411)) % 52.56/52.85 (step @p591 :rule trans :premises (@p590 @p578)) % 52.56/52.85 (step @p592 :rule cong :premises (@p591) :args (@t412)) % 52.56/52.85 (step @p593 :rule cong :premises (@p592) :args (@t413)) % 52.56/52.85 (step @p594 :rule beta-reduce :args ((= (_ @t158 @t233) @t413))) % 52.56/52.85 (step @p595 :rule trans :premises (@p594 @p593)) % 52.56/52.85 (step @p596 :rule ho_cong :premises (@p155 @p272)) % 52.56/52.85 (step @p597 :rule trans :premises (@p596 @p595)) % 52.56/52.85 (step @p598 :rule ho_cong :premises (@p268 @p597)) % 52.56/52.85 (step @p599 :rule trans :premises (@p598 @p566)) % 52.56/52.85 (step @p600 :rule ho_cong :premises (@p599 @p154)) % 52.56/52.85 (step @p601 :rule trans :premises (@p600 @p553)) % 52.56/52.85 (step @p602 :rule ho_cong :premises (@p38 @p601)) % 52.56/52.85 (step @p603 :rule trans :premises (@p602 @p548)) % 52.56/52.85 (step @p604 :rule ho_cong :premises (@p371 @p435)) % 52.56/52.85 (step @p605 :rule ho_cong :premises (@p433 @p604)) % 52.56/52.85 (step @p606 :rule ho_cong :premises (@p605 @p335)) % 52.56/52.85 (step @p607 :rule ho_cong :premises (@p50 @p606)) % 52.56/52.85 (step @p608 :rule trans :premises (@p607 @p603)) % 52.56/52.85 (step @p609 :rule eq_resolve :premises (@p5 @p608)) % 52.56/52.85 (step @p610 :rule instantiate :premises (@p609) :args ((@list @t306 @t353))) % 52.56/52.85 (step @p611 :rule cnf_or_pos :args (@t416)) % 52.56/52.85 (step @p612 :rule reordering :premises (@p611) :args ((or @t415 @t354 @t414 (not @t416)))) % 52.56/52.85 (step @p613 :rule refl :args (@t422)) % 52.56/52.85 (step @p614 :rule bool-double-not-elim :args (@t336)) % 52.56/52.85 (step @p615 :rule nary_cong :premises (@p614 @p613) :args ((or (not @t415) @t422))) % 52.56/52.85 (assume-push @p711 @t415) % 52.56/52.85 (step @p617 :rule skolemize :premises (@p711)) % 52.56/52.85 (step-pop @p712 :rule scope :premises (@p617)) % 52.56/52.85 (step @p618 :rule process_scope :premises (@p712) :args (@t422)) % 52.56/52.85 (step @p620 :rule implies_elim :premises (@p618)) % 52.56/52.85 (step @p621 :rule eq_resolve :premises (@p620 @p615)) % 52.56/52.85 (step @p622 :rule bool-double-not-elim :args (@t419)) % 52.56/52.85 (step @p623 :rule refl :args (@t421)) % 52.56/52.85 (step @p624 :rule nary_cong :premises (@p623 @p622) :args ((or @t421 (not @t420)))) % 52.56/52.85 (step @p625 :rule cnf_or_neg :args (@t421 0)) % 52.56/52.85 (step @p626 :rule eq_resolve :premises (@p625 @p624)) % 52.56/52.85 (step @p627 :rule reordering :premises (@p626) :args ((or @t419 @t421))) % 52.56/52.85 (step @p628 :rule bool-double-not-elim :args (@t417)) % 52.56/52.85 (step @p629 :rule nary_cong :premises (@p623 @p628) :args ((or @t421 (not @t418)))) % 52.56/52.85 (step @p630 :rule cnf_or_neg :args (@t421 1)) % 52.56/52.85 (step @p631 :rule eq_resolve :premises (@p630 @p629)) % 52.56/52.85 (step @p632 :rule reordering :premises (@p631) :args ((or @t417 @t421))) % 52.56/52.85 (step @p633 :rule instantiate :premises (@p528) :args ((@list @t311 @t306 @t337))) % 52.56/52.85 (step @p634 :rule cnf_or_pos :args (@t424)) % 52.56/52.85 (step @p635 :rule reordering :premises (@p634) :args ((or @t313 @t420 @t423 (not @t424)))) % 52.56/52.85 (assume-push @p713 @t417) % 52.56/52.85 (step @p637 :rule instantiate :premises (@p713) :args ((@list @t339 @t425))) % 52.56/52.85 (step-pop @p714 :rule scope :premises (@p637)) % 52.56/52.85 (step @p638 :rule process_scope :premises (@p714) :args (@t433)) % 52.56/52.85 (step @p640 :rule implies_elim :premises (@p638)) % 52.56/52.85 (step @p641 :rule instantiate :premises (@p468) :args ((@list @t337))) % 52.56/52.85 (step @p642 :rule cnf_or_pos :args (@t436)) % 52.56/52.85 (step @p643 :rule reordering :premises (@p642) :args ((or @t435 @t434 (not @t436)))) % 52.56/52.85 (step @p644 :rule refl :args (@t446)) % 52.56/52.85 (step @p645 :rule bool-double-not-elim :args (@t338)) % 52.56/52.85 (step @p646 :rule nary_cong :premises (@p645 @p644) :args ((or (not @t434) @t446))) % 52.56/52.85 (assume-push @p715 @t434) % 52.56/52.85 (step @p648 :rule skolemize :premises (@p715)) % 52.56/52.85 (step-pop @p716 :rule scope :premises (@p648)) % 52.56/52.85 (step @p649 :rule process_scope :premises (@p716) :args (@t446)) % 52.56/52.85 (step @p651 :rule implies_elim :premises (@p649)) % 52.56/52.85 (step @p652 :rule eq_resolve :premises (@p651 @p646)) % 52.56/52.85 (step @p653 :rule bool-double-not-elim :args (@t431)) % 52.56/52.85 (step @p654 :rule refl :args (@t445)) % 52.56/52.85 (step @p655 :rule nary_cong :premises (@p654 @p653) :args ((or @t445 (not @t432)))) % 52.56/52.85 (step @p656 :rule cnf_or_neg :args (@t445 0)) % 52.56/52.85 (step @p657 :rule eq_resolve :premises (@p656 @p655)) % 52.56/52.85 (step @p658 :rule reordering :premises (@p657) :args ((or @t431 @t445))) % 52.56/52.85 (step @p659 :rule cnf_or_neg :args (@t445 1)) % 52.56/52.85 (step @p660 :rule instantiate :premises (@p528) :args ((@list @t306 @t337 @t339))) % 52.56/52.85 (step @p661 :rule cnf_or_pos :args (@t447)) % 52.56/52.85 (step @p662 :rule reordering :premises (@p661) :args ((or @t420 @t432 @t342 (not @t447)))) % 52.56/52.85 (step @p663 :rule cnf_or_pos :args (@t344)) % 52.56/52.85 (step @p664 :rule reordering :premises (@p663) :args ((or @t343 @t341 (not @t344)))) % 52.56/52.85 (step @p665 :rule alpha_equiv :args (@t441 @t225 @t148)) % 52.56/52.85 (step @p666 :rule equiv_elim1 :premises (@p665)) % 52.56/52.85 (step @p667 :rule bool-double-not-elim :args (@t441)) % 52.56/52.85 (step @p668 :rule refl :args (@t443)) % 52.56/52.85 (step @p669 :rule nary_cong :premises (@p668 @p667) :args ((or @t443 (not @t442)))) % 52.56/52.85 (step @p670 :rule cnf_or_neg :args (@t443 0)) % 52.56/52.85 (step @p671 :rule eq_resolve :premises (@p670 @p669)) % 52.56/52.85 (step @p672 :rule reordering :premises (@p671) :args ((or @t441 @t443))) % 52.56/52.85 (step @p673 :rule cnf_and_neg :args (@t444)) % 52.56/52.88 (step @p674 :rule bool-double-not-elim :args (@t437)) % 52.56/52.88 (step @p675 :rule refl :args (@t439)) % 52.56/52.88 (step @p676 :rule nary_cong :premises (@p675 @p674) :args ((or @t439 (not @t438)))) % 52.56/52.88 (step @p677 :rule cnf_or_neg :args (@t439 0)) % 52.56/52.88 (step @p678 :rule eq_resolve :premises (@p677 @p676)) % 52.56/52.88 (step @p679 :rule reordering :premises (@p678) :args ((or @t437 @t439))) % 52.56/52.88 (step @p680 :rule bool-double-not-elim :args (@t427)) % 52.56/52.88 (step @p681 :rule nary_cong :premises (@p675 @p680) :args ((or @t439 (not @t428)))) % 52.56/52.88 (step @p682 :rule cnf_or_neg :args (@t439 1)) % 52.56/52.88 (step @p683 :rule eq_resolve :premises (@p682 @p681)) % 52.56/52.88 (step @p684 :rule reordering :premises (@p683) :args ((or @t427 @t439))) % 52.56/52.88 (step @p685 :rule cnf_or_neg :args (@t439 2)) % 52.56/52.88 (step @p686 :rule alpha_equiv :args (@t437 @t220 @t409)) % 52.56/52.88 (step @p687 :rule equiv_elim1 :premises (@p686)) % 52.56/52.88 (step @p688 :rule cnf_or_pos :args (@t433)) % 52.56/52.88 (step @p689 :rule reordering :premises (@p688) :args ((or @t432 @t428 @t426 @t430 (not @t433)))) % 52.56/52.88 (step @p690 :rule chain_m_resolution :premises (@p689 @p687 @p685 @p684 @p679 @p673 @p672 @p666 @p664 @p662 @p660 @p659 @p658 @p652 @p643 @p641 @p640 @p635 @p633 @p475 @p632 @p627 @p621 @p612 @p610 @p531 @p529 @p486 @p506 @p505 @p499 @p490 @p488 @p486 @p461 @p456) :args (@t309 (@list false true false false true false true true false false true false true true false false false false false false false true true false false false false true false true true true false false false) (@list @t429 @t426 @t427 @t437 @t439 @t443 @t441 @t340 @t342 @t447 @t444 @t431 @t445 @t338 @t436 @t433 @t423 @t424 @t312 @t417 @t419 @t421 @t336 @t416 @t363 @t364 @t323 @t354 @t355 @t357 @t350 @t321 @t323 @t344 @t325))) % 52.56/52.88 (step @p691 :rule refl :args (@t448)) % 52.56/52.88 (step @p692 :rule bool-double-not-elim :args (@t308)) % 52.56/52.88 (step @p693 :rule refl :args (@t310)) % 52.56/52.88 (step @p694 :rule nary_cong :premises (@p693 @p692 @p691) :args ((or @t310 (not @t309) @t448))) % 52.56/52.88 (step @p695 :rule cnf_and_neg :args (@t310)) % 52.56/52.88 (step @p696 :rule eq_resolve :premises (@p695 @p694)) % 52.56/52.88 (step @p697 :rule reordering :premises (@p696) :args ((or @t308 @t310 @t448))) % 52.56/52.88 (step @p698 :rule chain_m_resolution :premises (@p697 @p690 @p451) :args (@t448 (@list true true) (@list @t308 @t310))) % 52.56/52.88 (assume-push @p717 @t449) % 52.56/52.88 (step @p700 :rule instantiate :premises (@p53) :args (@t345)) % 52.56/52.88 (step-pop @p718 :rule scope :premises (@p700)) % 52.56/52.88 (step @p701 :rule process_scope :premises (@p718) :args (@t307)) % 52.56/52.88 (step @p703 :rule implies_elim :premises (@p701)) % 52.56/52.88 (step @p704 false :rule chain_m_resolution :premises (@p703 @p698 @p53) :args (false (@list true false) (@list @t307 @t449))) % 52.56/52.88 ) % 52.56/52.88 % SZS output end Proof % 52.56/52.88 % cvc5 exiting %------------------------------------------------------------------------------