cvc5---1.3.4.UNS-Prf.s

%------------------------------------------------------------------------------
% File     : cvc5---1.3.4
% Problem  : LAT009-1 : TPTP v9.2.1. Released v2.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n023.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:36 AM UTC 2026

% Result   : Unsatisfiable 1.51s 1.73s
% Output   : Proof 1.51s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : LAT009-1 : TPTP v9.2.1. Released v2.2.0.
% 0.13/0.13  % Command  : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.17/0.34  % Computer : n023.cluster.edu
% 0.17/0.34  % Model    : x86_64 x86_64
% 0.17/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34  % Memory   : 8042.1875MB
% 0.17/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34  % CPULimit : 300
% 0.17/0.34  % WCLimit  : 300
% 0.17/0.34  % DateTime : Tue Jun  2 05:44:28 EDT 2026
% 0.17/0.34  % CPUTime  : 
% 0.31/0.49  %----Proving TF0_NAR, FOF, or CNF
% 0.31/0.50  --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15...
% 1.51/1.73  % SZS status Unsatisfiable
% 1.51/1.73  % SZS output start Proof
% 1.51/1.76  (
% 1.51/1.76  (declare-sort $$unsorted 0)
% 1.51/1.76  (declare-const tptp.b $$unsorted)
% 1.51/1.76  (declare-const tptp.a $$unsorted)
% 1.51/1.76  (declare-const tptp.c $$unsorted)
% 1.51/1.76  (declare-const tptp.join (-> $$unsorted $$unsorted $$unsorted))
% 1.51/1.76  (declare-const tptp.meet (-> $$unsorted $$unsorted $$unsorted))
% 1.51/1.76  (define @t1 () (@var "X" $$unsorted))
% 1.51/1.76  (define @t2 () (tptp.meet @t1 @t1))
% 1.51/1.76  (define @t3 () (@list @t1))
% 1.51/1.76  (define @t4 () (forall @t3 (= @t2 @t1)))
% 1.51/1.76  (define @t5 () (tptp.join @t1 @t1))
% 1.51/1.76  (define @t6 () (forall @t3 (= @t5 @t1)))
% 1.51/1.76  (define @t7 () (@var "Y" $$unsorted))
% 1.51/1.76  (define @t8 () (tptp.join @t1 @t7))
% 1.51/1.76  (define @t9 () (tptp.meet @t1 @t8))
% 1.51/1.76  (define @t10 () (@list @t1 @t7))
% 1.51/1.76  (define @t11 () (forall @t10 (= @t9 @t1)))
% 1.51/1.76  (define @t12 () (tptp.meet @t1 @t7))
% 1.51/1.76  (define @t13 () (tptp.join @t1 @t12))
% 1.51/1.76  (define @t14 () (forall @t10 (= @t13 @t1)))
% 1.51/1.76  (define @t15 () (forall @t10 (= @t12 (tptp.meet @t7 @t1))))
% 1.51/1.76  (define @t16 () (forall @t10 (= @t8 (tptp.join @t7 @t1))))
% 1.51/1.76  (define @t17 () (@var "Z" $$unsorted))
% 1.51/1.76  (define @t18 () (@list @t1 @t7 @t17))
% 1.51/1.76  (define @t19 () (forall @t18 (= (tptp.meet @t12 @t17) (tptp.meet @t1 (tptp.meet @t7 @t17)))))
% 1.51/1.76  (define @t20 () (forall @t18 (= (tptp.join @t8 @t17) (tptp.join @t1 (tptp.join @t7 @t17)))))
% 1.51/1.76  (define @t21 () (tptp.join tptp.a tptp.c))
% 1.51/1.76  (define @t22 () (tptp.join tptp.a tptp.b))
% 1.51/1.76  (define @t23 () (tptp.meet @t22 @t21))
% 1.51/1.76  (define @t24 () (tptp.meet tptp.b tptp.c))
% 1.51/1.76  (define @t25 () (tptp.join tptp.a @t24))
% 1.51/1.76  (define @t26 () (= @t25 @t23))
% 1.51/1.76  (define @t27 () (@list tptp.a tptp.b))
% 1.51/1.76  (define @t28 () (@list tptp.a tptp.c))
% 1.51/1.76  (define @t29 () (@list tptp.a @t24))
% 1.51/1.76  (define @t30 () (@list tptp.b tptp.c))
% 1.51/1.76  (define @t31 () (@list @t22 @t21))
% 1.51/1.76  (define @t32 () (@list tptp.b tptp.a))
% 1.51/1.76  (define @t33 () (@list tptp.b @t24))
% 1.51/1.76  (define @t34 () (@list tptp.c tptp.a))
% 1.51/1.76  (define @t35 () (@list @t24 tptp.a))
% 1.51/1.76  (define @t36 () (@list @t22 @t23))
% 1.51/1.76  (define @t37 () (@list tptp.a @t25))
% 1.51/1.76  (define @t38 () (@list tptp.c tptp.b))
% 1.51/1.76  (define @t39 () (@list tptp.a @t22))
% 1.51/1.76  (define @t40 () (@list tptp.a @t21))
% 1.51/1.76  (define @t41 () (tptp.meet tptp.a @t25))
% 1.51/1.76  (define @t42 () (tptp.meet tptp.c tptp.b))
% 1.51/1.76  (define @t43 () (@list tptp.c @t42))
% 1.51/1.76  (define @t44 () (tptp.meet @t21 @t22))
% 1.51/1.76  (define @t45 () (@list @t21 @t44))
% 1.51/1.76  (define @t46 () (tptp.join tptp.a @t21))
% 1.51/1.76  (define @t47 () (tptp.meet @t46 tptp.b))
% 1.51/1.76  (define @t48 () (@list @t47 @t21))
% 1.51/1.76  (define @t49 () (tptp.join tptp.b @t24))
% 1.51/1.76  (define @t50 () (tptp.join tptp.c tptp.a))
% 1.51/1.76  (define @t51 () (@list tptp.c @t50))
% 1.51/1.76  (define @t52 () (tptp.join @t22 @t23))
% 1.51/1.76  (define @t53 () (@list @t46 tptp.b))
% 1.51/1.76  (define @t54 () (tptp.join tptp.a @t22))
% 1.51/1.76  (define @t55 () (@list @t54 tptp.c))
% 1.51/1.76  (define @t56 () (tptp.meet @t25 @t21))
% 1.51/1.76  (define @t57 () (@list tptp.a @t56))
% 1.51/1.76  (define @t58 () (tptp.join tptp.b tptp.a))
% 1.51/1.76  (define @t59 () (@list tptp.b @t58))
% 1.51/1.76  (define @t60 () (tptp.join @t24 tptp.a))
% 1.51/1.76  (define @t61 () (tptp.meet @t54 tptp.c))
% 1.51/1.76  (define @t62 () (tptp.join @t61 @t22))
% 1.51/1.76  (define @t63 () (tptp.join tptp.b @t23))
% 1.51/1.76  (define @t64 () (tptp.meet tptp.c tptp.a))
% 1.51/1.76  (define @t65 () (tptp.meet tptp.a @t22))
% 1.51/1.76  (define @t66 () (tptp.join @t65 tptp.c))
% 1.51/1.76  (define @t67 () (tptp.meet @t66 @t22))
% 1.51/1.76  (define @t68 () (tptp.meet @t25 @t25))
% 1.51/1.76  (define @t69 () (tptp.join @t23 tptp.a))
% 1.51/1.76  (define @t70 () (tptp.join @t69 tptp.b))
% 1.51/1.76  (define @t71 () (tptp.join @t23 @t22))
% 1.51/1.76  (define @t72 () (= @t70 @t71))
% 1.51/1.76  (define @t73 () (@list @t23 tptp.a tptp.b))
% 1.51/1.76  (define @t74 () (= @t71 @t70))
% 1.51/1.76  (define @t75 () (@list false))
% 1.51/1.76  (define @t76 () (@list @t20))
% 1.51/1.76  (define @t77 () (tptp.join @t47 tptp.a))
% 1.51/1.76  (define @t78 () (tptp.join @t77 tptp.c))
% 1.51/1.76  (define @t79 () (tptp.join @t47 @t21))
% 1.51/1.76  (define @t80 () (= @t78 @t79))
% 1.51/1.76  (define @t81 () (@list @t47 tptp.a tptp.c))
% 1.51/1.76  (define @t82 () (= @t79 @t78))
% 1.51/1.76  (define @t83 () (tptp.join @t61 tptp.a))
% 1.51/1.76  (define @t84 () (tptp.join @t83 tptp.b))
% 1.51/1.76  (define @t85 () (= @t84 @t62))
% 1.51/1.76  (define @t86 () (@list @t61 tptp.a tptp.b))
% 1.51/1.76  (define @t87 () (= @t62 @t84))
% 1.51/1.76  (define @t88 () (tptp.join @t24 @t24))
% 1.51/1.76  (define @t89 () (@list @t60 tptp.b))
% 1.51/1.76  (define @t90 () (@list @t77 tptp.c))
% 1.51/1.76  (define @t91 () (tptp.meet @t24 tptp.a))
% 1.51/1.76  (define @t92 () (tptp.meet tptp.a @t21))
% 1.51/1.76  (define @t93 () (tptp.join @t92 @t24))
% 1.51/1.76  (define @t94 () (tptp.meet @t93 @t21))
% 1.51/1.76  (define @t95 () (tptp.meet tptp.c @t42))
% 1.51/1.76  (define @t96 () (tptp.meet tptp.a tptp.a))
% 1.51/1.76  (define @t97 () (tptp.meet tptp.a @t63))
% 1.51/1.76  (define @t98 () (tptp.join @t97 tptp.a))
% 1.51/1.76  (define @t99 () (tptp.meet @t98 @t63))
% 1.51/1.76  (define @t100 () (tptp.meet @t52 @t22))
% 1.51/1.76  (define @t101 () (tptp.meet @t22 @t24))
% 1.51/1.76  (define @t102 () (tptp.join @t101 @t52))
% 1.51/1.76  (define @t103 () (tptp.meet @t102 @t24))
% 1.51/1.76  (define @t104 () (tptp.join @t21 @t44))
% 1.51/1.76  (define @t105 () (tptp.join tptp.b tptp.c))
% 1.51/1.76  (define @t106 () (@list @t105 tptp.b))
% 1.51/1.76  (define @t107 () (tptp.join @t41 tptp.a))
% 1.51/1.76  (define @t108 () (tptp.join tptp.a @t56))
% 1.51/1.76  (define @t109 () (tptp.meet @t108 @t41))
% 1.51/1.76  (define @t110 () (tptp.join @t109 @t56))
% 1.51/1.76  (define @t111 () (tptp.join @t95 @t50))
% 1.51/1.76  (define @t112 () (@list @t111 @t42))
% 1.51/1.76  (define @t113 () (tptp.meet tptp.a @t23))
% 1.51/1.76  (define @t114 () (tptp.meet @t23 tptp.a))
% 1.51/1.76  (define @t115 () (= @t113 @t114))
% 1.51/1.76  (define @t116 () (@list tptp.a @t23))
% 1.51/1.76  (define @t117 () (= @t114 @t113))
% 1.51/1.76  (define @t118 () (@list @t15))
% 1.51/1.76  (define @t119 () (tptp.meet @t42 tptp.c))
% 1.51/1.76  (define @t120 () (= @t95 @t119))
% 1.51/1.76  (define @t121 () (= @t119 @t95))
% 1.51/1.76  (define @t122 () (tptp.meet tptp.b tptp.a))
% 1.51/1.76  (define @t123 () (tptp.join tptp.b @t58))
% 1.51/1.76  (define @t124 () (tptp.join (tptp.meet (tptp.join tptp.a @t52) tptp.b) @t52))
% 1.51/1.76  (define @t125 () (tptp.join @t24 @t21))
% 1.51/1.76  (define @t126 () (tptp.join @t21 tptp.a))
% 1.51/1.76  (define @t127 () (tptp.meet @t126 @t24))
% 1.51/1.76  (define @t128 () (tptp.join @t127 tptp.a))
% 1.51/1.76  (define @t129 () (tptp.join tptp.a @t23))
% 1.51/1.76  (define @t130 () (= @t129 @t69))
% 1.51/1.76  (define @t131 () (= @t69 @t129))
% 1.51/1.76  (define @t132 () (tptp.meet tptp.b @t21))
% 1.51/1.76  (define @t133 () (tptp.meet @t21 tptp.a))
% 1.51/1.76  (define @t134 () (tptp.join @t133 tptp.b))
% 1.51/1.76  (define @t135 () (tptp.meet @t134 tptp.a))
% 1.51/1.76  (define @t136 () (tptp.meet (tptp.join (tptp.meet tptp.a @t52) tptp.b) @t52))
% 1.51/1.76  (define @t137 () (tptp.join @t24 tptp.b))
% 1.51/1.76  (define @t138 () (tptp.join @t88 tptp.b))
% 1.51/1.76  (define @t139 () (tptp.meet @t123 @t88))
% 1.51/1.76  (define @t140 () (tptp.join @t139 @t58))
% 1.51/1.76  (define @t141 () (tptp.join (tptp.join @t44 tptp.a) tptp.c))
% 1.51/1.76  (define @t142 () (tptp.join @t44 @t21))
% 1.51/1.76  (define @t143 () (= @t141 @t142))
% 1.51/1.76  (define @t144 () (@list @t44 tptp.a tptp.c))
% 1.51/1.76  (define @t145 () (= @t142 @t141))
% 1.51/1.76  (define @t146 () (tptp.meet tptp.c @t50))
% 1.51/1.76  (define @t147 () (tptp.meet @t50 tptp.b))
% 1.51/1.76  (define @t148 () (tptp.meet tptp.c @t60))
% 1.51/1.76  (define @t149 () (@list tptp.c @t47))
% 1.51/1.76  (define @t150 () (tptp.meet @t47 @t50))
% 1.51/1.76  (define @t151 () (tptp.meet @t46 @t132))
% 1.51/1.76  (define @t152 () (tptp.join @t151 tptp.a))
% 1.51/1.76  (define @t153 () (tptp.join tptp.c @t147))
% 1.51/1.76  (define @t154 () (@list @t153 tptp.c))
% 1.51/1.76  (define @t155 () (tptp.join tptp.c tptp.c))
% 1.51/1.76  (define @t156 () (tptp.meet @t153 tptp.c))
% 1.51/1.76  (define @t157 () (tptp.join @t156 @t147))
% 1.51/1.76  (define @t158 () (tptp.join tptp.c tptp.b))
% 1.51/1.76  (define @t159 () (@list @t47 @t77))
% 1.51/1.76  (define @t160 () (tptp.join tptp.b @t148))
% 1.51/1.76  (define @t161 () (tptp.join @t119 @t147))
% 1.51/1.76  (define @t162 () (tptp.meet tptp.b @t46))
% 1.51/1.76  (define @t163 () (tptp.join @t41 tptp.b))
% 1.51/1.76  (define @t164 () (tptp.meet @t163 @t25))
% 1.51/1.76  (define @t165 () (tptp.join tptp.a @t25))
% 1.51/1.76  (define @t166 () (tptp.meet @t165 tptp.c))
% 1.51/1.76  (define @t167 () (tptp.meet @t77 tptp.c))
% 1.51/1.76  (define @t168 () (tptp.meet tptp.a @t83))
% 1.51/1.76  (define @t169 () (tptp.meet (tptp.join (tptp.meet @t83 tptp.b) tptp.a) tptp.b))
% 1.51/1.76  (define @t170 () (tptp.join @t24 @t47))
% 1.51/1.76  (define @t171 () (tptp.join (tptp.meet @t79 @t24) @t21))
% 1.51/1.76  (define @t172 () (tptp.join tptp.b tptp.b))
% 1.51/1.76  (define @t173 () (tptp.meet @t160 tptp.b))
% 1.51/1.76  (define @t174 () (tptp.join @t173 @t148))
% 1.51/1.76  (define @t175 () (tptp.meet tptp.a @t46))
% 1.51/1.76  (define @t176 () (tptp.meet @t175 tptp.b))
% 1.51/1.76  (define @t177 () (tptp.meet tptp.a @t47))
% 1.51/1.76  (define @t178 () (= @t176 @t177))
% 1.51/1.76  (define @t179 () (@list tptp.a @t46 tptp.b))
% 1.51/1.76  (define @t180 () (= @t177 @t176))
% 1.51/1.76  (define @t181 () (tptp.meet @t152 @t132))
% 1.51/1.76  (define @t182 () (tptp.meet @t24 tptp.c))
% 1.51/1.76  (define @t183 () (tptp.meet (tptp.join @t64 @t24) tptp.a))
% 1.51/1.76  (define @t184 () (tptp.meet tptp.c @t110))
% 1.51/1.76  (define @t185 () (tptp.meet @t50 @t137))
% 1.51/1.76  (define @t186 () (tptp.join @t64 @t42))
% 1.51/1.76  (define @t187 () (tptp.join @t150 tptp.c))
% 1.51/1.76  (define @t188 () (tptp.meet @t138 @t46))
% 1.51/1.76  (define @t189 () (tptp.meet @t25 @t22))
% 1.51/1.76  (define @t190 () (tptp.meet @t54 @t50))
% 1.51/1.76  (define @t191 () (= tptp.a @t65))
% 1.51/1.76  (define @t192 () (= tptp.a @t92))
% 1.51/1.76  (define @t193 () (= tptp.a @t41))
% 1.51/1.76  (define @t194 () (= tptp.b @t49))
% 1.51/1.76  (define @t195 () (= @t22 @t52))
% 1.51/1.76  (define @t196 () (= @t24 @t42))
% 1.51/1.76  (define @t197 () (= @t23 @t44))
% 1.51/1.76  (define @t198 () (= @t22 @t58))
% 1.51/1.76  (define @t199 () (= @t21 @t50))
% 1.51/1.76  (define @t200 () (= @t25 @t60))
% 1.51/1.76  (define @t201 () (tptp.meet tptp.b @t58))
% 1.51/1.76  (define @t202 () (= tptp.b @t201))
% 1.51/1.76  (define @t203 () (tptp.meet tptp.b @t49))
% 1.51/1.76  (define @t204 () (= tptp.b @t203))
% 1.51/1.76  (define @t205 () (= tptp.c @t146))
% 1.51/1.76  (define @t206 () (tptp.meet @t24 @t60))
% 1.51/1.76  (define @t207 () (= @t24 @t206))
% 1.51/1.76  (define @t208 () (tptp.meet @t22 @t52))
% 1.51/1.76  (define @t209 () (= @t22 @t208))
% 1.51/1.76  (define @t210 () (tptp.join tptp.a @t41))
% 1.51/1.76  (define @t211 () (= tptp.a @t210))
% 1.51/1.76  (define @t212 () (tptp.join tptp.c @t42))
% 1.51/1.76  (define @t213 () (= tptp.c @t212))
% 1.51/1.76  (define @t214 () (= @t21 @t104))
% 1.51/1.76  (define @t215 () (tptp.meet @t25 tptp.a))
% 1.51/1.76  (define @t216 () (= @t41 @t215))
% 1.51/1.76  (define @t217 () (tptp.meet @t22 tptp.a))
% 1.51/1.76  (define @t218 () (= @t65 @t217))
% 1.51/1.76  (define @t219 () (= @t92 @t133))
% 1.51/1.76  (define @t220 () (= @t49 @t137))
% 1.51/1.76  (define @t221 () (= @t52 @t71))
% 1.51/1.76  (define @t222 () (tptp.meet tptp.a @t56))
% 1.51/1.76  (define @t223 () (= (tptp.meet @t41 @t21) @t222))
% 1.51/1.76  (define @t224 () (tptp.meet tptp.a @t68))
% 1.51/1.76  (define @t225 () (tptp.meet @t41 @t25))
% 1.51/1.76  (define @t226 () (= @t225 @t224))
% 1.51/1.76  (define @t227 () (tptp.join tptp.b @t88))
% 1.51/1.76  (define @t228 () (= (tptp.join @t49 @t24) @t227))
% 1.51/1.76  (define @t229 () (tptp.join tptp.a @t63))
% 1.51/1.76  (define @t230 () (= @t52 @t229))
% 1.51/1.76  (define @t231 () (tptp.join tptp.b @t60))
% 1.51/1.76  (define @t232 () (= (tptp.join @t49 tptp.a) @t231))
% 1.51/1.76  (define @t233 () (tptp.join @t22 @t24))
% 1.51/1.76  (define @t234 () (= @t233 (tptp.join tptp.a @t49)))
% 1.51/1.76  (define @t235 () (tptp.meet @t62 @t50))
% 1.51/1.76  (define @t236 () (tptp.join @t67 @t64))
% 1.51/1.76  (define @t237 () (= @t236 @t235))
% 1.51/1.76  (define @t238 () (= @t25 @t68))
% 1.51/1.76  (define @t239 () (= @t24 @t88))
% 1.51/1.76  (define @t240 () (= tptp.a (tptp.meet tptp.a @t210)))
% 1.51/1.76  (define @t241 () (= tptp.a @t175))
% 1.51/1.76  (define @t242 () (tptp.meet tptp.c @t212))
% 1.51/1.76  (define @t243 () (= tptp.c @t242))
% 1.51/1.76  (define @t244 () (tptp.meet @t24 @t137))
% 1.51/1.76  (define @t245 () (= @t24 @t244))
% 1.51/1.76  (define @t246 () (tptp.meet @t21 @t104))
% 1.51/1.76  (define @t247 () (= @t21 @t246))
% 1.51/1.76  (define @t248 () (= @t23 (tptp.meet @t23 @t71)))
% 1.51/1.76  (define @t249 () (tptp.meet @t47 @t79))
% 1.51/1.76  (define @t250 () (= @t47 @t249))
% 1.51/1.76  (define @t251 () (tptp.join tptp.b @t203))
% 1.51/1.76  (define @t252 () (= tptp.b @t251))
% 1.51/1.76  (define @t253 () (tptp.join tptp.c @t64))
% 1.51/1.76  (define @t254 () (= tptp.c @t253))
% 1.51/1.76  (define @t255 () (tptp.join tptp.c @t146))
% 1.51/1.76  (define @t256 () (= tptp.c @t255))
% 1.51/1.76  (define @t257 () (tptp.join @t25 @t215))
% 1.51/1.76  (define @t258 () (= @t25 @t257))
% 1.51/1.76  (define @t259 () (= @t22 (tptp.join @t22 @t217)))
% 1.51/1.76  (define @t260 () (= @t22 (tptp.join @t22 @t208)))
% 1.51/1.76  (define @t261 () (= @t21 (tptp.join @t21 @t133)))
% 1.51/1.76  (define @t262 () (tptp.join @t46 @t47))
% 1.51/1.76  (define @t263 () (= @t46 @t262))
% 1.51/1.76  (define @t264 () (tptp.join @t54 @t61))
% 1.51/1.76  (define @t265 () (= @t54 @t264))
% 1.51/1.76  (define @t266 () (tptp.meet @t56 tptp.a))
% 1.51/1.76  (define @t267 () (= @t222 @t266))
% 1.51/1.76  (define @t268 () (tptp.meet tptp.a tptp.b))
% 1.51/1.76  (define @t269 () (= @t122 @t268))
% 1.51/1.76  (define @t270 () (tptp.meet @t58 tptp.b))
% 1.51/1.76  (define @t271 () (= @t201 @t270))
% 1.51/1.76  (define @t272 () (tptp.meet tptp.a tptp.c))
% 1.51/1.76  (define @t273 () (= @t64 @t272))
% 1.51/1.76  (define @t274 () (tptp.meet @t50 tptp.c))
% 1.51/1.76  (define @t275 () (= @t146 @t274))
% 1.51/1.76  (define @t276 () (tptp.meet @t60 @t24))
% 1.51/1.76  (define @t277 () (= @t206 @t276))
% 1.51/1.76  (define @t278 () (tptp.meet @t22 @t25))
% 1.51/1.76  (define @t279 () (= @t189 @t278))
% 1.51/1.76  (define @t280 () (= @t47 @t162))
% 1.51/1.76  (define @t281 () (tptp.meet tptp.c @t54))
% 1.51/1.76  (define @t282 () (= @t61 @t281))
% 1.51/1.76  (define @t283 () (= @t235 (tptp.meet @t50 @t62)))
% 1.51/1.76  (define @t284 () (tptp.join @t22 tptp.a))
% 1.51/1.76  (define @t285 () (= @t54 @t284))
% 1.51/1.76  (define @t286 () (= @t46 @t126))
% 1.51/1.76  (define @t287 () (tptp.join @t63 tptp.a))
% 1.51/1.76  (define @t288 () (= @t229 @t287))
% 1.51/1.76  (define @t289 () (tptp.join @t60 tptp.b))
% 1.51/1.76  (define @t290 () (= @t231 @t289))
% 1.51/1.76  (define @t291 () (tptp.join @t23 tptp.b))
% 1.51/1.76  (define @t292 () (= @t63 @t291))
% 1.51/1.76  (define @t293 () (tptp.join @t42 tptp.c))
% 1.51/1.76  (define @t294 () (= @t212 @t293))
% 1.51/1.76  (define @t295 () (tptp.join @t24 @t22))
% 1.51/1.76  (define @t296 () (= @t233 @t295))
% 1.51/1.76  (define @t297 () (= @t104 @t142))
% 1.51/1.76  (define @t298 () (tptp.join @t64 @t67))
% 1.51/1.76  (define @t299 () (= @t236 @t298))
% 1.51/1.76  (define @t300 () (= @t79 (tptp.join @t21 @t47)))
% 1.51/1.76  (define @t301 () (= @t62 (tptp.join @t22 @t61)))
% 1.51/1.76  (define @t302 () (tptp.meet @t208 @t21))
% 1.51/1.76  (define @t303 () (= @t302 (tptp.meet @t22 (tptp.meet @t52 @t21))))
% 1.51/1.76  (define @t304 () (tptp.meet @t49 tptp.c))
% 1.51/1.76  (define @t305 () (tptp.meet tptp.b @t304))
% 1.51/1.76  (define @t306 () (= (tptp.meet @t203 tptp.c) @t305))
% 1.51/1.76  (define @t307 () (tptp.meet tptp.c @t147))
% 1.51/1.76  (define @t308 () (tptp.meet @t146 tptp.b))
% 1.51/1.76  (define @t309 () (= @t308 @t307))
% 1.51/1.76  (define @t310 () (tptp.meet tptp.b @t148))
% 1.51/1.76  (define @t311 () (= @t206 @t310))
% 1.51/1.76  (define @t312 () (tptp.meet @t24 @t50))
% 1.51/1.76  (define @t313 () (= @t312 (tptp.meet tptp.b @t146)))
% 1.51/1.76  (define @t314 () (= @t114 (tptp.meet @t22 @t133)))
% 1.51/1.76  (define @t315 () (tptp.meet @t46 @t203))
% 1.51/1.76  (define @t316 () (tptp.meet @t47 @t49))
% 1.51/1.76  (define @t317 () (= @t316 @t315))
% 1.51/1.76  (define @t318 () (tptp.meet @t122 @t68))
% 1.51/1.76  (define @t319 () (= @t318 (tptp.meet tptp.b @t224)))
% 1.51/1.76  (define @t320 () (tptp.meet @t54 @t146))
% 1.51/1.76  (define @t321 () (= (tptp.meet @t61 @t50) @t320))
% 1.51/1.76  (define @t322 () (tptp.join @t41 @t24))
% 1.51/1.76  (define @t323 () (tptp.join @t210 @t24))
% 1.51/1.76  (define @t324 () (= @t323 (tptp.join tptp.a @t322)))
% 1.51/1.76  (define @t325 () (tptp.join tptp.a @t212))
% 1.51/1.76  (define @t326 () (tptp.join @t21 @t42))
% 1.51/1.76  (define @t327 () (= @t326 @t325))
% 1.51/1.76  (define @t328 () (tptp.meet @t140 @t138))
% 1.51/1.76  (define @t329 () (tptp.meet @t88 tptp.b))
% 1.51/1.76  (define @t330 () (= (tptp.join (tptp.meet (tptp.join @t201 @t88) @t58) @t329) @t328))
% 1.51/1.76  (define @t331 () (tptp.meet @t124 @t58))
% 1.51/1.76  (define @t332 () (tptp.join @t136 @t122))
% 1.51/1.76  (define @t333 () (= @t332 @t331))
% 1.51/1.76  (define @t334 () (tptp.meet @t128 @t125))
% 1.51/1.76  (define @t335 () (tptp.meet @t24 @t21))
% 1.51/1.76  (define @t336 () (tptp.join @t133 @t24))
% 1.51/1.76  (define @t337 () (tptp.meet @t336 tptp.a))
% 1.51/1.76  (define @t338 () (tptp.join @t337 @t335))
% 1.51/1.76  (define @t339 () (= @t338 @t334))
% 1.51/1.76  (define @t340 () (tptp.meet @t46 @t24))
% 1.51/1.76  (define @t341 () (tptp.join @t340 @t21))
% 1.51/1.76  (define @t342 () (tptp.join @t94 @t91))
% 1.51/1.76  (define @t343 () (= @t342 (tptp.meet @t341 @t60)))
% 1.51/1.76  (define @t344 () (tptp.meet @t110 @t107))
% 1.51/1.76  (define @t345 () (tptp.meet @t41 tptp.a))
% 1.51/1.76  (define @t346 () (tptp.join @t222 @t41))
% 1.51/1.76  (define @t347 () (tptp.meet @t346 @t56))
% 1.51/1.76  (define @t348 () (tptp.join @t347 @t345))
% 1.51/1.76  (define @t349 () (= @t348 @t344))
% 1.51/1.76  (define @t350 () (tptp.meet @t233 tptp.a))
% 1.51/1.76  (define @t351 () (tptp.join @t350 @t24))
% 1.51/1.76  (define @t352 () (tptp.meet @t351 @t54))
% 1.51/1.76  (define @t353 () (= (tptp.join (tptp.meet (tptp.join @t101 tptp.a) @t24) @t65) @t352))
% 1.51/1.76  (define @t354 () (tptp.join tptp.c @t24))
% 1.51/1.76  (define @t355 () (tptp.meet @t137 tptp.c))
% 1.51/1.76  (define @t356 () (tptp.join @t355 tptp.b))
% 1.51/1.76  (define @t357 () (tptp.meet @t356 @t354))
% 1.51/1.76  (define @t358 () (tptp.meet tptp.c @t24))
% 1.51/1.76  (define @t359 () (= (tptp.join (tptp.meet (tptp.join (tptp.meet @t24 tptp.b) tptp.c) tptp.b) @t358) @t357))
% 1.51/1.76  (define @t360 () (tptp.meet (tptp.join @t304 @t24) @t158))
% 1.51/1.76  (define @t361 () (tptp.meet tptp.b @t24))
% 1.51/1.76  (define @t362 () (tptp.join @t361 tptp.c))
% 1.51/1.76  (define @t363 () (tptp.meet @t362 @t24))
% 1.51/1.76  (define @t364 () (tptp.join @t363 @t42))
% 1.51/1.76  (define @t365 () (= @t364 @t360))
% 1.51/1.76  (define @t366 () (tptp.join tptp.a tptp.a))
% 1.51/1.76  (define @t367 () (tptp.meet @t229 tptp.a))
% 1.51/1.76  (define @t368 () (tptp.join @t367 @t63))
% 1.51/1.76  (define @t369 () (tptp.meet @t368 @t366))
% 1.51/1.76  (define @t370 () (tptp.join @t99 @t96))
% 1.51/1.76  (define @t371 () (= @t370 @t369))
% 1.51/1.76  (define @t372 () (tptp.join @t52 @t22))
% 1.51/1.76  (define @t373 () (tptp.meet @t233 @t52))
% 1.51/1.76  (define @t374 () (tptp.join @t373 @t24))
% 1.51/1.76  (define @t375 () (tptp.meet @t374 @t372))
% 1.51/1.76  (define @t376 () (tptp.join @t103 @t100))
% 1.51/1.76  (define @t377 () (= @t376 @t375))
% 1.51/1.76  (define @t378 () (= tptp.a (tptp.meet tptp.a @t108)))
% 1.51/1.76  (define @t379 () (tptp.meet tptp.b @t105))
% 1.51/1.76  (define @t380 () (= tptp.b @t379))
% 1.51/1.76  (define @t381 () (tptp.meet tptp.c @t158))
% 1.51/1.76  (define @t382 () (= tptp.c @t381))
% 1.51/1.76  (define @t383 () (= @t42 (tptp.meet @t42 @t293)))
% 1.51/1.76  (define @t384 () (= @t24 (tptp.meet @t24 @t295)))
% 1.51/1.76  (define @t385 () (= @t60 (tptp.meet @t60 @t289)))
% 1.51/1.76  (define @t386 () (= @t44 (tptp.meet @t44 @t142)))
% 1.51/1.76  (define @t387 () (tptp.meet @t47 @t77))
% 1.51/1.76  (define @t388 () (= @t47 @t387))
% 1.51/1.76  (define @t389 () (= @t77 (tptp.meet @t77 @t78)))
% 1.51/1.76  (define @t390 () (= @t94 (tptp.meet @t94 @t342)))
% 1.51/1.76  (define @t391 () (tptp.meet @t95 @t111))
% 1.51/1.76  (define @t392 () (= @t95 @t391))
% 1.51/1.76  (define @t393 () (= @t99 (tptp.meet @t99 @t370)))
% 1.51/1.76  (define @t394 () (tptp.meet @t103 @t376))
% 1.51/1.76  (define @t395 () (= @t103 @t394))
% 1.51/1.76  (define @t396 () (= tptp.a (tptp.join tptp.a @t272)))
% 1.51/1.76  (define @t397 () (tptp.join tptp.b @t162))
% 1.51/1.76  (define @t398 () (= tptp.b @t397))
% 1.51/1.76  (define @t399 () (tptp.join @t24 @t91))
% 1.51/1.76  (define @t400 () (= @t24 @t399))
% 1.51/1.76  (define @t401 () (= @t60 (tptp.join @t60 @t276)))
% 1.51/1.76  (define @t402 () (= @t58 (tptp.join @t58 @t270)))
% 1.51/1.76  (define @t403 () (= @t50 (tptp.join @t50 @t274)))
% 1.51/1.76  (define @t404 () (= @t21 (tptp.join @t21 @t246)))
% 1.51/1.76  (define @t405 () (= @t23 (tptp.join @t23 @t114)))
% 1.51/1.76  (define @t406 () (tptp.meet @t105 tptp.b))
% 1.51/1.76  (define @t407 () (= @t105 (tptp.join @t105 @t406)))
% 1.51/1.76  (define @t408 () (= @t56 (tptp.join @t56 @t266)))
% 1.51/1.76  (define @t409 () (= @t110 (tptp.join @t110 @t344)))
% 1.51/1.76  (define @t410 () (tptp.meet @t111 @t42))
% 1.51/1.76  (define @t411 () (= @t111 (tptp.join @t111 @t410)))
% 1.51/1.76  (define @t412 () (tptp.meet @t60 tptp.c))
% 1.51/1.76  (define @t413 () (= @t148 @t412))
% 1.51/1.76  (define @t414 () (tptp.meet @t50 @t24))
% 1.51/1.76  (define @t415 () (= @t312 @t414))
% 1.51/1.76  (define @t416 () (tptp.meet @t56 @t68))
% 1.51/1.76  (define @t417 () (tptp.meet @t68 @t56))
% 1.51/1.76  (define @t418 () (= @t417 @t416))
% 1.51/1.76  (define @t419 () (tptp.meet @t24 @t54))
% 1.51/1.76  (define @t420 () (tptp.meet @t54 @t24))
% 1.51/1.76  (define @t421 () (= @t420 @t419))
% 1.51/1.76  (define @t422 () (tptp.meet @t23 @t21))
% 1.51/1.76  (define @t423 () (= (tptp.meet @t21 @t23) @t422))
% 1.51/1.76  (define @t424 () (tptp.meet @t49 @t47))
% 1.51/1.76  (define @t425 () (= @t316 @t424))
% 1.51/1.76  (define @t426 () (= @t249 (tptp.meet @t79 @t47)))
% 1.51/1.76  (define @t427 () (tptp.meet @t68 @t122))
% 1.51/1.76  (define @t428 () (= @t318 @t427))
% 1.51/1.76  (define @t429 () (= @t406 @t379))
% 1.51/1.76  (define @t430 () (tptp.meet @t88 @t123))
% 1.51/1.76  (define @t431 () (= @t139 @t430))
% 1.51/1.76  (define @t432 () (= @t331 (tptp.meet @t58 @t124)))
% 1.51/1.76  (define @t433 () (tptp.meet @t125 @t128))
% 1.51/1.76  (define @t434 () (= @t334 @t433))
% 1.51/1.76  (define @t435 () (tptp.meet @t41 @t108))
% 1.51/1.76  (define @t436 () (= @t109 @t435))
% 1.51/1.76  (define @t437 () (= @t410 (tptp.meet @t42 @t111)))
% 1.51/1.76  (define @t438 () (tptp.join @t135 @t132))
% 1.51/1.76  (define @t439 () (= @t438 (tptp.join @t132 @t135)))
% 1.51/1.76  (define @t440 () (tptp.join @t56 tptp.a))
% 1.51/1.76  (define @t441 () (= @t108 @t440))
% 1.51/1.76  (define @t442 () (= @t105 @t158))
% 1.51/1.76  (define @t443 () (tptp.join @t58 tptp.b))
% 1.51/1.76  (define @t444 () (= @t123 @t443))
% 1.51/1.76  (define @t445 () (tptp.join @t50 tptp.c))
% 1.51/1.76  (define @t446 () (= (tptp.join tptp.c @t50) @t445))
% 1.51/1.76  (define @t447 () (tptp.join @t60 @t88))
% 1.51/1.76  (define @t448 () (= (tptp.join @t88 @t60) @t447))
% 1.51/1.76  (define @t449 () (= @t125 (tptp.join @t21 @t24)))
% 1.51/1.76  (define @t450 () (tptp.join @t23 @t24))
% 1.51/1.76  (define @t451 () (= (tptp.join @t24 @t23) @t450))
% 1.51/1.76  (define @t452 () (tptp.join @t122 @t136))
% 1.51/1.76  (define @t453 () (= @t332 @t452))
% 1.51/1.76  (define @t454 () (tptp.join tptp.a @t61))
% 1.51/1.76  (define @t455 () (= @t83 @t454))
% 1.51/1.76  (define @t456 () (tptp.join tptp.c @t77))
% 1.51/1.76  (define @t457 () (= @t78 @t456))
% 1.51/1.76  (define @t458 () (tptp.meet @t312 @t137))
% 1.51/1.76  (define @t459 () (= @t458 (tptp.meet @t24 @t185)))
% 1.51/1.76  (define @t460 () (tptp.meet @t328 @t46))
% 1.51/1.76  (define @t461 () (= @t460 (tptp.meet @t140 @t188)))
% 1.51/1.76  (define @t462 () (tptp.meet @t281 @t50))
% 1.51/1.76  (define @t463 () (= @t462 (tptp.meet tptp.c @t190)))
% 1.51/1.76  (define @t464 () (tptp.meet @t46 @t140))
% 1.51/1.76  (define @t465 () (tptp.meet @t464 @t138))
% 1.51/1.76  (define @t466 () (= @t465 (tptp.meet @t46 @t328)))
% 1.51/1.76  (define @t467 () (tptp.meet @t190 tptp.c))
% 1.51/1.76  (define @t468 () (= @t467 (tptp.meet @t54 @t274)))
% 1.51/1.76  (define @t469 () (tptp.meet tptp.c @t344))
% 1.51/1.76  (define @t470 () (= (tptp.meet @t184 @t107) @t469))
% 1.51/1.76  (define @t471 () (tptp.meet @t23 @t344))
% 1.51/1.76  (define @t472 () (tptp.meet (tptp.meet @t23 @t110) @t107))
% 1.51/1.76  (define @t473 () (= @t472 @t471))
% 1.51/1.76  (define @t474 () (tptp.join tptp.c @t186))
% 1.51/1.76  (define @t475 () (tptp.join @t253 @t42))
% 1.51/1.76  (define @t476 () (= @t475 @t474))
% 1.51/1.76  (define @t477 () (tptp.join tptp.b @t255))
% 1.51/1.76  (define @t478 () (= (tptp.join @t105 @t146) @t477))
% 1.51/1.76  (define @t479 () (tptp.join @t24 @t46))
% 1.51/1.76  (define @t480 () (tptp.meet @t479 tptp.b))
% 1.51/1.76  (define @t481 () (tptp.join @t480 @t46))
% 1.51/1.76  (define @t482 () (tptp.meet @t481 @t49))
% 1.51/1.76  (define @t483 () (tptp.join (tptp.meet (tptp.join (tptp.meet @t24 @t46) tptp.b) @t46) @t361))
% 1.51/1.76  (define @t484 () (= @t483 @t482))
% 1.51/1.76  (define @t485 () (tptp.meet @t157 @t155))
% 1.51/1.76  (define @t486 () (= (tptp.join (tptp.meet (tptp.join @t307 tptp.c) @t147) (tptp.meet tptp.c tptp.c)) @t485))
% 1.51/1.76  (define @t487 () (tptp.meet @t174 @t172))
% 1.51/1.76  (define @t488 () (= (tptp.join (tptp.meet (tptp.join @t310 tptp.b) @t148) (tptp.meet tptp.b tptp.b)) @t487))
% 1.51/1.76  (define @t489 () (tptp.join @t67 tptp.c))
% 1.51/1.76  (define @t490 () (tptp.meet @t50 @t67))
% 1.51/1.76  (define @t491 () (tptp.join @t490 tptp.a))
% 1.51/1.76  (define @t492 () (tptp.meet @t491 @t489))
% 1.51/1.76  (define @t493 () (= (tptp.join (tptp.meet @t298 tptp.a) (tptp.meet @t67 tptp.c)) @t492))
% 1.51/1.76  (define @t494 () (tptp.join tptp.a @t83))
% 1.51/1.76  (define @t495 () (tptp.meet @t84 tptp.a))
% 1.51/1.76  (define @t496 () (tptp.join @t495 tptp.b))
% 1.51/1.76  (define @t497 () (tptp.meet @t496 @t494))
% 1.51/1.76  (define @t498 () (tptp.join @t169 @t168))
% 1.51/1.76  (define @t499 () (= @t498 @t497))
% 1.51/1.76  (define @t500 () (tptp.join @t21 @t103))
% 1.51/1.76  (define @t501 () (tptp.join @t103 @t22))
% 1.51/1.76  (define @t502 () (tptp.meet @t501 @t21))
% 1.51/1.76  (define @t503 () (tptp.join @t502 @t22))
% 1.51/1.76  (define @t504 () (tptp.meet @t503 @t500))
% 1.51/1.76  (define @t505 () (= (tptp.join (tptp.meet (tptp.join (tptp.meet @t103 @t22) @t21) @t22) (tptp.meet @t21 @t103)) @t504))
% 1.51/1.76  (define @t506 () (tptp.join tptp.b @t47))
% 1.51/1.76  (define @t507 () (tptp.meet @t79 tptp.b))
% 1.51/1.76  (define @t508 () (tptp.join @t507 @t21))
% 1.51/1.76  (define @t509 () (tptp.meet @t508 @t506))
% 1.51/1.76  (define @t510 () (tptp.meet @t47 @t21))
% 1.51/1.76  (define @t511 () (tptp.join @t510 tptp.b))
% 1.51/1.76  (define @t512 () (tptp.join (tptp.meet @t511 @t21) (tptp.meet tptp.b @t47)))
% 1.51/1.76  (define @t513 () (= @t512 @t509))
% 1.51/1.76  (define @t514 () (tptp.join @t147 tptp.a))
% 1.51/1.76  (define @t515 () (tptp.meet @t514 @t105))
% 1.51/1.76  (define @t516 () (tptp.join @t64 tptp.b))
% 1.51/1.76  (define @t517 () (tptp.meet @t516 tptp.a))
% 1.51/1.76  (define @t518 () (= (tptp.join @t517 @t24) @t515))
% 1.51/1.76  (define @t519 () (tptp.join @t24 tptp.c))
% 1.51/1.76  (define @t520 () (tptp.join @t414 tptp.a))
% 1.51/1.76  (define @t521 () (tptp.meet @t520 @t519))
% 1.51/1.76  (define @t522 () (tptp.join @t183 @t182))
% 1.51/1.76  (define @t523 () (= @t522 @t521))
% 1.51/1.76  (define @t524 () (tptp.join tptp.a @t46))
% 1.51/1.76  (define @t525 () (tptp.join @t46 @t132))
% 1.51/1.76  (define @t526 () (tptp.meet @t525 tptp.a))
% 1.51/1.76  (define @t527 () (tptp.join @t526 @t132))
% 1.51/1.76  (define @t528 () (tptp.meet @t527 @t524))
% 1.51/1.76  (define @t529 () (tptp.join @t181 @t175))
% 1.51/1.76  (define @t530 () (= @t529 @t528))
% 1.51/1.76  (define @t531 () (tptp.meet @t171 @t170))
% 1.51/1.76  (define @t532 () (tptp.meet @t24 @t47))
% 1.51/1.76  (define @t533 () (tptp.join @t510 @t24))
% 1.51/1.76  (define @t534 () (tptp.meet @t533 @t21))
% 1.51/1.76  (define @t535 () (tptp.join @t534 @t532))
% 1.51/1.76  (define @t536 () (= @t535 @t531))
% 1.51/1.76  (define @t537 () (tptp.join @t24 @t101))
% 1.51/1.76  (define @t538 () (tptp.join @t101 @t65))
% 1.51/1.76  (define @t539 () (tptp.meet @t538 @t24))
% 1.51/1.76  (define @t540 () (tptp.join @t539 @t65))
% 1.51/1.76  (define @t541 () (tptp.meet @t540 @t537))
% 1.51/1.76  (define @t542 () (tptp.join (tptp.meet (tptp.join (tptp.meet @t101 @t65) @t24) @t65) (tptp.meet @t24 @t101)))
% 1.51/1.76  (define @t543 () (= @t542 @t541))
% 1.51/1.76  (define @t544 () (tptp.join tptp.a @t64))
% 1.51/1.76  (define @t545 () (tptp.join @t64 @t23))
% 1.51/1.76  (define @t546 () (tptp.meet @t545 tptp.a))
% 1.51/1.76  (define @t547 () (tptp.join @t546 @t23))
% 1.51/1.76  (define @t548 () (tptp.meet @t547 @t544))
% 1.51/1.76  (define @t549 () (tptp.join (tptp.meet (tptp.join (tptp.meet @t64 @t23) tptp.a) @t23) (tptp.meet tptp.a @t64)))
% 1.51/1.76  (define @t550 () (= @t549 @t548))
% 1.51/1.76  (define @t551 () (tptp.meet tptp.b @t160))
% 1.51/1.76  (define @t552 () (= tptp.b @t551))
% 1.51/1.76  (define @t553 () (tptp.join tptp.c @t47))
% 1.51/1.76  (define @t554 () (= tptp.c (tptp.meet tptp.c @t553)))
% 1.51/1.76  (define @t555 () (tptp.meet @t150 @t187))
% 1.51/1.76  (define @t556 () (= @t150 @t555))
% 1.51/1.76  (define @t557 () (= @t122 (tptp.meet @t122 @t452)))
% 1.51/1.76  (define @t558 () (tptp.meet @t60 tptp.b))
% 1.51/1.76  (define @t559 () (tptp.join @t60 @t558))
% 1.51/1.76  (define @t560 () (= @t60 @t559))
% 1.51/1.76  (define @t561 () (tptp.join @t60 @t412))
% 1.51/1.76  (define @t562 () (= @t60 @t561))
% 1.51/1.76  (define @t563 () (= @t68 (tptp.join @t68 @t427)))
% 1.51/1.76  (define @t564 () (= @t152 (tptp.join @t152 @t181)))
% 1.51/1.76  (define @t565 () (= @t153 (tptp.join @t153 @t156)))
% 1.51/1.76  (define @t566 () (= @t157 (tptp.join @t157 @t485)))
% 1.51/1.76  (define @t567 () (tptp.meet @t47 tptp.a))
% 1.51/1.76  (define @t568 () (= @t177 @t567))
% 1.51/1.76  (define @t569 () (tptp.meet @t158 tptp.c))
% 1.51/1.76  (define @t570 () (= @t381 @t569))
% 1.51/1.76  (define @t571 () (tptp.meet @t77 @t47))
% 1.51/1.76  (define @t572 () (= @t387 @t571))
% 1.51/1.76  (define @t573 () (tptp.meet tptp.c @t77))
% 1.51/1.76  (define @t574 () (= @t167 @t573))
% 1.51/1.76  (define @t575 () (tptp.meet tptp.c @t153))
% 1.51/1.76  (define @t576 () (= @t156 @t575))
% 1.51/1.76  (define @t577 () (= @t173 @t551))
% 1.51/1.76  (define @t578 () (tptp.meet tptp.c @t161))
% 1.51/1.76  (define @t579 () (= (tptp.meet @t161 tptp.c) @t578))
% 1.51/1.76  (define @t580 () (tptp.join @t162 tptp.b))
% 1.51/1.76  (define @t581 () (= @t397 @t580))
% 1.51/1.76  (define @t582 () (tptp.join @t47 tptp.c))
% 1.51/1.76  (define @t583 () (= @t553 @t582))
% 1.51/1.76  (define @t584 () (tptp.join @t147 @t119))
% 1.51/1.76  (define @t585 () (= @t161 @t584))
% 1.51/1.76  (define @t586 () (tptp.join @t164 @t122))
% 1.51/1.76  (define @t587 () (= @t586 (tptp.join @t122 @t164)))
% 1.51/1.76  (define @t588 () (tptp.join @t77 @t47))
% 1.51/1.76  (define @t589 () (= (tptp.join @t47 @t77) @t588))
% 1.51/1.76  (define @t590 () (tptp.join @t42 @t77))
% 1.51/1.76  (define @t591 () (= (tptp.join @t77 @t42) @t590))
% 1.51/1.76  (define @t592 () (tptp.join @t166 @t25))
% 1.51/1.76  (define @t593 () (= @t592 (tptp.join @t25 @t166)))
% 1.51/1.76  (define @t594 () (tptp.join tptp.a @t167))
% 1.51/1.76  (define @t595 () (= (tptp.join @t167 tptp.a) @t594))
% 1.51/1.76  (define @t596 () (= @t498 (tptp.join @t168 @t169)))
% 1.51/1.76  (define @t597 () (tptp.meet @t140 @t531))
% 1.51/1.76  (define @t598 () (= (tptp.meet (tptp.meet @t140 @t171) @t170) @t597))
% 1.51/1.76  (define @t599 () (tptp.meet @t60 @t174))
% 1.51/1.76  (define @t600 () (tptp.meet @t599 @t172))
% 1.51/1.76  (define @t601 () (= @t600 (tptp.meet @t60 @t487)))
% 1.51/1.76  (define @t602 () (tptp.meet @t152 @t46))
% 1.51/1.76  (define @t603 () (tptp.meet @t602 tptp.b))
% 1.51/1.76  (define @t604 () (= @t603 (tptp.meet @t152 @t47)))
% 1.51/1.76  (define @t605 () (tptp.join @t529 @t42))
% 1.51/1.76  (define @t606 () (= @t605 (tptp.join @t181 (tptp.join @t175 @t42))))
% 1.51/1.76  (define @t607 () (tptp.join @t522 tptp.a))
% 1.51/1.76  (define @t608 () (= @t607 (tptp.join @t183 (tptp.join @t182 tptp.a))))
% 1.51/1.76  (define @t609 () (tptp.join @t182 @t25))
% 1.51/1.76  (define @t610 () (tptp.join @t183 @t609))
% 1.51/1.76  (define @t611 () (= (tptp.join @t522 @t25) @t610))
% 1.51/1.76  (define @t612 () (tptp.meet @t105 @t147))
% 1.51/1.76  (define @t613 () (tptp.join @t612 tptp.c))
% 1.51/1.76  (define @t614 () (tptp.meet @t147 tptp.b))
% 1.51/1.76  (define @t615 () (tptp.join @t24 @t147))
% 1.51/1.76  (define @t616 () (tptp.meet @t615 tptp.c))
% 1.51/1.76  (define @t617 () (tptp.join @t616 @t614))
% 1.51/1.76  (define @t618 () (= @t617 (tptp.meet @t613 (tptp.join @t147 tptp.b))))
% 1.51/1.76  (define @t619 () (tptp.meet tptp.b @t184))
% 1.51/1.76  (define @t620 () (tptp.meet @t184 tptp.a))
% 1.51/1.76  (define @t621 () (tptp.join @t620 tptp.b))
% 1.51/1.76  (define @t622 () (tptp.meet @t621 tptp.a))
% 1.51/1.76  (define @t623 () (tptp.join @t622 @t619))
% 1.51/1.76  (define @t624 () (= @t623 (tptp.meet (tptp.join (tptp.meet (tptp.join @t184 tptp.a) tptp.b) tptp.a) (tptp.join tptp.b @t184))))
% 1.51/1.76  (define @t625 () (tptp.join @t268 @t25))
% 1.51/1.76  (define @t626 () (tptp.meet @t625 tptp.b))
% 1.51/1.76  (define @t627 () (tptp.join @t626 @t215))
% 1.51/1.76  (define @t628 () (= @t627 (tptp.meet (tptp.join @t278 tptp.b) (tptp.join @t25 tptp.a))))
% 1.51/1.76  (define @t629 () (tptp.join @t122 tptp.c))
% 1.51/1.76  (define @t630 () (tptp.meet @t629 tptp.a))
% 1.51/1.76  (define @t631 () (tptp.join @t630 @t42))
% 1.51/1.76  (define @t632 () (= @t631 (tptp.meet (tptp.join (tptp.meet @t58 tptp.c) tptp.a) @t158)))
% 1.51/1.76  (define @t633 () (tptp.join @t185 @t24))
% 1.51/1.76  (define @t634 () (tptp.meet @t399 @t185))
% 1.51/1.76  (define @t635 () (tptp.join @t634 @t91))
% 1.51/1.76  (define @t636 () (tptp.meet @t635 @t633))
% 1.51/1.76  (define @t637 () (tptp.join (tptp.meet (tptp.join (tptp.meet @t24 @t91) @t185) @t91) (tptp.meet @t185 @t24)))
% 1.51/1.76  (define @t638 () (= @t637 @t636))
% 1.51/1.76  (define @t639 () (tptp.join @t158 tptp.c))
% 1.51/1.76  (define @t640 () (tptp.meet @t474 @t158))
% 1.51/1.76  (define @t641 () (tptp.join @t640 @t186))
% 1.51/1.76  (define @t642 () (tptp.meet @t641 @t639))
% 1.51/1.76  (define @t643 () (tptp.join (tptp.meet (tptp.join (tptp.meet tptp.c @t186) @t158) @t186) @t569))
% 1.51/1.76  (define @t644 () (= @t643 @t642))
% 1.51/1.76  (define @t645 () (tptp.join tptp.c @t181))
% 1.51/1.76  (define @t646 () (tptp.join @t181 tptp.a))
% 1.51/1.76  (define @t647 () (tptp.meet @t646 tptp.c))
% 1.51/1.76  (define @t648 () (tptp.join @t647 tptp.a))
% 1.51/1.76  (define @t649 () (tptp.meet @t648 @t645))
% 1.51/1.76  (define @t650 () (= (tptp.join (tptp.meet (tptp.join (tptp.meet @t181 tptp.a) tptp.c) tptp.a) (tptp.meet tptp.c @t181)) @t649))
% 1.51/1.76  (define @t651 () (tptp.join tptp.b @t147))
% 1.51/1.76  (define @t652 () (tptp.meet @t651 tptp.c))
% 1.51/1.76  (define @t653 () (tptp.join @t652 @t147))
% 1.51/1.76  (define @t654 () (tptp.meet @t653 @t158))
% 1.51/1.76  (define @t655 () (tptp.meet (tptp.join (tptp.meet tptp.b @t147) tptp.c) @t147))
% 1.51/1.76  (define @t656 () (= (tptp.join @t655 @t42) @t654))
% 1.51/1.76  (define @t657 () (tptp.meet @t158 @t185))
% 1.51/1.76  (define @t658 () (= (tptp.meet @t185 @t158) @t657))
% 1.51/1.76  (define @t659 () (tptp.meet @t187 @t150))
% 1.51/1.76  (define @t660 () (= @t555 @t659))
% 1.51/1.76  (define @t661 () (tptp.join @t188 @t189))
% 1.51/1.76  (define @t662 () (= (tptp.join @t189 @t188) @t661))
% 1.51/1.76  (define @t663 () (tptp.meet @t157 @t172))
% 1.51/1.76  (define @t664 () (tptp.meet @t190 @t663))
% 1.51/1.76  (define @t665 () (= (tptp.meet (tptp.meet @t190 @t157) @t172) @t664))
% 1.51/1.76  (define @t666 () (tptp.meet @t71 tptp.a))
% 1.51/1.76  (define @t667 () (tptp.join @t420 @t100))
% 1.51/1.76  (define @t668 () (tptp.join tptp.c @t21))
% 1.51/1.76  (define @t669 () (tptp.meet @t126 tptp.c))
% 1.51/1.76  (define @t670 () (tptp.join @t669 tptp.a))
% 1.51/1.76  (define @t671 () (tptp.join @t670 @t668))
% 1.51/1.76  (define @t672 () (tptp.meet @t671 @t42))
% 1.51/1.76  (define @t673 () (tptp.meet @t23 @t22))
% 1.51/1.76  (define @t674 () (tptp.meet @t287 tptp.c))
% 1.51/1.76  (define @t675 () (tptp.join @t203 @t88))
% 1.51/1.76  (define @t676 () (tptp.meet @t675 @t49))
% 1.51/1.76  (define @t677 () (tptp.meet @t126 tptp.b))
% 1.51/1.76  (define @t678 () (tptp.join @t677 tptp.a))
% 1.51/1.76  (define @t679 () (tptp.join @t24 @t358))
% 1.51/1.76  (define @t680 () (tptp.join @t360 @t147))
% 1.51/1.76  (define @t681 () (tptp.meet @t21 tptp.b))
% 1.51/1.76  (define @t682 () (tptp.join @t157 tptp.c))
% 1.51/1.76  (define @t683 () (tptp.join @t153 @t155))
% 1.51/1.76  (define @t684 () (tptp.join @t96 @t132))
% 1.51/1.76  (define @t685 () (tptp.meet @t456 tptp.b))
% 1.51/1.76  (define @t686 () (tptp.join @t685 @t77))
% 1.51/1.76  (define @t687 () (tptp.join tptp.b @t212))
% 1.51/1.76  (define @t688 () (tptp.join @t105 @t172))
% 1.51/1.76  (define @t689 () (tptp.meet @t688 tptp.c))
% 1.51/1.76  (define @t690 () (tptp.join @t689 @t172))
% 1.51/1.76  (define @t691 () (tptp.join @t127 @t215))
% 1.51/1.76  (define @t692 () (tptp.meet @t691 @t125))
% 1.51/1.76  (define @t693 () (tptp.join @t125 @t127))
% 1.51/1.76  (define @t694 () (tptp.join @t692 @t215))
% 1.51/1.76  (define @t695 () (tptp.join @t224 @t41))
% 1.51/1.76  (define @t696 () (tptp.meet @t695 @t68))
% 1.51/1.76  (define @t697 () (tptp.join @t65 @t41))
% 1.51/1.76  (define @t698 () (tptp.meet @t697 @t22))
% 1.51/1.76  (define @t699 () (tptp.join @t99 tptp.a))
% 1.51/1.76  (define @t700 () (tptp.join @t97 @t96))
% 1.51/1.76  (define @t701 () (tptp.meet @t99 @t41))
% 1.51/1.76  (define @t702 () (tptp.join @t701 @t417))
% 1.51/1.76  (define @t703 () (tptp.join tptp.a @t417))
% 1.51/1.76  (define @t704 () (tptp.meet @t703 @t41))
% 1.51/1.76  (define @t705 () (tptp.join @t206 tptp.c))
% 1.51/1.76  (define @t706 () (tptp.meet tptp.c @t322))
% 1.51/1.76  (define @t707 () (tptp.join @t110 tptp.a))
% 1.51/1.76  (define @t708 () (tptp.meet @t707 tptp.c))
% 1.51/1.76  (define @t709 () (tptp.meet @t165 tptp.b))
% 1.51/1.76  (define @t710 () (tptp.meet @t707 tptp.b))
% 1.51/1.76  (define @t711 () (tptp.join @t56 tptp.b))
% 1.51/1.76  (define @t712 () (tptp.meet @t122 @t711))
% 1.51/1.76  (define @t713 () (and @t191 @t192 @t193 @t194 @t195 @t196 @t197 @t198 @t199 @t200 @t202 @t204 @t205 @t207 @t209 @t211 @t213 @t214 @t216 @t218 @t219 @t220 @t221 @t223 @t226 @t228 @t230 @t232 @t234 @t237 @t238 @t239 @t240 @t241 @t243 @t245 @t247 @t248 @t250 @t252 @t254 @t256 @t258 @t259 @t260 @t261 @t263 @t265 @t267 @t269 @t271 @t273 @t275 @t277 @t279 @t280 @t282 @t283 @t285 @t286 @t288 @t290 @t292 @t294 @t296 @t297 @t299 @t300 @t301 @t303 @t306 @t309 @t311 @t313 @t314 @t317 @t319 @t321 @t324 @t327 @t74 @t82 @t87 @t330 @t333 @t339 @t343 @t349 @t353 @t359 @t365 @t371 @t377 @t378 @t380 @t382 @t383 @t384 @t385 @t386 @t388 @t389 @t390 @t392 @t393 @t395 @t396 @t398 @t400 @t401 @t402 @t403 @t404 @t405 @t407 @t408 @t409 @t411 @t117 @t121 @t413 @t415 @t418 @t421 @t423 @t425 @t426 @t428 @t429 @t431 @t432 @t434 @t436 @t437 @t131 @t439 @t441 @t442 @t444 @t446 @t448 @t449 @t451 @t453 @t455 @t457 @t459 @t461 @t463 @t466 @t468 @t470 @t473 @t476 @t145 @t478 @t484 @t486 @t488 @t493 @t499 @t505 @t513 @t518 @t523 @t530 @t536 @t543 @t550 @t552 @t554 @t556 @t557 @t560 @t562 @t563 @t564 @t565 @t566 @t568 @t570 @t572 @t574 @t576 @t577 @t579 @t581 @t583 @t585 @t587 @t589 @t591 @t593 @t595 @t596 @t598 @t601 @t180 @t604 @t606 @t608 @t611 @t618 @t624 @t628 @t632 @t638 @t644 @t650 @t656 @t658 @t660 @t662 @t665))
% 1.51/1.76  (assume @p1 @t4)
% 1.51/1.76  (assume @p2 @t6)
% 1.51/1.76  (assume @p3 @t11)
% 1.51/1.76  (assume @p4 @t14)
% 1.51/1.76  (assume @p5 @t15)
% 1.51/1.76  (assume @p6 @t16)
% 1.51/1.76  (assume @p7 @t19)
% 1.51/1.76  (assume @p8 @t20)
% 1.51/1.76  (assume @p9 (forall @t18 (= (tptp.join (tptp.meet (tptp.join @t12 @t17) @t7) (tptp.meet @t17 @t1)) (tptp.meet (tptp.join (tptp.meet @t8 @t17) @t7) (tptp.join @t17 @t1)))))
% 1.51/1.76  (assume @p10 (not @t26))
% 1.51/1.76  (step @p11 :rule eq-symm :args (@t9 @t1))
% 1.51/1.76  (step @p12 :rule cong :premises (@p11) :args (@t11))
% 1.51/1.76  (step @p13 :rule eq_resolve :premises (@p3 @p12))
% 1.51/1.76  (step @p14 :rule instantiate :premises (@p13) :args (@t27))
% 1.51/1.76  (step @p15 :rule instantiate :premises (@p13) :args (@t28))
% 1.51/1.76  (step @p16 :rule instantiate :premises (@p13) :args (@t29))
% 1.51/1.76  (step @p17 :rule eq-symm :args (@t13 @t1))
% 1.51/1.76  (step @p18 :rule cong :premises (@p17) :args (@t14))
% 1.51/1.76  (step @p19 :rule eq_resolve :premises (@p4 @p18))
% 1.51/1.76  (step @p20 :rule instantiate :premises (@p19) :args (@t30))
% 1.51/1.76  (step @p21 :rule instantiate :premises (@p19) :args (@t31))
% 1.51/1.76  (step @p22 :rule instantiate :premises (@p5) :args (@t30))
% 1.51/1.76  (step @p23 :rule instantiate :premises (@p5) :args (@t31))
% 1.51/1.76  (step @p24 :rule instantiate :premises (@p6) :args (@t27))
% 1.51/1.76  (step @p25 :rule instantiate :premises (@p6) :args (@t28))
% 1.51/1.76  (step @p26 :rule instantiate :premises (@p6) :args (@t29))
% 1.51/1.76  (step @p27 :rule instantiate :premises (@p13) :args (@t32))
% 1.51/1.76  (step @p28 :rule instantiate :premises (@p13) :args (@t33))
% 1.51/1.76  (step @p29 :rule instantiate :premises (@p13) :args (@t34))
% 1.51/1.76  (step @p30 :rule instantiate :premises (@p13) :args (@t35))
% 1.51/1.76  (step @p31 :rule instantiate :premises (@p13) :args (@t36))
% 1.51/1.76  (step @p32 :rule instantiate :premises (@p19) :args (@t37))
% 1.51/1.76  (step @p33 :rule instantiate :premises (@p19) :args (@t38))
% 1.51/1.76  (step @p34 :rule instantiate :premises (@p19) :args ((@list @t21 @t22)))
% 1.51/1.76  (step @p35 :rule instantiate :premises (@p5) :args (@t37))
% 1.51/1.76  (step @p36 :rule instantiate :premises (@p5) :args (@t39))
% 1.51/1.76  (step @p37 :rule instantiate :premises (@p5) :args (@t40))
% 1.51/1.76  (step @p38 :rule instantiate :premises (@p6) :args (@t33))
% 1.51/1.76  (step @p39 :rule instantiate :premises (@p6) :args (@t36))
% 1.51/1.76  (step @p40 :rule instantiate :premises (@p7) :args ((@list tptp.a @t25 @t21)))
% 1.51/1.76  (step @p41 :rule instantiate :premises (@p7) :args ((@list tptp.a @t25 @t25)))
% 1.51/1.76  (step @p42 :rule instantiate :premises (@p8) :args ((@list tptp.b @t24 @t24)))
% 1.51/1.76  (step @p43 :rule instantiate :premises (@p8) :args ((@list tptp.a tptp.b @t23)))
% 1.51/1.76  (step @p44 :rule instantiate :premises (@p8) :args ((@list tptp.b @t24 tptp.a)))
% 1.51/1.76  (step @p45 :rule instantiate :premises (@p8) :args ((@list tptp.a tptp.b @t24)))
% 1.51/1.76  (step @p46 :rule instantiate :premises (@p9) :args ((@list tptp.a @t22 tptp.c)))
% 1.51/1.76  (step @p47 :rule eq-symm :args (@t2 @t1))
% 1.51/1.76  (step @p48 :rule cong :premises (@p47) :args (@t4))
% 1.51/1.76  (step @p49 :rule eq_resolve :premises (@p1 @p48))
% 1.51/1.76  (step @p50 :rule instantiate :premises (@p49) :args ((@list @t25)))
% 1.51/1.76  (step @p51 :rule eq-symm :args (@t5 @t1))
% 1.51/1.76  (step @p52 :rule cong :premises (@p51) :args (@t6))
% 1.51/1.76  (step @p53 :rule eq_resolve :premises (@p2 @p52))
% 1.51/1.76  (step @p54 :rule instantiate :premises (@p53) :args ((@list @t24)))
% 1.51/1.76  (step @p55 :rule instantiate :premises (@p13) :args ((@list tptp.a @t41)))
% 1.51/1.76  (step @p56 :rule instantiate :premises (@p13) :args (@t40))
% 1.51/1.76  (step @p57 :rule instantiate :premises (@p13) :args (@t43))
% 1.51/1.76  (step @p58 :rule instantiate :premises (@p13) :args ((@list @t24 tptp.b)))
% 1.51/1.76  (step @p59 :rule instantiate :premises (@p13) :args (@t45))
% 1.51/1.76  (step @p60 :rule instantiate :premises (@p13) :args ((@list @t23 @t22)))
% 1.51/1.76  (step @p61 :rule instantiate :premises (@p13) :args (@t48))
% 1.51/1.76  (step @p62 :rule instantiate :premises (@p19) :args ((@list tptp.b @t49)))
% 1.51/1.76  (step @p63 :rule instantiate :premises (@p19) :args (@t34))
% 1.51/1.76  (step @p64 :rule instantiate :premises (@p19) :args (@t51))
% 1.51/1.76  (step @p65 :rule instantiate :premises (@p19) :args ((@list @t25 tptp.a)))
% 1.51/1.76  (step @p66 :rule instantiate :premises (@p19) :args ((@list @t22 tptp.a)))
% 1.51/1.76  (step @p67 :rule instantiate :premises (@p19) :args ((@list @t22 @t52)))
% 1.51/1.76  (step @p68 :rule instantiate :premises (@p19) :args ((@list @t21 tptp.a)))
% 1.51/1.76  (step @p69 :rule instantiate :premises (@p19) :args (@t53))
% 1.51/1.76  (step @p70 :rule instantiate :premises (@p19) :args (@t55))
% 1.51/1.76  (step @p71 :rule instantiate :premises (@p5) :args (@t57))
% 1.51/1.76  (step @p72 :rule instantiate :premises (@p5) :args (@t32))
% 1.51/1.76  (step @p73 :rule instantiate :premises (@p5) :args (@t59))
% 1.51/1.76  (step @p74 :rule instantiate :premises (@p5) :args (@t34))
% 1.51/1.76  (step @p75 :rule instantiate :premises (@p5) :args (@t51))
% 1.51/1.76  (step @p76 :rule instantiate :premises (@p5) :args ((@list @t24 @t60)))
% 1.51/1.76  (step @p77 :rule instantiate :premises (@p5) :args ((@list @t25 @t22)))
% 1.51/1.76  (step @p78 :rule instantiate :premises (@p5) :args (@t53))
% 1.51/1.76  (step @p79 :rule instantiate :premises (@p5) :args (@t55))
% 1.51/1.76  (step @p80 :rule instantiate :premises (@p5) :args ((@list @t62 @t50)))
% 1.51/1.76  (step @p81 :rule instantiate :premises (@p6) :args (@t39))
% 1.51/1.76  (step @p82 :rule instantiate :premises (@p6) :args (@t40))
% 1.51/1.76  (step @p83 :rule instantiate :premises (@p6) :args ((@list tptp.a @t63)))
% 1.51/1.76  (step @p84 :rule instantiate :premises (@p6) :args ((@list tptp.b @t60)))
% 1.51/1.76  (step @p85 :rule instantiate :premises (@p6) :args ((@list tptp.b @t23)))
% 1.51/1.76  (step @p86 :rule instantiate :premises (@p6) :args (@t43))
% 1.51/1.76  (step @p87 :rule instantiate :premises (@p6) :args ((@list @t22 @t24)))
% 1.51/1.76  (step @p88 :rule instantiate :premises (@p6) :args (@t45))
% 1.51/1.76  (step @p89 :rule instantiate :premises (@p6) :args ((@list @t67 @t64)))
% 1.51/1.76  (step @p90 :rule instantiate :premises (@p6) :args (@t48))
% 1.51/1.76  (step @p91 :rule instantiate :premises (@p6) :args ((@list @t61 @t22)))
% 1.51/1.76  (step @p92 :rule instantiate :premises (@p7) :args ((@list @t22 @t52 @t21)))
% 1.51/1.76  (step @p93 :rule instantiate :premises (@p7) :args ((@list tptp.b @t49 tptp.c)))
% 1.51/1.76  (step @p94 :rule instantiate :premises (@p7) :args ((@list tptp.c @t50 tptp.b)))
% 1.51/1.76  (step @p95 :rule instantiate :premises (@p7) :args ((@list tptp.b tptp.c @t60)))
% 1.51/1.76  (step @p96 :rule instantiate :premises (@p7) :args ((@list tptp.b tptp.c @t50)))
% 1.51/1.76  (step @p97 :rule instantiate :premises (@p7) :args ((@list @t22 @t21 tptp.a)))
% 1.51/1.76  (step @p98 :rule instantiate :premises (@p7) :args ((@list @t46 tptp.b @t49)))
% 1.51/1.76  (step @p99 :rule instantiate :premises (@p7) :args ((@list tptp.b tptp.a @t68)))
% 1.51/1.76  (step @p100 :rule instantiate :premises (@p7) :args ((@list @t54 tptp.c @t50)))
% 1.51/1.76  (step @p101 :rule instantiate :premises (@p8) :args ((@list tptp.a @t41 @t24)))
% 1.51/1.76  (step @p102 :rule instantiate :premises (@p8) :args ((@list tptp.a tptp.c @t42)))
% 1.51/1.76  (step @p103 :rule eq-symm :args (@t70 @t71))
% 1.51/1.76  (step @p104 :rule refl :args (@t20))
% 1.51/1.76  (step @p105 :rule cong :premises (@p104 @p103) :args ((=> @t20 @t72)))
% 1.51/1.76  (assume-push @p1902 @t20)
% 1.51/1.76  (step @p107 :rule instantiate :premises (@p8) :args (@t73))
% 1.51/1.76  (step-pop @p1903 :rule scope :premises (@p107))
% 1.51/1.76  (step @p108 :rule process_scope :premises (@p1903) :args (@t72))
% 1.51/1.76  (step @p110 :rule eq_resolve :premises (@p108 @p105))
% 1.51/1.76  (step @p111 :rule implies_elim :premises (@p110))
% 1.51/1.76  (step @p112 :rule chain_m_resolution :premises (@p111 @p8) :args (@t74 @t75 @t76))
% 1.51/1.76  (step @p113 :rule eq-symm :args (@t78 @t79))
% 1.51/1.76  (step @p114 :rule cong :premises (@p104 @p113) :args ((=> @t20 @t80)))
% 1.51/1.76  (assume-push @p1904 @t20)
% 1.51/1.76  (step @p116 :rule instantiate :premises (@p8) :args (@t81))
% 1.51/1.76  (step-pop @p1905 :rule scope :premises (@p116))
% 1.51/1.76  (step @p117 :rule process_scope :premises (@p1905) :args (@t80))
% 1.51/1.76  (step @p119 :rule eq_resolve :premises (@p117 @p114))
% 1.51/1.76  (step @p120 :rule implies_elim :premises (@p119))
% 1.51/1.76  (step @p121 :rule chain_m_resolution :premises (@p120 @p8) :args (@t82 @t75 @t76))
% 1.51/1.76  (step @p122 :rule eq-symm :args (@t84 @t62))
% 1.51/1.76  (step @p123 :rule cong :premises (@p104 @p122) :args ((=> @t20 @t85)))
% 1.51/1.76  (assume-push @p1906 @t20)
% 1.51/1.76  (step @p125 :rule instantiate :premises (@p8) :args (@t86))
% 1.51/1.76  (step-pop @p1907 :rule scope :premises (@p125))
% 1.51/1.76  (step @p126 :rule process_scope :premises (@p1907) :args (@t85))
% 1.51/1.76  (step @p128 :rule eq_resolve :premises (@p126 @p123))
% 1.51/1.76  (step @p129 :rule implies_elim :premises (@p128))
% 1.51/1.76  (step @p130 :rule chain_m_resolution :premises (@p129 @p8) :args (@t87 @t75 @t76))
% 1.51/1.76  (step @p131 :rule instantiate :premises (@p9) :args ((@list tptp.b @t58 @t88)))
% 1.51/1.76  (step @p132 :rule instantiate :premises (@p9) :args ((@list tptp.a @t52 tptp.b)))
% 1.51/1.76  (step @p133 :rule instantiate :premises (@p9) :args ((@list @t21 tptp.a @t24)))
% 1.51/1.76  (step @p134 :rule instantiate :premises (@p9) :args ((@list tptp.a @t21 @t24)))
% 1.51/1.76  (step @p135 :rule instantiate :premises (@p9) :args ((@list tptp.a @t56 @t41)))
% 1.51/1.76  (step @p136 :rule instantiate :premises (@p9) :args ((@list @t22 @t24 tptp.a)))
% 1.51/1.76  (step @p137 :rule instantiate :premises (@p9) :args ((@list @t24 tptp.b tptp.c)))
% 1.51/1.76  (step @p138 :rule instantiate :premises (@p9) :args ((@list tptp.b @t24 tptp.c)))
% 1.51/1.76  (step @p139 :rule instantiate :premises (@p9) :args ((@list tptp.a @t63 tptp.a)))
% 1.51/1.76  (step @p140 :rule instantiate :premises (@p9) :args ((@list @t22 @t24 @t52)))
% 1.51/1.76  (step @p141 :rule instantiate :premises (@p13) :args (@t57))
% 1.51/1.76  (step @p142 :rule instantiate :premises (@p13) :args (@t30))
% 1.51/1.76  (step @p143 :rule instantiate :premises (@p13) :args (@t38))
% 1.51/1.76  (step @p144 :rule instantiate :premises (@p13) :args ((@list @t42 tptp.c)))
% 1.51/1.76  (step @p145 :rule instantiate :premises (@p13) :args ((@list @t24 @t22)))
% 1.51/1.76  (step @p146 :rule instantiate :premises (@p13) :args (@t89))
% 1.51/1.76  (step @p147 :rule instantiate :premises (@p13) :args ((@list @t44 @t21)))
% 1.51/1.76  (step @p148 :rule instantiate :premises (@p13) :args ((@list @t47 tptp.a)))
% 1.51/1.76  (step @p149 :rule instantiate :premises (@p13) :args (@t90))
% 1.51/1.76  (step @p150 :rule instantiate :premises (@p13) :args ((@list @t94 @t91)))
% 1.51/1.76  (step @p151 :rule instantiate :premises (@p13) :args ((@list @t95 @t50)))
% 1.51/1.76  (step @p152 :rule instantiate :premises (@p13) :args ((@list @t99 @t96)))
% 1.51/1.76  (step @p153 :rule instantiate :premises (@p13) :args ((@list @t103 @t100)))
% 1.51/1.76  (step @p154 :rule instantiate :premises (@p19) :args (@t28))
% 1.51/1.76  (step @p155 :rule instantiate :premises (@p19) :args ((@list tptp.b @t46)))
% 1.51/1.76  (step @p156 :rule instantiate :premises (@p19) :args (@t35))
% 1.51/1.76  (step @p157 :rule instantiate :premises (@p19) :args ((@list @t60 @t24)))
% 1.51/1.76  (step @p158 :rule instantiate :premises (@p19) :args ((@list @t58 tptp.b)))
% 1.51/1.76  (step @p159 :rule instantiate :premises (@p19) :args ((@list @t50 tptp.c)))
% 1.51/1.76  (step @p160 :rule instantiate :premises (@p19) :args ((@list @t21 @t104)))
% 1.51/1.76  (step @p161 :rule instantiate :premises (@p19) :args ((@list @t23 tptp.a)))
% 1.51/1.76  (step @p162 :rule instantiate :premises (@p19) :args (@t106))
% 1.51/1.76  (step @p163 :rule instantiate :premises (@p19) :args ((@list @t56 tptp.a)))
% 1.51/1.76  (step @p164 :rule instantiate :premises (@p19) :args ((@list @t110 @t107)))
% 1.51/1.76  (step @p165 :rule instantiate :premises (@p19) :args (@t112))
% 1.51/1.76  (step @p166 :rule eq-symm :args (@t113 @t114))
% 1.51/1.76  (step @p167 :rule refl :args (@t15))
% 1.51/1.76  (step @p168 :rule cong :premises (@p167 @p166) :args ((=> @t15 @t115)))
% 1.51/1.76  (assume-push @p1908 @t15)
% 1.51/1.76  (step @p170 :rule instantiate :premises (@p5) :args (@t116))
% 1.51/1.76  (step-pop @p1909 :rule scope :premises (@p170))
% 1.51/1.76  (step @p171 :rule process_scope :premises (@p1909) :args (@t115))
% 1.51/1.76  (step @p173 :rule eq_resolve :premises (@p171 @p168))
% 1.51/1.76  (step @p174 :rule implies_elim :premises (@p173))
% 1.51/1.76  (step @p175 :rule chain_m_resolution :premises (@p174 @p5) :args (@t117 @t75 @t118))
% 1.51/1.76  (step @p176 :rule eq-symm :args (@t95 @t119))
% 1.51/1.76  (step @p177 :rule cong :premises (@p167 @p176) :args ((=> @t15 @t120)))
% 1.51/1.76  (assume-push @p1910 @t15)
% 1.51/1.76  (step @p179 :rule instantiate :premises (@p5) :args (@t43))
% 1.51/1.76  (step-pop @p1911 :rule scope :premises (@p179))
% 1.51/1.76  (step @p180 :rule process_scope :premises (@p1911) :args (@t120))
% 1.51/1.76  (step @p182 :rule eq_resolve :premises (@p180 @p177))
% 1.51/1.76  (step @p183 :rule implies_elim :premises (@p182))
% 1.51/1.76  (step @p184 :rule chain_m_resolution :premises (@p183 @p5) :args (@t121 @t75 @t118))
% 1.51/1.76  (step @p185 :rule instantiate :premises (@p5) :args ((@list tptp.c @t60)))
% 1.51/1.76  (step @p186 :rule instantiate :premises (@p5) :args ((@list @t24 @t50)))
% 1.51/1.76  (step @p187 :rule instantiate :premises (@p5) :args ((@list @t68 @t56)))
% 1.51/1.76  (step @p188 :rule instantiate :premises (@p5) :args ((@list @t54 @t24)))
% 1.51/1.76  (step @p189 :rule instantiate :premises (@p5) :args ((@list @t21 @t23)))
% 1.51/1.76  (step @p190 :rule instantiate :premises (@p5) :args ((@list @t47 @t49)))
% 1.51/1.76  (step @p191 :rule instantiate :premises (@p5) :args ((@list @t47 @t79)))
% 1.51/1.76  (step @p192 :rule instantiate :premises (@p5) :args ((@list @t122 @t68)))
% 1.51/1.76  (step @p193 :rule instantiate :premises (@p5) :args (@t106))
% 1.51/1.76  (step @p194 :rule instantiate :premises (@p5) :args ((@list @t123 @t88)))
% 1.51/1.76  (step @p195 :rule instantiate :premises (@p5) :args ((@list @t124 @t58)))
% 1.51/1.76  (step @p196 :rule instantiate :premises (@p5) :args ((@list @t128 @t125)))
% 1.51/1.76  (step @p197 :rule instantiate :premises (@p5) :args ((@list @t108 @t41)))
% 1.51/1.76  (step @p198 :rule instantiate :premises (@p5) :args (@t112))
% 1.51/1.76  (step @p199 :rule eq-symm :args (@t129 @t69))
% 1.51/1.76  (step @p200 :rule refl :args (@t16))
% 1.51/1.76  (step @p201 :rule cong :premises (@p200 @p199) :args ((=> @t16 @t130)))
% 1.51/1.76  (assume-push @p1912 @t16)
% 1.51/1.76  (step @p203 :rule instantiate :premises (@p6) :args (@t116))
% 1.51/1.76  (step-pop @p1913 :rule scope :premises (@p203))
% 1.51/1.76  (step @p204 :rule process_scope :premises (@p1913) :args (@t130))
% 1.51/1.76  (step @p206 :rule eq_resolve :premises (@p204 @p201))
% 1.51/1.76  (step @p207 :rule implies_elim :premises (@p206))
% 1.51/1.76  (step @p208 :rule chain_m_resolution :premises (@p207 @p6) :args (@t131 @t75 (@list @t16)))
% 1.51/1.76  (step @p209 :rule instantiate :premises (@p6) :args ((@list @t135 @t132)))
% 1.51/1.76  (step @p210 :rule instantiate :premises (@p6) :args (@t57))
% 1.51/1.76  (step @p211 :rule instantiate :premises (@p6) :args (@t30))
% 1.51/1.76  (step @p212 :rule instantiate :premises (@p6) :args (@t59))
% 1.51/1.76  (step @p213 :rule instantiate :premises (@p6) :args (@t51))
% 1.51/1.76  (step @p214 :rule instantiate :premises (@p6) :args ((@list @t88 @t60)))
% 1.51/1.76  (step @p215 :rule instantiate :premises (@p6) :args ((@list @t24 @t21)))
% 1.51/1.76  (step @p216 :rule instantiate :premises (@p6) :args ((@list @t24 @t23)))
% 1.51/1.76  (step @p217 :rule instantiate :premises (@p6) :args ((@list @t136 @t122)))
% 1.51/1.76  (step @p218 :rule instantiate :premises (@p6) :args ((@list @t61 tptp.a)))
% 1.51/1.76  (step @p219 :rule instantiate :premises (@p6) :args (@t90))
% 1.51/1.76  (step @p220 :rule instantiate :premises (@p7) :args ((@list @t24 @t50 @t137)))
% 1.51/1.76  (step @p221 :rule instantiate :premises (@p7) :args ((@list @t140 @t138 @t46)))
% 1.51/1.76  (step @p222 :rule instantiate :premises (@p7) :args ((@list tptp.c @t54 @t50)))
% 1.51/1.76  (step @p223 :rule instantiate :premises (@p7) :args ((@list @t46 @t140 @t138)))
% 1.51/1.76  (step @p224 :rule instantiate :premises (@p7) :args ((@list @t54 @t50 tptp.c)))
% 1.51/1.76  (step @p225 :rule instantiate :premises (@p7) :args ((@list tptp.c @t110 @t107)))
% 1.51/1.76  (step @p226 :rule instantiate :premises (@p7) :args ((@list @t23 @t110 @t107)))
% 1.51/1.76  (step @p227 :rule instantiate :premises (@p8) :args ((@list tptp.c @t64 @t42)))
% 1.51/1.76  (step @p228 :rule eq-symm :args (@t141 @t142))
% 1.51/1.76  (step @p229 :rule cong :premises (@p104 @p228) :args ((=> @t20 @t143)))
% 1.51/1.76  (assume-push @p1914 @t20)
% 1.51/1.76  (step @p231 :rule instantiate :premises (@p8) :args (@t144))
% 1.51/1.76  (step-pop @p1915 :rule scope :premises (@p231))
% 1.51/1.76  (step @p232 :rule process_scope :premises (@p1915) :args (@t143))
% 1.51/1.76  (step @p234 :rule eq_resolve :premises (@p232 @p229))
% 1.51/1.76  (step @p235 :rule implies_elim :premises (@p234))
% 1.51/1.76  (step @p236 :rule chain_m_resolution :premises (@p235 @p8) :args (@t145 @t75 @t76))
% 1.51/1.76  (step @p237 :rule instantiate :premises (@p8) :args ((@list tptp.b tptp.c @t146)))
% 1.51/1.76  (step @p238 :rule instantiate :premises (@p9) :args ((@list @t24 @t46 tptp.b)))
% 1.51/1.76  (step @p239 :rule instantiate :premises (@p9) :args ((@list tptp.c @t147 tptp.c)))
% 1.51/1.76  (step @p240 :rule instantiate :premises (@p9) :args ((@list tptp.b @t148 tptp.b)))
% 1.51/1.76  (step @p241 :rule instantiate :premises (@p9) :args ((@list tptp.c tptp.a @t67)))
% 1.51/1.76  (step @p242 :rule instantiate :premises (@p9) :args ((@list @t83 tptp.b tptp.a)))
% 1.51/1.76  (step @p243 :rule instantiate :premises (@p9) :args ((@list @t103 @t22 @t21)))
% 1.51/1.76  (step @p244 :rule instantiate :premises (@p9) :args ((@list @t47 @t21 tptp.b)))
% 1.51/1.76  (step @p245 :rule instantiate :premises (@p9) :args ((@list tptp.c tptp.a tptp.b)))
% 1.51/1.76  (step @p246 :rule instantiate :premises (@p9) :args ((@list tptp.c tptp.a @t24)))
% 1.51/1.76  (step @p247 :rule instantiate :premises (@p9) :args ((@list @t46 @t132 tptp.a)))
% 1.51/1.76  (step @p248 :rule instantiate :premises (@p9) :args ((@list @t47 @t21 @t24)))
% 1.51/1.76  (step @p249 :rule instantiate :premises (@p9) :args ((@list @t101 @t65 @t24)))
% 1.51/1.76  (step @p250 :rule instantiate :premises (@p9) :args ((@list @t64 @t23 tptp.a)))
% 1.51/1.76  (step @p251 :rule instantiate :premises (@p13) :args ((@list tptp.b @t148)))
% 1.51/1.76  (step @p252 :rule instantiate :premises (@p13) :args (@t149))
% 1.51/1.76  (step @p253 :rule instantiate :premises (@p13) :args ((@list @t150 tptp.c)))
% 1.51/1.76  (step @p254 :rule instantiate :premises (@p13) :args ((@list @t122 @t136)))
% 1.51/1.76  (step @p255 :rule instantiate :premises (@p19) :args (@t89))
% 1.51/1.76  (step @p256 :rule instantiate :premises (@p19) :args ((@list @t60 tptp.c)))
% 1.51/1.76  (step @p257 :rule instantiate :premises (@p19) :args ((@list @t68 @t122)))
% 1.51/1.76  (step @p258 :rule instantiate :premises (@p19) :args ((@list @t152 @t132)))
% 1.51/1.76  (step @p259 :rule instantiate :premises (@p19) :args (@t154))
% 1.51/1.76  (step @p260 :rule instantiate :premises (@p19) :args ((@list @t157 @t155)))
% 1.51/1.76  (step @p261 :rule instantiate :premises (@p5) :args ((@list tptp.a @t47)))
% 1.51/1.76  (step @p262 :rule instantiate :premises (@p5) :args ((@list tptp.c @t158)))
% 1.51/1.76  (step @p263 :rule instantiate :premises (@p5) :args (@t159))
% 1.51/1.76  (step @p264 :rule instantiate :premises (@p5) :args (@t90))
% 1.51/1.76  (step @p265 :rule instantiate :premises (@p5) :args (@t154))
% 1.51/1.76  (step @p266 :rule instantiate :premises (@p5) :args ((@list @t160 tptp.b)))
% 1.51/1.76  (step @p267 :rule instantiate :premises (@p5) :args ((@list @t161 tptp.c)))
% 1.51/1.76  (step @p268 :rule instantiate :premises (@p6) :args ((@list tptp.b @t162)))
% 1.51/1.76  (step @p269 :rule instantiate :premises (@p6) :args (@t149))
% 1.51/1.76  (step @p270 :rule instantiate :premises (@p6) :args ((@list @t119 @t147)))
% 1.51/1.76  (step @p271 :rule instantiate :premises (@p6) :args ((@list @t164 @t122)))
% 1.51/1.76  (step @p272 :rule instantiate :premises (@p6) :args (@t159))
% 1.51/1.76  (step @p273 :rule instantiate :premises (@p6) :args ((@list @t77 @t42)))
% 1.51/1.76  (step @p274 :rule instantiate :premises (@p6) :args ((@list @t166 @t25)))
% 1.51/1.76  (step @p275 :rule instantiate :premises (@p6) :args ((@list @t167 tptp.a)))
% 1.51/1.76  (step @p276 :rule instantiate :premises (@p6) :args ((@list @t169 @t168)))
% 1.51/1.76  (step @p277 :rule instantiate :premises (@p7) :args ((@list @t140 @t171 @t170)))
% 1.51/1.76  (step @p278 :rule instantiate :premises (@p7) :args ((@list @t60 @t174 @t172)))
% 1.51/1.76  (step @p279 :rule eq-symm :args (@t176 @t177))
% 1.51/1.76  (step @p280 :rule refl :args (@t19))
% 1.51/1.76  (step @p281 :rule cong :premises (@p280 @p279) :args ((=> @t19 @t178)))
% 1.51/1.76  (assume-push @p1916 @t19)
% 1.51/1.76  (step @p283 :rule instantiate :premises (@p7) :args (@t179))
% 1.51/1.76  (step-pop @p1917 :rule scope :premises (@p283))
% 1.51/1.76  (step @p284 :rule process_scope :premises (@p1917) :args (@t178))
% 1.51/1.76  (step @p286 :rule eq_resolve :premises (@p284 @p281))
% 1.51/1.76  (step @p287 :rule implies_elim :premises (@p286))
% 1.51/1.76  (step @p288 :rule chain_m_resolution :premises (@p287 @p7) :args (@t180 @t75 (@list @t19)))
% 1.51/1.76  (step @p289 :rule instantiate :premises (@p7) :args ((@list @t152 @t46 tptp.b)))
% 1.51/1.76  (step @p290 :rule instantiate :premises (@p8) :args ((@list @t181 @t175 @t42)))
% 1.51/1.76  (step @p291 :rule instantiate :premises (@p8) :args ((@list @t183 @t182 tptp.a)))
% 1.51/1.76  (step @p292 :rule instantiate :premises (@p8) :args ((@list @t183 @t182 @t25)))
% 1.51/1.76  (step @p293 :rule instantiate :premises (@p9) :args ((@list tptp.b tptp.c @t147)))
% 1.51/1.76  (step @p294 :rule instantiate :premises (@p9) :args ((@list @t184 tptp.a tptp.b)))
% 1.51/1.76  (step @p295 :rule instantiate :premises (@p9) :args ((@list tptp.a tptp.b @t25)))
% 1.51/1.76  (step @p296 :rule instantiate :premises (@p9) :args ((@list tptp.b tptp.a tptp.c)))
% 1.51/1.76  (step @p297 :rule instantiate :premises (@p9) :args ((@list @t24 @t91 @t185)))
% 1.51/1.76  (step @p298 :rule instantiate :premises (@p9) :args ((@list tptp.c @t186 @t158)))
% 1.51/1.76  (step @p299 :rule instantiate :premises (@p9) :args ((@list @t181 tptp.a tptp.c)))
% 1.51/1.76  (step @p300 :rule instantiate :premises (@p9) :args ((@list tptp.b @t147 tptp.c)))
% 1.51/1.76  (step @p301 :rule instantiate :premises (@p5) :args ((@list @t185 @t158)))
% 1.51/1.76  (step @p302 :rule instantiate :premises (@p5) :args ((@list @t150 @t187)))
% 1.51/1.76  (step @p303 :rule instantiate :premises (@p6) :args ((@list @t189 @t188)))
% 1.51/1.76  (step @p304 :rule instantiate :premises (@p7) :args ((@list @t190 @t157 @t172)))
% 1.51/1.76  (assume-push @p1918 @t191)
% 1.51/1.76  (assume-push @p1919 @t192)
% 1.51/1.76  (assume-push @p1920 @t193)
% 1.51/1.76  (assume-push @p1921 @t194)
% 1.51/1.76  (assume-push @p1922 @t195)
% 1.51/1.76  (assume-push @p1923 @t196)
% 1.51/1.76  (assume-push @p1924 @t197)
% 1.51/1.76  (assume-push @p1925 @t198)
% 1.51/1.76  (assume-push @p1926 @t199)
% 1.51/1.76  (assume-push @p1927 @t200)
% 1.51/1.76  (assume-push @p1928 @t202)
% 1.51/1.76  (assume-push @p1929 @t204)
% 1.51/1.76  (assume-push @p1930 @t205)
% 1.51/1.76  (assume-push @p1931 @t207)
% 1.51/1.76  (assume-push @p1932 @t209)
% 1.51/1.76  (assume-push @p1933 @t211)
% 1.51/1.76  (assume-push @p1934 @t213)
% 1.51/1.76  (assume-push @p1935 @t214)
% 1.51/1.76  (assume-push @p1936 @t216)
% 1.51/1.76  (assume-push @p1937 @t218)
% 1.51/1.76  (assume-push @p1938 @t219)
% 1.51/1.76  (assume-push @p1939 @t220)
% 1.51/1.76  (assume-push @p1940 @t221)
% 1.51/1.76  (assume-push @p1941 @t223)
% 1.51/1.76  (assume-push @p1942 @t226)
% 1.51/1.76  (assume-push @p1943 @t228)
% 1.51/1.76  (assume-push @p1944 @t230)
% 1.51/1.76  (assume-push @p1945 @t232)
% 1.51/1.76  (assume-push @p1946 @t234)
% 1.51/1.76  (assume-push @p1947 @t237)
% 1.51/1.76  (assume-push @p1948 @t238)
% 1.51/1.76  (assume-push @p1949 @t239)
% 1.51/1.76  (assume-push @p1950 @t240)
% 1.51/1.76  (assume-push @p1951 @t241)
% 1.51/1.76  (assume-push @p1952 @t243)
% 1.51/1.76  (assume-push @p1953 @t245)
% 1.51/1.76  (assume-push @p1954 @t247)
% 1.51/1.76  (assume-push @p1955 @t248)
% 1.51/1.76  (assume-push @p1956 @t250)
% 1.51/1.76  (assume-push @p1957 @t252)
% 1.51/1.76  (assume-push @p1958 @t254)
% 1.51/1.76  (assume-push @p1959 @t256)
% 1.51/1.76  (assume-push @p1960 @t258)
% 1.51/1.76  (assume-push @p1961 @t259)
% 1.51/1.76  (assume-push @p1962 @t260)
% 1.51/1.76  (assume-push @p1963 @t261)
% 1.51/1.76  (assume-push @p1964 @t263)
% 1.51/1.76  (assume-push @p1965 @t265)
% 1.51/1.76  (assume-push @p1966 @t267)
% 1.51/1.76  (assume-push @p1967 @t269)
% 1.51/1.76  (assume-push @p1968 @t271)
% 1.51/1.76  (assume-push @p1969 @t273)
% 1.51/1.76  (assume-push @p1970 @t275)
% 1.51/1.76  (assume-push @p1971 @t277)
% 1.51/1.76  (assume-push @p1972 @t279)
% 1.51/1.76  (assume-push @p1973 @t280)
% 1.51/1.76  (assume-push @p1974 @t282)
% 1.51/1.76  (assume-push @p1975 @t283)
% 1.51/1.76  (assume-push @p1976 @t285)
% 1.51/1.76  (assume-push @p1977 @t286)
% 1.51/1.76  (assume-push @p1978 @t288)
% 1.51/1.76  (assume-push @p1979 @t290)
% 1.51/1.76  (assume-push @p1980 @t292)
% 1.51/1.76  (assume-push @p1981 @t294)
% 1.51/1.76  (assume-push @p1982 @t296)
% 1.51/1.76  (assume-push @p1983 @t297)
% 1.51/1.76  (assume-push @p1984 @t299)
% 1.51/1.76  (assume-push @p1985 @t300)
% 1.51/1.76  (assume-push @p1986 @t301)
% 1.51/1.76  (assume-push @p1987 @t303)
% 1.51/1.76  (assume-push @p1988 @t306)
% 1.51/1.76  (assume-push @p1989 @t309)
% 1.51/1.76  (assume-push @p1990 @t311)
% 1.51/1.76  (assume-push @p1991 @t313)
% 1.51/1.76  (assume-push @p1992 @t314)
% 1.51/1.76  (assume-push @p1993 @t317)
% 1.51/1.76  (assume-push @p1994 @t319)
% 1.51/1.76  (assume-push @p1995 @t321)
% 1.51/1.76  (assume-push @p1996 @t324)
% 1.51/1.76  (assume-push @p1997 @t327)
% 1.51/1.76  (assume-push @p1998 @t74)
% 1.51/1.76  (assume-push @p1999 @t82)
% 1.51/1.76  (assume-push @p2000 @t87)
% 1.51/1.76  (assume-push @p2001 @t330)
% 1.51/1.76  (assume-push @p2002 @t333)
% 1.51/1.76  (assume-push @p2003 @t339)
% 1.51/1.76  (assume-push @p2004 @t343)
% 1.51/1.76  (assume-push @p2005 @t349)
% 1.51/1.76  (assume-push @p2006 @t353)
% 1.51/1.76  (assume-push @p2007 @t359)
% 1.51/1.76  (assume-push @p2008 @t365)
% 1.51/1.76  (assume-push @p2009 @t371)
% 1.51/1.76  (assume-push @p2010 @t377)
% 1.51/1.76  (assume-push @p2011 @t378)
% 1.51/1.76  (assume-push @p2012 @t380)
% 1.51/1.76  (assume-push @p2013 @t382)
% 1.51/1.76  (assume-push @p2014 @t383)
% 1.51/1.76  (assume-push @p2015 @t384)
% 1.51/1.76  (assume-push @p2016 @t385)
% 1.51/1.76  (assume-push @p2017 @t386)
% 1.51/1.76  (assume-push @p2018 @t388)
% 1.51/1.76  (assume-push @p2019 @t389)
% 1.51/1.76  (assume-push @p2020 @t390)
% 1.51/1.76  (assume-push @p2021 @t392)
% 1.51/1.76  (assume-push @p2022 @t393)
% 1.51/1.76  (assume-push @p2023 @t395)
% 1.51/1.76  (assume-push @p2024 @t396)
% 1.51/1.76  (assume-push @p2025 @t398)
% 1.51/1.76  (assume-push @p2026 @t400)
% 1.51/1.76  (assume-push @p2027 @t401)
% 1.51/1.76  (assume-push @p2028 @t402)
% 1.51/1.76  (assume-push @p2029 @t403)
% 1.51/1.76  (assume-push @p2030 @t404)
% 1.51/1.76  (assume-push @p2031 @t405)
% 1.51/1.76  (assume-push @p2032 @t407)
% 1.51/1.76  (assume-push @p2033 @t408)
% 1.51/1.76  (assume-push @p2034 @t409)
% 1.51/1.76  (assume-push @p2035 @t411)
% 1.51/1.76  (assume-push @p2036 @t117)
% 1.51/1.76  (assume-push @p2037 @t121)
% 1.51/1.76  (assume-push @p2038 @t413)
% 1.51/1.76  (assume-push @p2039 @t415)
% 1.51/1.76  (assume-push @p2040 @t418)
% 1.51/1.76  (assume-push @p2041 @t421)
% 1.51/1.76  (assume-push @p2042 @t423)
% 1.51/1.76  (assume-push @p2043 @t425)
% 1.51/1.76  (assume-push @p2044 @t426)
% 1.51/1.76  (assume-push @p2045 @t428)
% 1.51/1.76  (assume-push @p2046 @t429)
% 1.51/1.76  (assume-push @p2047 @t431)
% 1.51/1.76  (assume-push @p2048 @t432)
% 1.51/1.76  (assume-push @p2049 @t434)
% 1.51/1.76  (assume-push @p2050 @t436)
% 1.51/1.76  (assume-push @p2051 @t437)
% 1.51/1.76  (assume-push @p2052 @t131)
% 1.51/1.76  (assume-push @p2053 @t439)
% 1.51/1.76  (assume-push @p2054 @t441)
% 1.51/1.76  (assume-push @p2055 @t442)
% 1.51/1.76  (assume-push @p2056 @t444)
% 1.51/1.76  (assume-push @p2057 @t446)
% 1.51/1.76  (assume-push @p2058 @t448)
% 1.51/1.76  (assume-push @p2059 @t449)
% 1.51/1.76  (assume-push @p2060 @t451)
% 1.51/1.76  (assume-push @p2061 @t453)
% 1.51/1.76  (assume-push @p2062 @t455)
% 1.51/1.76  (assume-push @p2063 @t457)
% 1.51/1.76  (assume-push @p2064 @t459)
% 1.51/1.76  (assume-push @p2065 @t461)
% 1.51/1.76  (assume-push @p2066 @t463)
% 1.51/1.76  (assume-push @p2067 @t466)
% 1.51/1.76  (assume-push @p2068 @t468)
% 1.51/1.76  (assume-push @p2069 @t470)
% 1.51/1.76  (assume-push @p2070 @t473)
% 1.51/1.76  (assume-push @p2071 @t476)
% 1.51/1.76  (assume-push @p2072 @t145)
% 1.51/1.76  (assume-push @p2073 @t478)
% 1.51/1.76  (assume-push @p2074 @t484)
% 1.51/1.76  (assume-push @p2075 @t486)
% 1.51/1.76  (assume-push @p2076 @t488)
% 1.51/1.76  (assume-push @p2077 @t493)
% 1.51/1.76  (assume-push @p2078 @t499)
% 1.51/1.76  (assume-push @p2079 @t505)
% 1.51/1.76  (assume-push @p2080 @t513)
% 1.51/1.76  (assume-push @p2081 @t518)
% 1.51/1.76  (assume-push @p2082 @t523)
% 1.51/1.76  (assume-push @p2083 @t530)
% 1.51/1.76  (assume-push @p2084 @t536)
% 1.51/1.76  (assume-push @p2085 @t543)
% 1.51/1.76  (assume-push @p2086 @t550)
% 1.51/1.76  (assume-push @p2087 @t552)
% 1.51/1.76  (assume-push @p2088 @t554)
% 1.51/1.76  (assume-push @p2089 @t556)
% 1.51/1.76  (assume-push @p2090 @t557)
% 1.51/1.76  (assume-push @p2091 @t560)
% 1.51/1.76  (assume-push @p2092 @t562)
% 1.51/1.76  (assume-push @p2093 @t563)
% 1.51/1.76  (assume-push @p2094 @t564)
% 1.51/1.76  (assume-push @p2095 @t565)
% 1.51/1.76  (assume-push @p2096 @t566)
% 1.51/1.76  (assume-push @p2097 @t568)
% 1.51/1.76  (assume-push @p2098 @t570)
% 1.51/1.76  (assume-push @p2099 @t572)
% 1.51/1.76  (assume-push @p2100 @t574)
% 1.51/1.76  (assume-push @p2101 @t576)
% 1.51/1.76  (assume-push @p2102 @t577)
% 1.51/1.76  (assume-push @p2103 @t579)
% 1.51/1.76  (assume-push @p2104 @t581)
% 1.51/1.76  (assume-push @p2105 @t583)
% 1.51/1.76  (assume-push @p2106 @t585)
% 1.51/1.76  (assume-push @p2107 @t587)
% 1.51/1.76  (assume-push @p2108 @t589)
% 1.51/1.76  (assume-push @p2109 @t591)
% 1.51/1.76  (assume-push @p2110 @t593)
% 1.51/1.76  (assume-push @p2111 @t595)
% 1.51/1.76  (assume-push @p2112 @t596)
% 1.51/1.76  (assume-push @p2113 @t598)
% 1.51/1.76  (assume-push @p2114 @t601)
% 1.51/1.76  (assume-push @p2115 @t180)
% 1.51/1.76  (assume-push @p2116 @t604)
% 1.51/1.76  (assume-push @p2117 @t606)
% 1.51/1.76  (assume-push @p2118 @t608)
% 1.51/1.76  (assume-push @p2119 @t611)
% 1.51/1.76  (assume-push @p2120 @t618)
% 1.51/1.76  (assume-push @p2121 @t624)
% 1.51/1.76  (assume-push @p2122 @t628)
% 1.51/1.76  (assume-push @p2123 @t632)
% 1.51/1.76  (assume-push @p2124 @t638)
% 1.51/1.76  (assume-push @p2125 @t644)
% 1.51/1.76  (assume-push @p2126 @t650)
% 1.51/1.76  (assume-push @p2127 @t656)
% 1.51/1.76  (assume-push @p2128 @t658)
% 1.51/1.76  (assume-push @p2129 @t660)
% 1.51/1.76  (assume-push @p2130 @t662)
% 1.51/1.76  (assume-push @p2131 @t665)
% 1.51/1.76  (step @p519 :rule symm :premises (@p33))
% 1.51/1.76  (step @p520 :rule refl :args (tptp.a))
% 1.51/1.76  (step @p521 :rule cong :premises (@p520 @p519) :args (@t325))
% 1.51/1.76  (step @p522 :rule symm :premises (@p145))
% 1.51/1.76  (step @p523 :rule symm :premises (@p45))
% 1.51/1.76  (step @p524 :rule cong :premises (@p520 @p20) :args (@t22))
% 1.51/1.76  (step @p525 :rule symm :premises (@p66))
% 1.51/1.76  (step @p526 :rule trans :premises (@p14 @p36))
% 1.51/1.76  (step @p527 :rule refl :args (@t22))
% 1.51/1.76  (step @p528 :rule cong :premises (@p527 @p526) :args (@t284))
% 1.51/1.76  (step @p529 :rule trans :premises (@p81 @p528 @p525 @p524 @p523 @p87))
% 1.51/1.76  (step @p530 :rule refl :args (@t24))
% 1.51/1.76  (step @p531 :rule cong :premises (@p530 @p529) :args (@t419))
% 1.51/1.76  (step @p532 :rule symm :premises (@p14))
% 1.51/1.76  (step @p533 :rule symm :premises (@p36))
% 1.51/1.76  (step @p534 :rule symm :premises (@p21))
% 1.51/1.76  (step @p535 :rule symm :premises (@p39))
% 1.51/1.76  (step @p536 :rule trans :premises (@p535 @p534))
% 1.51/1.76  (step @p537 :rule cong :premises (@p536 @p520) :args (@t666))
% 1.51/1.76  (step @p538 :rule trans :premises (@p537 @p533 @p532))
% 1.51/1.76  (step @p539 :rule cong :premises (@p538 @p527) :args ((tptp.join @t666 @t22)))
% 1.51/1.76  (step @p540 :rule symm :premises (@p539))
% 1.51/1.76  (step @p541 :rule symm :premises (@p81))
% 1.51/1.76  (step @p542 :rule symm :premises (@p528))
% 1.51/1.76  (step @p543 :rule trans :premises (@p66 @p542 @p541 @p540))
% 1.51/1.76  (step @p544 :rule trans :premises (@p543 @p539))
% 1.51/1.76  (step @p545 :rule cong :premises (@p544 @p530) :args (@t101))
% 1.51/1.76  (step @p546 :rule symm :premises (@p524))
% 1.51/1.76  (step @p547 :rule symm :premises (@p87))
% 1.51/1.76  (step @p548 :rule trans :premises (@p188 @p531 @p522))
% 1.51/1.76  (step @p549 :rule trans :premises (@p545 @p548))
% 1.51/1.76  (step @p550 :rule cong :premises (@p549 @p534) :args (@t102))
% 1.51/1.76  (step @p551 :rule symm :premises (@p545))
% 1.51/1.76  (step @p552 :rule cong :premises (@p551 @p21) :args ((tptp.join @t420 @t22)))
% 1.51/1.76  (step @p553 :rule trans :premises (@p552 @p550 @p547 @p45 @p546))
% 1.51/1.76  (step @p554 :rule symm :premises (@p552))
% 1.51/1.76  (step @p555 :rule trans :premises (@p554 @p553))
% 1.51/1.76  (step @p556 :rule cong :premises (@p555 @p530) :args (@t103))
% 1.51/1.76  (step @p557 :rule trans :premises (@p556 @p545 @p188 @p531 @p522 @p22))
% 1.51/1.76  (step @p558 :rule refl :args (@t21))
% 1.51/1.76  (step @p559 :rule cong :premises (@p558 @p557) :args (@t500))
% 1.51/1.76  (step @p560 :rule trans :premises (@p559 @p102 @p521))
% 1.51/1.76  (step @p561 :rule symm :premises (@p31))
% 1.51/1.76  (step @p562 :rule symm :premises (@p67))
% 1.51/1.76  (step @p563 :rule cong :premises (@p534 @p31) :args (@t372))
% 1.51/1.76  (step @p564 :rule trans :premises (@p563 @p562 @p21))
% 1.51/1.76  (step @p565 :rule refl :args (@t52))
% 1.51/1.76  (step @p566 :rule trans :premises (@p45 @p546))
% 1.51/1.76  (step @p567 :rule cong :premises (@p566 @p565) :args (@t373))
% 1.51/1.76  (step @p568 :rule trans :premises (@p567 @p561))
% 1.51/1.76  (step @p569 :rule cong :premises (@p568 @p530) :args (@t374))
% 1.51/1.76  (step @p570 :rule trans :premises (@p569 @p45 @p546))
% 1.51/1.76  (step @p571 :rule cong :premises (@p570 @p564) :args (@t375))
% 1.51/1.76  (step @p572 :rule cong :premises (@p21 @p534) :args (@t208))
% 1.51/1.76  (step @p573 :rule trans :premises (@p31 @p572))
% 1.51/1.76  (step @p574 :rule refl :args (@t103))
% 1.51/1.76  (step @p575 :rule cong :premises (@p574 @p573) :args (@t501))
% 1.51/1.76  (step @p576 :rule trans :premises (@p575 @p140 @p571 @p561))
% 1.51/1.76  (step @p577 :rule cong :premises (@p576 @p558) :args (@t502))
% 1.51/1.76  (step @p578 :rule cong :premises (@p577 @p527) :args (@t503))
% 1.51/1.76  (step @p579 :rule trans :premises (@p578 @p535 @p534))
% 1.51/1.76  (step @p580 :rule cong :premises (@p579 @p560) :args (@t504))
% 1.51/1.76  (step @p581 :rule symm :premises (@p556))
% 1.51/1.76  (step @p582 :rule symm :premises (@p188))
% 1.51/1.76  (step @p583 :rule symm :premises (@p531))
% 1.51/1.76  (step @p584 :rule trans :premises (@p145 @p583 @p582 @p551 @p581))
% 1.51/1.76  (step @p585 :rule symm :premises (@p68))
% 1.51/1.76  (step @p586 :rule trans :premises (@p15 @p37))
% 1.51/1.76  (step @p587 :rule cong :premises (@p558 @p586) :args (@t126))
% 1.51/1.76  (step @p588 :rule trans :premises (@p587 @p585))
% 1.51/1.76  (step @p589 :rule cong :premises (@p588 @p584) :args (@t127))
% 1.51/1.76  (step @p590 :rule symm :premises (@p588))
% 1.51/1.76  (step @p591 :rule symm :premises (@p25))
% 1.51/1.76  (step @p592 :rule trans :premises (@p591 @p590))
% 1.51/1.76  (step @p593 :rule cong :premises (@p592 @p530) :args (@t414))
% 1.51/1.76  (step @p594 :rule symm :premises (@p96))
% 1.51/1.76  (step @p595 :rule refl :args (tptp.b))
% 1.51/1.76  (step @p596 :rule cong :premises (@p595 @p29) :args (@t24))
% 1.51/1.76  (step @p597 :rule trans :premises (@p596 @p594 @p186 @p593 @p589))
% 1.51/1.76  (step @p598 :rule trans :premises (@p140 @p571 @p561))
% 1.51/1.76  (step @p599 :rule cong :premises (@p574 @p598) :args (@t394))
% 1.51/1.76  (step @p600 :rule symm :premises (@p572))
% 1.51/1.76  (step @p601 :rule trans :premises (@p600 @p561 @p21))
% 1.51/1.76  (step @p602 :rule cong :premises (@p551 @p601) :args (@t667))
% 1.51/1.76  (step @p603 :rule cong :premises (@p602 @p530) :args ((tptp.meet @t667 @t24)))
% 1.51/1.76  (step @p604 :rule trans :premises (@p603 @p153 @p599))
% 1.51/1.76  (step @p605 :rule symm :premises (@p603))
% 1.51/1.76  (step @p606 :rule trans :premises (@p584 @p605 @p604))
% 1.51/1.76  (step @p607 :rule cong :premises (@p606 @p558) :args (@t125))
% 1.51/1.76  (step @p608 :rule symm :premises (@p159))
% 1.51/1.76  (step @p609 :rule trans :premises (@p29 @p75))
% 1.51/1.76  (step @p610 :rule refl :args (@t50))
% 1.51/1.76  (step @p611 :rule cong :premises (@p610 @p609) :args (@t445))
% 1.51/1.76  (step @p612 :rule refl :args (tptp.c))
% 1.51/1.76  (step @p613 :rule cong :premises (@p612 @p25) :args (@t668))
% 1.51/1.76  (step @p614 :rule trans :premises (@p613 @p213 @p611 @p608 @p591))
% 1.51/1.76  (step @p615 :rule symm :premises (@p596))
% 1.51/1.76  (step @p616 :rule symm :premises (@p186))
% 1.51/1.76  (step @p617 :rule symm :premises (@p593))
% 1.51/1.76  (step @p618 :rule symm :premises (@p22))
% 1.51/1.76  (step @p619 :rule symm :premises (@p160))
% 1.51/1.76  (step @p620 :rule trans :premises (@p613 @p213 @p611 @p608 @p591 @p59))
% 1.51/1.76  (step @p621 :rule symm :premises (@p29))
% 1.51/1.76  (step @p622 :rule symm :premises (@p75))
% 1.51/1.76  (step @p623 :rule symm :premises (@p592))
% 1.51/1.76  (step @p624 :rule cong :premises (@p623 @p612) :args (@t669))
% 1.51/1.76  (step @p625 :rule trans :premises (@p624 @p622 @p621))
% 1.51/1.76  (step @p626 :rule cong :premises (@p625 @p520) :args (@t670))
% 1.51/1.76  (step @p627 :rule trans :premises (@p626 @p591))
% 1.51/1.76  (step @p628 :rule cong :premises (@p627 @p620) :args (@t671))
% 1.51/1.76  (step @p629 :rule trans :premises (@p628 @p619))
% 1.51/1.76  (step @p630 :rule trans :premises (@p629 @p590))
% 1.51/1.76  (step @p631 :rule cong :premises (@p630 @p618) :args (@t672))
% 1.51/1.76  (step @p632 :rule trans :premises (@p631 @p617 @p616 @p96 @p615))
% 1.51/1.76  (step @p633 :rule cong :premises (@p632 @p614) :args ((tptp.join @t672 @t668)))
% 1.51/1.76  (step @p634 :rule symm :premises (@p633))
% 1.51/1.76  (step @p635 :rule symm :premises (@p215))
% 1.51/1.76  (step @p636 :rule cong :premises (@p558 @p618) :args (@t326))
% 1.51/1.76  (step @p637 :rule symm :premises (@p102))
% 1.51/1.76  (step @p638 :rule symm :premises (@p521))
% 1.51/1.76  (step @p639 :rule trans :premises (@p638 @p637 @p636 @p635 @p634))
% 1.51/1.76  (step @p640 :rule trans :premises (@p639 @p633 @p607))
% 1.51/1.76  (step @p641 :rule cong :premises (@p640 @p527) :args (@t44))
% 1.51/1.76  (step @p642 :rule trans :premises (@p23 @p641))
% 1.51/1.76  (step @p643 :rule cong :premises (@p642 @p597) :args (@t450))
% 1.51/1.76  (step @p644 :rule cong :premises (@p561 @p558) :args (@t302))
% 1.51/1.76  (step @p645 :rule symm :premises (@p92))
% 1.51/1.76  (step @p646 :rule cong :premises (@p21 @p558) :args (@t23))
% 1.51/1.76  (step @p647 :rule symm :premises (@p161))
% 1.51/1.76  (step @p648 :rule symm :premises (@p97))
% 1.51/1.76  (step @p649 :rule cong :premises (@p527 @p586) :args (@t217))
% 1.51/1.76  (step @p650 :rule trans :premises (@p14 @p36 @p649 @p648))
% 1.51/1.76  (step @p651 :rule refl :args (@t23))
% 1.51/1.76  (step @p652 :rule cong :premises (@p651 @p650) :args (@t69))
% 1.51/1.76  (step @p203 :rule instantiate :premises (@p6) :args (@t116))
% 1.51/1.76  (step @p653 :rule symm :premises (@p23))
% 1.51/1.76  (step @p654 :rule symm :premises (@p147))
% 1.51/1.76  (step @p231 :rule instantiate :premises (@p8) :args (@t144))
% 1.51/1.76  (step @p655 :rule cong :premises (@p23 @p520) :args (@t69))
% 1.51/1.76  (step @p656 :rule symm :premises (@p60))
% 1.51/1.76  (step @p657 :rule symm :premises (@p536))
% 1.51/1.76  (step @p658 :rule cong :premises (@p651 @p657) :args (@t673))
% 1.51/1.76  (step @p659 :rule trans :premises (@p658 @p656))
% 1.51/1.76  (step @p660 :rule cong :premises (@p659 @p520) :args ((tptp.join @t673 tptp.a)))
% 1.51/1.76  (step @p661 :rule symm :premises (@p660))
% 1.51/1.76  (step @p662 :rule symm :premises (@p652))
% 1.51/1.76  (step @p663 :rule trans :premises (@p161 @p662 @p661))
% 1.51/1.76  (step @p664 :rule trans :premises (@p653 @p663 @p660 @p655))
% 1.51/1.76  (step @p665 :rule cong :premises (@p664 @p612) :args ((tptp.join @t44 tptp.c)))
% 1.51/1.76  (step @p666 :rule cong :premises (@p532 @p612) :args (@t66))
% 1.51/1.76  (step @p667 :rule cong :premises (@p666 @p527) :args (@t67))
% 1.51/1.76  (step @p668 :rule cong :premises (@p667 @p612) :args (@t489))
% 1.51/1.76  (step @p669 :rule trans :premises (@p668 @p665 @p231))
% 1.51/1.76  (step @p670 :rule trans :premises (@p34 @p88))
% 1.51/1.76  (step @p671 :rule cong :premises (@p23 @p670) :args (@t422))
% 1.51/1.76  (step @p672 :rule cong :premises (@p558 @p653) :args ((tptp.meet @t21 @t44)))
% 1.51/1.76  (step @p673 :rule trans :premises (@p672 @p189 @p671 @p654 @p653))
% 1.51/1.76  (step @p674 :rule symm :premises (@p672))
% 1.51/1.76  (step @p675 :rule trans :premises (@p667 @p653))
% 1.51/1.76  (step @p676 :rule cong :premises (@p591 @p675) :args (@t490))
% 1.51/1.76  (step @p677 :rule trans :premises (@p676 @p674 @p673))
% 1.51/1.76  (step @p678 :rule cong :premises (@p677 @p520) :args (@t491))
% 1.51/1.76  (step @p679 :rule trans :premises (@p678 @p652 @p647))
% 1.51/1.76  (step @p680 :rule trans :premises (@p679 @p23))
% 1.51/1.76  (step @p681 :rule cong :premises (@p680 @p669) :args (@t492))
% 1.51/1.76  (step @p682 :rule symm :premises (@p675))
% 1.51/1.76  (step @p683 :rule symm :premises (@p544))
% 1.51/1.76  (step @p684 :rule cong :premises (@p683 @p591) :args (@t190))
% 1.51/1.76  (step @p685 :rule trans :premises (@p684 @p682))
% 1.51/1.76  (step @p686 :rule cong :premises (@p685 @p612) :args (@t467))
% 1.51/1.76  (step @p687 :rule symm :premises (@p224))
% 1.51/1.76  (step @p688 :rule refl :args (@t54))
% 1.51/1.76  (step @p689 :rule cong :premises (@p688 @p75) :args (@t320))
% 1.51/1.76  (step @p690 :rule cong :premises (@p688 @p29) :args (@t61))
% 1.51/1.76  (step @p691 :rule trans :premises (@p690 @p689 @p687 @p686))
% 1.51/1.76  (step @p692 :rule symm :premises (@p46))
% 1.51/1.76  (step @p693 :rule symm :premises (@p80))
% 1.51/1.76  (step @p694 :rule symm :premises (@p91))
% 1.51/1.76  (step @p695 :rule refl :args (@t61))
% 1.51/1.76  (step @p696 :rule cong :premises (@p683 @p695) :args (@t264))
% 1.51/1.76  (step @p697 :rule trans :premises (@p66 @p542 @p541 @p70 @p696 @p694))
% 1.51/1.76  (step @p698 :rule cong :premises (@p25 @p697) :args (@t44))
% 1.51/1.76  (step @p699 :rule trans :premises (@p23 @p698 @p693 @p692 @p89))
% 1.51/1.76  (step @p700 :rule cong :premises (@p699 @p520) :args (@t114))
% 1.51/1.76  (step @p701 :rule trans :premises (@p14 @p36 @p649 @p648 @p700))
% 1.51/1.76  (step @p702 :rule cong :premises (@p701 @p691) :args (@t454))
% 1.51/1.76  (step @p703 :rule trans :premises (@p218 @p702 @p241 @p681 @p654 @p653))
% 1.51/1.76  (step @p704 :rule cong :premises (@p520 @p703) :args (@t494))
% 1.51/1.76  (step @p705 :rule trans :premises (@p704 @p203 @p652 @p647 @p646))
% 1.51/1.76  (step @p706 :rule symm :premises (@p70))
% 1.51/1.76  (step @p707 :rule symm :premises (@p696))
% 1.51/1.76  (step @p125 :rule instantiate :premises (@p8) :args (@t86))
% 1.51/1.76  (step @p708 :rule trans :premises (@p125 @p91 @p707 @p706 @p81 @p528 @p525))
% 1.51/1.76  (step @p709 :rule cong :premises (@p708 @p520) :args (@t495))
% 1.51/1.76  (step @p710 :rule trans :premises (@p709 @p533 @p532))
% 1.51/1.76  (step @p711 :rule cong :premises (@p710 @p595) :args (@t496))
% 1.51/1.76  (step @p712 :rule cong :premises (@p711 @p705) :args (@t497))
% 1.51/1.76  (step @p713 :rule symm :premises (@p276))
% 1.51/1.76  (step @p714 :rule symm :premises (@p20))
% 1.51/1.76  (step @p715 :rule symm :premises (@p38))
% 1.51/1.76  (step @p716 :rule symm :premises (@p54))
% 1.51/1.76  (step @p717 :rule cong :premises (@p716 @p595) :args (@t138))
% 1.51/1.76  (step @p718 :rule trans :premises (@p717 @p715 @p714))
% 1.51/1.76  (step @p719 :rule symm :premises (@p690))
% 1.51/1.76  (step @p720 :rule symm :premises (@p43))
% 1.51/1.76  (step @p721 :rule symm :premises (@p83))
% 1.51/1.76  (step @p722 :rule trans :premises (@p721 @p720 @p534))
% 1.51/1.76  (step @p723 :rule trans :premises (@p722 @p543 @p539))
% 1.51/1.76  (step @p724 :rule cong :premises (@p723 @p29) :args (@t674))
% 1.51/1.76  (step @p725 :rule trans :premises (@p724 @p719))
% 1.51/1.76  (step @p726 :rule cong :premises (@p725 @p520) :args ((tptp.join @t674 tptp.a)))
% 1.51/1.76  (step @p727 :rule symm :premises (@p726))
% 1.51/1.76  (step @p728 :rule symm :premises (@p218))
% 1.51/1.76  (step @p729 :rule symm :premises (@p702))
% 1.51/1.76  (step @p730 :rule symm :premises (@p241))
% 1.51/1.76  (step @p731 :rule symm :premises (@p681))
% 1.51/1.76  (step @p732 :rule trans :premises (@p23 @p147 @p731 @p730 @p729 @p728 @p727))
% 1.51/1.76  (step @p733 :rule symm :premises (@p24))
% 1.51/1.76  (step @p734 :rule symm :premises (@p158))
% 1.51/1.76  (step @p735 :rule trans :premises (@p27 @p73))
% 1.51/1.76  (step @p736 :rule refl :args (@t58))
% 1.51/1.76  (step @p737 :rule cong :premises (@p736 @p735) :args (@t443))
% 1.51/1.76  (step @p738 :rule trans :premises (@p212 @p737 @p734 @p733 @p524 @p523 @p87))
% 1.51/1.76  (step @p739 :rule cong :premises (@p716 @p738) :args (@t430))
% 1.51/1.76  (step @p740 :rule trans :premises (@p194 @p739 @p522))
% 1.51/1.76  (step @p741 :rule cong :premises (@p740 @p527) :args ((tptp.join @t139 @t22)))
% 1.51/1.76  (step @p742 :rule refl :args (@t139))
% 1.51/1.76  (step @p743 :rule cong :premises (@p742 @p733) :args (@t140))
% 1.51/1.76  (step @p744 :rule trans :premises (@p743 @p741 @p547 @p45 @p546))
% 1.51/1.76  (step @p745 :rule trans :premises (@p82 @p587 @p585))
% 1.51/1.76  (step @p746 :rule cong :premises (@p745 @p744) :args (@t464))
% 1.51/1.76  (step @p747 :rule trans :premises (@p746 @p653))
% 1.51/1.76  (step @p748 :rule trans :premises (@p747 @p732 @p726))
% 1.51/1.76  (step @p749 :rule cong :premises (@p748 @p718) :args (@t465))
% 1.51/1.76  (step @p750 :rule symm :premises (@p223))
% 1.51/1.76  (step @p751 :rule refl :args (@t329))
% 1.51/1.76  (step @p752 :rule refl :args (@t88))
% 1.51/1.76  (step @p753 :rule cong :premises (@p27 @p752) :args (@t227))
% 1.51/1.76  (step @p754 :rule cong :premises (@p20 @p530) :args (@t49))
% 1.51/1.76  (step @p755 :rule trans :premises (@p20 @p754 @p42 @p753))
% 1.51/1.76  (step @p756 :rule cong :premises (@p755 @p736) :args (@t201))
% 1.51/1.76  (step @p757 :rule trans :premises (@p27 @p756))
% 1.51/1.76  (step @p758 :rule symm :premises (@p28))
% 1.51/1.76  (step @p759 :rule refl :args (@t49))
% 1.51/1.76  (step @p760 :rule symm :premises (@p754))
% 1.51/1.76  (step @p761 :rule symm :premises (@p42))
% 1.51/1.76  (step @p762 :rule cong :premises (@p758 @p752) :args (@t675))
% 1.51/1.76  (step @p763 :rule trans :premises (@p762 @p761 @p760 @p714))
% 1.51/1.76  (step @p764 :rule cong :premises (@p763 @p759) :args (@t676))
% 1.51/1.76  (step @p765 :rule trans :premises (@p764 @p758))
% 1.51/1.76  (step @p766 :rule trans :premises (@p765 @p757))
% 1.51/1.76  (step @p767 :rule cong :premises (@p766 @p751) :args ((tptp.join @t676 @t329)))
% 1.51/1.76  (step @p768 :rule trans :premises (@p715 @p714))
% 1.51/1.76  (step @p769 :rule cong :premises (@p54 @p768) :args (@t244))
% 1.51/1.76  (step @p770 :rule trans :premises (@p58 @p769))
% 1.51/1.76  (step @p771 :rule symm :premises (@p765))
% 1.51/1.76  (step @p772 :rule cong :premises (@p771 @p770) :args (@t49))
% 1.51/1.76  (step @p773 :rule trans :premises (@p20 @p772 @p767 @p131))
% 1.51/1.76  (step @p774 :rule symm :premises (@p745))
% 1.51/1.76  (step @p775 :rule trans :premises (@p591 @p774))
% 1.51/1.76  (step @p776 :rule cong :premises (@p775 @p773) :args (@t147))
% 1.51/1.76  (step @p777 :rule symm :premises (@p775))
% 1.51/1.76  (step @p778 :rule cong :premises (@p777 @p758) :args (@t315))
% 1.51/1.76  (step @p779 :rule refl :args (@t46))
% 1.51/1.76  (step @p780 :rule cong :premises (@p779 @p28) :args (@t47))
% 1.51/1.76  (step @p781 :rule trans :premises (@p780 @p778 @p776 @p750 @p749))
% 1.51/1.76  (step @p782 :rule cong :premises (@p781 @p520) :args (@t77))
% 1.51/1.76  (step @p783 :rule symm :premises (@p780))
% 1.51/1.76  (step @p784 :rule symm :premises (@p778))
% 1.51/1.76  (step @p785 :rule cong :premises (@p623 @p595) :args (@t677))
% 1.51/1.76  (step @p786 :rule trans :premises (@p785 @p784 @p783))
% 1.51/1.76  (step @p787 :rule cong :premises (@p786 @p520) :args (@t678))
% 1.51/1.76  (step @p788 :rule trans :premises (@p787 @p782))
% 1.51/1.76  (step @p789 :rule symm :premises (@p787))
% 1.51/1.76  (step @p790 :rule symm :premises (@p149))
% 1.51/1.76  (step @p791 :rule symm :premises (@p90))
% 1.51/1.76  (step @p792 :rule refl :args (@t47))
% 1.51/1.76  (step @p793 :rule cong :premises (@p745 @p792) :args (@t262))
% 1.51/1.76  (step @p794 :rule trans :premises (@p69 @p793 @p791 @p121))
% 1.51/1.76  (step @p795 :rule symm :premises (@p61))
% 1.51/1.76  (step @p796 :rule symm :premises (@p191))
% 1.51/1.76  (step @p797 :rule symm :premises (@p78))
% 1.51/1.76  (step @p798 :rule cong :premises (@p595 @p774) :args (@t132))
% 1.51/1.76  (step @p799 :rule trans :premises (@p798 @p797))
% 1.51/1.76  (step @p800 :rule symm :premises (@p82))
% 1.51/1.76  (step @p801 :rule symm :premises (@p587))
% 1.51/1.76  (step @p802 :rule trans :premises (@p68 @p801 @p800 @p69 @p793 @p791))
% 1.51/1.76  (step @p803 :rule trans :premises (@p745 @p802))
% 1.51/1.76  (step @p804 :rule cong :premises (@p803 @p799) :args (@t151))
% 1.51/1.76  (step @p805 :rule trans :premises (@p804 @p796 @p795))
% 1.51/1.76  (step @p806 :rule cong :premises (@p805 @p520) :args (@t152))
% 1.51/1.76  (step @p807 :rule cong :premises (@p806 @p794) :args (@t602))
% 1.51/1.76  (step @p808 :rule trans :premises (@p807 @p790 @p789))
% 1.51/1.76  (step @p809 :rule trans :premises (@p808 @p788))
% 1.51/1.76  (step @p810 :rule cong :premises (@p809 @p595) :args (@t603))
% 1.51/1.76  (step @p811 :rule symm :premises (@p289))
% 1.51/1.76  (step @p812 :rule refl :args (@t152))
% 1.51/1.76  (step @p813 :rule cong :premises (@p812 @p799) :args (@t181))
% 1.51/1.76  (step @p814 :rule symm :premises (@p799))
% 1.51/1.76  (step @p815 :rule symm :premises (@p806))
% 1.51/1.76  (step @p816 :rule cong :premises (@p815 @p814) :args (@t571))
% 1.51/1.76  (step @p817 :rule trans :premises (@p798 @p797 @p148 @p263 @p816 @p813 @p811 @p810))
% 1.51/1.76  (step @p818 :rule symm :premises (@p703))
% 1.51/1.76  (step @p819 :rule cong :premises (@p520 @p818) :args (@t113))
% 1.51/1.76  (step @p820 :rule trans :premises (@p14 @p36 @p649 @p648 @p175 @p819))
% 1.51/1.76  (step @p821 :rule symm :premises (@p586))
% 1.51/1.76  (step @p822 :rule cong :premises (@p821 @p595) :args (@t134))
% 1.51/1.76  (step @p823 :rule cong :premises (@p822 @p520) :args (@t135))
% 1.51/1.76  (step @p824 :rule trans :premises (@p823 @p533 @p532))
% 1.51/1.76  (step @p825 :rule trans :premises (@p824 @p820))
% 1.51/1.76  (step @p826 :rule cong :premises (@p825 @p817) :args (@t438))
% 1.51/1.76  (step @p827 :rule symm :premises (@p209))
% 1.51/1.76  (step @p828 :rule symm :premises (@p824))
% 1.51/1.76  (step @p829 :rule cong :premises (@p814 @p828) :args (@t77))
% 1.51/1.76  (step @p830 :rule trans :premises (@p829 @p827 @p826 @p713 @p242 @p712 @p645 @p644))
% 1.51/1.76  (step @p831 :rule cong :premises (@p618 @p830) :args (@t590))
% 1.51/1.76  (step @p832 :rule refl :args (@t42))
% 1.51/1.76  (step @p833 :rule cong :premises (@p520 @p745) :args (@t524))
% 1.51/1.76  (step @p834 :rule trans :premises (@p833 @p69 @p793 @p791 @p121))
% 1.51/1.76  (step @p835 :rule symm :premises (@p829))
% 1.51/1.76  (step @p836 :rule refl :args (@t132))
% 1.51/1.76  (step @p837 :rule symm :premises (@p15))
% 1.51/1.76  (step @p838 :rule symm :premises (@p37))
% 1.51/1.76  (step @p839 :rule symm :premises (@p69))
% 1.51/1.76  (step @p840 :rule symm :premises (@p793))
% 1.51/1.76  (step @p841 :rule cong :premises (@p745 @p799) :args (@t525))
% 1.51/1.76  (step @p842 :rule trans :premises (@p841 @p840 @p839 @p82 @p587 @p585))
% 1.51/1.76  (step @p843 :rule cong :premises (@p842 @p520) :args (@t526))
% 1.51/1.76  (step @p844 :rule trans :premises (@p843 @p838 @p837))
% 1.51/1.76  (step @p845 :rule trans :premises (@p844 @p828))
% 1.51/1.76  (step @p846 :rule cong :premises (@p845 @p836) :args (@t527))
% 1.51/1.76  (step @p847 :rule trans :premises (@p846 @p209 @p835 @p789))
% 1.51/1.76  (step @p848 :rule trans :premises (@p847 @p787))
% 1.51/1.76  (step @p849 :rule cong :premises (@p848 @p834) :args (@t528))
% 1.51/1.76  (step @p850 :rule trans :premises (@p247 @p849 @p790))
% 1.51/1.76  (step @p851 :rule cong :premises (@p850 @p832) :args (@t605))
% 1.51/1.76  (step @p852 :rule symm :premises (@p290))
% 1.51/1.76  (step @p853 :rule cong :premises (@p56 @p22) :args (@t25))
% 1.51/1.76  (step @p854 :rule trans :premises (@p806 @p789))
% 1.51/1.76  (step @p855 :rule symm :premises (@p854))
% 1.51/1.76  (step @p856 :rule trans :premises (@p247 @p849 @p790 @p789))
% 1.51/1.76  (step @p857 :rule trans :premises (@p856 @p855))
% 1.51/1.76  (step @p858 :rule cong :premises (@p857 @p836) :args ((tptp.meet @t529 @t132)))
% 1.51/1.76  (step @p859 :rule symm :premises (@p858))
% 1.51/1.76  (step @p860 :rule trans :premises (@p148 @p263 @p816 @p859))
% 1.51/1.76  (step @p861 :rule cong :premises (@p718 @p745) :args (@t188))
% 1.51/1.76  (step @p862 :rule trans :premises (@p861 @p798 @p797))
% 1.51/1.76  (step @p863 :rule trans :premises (@p862 @p860 @p858))
% 1.51/1.76  (step @p864 :rule cong :premises (@p863 @p853) :args ((tptp.join @t188 @t25)))
% 1.51/1.76  (step @p865 :rule symm :premises (@p26))
% 1.51/1.76  (step @p866 :rule symm :premises (@p146))
% 1.51/1.76  (step @p867 :rule cong :premises (@p20 @p520) :args (@t58))
% 1.51/1.76  (step @p868 :rule trans :premises (@p24 @p867 @p44 @p84))
% 1.51/1.76  (step @p869 :rule cong :premises (@p26 @p868) :args (@t189))
% 1.51/1.76  (step @p870 :rule trans :premises (@p869 @p866 @p865))
% 1.51/1.76  (step @p871 :rule refl :args (@t188))
% 1.51/1.76  (step @p872 :rule cong :premises (@p871 @p870) :args (@t661))
% 1.51/1.76  (step @p873 :rule symm :premises (@p861))
% 1.51/1.76  (step @p874 :rule symm :premises (@p773))
% 1.51/1.76  (step @p875 :rule cong :premises (@p874 @p745) :args (@t460))
% 1.51/1.76  (step @p876 :rule symm :premises (@p221))
% 1.51/1.76  (step @p877 :rule symm :premises (@p862))
% 1.51/1.76  (step @p878 :rule symm :premises (@p744))
% 1.51/1.76  (step @p879 :rule cong :premises (@p878 @p877) :args ((tptp.meet @t22 @t47)))
% 1.51/1.76  (step @p880 :rule symm :premises (@p639))
% 1.51/1.76  (step @p881 :rule symm :premises (@p144))
% 1.51/1.76  (step @p882 :rule trans :premises (@p33 @p86))
% 1.51/1.76  (step @p883 :rule cong :premises (@p832 @p882) :args (@t119))
% 1.51/1.76  (step @p179 :rule instantiate :premises (@p5) :args (@t43))
% 1.51/1.76  (step @p884 :rule cong :premises (@p612 @p22) :args (@t358))
% 1.51/1.76  (step @p885 :rule trans :premises (@p884 @p179 @p883 @p881 @p618))
% 1.51/1.76  (step @p886 :rule symm :premises (@p884))
% 1.51/1.76  (step @p887 :rule trans :premises (@p886 @p885))
% 1.51/1.76  (step @p888 :rule cong :premises (@p887 @p558) :args ((tptp.join @t95 @t21)))
% 1.51/1.76  (step @p889 :rule refl :args (@t95))
% 1.51/1.76  (step @p890 :rule cong :premises (@p889 @p591) :args (@t111))
% 1.51/1.76  (step @p891 :rule trans :premises (@p890 @p888))
% 1.51/1.76  (step @p892 :rule trans :premises (@p891 @p634 @p880 @p25))
% 1.51/1.76  (step @p893 :rule cong :premises (@p892 @p595) :args ((tptp.meet @t111 tptp.b)))
% 1.51/1.76  (step @p894 :rule symm :premises (@p891))
% 1.51/1.76  (step @p895 :rule cong :premises (@p530 @p745) :args (@t479))
% 1.51/1.76  (step @p896 :rule trans :premises (@p895 @p894))
% 1.51/1.76  (step @p897 :rule cong :premises (@p896 @p595) :args (@t480))
% 1.51/1.76  (step @p898 :rule trans :premises (@p897 @p893 @p784 @p783))
% 1.51/1.76  (step @p899 :rule cong :premises (@p898 @p745) :args (@t481))
% 1.51/1.76  (step @p900 :rule trans :premises (@p899 @p90 @p840 @p839 @p82 @p587 @p585))
% 1.51/1.76  (step @p901 :rule trans :premises (@p900 @p25))
% 1.51/1.76  (step @p902 :rule cong :premises (@p901 @p714) :args (@t482))
% 1.51/1.76  (step @p903 :rule cong :premises (@p714 @p612) :args (@t304))
% 1.51/1.76  (step @p904 :rule cong :premises (@p595 @p903) :args (@t305))
% 1.51/1.76  (step @p905 :rule cong :premises (@p28 @p612) :args (@t24))
% 1.51/1.76  (step @p906 :rule symm :premises (@p58))
% 1.51/1.76  (step @p907 :rule refl :args (@t137))
% 1.51/1.76  (step @p908 :rule trans :premises (@p96 @p615))
% 1.51/1.76  (step @p909 :rule cong :premises (@p908 @p907) :args (@t458))
% 1.51/1.76  (step @p910 :rule symm :premises (@p220))
% 1.51/1.76  (step @p911 :rule symm :premises (@p768))
% 1.51/1.76  (step @p912 :rule cong :premises (@p610 @p911) :args (@t147))
% 1.51/1.76  (step @p913 :rule trans :premises (@p780 @p778 @p912))
% 1.51/1.76  (step @p914 :rule cong :premises (@p530 @p913) :args (@t532))
% 1.51/1.76  (step @p915 :rule trans :premises (@p914 @p910 @p909 @p906 @p905 @p93 @p904))
% 1.51/1.76  (step @p916 :rule cong :premises (@p530 @p775) :args (@t312))
% 1.51/1.76  (step @p917 :rule trans :premises (@p596 @p594 @p916))
% 1.51/1.76  (step @p918 :rule cong :premises (@p917 @p595) :args (@t137))
% 1.51/1.76  (step @p919 :rule trans :premises (@p20 @p38 @p918))
% 1.51/1.76  (step @p920 :rule cong :premises (@p919 @p774) :args (@t132))
% 1.51/1.76  (step @p921 :rule symm :premises (@p798))
% 1.51/1.76  (step @p922 :rule trans :premises (@p78 @p921 @p920))
% 1.51/1.76  (step @p923 :rule trans :premises (@p905 @p93 @p904))
% 1.51/1.76  (step @p924 :rule cong :premises (@p792 @p802) :args (@t510))
% 1.51/1.76  (step @p925 :rule trans :premises (@p924 @p795))
% 1.51/1.76  (step @p926 :rule trans :premises (@p925 @p922))
% 1.51/1.76  (step @p927 :rule cong :premises (@p926 @p923) :args (@t533))
% 1.51/1.76  (step @p928 :rule trans :premises (@p927 @p238 @p902 @p784 @p783))
% 1.51/1.76  (step @p929 :rule cong :premises (@p928 @p802) :args (@t534))
% 1.51/1.76  (step @p930 :rule trans :premises (@p929 @p795))
% 1.51/1.76  (step @p931 :rule trans :premises (@p930 @p922))
% 1.51/1.76  (step @p932 :rule cong :premises (@p931 @p915) :args (@t535))
% 1.51/1.76  (step @p933 :rule symm :premises (@p248))
% 1.51/1.76  (step @p934 :rule trans :premises (@p933 @p932 @p238 @p902 @p784 @p783))
% 1.51/1.76  (step @p935 :rule cong :premises (@p744 @p934) :args (@t597))
% 1.51/1.76  (step @p936 :rule trans :premises (@p784 @p783))
% 1.51/1.76  (step @p937 :rule cong :premises (@p936 @p20) :args (@t614))
% 1.51/1.76  (step @p938 :rule trans :premises (@p937 @p98 @p783))
% 1.51/1.76  (step @p939 :rule cong :premises (@p621 @p595) :args (@t308))
% 1.51/1.76  (step @p940 :rule symm :premises (@p94))
% 1.51/1.76  (step @p941 :rule trans :premises (@p883 @p881 @p618 @p905 @p93 @p904))
% 1.51/1.76  (step @p942 :rule trans :premises (@p936 @p922))
% 1.51/1.76  (step @p943 :rule cong :premises (@p942 @p941) :args (@t584))
% 1.51/1.76  (step @p944 :rule trans :premises (@p270 @p943 @p238 @p902))
% 1.51/1.76  (step @p945 :rule cong :premises (@p612 @p944) :args (@t578))
% 1.51/1.76  (step @p946 :rule symm :premises (@p936))
% 1.51/1.76  (step @p947 :rule cong :premises (@p612 @p22) :args (@t354))
% 1.51/1.76  (step @p948 :rule trans :premises (@p947 @p519))
% 1.51/1.76  (step @p949 :rule cong :premises (@p768 @p612) :args (@t355))
% 1.51/1.76  (step @p950 :rule cong :premises (@p949 @p595) :args (@t356))
% 1.51/1.76  (step @p951 :rule trans :premises (@p950 @p715 @p714))
% 1.51/1.76  (step @p952 :rule cong :premises (@p951 @p948) :args (@t357))
% 1.51/1.76  (step @p953 :rule refl :args (@t358))
% 1.51/1.76  (step @p954 :rule cong :premises (@p530 @p768) :args (@t244))
% 1.51/1.76  (step @p955 :rule trans :premises (@p58 @p954))
% 1.51/1.76  (step @p956 :rule trans :premises (@p618 @p955))
% 1.51/1.76  (step @p957 :rule cong :premises (@p956 @p612) :args (@t293))
% 1.51/1.76  (step @p958 :rule trans :premises (@p33 @p86 @p957))
% 1.51/1.76  (step @p959 :rule cong :premises (@p958 @p595) :args (@t42))
% 1.51/1.76  (step @p960 :rule trans :premises (@p22 @p959))
% 1.51/1.76  (step @p961 :rule cong :premises (@p960 @p953) :args (@t679))
% 1.51/1.76  (step @p962 :rule trans :premises (@p961 @p137 @p952))
% 1.51/1.76  (step @p963 :rule trans :premises (@p962 @p22))
% 1.51/1.76  (step @p964 :rule cong :premises (@p963 @p612) :args ((tptp.meet @t679 tptp.c)))
% 1.51/1.76  (step @p965 :rule symm :premises (@p964))
% 1.51/1.76  (step @p966 :rule symm :premises (@p883))
% 1.51/1.76  (step @p967 :rule trans :premises (@p22 @p144 @p966 @p965))
% 1.51/1.76  (step @p968 :rule trans :premises (@p967 @p964))
% 1.51/1.76  (step @p969 :rule cong :premises (@p968 @p946) :args (@t170))
% 1.51/1.76  (step @p970 :rule cong :premises (@p530 @p936) :args (@t615))
% 1.51/1.76  (step @p971 :rule trans :premises (@p970 @p969))
% 1.51/1.76  (step @p972 :rule cong :premises (@p971 @p612) :args (@t616))
% 1.51/1.76  (step @p973 :rule trans :premises (@p972 @p267 @p945 @p940 @p939 @p618))
% 1.51/1.76  (step @p974 :rule cong :premises (@p973 @p938) :args (@t617))
% 1.51/1.76  (step @p975 :rule symm :premises (@p293))
% 1.51/1.76  (step @p976 :rule trans :premises (@p925 @p946))
% 1.51/1.76  (step @p977 :rule cong :premises (@p976 @p595) :args (@t511))
% 1.51/1.76  (step @p978 :rule symm :premises (@p925))
% 1.51/1.76  (step @p979 :rule trans :premises (@p797 @p978))
% 1.51/1.76  (step @p980 :rule cong :premises (@p979 @p595) :args (@t580))
% 1.51/1.76  (step @p981 :rule trans :premises (@p717 @p715 @p714 @p155 @p268 @p980 @p977))
% 1.51/1.76  (step @p982 :rule refl :args (@t613))
% 1.51/1.76  (step @p983 :rule cong :premises (@p982 @p981) :args ((tptp.meet @t613 @t138)))
% 1.51/1.76  (step @p984 :rule symm :premises (@p718))
% 1.51/1.76  (step @p985 :rule symm :premises (@p143))
% 1.51/1.76  (step @p986 :rule cong :premises (@p612 @p211) :args ((tptp.meet tptp.c @t105)))
% 1.51/1.76  (step @p987 :rule symm :premises (@p64))
% 1.51/1.76  (step @p988 :rule cong :premises (@p595 @p987) :args (@t477))
% 1.51/1.76  (step @p989 :rule symm :premises (@p211))
% 1.51/1.76  (step @p990 :rule cong :premises (@p989 @p29) :args (@t639))
% 1.51/1.76  (step @p991 :rule trans :premises (@p990 @p237 @p988))
% 1.51/1.76  (step @p992 :rule symm :premises (@p63))
% 1.51/1.76  (step @p993 :rule cong :premises (@p992 @p832) :args (@t475))
% 1.51/1.76  (step @p994 :rule symm :premises (@p227))
% 1.51/1.76  (step @p995 :rule refl :args (@t186))
% 1.51/1.76  (step @p996 :rule trans :premises (@p994 @p993 @p519))
% 1.51/1.76  (step @p997 :rule cong :premises (@p996 @p989) :args (@t640))
% 1.51/1.76  (step @p998 :rule trans :premises (@p997 @p986 @p985))
% 1.51/1.76  (step @p999 :rule cong :premises (@p998 @p995) :args (@t641))
% 1.51/1.76  (step @p1000 :rule trans :premises (@p999 @p994 @p993 @p519))
% 1.51/1.76  (step @p1001 :rule cong :premises (@p1000 @p991) :args (@t642))
% 1.51/1.76  (step @p1002 :rule trans :premises (@p298 @p1001 @p986 @p985))
% 1.51/1.76  (step @p1003 :rule refl :args (@t612))
% 1.51/1.76  (step @p1004 :rule cong :premises (@p1003 @p1002) :args ((tptp.join @t612 @t643)))
% 1.51/1.76  (step @p1005 :rule symm :premises (@p1002))
% 1.51/1.76  (step @p1006 :rule symm :premises (@p912))
% 1.51/1.76  (step @p1007 :rule cong :premises (@p989 @p1006) :args (@t657))
% 1.51/1.76  (step @p1008 :rule refl :args (@t158))
% 1.51/1.76  (step @p1009 :rule symm :premises (@p86))
% 1.51/1.76  (step @p1010 :rule symm :premises (@p923))
% 1.51/1.76  (step @p1011 :rule trans :premises (@p1010 @p22))
% 1.51/1.76  (step @p1012 :rule cong :premises (@p1011 @p612) :args (@t362))
% 1.51/1.76  (step @p1013 :rule trans :premises (@p1012 @p1009 @p519))
% 1.51/1.76  (step @p1014 :rule cong :premises (@p1013 @p22) :args (@t363))
% 1.51/1.76  (step @p1015 :rule trans :premises (@p1014 @p886 @p885))
% 1.51/1.76  (step @p1016 :rule cong :premises (@p1015 @p618) :args (@t364))
% 1.51/1.76  (step @p1017 :rule symm :premises (@p138))
% 1.51/1.76  (step @p1018 :rule trans :premises (@p1017 @p1016 @p716))
% 1.51/1.76  (step @p1019 :rule cong :premises (@p1018 @p936) :args (@t680))
% 1.51/1.76  (step @p1020 :rule trans :premises (@p1019 @p969 @p270 @p943 @p238 @p902 @p784 @p783))
% 1.51/1.76  (step @p1021 :rule trans :premises (@p1020 @p913))
% 1.51/1.76  (step @p1022 :rule cong :premises (@p1021 @p1008) :args ((tptp.meet @t680 @t158)))
% 1.51/1.76  (step @p1023 :rule trans :premises (@p1022 @p301 @p1007))
% 1.51/1.76  (step @p1024 :rule symm :premises (@p1022))
% 1.51/1.76  (step @p1025 :rule trans :premises (@p270 @p943 @p238 @p902 @p784 @p783))
% 1.51/1.76  (step @p1026 :rule symm :premises (@p155))
% 1.51/1.76  (step @p1027 :rule trans :premises (@p784 @p783 @p78))
% 1.51/1.76  (step @p1028 :rule cong :premises (@p595 @p1027) :args (@t651))
% 1.51/1.76  (step @p1029 :rule trans :premises (@p1028 @p1026))
% 1.51/1.76  (step @p1030 :rule cong :premises (@p1029 @p612) :args (@t652))
% 1.51/1.76  (step @p1031 :rule cong :premises (@p1030 @p936) :args (@t653))
% 1.51/1.76  (step @p1032 :rule trans :premises (@p1031 @p969))
% 1.51/1.76  (step @p1033 :rule trans :premises (@p1032 @p1025 @p913))
% 1.51/1.76  (step @p1034 :rule cong :premises (@p1033 @p1008) :args (@t654))
% 1.51/1.76  (step @p1035 :rule symm :premises (@p913))
% 1.51/1.76  (step @p1036 :rule trans :premises (@p1035 @p922))
% 1.51/1.76  (step @p1037 :rule cong :premises (@p1036 @p923) :args (@t633))
% 1.51/1.76  (step @p1038 :rule trans :premises (@p1037 @p238 @p902 @p912))
% 1.51/1.76  (step @p1039 :rule symm :premises (@p156))
% 1.51/1.76  (step @p1040 :rule refl :args (@t91))
% 1.51/1.76  (step @p1041 :rule refl :args (@t185))
% 1.51/1.76  (step @p1042 :rule cong :premises (@p1039 @p1041) :args (@t634))
% 1.51/1.76  (step @p1043 :rule trans :premises (@p1042 @p910 @p909 @p906))
% 1.51/1.76  (step @p1044 :rule cong :premises (@p1043 @p1040) :args (@t635))
% 1.51/1.76  (step @p1045 :rule trans :premises (@p1044 @p1039))
% 1.51/1.76  (step @p1046 :rule cong :premises (@p1045 @p1038) :args (@t636))
% 1.51/1.76  (step @p1047 :rule trans :premises (@p297 @p1046 @p910 @p909 @p906 @p22))
% 1.51/1.76  (step @p1048 :rule refl :args (@t655))
% 1.51/1.76  (step @p1049 :rule cong :premises (@p1048 @p1047) :args ((tptp.join @t655 @t637)))
% 1.51/1.76  (step @p1050 :rule symm :premises (@p297))
% 1.51/1.76  (step @p1051 :rule symm :premises (@p1046))
% 1.51/1.76  (step @p1052 :rule symm :premises (@p909))
% 1.51/1.76  (step @p1053 :rule symm :premises (@p905))
% 1.51/1.76  (step @p1054 :rule symm :premises (@p93))
% 1.51/1.76  (step @p1055 :rule symm :premises (@p904))
% 1.51/1.76  (step @p1056 :rule trans :premises (@p1055 @p1054 @p1053 @p58 @p1052 @p220 @p1051 @p1050))
% 1.51/1.76  (step @p1057 :rule cong :premises (@p714 @p946) :args (@t424))
% 1.51/1.76  (step @p1058 :rule symm :premises (@p98))
% 1.51/1.76  (step @p1059 :rule trans :premises (@p780 @p1058 @p190 @p1057))
% 1.51/1.76  (step @p1060 :rule trans :premises (@p591 @p68 @p801 @p800 @p69 @p793 @p791))
% 1.51/1.76  (step @p1061 :rule cong :premises (@p792 @p1060) :args (@t150))
% 1.51/1.76  (step @p1062 :rule trans :premises (@p1061 @p795))
% 1.51/1.76  (step @p1063 :rule trans :premises (@p1062 @p1059))
% 1.51/1.76  (step @p1064 :rule cong :premises (@p1063 @p612) :args (@t187))
% 1.51/1.76  (step @p1065 :rule symm :premises (@p1062))
% 1.51/1.76  (step @p1066 :rule cong :premises (@p25 @p595) :args (@t681))
% 1.51/1.76  (step @p1067 :rule trans :premises (@p1066 @p784 @p783))
% 1.51/1.76  (step @p1068 :rule trans :premises (@p1067 @p1065))
% 1.51/1.76  (step @p1069 :rule cong :premises (@p1068 @p612) :args ((tptp.join @t681 tptp.c)))
% 1.51/1.76  (step @p1070 :rule symm :premises (@p1069))
% 1.51/1.77  (step @p1071 :rule cong :premises (@p1065 @p612) :args (@t582))
% 1.51/1.77  (step @p1072 :rule cong :premises (@p612 @p936) :args (@t153))
% 1.51/1.77  (step @p1073 :rule trans :premises (@p1072 @p269 @p1071 @p1070))
% 1.51/1.77  (step @p1074 :rule symm :premises (@p1072))
% 1.51/1.77  (step @p1075 :rule cong :premises (@p595 @p78) :args (@t506))
% 1.51/1.77  (step @p1076 :rule trans :premises (@p1075 @p1026))
% 1.51/1.77  (step @p1077 :rule symm :premises (@p1060))
% 1.51/1.77  (step @p1078 :rule cong :premises (@p1077 @p595) :args (@t507))
% 1.51/1.77  (step @p1079 :rule trans :premises (@p1078 @p784 @p783))
% 1.51/1.77  (step @p1080 :rule cong :premises (@p1079 @p558) :args (@t508))
% 1.51/1.77  (step @p1081 :rule trans :premises (@p1080 @p90 @p840 @p839 @p82 @p587 @p585))
% 1.51/1.77  (step @p1082 :rule trans :premises (@p1081 @p25))
% 1.51/1.77  (step @p1083 :rule cong :premises (@p1082 @p1076) :args (@t509))
% 1.51/1.77  (step @p1084 :rule trans :premises (@p244 @p1083 @p784 @p783))
% 1.51/1.77  (step @p1085 :rule symm :premises (@p252))
% 1.51/1.77  (step @p1086 :rule cong :premises (@p612 @p1072) :args (@t575))
% 1.51/1.77  (step @p1087 :rule cong :premises (@p612 @p29) :args (@t155))
% 1.51/1.77  (step @p1088 :rule trans :premises (@p1087 @p987))
% 1.51/1.77  (step @p1089 :rule refl :args (@t153))
% 1.51/1.77  (step @p1090 :rule cong :premises (@p1089 @p1088) :args ((tptp.meet @t153 @t155)))
% 1.51/1.77  (step @p1091 :rule trans :premises (@p1090 @p265 @p1086 @p1085))
% 1.51/1.77  (step @p1092 :rule symm :premises (@p1090))
% 1.51/1.77  (step @p1093 :rule trans :premises (@p1092 @p1091))
% 1.51/1.77  (step @p1094 :rule cong :premises (@p1093 @p1084) :args ((tptp.join @t156 @t512)))
% 1.51/1.77  (step @p1095 :rule symm :premises (@p244))
% 1.51/1.77  (step @p1096 :rule symm :premises (@p1083))
% 1.51/1.77  (step @p1097 :rule trans :premises (@p1096 @p1095))
% 1.51/1.77  (step @p1098 :rule refl :args (@t156))
% 1.51/1.77  (step @p1099 :rule cong :premises (@p1098 @p1097) :args (@t157))
% 1.51/1.77  (step @p1100 :rule trans :premises (@p1099 @p1094 @p1074))
% 1.51/1.77  (step @p1101 :rule symm :premises (@p260))
% 1.51/1.77  (step @p1102 :rule cong :premises (@p612 @p519) :args (@t242))
% 1.51/1.77  (step @p1103 :rule trans :premises (@p57 @p1102))
% 1.51/1.77  (step @p1104 :rule refl :args (@t147))
% 1.51/1.77  (step @p1105 :rule symm :premises (@p939))
% 1.51/1.77  (step @p1106 :rule trans :premises (@p22 @p1105 @p94))
% 1.51/1.77  (step @p1107 :rule trans :premises (@p618 @p1106))
% 1.51/1.77  (step @p1108 :rule cong :premises (@p1107 @p612) :args (@t293))
% 1.51/1.77  (step @p1109 :rule trans :premises (@p33 @p86 @p1108))
% 1.51/1.77  (step @p1110 :rule cong :premises (@p1109 @p1104) :args (@t307))
% 1.51/1.77  (step @p1111 :rule trans :premises (@p22 @p1105 @p94 @p1110))
% 1.51/1.77  (step @p1112 :rule trans :premises (@p618 @p1111))
% 1.51/1.77  (step @p1113 :rule cong :premises (@p1112 @p1103) :args (@t293))
% 1.51/1.77  (step @p1114 :rule trans :premises (@p86 @p1113 @p239))
% 1.51/1.77  (step @p1115 :rule refl :args (@t157))
% 1.51/1.77  (step @p1116 :rule cong :premises (@p1115 @p1114) :args ((tptp.join @t157 @t212)))
% 1.51/1.77  (step @p1117 :rule cong :premises (@p1115 @p33) :args (@t682))
% 1.51/1.77  (step @p1118 :rule trans :premises (@p1117 @p1116 @p1101))
% 1.51/1.77  (step @p1119 :rule trans :premises (@p1118 @p1100 @p1073 @p1069 @p1064))
% 1.51/1.77  (step @p1120 :rule cong :premises (@p1119 @p946) :args ((tptp.meet @t682 @t47)))
% 1.51/1.77  (step @p1121 :rule symm :premises (@p1118))
% 1.51/1.77  (step @p1122 :rule symm :premises (@p1100))
% 1.51/1.77  (step @p1123 :rule symm :premises (@p259))
% 1.51/1.77  (step @p1124 :rule symm :premises (@p265))
% 1.51/1.77  (step @p1125 :rule symm :premises (@p1086))
% 1.51/1.77  (step @p1126 :rule trans :premises (@p1087 @p987 @p252 @p1125 @p1124))
% 1.51/1.77  (step @p1127 :rule cong :premises (@p1089 @p1126) :args (@t683))
% 1.51/1.77  (step @p1128 :rule trans :premises (@p1127 @p1123))
% 1.51/1.77  (step @p1129 :rule trans :premises (@p1128 @p1122 @p1121))
% 1.51/1.77  (step @p1130 :rule cong :premises (@p1129 @p936) :args ((tptp.meet @t683 @t147)))
% 1.51/1.77  (step @p1131 :rule trans :premises (@p1130 @p1120))
% 1.51/1.77  (step @p1132 :rule symm :premises (@p1130))
% 1.51/1.77  (step @p1133 :rule symm :premises (@p269))
% 1.51/1.77  (step @p1134 :rule symm :premises (@p1071))
% 1.51/1.77  (step @p1135 :rule trans :premises (@p1134 @p1133 @p1074))
% 1.51/1.77  (step @p1136 :rule trans :premises (@p1135 @p1122 @p1121))
% 1.51/1.77  (step @p1137 :rule cong :premises (@p1136 @p1062) :args (@t659))
% 1.51/1.77  (step @p1138 :rule symm :premises (@p1061))
% 1.51/1.77  (step @p1139 :rule trans :premises (@p61 @p1138 @p253 @p302 @p1137 @p1132))
% 1.51/1.77  (step @p1140 :rule symm :premises (@p922))
% 1.51/1.77  (step @p1141 :rule trans :premises (@p1140 @p1139 @p1131))
% 1.51/1.77  (step @p1142 :rule cong :premises (@p1141 @p1056) :args (@t483))
% 1.51/1.77  (step @p1143 :rule symm :premises (@p238))
% 1.51/1.77  (step @p1144 :rule symm :premises (@p902))
% 1.51/1.77  (step @p1145 :rule trans :premises (@p780 @p778 @p1144 @p1143 @p1142 @p1049 @p300 @p1034 @p1024))
% 1.51/1.77  (step @p1146 :rule trans :premises (@p1062 @p1145 @p1023))
% 1.51/1.77  (step @p1147 :rule cong :premises (@p1146 @p1005) :args (@t187))
% 1.51/1.77  (step @p1148 :rule trans :premises (@p1072 @p269 @p1071 @p1147 @p1004))
% 1.51/1.77  (step @p1149 :rule trans :premises (@p1100 @p1148))
% 1.51/1.77  (step @p1150 :rule cong :premises (@p1149 @p984) :args ((tptp.meet @t157 tptp.b)))
% 1.51/1.77  (step @p1151 :rule symm :premises (@p62))
% 1.51/1.77  (step @p1152 :rule cong :premises (@p595 @p28) :args (@t172))
% 1.51/1.77  (step @p1153 :rule trans :premises (@p1152 @p1151))
% 1.51/1.77  (step @p1154 :rule cong :premises (@p1115 @p1153) :args (@t663))
% 1.51/1.77  (step @p1155 :rule trans :premises (@p1154 @p1150 @p983 @p975 @p974))
% 1.51/1.77  (step @p1156 :rule trans :premises (@p588 @p802))
% 1.51/1.77  (step @p1157 :rule cong :premises (@p1156 @p530) :args (@t127))
% 1.51/1.77  (step @p1158 :rule cong :premises (@p82 @p530) :args (@t340))
% 1.51/1.77  (step @p1159 :rule trans :premises (@p1158 @p1157))
% 1.51/1.77  (step @p1160 :rule symm :premises (@p1158))
% 1.51/1.77  (step @p1161 :rule trans :premises (@p596 @p594 @p186 @p593 @p1160))
% 1.51/1.77  (step @p1162 :rule trans :premises (@p1161 @p1159))
% 1.51/1.77  (step @p1163 :rule cong :premises (@p1162 @p558) :args (@t125))
% 1.51/1.77  (step @p1164 :rule trans :premises (@p638 @p637 @p636 @p635 @p1163))
% 1.51/1.77  (step @p1165 :rule cong :premises (@p878 @p1164) :args (@t23))
% 1.51/1.77  (step @p1166 :rule trans :premises (@p684 @p1165))
% 1.51/1.77  (step @p1167 :rule cong :premises (@p1166 @p1155) :args (@t664))
% 1.51/1.77  (step @p1168 :rule refl :args (@t172))
% 1.51/1.77  (step @p1169 :rule symm :premises (@p1099))
% 1.51/1.77  (step @p1170 :rule symm :premises (@p1094))
% 1.51/1.77  (step @p1171 :rule symm :premises (@p148))
% 1.51/1.77  (step @p1172 :rule symm :premises (@p263))
% 1.51/1.77  (step @p1173 :rule symm :premises (@p816))
% 1.51/1.77  (step @p1174 :rule trans :premises (@p1173 @p1172 @p1171))
% 1.51/1.77  (step @p1175 :rule cong :premises (@p612 @p1174) :args (@t645))
% 1.51/1.77  (step @p1176 :rule trans :premises (@p1175 @p1170 @p1169))
% 1.51/1.77  (step @p1177 :rule symm :premises (@p684))
% 1.51/1.77  (step @p1178 :rule symm :premises (@p79))
% 1.51/1.77  (step @p1179 :rule cong :premises (@p1178 @p610) :args (@t462))
% 1.51/1.77  (step @p1180 :rule symm :premises (@p222))
% 1.51/1.77  (step @p1181 :rule symm :premises (@p55))
% 1.51/1.77  (step @p1182 :rule cong :premises (@p520 @p32) :args (@t96))
% 1.51/1.77  (step @p1183 :rule trans :premises (@p1182 @p1181))
% 1.51/1.77  (step @p1184 :rule trans :premises (@p1183 @p828))
% 1.51/1.77  (step @p1185 :rule cong :premises (@p1184 @p836) :args (@t684))
% 1.51/1.77  (step @p1186 :rule trans :premises (@p1185 @p826 @p713 @p242 @p712 @p645 @p644 @p1177))
% 1.51/1.77  (step @p1187 :rule cong :premises (@p612 @p1186) :args ((tptp.meet tptp.c @t684)))
% 1.51/1.77  (step @p1188 :rule symm :premises (@p1185))
% 1.51/1.77  (step @p1189 :rule trans :premises (@p829 @p827 @p1188))
% 1.51/1.77  (step @p1190 :rule cong :premises (@p612 @p1189) :args (@t573))
% 1.51/1.77  (step @p1191 :rule trans :premises (@p264 @p1190 @p1187 @p1180 @p1179 @p100 @p719))
% 1.51/1.77  (step @p1192 :rule cong :premises (@p520 @p1191) :args (@t594))
% 1.51/1.77  (step @p1193 :rule trans :premises (@p275 @p1192 @p702 @p241 @p681 @p654 @p653))
% 1.51/1.77  (step @p1194 :rule symm :premises (@p649))
% 1.51/1.77  (step @p1195 :rule symm :premises (@p154))
% 1.51/1.77  (step @p1196 :rule cong :premises (@p520 @p74) :args (@t544))
% 1.51/1.77  (step @p1197 :rule trans :premises (@p1196 @p1195))
% 1.51/1.77  (step @p1198 :rule symm :premises (@p698))
% 1.51/1.77  (step @p1199 :rule symm :premises (@p89))
% 1.51/1.77  (step @p1200 :rule refl :args (@t64))
% 1.51/1.77  (step @p1201 :rule cong :premises (@p1200 @p682) :args (@t545))
% 1.51/1.77  (step @p1202 :rule trans :premises (@p1201 @p1199 @p46 @p80 @p1198 @p653))
% 1.51/1.77  (step @p1203 :rule cong :premises (@p1202 @p520) :args (@t546))
% 1.51/1.77  (step @p1204 :rule trans :premises (@p1203 @p97 @p1194 @p533 @p532))
% 1.51/1.77  (step @p1205 :rule cong :premises (@p1204 @p651) :args (@t547))
% 1.51/1.77  (step @p1206 :rule trans :premises (@p1205 @p203 @p652 @p647))
% 1.51/1.77  (step @p1207 :rule cong :premises (@p1206 @p1197) :args (@t548))
% 1.51/1.77  (step @p1208 :rule trans :premises (@p250 @p1207 @p97 @p1194 @p533 @p532))
% 1.51/1.77  (step @p1209 :rule refl :args (@t167))
% 1.51/1.77  (step @p1210 :rule cong :premises (@p1209 @p1208) :args ((tptp.join @t167 @t549)))
% 1.51/1.77  (step @p1211 :rule symm :premises (@p1208))
% 1.51/1.77  (step @p1212 :rule refl :args (@t181))
% 1.51/1.77  (step @p1213 :rule cong :premises (@p1212 @p56) :args (@t646))
% 1.51/1.77  (step @p1214 :rule trans :premises (@p1213 @p247 @p849 @p790 @p789))
% 1.51/1.77  (step @p1215 :rule trans :premises (@p1214 @p787))
% 1.51/1.77  (step @p1216 :rule cong :premises (@p1215 @p612) :args (@t647))
% 1.51/1.77  (step @p1217 :rule cong :premises (@p1216 @p1211) :args (@t648))
% 1.51/1.77  (step @p1218 :rule trans :premises (@p1217 @p1210))
% 1.51/1.77  (step @p1219 :rule trans :premises (@p1218 @p1193 @p1177))
% 1.51/1.77  (step @p1220 :rule cong :premises (@p1219 @p1176) :args (@t649))
% 1.51/1.77  (step @p1221 :rule trans :premises (@p784 @p783 @p148 @p263 @p816))
% 1.51/1.77  (step @p1222 :rule cong :premises (@p612 @p1221) :args (@t307))
% 1.51/1.77  (step @p1223 :rule trans :premises (@p1105 @p94 @p1222))
% 1.51/1.77  (step @p1224 :rule cong :premises (@p1212 @p1183) :args ((tptp.meet @t181 @t96)))
% 1.51/1.77  (step @p1225 :rule symm :premises (@p1182))
% 1.51/1.77  (step @p1226 :rule symm :premises (@p56))
% 1.51/1.77  (step @p1227 :rule trans :premises (@p1226 @p55 @p1225))
% 1.51/1.77  (step @p1228 :rule cong :premises (@p1212 @p1227) :args ((tptp.meet @t181 @t175)))
% 1.51/1.77  (step @p1229 :rule symm :premises (@p1228))
% 1.51/1.77  (step @p1230 :rule symm :premises (@p1183))
% 1.51/1.77  (step @p1231 :rule symm :premises (@p1174))
% 1.51/1.77  (step @p1232 :rule cong :premises (@p1231 @p1230) :args (@t567))
% 1.51/1.77  (step @p283 :rule instantiate :premises (@p7) :args (@t179))
% 1.51/1.77  (step @p1233 :rule cong :premises (@p56 @p595) :args (@t268))
% 1.51/1.77  (step @p1234 :rule trans :premises (@p72 @p1233 @p283 @p261 @p1232 @p1229))
% 1.51/1.77  (step @p1235 :rule trans :premises (@p1234 @p1228 @p1224))
% 1.51/1.77  (step @p1236 :rule cong :premises (@p1235 @p612) :args (@t629))
% 1.51/1.77  (step @p1237 :rule cong :premises (@p1236 @p520) :args (@t630))
% 1.51/1.77  (step @p1238 :rule cong :premises (@p1237 @p1223) :args (@t631))
% 1.51/1.77  (step @p1239 :rule symm :premises (@p296))
% 1.51/1.77  (step @p1240 :rule symm :premises (@p543))
% 1.51/1.77  (step @p1241 :rule trans :premises (@p540 @p1240 @p24))
% 1.51/1.77  (step @p1242 :rule cong :premises (@p1241 @p621) :args (@t320))
% 1.51/1.77  (step @p1243 :rule trans :premises (@p690 @p1242))
% 1.51/1.77  (step @p1244 :rule cong :premises (@p1243 @p520) :args (@t83))
% 1.51/1.77  (step @p1245 :rule trans :premises (@p23 @p147 @p731 @p730 @p729 @p728 @p1244))
% 1.51/1.77  (step @p1246 :rule trans :premises (@p787 @p829 @p827 @p826 @p713 @p242 @p712 @p645 @p644))
% 1.51/1.77  (step @p1247 :rule symm :premises (@p258))
% 1.51/1.77  (step @p1248 :rule cong :premises (@p855 @p1212) :args ((tptp.join @t678 @t181)))
% 1.51/1.77  (step @p1249 :rule cong :premises (@p789 @p1231) :args (@t588))
% 1.51/1.77  (step @p1250 :rule refl :args (@t77))
% 1.51/1.77  (step @p116 :rule instantiate :premises (@p8) :args (@t81))
% 1.51/1.77  (step @p1251 :rule symm :premises (@p219))
% 1.51/1.77  (step @p1252 :rule trans :premises (@p1251 @p116 @p90 @p840 @p839 @p82 @p587 @p585))
% 1.51/1.77  (step @p1253 :rule trans :premises (@p1252 @p25))
% 1.51/1.77  (step @p1254 :rule cong :premises (@p1253 @p595) :args (@t685))
% 1.51/1.77  (step @p1255 :rule trans :premises (@p1254 @p784 @p783))
% 1.51/1.77  (step @p1256 :rule cong :premises (@p1255 @p1250) :args (@t686))
% 1.51/1.77  (step @p1257 :rule trans :premises (@p1256 @p272 @p1249 @p1248 @p1247 @p806 @p789))
% 1.51/1.77  (step @p1258 :rule trans :premises (@p1257 @p1246 @p1245))
% 1.51/1.77  (step @p1259 :rule cong :premises (@p1258 @p211) :args ((tptp.meet @t686 @t105)))
% 1.51/1.77  (step @p1260 :rule refl :args (@t105))
% 1.51/1.77  (step @p1261 :rule symm :premises (@p1257))
% 1.51/1.77  (step @p1262 :rule cong :premises (@p936 @p520) :args (@t514))
% 1.51/1.77  (step @p1263 :rule trans :premises (@p1262 @p789))
% 1.51/1.77  (step @p1264 :rule trans :premises (@p1263 @p1261))
% 1.51/1.77  (step @p1265 :rule cong :premises (@p1264 @p1260) :args (@t515))
% 1.51/1.77  (step @p1266 :rule symm :premises (@p142))
% 1.51/1.77  (step @p1267 :rule trans :premises (@p193 @p1266))
% 1.51/1.77  (step @p1268 :rule symm :premises (@p262))
% 1.51/1.77  (step @p1269 :rule cong :premises (@p595 @p519) :args (@t687))
% 1.51/1.77  (step @p1270 :rule trans :premises (@p1269 @p211))
% 1.51/1.77  (step @p1271 :rule cong :premises (@p1270 @p612) :args ((tptp.meet @t687 tptp.c)))
% 1.51/1.77  (step @p1272 :rule symm :premises (@p1269))
% 1.51/1.77  (step @p1273 :rule symm :premises (@p162))
% 1.51/1.77  (step @p1274 :rule symm :premises (@p193))
% 1.51/1.77  (step @p1275 :rule trans :premises (@p1152 @p1151 @p142 @p1274))
% 1.51/1.77  (step @p1276 :rule cong :premises (@p1260 @p1275) :args (@t688))
% 1.51/1.77  (step @p1277 :rule trans :premises (@p1276 @p1273))
% 1.51/1.77  (step @p1278 :rule trans :premises (@p1277 @p1272))
% 1.51/1.77  (step @p1279 :rule cong :premises (@p1278 @p612) :args (@t689))
% 1.51/1.77  (step @p1280 :rule trans :premises (@p1279 @p1271 @p1268 @p985))
% 1.51/1.77  (step @p1281 :rule symm :premises (@p1279))
% 1.51/1.77  (step @p1282 :rule symm :premises (@p1271))
% 1.51/1.77  (step @p1283 :rule trans :premises (@p1282 @p1281))
% 1.51/1.77  (step @p1284 :rule trans :premises (@p1283 @p1280))
% 1.51/1.77  (step @p1285 :rule cong :premises (@p1284 @p1267) :args ((tptp.join @t569 @t406)))
% 1.51/1.77  (step @p1286 :rule symm :premises (@p1283))
% 1.51/1.77  (step @p1287 :rule cong :premises (@p1286 @p1275) :args (@t690))
% 1.51/1.77  (step @p1288 :rule trans :premises (@p1287 @p1285 @p989))
% 1.51/1.77  (step @p1289 :rule refl :args (@t514))
% 1.51/1.77  (step @p1290 :rule cong :premises (@p1289 @p1288) :args ((tptp.meet @t514 @t690)))
% 1.51/1.77  (step @p1291 :rule trans :premises (@p1290 @p1265 @p1259 @p1239 @p1238 @p299 @p1220))
% 1.51/1.77  (step @p1292 :rule symm :premises (@p1290))
% 1.51/1.77  (step @p1293 :rule symm :premises (@p30))
% 1.51/1.77  (step @p1294 :rule symm :premises (@p76))
% 1.51/1.77  (step @p1295 :rule cong :premises (@p530 @p548) :args ((tptp.join @t24 @t420)))
% 1.51/1.77  (step @p1296 :rule cong :premises (@p530 @p545) :args (@t537))
% 1.51/1.77  (step @p1297 :rule trans :premises (@p1296 @p1295 @p716))
% 1.51/1.77  (step @p1298 :rule cong :premises (@p566 @p520) :args (@t350))
% 1.51/1.77  (step @p1299 :rule trans :premises (@p1298 @p533 @p532))
% 1.51/1.77  (step @p1300 :rule cong :premises (@p1299 @p530) :args (@t351))
% 1.51/1.77  (step @p1301 :rule cong :premises (@p1300 @p683) :args (@t352))
% 1.51/1.77  (step @p1302 :rule refl :args (@t65))
% 1.51/1.77  (step @p1303 :rule refl :args (@t101))
% 1.51/1.77  (step @p1304 :rule cong :premises (@p1303 @p532) :args (@t538))
% 1.51/1.77  (step @p1305 :rule cong :premises (@p1304 @p530) :args (@t539))
% 1.51/1.77  (step @p1306 :rule cong :premises (@p1305 @p1302) :args (@t540))
% 1.51/1.77  (step @p1307 :rule trans :premises (@p1306 @p136 @p1301 @p869 @p866 @p865))
% 1.51/1.77  (step @p1308 :rule trans :premises (@p1307 @p26))
% 1.51/1.77  (step @p1309 :rule cong :premises (@p1308 @p1297) :args (@t541))
% 1.51/1.77  (step @p1310 :rule trans :premises (@p249 @p1309 @p1294 @p1293))
% 1.51/1.77  (step @p1311 :rule refl :args (@t517))
% 1.51/1.77  (step @p1312 :rule cong :premises (@p1311 @p1310) :args ((tptp.join @t517 @t542)))
% 1.51/1.77  (step @p1313 :rule symm :premises (@p249))
% 1.51/1.77  (step @p1314 :rule symm :premises (@p1309))
% 1.51/1.77  (step @p1315 :rule symm :premises (@p95))
% 1.51/1.77  (step @p1316 :rule cong :premises (@p530 @p25) :args (@t335))
% 1.51/1.77  (step @p1317 :rule trans :premises (@p1316 @p96 @p615))
% 1.51/1.77  (step @p1318 :rule symm :premises (@p16))
% 1.51/1.77  (step @p1319 :rule symm :premises (@p35))
% 1.51/1.77  (step @p1320 :rule cong :premises (@p821 @p530) :args (@t336))
% 1.51/1.77  (step @p1321 :rule cong :premises (@p1320 @p520) :args (@t337))
% 1.51/1.77  (step @p1322 :rule trans :premises (@p1321 @p1319 @p1318))
% 1.51/1.77  (step @p1323 :rule cong :premises (@p1322 @p1317) :args (@t338))
% 1.51/1.77  (step @p1324 :rule symm :premises (@p133))
% 1.51/1.77  (step @p1325 :rule refl :args (@t125))
% 1.51/1.77  (step @p1326 :rule trans :premises (@p1319 @p1318))
% 1.51/1.77  (step @p1327 :rule refl :args (@t127))
% 1.51/1.77  (step @p1328 :rule cong :premises (@p1327 @p1326) :args (@t691))
% 1.51/1.77  (step @p1329 :rule cong :premises (@p1328 @p1325) :args (@t692))
% 1.51/1.77  (step @p1330 :rule symm :premises (@p1163))
% 1.51/1.77  (step @p1331 :rule cong :premises (@p1159 @p558) :args (@t341))
% 1.51/1.77  (step @p1332 :rule trans :premises (@p1331 @p1330))
% 1.51/1.77  (step @p1333 :rule symm :premises (@p1328))
% 1.51/1.77  (step @p1334 :rule cong :premises (@p593 @p520) :args (@t520))
% 1.51/1.77  (step @p1335 :rule symm :premises (@p1334))
% 1.51/1.77  (step @p1336 :rule trans :premises (@p1161 @p1158))
% 1.51/1.77  (step @p1337 :rule cong :premises (@p1336 @p520) :args (@t60))
% 1.51/1.77  (step @p1338 :rule trans :premises (@p26 @p1337 @p1335))
% 1.51/1.77  (step @p1339 :rule trans :premises (@p865 @p1338 @p1334 @p1333))
% 1.51/1.77  (step @p1340 :rule cong :premises (@p1339 @p1332) :args ((tptp.meet @t60 @t341)))
% 1.51/1.77  (step @p1341 :rule symm :premises (@p1331))
% 1.51/1.77  (step @p1342 :rule symm :premises (@p165))
% 1.51/1.77  (step @p1343 :rule symm :premises (@p198))
% 1.51/1.77  (step @p1344 :rule refl :args (@t111))
% 1.51/1.77  (step @p1345 :rule trans :premises (@p1014 @p886))
% 1.51/1.77  (step @p1346 :rule symm :premises (@p1014))
% 1.51/1.77  (step @p1347 :rule trans :premises (@p1346 @p1345 @p885 @p22))
% 1.51/1.77  (step @p1348 :rule cong :premises (@p1347 @p1344) :args (@t391))
% 1.51/1.77  (step @p1349 :rule trans :premises (@p617 @p616 @p96 @p615 @p22 @p144 @p966 @p184 @p151 @p1348 @p1343))
% 1.51/1.77  (step @p1350 :rule cong :premises (@p894 @p1349) :args (@t693))
% 1.51/1.77  (step @p1351 :rule trans :premises (@p1350 @p1342 @p890 @p888 @p1163 @p1341))
% 1.51/1.77  (step @p1352 :rule symm :premises (@p65))
% 1.51/1.77  (step @p1353 :rule refl :args (@t215))
% 1.51/1.77  (step @p1354 :rule trans :premises (@p1329 @p1324 @p1323))
% 1.51/1.77  (step @p1355 :rule cong :premises (@p1354 @p1353) :args (@t694))
% 1.51/1.77  (step @p1356 :rule trans :premises (@p1355 @p1352))
% 1.51/1.77  (step @p1357 :rule trans :premises (@p1356 @p26))
% 1.51/1.77  (step @p1358 :rule cong :premises (@p1357 @p1351) :args ((tptp.meet @t694 @t693)))
% 1.51/1.77  (step @p1359 :rule symm :premises (@p1350))
% 1.51/1.77  (step @p1360 :rule symm :premises (@p890))
% 1.51/1.77  (step @p1361 :rule symm :premises (@p888))
% 1.51/1.77  (step @p1362 :rule trans :premises (@p638 @p637 @p636 @p635 @p1361 @p1360 @p165 @p1359))
% 1.51/1.77  (step @p1363 :rule symm :premises (@p1356))
% 1.51/1.77  (step @p1364 :rule cong :premises (@p1363 @p1362) :args (@t56))
% 1.51/1.77  (step @p1365 :rule symm :premises (@p163))
% 1.51/1.77  (step @p1366 :rule cong :premises (@p16 @p558) :args (@t92))
% 1.51/1.77  (step @p1367 :rule trans :premises (@p15 @p1366 @p40 @p71))
% 1.51/1.77  (step @p1368 :rule refl :args (@t56))
% 1.51/1.77  (step @p1369 :rule cong :premises (@p1368 @p1367) :args (@t440))
% 1.51/1.77  (step @p1370 :rule cong :premises (@p837 @p530) :args (@t93))
% 1.51/1.77  (step @p1371 :rule cong :premises (@p1370 @p558) :args (@t94))
% 1.51/1.77  (step @p1372 :rule symm :premises (@p150))
% 1.51/1.77  (step @p1373 :rule symm :premises (@p134))
% 1.51/1.77  (step @p1374 :rule trans :premises (@p1324 @p1323 @p26))
% 1.51/1.77  (step @p1375 :rule refl :args (@t341))
% 1.51/1.77  (step @p1376 :rule cong :premises (@p1375 @p1374) :args ((tptp.meet @t341 @t334)))
% 1.51/1.77  (step @p1377 :rule symm :premises (@p1323))
% 1.51/1.77  (step @p1378 :rule trans :premises (@p1377 @p133))
% 1.51/1.77  (step @p1379 :rule symm :premises (@p1332))
% 1.51/1.77  (step @p1380 :rule cong :premises (@p1379 @p1378) :args ((tptp.meet @t125 @t25)))
% 1.51/1.77  (step @p1381 :rule symm :premises (@p1337))
% 1.51/1.77  (step @p1382 :rule trans :premises (@p1381 @p865))
% 1.51/1.77  (step @p1383 :rule cong :premises (@p1325 @p1382) :args (@t433))
% 1.51/1.77  (step @p1384 :rule symm :premises (@p50))
% 1.51/1.77  (step @p1385 :rule trans :premises (@p1384 @p1377 @p133 @p196 @p1383 @p1380 @p1376 @p1373))
% 1.51/1.77  (step @p1386 :rule symm :premises (@p1371))
% 1.51/1.77  (step @p1387 :rule cong :premises (@p1386 @p1385) :args (@t416))
% 1.51/1.77  (step @p1388 :rule trans :premises (@p187 @p1387 @p1372 @p1371))
% 1.51/1.77  (step @p1389 :rule symm :premises (@p141))
% 1.51/1.77  (step @p1390 :rule refl :args (@t108))
% 1.51/1.77  (step @p1391 :rule cong :premises (@p1318 @p1390) :args (@t435))
% 1.51/1.77  (step @p1392 :rule trans :premises (@p197 @p1391 @p1389))
% 1.51/1.77  (step @p1393 :rule symm :premises (@p32))
% 1.51/1.77  (step @p1394 :rule cong :premises (@p1318 @p32) :args (@t345))
% 1.51/1.77  (step @p1395 :rule trans :premises (@p1394 @p1181 @p16))
% 1.51/1.77  (step @p1396 :rule refl :args (@t25))
% 1.51/1.77  (step @p1397 :rule cong :premises (@p1318 @p1396) :args (@t225))
% 1.51/1.77  (step @p1398 :rule symm :premises (@p41))
% 1.51/1.77  (step @p1399 :rule refl :args (@t68))
% 1.51/1.77  (step @p1400 :rule trans :premises (@p1398 @p1397 @p1318))
% 1.51/1.77  (step @p1401 :rule cong :premises (@p1400 @p1399) :args ((tptp.meet @t224 @t68)))
% 1.51/1.77  (step @p1402 :rule symm :premises (@p1400))
% 1.51/1.77  (step @p1403 :rule refl :args (@t41))
% 1.51/1.77  (step @p1404 :rule cong :premises (@p1400 @p1403) :args (@t695))
% 1.51/1.77  (step @p1405 :rule trans :premises (@p1404 @p1393))
% 1.51/1.77  (step @p1406 :rule trans :premises (@p1405 @p1402))
% 1.51/1.77  (step @p1407 :rule cong :premises (@p1406 @p1399) :args (@t696))
% 1.51/1.77  (step @p1408 :rule trans :premises (@p1407 @p1401 @p1398 @p1397 @p1318))
% 1.51/1.77  (step @p1409 :rule cong :premises (@p1408 @p1395) :args ((tptp.join @t696 @t345)))
% 1.51/1.77  (step @p1410 :rule refl :args (@t345))
% 1.51/1.77  (step @p1411 :rule symm :premises (@p1408))
% 1.51/1.77  (step @p1412 :rule cong :premises (@p532 @p1403) :args (@t697))
% 1.51/1.77  (step @p1413 :rule trans :premises (@p1412 @p1393))
% 1.51/1.77  (step @p1414 :rule cong :premises (@p1413 @p527) :args (@t698))
% 1.51/1.77  (step @p1415 :rule trans :premises (@p1414 @p532))
% 1.51/1.77  (step @p1416 :rule trans :premises (@p1415 @p1411))
% 1.51/1.77  (step @p1417 :rule cong :premises (@p1416 @p1410) :args ((tptp.join @t698 @t345)))
% 1.51/1.77  (step @p1418 :rule symm :premises (@p1415))
% 1.51/1.77  (step @p1419 :rule symm :premises (@p1366))
% 1.51/1.77  (step @p1420 :rule symm :premises (@p40))
% 1.51/1.77  (step @p1421 :rule cong :premises (@p1400 @p1368) :args ((tptp.meet @t224 @t56)))
% 1.51/1.77  (step @p1422 :rule trans :premises (@p1420 @p1419 @p837))
% 1.51/1.77  (step @p1423 :rule cong :premises (@p1422 @p1403) :args (@t346))
% 1.51/1.77  (step @p1424 :rule trans :premises (@p1423 @p1393))
% 1.51/1.77  (step @p1425 :rule trans :premises (@p1424 @p1402))
% 1.51/1.77  (step @p1426 :rule cong :premises (@p1425 @p1368) :args (@t347))
% 1.51/1.77  (step @p1427 :rule trans :premises (@p1426 @p1421 @p1420 @p1419 @p837))
% 1.51/1.77  (step @p1428 :rule trans :premises (@p1427 @p1418))
% 1.51/1.77  (step @p1429 :rule cong :premises (@p1428 @p1410) :args (@t348))
% 1.51/1.77  (step @p1430 :rule symm :premises (@p135))
% 1.51/1.77  (step @p1431 :rule trans :premises (@p1430 @p1429 @p1417 @p1409 @p1393 @p16))
% 1.51/1.77  (step @p1432 :rule cong :premises (@p1390 @p1431) :args ((tptp.meet @t108 @t344)))
% 1.51/1.77  (step @p1433 :rule symm :premises (@p1431))
% 1.51/1.77  (step @p107 :rule instantiate :premises (@p8) :args (@t73))
% 1.51/1.77  (step @p1434 :rule refl :args (@t69))
% 1.51/1.77  (step @p1435 :rule cong :premises (@p1434 @p1151) :args ((tptp.join @t69 @t251)))
% 1.51/1.77  (step @p1436 :rule trans :premises (@p663 @p660))
% 1.51/1.77  (step @p1437 :rule cong :premises (@p1436 @p62) :args (@t291))
% 1.51/1.77  (step @p1438 :rule trans :premises (@p85 @p1437 @p1435 @p107 @p535 @p534))
% 1.51/1.77  (step @p1439 :rule cong :premises (@p520 @p16) :args (@t366))
% 1.51/1.77  (step @p1440 :rule trans :premises (@p1439 @p1393))
% 1.51/1.77  (step @p1441 :rule refl :args (@t63))
% 1.51/1.77  (step @p1442 :rule trans :premises (@p720 @p534))
% 1.51/1.77  (step @p1443 :rule cong :premises (@p1442 @p520) :args (@t367))
% 1.51/1.77  (step @p1444 :rule trans :premises (@p1443 @p533 @p532))
% 1.51/1.77  (step @p1445 :rule cong :premises (@p1444 @p1441) :args (@t368))
% 1.51/1.77  (step @p1446 :rule trans :premises (@p1445 @p720 @p534))
% 1.51/1.77  (step @p1447 :rule cong :premises (@p1446 @p1440) :args (@t369))
% 1.51/1.77  (step @p1448 :rule trans :premises (@p139 @p1447 @p533 @p532 @p16))
% 1.51/1.77  (step @p1449 :rule refl :args (@t99))
% 1.51/1.77  (step @p1450 :rule cong :premises (@p1449 @p1230) :args (@t699))
% 1.51/1.77  (step @p1451 :rule trans :premises (@p1450 @p139 @p1447 @p533 @p532))
% 1.51/1.77  (step @p1452 :rule cong :premises (@p1451 @p1438) :args ((tptp.meet @t699 @t63)))
% 1.51/1.77  (step @p1453 :rule trans :premises (@p1452 @p532))
% 1.51/1.77  (step @p1454 :rule symm :premises (@p1451))
% 1.51/1.77  (step @p1455 :rule cong :premises (@p1454 @p1441) :args (@t97))
% 1.51/1.77  (step @p1456 :rule trans :premises (@p1455 @p1453))
% 1.51/1.77  (step @p1457 :rule cong :premises (@p1456 @p1448) :args ((tptp.join @t97 @t370)))
% 1.51/1.77  (step @p1458 :rule symm :premises (@p139))
% 1.51/1.77  (step @p1459 :rule symm :premises (@p1447))
% 1.51/1.77  (step @p1460 :rule trans :premises (@p14 @p36 @p1459 @p1458))
% 1.51/1.77  (step @p1461 :rule refl :args (@t97))
% 1.51/1.77  (step @p1462 :rule cong :premises (@p1461 @p1460) :args (@t98))
% 1.51/1.77  (step @p1463 :rule trans :premises (@p1462 @p1457 @p1393))
% 1.51/1.77  (step @p1464 :rule symm :premises (@p1462))
% 1.51/1.77  (step @p1465 :rule trans :premises (@p1182 @p1181 @p14 @p36 @p1459 @p1458))
% 1.51/1.77  (step @p1466 :rule cong :premises (@p1461 @p1465) :args (@t700))
% 1.51/1.77  (step @p1467 :rule trans :premises (@p1466 @p1464))
% 1.51/1.77  (step @p1468 :rule trans :premises (@p1467 @p1463))
% 1.51/1.77  (step @p1469 :rule cong :premises (@p1468 @p1438) :args ((tptp.meet @t700 @t63)))
% 1.51/1.77  (step @p1470 :rule symm :premises (@p1467))
% 1.51/1.77  (step @p1471 :rule cong :premises (@p1470 @p1441) :args (@t99))
% 1.51/1.77  (step @p1472 :rule trans :premises (@p1471 @p1469 @p532))
% 1.51/1.77  (step @p1473 :rule symm :premises (@p1471))
% 1.51/1.77  (step @p1474 :rule symm :premises (@p152))
% 1.51/1.77  (step @p1475 :rule symm :premises (@p1448))
% 1.51/1.77  (step @p1476 :rule cong :premises (@p1449 @p1475) :args (@t701))
% 1.51/1.77  (step @p1477 :rule trans :premises (@p1476 @p1474 @p1471))
% 1.51/1.77  (step @p1478 :rule trans :premises (@p1477 @p1473 @p1472))
% 1.51/1.77  (step @p1479 :rule cong :premises (@p1478 @p1388) :args (@t702))
% 1.51/1.77  (step @p1480 :rule refl :args (@t417))
% 1.51/1.77  (step @p1481 :rule symm :premises (@p1478))
% 1.51/1.77  (step @p1482 :rule cong :premises (@p1481 @p1480) :args (@t703))
% 1.51/1.77  (step @p1483 :rule trans :premises (@p1482 @p1479))
% 1.51/1.77  (step @p1484 :rule cong :premises (@p1483 @p1433) :args (@t704))
% 1.51/1.77  (step @p1485 :rule symm :premises (@p1482))
% 1.51/1.77  (step @p1486 :rule cong :premises (@p1485 @p1403) :args ((tptp.meet @t702 @t41)))
% 1.51/1.77  (step @p1487 :rule trans :premises (@p1486 @p1484 @p1432))
% 1.51/1.77  (step @p1488 :rule symm :premises (@p1486))
% 1.51/1.77  (step @p1489 :rule trans :premises (@p1488 @p1487 @p1392))
% 1.51/1.77  (step @p1490 :rule cong :premises (@p1489 @p1388) :args ((tptp.join @t704 @t417)))
% 1.51/1.77  (step @p1491 :rule symm :premises (@p1388))
% 1.51/1.77  (step @p1492 :rule symm :premises (@p1487))
% 1.51/1.77  (step @p1493 :rule trans :premises (@p1492 @p1486))
% 1.51/1.77  (step @p1494 :rule cong :premises (@p1493 @p1491) :args (@t110))
% 1.51/1.77  (step @p1495 :rule trans :premises (@p1494 @p1490 @p210 @p1369 @p1365 @p1364 @p1358 @p1340 @p1329 @p1324 @p1323 @p26))
% 1.51/1.77  (step @p1496 :rule cong :premises (@p612 @p1495) :args (@t184))
% 1.51/1.77  (step @p1497 :rule cong :premises (@p595 @p1496) :args (@t619))
% 1.51/1.77  (step @p1498 :rule trans :premises (@p1497 @p1315 @p76 @p1314 @p1313))
% 1.51/1.77  (step @p1499 :rule trans :premises (@p1430 @p1429 @p1417 @p1409 @p1393))
% 1.51/1.77  (step @p1500 :rule cong :premises (@p651 @p1499) :args (@t471))
% 1.51/1.77  (step @p1501 :rule trans :premises (@p226 @p1500 @p97 @p1194 @p533 @p532))
% 1.51/1.77  (step @p1502 :rule refl :args (@t516))
% 1.51/1.77  (step @p1503 :rule cong :premises (@p1502 @p1501) :args ((tptp.meet @t516 @t472)))
% 1.51/1.77  (step @p1504 :rule symm :premises (@p1501))
% 1.51/1.77  (step @p1505 :rule cong :premises (@p612 @p1499) :args (@t469))
% 1.51/1.77  (step @p1506 :rule cong :premises (@p16 @p1318) :args (@t210))
% 1.51/1.77  (step @p1507 :rule trans :premises (@p32 @p1506))
% 1.51/1.77  (step @p1508 :rule refl :args (@t184))
% 1.51/1.77  (step @p1509 :rule cong :premises (@p1508 @p1507) :args (@t620))
% 1.51/1.77  (step @p1510 :rule trans :premises (@p1509 @p225 @p1505))
% 1.51/1.77  (step @p1511 :rule cong :premises (@p1510 @p595) :args (@t621))
% 1.51/1.77  (step @p1512 :rule cong :premises (@p1511 @p1504) :args (@t622))
% 1.51/1.77  (step @p1513 :rule trans :premises (@p1512 @p1503))
% 1.51/1.77  (step @p1514 :rule cong :premises (@p1513 @p1498) :args (@t623))
% 1.51/1.77  (step @p1515 :rule symm :premises (@p294))
% 1.51/1.77  (step @p1516 :rule symm :premises (@p1496))
% 1.51/1.77  (step @p1517 :rule cong :premises (@p595 @p1516) :args (@t160))
% 1.51/1.77  (step @p1518 :rule symm :premises (@p185))
% 1.51/1.77  (step @p1519 :rule cong :premises (@p22 @p612) :args (@t519))
% 1.51/1.77  (step @p1520 :rule trans :premises (@p1519 @p1009 @p519))
% 1.51/1.77  (step @p1521 :rule symm :premises (@p1338))
% 1.51/1.77  (step @p1522 :rule trans :premises (@p1521 @p26))
% 1.51/1.77  (step @p1523 :rule cong :premises (@p1522 @p1520) :args (@t521))
% 1.51/1.77  (step @p1524 :rule trans :premises (@p246 @p1523 @p1518))
% 1.51/1.77  (step @p1525 :rule symm :premises (@p251))
% 1.51/1.77  (step @p1526 :rule trans :premises (@p266 @p1525))
% 1.51/1.77  (step @p1527 :rule cong :premises (@p1526 @p1524) :args ((tptp.join @t173 @t522)))
% 1.51/1.77  (step @p1528 :rule symm :premises (@p1524))
% 1.51/1.77  (step @p1529 :rule refl :args (@t173))
% 1.51/1.77  (step @p1530 :rule cong :premises (@p1529 @p1528) :args (@t174))
% 1.51/1.77  (step @p1531 :rule trans :premises (@p1530 @p1527 @p1517))
% 1.51/1.77  (step @p1532 :rule refl :args (@t60))
% 1.51/1.77  (step @p1533 :rule trans :premises (@p1293 @p22))
% 1.51/1.77  (step @p1534 :rule cong :premises (@p1533 @p612) :args (@t705))
% 1.51/1.77  (step @p1535 :rule trans :premises (@p1534 @p1009 @p519))
% 1.51/1.77  (step @p1536 :rule cong :premises (@p1535 @p1532) :args ((tptp.meet @t705 @t60)))
% 1.51/1.77  (step @p1537 :rule trans :premises (@p1536 @p1516))
% 1.51/1.77  (step @p1538 :rule symm :premises (@p1536))
% 1.51/1.77  (step @p1539 :rule cong :premises (@p1318 @p530) :args (@t322))
% 1.51/1.77  (step @p1540 :rule trans :premises (@p1539 @p26))
% 1.51/1.77  (step @p1541 :rule cong :premises (@p612 @p1540) :args (@t706))
% 1.51/1.77  (step @p1542 :rule trans :premises (@p1541 @p1538))
% 1.51/1.77  (step @p1543 :rule trans :premises (@p1542 @p1537))
% 1.51/1.77  (step @p1544 :rule cong :premises (@p1543 @p520) :args ((tptp.join @t706 tptp.a)))
% 1.51/1.77  (step @p1545 :rule symm :premises (@p1542))
% 1.51/1.77  (step @p1546 :rule trans :premises (@p1371 @p1364 @p1358 @p1340 @p1329 @p1324 @p1323))
% 1.51/1.77  (step @p1547 :rule trans :premises (@p1490 @p210 @p1369 @p1365))
% 1.51/1.77  (step @p1548 :rule symm :premises (@p164))
% 1.51/1.77  (step @p1549 :rule symm :premises (@p1499))
% 1.51/1.77  (step @p1550 :rule refl :args (@t110))
% 1.51/1.77  (step @p1551 :rule cong :premises (@p1550 @p1549) :args (@t707))
% 1.51/1.77  (step @p1552 :rule trans :premises (@p1551 @p1548 @p1494))
% 1.51/1.77  (step @p1553 :rule trans :premises (@p1552 @p1547 @p1386 @p1546 @p26))
% 1.51/1.77  (step @p1554 :rule cong :premises (@p1553 @p612) :args (@t708))
% 1.51/1.77  (step @p1555 :rule trans :premises (@p1554 @p1518 @p1538))
% 1.51/1.77  (step @p1556 :rule trans :premises (@p1555 @p1545))
% 1.51/1.77  (step @p1557 :rule cong :premises (@p1556 @p520) :args ((tptp.join @t708 tptp.a)))
% 1.51/1.77  (step @p1558 :rule trans :premises (@p1557 @p1544))
% 1.51/1.77  (step @p1559 :rule symm :premises (@p1557))
% 1.51/1.77  (step @p1560 :rule trans :premises (@p246 @p1523 @p1518 @p1538))
% 1.51/1.77  (step @p1561 :rule trans :premises (@p1560 @p1545))
% 1.51/1.77  (step @p1562 :rule cong :premises (@p1561 @p520) :args (@t607))
% 1.51/1.77  (step @p1563 :rule symm :premises (@p291))
% 1.51/1.77  (step @p1564 :rule cong :premises (@p618 @p612) :args (@t119))
% 1.51/1.77  (step @p1565 :rule trans :premises (@p22 @p144 @p966 @p1564))
% 1.51/1.77  (step @p1566 :rule cong :premises (@p1565 @p520) :args (@t60))
% 1.51/1.77  (step @p1567 :rule symm :premises (@p157))
% 1.51/1.77  (step @p1568 :rule trans :premises (@p716 @p30 @p76))
% 1.51/1.77  (step @p1569 :rule cong :premises (@p1532 @p1568) :args (@t447))
% 1.51/1.77  (step @p1570 :rule symm :premises (@p1565))
% 1.51/1.77  (step @p1571 :rule trans :premises (@p1570 @p54))
% 1.51/1.77  (step @p1572 :rule cong :premises (@p1571 @p26) :args (@t609))
% 1.51/1.77  (step @p1573 :rule trans :premises (@p1572 @p214 @p1569 @p1567 @p1566))
% 1.51/1.77  (step @p1574 :rule refl :args (@t183))
% 1.51/1.77  (step @p1575 :rule cong :premises (@p1574 @p1573) :args (@t610))
% 1.51/1.77  (step @p1576 :rule symm :premises (@p1560))
% 1.51/1.77  (step @p1577 :rule cong :premises (@p1393 @p530) :args (@t323))
% 1.51/1.77  (step @p1578 :rule symm :premises (@p101))
% 1.51/1.77  (step @p1579 :rule symm :premises (@p1539))
% 1.51/1.77  (step @p1580 :rule cong :premises (@p520 @p1579) :args (@t165))
% 1.51/1.77  (step @p1581 :rule trans :premises (@p1580 @p1578 @p1577))
% 1.51/1.77  (step @p1582 :rule trans :premises (@p1581 @p26))
% 1.51/1.77  (step @p1583 :rule cong :premises (@p1582 @p612) :args (@t166))
% 1.51/1.77  (step @p1584 :rule trans :premises (@p1583 @p1518 @p1538))
% 1.51/1.77  (step @p1585 :rule trans :premises (@p1584 @p1576))
% 1.51/1.77  (step @p1586 :rule cong :premises (@p1585 @p1396) :args (@t592))
% 1.51/1.77  (step @p1587 :rule symm :premises (@p274))
% 1.51/1.77  (step @p1588 :rule symm :premises (@p1583))
% 1.51/1.77  (step @p1589 :rule cong :premises (@p865 @p1588) :args (@t561))
% 1.51/1.77  (step @p1590 :rule trans :premises (@p26 @p256 @p1589 @p1587 @p1586 @p292 @p1575 @p1563 @p1562 @p1559))
% 1.51/1.77  (step @p1591 :rule trans :premises (@p865 @p1590 @p1558))
% 1.51/1.77  (step @p1592 :rule cong :premises (@p1591 @p595) :args (@t558))
% 1.51/1.77  (step @p1593 :rule cong :premises (@p1582 @p595) :args (@t709))
% 1.51/1.77  (step @p1594 :rule trans :premises (@p1593 @p1592))
% 1.51/1.77  (step @p1595 :rule symm :premises (@p1593))
% 1.51/1.77  (step @p1596 :rule cong :premises (@p1553 @p595) :args (@t710))
% 1.51/1.77  (step @p1597 :rule trans :premises (@p1596 @p1595))
% 1.51/1.77  (step @p1598 :rule trans :premises (@p1597 @p1594))
% 1.51/1.77  (step @p1599 :rule cong :premises (@p1598 @p520) :args ((tptp.join @t710 tptp.a)))
% 1.51/1.77  (step @p1600 :rule symm :premises (@p1597))
% 1.51/1.77  (step @p1601 :rule symm :premises (@p257))
% 1.51/1.77  (step @p1602 :rule symm :premises (@p99))
% 1.51/1.77  (step @p1603 :rule cong :premises (@p595 @p1402) :args (@t122))
% 1.51/1.77  (step @p1604 :rule trans :premises (@p1603 @p1602 @p192))
% 1.51/1.77  (step @p1605 :rule symm :premises (@p77))
% 1.51/1.77  (step @p1606 :rule cong :premises (@p1318 @p595) :args (@t163))
% 1.51/1.77  (step @p1607 :rule cong :premises (@p1606 @p1396) :args (@t164))
% 1.51/1.77  (step @p1608 :rule trans :premises (@p1607 @p1605 @p869 @p866 @p865))
% 1.51/1.77  (step @p1609 :rule trans :premises (@p1608 @p50))
% 1.51/1.77  (step @p1610 :rule cong :premises (@p1609 @p1604) :args (@t586))
% 1.51/1.77  (step @p1611 :rule symm :premises (@p271))
% 1.51/1.77  (step @p1612 :rule symm :premises (@p1608))
% 1.51/1.77  (step @p1613 :rule symm :premises (@p254))
% 1.51/1.77  (step @p1614 :rule symm :premises (@p132))
% 1.51/1.77  (step @p1615 :rule symm :premises (@p195))
% 1.51/1.77  (step @p1616 :rule trans :premises (@p733 @p21))
% 1.51/1.77  (step @p1617 :rule cong :premises (@p520 @p21) :args (@t54))
% 1.51/1.77  (step @p1618 :rule trans :premises (@p733 @p543 @p539 @p1617))
% 1.51/1.77  (step @p1619 :rule cong :premises (@p1618 @p595) :args (@t270))
% 1.51/1.77  (step @p1620 :rule trans :premises (@p27 @p73 @p1619))
% 1.51/1.77  (step @p1621 :rule cong :premises (@p1620 @p1616) :args (@t123))
% 1.51/1.77  (step @p1622 :rule symm :premises (@p212))
% 1.51/1.77  (step @p1623 :rule symm :premises (@p737))
% 1.51/1.77  (step @p1624 :rule trans :premises (@p534 @p24 @p158 @p1623 @p1622 @p1621))
% 1.51/1.77  (step @p1625 :rule cong :premises (@p24 @p1624) :args (@t208))
% 1.51/1.77  (step @p1626 :rule symm :premises (@p867))
% 1.51/1.77  (step @p1627 :rule symm :premises (@p44))
% 1.51/1.77  (step @p1628 :rule symm :premises (@p84))
% 1.51/1.77  (step @p1629 :rule trans :premises (@p1386 @p1546 @p26))
% 1.51/1.77  (step @p1630 :rule cong :premises (@p1629 @p595) :args (@t711))
% 1.51/1.77  (step @p1631 :rule trans :premises (@p1630 @p1628 @p1627 @p1626 @p733 @p31 @p1625 @p1615 @p1614 @p217))
% 1.51/1.77  (step @p1632 :rule refl :args (@t122))
% 1.51/1.77  (step @p1633 :rule cong :premises (@p1632 @p1631) :args (@t712))
% 1.51/1.77  (step @p1634 :rule trans :premises (@p1633 @p1613))
% 1.51/1.77  (step @p1635 :rule cong :premises (@p1634 @p1612) :args ((tptp.join @t712 @t25)))
% 1.51/1.77  (step @p1636 :rule trans :premises (@p1635 @p1611 @p1610 @p1601 @p1384))
% 1.51/1.77  (step @p1637 :rule symm :premises (@p1635))
% 1.51/1.77  (step @p1638 :rule symm :premises (@p1609))
% 1.51/1.77  (step @p1639 :rule cong :premises (@p1632 @p1638) :args ((tptp.join @t122 @t68)))
% 1.51/1.77  (step @p1640 :rule trans :premises (@p1639 @p1637))
% 1.51/1.77  (step @p1641 :rule symm :premises (@p1639))
% 1.51/1.77  (step @p1642 :rule symm :premises (@p72))
% 1.51/1.77  (step @p1643 :rule cong :premises (@p1642 @p1612) :args (@t625))
% 1.51/1.77  (step @p1644 :rule trans :premises (@p1643 @p1641))
% 1.51/1.77  (step @p1645 :rule trans :premises (@p1644 @p1640 @p1636 @p26))
% 1.51/1.77  (step @p1646 :rule cong :premises (@p1645 @p595) :args (@t626))
% 1.51/1.77  (step @p1647 :rule trans :premises (@p1646 @p1595))
% 1.51/1.77  (step @p1648 :rule trans :premises (@p1647 @p1600))
% 1.51/1.77  (step @p1649 :rule cong :premises (@p1648 @p1326) :args (@t627))
% 1.51/1.77  (step @p1650 :rule symm :premises (@p295))
% 1.51/1.77  (step @p1651 :rule cong :premises (@p1396 @p1326) :args (@t257))
% 1.51/1.77  (step @p1652 :rule trans :premises (@p65 @p1651))
% 1.51/1.77  (step @p1653 :rule symm :premises (@p869))
% 1.51/1.77  (step @p1654 :rule trans :premises (@p26 @p146 @p1653 @p77))
% 1.51/1.77  (step @p1655 :rule trans :premises (@p865 @p1654))
% 1.51/1.77  (step @p1656 :rule cong :premises (@p1655 @p595) :args (@t289))
% 1.51/1.77  (step @p1657 :rule trans :premises (@p24 @p867 @p44 @p84 @p1656))
% 1.51/1.77  (step @p1658 :rule cong :premises (@p1657 @p1652) :args (@t278))
% 1.51/1.77  (step @p1659 :rule trans :premises (@p26 @p146 @p1653 @p77 @p1658 @p1650 @p1649 @p1599))
% 1.51/1.77  (step @p1660 :rule trans :premises (@p865 @p1659))
% 1.51/1.77  (step @p1661 :rule cong :premises (@p1660 @p1531) :args (@t599))
% 1.51/1.77  (step @p1662 :rule trans :premises (@p1661 @p1515 @p1514 @p1312 @p245 @p1292))
% 1.51/1.77  (step @p1663 :rule trans :premises (@p1662 @p1291))
% 1.51/1.77  (step @p1664 :rule cong :premises (@p1663 @p1168) :args (@t600))
% 1.51/1.77  (step @p1665 :rule symm :premises (@p278))
% 1.51/1.77  (step @p1666 :rule cong :premises (@p595 @p714) :args (@t203))
% 1.51/1.77  (step @p1667 :rule trans :premises (@p28 @p1666))
% 1.51/1.77  (step @p1668 :rule refl :args (@t148))
% 1.51/1.77  (step @p1669 :rule trans :premises (@p30 @p95))
% 1.51/1.77  (step @p1670 :rule cong :premises (@p1669 @p595) :args (@t137))
% 1.51/1.77  (step @p1671 :rule trans :premises (@p20 @p38 @p1670))
% 1.51/1.77  (step @p1672 :rule cong :premises (@p1671 @p1668) :args (@t310))
% 1.51/1.77  (step @p1673 :rule trans :premises (@p30 @p95 @p1672))
% 1.51/1.77  (step @p1674 :rule cong :premises (@p1673 @p1667) :args (@t137))
% 1.51/1.77  (step @p1675 :rule trans :premises (@p20 @p38 @p1674 @p240))
% 1.51/1.77  (step @p1676 :rule cong :premises (@p1532 @p1675) :args (@t558))
% 1.51/1.77  (step @p1677 :rule trans :premises (@p1593 @p1676 @p1665 @p1664 @p304 @p1167 @p277 @p935 @p879 @p876 @p875 @p873))
% 1.51/1.77  (step @p1678 :rule symm :premises (@p870))
% 1.51/1.77  (step @p1679 :rule cong :premises (@p1678 @p1677) :args ((tptp.join @t25 @t709)))
% 1.51/1.77  (step @p1680 :rule cong :premises (@p865 @p1595) :args (@t559))
% 1.51/1.77  (step @p1681 :rule trans :premises (@p26 @p255 @p1680 @p1679 @p303 @p872 @p864 @p852 @p851 @p273 @p831 @p216 @p643 @p243 @p580))
% 1.51/1.77  (step-pop @p2132 :rule scope :premises (@p1681))
% 1.51/1.77  (step-pop @p2133 :rule scope :premises (@p2132))
% 1.51/1.77  (step-pop @p2134 :rule scope :premises (@p2133))
% 1.51/1.77  (step-pop @p2135 :rule scope :premises (@p2134))
% 1.51/1.77  (step-pop @p2136 :rule scope :premises (@p2135))
% 1.51/1.77  (step-pop @p2137 :rule scope :premises (@p2136))
% 1.51/1.77  (step-pop @p2138 :rule scope :premises (@p2137))
% 1.51/1.77  (step-pop @p2139 :rule scope :premises (@p2138))
% 1.51/1.77  (step-pop @p2140 :rule scope :premises (@p2139))
% 1.51/1.77  (step-pop @p2141 :rule scope :premises (@p2140))
% 1.51/1.77  (step-pop @p2142 :rule scope :premises (@p2141))
% 1.51/1.77  (step-pop @p2143 :rule scope :premises (@p2142))
% 1.51/1.77  (step-pop @p2144 :rule scope :premises (@p2143))
% 1.51/1.77  (step-pop @p2145 :rule scope :premises (@p2144))
% 1.51/1.77  (step-pop @p2146 :rule scope :premises (@p2145))
% 1.51/1.77  (step-pop @p2147 :rule scope :premises (@p2146))
% 1.51/1.77  (step-pop @p2148 :rule scope :premises (@p2147))
% 1.51/1.77  (step-pop @p2149 :rule scope :premises (@p2148))
% 1.51/1.77  (step-pop @p2150 :rule scope :premises (@p2149))
% 1.51/1.77  (step-pop @p2151 :rule scope :premises (@p2150))
% 1.51/1.77  (step-pop @p2152 :rule scope :premises (@p2151))
% 1.51/1.77  (step-pop @p2153 :rule scope :premises (@p2152))
% 1.51/1.77  (step-pop @p2154 :rule scope :premises (@p2153))
% 1.51/1.77  (step-pop @p2155 :rule scope :premises (@p2154))
% 1.51/1.77  (step-pop @p2156 :rule scope :premises (@p2155))
% 1.51/1.77  (step-pop @p2157 :rule scope :premises (@p2156))
% 1.51/1.77  (step-pop @p2158 :rule scope :premises (@p2157))
% 1.51/1.77  (step-pop @p2159 :rule scope :premises (@p2158))
% 1.51/1.77  (step-pop @p2160 :rule scope :premises (@p2159))
% 1.51/1.77  (step-pop @p2161 :rule scope :premises (@p2160))
% 1.51/1.77  (step-pop @p2162 :rule scope :premises (@p2161))
% 1.51/1.77  (step-pop @p2163 :rule scope :premises (@p2162))
% 1.51/1.77  (step-pop @p2164 :rule scope :premises (@p2163))
% 1.51/1.77  (step-pop @p2165 :rule scope :premises (@p2164))
% 1.51/1.77  (step-pop @p2166 :rule scope :premises (@p2165))
% 1.51/1.77  (step-pop @p2167 :rule scope :premises (@p2166))
% 1.51/1.77  (step-pop @p2168 :rule scope :premises (@p2167))
% 1.51/1.77  (step-pop @p2169 :rule scope :premises (@p2168))
% 1.51/1.77  (step-pop @p2170 :rule scope :premises (@p2169))
% 1.51/1.77  (step-pop @p2171 :rule scope :premises (@p2170))
% 1.51/1.77  (step-pop @p2172 :rule scope :premises (@p2171))
% 1.51/1.77  (step-pop @p2173 :rule scope :premises (@p2172))
% 1.51/1.77  (step-pop @p2174 :rule scope :premises (@p2173))
% 1.51/1.77  (step-pop @p2175 :rule scope :premises (@p2174))
% 1.51/1.77  (step-pop @p2176 :rule scope :premises (@p2175))
% 1.51/1.77  (step-pop @p2177 :rule scope :premises (@p2176))
% 1.51/1.77  (step-pop @p2178 :rule scope :premises (@p2177))
% 1.51/1.77  (step-pop @p2179 :rule scope :premises (@p2178))
% 1.51/1.77  (step-pop @p2180 :rule scope :premises (@p2179))
% 1.51/1.77  (step-pop @p2181 :rule scope :premises (@p2180))
% 1.51/1.77  (step-pop @p2182 :rule scope :premises (@p2181))
% 1.51/1.77  (step-pop @p2183 :rule scope :premises (@p2182))
% 1.51/1.77  (step-pop @p2184 :rule scope :premises (@p2183))
% 1.51/1.77  (step-pop @p2185 :rule scope :premises (@p2184))
% 1.51/1.77  (step-pop @p2186 :rule scope :premises (@p2185))
% 1.51/1.77  (step-pop @p2187 :rule scope :premises (@p2186))
% 1.51/1.77  (step-pop @p2188 :rule scope :premises (@p2187))
% 1.51/1.77  (step-pop @p2189 :rule scope :premises (@p2188))
% 1.51/1.77  (step-pop @p2190 :rule scope :premises (@p2189))
% 1.51/1.77  (step-pop @p2191 :rule scope :premises (@p2190))
% 1.51/1.77  (step-pop @p2192 :rule scope :premises (@p2191))
% 1.51/1.77  (step-pop @p2193 :rule scope :premises (@p2192))
% 1.51/1.77  (step-pop @p2194 :rule scope :premises (@p2193))
% 1.51/1.77  (step-pop @p2195 :rule scope :premises (@p2194))
% 1.51/1.77  (step-pop @p2196 :rule scope :premises (@p2195))
% 1.51/1.77  (step-pop @p2197 :rule scope :premises (@p2196))
% 1.51/1.77  (step-pop @p2198 :rule scope :premises (@p2197))
% 1.51/1.77  (step-pop @p2199 :rule scope :premises (@p2198))
% 1.51/1.77  (step-pop @p2200 :rule scope :premises (@p2199))
% 1.51/1.77  (step-pop @p2201 :rule scope :premises (@p2200))
% 1.51/1.77  (step-pop @p2202 :rule scope :premises (@p2201))
% 1.51/1.77  (step-pop @p2203 :rule scope :premises (@p2202))
% 1.51/1.77  (step-pop @p2204 :rule scope :premises (@p2203))
% 1.51/1.77  (step-pop @p2205 :rule scope :premises (@p2204))
% 1.51/1.77  (step-pop @p2206 :rule scope :premises (@p2205))
% 1.51/1.77  (step-pop @p2207 :rule scope :premises (@p2206))
% 1.51/1.77  (step-pop @p2208 :rule scope :premises (@p2207))
% 1.51/1.77  (step-pop @p2209 :rule scope :premises (@p2208))
% 1.51/1.77  (step-pop @p2210 :rule scope :premises (@p2209))
% 1.51/1.77  (step-pop @p2211 :rule scope :premises (@p2210))
% 1.51/1.77  (step-pop @p2212 :rule scope :premises (@p2211))
% 1.51/1.77  (step-pop @p2213 :rule scope :premises (@p2212))
% 1.51/1.77  (step-pop @p2214 :rule scope :premises (@p2213))
% 1.51/1.77  (step-pop @p2215 :rule scope :premises (@p2214))
% 1.51/1.77  (step-pop @p2216 :rule scope :premises (@p2215))
% 1.51/1.77  (step-pop @p2217 :rule scope :premises (@p2216))
% 1.51/1.77  (step-pop @p2218 :rule scope :premises (@p2217))
% 1.51/1.77  (step-pop @p2219 :rule scope :premises (@p2218))
% 1.51/1.77  (step-pop @p2220 :rule scope :premises (@p2219))
% 1.51/1.77  (step-pop @p2221 :rule scope :premises (@p2220))
% 1.51/1.77  (step-pop @p2222 :rule scope :premises (@p2221))
% 1.51/1.77  (step-pop @p2223 :rule scope :premises (@p2222))
% 1.51/1.77  (step-pop @p2224 :rule scope :premises (@p2223))
% 1.51/1.77  (step-pop @p2225 :rule scope :premises (@p2224))
% 1.51/1.77  (step-pop @p2226 :rule scope :premises (@p2225))
% 1.51/1.77  (step-pop @p2227 :rule scope :premises (@p2226))
% 1.51/1.77  (step-pop @p2228 :rule scope :premises (@p2227))
% 1.51/1.77  (step-pop @p2229 :rule scope :premises (@p2228))
% 1.51/1.77  (step-pop @p2230 :rule scope :premises (@p2229))
% 1.51/1.77  (step-pop @p2231 :rule scope :premises (@p2230))
% 1.51/1.77  (step-pop @p2232 :rule scope :premises (@p2231))
% 1.51/1.77  (step-pop @p2233 :rule scope :premises (@p2232))
% 1.51/1.77  (step-pop @p2234 :rule scope :premises (@p2233))
% 1.51/1.77  (step-pop @p2235 :rule scope :premises (@p2234))
% 1.51/1.77  (step-pop @p2236 :rule scope :premises (@p2235))
% 1.51/1.77  (step-pop @p2237 :rule scope :premises (@p2236))
% 1.51/1.77  (step-pop @p2238 :rule scope :premises (@p2237))
% 1.51/1.77  (step-pop @p2239 :rule scope :premises (@p2238))
% 1.51/1.77  (step-pop @p2240 :rule scope :premises (@p2239))
% 1.51/1.77  (step-pop @p2241 :rule scope :premises (@p2240))
% 1.51/1.77  (step-pop @p2242 :rule scope :premises (@p2241))
% 1.51/1.77  (step-pop @p2243 :rule scope :premises (@p2242))
% 1.51/1.77  (step-pop @p2244 :rule scope :premises (@p2243))
% 1.51/1.77  (step-pop @p2245 :rule scope :premises (@p2244))
% 1.51/1.77  (step-pop @p2246 :rule scope :premises (@p2245))
% 1.51/1.77  (step-pop @p2247 :rule scope :premises (@p2246))
% 1.51/1.77  (step-pop @p2248 :rule scope :premises (@p2247))
% 1.51/1.77  (step-pop @p2249 :rule scope :premises (@p2248))
% 1.51/1.77  (step-pop @p2250 :rule scope :premises (@p2249))
% 1.51/1.77  (step-pop @p2251 :rule scope :premises (@p2250))
% 1.51/1.77  (step-pop @p2252 :rule scope :premises (@p2251))
% 1.51/1.77  (step-pop @p2253 :rule scope :premises (@p2252))
% 1.51/1.77  (step-pop @p2254 :rule scope :premises (@p2253))
% 1.51/1.77  (step-pop @p2255 :rule scope :premises (@p2254))
% 1.51/1.77  (step-pop @p2256 :rule scope :premises (@p2255))
% 1.51/1.77  (step-pop @p2257 :rule scope :premises (@p2256))
% 1.51/1.77  (step-pop @p2258 :rule scope :premises (@p2257))
% 1.51/1.77  (step-pop @p2259 :rule scope :premises (@p2258))
% 1.51/1.77  (step-pop @p2260 :rule scope :premises (@p2259))
% 1.51/1.77  (step-pop @p2261 :rule scope :premises (@p2260))
% 1.51/1.77  (step-pop @p2262 :rule scope :premises (@p2261))
% 1.51/1.77  (step-pop @p2263 :rule scope :premises (@p2262))
% 1.51/1.77  (step-pop @p2264 :rule scope :premises (@p2263))
% 1.51/1.77  (step-pop @p2265 :rule scope :premises (@p2264))
% 1.51/1.77  (step-pop @p2266 :rule scope :premises (@p2265))
% 1.51/1.77  (step-pop @p2267 :rule scope :premises (@p2266))
% 1.51/1.77  (step-pop @p2268 :rule scope :premises (@p2267))
% 1.51/1.77  (step-pop @p2269 :rule scope :premises (@p2268))
% 1.51/1.77  (step-pop @p2270 :rule scope :premises (@p2269))
% 1.51/1.77  (step-pop @p2271 :rule scope :premises (@p2270))
% 1.51/1.77  (step-pop @p2272 :rule scope :premises (@p2271))
% 1.51/1.77  (step-pop @p2273 :rule scope :premises (@p2272))
% 1.51/1.77  (step-pop @p2274 :rule scope :premises (@p2273))
% 1.51/1.77  (step-pop @p2275 :rule scope :premises (@p2274))
% 1.51/1.77  (step-pop @p2276 :rule scope :premises (@p2275))
% 1.51/1.77  (step-pop @p2277 :rule scope :premises (@p2276))
% 1.51/1.77  (step-pop @p2278 :rule scope :premises (@p2277))
% 1.51/1.77  (step-pop @p2279 :rule scope :premises (@p2278))
% 1.51/1.77  (step-pop @p2280 :rule scope :premises (@p2279))
% 1.51/1.77  (step-pop @p2281 :rule scope :premises (@p2280))
% 1.51/1.77  (step-pop @p2282 :rule scope :premises (@p2281))
% 1.51/1.77  (step-pop @p2283 :rule scope :premises (@p2282))
% 1.51/1.77  (step-pop @p2284 :rule scope :premises (@p2283))
% 1.51/1.77  (step-pop @p2285 :rule scope :premises (@p2284))
% 1.51/1.77  (step-pop @p2286 :rule scope :premises (@p2285))
% 1.51/1.77  (step-pop @p2287 :rule scope :premises (@p2286))
% 1.51/1.77  (step-pop @p2288 :rule scope :premises (@p2287))
% 1.51/1.77  (step-pop @p2289 :rule scope :premises (@p2288))
% 1.51/1.77  (step-pop @p2290 :rule scope :premises (@p2289))
% 1.51/1.77  (step-pop @p2291 :rule scope :premises (@p2290))
% 1.51/1.77  (step-pop @p2292 :rule scope :premises (@p2291))
% 1.51/1.77  (step-pop @p2293 :rule scope :premises (@p2292))
% 1.51/1.77  (step-pop @p2294 :rule scope :premises (@p2293))
% 1.51/1.77  (step-pop @p2295 :rule scope :premises (@p2294))
% 1.51/1.77  (step-pop @p2296 :rule scope :premises (@p2295))
% 1.51/1.77  (step-pop @p2297 :rule scope :premises (@p2296))
% 1.51/1.77  (step-pop @p2298 :rule scope :premises (@p2297))
% 1.51/1.77  (step-pop @p2299 :rule scope :premises (@p2298))
% 1.51/1.77  (step-pop @p2300 :rule scope :premises (@p2299))
% 1.51/1.77  (step-pop @p2301 :rule scope :premises (@p2300))
% 1.51/1.77  (step-pop @p2302 :rule scope :premises (@p2301))
% 1.51/1.77  (step-pop @p2303 :rule scope :premises (@p2302))
% 1.51/1.77  (step-pop @p2304 :rule scope :premises (@p2303))
% 1.51/1.77  (step-pop @p2305 :rule scope :premises (@p2304))
% 1.51/1.77  (step-pop @p2306 :rule scope :premises (@p2305))
% 1.51/1.77  (step-pop @p2307 :rule scope :premises (@p2306))
% 1.51/1.77  (step-pop @p2308 :rule scope :premises (@p2307))
% 1.51/1.77  (step-pop @p2309 :rule scope :premises (@p2308))
% 1.51/1.77  (step-pop @p2310 :rule scope :premises (@p2309))
% 1.51/1.77  (step-pop @p2311 :rule scope :premises (@p2310))
% 1.51/1.77  (step-pop @p2312 :rule scope :premises (@p2311))
% 1.51/1.77  (step-pop @p2313 :rule scope :premises (@p2312))
% 1.51/1.77  (step-pop @p2314 :rule scope :premises (@p2313))
% 1.51/1.77  (step-pop @p2315 :rule scope :premises (@p2314))
% 1.51/1.77  (step-pop @p2316 :rule scope :premises (@p2315))
% 1.51/1.77  (step-pop @p2317 :rule scope :premises (@p2316))
% 1.51/1.77  (step-pop @p2318 :rule scope :premises (@p2317))
% 1.51/1.77  (step-pop @p2319 :rule scope :premises (@p2318))
% 1.51/1.77  (step-pop @p2320 :rule scope :premises (@p2319))
% 1.51/1.77  (step-pop @p2321 :rule scope :premises (@p2320))
% 1.51/1.77  (step-pop @p2322 :rule scope :premises (@p2321))
% 1.51/1.77  (step-pop @p2323 :rule scope :premises (@p2322))
% 1.51/1.77  (step-pop @p2324 :rule scope :premises (@p2323))
% 1.51/1.77  (step-pop @p2325 :rule scope :premises (@p2324))
% 1.51/1.77  (step-pop @p2326 :rule scope :premises (@p2325))
% 1.51/1.77  (step-pop @p2327 :rule scope :premises (@p2326))
% 1.51/1.77  (step-pop @p2328 :rule scope :premises (@p2327))
% 1.51/1.77  (step-pop @p2329 :rule scope :premises (@p2328))
% 1.51/1.77  (step-pop @p2330 :rule scope :premises (@p2329))
% 1.51/1.77  (step-pop @p2331 :rule scope :premises (@p2330))
% 1.51/1.77  (step-pop @p2332 :rule scope :premises (@p2331))
% 1.51/1.77  (step-pop @p2333 :rule scope :premises (@p2332))
% 1.51/1.77  (step-pop @p2334 :rule scope :premises (@p2333))
% 1.51/1.77  (step-pop @p2335 :rule scope :premises (@p2334))
% 1.51/1.77  (step-pop @p2336 :rule scope :premises (@p2335))
% 1.51/1.77  (step-pop @p2337 :rule scope :premises (@p2336))
% 1.51/1.77  (step-pop @p2338 :rule scope :premises (@p2337))
% 1.51/1.77  (step-pop @p2339 :rule scope :premises (@p2338))
% 1.51/1.77  (step-pop @p2340 :rule scope :premises (@p2339))
% 1.51/1.77  (step-pop @p2341 :rule scope :premises (@p2340))
% 1.51/1.77  (step-pop @p2342 :rule scope :premises (@p2341))
% 1.51/1.77  (step-pop @p2343 :rule scope :premises (@p2342))
% 1.51/1.77  (step-pop @p2344 :rule scope :premises (@p2343))
% 1.51/1.77  (step-pop @p2345 :rule scope :premises (@p2344))
% 1.51/1.77  (step @p1682 :rule process_scope :premises (@p2345) :args (@t26))
% 1.51/1.77  (step @p1897 :rule implies_elim :premises (@p1682))
% 1.51/1.77  (step @p1898 :rule cnf_and_neg :args (@t713))
% 1.51/1.77  (step @p1899 :rule resolution :premises (@p1898 @p1897) :args (true @t713))
% 1.51/1.77  (step @p1900 :rule reordering :premises (@p1899) :args ((or @t26 (not @t191) (not @t192) (not @t193) (not @t194) (not @t195) (not @t196) (not @t197) (not @t198) (not @t199) (not @t200) (not @t202) (not @t204) (not @t205) (not @t207) (not @t209) (not @t211) (not @t213) (not @t214) (not @t216) (not @t218) (not @t219) (not @t220) (not @t221) (not @t223) (not @t226) (not @t228) (not @t230) (not @t232) (not @t234) (not @t237) (not @t238) (not @t239) (not @t240) (not @t241) (not @t243) (not @t245) (not @t247) (not @t248) (not @t250) (not @t252) (not @t254) (not @t256) (not @t258) (not @t259) (not @t260) (not @t261) (not @t263) (not @t265) (not @t267) (not @t269) (not @t271) (not @t273) (not @t275) (not @t277) (not @t279) (not @t280) (not @t282) (not @t283) (not @t285) (not @t286) (not @t288) (not @t290) (not @t292) (not @t294) (not @t296) (not @t297) (not @t299) (not @t300) (not @t301) (not @t303) (not @t306) (not @t309) (not @t311) (not @t313) (not @t314) (not @t317) (not @t319) (not @t321) (not @t324) (not @t327) (not @t74) (not @t82) (not @t87) (not @t330) (not @t333) (not @t339) (not @t343) (not @t349) (not @t353) (not @t359) (not @t365) (not @t371) (not @t377) (not @t378) (not @t380) (not @t382) (not @t383) (not @t384) (not @t385) (not @t386) (not @t388) (not @t389) (not @t390) (not @t392) (not @t393) (not @t395) (not @t396) (not @t398) (not @t400) (not @t401) (not @t402) (not @t403) (not @t404) (not @t405) (not @t407) (not @t408) (not @t409) (not @t411) (not @t117) (not @t121) (not @t413) (not @t415) (not @t418) (not @t421) (not @t423) (not @t425) (not @t426) (not @t428) (not @t429) (not @t431) (not @t432) (not @t434) (not @t436) (not @t437) (not @t131) (not @t439) (not @t441) (not @t442) (not @t444) (not @t446) (not @t448) (not @t449) (not @t451) (not @t453) (not @t455) (not @t457) (not @t459) (not @t461) (not @t463) (not @t466) (not @t468) (not @t470) (not @t473) (not @t476) (not @t145) (not @t478) (not @t484) (not @t486) (not @t488) (not @t493) (not @t499) (not @t505) (not @t513) (not @t518) (not @t523) (not @t530) (not @t536) (not @t543) (not @t550) (not @t552) (not @t554) (not @t556) (not @t557) (not @t560) (not @t562) (not @t563) (not @t564) (not @t565) (not @t566) (not @t568) (not @t570) (not @t572) (not @t574) (not @t576) (not @t577) (not @t579) (not @t581) (not @t583) (not @t585) (not @t587) (not @t589) (not @t591) (not @t593) (not @t595) (not @t596) (not @t598) (not @t601) (not @t180) (not @t604) (not @t606) (not @t608) (not @t611) (not @t618) (not @t624) (not @t628) (not @t632) (not @t638) (not @t644) (not @t650) (not @t656) (not @t658) (not @t660) (not @t662) (not @t665))))
% 1.51/1.77  (step @p1901 false :rule chain_m_resolution :premises (@p1900 @p304 @p303 @p302 @p301 @p300 @p299 @p298 @p297 @p296 @p295 @p294 @p293 @p292 @p291 @p290 @p289 @p288 @p278 @p277 @p276 @p275 @p274 @p273 @p272 @p271 @p270 @p269 @p268 @p267 @p266 @p265 @p264 @p263 @p262 @p261 @p260 @p259 @p258 @p257 @p256 @p255 @p254 @p253 @p252 @p251 @p250 @p249 @p248 @p247 @p246 @p245 @p244 @p243 @p242 @p241 @p240 @p239 @p238 @p237 @p236 @p227 @p226 @p225 @p224 @p223 @p222 @p221 @p220 @p219 @p218 @p217 @p216 @p215 @p214 @p213 @p212 @p211 @p210 @p209 @p208 @p198 @p197 @p196 @p195 @p194 @p193 @p192 @p191 @p190 @p189 @p188 @p187 @p186 @p185 @p184 @p175 @p165 @p164 @p163 @p162 @p161 @p160 @p159 @p158 @p157 @p156 @p155 @p154 @p153 @p152 @p151 @p150 @p149 @p148 @p147 @p146 @p145 @p144 @p143 @p142 @p141 @p140 @p139 @p138 @p137 @p136 @p135 @p134 @p133 @p132 @p131 @p130 @p121 @p112 @p102 @p101 @p100 @p99 @p98 @p97 @p96 @p95 @p94 @p93 @p92 @p91 @p90 @p89 @p88 @p87 @p86 @p85 @p84 @p83 @p82 @p81 @p80 @p79 @p78 @p77 @p76 @p75 @p74 @p73 @p72 @p71 @p70 @p69 @p68 @p67 @p66 @p65 @p64 @p63 @p62 @p61 @p60 @p59 @p58 @p57 @p56 @p55 @p54 @p50 @p46 @p45 @p44 @p43 @p42 @p41 @p40 @p39 @p38 @p37 @p36 @p35 @p34 @p33 @p32 @p31 @p30 @p29 @p28 @p27 @p26 @p25 @p24 @p23 @p22 @p21 @p20 @p16 @p15 @p14 @p10) :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 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 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 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 false false true) (@list @t665 @t662 @t660 @t658 @t656 @t650 @t644 @t638 @t632 @t628 @t624 @t618 @t611 @t608 @t606 @t604 @t180 @t601 @t598 @t596 @t595 @t593 @t591 @t589 @t587 @t585 @t583 @t581 @t579 @t577 @t576 @t574 @t572 @t570 @t568 @t566 @t565 @t564 @t563 @t562 @t560 @t557 @t556 @t554 @t552 @t550 @t543 @t536 @t530 @t523 @t518 @t513 @t505 @t499 @t493 @t488 @t486 @t484 @t478 @t145 @t476 @t473 @t470 @t468 @t466 @t463 @t461 @t459 @t457 @t455 @t453 @t451 @t449 @t448 @t446 @t444 @t442 @t441 @t439 @t131 @t437 @t436 @t434 @t432 @t431 @t429 @t428 @t426 @t425 @t423 @t421 @t418 @t415 @t413 @t121 @t117 @t411 @t409 @t408 @t407 @t405 @t404 @t403 @t402 @t401 @t400 @t398 @t396 @t395 @t393 @t392 @t390 @t389 @t388 @t386 @t385 @t384 @t383 @t382 @t380 @t378 @t377 @t371 @t365 @t359 @t353 @t349 @t343 @t339 @t333 @t330 @t87 @t82 @t74 @t327 @t324 @t321 @t319 @t317 @t314 @t313 @t311 @t309 @t306 @t303 @t301 @t300 @t299 @t297 @t296 @t294 @t292 @t290 @t288 @t286 @t285 @t283 @t282 @t280 @t279 @t277 @t275 @t273 @t271 @t269 @t267 @t265 @t263 @t261 @t260 @t259 @t258 @t256 @t254 @t252 @t250 @t248 @t247 @t245 @t243 @t241 @t240 @t239 @t238 @t237 @t234 @t232 @t230 @t228 @t226 @t223 @t221 @t220 @t219 @t218 @t216 @t214 @t213 @t211 @t209 @t207 @t205 @t204 @t202 @t200 @t199 @t198 @t197 @t196 @t195 @t194 @t193 @t192 @t191 @t26)))
% 1.51/1.77  )
% 1.51/1.77  % SZS output end Proof
% 1.51/1.77  % cvc5 exiting
%------------------------------------------------------------------------------