%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : KRS151+1 : TPTP v9.2.1. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:29:01 AM UTC 2026 % Result : Theorem 1.00s 1.28s % Output : Proof 1.00s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : KRS151+1 : TPTP v9.2.1. Released v3.1.0. % 0.00/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.16/0.34 % Computer : n006.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Jun 2 05:28:19 EDT 2026 % 0.16/0.34 % CPUTime : % 0.31/0.53 %----Proving TF0_NAR, FOF, or CNF % 1.00/1.28 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 1.00/1.28 % SZS status Theorem % 1.00/1.28 % SZS output start Proof % 1.00/1.28 ( % 1.00/1.28 (declare-sort $$unsorted 0) % 1.00/1.28 (declare-const tptp.iV21033 $$unsorted) % 1.00/1.28 (declare-const tptp.iV21036 $$unsorted) % 1.00/1.28 (declare-const tptp.iV21027 $$unsorted) % 1.00/1.28 (declare-const tptp.cC86 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.iV21029 $$unsorted) % 1.00/1.28 (declare-const tptp.cC84 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC82 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC80 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC74 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC72 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC70 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC68 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC64 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC62 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC56 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC52 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.iV21032 $$unsorted) % 1.00/1.28 (declare-const tptp.cC50 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC48 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC46 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC42 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC40 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.iV21030 $$unsorted) % 1.00/1.28 (declare-const tptp.cC38 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC34 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC76 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC32 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC30 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC28 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC26 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC24 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC2 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC130 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.xsd_integer (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC94 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC128 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC118 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC92 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC124 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.iV21034 $$unsorted) % 1.00/1.28 (declare-const tptp.cC116 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC170 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC114 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC108 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cTOP (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC90 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cowlNothing (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC100 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC110 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC88 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC164 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC112 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cowlThing (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC104 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC174 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC120 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC6 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC12 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.iV21031 $$unsorted) % 1.00/1.28 (declare-const tptp.cTEST (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.xsd_string (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC166 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC106 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC16 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC122 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC60 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC140 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC54 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC8 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC132 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC150 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC10 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC96 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC168 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC44 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC126 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC98 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC180 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC4 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC136 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC102 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC134 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC138 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC154 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC176 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.rR1 (-> $$unsorted $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC14 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC78 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC156 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC20 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC142 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.iV21028 $$unsorted) % 1.00/1.28 (declare-const tptp.cC160 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC66 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC144 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC146 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC148 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC152 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC18 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC36 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC22 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC158 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC162 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.iV21026 $$unsorted) % 1.00/1.28 (declare-const tptp.cC172 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.iV21035 $$unsorted) % 1.00/1.28 (declare-const tptp.cC58 (-> $$unsorted Bool)) % 1.00/1.28 (declare-const tptp.cC178 (-> $$unsorted Bool)) % 1.00/1.28 (define @t1 () (@var "X" $$unsorted)) % 1.00/1.28 (define @t2 () (not (tptp.cowlNothing @t1))) % 1.00/1.28 (define @t3 () (tptp.cowlThing @t1)) % 1.00/1.28 (define @t4 () (@list @t1)) % 1.00/1.28 (define @t5 () (forall @t4 (and @t3 @t2))) % 1.00/1.28 (define @t6 () (forall @t4 (= (tptp.xsd_string @t1) (not (tptp.xsd_integer @t1))))) % 1.00/1.28 (define @t7 () (tptp.cC4 @t1)) % 1.00/1.28 (define @t8 () (tptp.cC8 @t1)) % 1.00/1.28 (define @t9 () (tptp.cC10 @t1)) % 1.00/1.28 (define @t10 () (@var "Y" $$unsorted)) % 1.00/1.28 (define @t11 () (tptp.rR1 @t1 @t10)) % 1.00/1.28 (define @t12 () (@list @t10)) % 1.00/1.28 (define @t13 () (exists @t12 (and @t11 (not (tptp.cC6 @t10))))) % 1.00/1.28 (define @t14 () (tptp.cC102 @t1)) % 1.00/1.28 (define @t15 () (tptp.cC100 @t1)) % 1.00/1.28 (define @t16 () (not @t15)) % 1.00/1.28 (define @t17 () (tptp.cC104 @t1)) % 1.00/1.28 (define @t18 () (tptp.cC106 @t1)) % 1.00/1.28 (define @t19 () (tptp.cC98 @t1)) % 1.00/1.28 (define @t20 () (tptp.cC108 @t1)) % 1.00/1.28 (define @t21 () (tptp.cTOP @t1)) % 1.00/1.28 (define @t22 () (tptp.cC110 @t1)) % 1.00/1.28 (define @t23 () (tptp.cC90 @t1)) % 1.00/1.28 (define @t24 () (tptp.cC112 @t1)) % 1.00/1.28 (define @t25 () (tptp.cC114 @t1)) % 1.00/1.28 (define @t26 () (forall @t4 (= @t25 @t21))) % 1.00/1.28 (define @t27 () (tptp.cC116 @t1)) % 1.00/1.28 (define @t28 () (exists @t12 (and @t11 (not (tptp.cC92 @t10))))) % 1.00/1.28 (define @t29 () (tptp.cC118 @t1)) % 1.00/1.28 (define @t30 () (tptp.cC92 @t1)) % 1.00/1.28 (define @t31 () (not @t30)) % 1.00/1.28 (define @t32 () (tptp.cC120 @t1)) % 1.00/1.28 (define @t33 () (tptp.cC122 @t1)) % 1.00/1.28 (define @t34 () (tptp.cC124 @t1)) % 1.00/1.28 (define @t35 () (tptp.cC126 @t1)) % 1.00/1.28 (define @t36 () (tptp.cC128 @t1)) % 1.00/1.28 (define @t37 () (tptp.cC130 @t1)) % 1.00/1.28 (define @t38 () (tptp.cC132 @t1)) % 1.00/1.28 (define @t39 () (tptp.cC134 @t1)) % 1.00/1.28 (define @t40 () (tptp.cC136 @t1)) % 1.00/1.28 (define @t41 () (forall @t4 (= @t40 @t21))) % 1.00/1.28 (define @t42 () (tptp.cC138 @t1)) % 1.00/1.28 (define @t43 () (exists @t12 (and @t11 (not (tptp.cC12 @t10))))) % 1.00/1.28 (define @t44 () (tptp.cC14 @t1)) % 1.00/1.28 (define @t45 () (exists @t12 (and @t11 (not (tptp.cC100 @t10))))) % 1.00/1.28 (define @t46 () (tptp.cC140 @t1)) % 1.00/1.28 (define @t47 () (tptp.cC142 @t1)) % 1.00/1.28 (define @t48 () (tptp.cC144 @t1)) % 1.00/1.28 (define @t49 () (tptp.cC146 @t1)) % 1.00/1.28 (define @t50 () (tptp.cC148 @t1)) % 1.00/1.28 (define @t51 () (tptp.cC150 @t1)) % 1.00/1.28 (define @t52 () (tptp.cC152 @t1)) % 1.00/1.28 (define @t53 () (tptp.cC154 @t1)) % 1.00/1.28 (define @t54 () (tptp.cC156 @t1)) % 1.00/1.28 (define @t55 () (tptp.cC22 @t1)) % 1.00/1.28 (define @t56 () (tptp.cC158 @t1)) % 1.00/1.28 (define @t57 () (tptp.cC16 @t1)) % 1.00/1.28 (define @t58 () (tptp.cC160 @t1)) % 1.00/1.28 (define @t59 () (tptp.cC162 @t1)) % 1.00/1.28 (define @t60 () (tptp.cC164 @t1)) % 1.00/1.28 (define @t61 () (tptp.cC166 @t1)) % 1.00/1.28 (define @t62 () (tptp.cC168 @t1)) % 1.00/1.28 (define @t63 () (exists @t12 (and @t11 (not (tptp.cC18 @t10))))) % 1.00/1.28 (define @t64 () (tptp.cC170 @t1)) % 1.00/1.28 (define @t65 () (tptp.cC172 @t1)) % 1.00/1.28 (define @t66 () (tptp.cC174 @t1)) % 1.00/1.28 (define @t67 () (tptp.cC176 @t1)) % 1.00/1.28 (define @t68 () (tptp.cC178 @t1)) % 1.00/1.28 (define @t69 () (tptp.cC180 @t1)) % 1.00/1.28 (define @t70 () (tptp.cC20 @t1)) % 1.00/1.28 (define @t71 () (tptp.cC2 @t10)) % 1.00/1.28 (define @t72 () (not @t71)) % 1.00/1.28 (define @t73 () (and @t11 @t72)) % 1.00/1.28 (define @t74 () (exists @t12 @t73)) % 1.00/1.28 (define @t75 () (tptp.cC24 @t1)) % 1.00/1.28 (define @t76 () (not (tptp.cC2 @t1))) % 1.00/1.28 (define @t77 () (tptp.cC26 @t1)) % 1.00/1.28 (define @t78 () (tptp.cC28 @t1)) % 1.00/1.28 (define @t79 () (tptp.cC30 @t1)) % 1.00/1.28 (define @t80 () (tptp.cC32 @t1)) % 1.00/1.28 (define @t81 () (tptp.cC34 @t1)) % 1.00/1.28 (define @t82 () (tptp.cC36 @t1)) % 1.00/1.28 (define @t83 () (tptp.cC38 @t1)) % 1.00/1.28 (define @t84 () (= @t7 @t74)) % 1.00/1.28 (define @t85 () (forall @t4 @t84)) % 1.00/1.28 (define @t86 () (tptp.cC40 @t1)) % 1.00/1.28 (define @t87 () (forall @t4 (= @t86 @t21))) % 1.00/1.28 (define @t88 () (tptp.cC42 @t1)) % 1.00/1.28 (define @t89 () (tptp.cC44 @t1)) % 1.00/1.28 (define @t90 () (not (tptp.cC12 @t1))) % 1.00/1.28 (define @t91 () (tptp.cC46 @t1)) % 1.00/1.28 (define @t92 () (tptp.cC48 @t1)) % 1.00/1.28 (define @t93 () (tptp.cC50 @t1)) % 1.00/1.28 (define @t94 () (tptp.cC52 @t1)) % 1.00/1.28 (define @t95 () (tptp.cC54 @t1)) % 1.00/1.28 (define @t96 () (tptp.cC56 @t1)) % 1.00/1.28 (define @t97 () (tptp.cC58 @t1)) % 1.00/1.28 (define @t98 () (tptp.cC60 @t1)) % 1.00/1.28 (define @t99 () (tptp.cC62 @t1)) % 1.00/1.28 (define @t100 () (forall @t4 (= @t99 @t21))) % 1.00/1.28 (define @t101 () (tptp.cC64 @t1)) % 1.00/1.28 (define @t102 () (tptp.cC66 @t1)) % 1.00/1.28 (define @t103 () (tptp.cC18 @t1)) % 1.00/1.28 (define @t104 () (not @t103)) % 1.00/1.28 (define @t105 () (tptp.cC68 @t1)) % 1.00/1.28 (define @t106 () (tptp.cC70 @t1)) % 1.00/1.28 (define @t107 () (tptp.cC72 @t1)) % 1.00/1.28 (define @t108 () (tptp.cC74 @t1)) % 1.00/1.28 (define @t109 () (tptp.cC76 @t1)) % 1.00/1.28 (define @t110 () (tptp.cC78 @t1)) % 1.00/1.28 (define @t111 () (tptp.cC80 @t1)) % 1.00/1.28 (define @t112 () (tptp.cC82 @t1)) % 1.00/1.28 (define @t113 () (tptp.cC84 @t1)) % 1.00/1.28 (define @t114 () (forall @t4 (= @t113 @t21))) % 1.00/1.28 (define @t115 () (tptp.cC86 @t1)) % 1.00/1.28 (define @t116 () (tptp.cC88 @t1)) % 1.00/1.28 (define @t117 () (forall @t4 (= @t116 @t21))) % 1.00/1.28 (define @t118 () (tptp.cC94 @t1)) % 1.00/1.28 (define @t119 () (tptp.cC96 @t1)) % 1.00/1.28 (define @t120 () (tptp.rR1 tptp.iV21026 @t1)) % 1.00/1.28 (define @t121 () (tptp.cTOP tptp.iV21026)) % 1.00/1.28 (define @t122 () (tptp.cTEST tptp.iV21026)) % 1.00/1.28 (define @t123 () (tptp.cC98 tptp.iV21026)) % 1.00/1.28 (define @t124 () (not @t123)) % 1.00/1.28 (define @t125 () (tptp.cC122 tptp.iV21026)) % 1.00/1.28 (define @t126 () (not @t125)) % 1.00/1.28 (define @t127 () (tptp.cC34 tptp.iV21026)) % 1.00/1.28 (define @t128 () (not @t127)) % 1.00/1.28 (define @t129 () (tptp.cC28 tptp.iV21026)) % 1.00/1.28 (define @t130 () (not @t129)) % 1.00/1.28 (define @t131 () (tptp.cC70 tptp.iV21026)) % 1.00/1.28 (define @t132 () (not @t131)) % 1.00/1.28 (define @t133 () (tptp.cC162 tptp.iV21026)) % 1.00/1.28 (define @t134 () (not @t133)) % 1.00/1.28 (define @t135 () (tptp.cC166 tptp.iV21026)) % 1.00/1.28 (define @t136 () (not @t135)) % 1.00/1.28 (define @t137 () (tptp.cC150 tptp.iV21026)) % 1.00/1.28 (define @t138 () (not @t137)) % 1.00/1.28 (define @t139 () (tptp.cC54 tptp.iV21026)) % 1.00/1.28 (define @t140 () (not @t139)) % 1.00/1.28 (define @t141 () (tptp.cC106 tptp.iV21026)) % 1.00/1.28 (define @t142 () (not @t141)) % 1.00/1.28 (define @t143 () (tptp.cC144 tptp.iV21026)) % 1.00/1.28 (define @t144 () (not @t143)) % 1.00/1.28 (define @t145 () (tptp.cC48 tptp.iV21026)) % 1.00/1.28 (define @t146 () (not @t145)) % 1.00/1.28 (define @t147 () (tptp.cC76 tptp.iV21026)) % 1.00/1.28 (define @t148 () (not @t147)) % 1.00/1.28 (define @t149 () (tptp.cC128 tptp.iV21026)) % 1.00/1.28 (define @t150 () (not @t149)) % 1.00/1.28 (define @t151 () (tptp.cC172 tptp.iV21026)) % 1.00/1.28 (define @t152 () (not @t151)) % 1.00/1.28 (define @t153 () (tptp.cowlThing tptp.iV21026)) % 1.00/1.28 (define @t154 () (tptp.rR1 tptp.iV21026 tptp.iV21027)) % 1.00/1.28 (define @t155 () (tptp.cC26 tptp.iV21027)) % 1.00/1.28 (define @t156 () (tptp.rR1 tptp.iV21027 @t1)) % 1.00/1.28 (define @t157 () (tptp.cC6 @t1)) % 1.00/1.28 (define @t158 () (tptp.cC32 tptp.iV21027)) % 1.00/1.28 (define @t159 () (tptp.cC2 tptp.iV21027)) % 1.00/1.28 (define @t160 () (not @t159)) % 1.00/1.28 (define @t161 () (tptp.cowlThing tptp.iV21027)) % 1.00/1.28 (define @t162 () (tptp.cC46 tptp.iV21029)) % 1.00/1.28 (define @t163 () (tptp.rR1 tptp.iV21029 @t1)) % 1.00/1.28 (define @t164 () (tptp.cC12 tptp.iV21029)) % 1.00/1.28 (define @t165 () (not @t164)) % 1.00/1.28 (define @t166 () (tptp.cC52 tptp.iV21029)) % 1.00/1.28 (define @t167 () (tptp.cowlThing tptp.iV21029)) % 1.00/1.28 (define @t168 () (tptp.rR1 tptp.iV21030 @t1)) % 1.00/1.28 (define @t169 () (tptp.cC68 tptp.iV21030)) % 1.00/1.28 (define @t170 () (tptp.cC74 tptp.iV21030)) % 1.00/1.28 (define @t171 () (tptp.cC18 tptp.iV21030)) % 1.00/1.28 (define @t172 () (not @t171)) % 1.00/1.28 (define @t173 () (tptp.cowlThing tptp.iV21030)) % 1.00/1.28 (define @t174 () (tptp.cC72 tptp.iV21030)) % 1.00/1.28 (define @t175 () (tptp.cC66 tptp.iV21030)) % 1.00/1.28 (define @t176 () (tptp.cC44 tptp.iV21029)) % 1.00/1.28 (define @t177 () (tptp.cC50 tptp.iV21029)) % 1.00/1.28 (define @t178 () (tptp.cC24 tptp.iV21027)) % 1.00/1.28 (define @t179 () (tptp.cC30 tptp.iV21027)) % 1.00/1.28 (define @t180 () (tptp.cC90 tptp.iV21026)) % 1.00/1.28 (define @t181 () (tptp.cC14 tptp.iV21026)) % 1.00/1.28 (define @t182 () (tptp.cC108 tptp.iV21026)) % 1.00/1.28 (define @t183 () (tptp.cC4 tptp.iV21026)) % 1.00/1.28 (define @t184 () (tptp.cC138 tptp.iV21026)) % 1.00/1.28 (define @t185 () (tptp.cC82 tptp.iV21026)) % 1.00/1.28 (define @t186 () (tptp.cC116 tptp.iV21026)) % 1.00/1.28 (define @t187 () (tptp.cC110 tptp.iV21026)) % 1.00/1.28 (define @t188 () (tptp.cC64 tptp.iV21026)) % 1.00/1.28 (define @t189 () (tptp.cC114 tptp.iV21026)) % 1.00/1.28 (define @t190 () (tptp.cC180 tptp.iV21026)) % 1.00/1.28 (define @t191 () (tptp.cC112 tptp.iV21026)) % 1.00/1.28 (define @t192 () (tptp.cC136 tptp.iV21026)) % 1.00/1.28 (define @t193 () (tptp.cC8 tptp.iV21026)) % 1.00/1.28 (define @t194 () (tptp.cC80 tptp.iV21026)) % 1.00/1.28 (define @t195 () (tptp.cC154 tptp.iV21026)) % 1.00/1.28 (define @t196 () (tptp.cC62 tptp.iV21026)) % 1.00/1.28 (define @t197 () (tptp.cC130 tptp.iV21026)) % 1.00/1.28 (define @t198 () (tptp.cC132 tptp.iV21026)) % 1.00/1.28 (define @t199 () (tptp.cC40 tptp.iV21026)) % 1.00/1.28 (define @t200 () (tptp.cC152 tptp.iV21026)) % 1.00/1.28 (define @t201 () (tptp.cC58 tptp.iV21026)) % 1.00/1.28 (define @t202 () (tptp.cC78 tptp.iV21026)) % 1.00/1.28 (define @t203 () (tptp.cC56 tptp.iV21026)) % 1.00/1.28 (define @t204 () (tptp.cC168 tptp.iV21026)) % 1.00/1.28 (define @t205 () (tptp.cC22 tptp.iV21026)) % 1.00/1.28 (define @t206 () (tptp.cC134 tptp.iV21026)) % 1.00/1.28 (define @t207 () (tptp.cC10 tptp.iV21026)) % 1.00/1.28 (define @t208 () (tptp.cC158 tptp.iV21026)) % 1.00/1.28 (define @t209 () (tptp.cC38 tptp.iV21026)) % 1.00/1.28 (define @t210 () (tptp.cC60 tptp.iV21026)) % 1.00/1.28 (define @t211 () (tptp.cC156 tptp.iV21026)) % 1.00/1.28 (define @t212 () (tptp.cC20 tptp.iV21026)) % 1.00/1.28 (define @t213 () (tptp.cC174 tptp.iV21026)) % 1.00/1.28 (define @t214 () (tptp.cC86 tptp.iV21026)) % 1.00/1.28 (define @t215 () (tptp.cC88 tptp.iV21026)) % 1.00/1.28 (define @t216 () (tptp.cC42 tptp.iV21026)) % 1.00/1.28 (define @t217 () (tptp.cC36 tptp.iV21026)) % 1.00/1.28 (define @t218 () (tptp.cC16 tptp.iV21026)) % 1.00/1.28 (define @t219 () (tptp.cC84 tptp.iV21026)) % 1.00/1.28 (define @t220 () (and @t5 @t6 @t153 @t219 @t218 @t217 @t216 @t215 @t214 @t213 @t212 @t211 @t210 @t209 @t208 @t207 @t206 @t205 @t204 @t203 @t202 @t201 @t200 @t199 @t198 @t197 @t196 @t195 @t194 @t193 @t192 @t191 @t190 @t189 @t188 @t187 @t186 @t185 @t184 @t183 @t182 @t181 @t180 @t161 @t179 @t178 @t167 @t177 @t176 @t173 @t175 @t174)) % 1.00/1.28 (define @t221 () (not @t220)) % 1.00/1.28 (define @t222 () (forall @t4 @t2)) % 1.00/1.28 (define @t223 () (@list @t1)) % 1.00/1.28 (define @t224 () (@var "BOUND_VARIABLE_8270" $$unsorted)) % 1.00/1.28 (define @t225 () (forall @t4 @t3)) % 1.00/1.28 (define @t226 () (@var "BOUND_VARIABLE_8265" $$unsorted)) % 1.00/1.28 (define @t227 () (and @t225 @t222)) % 1.00/1.28 (define @t228 () (@list tptp.iV21030)) % 1.00/1.28 (define @t229 () (not @t174)) % 1.00/1.28 (define @t230 () (and @t172 @t229)) % 1.00/1.28 (define @t231 () (= @t170 @t230)) % 1.00/1.28 (define @t232 () (not @t230)) % 1.00/1.28 (define @t233 () (@list true false)) % 1.00/1.28 (define @t234 () (not @t172)) % 1.00/1.28 (define @t235 () (@list true true)) % 1.00/1.28 (define @t236 () (not @t175)) % 1.00/1.28 (define @t237 () (and @t236 @t172)) % 1.00/1.28 (define @t238 () (= @t169 @t237)) % 1.00/1.28 (define @t239 () (not @t237)) % 1.00/1.28 (define @t240 () (@list tptp.iV21029)) % 1.00/1.28 (define @t241 () (not @t176)) % 1.00/1.28 (define @t242 () (and @t165 @t241)) % 1.00/1.28 (define @t243 () (= @t162 @t242)) % 1.00/1.28 (define @t244 () (not @t242)) % 1.00/1.28 (define @t245 () (not @t165)) % 1.00/1.28 (define @t246 () (not @t177)) % 1.00/1.28 (define @t247 () (and @t165 @t246)) % 1.00/1.28 (define @t248 () (= @t166 @t247)) % 1.00/1.28 (define @t249 () (not @t247)) % 1.00/1.28 (define @t250 () (@list tptp.iV21027)) % 1.00/1.28 (define @t251 () (not @t178)) % 1.00/1.28 (define @t252 () (and @t251 @t160)) % 1.00/1.28 (define @t253 () (= @t155 @t252)) % 1.00/1.28 (define @t254 () (not @t252)) % 1.00/1.28 (define @t255 () (not @t160)) % 1.00/1.28 (define @t256 () (not @t179)) % 1.00/1.28 (define @t257 () (and @t160 @t256)) % 1.00/1.28 (define @t258 () (= @t158 @t257)) % 1.00/1.28 (define @t259 () (not @t257)) % 1.00/1.28 (define @t260 () (@list tptp.iV21026)) % 1.00/1.28 (define @t261 () (and @t208 @t190)) % 1.00/1.28 (define @t262 () (= @t122 @t261)) % 1.00/1.28 (define @t263 () (@list false false)) % 1.00/1.28 (define @t264 () (not @t261)) % 1.00/1.28 (define @t265 () (@list false)) % 1.00/1.28 (define @t266 () (@list @t261)) % 1.00/1.28 (define @t267 () (and @t205 @t211)) % 1.00/1.28 (define @t268 () (= @t208 @t267)) % 1.00/1.28 (define @t269 () (not @t208)) % 1.00/1.28 (define @t270 () (not @t267)) % 1.00/1.28 (define @t271 () (@list @t267)) % 1.00/1.28 (define @t272 () (and @t195 @t184)) % 1.00/1.28 (define @t273 () (= @t211 @t272)) % 1.00/1.28 (define @t274 () (not @t211)) % 1.00/1.28 (define @t275 () (and @t192 @t206)) % 1.00/1.28 (define @t276 () (= @t184 @t275)) % 1.00/1.28 (define @t277 () (not @t184)) % 1.00/1.28 (define @t278 () (and @t198 @t186)) % 1.00/1.28 (define @t279 () (= @t206 @t278)) % 1.00/1.28 (define @t280 () (not @t206)) % 1.00/1.28 (define @t281 () (and @t189 @t191)) % 1.00/1.28 (define @t282 () (= @t186 @t281)) % 1.00/1.28 (define @t283 () (not @t186)) % 1.00/1.28 (define @t284 () (and @t218 @t212)) % 1.00/1.28 (define @t285 () (= @t205 @t284)) % 1.00/1.28 (define @t286 () (not @t205)) % 1.00/1.28 (define @t287 () (not @t284)) % 1.00/1.28 (define @t288 () (@list @t284)) % 1.00/1.28 (define @t289 () (and @t181 @t207)) % 1.00/1.28 (define @t290 () (= @t218 @t289)) % 1.00/1.28 (define @t291 () (not @t218)) % 1.00/1.28 (define @t292 () (not @t289)) % 1.00/1.28 (define @t293 () (@list @t289)) % 1.00/1.28 (define @t294 () (and @t142 @t124)) % 1.00/1.28 (define @t295 () (= @t182 @t294)) % 1.00/1.28 (define @t296 () (not @t11)) % 1.00/1.28 (define @t297 () (forall @t12 (not @t73))) % 1.00/1.28 (define @t298 () (not @t297)) % 1.00/1.28 (define @t299 () (not @t154)) % 1.00/1.28 (define @t300 () (or @t299 @t159)) % 1.00/1.28 (define @t301 () (not @t300)) % 1.00/1.28 (define @t302 () (forall @t12 (or (not (tptp.rR1 tptp.iV21026 @t10)) @t71))) % 1.00/1.28 (define @t303 () (not @t302)) % 1.00/1.28 (define @t304 () (= @t183 @t303)) % 1.00/1.28 (define @t305 () (not @t304)) % 1.00/1.28 (define @t306 () (= @t121 @t196)) % 1.00/1.28 (define @t307 () (not @t121)) % 1.00/1.28 (define @t308 () (and @t146 @t140)) % 1.00/1.28 (define @t309 () (= @t203 @t308)) % 1.00/1.28 (define @t310 () (and @t203 @t121)) % 1.00/1.28 (define @t311 () (not @t203)) % 1.00/1.28 (define @t312 () (= @t201 @t310)) % 1.00/1.28 (define @t313 () (= @t121 @t199)) % 1.00/1.28 (define @t314 () (and @t130 @t128)) % 1.00/1.28 (define @t315 () (= @t217 @t314)) % 1.00/1.28 (define @t316 () (and @t217 @t121)) % 1.00/1.28 (define @t317 () (not @t217)) % 1.00/1.28 (define @t318 () (= @t209 @t316)) % 1.00/1.28 (define @t319 () (and @t199 @t209)) % 1.00/1.28 (define @t320 () (not @t199)) % 1.00/1.28 (define @t321 () (not @t209)) % 1.00/1.28 (define @t322 () (= @t216 @t319)) % 1.00/1.28 (define @t323 () (and @t201 @t216)) % 1.00/1.28 (define @t324 () (not @t201)) % 1.00/1.28 (define @t325 () (not @t216)) % 1.00/1.28 (define @t326 () (= @t210 @t323)) % 1.00/1.28 (define @t327 () (and @t196 @t210)) % 1.00/1.28 (define @t328 () (not @t196)) % 1.00/1.28 (define @t329 () (not @t210)) % 1.00/1.28 (define @t330 () (= @t188 @t327)) % 1.00/1.28 (define @t331 () (and @t132 @t148)) % 1.00/1.28 (define @t332 () (= @t202 @t331)) % 1.00/1.28 (define @t333 () (and @t121 @t202)) % 1.00/1.28 (define @t334 () (not @t202)) % 1.00/1.28 (define @t335 () (= @t194 @t333)) % 1.00/1.28 (define @t336 () (and @t194 @t188)) % 1.00/1.28 (define @t337 () (not @t188)) % 1.00/1.28 (define @t338 () (not @t194)) % 1.00/1.28 (define @t339 () (= @t185 @t336)) % 1.00/1.28 (define @t340 () (and @t182 @t121)) % 1.00/1.28 (define @t341 () (not @t182)) % 1.00/1.28 (define @t342 () (= @t187 @t340)) % 1.00/1.28 (define @t343 () (= @t121 @t189)) % 1.00/1.28 (define @t344 () (and @t193 @t183)) % 1.00/1.28 (define @t345 () (= @t207 @t344)) % 1.00/1.28 (define @t346 () (not @t207)) % 1.00/1.28 (define @t347 () (= @t121 @t192)) % 1.00/1.28 (define @t348 () (and @t138 @t144)) % 1.00/1.28 (define @t349 () (= @t200 @t348)) % 1.00/1.28 (define @t350 () (and @t121 @t200)) % 1.00/1.28 (define @t351 () (not @t200)) % 1.00/1.28 (define @t352 () (= @t195 @t350)) % 1.00/1.28 (define @t353 () (and @t126 @t150)) % 1.00/1.28 (define @t354 () (= @t197 @t353)) % 1.00/1.28 (define @t355 () (and @t121 @t197)) % 1.00/1.28 (define @t356 () (not @t197)) % 1.00/1.28 (define @t357 () (= @t198 @t355)) % 1.00/1.28 (define @t358 () (and @t136 @t134)) % 1.00/1.28 (define @t359 () (= @t204 @t358)) % 1.00/1.28 (define @t360 () (not @t204)) % 1.00/1.28 (define @t361 () (and @t204 @t152)) % 1.00/1.28 (define @t362 () (= @t213 @t361)) % 1.00/1.28 (define @t363 () (= @t121 @t215)) % 1.00/1.28 (define @t364 () (= @t121 @t219)) % 1.00/1.28 (define @t365 () (and @t185 @t219)) % 1.00/1.28 (define @t366 () (not @t185)) % 1.00/1.28 (define @t367 () (not @t219)) % 1.00/1.28 (define @t368 () (= @t214 @t365)) % 1.00/1.28 (define @t369 () (and @t180 @t187)) % 1.00/1.28 (define @t370 () (= @t191 @t369)) % 1.00/1.28 (define @t371 () (not @t191)) % 1.00/1.28 (define @t372 () (forall (@list @t224) (not (tptp.cowlNothing @t224)))) % 1.00/1.28 (define @t373 () (forall (@list @t226) (tptp.cowlThing @t226))) % 1.00/1.28 (assume @p1 @t5) % 1.00/1.28 (assume @p2 @t6) % 1.00/1.28 (assume @p3 (forall @t4 (= @t9 (and @t8 @t7)))) % 1.00/1.28 (assume @p4 (forall @t4 (= @t14 @t13))) % 1.00/1.28 (assume @p5 (forall @t4 (= @t17 (and @t16 (not @t14))))) % 1.00/1.28 (assume @p6 (forall @t4 (= @t18 (exists @t12 (and @t11 (tptp.cC104 @t10)))))) % 1.00/1.28 (assume @p7 (forall @t4 (= @t20 (and (not @t18) (not @t19))))) % 1.00/1.28 (assume @p8 (forall @t4 (= @t22 (and @t20 @t21)))) % 1.00/1.28 (assume @p9 (forall @t4 (= @t24 (and @t23 @t22)))) % 1.00/1.28 (assume @p10 @t26) % 1.00/1.28 (assume @p11 (forall @t4 (= @t27 (and @t25 @t24)))) % 1.00/1.28 (assume @p12 (forall @t4 (= @t29 @t28))) % 1.00/1.28 (assume @p13 (forall @t4 (= @t32 (and (not @t29) @t31)))) % 1.00/1.28 (assume @p14 (forall @t4 (= @t33 (exists @t12 (and @t11 (tptp.cC120 @t10)))))) % 1.00/1.28 (assume @p15 (forall @t4 (= @t34 @t28))) % 1.00/1.28 (assume @p16 (forall @t4 (= @t35 (and (not @t34) @t16)))) % 1.00/1.28 (assume @p17 (forall @t4 (= @t36 (exists @t12 (and @t11 (tptp.cC126 @t10)))))) % 1.00/1.28 (assume @p18 (forall @t4 (= @t37 (and (not @t33) (not @t36))))) % 1.00/1.28 (assume @p19 (forall @t4 (= @t38 (and @t21 @t37)))) % 1.00/1.28 (assume @p20 (forall @t4 (= @t39 (and @t38 @t27)))) % 1.00/1.28 (assume @p21 @t41) % 1.00/1.28 (assume @p22 (forall @t4 (= @t42 (and @t40 @t39)))) % 1.00/1.28 (assume @p23 (forall @t4 (= @t44 @t43))) % 1.00/1.28 (assume @p24 (forall @t4 (= @t46 @t45))) % 1.00/1.28 (assume @p25 (forall @t4 (= @t47 (and (not @t46) @t31)))) % 1.00/1.28 (assume @p26 (forall @t4 (= @t48 (exists @t12 (and @t11 (tptp.cC142 @t10)))))) % 1.00/1.28 (assume @p27 (forall @t4 (= @t49 @t45))) % 1.00/1.28 (assume @p28 (forall @t4 (= @t50 (and (not @t49) @t16)))) % 1.00/1.28 (assume @p29 (forall @t4 (= @t51 (exists @t12 (and @t11 (tptp.cC148 @t10)))))) % 1.00/1.28 (assume @p30 (forall @t4 (= @t52 (and (not @t51) (not @t48))))) % 1.00/1.28 (assume @p31 (forall @t4 (= @t53 (and @t21 @t52)))) % 1.00/1.28 (assume @p32 (forall @t4 (= @t54 (and @t53 @t42)))) % 1.00/1.28 (assume @p33 (forall @t4 (= @t56 (and @t55 @t54)))) % 1.00/1.28 (assume @p34 (forall @t4 (= @t57 (and @t44 @t9)))) % 1.00/1.28 (assume @p35 (forall @t4 (= @t58 @t13))) % 1.00/1.28 (assume @p36 (forall @t4 (= @t59 (exists @t12 (and @t11 (tptp.cC160 @t10)))))) % 1.00/1.28 (assume @p37 (forall @t4 (= @t60 @t28))) % 1.00/1.28 (assume @p38 (forall @t4 (= @t61 (exists @t12 (and @t11 (tptp.cC164 @t10)))))) % 1.00/1.28 (assume @p39 (forall @t4 (= @t62 (and (not @t61) (not @t59))))) % 1.00/1.28 (assume @p40 (forall @t4 (= @t64 @t63))) % 1.00/1.28 (assume @p41 (forall @t4 (= @t65 (exists @t12 (and @t11 (tptp.cC170 @t10)))))) % 1.00/1.28 (assume @p42 (forall @t4 (= @t66 (and @t62 (not @t65))))) % 1.00/1.28 (assume @p43 (forall @t4 (= @t67 @t45))) % 1.00/1.28 (assume @p44 (forall @t4 (= @t68 (exists @t12 (and @t11 (tptp.cC176 @t10)))))) % 1.00/1.28 (assume @p45 (forall @t4 (= @t69 (and (not @t68) @t66)))) % 1.00/1.28 (assume @p46 (forall @t4 (= @t70 @t63))) % 1.00/1.28 (assume @p47 (forall @t4 (= @t55 (and @t57 @t70)))) % 1.00/1.28 (assume @p48 (forall @t4 (= @t75 @t74))) % 1.00/1.28 (assume @p49 (forall @t4 (= @t77 (and (not @t75) @t76)))) % 1.00/1.28 (assume @p50 (forall @t4 (= @t78 (exists @t12 (and @t11 (tptp.cC26 @t10)))))) % 1.00/1.28 (assume @p51 (forall @t4 (= @t79 @t43))) % 1.00/1.28 (assume @p52 (forall @t4 (= @t80 (and @t76 (not @t79))))) % 1.00/1.28 (assume @p53 (forall @t4 (= @t81 (exists @t12 (and @t11 (tptp.cC32 @t10)))))) % 1.00/1.28 (assume @p54 (forall @t4 (= @t82 (and (not @t78) (not @t81))))) % 1.00/1.28 (assume @p55 (forall @t4 (= @t83 (and @t82 @t21)))) % 1.00/1.28 (assume @p56 @t85) % 1.00/1.28 (assume @p57 @t87) % 1.00/1.28 (assume @p58 (forall @t4 (= @t88 (and @t86 @t83)))) % 1.00/1.28 (assume @p59 (forall @t4 (= @t89 @t74))) % 1.00/1.28 (assume @p60 (forall @t4 (= @t91 (and @t90 (not @t89))))) % 1.00/1.28 (assume @p61 (forall @t4 (= @t92 (exists @t12 (and @t11 (tptp.cC46 @t10)))))) % 1.00/1.28 (assume @p62 (forall @t4 (= @t93 @t43))) % 1.00/1.28 (assume @p63 (forall @t4 (= @t94 (and @t90 (not @t93))))) % 1.00/1.28 (assume @p64 (forall @t4 (= @t95 (exists @t12 (and @t11 (tptp.cC52 @t10)))))) % 1.00/1.28 (assume @p65 (forall @t4 (= @t96 (and (not @t92) (not @t95))))) % 1.00/1.28 (assume @p66 (forall @t4 (= @t97 (and @t96 @t21)))) % 1.00/1.28 (assume @p67 (forall @t4 (= @t98 (and @t97 @t88)))) % 1.00/1.28 (assume @p68 @t100) % 1.00/1.28 (assume @p69 (forall @t4 (= @t101 (and @t99 @t98)))) % 1.00/1.28 (assume @p70 (forall @t4 (= @t102 @t74))) % 1.00/1.28 (assume @p71 (forall @t4 (= @t105 (and (not @t102) @t104)))) % 1.00/1.28 (assume @p72 (forall @t4 (= @t106 (exists @t12 (and @t11 (tptp.cC68 @t10)))))) % 1.00/1.28 (assume @p73 (forall @t4 (= @t107 @t43))) % 1.00/1.28 (assume @p74 (forall @t4 (= @t108 (and @t104 (not @t107))))) % 1.00/1.28 (assume @p75 (forall @t4 (= @t109 (exists @t12 (and @t11 (tptp.cC74 @t10)))))) % 1.00/1.28 (assume @p76 (forall @t4 (= @t110 (and (not @t106) (not @t109))))) % 1.00/1.28 (assume @p77 (forall @t4 (= @t8 @t13))) % 1.00/1.28 (assume @p78 (forall @t4 (= @t111 (and @t21 @t110)))) % 1.00/1.28 (assume @p79 (forall @t4 (= @t112 (and @t111 @t101)))) % 1.00/1.28 (assume @p80 @t114) % 1.00/1.28 (assume @p81 (forall @t4 (= @t115 (and @t112 @t113)))) % 1.00/1.28 (assume @p82 @t117) % 1.00/1.28 (assume @p83 (forall @t4 (= @t23 (and @t116 @t115)))) % 1.00/1.28 (assume @p84 (forall @t4 (= @t118 @t13))) % 1.00/1.28 (assume @p85 (forall @t4 (= @t119 (and @t31 (not @t118))))) % 1.00/1.28 (assume @p86 (forall @t4 (= @t19 (exists @t12 (and @t11 (tptp.cC96 @t10)))))) % 1.00/1.28 (assume @p87 (forall @t4 (= (tptp.cTEST @t1) (and @t56 @t69)))) % 1.00/1.28 (assume @p88 (forall @t4 (=> @t120 (not @t77)))) % 1.00/1.28 (assume @p89 @t121) % 1.00/1.28 (assume @p90 @t122) % 1.00/1.28 (assume @p91 (forall @t4 (=> @t120 (not @t17)))) % 1.00/1.28 (assume @p92 @t124) % 1.00/1.28 (assume @p93 @t126) % 1.00/1.28 (assume @p94 (forall @t4 (=> @t120 (not @t50)))) % 1.00/1.28 (assume @p95 (forall @t4 (=> @t120 (not @t58)))) % 1.00/1.28 (assume @p96 @t128) % 1.00/1.28 (assume @p97 @t130) % 1.00/1.28 (assume @p98 (forall @t4 (=> @t120 (not @t35)))) % 1.00/1.28 (assume @p99 @t132) % 1.00/1.28 (assume @p100 (not (tptp.cC178 tptp.iV21026))) % 1.00/1.28 (assume @p101 @t134) % 1.00/1.28 (assume @p102 @t136) % 1.00/1.28 (assume @p103 (forall @t4 (=> @t120 (not @t105)))) % 1.00/1.28 (assume @p104 (forall @t4 (=> @t120 (not @t60)))) % 1.00/1.28 (assume @p105 (forall @t4 (=> @t120 (not @t91)))) % 1.00/1.28 (assume @p106 (forall @t4 (=> @t120 (not @t94)))) % 1.00/1.28 (assume @p107 (forall @t4 (=> @t120 (not @t67)))) % 1.00/1.28 (assume @p108 (forall @t4 (=> @t120 (not @t47)))) % 1.00/1.28 (assume @p109 @t138) % 1.00/1.28 (assume @p110 @t140) % 1.00/1.28 (assume @p111 @t142) % 1.00/1.28 (assume @p112 @t144) % 1.00/1.28 (assume @p113 @t146) % 1.00/1.28 (assume @p114 @t148) % 1.00/1.28 (assume @p115 (forall @t4 (=> @t120 (not @t80)))) % 1.00/1.28 (assume @p116 @t150) % 1.00/1.28 (assume @p117 @t152) % 1.00/1.28 (assume @p118 (forall @t4 (=> @t120 (not @t32)))) % 1.00/1.28 (assume @p119 (forall @t4 (=> @t120 (not @t119)))) % 1.00/1.28 (assume @p120 (forall @t4 (=> @t120 (not @t64)))) % 1.00/1.28 (assume @p121 @t153) % 1.00/1.28 (assume @p122 (forall @t4 (=> @t120 (not @t108)))) % 1.00/1.28 (assume @p123 (tptp.rR1 tptp.iV21026 tptp.iV21030)) % 1.00/1.28 (assume @p124 @t154) % 1.00/1.28 (assume @p125 (tptp.rR1 tptp.iV21026 tptp.iV21028)) % 1.00/1.28 (assume @p126 (tptp.rR1 tptp.iV21026 tptp.iV21029)) % 1.00/1.28 (assume @p127 (not @t155)) % 1.00/1.28 (assume @p128 (not (tptp.cC176 tptp.iV21027))) % 1.00/1.28 (assume @p129 (forall @t4 (=> @t156 @t103))) % 1.00/1.28 (assume @p130 (not (tptp.cC46 tptp.iV21027))) % 1.00/1.28 (assume @p131 (not (tptp.cC170 tptp.iV21027))) % 1.00/1.28 (assume @p132 (tptp.cC12 tptp.iV21027)) % 1.00/1.28 (assume @p133 (not (tptp.cC120 tptp.iV21027))) % 1.00/1.28 (assume @p134 (not (tptp.cC74 tptp.iV21027))) % 1.00/1.28 (assume @p135 (forall @t4 (=> @t156 @t157))) % 1.00/1.28 (assume @p136 (not (tptp.cC52 tptp.iV21027))) % 1.00/1.28 (assume @p137 (not @t158)) % 1.00/1.28 (assume @p138 (not (tptp.cC96 tptp.iV21027))) % 1.00/1.28 (assume @p139 (not (tptp.cC68 tptp.iV21027))) % 1.00/1.28 (assume @p140 (tptp.cC92 tptp.iV21027)) % 1.00/1.28 (assume @p141 (not (tptp.cC126 tptp.iV21027))) % 1.00/1.28 (assume @p142 (tptp.cC100 tptp.iV21027)) % 1.00/1.28 (assume @p143 (not (tptp.cC160 tptp.iV21027))) % 1.00/1.28 (assume @p144 (not (tptp.cC104 tptp.iV21027))) % 1.00/1.28 (assume @p145 (not (tptp.cC148 tptp.iV21027))) % 1.00/1.28 (assume @p146 (not (tptp.cC142 tptp.iV21027))) % 1.00/1.28 (assume @p147 (tptp.cC18 tptp.iV21027)) % 1.00/1.28 (assume @p148 (forall @t4 (=> @t156 @t30))) % 1.00/1.28 (assume @p149 (forall @t4 (=> @t156 @t15))) % 1.00/1.28 (assume @p150 (not (tptp.cC164 tptp.iV21027))) % 1.00/1.28 (assume @p151 @t160) % 1.00/1.28 (assume @p152 @t161) % 1.00/1.28 (assume @p153 (tptp.rR1 tptp.iV21027 tptp.iV21036)) % 1.00/1.28 (assume @p154 (tptp.rR1 tptp.iV21027 tptp.iV21035)) % 1.00/1.28 (assume @p155 (tptp.cowlThing tptp.iV21028)) % 1.00/1.28 (assume @p156 (not (tptp.cC148 tptp.iV21029))) % 1.00/1.28 (assume @p157 (not (tptp.cC68 tptp.iV21029))) % 1.00/1.28 (assume @p158 (not @t162)) % 1.00/1.28 (assume @p159 (not (tptp.cC104 tptp.iV21029))) % 1.00/1.28 (assume @p160 (forall @t4 (=> @t163 @t15))) % 1.00/1.28 (assume @p161 (not (tptp.cC176 tptp.iV21029))) % 1.00/1.28 (assume @p162 (not (tptp.cC142 tptp.iV21029))) % 1.00/1.28 (assume @p163 (forall @t4 (=> @t163 @t30))) % 1.00/1.28 (assume @p164 @t165) % 1.00/1.28 (assume @p165 (tptp.cC2 tptp.iV21029)) % 1.00/1.28 (assume @p166 (not (tptp.cC74 tptp.iV21029))) % 1.00/1.28 (assume @p167 (not (tptp.cC120 tptp.iV21029))) % 1.00/1.28 (assume @p168 (tptp.cC92 tptp.iV21029)) % 1.00/1.28 (assume @p169 (not @t166)) % 1.00/1.28 (assume @p170 (not (tptp.cC32 tptp.iV21029))) % 1.00/1.28 (assume @p171 (tptp.cC100 tptp.iV21029)) % 1.00/1.28 (assume @p172 (tptp.cC18 tptp.iV21029)) % 1.00/1.28 (assume @p173 (not (tptp.cC170 tptp.iV21029))) % 1.00/1.28 (assume @p174 (not (tptp.cC26 tptp.iV21029))) % 1.00/1.28 (assume @p175 (not (tptp.cC96 tptp.iV21029))) % 1.00/1.28 (assume @p176 (not (tptp.cC126 tptp.iV21029))) % 1.00/1.28 (assume @p177 (forall @t4 (=> @t163 @t157))) % 1.00/1.28 (assume @p178 (not (tptp.cC164 tptp.iV21029))) % 1.00/1.28 (assume @p179 (not (tptp.cC160 tptp.iV21029))) % 1.00/1.28 (assume @p180 (forall @t4 (=> @t163 @t103))) % 1.00/1.28 (assume @p181 @t167) % 1.00/1.28 (assume @p182 (tptp.rR1 tptp.iV21029 tptp.iV21034)) % 1.00/1.28 (assume @p183 (tptp.rR1 tptp.iV21029 tptp.iV21033)) % 1.00/1.28 (assume @p184 (not (tptp.cC32 tptp.iV21030))) % 1.00/1.28 (assume @p185 (not (tptp.cC26 tptp.iV21030))) % 1.00/1.28 (assume @p186 (not (tptp.cC126 tptp.iV21030))) % 1.00/1.28 (assume @p187 (forall @t4 (=> @t168 @t103))) % 1.00/1.28 (assume @p188 (not (tptp.cC148 tptp.iV21030))) % 1.00/1.28 (assume @p189 (not (tptp.cC46 tptp.iV21030))) % 1.00/1.28 (assume @p190 (forall @t4 (=> @t168 @t157))) % 1.00/1.28 (assume @p191 (tptp.cC12 tptp.iV21030)) % 1.00/1.28 (assume @p192 (not @t169)) % 1.00/1.28 (assume @p193 (not @t170)) % 1.00/1.28 (assume @p194 (not (tptp.cC96 tptp.iV21030))) % 1.00/1.28 (assume @p195 (not (tptp.cC176 tptp.iV21030))) % 1.00/1.28 (assume @p196 (tptp.cC2 tptp.iV21030)) % 1.00/1.28 (assume @p197 (not (tptp.cC104 tptp.iV21030))) % 1.00/1.28 (assume @p198 (tptp.cC92 tptp.iV21030)) % 1.00/1.28 (assume @p199 (tptp.cC100 tptp.iV21030)) % 1.00/1.28 (assume @p200 (not (tptp.cC120 tptp.iV21030))) % 1.00/1.28 (assume @p201 (forall @t4 (=> @t168 @t15))) % 1.00/1.28 (assume @p202 (not (tptp.cC170 tptp.iV21030))) % 1.00/1.28 (assume @p203 @t172) % 1.00/1.28 (assume @p204 (forall @t4 (=> @t168 @t30))) % 1.00/1.28 (assume @p205 (not (tptp.cC52 tptp.iV21030))) % 1.00/1.28 (assume @p206 (not (tptp.cC160 tptp.iV21030))) % 1.00/1.28 (assume @p207 (not (tptp.cC164 tptp.iV21030))) % 1.00/1.28 (assume @p208 @t173) % 1.00/1.28 (assume @p209 (not (tptp.cC142 tptp.iV21030))) % 1.00/1.28 (assume @p210 (tptp.rR1 tptp.iV21030 tptp.iV21032)) % 1.00/1.28 (assume @p211 (tptp.rR1 tptp.iV21030 tptp.iV21031)) % 1.00/1.28 (assume @p212 (tptp.cowlThing tptp.iV21031)) % 1.00/1.28 (assume @p213 (tptp.cC92 tptp.iV21032)) % 1.00/1.28 (assume @p214 (tptp.cC100 tptp.iV21032)) % 1.00/1.28 (assume @p215 (not (tptp.cC2 tptp.iV21032))) % 1.00/1.28 (assume @p216 (tptp.cC18 tptp.iV21032)) % 1.00/1.28 (assume @p217 (tptp.cC6 tptp.iV21032)) % 1.00/1.28 (assume @p218 (tptp.cowlThing tptp.iV21032)) % 1.00/1.28 (assume @p219 (tptp.cC92 tptp.iV21033)) % 1.00/1.28 (assume @p220 (tptp.cC100 tptp.iV21033)) % 1.00/1.28 (assume @p221 (tptp.cC18 tptp.iV21033)) % 1.00/1.28 (assume @p222 (tptp.cC6 tptp.iV21033)) % 1.00/1.28 (assume @p223 (not (tptp.cC12 tptp.iV21033))) % 1.00/1.28 (assume @p224 (tptp.cowlThing tptp.iV21033)) % 1.00/1.28 (assume @p225 (tptp.cC92 tptp.iV21034)) % 1.00/1.28 (assume @p226 (tptp.cC100 tptp.iV21034)) % 1.00/1.28 (assume @p227 (tptp.cC18 tptp.iV21034)) % 1.00/1.28 (assume @p228 (tptp.cC6 tptp.iV21034)) % 1.00/1.28 (assume @p229 (not (tptp.cC2 tptp.iV21034))) % 1.00/1.28 (assume @p230 (tptp.cowlThing tptp.iV21034)) % 1.00/1.28 (assume @p231 (tptp.cC92 tptp.iV21035)) % 1.00/1.28 (assume @p232 (tptp.cC100 tptp.iV21035)) % 1.00/1.28 (assume @p233 (not (tptp.cC12 tptp.iV21035))) % 1.00/1.28 (assume @p234 (tptp.cC18 tptp.iV21035)) % 1.00/1.28 (assume @p235 (tptp.cC6 tptp.iV21035)) % 1.00/1.28 (assume @p236 (tptp.cowlThing tptp.iV21035)) % 1.00/1.28 (assume @p237 (tptp.cC92 tptp.iV21036)) % 1.00/1.28 (assume @p238 (tptp.cC100 tptp.iV21036)) % 1.00/1.28 (assume @p239 (tptp.cC18 tptp.iV21036)) % 1.00/1.28 (assume @p240 (tptp.cC6 tptp.iV21036)) % 1.00/1.28 (assume @p241 (not (tptp.cC2 tptp.iV21036))) % 1.00/1.28 (assume @p242 (tptp.cowlThing tptp.iV21036)) % 1.00/1.28 (assume @p243 @t221) % 1.00/1.28 (assume @p244 true) % 1.00/1.28 (step @p245 :rule alpha_equiv :args (@t222 @t223 (@list @t224))) % 1.00/1.28 (step @p246 :rule alpha_equiv :args (@t225 @t223 (@list @t226))) % 1.00/1.28 (step @p247 :rule nary_cong :premises (@p246 @p245) :args (@t227)) % 1.00/1.28 (step @p248 :rule quant-miniscope-and :args ((= @t5 @t227))) % 1.00/1.28 (step @p249 :rule trans :premises (@p248 @p247)) % 1.00/1.28 (step @p250 :rule eq_resolve :premises (@p1 @p249)) % 1.00/1.28 (step @p251 :rule and_elim :premises (@p250) :args (0)) % 1.00/1.28 (step @p252 :rule and_elim :premises (@p250) :args (1)) % 1.00/1.28 (step @p253 :rule instantiate :premises (@p74) :args (@t228)) % 1.00/1.28 (step @p254 :rule cnf_equiv_pos2 :args (@t231)) % 1.00/1.28 (step @p255 :rule reordering :premises (@p254) :args ((or @t170 @t232 (not @t231)))) % 1.00/1.28 (step @p256 :rule chain_m_resolution :premises (@p255 @p193 @p253) :args (@t232 @t233 (@list @t170 @t231))) % 1.00/1.28 (step @p257 :rule bool-double-not-elim :args (@t174)) % 1.00/1.28 (step @p258 :rule bool-double-not-elim :args (@t171)) % 1.00/1.28 (step @p259 :rule refl :args (@t230)) % 1.00/1.28 (step @p260 :rule nary_cong :premises (@p259 @p258 @p257) :args ((or @t230 @t234 (not @t229)))) % 1.00/1.28 (step @p261 :rule cnf_and_neg :args (@t230)) % 1.00/1.28 (step @p262 :rule eq_resolve :premises (@p261 @p260)) % 1.00/1.28 (step @p263 :rule reordering :premises (@p262) :args ((or @t171 @t174 @t230))) % 1.00/1.28 (step @p264 :rule chain_m_resolution :premises (@p263 @p203 @p256) :args (@t174 @t235 (@list @t171 @t230))) % 1.00/1.28 (step @p265 :rule instantiate :premises (@p71) :args (@t228)) % 1.00/1.28 (step @p266 :rule cnf_equiv_pos2 :args (@t238)) % 1.00/1.28 (step @p267 :rule reordering :premises (@p266) :args ((or @t169 @t239 (not @t238)))) % 1.00/1.28 (step @p268 :rule chain_m_resolution :premises (@p267 @p192 @p265) :args (@t239 @t233 (@list @t169 @t238))) % 1.00/1.28 (step @p269 :rule bool-double-not-elim :args (@t175)) % 1.00/1.28 (step @p270 :rule refl :args (@t237)) % 1.00/1.28 (step @p271 :rule nary_cong :premises (@p270 @p269 @p258) :args ((or @t237 (not @t236) @t234))) % 1.00/1.28 (step @p272 :rule cnf_and_neg :args (@t237)) % 1.00/1.28 (step @p273 :rule eq_resolve :premises (@p272 @p271)) % 1.00/1.28 (step @p274 :rule reordering :premises (@p273) :args ((or @t171 @t175 @t237))) % 1.00/1.28 (step @p275 :rule chain_m_resolution :premises (@p274 @p203 @p268) :args (@t175 @t235 (@list @t171 @t237))) % 1.00/1.28 (step @p276 :rule instantiate :premises (@p60) :args (@t240)) % 1.00/1.28 (step @p277 :rule cnf_equiv_pos2 :args (@t243)) % 1.00/1.28 (step @p278 :rule reordering :premises (@p277) :args ((or @t162 @t244 (not @t243)))) % 1.00/1.28 (step @p279 :rule chain_m_resolution :premises (@p278 @p158 @p276) :args (@t244 @t233 (@list @t162 @t243))) % 1.00/1.28 (step @p280 :rule bool-double-not-elim :args (@t176)) % 1.00/1.28 (step @p281 :rule bool-double-not-elim :args (@t164)) % 1.00/1.28 (step @p282 :rule refl :args (@t242)) % 1.00/1.28 (step @p283 :rule nary_cong :premises (@p282 @p281 @p280) :args ((or @t242 @t245 (not @t241)))) % 1.00/1.28 (step @p284 :rule cnf_and_neg :args (@t242)) % 1.00/1.28 (step @p285 :rule eq_resolve :premises (@p284 @p283)) % 1.00/1.28 (step @p286 :rule reordering :premises (@p285) :args ((or @t164 @t176 @t242))) % 1.00/1.28 (step @p287 :rule chain_m_resolution :premises (@p286 @p164 @p279) :args (@t176 @t235 (@list @t164 @t242))) % 1.00/1.28 (step @p288 :rule instantiate :premises (@p63) :args (@t240)) % 1.00/1.28 (step @p289 :rule cnf_equiv_pos2 :args (@t248)) % 1.00/1.28 (step @p290 :rule reordering :premises (@p289) :args ((or @t166 @t249 (not @t248)))) % 1.00/1.28 (step @p291 :rule chain_m_resolution :premises (@p290 @p169 @p288) :args (@t249 @t233 (@list @t166 @t248))) % 1.00/1.28 (step @p292 :rule bool-double-not-elim :args (@t177)) % 1.00/1.28 (step @p293 :rule refl :args (@t247)) % 1.00/1.28 (step @p294 :rule nary_cong :premises (@p293 @p281 @p292) :args ((or @t247 @t245 (not @t246)))) % 1.00/1.28 (step @p295 :rule cnf_and_neg :args (@t247)) % 1.00/1.28 (step @p296 :rule eq_resolve :premises (@p295 @p294)) % 1.00/1.28 (step @p297 :rule reordering :premises (@p296) :args ((or @t164 @t177 @t247))) % 1.00/1.28 (step @p298 :rule chain_m_resolution :premises (@p297 @p164 @p291) :args (@t177 @t235 (@list @t164 @t247))) % 1.00/1.28 (step @p299 :rule instantiate :premises (@p49) :args (@t250)) % 1.00/1.28 (step @p300 :rule cnf_equiv_pos2 :args (@t253)) % 1.00/1.28 (step @p301 :rule reordering :premises (@p300) :args ((or @t155 @t254 (not @t253)))) % 1.00/1.28 (step @p302 :rule chain_m_resolution :premises (@p301 @p127 @p299) :args (@t254 @t233 (@list @t155 @t253))) % 1.00/1.28 (step @p303 :rule bool-double-not-elim :args (@t159)) % 1.00/1.28 (step @p304 :rule bool-double-not-elim :args (@t178)) % 1.00/1.28 (step @p305 :rule refl :args (@t252)) % 1.00/1.28 (step @p306 :rule nary_cong :premises (@p305 @p304 @p303) :args ((or @t252 (not @t251) @t255))) % 1.00/1.28 (step @p307 :rule cnf_and_neg :args (@t252)) % 1.00/1.28 (step @p308 :rule eq_resolve :premises (@p307 @p306)) % 1.00/1.28 (step @p309 :rule reordering :premises (@p308) :args ((or @t159 @t178 @t252))) % 1.00/1.28 (step @p310 :rule chain_m_resolution :premises (@p309 @p151 @p302) :args (@t178 @t235 (@list @t159 @t252))) % 1.00/1.28 (step @p311 :rule instantiate :premises (@p52) :args (@t250)) % 1.00/1.28 (step @p312 :rule cnf_equiv_pos2 :args (@t258)) % 1.00/1.28 (step @p313 :rule reordering :premises (@p312) :args ((or @t158 @t259 (not @t258)))) % 1.00/1.28 (step @p314 :rule chain_m_resolution :premises (@p313 @p137 @p311) :args (@t259 @t233 (@list @t158 @t258))) % 1.00/1.28 (step @p315 :rule bool-double-not-elim :args (@t179)) % 1.00/1.28 (step @p316 :rule refl :args (@t257)) % 1.00/1.28 (step @p317 :rule nary_cong :premises (@p316 @p303 @p315) :args ((or @t257 @t255 (not @t256)))) % 1.00/1.28 (step @p318 :rule cnf_and_neg :args (@t257)) % 1.00/1.28 (step @p319 :rule eq_resolve :premises (@p318 @p317)) % 1.00/1.28 (step @p320 :rule reordering :premises (@p319) :args ((or @t159 @t179 @t257))) % 1.00/1.28 (step @p321 :rule chain_m_resolution :premises (@p320 @p151 @p314) :args (@t179 @t235 (@list @t159 @t257))) % 1.00/1.28 (step @p322 :rule instantiate :premises (@p11) :args (@t260)) % 1.00/1.28 (step @p323 :rule instantiate :premises (@p20) :args (@t260)) % 1.00/1.28 (step @p324 :rule instantiate :premises (@p22) :args (@t260)) % 1.00/1.28 (step @p325 :rule instantiate :premises (@p32) :args (@t260)) % 1.00/1.28 (step @p326 :rule instantiate :premises (@p33) :args (@t260)) % 1.00/1.28 (step @p327 :rule instantiate :premises (@p87) :args (@t260)) % 1.00/1.28 (step @p328 :rule cnf_equiv_pos1 :args (@t262)) % 1.00/1.28 (step @p329 :rule reordering :premises (@p328) :args ((or (not @t122) @t261 (not @t262)))) % 1.00/1.28 (step @p330 :rule chain_m_resolution :premises (@p329 @p90 @p327) :args (@t261 @t263 (@list @t122 @t262))) % 1.00/1.28 (step @p331 :rule cnf_and_pos :args (@t261 0)) % 1.00/1.28 (step @p332 :rule reordering :premises (@p331) :args ((or @t208 @t264))) % 1.00/1.28 (step @p333 :rule chain_m_resolution :premises (@p332 @p330) :args (@t208 @t265 @t266)) % 1.00/1.28 (step @p334 :rule cnf_equiv_pos1 :args (@t268)) % 1.00/1.28 (step @p335 :rule reordering :premises (@p334) :args ((or @t269 @t267 (not @t268)))) % 1.00/1.28 (step @p336 :rule chain_m_resolution :premises (@p335 @p333 @p326) :args (@t267 @t263 (@list @t208 @t268))) % 1.00/1.28 (step @p337 :rule cnf_and_pos :args (@t267 1)) % 1.00/1.28 (step @p338 :rule reordering :premises (@p337) :args ((or @t211 @t270))) % 1.00/1.28 (step @p339 :rule chain_m_resolution :premises (@p338 @p336) :args (@t211 @t265 @t271)) % 1.00/1.28 (step @p340 :rule cnf_equiv_pos1 :args (@t273)) % 1.00/1.28 (step @p341 :rule reordering :premises (@p340) :args ((or @t274 @t272 (not @t273)))) % 1.00/1.28 (step @p342 :rule chain_m_resolution :premises (@p341 @p339 @p325) :args (@t272 @t263 (@list @t211 @t273))) % 1.00/1.28 (step @p343 :rule cnf_and_pos :args (@t272 1)) % 1.00/1.28 (step @p344 :rule reordering :premises (@p343) :args ((or @t184 (not @t272)))) % 1.00/1.28 (step @p345 :rule chain_m_resolution :premises (@p344 @p342) :args (@t184 @t265 (@list @t272))) % 1.00/1.28 (step @p346 :rule cnf_equiv_pos1 :args (@t276)) % 1.00/1.28 (step @p347 :rule reordering :premises (@p346) :args ((or @t277 @t275 (not @t276)))) % 1.00/1.28 (step @p348 :rule chain_m_resolution :premises (@p347 @p345 @p324) :args (@t275 @t263 (@list @t184 @t276))) % 1.00/1.28 (step @p349 :rule cnf_and_pos :args (@t275 1)) % 1.00/1.28 (step @p350 :rule reordering :premises (@p349) :args ((or @t206 (not @t275)))) % 1.00/1.28 (step @p351 :rule chain_m_resolution :premises (@p350 @p348) :args (@t206 @t265 (@list @t275))) % 1.00/1.28 (step @p352 :rule cnf_equiv_pos1 :args (@t279)) % 1.00/1.28 (step @p353 :rule reordering :premises (@p352) :args ((or @t280 @t278 (not @t279)))) % 1.00/1.28 (step @p354 :rule chain_m_resolution :premises (@p353 @p351 @p323) :args (@t278 @t263 (@list @t206 @t279))) % 1.00/1.28 (step @p355 :rule cnf_and_pos :args (@t278 1)) % 1.00/1.28 (step @p356 :rule reordering :premises (@p355) :args ((or @t186 (not @t278)))) % 1.00/1.28 (step @p357 :rule chain_m_resolution :premises (@p356 @p354) :args (@t186 @t265 (@list @t278))) % 1.00/1.28 (step @p358 :rule cnf_equiv_pos1 :args (@t282)) % 1.00/1.28 (step @p359 :rule reordering :premises (@p358) :args ((or @t283 @t281 (not @t282)))) % 1.00/1.28 (step @p360 :rule chain_m_resolution :premises (@p359 @p357 @p322) :args (@t281 @t263 (@list @t186 @t282))) % 1.00/1.28 (step @p361 :rule cnf_and_pos :args (@t281 1)) % 1.00/1.28 (step @p362 :rule reordering :premises (@p361) :args ((or @t191 (not @t281)))) % 1.00/1.28 (step @p363 :rule chain_m_resolution :premises (@p362 @p360) :args (@t191 @t265 (@list @t281))) % 1.00/1.28 (step @p364 :rule instantiate :premises (@p34) :args (@t260)) % 1.00/1.28 (step @p365 :rule instantiate :premises (@p47) :args (@t260)) % 1.00/1.28 (step @p366 :rule cnf_and_pos :args (@t267 0)) % 1.00/1.28 (step @p367 :rule reordering :premises (@p366) :args ((or @t205 @t270))) % 1.00/1.28 (step @p368 :rule chain_m_resolution :premises (@p367 @p336) :args (@t205 @t265 @t271)) % 1.00/1.28 (step @p369 :rule cnf_equiv_pos1 :args (@t285)) % 1.00/1.28 (step @p370 :rule reordering :premises (@p369) :args ((or @t286 @t284 (not @t285)))) % 1.00/1.28 (step @p371 :rule chain_m_resolution :premises (@p370 @p368 @p365) :args (@t284 @t263 (@list @t205 @t285))) % 1.00/1.28 (step @p372 :rule cnf_and_pos :args (@t284 0)) % 1.00/1.28 (step @p373 :rule reordering :premises (@p372) :args ((or @t218 @t287))) % 1.00/1.28 (step @p374 :rule chain_m_resolution :premises (@p373 @p371) :args (@t218 @t265 @t288)) % 1.00/1.28 (step @p375 :rule cnf_equiv_pos1 :args (@t290)) % 1.00/1.28 (step @p376 :rule reordering :premises (@p375) :args ((or @t291 @t289 (not @t290)))) % 1.00/1.28 (step @p377 :rule chain_m_resolution :premises (@p376 @p374 @p364) :args (@t289 @t263 (@list @t218 @t290))) % 1.00/1.28 (step @p378 :rule cnf_and_pos :args (@t289 0)) % 1.00/1.28 (step @p379 :rule reordering :premises (@p378) :args ((or @t181 @t292))) % 1.00/1.28 (step @p380 :rule chain_m_resolution :premises (@p379 @p377) :args (@t181 @t265 @t293)) % 1.00/1.28 (step @p381 :rule instantiate :premises (@p7) :args (@t260)) % 1.00/1.28 (step @p382 :rule bool-double-not-elim :args (@t123)) % 1.00/1.28 (step @p383 :rule bool-double-not-elim :args (@t141)) % 1.00/1.28 (step @p384 :rule refl :args (@t294)) % 1.00/1.28 (step @p385 :rule nary_cong :premises (@p384 @p383 @p382) :args ((or @t294 (not @t142) (not @t124)))) % 1.00/1.28 (step @p386 :rule cnf_and_neg :args (@t294)) % 1.00/1.28 (step @p387 :rule eq_resolve :premises (@p386 @p385)) % 1.00/1.28 (step @p388 :rule reordering :premises (@p387) :args ((or @t123 @t141 @t294))) % 1.00/1.28 (step @p389 :rule chain_m_resolution :premises (@p388 @p92 @p111) :args (@t294 @t235 (@list @t123 @t141))) % 1.00/1.28 (step @p390 :rule cnf_equiv_pos2 :args (@t295)) % 1.00/1.28 (step @p391 :rule reordering :premises (@p390) :args ((or @t182 (not @t294) (not @t295)))) % 1.00/1.28 (step @p392 :rule chain_m_resolution :premises (@p391 @p389 @p381) :args (@t182 @t263 (@list @t294 @t295))) % 1.00/1.28 (step @p393 :rule bool-double-not-elim :args (@t71)) % 1.00/1.28 (step @p394 :rule refl :args (@t296)) % 1.00/1.28 (step @p395 :rule nary_cong :premises (@p394 @p393) :args ((or @t296 (not @t72)))) % 1.00/1.28 (step @p396 :rule bool-and-de-morgan :args (@t11 @t72 true)) % 1.00/1.28 (step @p397 :rule trans :premises (@p396 @p395)) % 1.00/1.28 (step @p398 :rule cong :premises (@p397) :args (@t297)) % 1.00/1.28 (step @p399 :rule cong :premises (@p398) :args (@t298)) % 1.00/1.28 (step @p400 :rule exists-elim :args ((= @t74 @t298))) % 1.00/1.28 (step @p401 :rule trans :premises (@p400 @p399)) % 1.00/1.28 (step @p402 :rule refl :args (@t7)) % 1.00/1.28 (step @p403 :rule cong :premises (@p402 @p401) :args (@t84)) % 1.00/1.28 (step @p404 :rule cong :premises (@p403) :args (@t85)) % 1.00/1.28 (step @p405 :rule eq_resolve :premises (@p56 @p404)) % 1.00/1.28 (step @p406 :rule instantiate :premises (@p405) :args (@t260)) % 1.00/1.28 (step @p407 :rule cnf_or_pos :args (@t300)) % 1.00/1.28 (step @p408 :rule reordering :premises (@p407) :args ((or @t159 @t299 @t301))) % 1.00/1.28 (step @p409 :rule chain_m_resolution :premises (@p408 @p151 @p124) :args (@t301 @t233 (@list @t159 @t154))) % 1.00/1.28 (assume-push @p708 @t302) % 1.00/1.28 (step @p411 :rule instantiate :premises (@p708) :args (@t250)) % 1.00/1.28 (step-pop @p709 :rule scope :premises (@p411)) % 1.00/1.28 (step @p412 :rule process_scope :premises (@p709) :args (@t300)) % 1.00/1.28 (step @p414 :rule implies_elim :premises (@p412)) % 1.00/1.28 (step @p415 :rule chain_m_resolution :premises (@p414 @p409) :args (@t303 (@list true) (@list @t300))) % 1.00/1.28 (step @p416 :rule bool-double-not-elim :args (@t302)) % 1.00/1.28 (step @p417 :rule refl :args (@t183)) % 1.00/1.28 (step @p418 :rule refl :args (@t305)) % 1.00/1.28 (step @p419 :rule nary_cong :premises (@p418 @p417 @p416) :args ((or @t305 @t183 (not @t303)))) % 1.00/1.28 (step @p420 :rule cnf_equiv_pos2 :args (@t304)) % 1.00/1.28 (step @p421 :rule eq_resolve :premises (@p420 @p419)) % 1.00/1.28 (step @p422 :rule reordering :premises (@p421) :args ((or @t183 @t302 @t305))) % 1.00/1.28 (step @p423 :rule chain_m_resolution :premises (@p422 @p415 @p406) :args (@t183 @t233 (@list @t302 @t304))) % 1.00/1.28 (step @p424 :rule instantiate :premises (@p79) :args (@t260)) % 1.00/1.28 (step @p425 :rule instantiate :premises (@p69) :args (@t260)) % 1.00/1.28 (step @p426 :rule eq-symm :args (@t99 @t21)) % 1.00/1.28 (step @p427 :rule cong :premises (@p426) :args (@t100)) % 1.00/1.28 (step @p428 :rule eq_resolve :premises (@p68 @p427)) % 1.00/1.28 (step @p429 :rule instantiate :premises (@p428) :args (@t260)) % 1.00/1.28 (step @p430 :rule cnf_equiv_pos1 :args (@t306)) % 1.00/1.28 (step @p431 :rule reordering :premises (@p430) :args ((or @t196 @t307 (not @t306)))) % 1.00/1.28 (step @p432 :rule chain_m_resolution :premises (@p431 @p89 @p429) :args (@t196 @t263 (@list @t121 @t306))) % 1.00/1.28 (step @p433 :rule instantiate :premises (@p67) :args (@t260)) % 1.00/1.28 (step @p434 :rule instantiate :premises (@p66) :args (@t260)) % 1.00/1.28 (step @p435 :rule instantiate :premises (@p65) :args (@t260)) % 1.00/1.28 (step @p436 :rule bool-double-not-elim :args (@t139)) % 1.00/1.28 (step @p437 :rule bool-double-not-elim :args (@t145)) % 1.00/1.28 (step @p438 :rule refl :args (@t308)) % 1.00/1.28 (step @p439 :rule nary_cong :premises (@p438 @p437 @p436) :args ((or @t308 (not @t146) (not @t140)))) % 1.00/1.28 (step @p440 :rule cnf_and_neg :args (@t308)) % 1.00/1.28 (step @p441 :rule eq_resolve :premises (@p440 @p439)) % 1.00/1.28 (step @p442 :rule reordering :premises (@p441) :args ((or @t139 @t145 @t308))) % 1.00/1.28 (step @p443 :rule chain_m_resolution :premises (@p442 @p110 @p113) :args (@t308 @t235 (@list @t139 @t145))) % 1.00/1.28 (step @p444 :rule cnf_equiv_pos2 :args (@t309)) % 1.00/1.28 (step @p445 :rule reordering :premises (@p444) :args ((or @t203 (not @t308) (not @t309)))) % 1.00/1.28 (step @p446 :rule chain_m_resolution :premises (@p445 @p443 @p435) :args (@t203 @t263 (@list @t308 @t309))) % 1.00/1.28 (step @p447 :rule cnf_and_neg :args (@t310)) % 1.00/1.28 (step @p448 :rule reordering :premises (@p447) :args ((or @t307 @t311 @t310))) % 1.00/1.28 (step @p449 :rule chain_m_resolution :premises (@p448 @p89 @p446) :args (@t310 @t263 (@list @t121 @t203))) % 1.00/1.28 (step @p450 :rule cnf_equiv_pos2 :args (@t312)) % 1.00/1.28 (step @p451 :rule reordering :premises (@p450) :args ((or @t201 (not @t310) (not @t312)))) % 1.00/1.28 (step @p452 :rule chain_m_resolution :premises (@p451 @p449 @p434) :args (@t201 @t263 (@list @t310 @t312))) % 1.00/1.28 (step @p453 :rule instantiate :premises (@p58) :args (@t260)) % 1.00/1.28 (step @p454 :rule eq-symm :args (@t86 @t21)) % 1.00/1.28 (step @p455 :rule cong :premises (@p454) :args (@t87)) % 1.00/1.28 (step @p456 :rule eq_resolve :premises (@p57 @p455)) % 1.00/1.28 (step @p457 :rule instantiate :premises (@p456) :args (@t260)) % 1.00/1.28 (step @p458 :rule cnf_equiv_pos1 :args (@t313)) % 1.00/1.28 (step @p459 :rule reordering :premises (@p458) :args ((or @t199 @t307 (not @t313)))) % 1.00/1.28 (step @p460 :rule chain_m_resolution :premises (@p459 @p89 @p457) :args (@t199 @t263 (@list @t121 @t313))) % 1.00/1.28 (step @p461 :rule instantiate :premises (@p55) :args (@t260)) % 1.00/1.28 (step @p462 :rule instantiate :premises (@p54) :args (@t260)) % 1.00/1.28 (step @p463 :rule bool-double-not-elim :args (@t127)) % 1.00/1.28 (step @p464 :rule bool-double-not-elim :args (@t129)) % 1.00/1.28 (step @p465 :rule refl :args (@t314)) % 1.00/1.28 (step @p466 :rule nary_cong :premises (@p465 @p464 @p463) :args ((or @t314 (not @t130) (not @t128)))) % 1.00/1.28 (step @p467 :rule cnf_and_neg :args (@t314)) % 1.00/1.28 (step @p468 :rule eq_resolve :premises (@p467 @p466)) % 1.00/1.28 (step @p469 :rule reordering :premises (@p468) :args ((or @t127 @t129 @t314))) % 1.00/1.28 (step @p470 :rule chain_m_resolution :premises (@p469 @p96 @p97) :args (@t314 @t235 (@list @t127 @t129))) % 1.00/1.28 (step @p471 :rule cnf_equiv_pos2 :args (@t315)) % 1.00/1.28 (step @p472 :rule reordering :premises (@p471) :args ((or @t217 (not @t314) (not @t315)))) % 1.00/1.28 (step @p473 :rule chain_m_resolution :premises (@p472 @p470 @p462) :args (@t217 @t263 (@list @t314 @t315))) % 1.00/1.28 (step @p474 :rule cnf_and_neg :args (@t316)) % 1.00/1.28 (step @p475 :rule reordering :premises (@p474) :args ((or @t307 @t317 @t316))) % 1.00/1.28 (step @p476 :rule chain_m_resolution :premises (@p475 @p89 @p473) :args (@t316 @t263 (@list @t121 @t217))) % 1.00/1.28 (step @p477 :rule cnf_equiv_pos2 :args (@t318)) % 1.00/1.28 (step @p478 :rule reordering :premises (@p477) :args ((or @t209 (not @t316) (not @t318)))) % 1.00/1.28 (step @p479 :rule chain_m_resolution :premises (@p478 @p476 @p461) :args (@t209 @t263 (@list @t316 @t318))) % 1.00/1.28 (step @p480 :rule cnf_and_neg :args (@t319)) % 1.00/1.28 (step @p481 :rule reordering :premises (@p480) :args ((or @t321 @t320 @t319))) % 1.00/1.28 (step @p482 :rule chain_m_resolution :premises (@p481 @p479 @p460) :args (@t319 @t263 (@list @t209 @t199))) % 1.00/1.28 (step @p483 :rule cnf_equiv_pos2 :args (@t322)) % 1.00/1.28 (step @p484 :rule reordering :premises (@p483) :args ((or @t216 (not @t319) (not @t322)))) % 1.00/1.28 (step @p485 :rule chain_m_resolution :premises (@p484 @p482 @p453) :args (@t216 @t263 (@list @t319 @t322))) % 1.00/1.28 (step @p486 :rule cnf_and_neg :args (@t323)) % 1.00/1.28 (step @p487 :rule reordering :premises (@p486) :args ((or @t325 @t324 @t323))) % 1.00/1.28 (step @p488 :rule chain_m_resolution :premises (@p487 @p485 @p452) :args (@t323 @t263 (@list @t216 @t201))) % 1.00/1.28 (step @p489 :rule cnf_equiv_pos2 :args (@t326)) % 1.00/1.28 (step @p490 :rule reordering :premises (@p489) :args ((or @t210 (not @t323) (not @t326)))) % 1.00/1.28 (step @p491 :rule chain_m_resolution :premises (@p490 @p488 @p433) :args (@t210 @t263 (@list @t323 @t326))) % 1.00/1.28 (step @p492 :rule cnf_and_neg :args (@t327)) % 1.00/1.28 (step @p493 :rule reordering :premises (@p492) :args ((or @t329 @t328 @t327))) % 1.00/1.28 (step @p494 :rule chain_m_resolution :premises (@p493 @p491 @p432) :args (@t327 @t263 (@list @t210 @t196))) % 1.00/1.28 (step @p495 :rule cnf_equiv_pos2 :args (@t330)) % 1.00/1.28 (step @p496 :rule reordering :premises (@p495) :args ((or @t188 (not @t327) (not @t330)))) % 1.00/1.28 (step @p497 :rule chain_m_resolution :premises (@p496 @p494 @p425) :args (@t188 @t263 (@list @t327 @t330))) % 1.00/1.28 (step @p498 :rule instantiate :premises (@p78) :args (@t260)) % 1.00/1.28 (step @p499 :rule instantiate :premises (@p76) :args (@t260)) % 1.00/1.28 (step @p500 :rule bool-double-not-elim :args (@t147)) % 1.00/1.28 (step @p501 :rule bool-double-not-elim :args (@t131)) % 1.00/1.28 (step @p502 :rule refl :args (@t331)) % 1.00/1.28 (step @p503 :rule nary_cong :premises (@p502 @p501 @p500) :args ((or @t331 (not @t132) (not @t148)))) % 1.00/1.28 (step @p504 :rule cnf_and_neg :args (@t331)) % 1.00/1.28 (step @p505 :rule eq_resolve :premises (@p504 @p503)) % 1.00/1.28 (step @p506 :rule reordering :premises (@p505) :args ((or @t131 @t147 @t331))) % 1.00/1.28 (step @p507 :rule chain_m_resolution :premises (@p506 @p99 @p114) :args (@t331 @t235 (@list @t131 @t147))) % 1.00/1.28 (step @p508 :rule cnf_equiv_pos2 :args (@t332)) % 1.00/1.28 (step @p509 :rule reordering :premises (@p508) :args ((or @t202 (not @t331) (not @t332)))) % 1.00/1.28 (step @p510 :rule chain_m_resolution :premises (@p509 @p507 @p499) :args (@t202 @t263 (@list @t331 @t332))) % 1.00/1.28 (step @p511 :rule cnf_and_neg :args (@t333)) % 1.00/1.28 (step @p512 :rule reordering :premises (@p511) :args ((or @t307 @t334 @t333))) % 1.00/1.28 (step @p513 :rule chain_m_resolution :premises (@p512 @p89 @p510) :args (@t333 @t263 (@list @t121 @t202))) % 1.00/1.28 (step @p514 :rule cnf_equiv_pos2 :args (@t335)) % 1.00/1.28 (step @p515 :rule reordering :premises (@p514) :args ((or @t194 (not @t333) (not @t335)))) % 1.00/1.28 (step @p516 :rule chain_m_resolution :premises (@p515 @p513 @p498) :args (@t194 @t263 (@list @t333 @t335))) % 1.00/1.28 (step @p517 :rule cnf_and_neg :args (@t336)) % 1.00/1.28 (step @p518 :rule reordering :premises (@p517) :args ((or @t338 @t337 @t336))) % 1.00/1.28 (step @p519 :rule chain_m_resolution :premises (@p518 @p516 @p497) :args (@t336 @t263 (@list @t194 @t188))) % 1.00/1.28 (step @p520 :rule cnf_equiv_pos2 :args (@t339)) % 1.00/1.28 (step @p521 :rule reordering :premises (@p520) :args ((or @t185 (not @t336) (not @t339)))) % 1.00/1.28 (step @p522 :rule chain_m_resolution :premises (@p521 @p519 @p424) :args (@t185 @t263 (@list @t336 @t339))) % 1.00/1.28 (step @p523 :rule instantiate :premises (@p8) :args (@t260)) % 1.00/1.28 (step @p524 :rule cnf_and_neg :args (@t340)) % 1.00/1.28 (step @p525 :rule reordering :premises (@p524) :args ((or @t307 @t341 @t340))) % 1.00/1.28 (step @p526 :rule chain_m_resolution :premises (@p525 @p89 @p392) :args (@t340 @t263 (@list @t121 @t182))) % 1.00/1.28 (step @p527 :rule cnf_equiv_pos2 :args (@t342)) % 1.00/1.28 (step @p528 :rule reordering :premises (@p527) :args ((or @t187 (not @t340) (not @t342)))) % 1.00/1.28 (step @p529 :rule chain_m_resolution :premises (@p528 @p526 @p523) :args (@t187 @t263 (@list @t340 @t342))) % 1.00/1.28 (step @p530 :rule eq-symm :args (@t25 @t21)) % 1.00/1.28 (step @p531 :rule cong :premises (@p530) :args (@t26)) % 1.00/1.28 (step @p532 :rule eq_resolve :premises (@p10 @p531)) % 1.00/1.28 (step @p533 :rule instantiate :premises (@p532) :args (@t260)) % 1.00/1.28 (step @p534 :rule cnf_equiv_pos1 :args (@t343)) % 1.00/1.28 (step @p535 :rule reordering :premises (@p534) :args ((or @t189 @t307 (not @t343)))) % 1.00/1.28 (step @p536 :rule chain_m_resolution :premises (@p535 @p89 @p533) :args (@t189 @t263 (@list @t121 @t343))) % 1.00/1.28 (step @p537 :rule cnf_and_pos :args (@t261 1)) % 1.00/1.28 (step @p538 :rule reordering :premises (@p537) :args ((or @t190 @t264))) % 1.00/1.28 (step @p539 :rule chain_m_resolution :premises (@p538 @p330) :args (@t190 @t265 @t266)) % 1.00/1.28 (step @p540 :rule instantiate :premises (@p3) :args (@t260)) % 1.00/1.28 (step @p541 :rule cnf_and_pos :args (@t289 1)) % 1.00/1.28 (step @p542 :rule reordering :premises (@p541) :args ((or @t207 @t292))) % 1.00/1.28 (step @p543 :rule chain_m_resolution :premises (@p542 @p377) :args (@t207 @t265 @t293)) % 1.00/1.28 (step @p544 :rule cnf_equiv_pos1 :args (@t345)) % 1.00/1.28 (step @p545 :rule reordering :premises (@p544) :args ((or @t346 @t344 (not @t345)))) % 1.00/1.28 (step @p546 :rule chain_m_resolution :premises (@p545 @p543 @p540) :args (@t344 @t263 (@list @t207 @t345))) % 1.00/1.28 (step @p547 :rule cnf_and_pos :args (@t344 0)) % 1.00/1.28 (step @p548 :rule reordering :premises (@p547) :args ((or @t193 (not @t344)))) % 1.00/1.28 (step @p549 :rule chain_m_resolution :premises (@p548 @p546) :args (@t193 @t265 (@list @t344))) % 1.00/1.28 (step @p550 :rule eq-symm :args (@t40 @t21)) % 1.00/1.28 (step @p551 :rule cong :premises (@p550) :args (@t41)) % 1.00/1.28 (step @p552 :rule eq_resolve :premises (@p21 @p551)) % 1.00/1.28 (step @p553 :rule instantiate :premises (@p552) :args (@t260)) % 1.00/1.28 (step @p554 :rule cnf_equiv_pos1 :args (@t347)) % 1.00/1.28 (step @p555 :rule reordering :premises (@p554) :args ((or @t192 @t307 (not @t347)))) % 1.00/1.28 (step @p556 :rule chain_m_resolution :premises (@p555 @p89 @p553) :args (@t192 @t263 (@list @t121 @t347))) % 1.00/1.28 (step @p557 :rule instantiate :premises (@p31) :args (@t260)) % 1.00/1.28 (step @p558 :rule instantiate :premises (@p30) :args (@t260)) % 1.00/1.28 (step @p559 :rule bool-double-not-elim :args (@t143)) % 1.00/1.28 (step @p560 :rule bool-double-not-elim :args (@t137)) % 1.00/1.28 (step @p561 :rule refl :args (@t348)) % 1.00/1.28 (step @p562 :rule nary_cong :premises (@p561 @p560 @p559) :args ((or @t348 (not @t138) (not @t144)))) % 1.00/1.28 (step @p563 :rule cnf_and_neg :args (@t348)) % 1.00/1.28 (step @p564 :rule eq_resolve :premises (@p563 @p562)) % 1.00/1.28 (step @p565 :rule reordering :premises (@p564) :args ((or @t137 @t143 @t348))) % 1.00/1.28 (step @p566 :rule chain_m_resolution :premises (@p565 @p109 @p112) :args (@t348 @t235 (@list @t137 @t143))) % 1.00/1.28 (step @p567 :rule cnf_equiv_pos2 :args (@t349)) % 1.00/1.28 (step @p568 :rule reordering :premises (@p567) :args ((or @t200 (not @t348) (not @t349)))) % 1.00/1.28 (step @p569 :rule chain_m_resolution :premises (@p568 @p566 @p558) :args (@t200 @t263 (@list @t348 @t349))) % 1.00/1.28 (step @p570 :rule cnf_and_neg :args (@t350)) % 1.00/1.28 (step @p571 :rule reordering :premises (@p570) :args ((or @t307 @t351 @t350))) % 1.00/1.28 (step @p572 :rule chain_m_resolution :premises (@p571 @p89 @p569) :args (@t350 @t263 (@list @t121 @t200))) % 1.00/1.28 (step @p573 :rule cnf_equiv_pos2 :args (@t352)) % 1.00/1.28 (step @p574 :rule reordering :premises (@p573) :args ((or @t195 (not @t350) (not @t352)))) % 1.00/1.28 (step @p575 :rule chain_m_resolution :premises (@p574 @p572 @p557) :args (@t195 @t263 (@list @t350 @t352))) % 1.00/1.28 (step @p576 :rule instantiate :premises (@p18) :args (@t260)) % 1.00/1.28 (step @p577 :rule bool-double-not-elim :args (@t149)) % 1.00/1.28 (step @p578 :rule bool-double-not-elim :args (@t125)) % 1.00/1.28 (step @p579 :rule refl :args (@t353)) % 1.00/1.28 (step @p580 :rule nary_cong :premises (@p579 @p578 @p577) :args ((or @t353 (not @t126) (not @t150)))) % 1.00/1.28 (step @p581 :rule cnf_and_neg :args (@t353)) % 1.00/1.28 (step @p582 :rule eq_resolve :premises (@p581 @p580)) % 1.00/1.28 (step @p583 :rule reordering :premises (@p582) :args ((or @t125 @t149 @t353))) % 1.00/1.28 (step @p584 :rule chain_m_resolution :premises (@p583 @p93 @p116) :args (@t353 @t235 (@list @t125 @t149))) % 1.00/1.28 (step @p585 :rule cnf_equiv_pos2 :args (@t354)) % 1.00/1.28 (step @p586 :rule reordering :premises (@p585) :args ((or @t197 (not @t353) (not @t354)))) % 1.00/1.28 (step @p587 :rule chain_m_resolution :premises (@p586 @p584 @p576) :args (@t197 @t263 (@list @t353 @t354))) % 1.00/1.28 (step @p588 :rule instantiate :premises (@p19) :args (@t260)) % 1.00/1.28 (step @p589 :rule cnf_and_neg :args (@t355)) % 1.00/1.28 (step @p590 :rule reordering :premises (@p589) :args ((or @t307 @t356 @t355))) % 1.00/1.28 (step @p591 :rule chain_m_resolution :premises (@p590 @p89 @p587) :args (@t355 @t263 (@list @t121 @t197))) % 1.00/1.28 (step @p592 :rule cnf_equiv_pos2 :args (@t357)) % 1.00/1.28 (step @p593 :rule reordering :premises (@p592) :args ((or @t198 (not @t355) (not @t357)))) % 1.00/1.28 (step @p594 :rule chain_m_resolution :premises (@p593 @p591 @p588) :args (@t198 @t263 (@list @t355 @t357))) % 1.00/1.28 (step @p595 :rule instantiate :premises (@p39) :args (@t260)) % 1.00/1.28 (step @p596 :rule bool-double-not-elim :args (@t133)) % 1.00/1.28 (step @p597 :rule bool-double-not-elim :args (@t135)) % 1.00/1.28 (step @p598 :rule refl :args (@t358)) % 1.00/1.28 (step @p599 :rule nary_cong :premises (@p598 @p597 @p596) :args ((or @t358 (not @t136) (not @t134)))) % 1.00/1.28 (step @p600 :rule cnf_and_neg :args (@t358)) % 1.00/1.28 (step @p601 :rule eq_resolve :premises (@p600 @p599)) % 1.00/1.28 (step @p602 :rule reordering :premises (@p601) :args ((or @t133 @t135 @t358))) % 1.00/1.28 (step @p603 :rule chain_m_resolution :premises (@p602 @p101 @p102) :args (@t358 @t235 (@list @t133 @t135))) % 1.00/1.28 (step @p604 :rule cnf_equiv_pos2 :args (@t359)) % 1.00/1.28 (step @p605 :rule reordering :premises (@p604) :args ((or @t204 (not @t358) (not @t359)))) % 1.00/1.28 (step @p606 :rule chain_m_resolution :premises (@p605 @p603 @p595) :args (@t204 @t263 (@list @t358 @t359))) % 1.00/1.28 (step @p607 :rule cnf_and_pos :args (@t284 1)) % 1.00/1.28 (step @p608 :rule reordering :premises (@p607) :args ((or @t212 @t287))) % 1.00/1.28 (step @p609 :rule chain_m_resolution :premises (@p608 @p371) :args (@t212 @t265 @t288)) % 1.00/1.28 (step @p610 :rule instantiate :premises (@p42) :args (@t260)) % 1.00/1.28 (step @p611 :rule bool-double-not-elim :args (@t151)) % 1.00/1.28 (step @p612 :rule refl :args (@t360)) % 1.00/1.28 (step @p613 :rule refl :args (@t361)) % 1.00/1.28 (step @p614 :rule nary_cong :premises (@p613 @p612 @p611) :args ((or @t361 @t360 (not @t152)))) % 1.00/1.28 (step @p615 :rule cnf_and_neg :args (@t361)) % 1.00/1.28 (step @p616 :rule eq_resolve :premises (@p615 @p614)) % 1.00/1.28 (step @p617 :rule reordering :premises (@p616) :args ((or @t151 @t360 @t361))) % 1.00/1.28 (step @p618 :rule chain_m_resolution :premises (@p617 @p117 @p606) :args (@t361 @t233 (@list @t151 @t204))) % 1.00/1.28 (step @p619 :rule cnf_equiv_pos2 :args (@t362)) % 1.00/1.28 (step @p620 :rule reordering :premises (@p619) :args ((or @t213 (not @t361) (not @t362)))) % 1.00/1.28 (step @p621 :rule chain_m_resolution :premises (@p620 @p618 @p610) :args (@t213 @t263 (@list @t361 @t362))) % 1.00/1.28 (step @p622 :rule eq-symm :args (@t116 @t21)) % 1.00/1.28 (step @p623 :rule cong :premises (@p622) :args (@t117)) % 1.00/1.28 (step @p624 :rule eq_resolve :premises (@p82 @p623)) % 1.00/1.28 (step @p625 :rule instantiate :premises (@p624) :args (@t260)) % 1.00/1.28 (step @p626 :rule cnf_equiv_pos1 :args (@t363)) % 1.00/1.28 (step @p627 :rule reordering :premises (@p626) :args ((or @t215 @t307 (not @t363)))) % 1.00/1.28 (step @p628 :rule chain_m_resolution :premises (@p627 @p89 @p625) :args (@t215 @t263 (@list @t121 @t363))) % 1.00/1.28 (step @p629 :rule eq-symm :args (@t113 @t21)) % 1.00/1.28 (step @p630 :rule cong :premises (@p629) :args (@t114)) % 1.00/1.28 (step @p631 :rule eq_resolve :premises (@p80 @p630)) % 1.00/1.28 (step @p632 :rule instantiate :premises (@p631) :args (@t260)) % 1.00/1.28 (step @p633 :rule cnf_equiv_pos1 :args (@t364)) % 1.00/1.28 (step @p634 :rule reordering :premises (@p633) :args ((or @t219 @t307 (not @t364)))) % 1.00/1.28 (step @p635 :rule chain_m_resolution :premises (@p634 @p89 @p632) :args (@t219 @t263 (@list @t121 @t364))) % 1.00/1.28 (step @p636 :rule instantiate :premises (@p81) :args (@t260)) % 1.00/1.28 (step @p637 :rule cnf_and_neg :args (@t365)) % 1.00/1.28 (step @p638 :rule reordering :premises (@p637) :args ((or @t367 @t366 @t365))) % 1.00/1.28 (step @p639 :rule chain_m_resolution :premises (@p638 @p635 @p522) :args (@t365 @t263 (@list @t219 @t185))) % 1.00/1.28 (step @p640 :rule cnf_equiv_pos2 :args (@t368)) % 1.00/1.28 (step @p641 :rule reordering :premises (@p640) :args ((or @t214 (not @t365) (not @t368)))) % 1.00/1.28 (step @p642 :rule chain_m_resolution :premises (@p641 @p639 @p636) :args (@t214 @t263 (@list @t365 @t368))) % 1.00/1.28 (step @p643 :rule instantiate :premises (@p9) :args (@t260)) % 1.00/1.28 (step @p644 :rule cnf_equiv_pos1 :args (@t370)) % 1.00/1.28 (step @p645 :rule reordering :premises (@p644) :args ((or @t371 @t369 (not @t370)))) % 1.00/1.28 (step @p646 :rule chain_m_resolution :premises (@p645 @p363 @p643) :args (@t369 @t263 (@list @t191 @t370))) % 1.00/1.28 (step @p647 :rule cnf_and_pos :args (@t369 0)) % 1.00/1.28 (step @p648 :rule reordering :premises (@p647) :args ((or @t180 (not @t369)))) % 1.00/1.28 (step @p649 :rule chain_m_resolution :premises (@p648 @p646) :args (@t180 @t265 (@list @t369))) % 1.00/1.28 (step @p650 :rule aci_norm :args ((= (and (and @t373 @t372) @t6 @t153 @t219 @t218 @t217 @t216 @t215 @t214 @t213 @t212 @t211 @t210 @t209 @t208 @t207 @t206 @t205 @t204 @t203 @t202 @t201 @t200 @t199 @t198 @t197 @t196 @t195 @t194 @t193 @t192 @t191 @t190 @t189 @t188 @t187 @t186 @t185 @t184 @t183 @t182 @t181 @t180 @t161 @t179 @t178 @t167 @t177 @t176 @t173 @t175 @t174) (and @t6 @t153 @t219 @t218 @t217 @t216 @t215 @t214 @t213 @t212 @t211 @t210 @t209 @t208 @t207 @t206 @t205 @t204 @t203 @t202 @t201 @t200 @t199 @t198 @t197 @t196 @t195 @t194 @t193 @t192 @t191 @t190 @t189 @t188 @t187 @t186 @t185 @t184 @t183 @t182 @t181 @t180 @t161 @t179 @t178 @t167 @t177 @t176 @t173 @t175 @t174 @t373 @t372)))) % 1.00/1.28 (step @p651 :rule refl :args (@t174)) % 1.00/1.28 (step @p652 :rule refl :args (@t175)) % 1.00/1.28 (step @p653 :rule refl :args (@t173)) % 1.00/1.28 (step @p654 :rule refl :args (@t176)) % 1.00/1.28 (step @p655 :rule refl :args (@t177)) % 1.00/1.28 (step @p656 :rule refl :args (@t167)) % 1.00/1.28 (step @p657 :rule refl :args (@t178)) % 1.00/1.28 (step @p658 :rule refl :args (@t179)) % 1.00/1.28 (step @p659 :rule refl :args (@t161)) % 1.00/1.28 (step @p660 :rule refl :args (@t180)) % 1.00/1.28 (step @p661 :rule refl :args (@t181)) % 1.00/1.28 (step @p662 :rule refl :args (@t182)) % 1.00/1.28 (step @p663 :rule refl :args (@t184)) % 1.00/1.28 (step @p664 :rule refl :args (@t185)) % 1.00/1.28 (step @p665 :rule refl :args (@t186)) % 1.00/1.28 (step @p666 :rule refl :args (@t187)) % 1.00/1.28 (step @p667 :rule refl :args (@t188)) % 1.00/1.28 (step @p668 :rule refl :args (@t189)) % 1.00/1.28 (step @p669 :rule refl :args (@t190)) % 1.00/1.28 (step @p670 :rule refl :args (@t191)) % 1.00/1.28 (step @p671 :rule refl :args (@t192)) % 1.00/1.28 (step @p672 :rule refl :args (@t193)) % 1.00/1.28 (step @p673 :rule refl :args (@t194)) % 1.00/1.28 (step @p674 :rule refl :args (@t195)) % 1.00/1.28 (step @p675 :rule refl :args (@t196)) % 1.00/1.28 (step @p676 :rule refl :args (@t197)) % 1.00/1.28 (step @p677 :rule refl :args (@t198)) % 1.00/1.28 (step @p678 :rule refl :args (@t199)) % 1.00/1.28 (step @p679 :rule refl :args (@t200)) % 1.00/1.28 (step @p680 :rule refl :args (@t201)) % 1.00/1.28 (step @p681 :rule refl :args (@t202)) % 1.00/1.28 (step @p682 :rule refl :args (@t203)) % 1.00/1.28 (step @p683 :rule refl :args (@t204)) % 1.00/1.28 (step @p684 :rule refl :args (@t205)) % 1.00/1.28 (step @p685 :rule refl :args (@t206)) % 1.00/1.28 (step @p686 :rule refl :args (@t207)) % 1.00/1.28 (step @p687 :rule refl :args (@t208)) % 1.00/1.28 (step @p688 :rule refl :args (@t209)) % 1.00/1.28 (step @p689 :rule refl :args (@t210)) % 1.00/1.28 (step @p690 :rule refl :args (@t211)) % 1.00/1.28 (step @p691 :rule refl :args (@t212)) % 1.00/1.28 (step @p692 :rule refl :args (@t213)) % 1.00/1.28 (step @p693 :rule refl :args (@t214)) % 1.00/1.28 (step @p694 :rule refl :args (@t215)) % 1.00/1.28 (step @p695 :rule refl :args (@t216)) % 1.00/1.28 (step @p696 :rule refl :args (@t217)) % 1.00/1.28 (step @p697 :rule refl :args (@t218)) % 1.00/1.28 (step @p698 :rule refl :args (@t219)) % 1.00/1.28 (step @p699 :rule refl :args (@t153)) % 1.00/1.28 (step @p700 :rule refl :args (@t6)) % 1.00/1.28 (step @p701 :rule nary_cong :premises (@p249 @p700 @p699 @p698 @p697 @p696 @p695 @p694 @p693 @p692 @p691 @p690 @p689 @p688 @p687 @p686 @p685 @p684 @p683 @p682 @p681 @p680 @p679 @p678 @p677 @p676 @p675 @p674 @p673 @p672 @p671 @p670 @p669 @p668 @p667 @p666 @p665 @p664 @p663 @p417 @p662 @p661 @p660 @p659 @p658 @p657 @p656 @p655 @p654 @p653 @p652 @p651) :args (@t220)) % 1.00/1.28 (step @p702 :rule trans :premises (@p701 @p650)) % 1.00/1.28 (step @p703 :rule cong :premises (@p702) :args (@t221)) % 1.00/1.28 (step @p704 :rule eq_resolve :premises (@p243 @p703)) % 1.00/1.28 (step @p705 :rule not_and :premises (@p704)) % 1.00/1.28 (step @p706 :rule reordering :premises (@p705) :args ((or (not @t373) (not @t372) (not @t6) (not @t153) (not @t161) (not @t167) (not @t173) @t367 @t291 @t317 @t325 (not @t215) (not @t214) (not @t213) (not @t212) @t274 @t329 @t321 @t269 @t346 @t280 @t286 @t360 @t311 @t334 @t324 @t351 @t320 (not @t198) @t356 @t328 (not @t195) @t338 (not @t193) (not @t192) @t371 (not @t190) (not @t189) @t337 (not @t187) @t283 @t366 @t277 (not @t183) @t341 (not @t181) (not @t180) @t256 @t251 @t246 @t241 @t236 @t229))) % 1.00/1.28 (step @p707 false :rule chain_m_resolution :premises (@p706 @p649 @p642 @p473 @p635 @p628 @p485 @p621 @p609 @p339 @p374 @p479 @p333 @p543 @p351 @p368 @p606 @p446 @p510 @p452 @p569 @p460 @p594 @p587 @p432 @p575 @p516 @p491 @p556 @p549 @p539 @p536 @p497 @p529 @p357 @p522 @p345 @p423 @p392 @p380 @p363 @p321 @p310 @p298 @p287 @p275 @p264 @p208 @p181 @p152 @p121 @p2 @p252 @p251) :args (false (@list false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false) (@list @t180 @t214 @t217 @t219 @t215 @t216 @t213 @t212 @t211 @t218 @t209 @t208 @t207 @t206 @t205 @t204 @t203 @t202 @t201 @t200 @t199 @t198 @t197 @t196 @t195 @t194 @t210 @t192 @t193 @t190 @t189 @t188 @t187 @t186 @t185 @t184 @t183 @t182 @t181 @t191 @t179 @t178 @t177 @t176 @t175 @t174 @t173 @t167 @t161 @t153 @t6 @t372 @t373))) % 1.00/1.28 ) % 1.00/1.28 % SZS output end Proof % 1.00/1.28 % cvc5 exiting %------------------------------------------------------------------------------