%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP081^1 : TPTP v9.2.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n001.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:25:00 AM UTC 2026 % Result : Theorem 0.48s 0.93s % Output : Proof 0.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP081^1 : TPTP v9.2.1. Released v7.5.0. % 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.16/0.35 % Computer : n001.cluster.edu % 0.16/0.35 % Model : x86_64 x86_64 % 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.35 % Memory : 8042.1875MB % 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.35 % CPULimit : 300 % 0.16/0.35 % WCLimit : 300 % 0.16/0.35 % DateTime : Tue Jun 2 04:14:20 EDT 2026 % 0.16/0.35 % CPUTime : % 0.39/0.62 %----Proving TH0 % 0.48/0.93 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 0.48/0.93 % SZS status Theorem % 0.48/0.93 % SZS output start Proof % 0.48/0.93 ( % 0.48/0.93 (declare-sort tptp.set_val 0) % 0.48/0.93 (declare-sort tptp.list_val 0) % 0.48/0.93 (declare-sort tptp.val 0) % 0.48/0.93 (declare-sort tptp.g 0) % 0.48/0.93 (declare-sort tptp.list_node 0) % 0.48/0.93 (declare-sort tptp.node 0) % 0.48/0.93 (declare-sort tptp.list_P561207620_edgeD 0) % 0.48/0.93 (declare-sort tptp.list_list_node 0) % 0.48/0.93 (declare-sort tptp.set_node 0) % 0.48/0.93 (declare-sort tptp.produc1432036078de_val 0) % 0.48/0.93 (declare-sort tptp.option_list_val 0) % 0.48/0.93 (declare-sort tptp.set_list_node 0) % 0.48/0.93 (declare-const tptp.append_node (-> tptp.list_node tptp.list_node tptp.list_node)) % 0.48/0.93 (declare-const tptp.ord_less_eq_set_val (-> tptp.set_val tptp.set_val Bool)) % 0.48/0.93 (declare-const tptp.hd_val (-> tptp.list_val tptp.val)) % 0.48/0.93 (declare-const tptp.finite_finite_node (-> tptp.set_node Bool)) % 0.48/0.93 (declare-const tptp.finite_finite_val (-> tptp.set_val Bool)) % 0.48/0.93 (declare-const tptp.hd_node (-> tptp.list_node tptp.node)) % 0.48/0.93 (declare-const tptp.ord_less_eq_set_node (-> tptp.set_node tptp.set_node Bool)) % 0.48/0.93 (declare-const tptp.collect_node (-> (-> tptp.node Bool) tptp.set_node)) % 0.48/0.93 (declare-const tptp.collect_val (-> (-> tptp.val Bool) tptp.set_val)) % 0.48/0.93 (declare-const tptp.nil_val tptp.list_val) % 0.48/0.93 (declare-const tptp.s tptp.val) % 0.48/0.93 (declare-const tptp.prefix_node (-> tptp.list_node tptp.list_node Bool)) % 0.48/0.93 (declare-const tptp.ms tptp.list_node) % 0.48/0.93 (declare-const tptp.set_val2 (-> tptp.list_val tptp.set_val)) % 0.48/0.93 (declare-const tptp.tl_val (-> tptp.list_val tptp.list_val)) % 0.48/0.93 (declare-const tptp.graph_435229452_edgeD (-> (-> tptp.g tptp.list_node) (-> tptp.g Bool) (-> tptp.g tptp.node tptp.list_P561207620_edgeD) tptp.g tptp.list_node Bool)) % 0.48/0.93 (declare-const tptp.member_list_node (-> tptp.list_node tptp.set_list_node Bool)) % 0.48/0.93 (declare-const tptp.set_list_node2 (-> tptp.list_list_node tptp.set_list_node)) % 0.48/0.93 (declare-const tptp.tl_list_node (-> tptp.list_list_node tptp.list_list_node)) % 0.48/0.93 (declare-const tptp.butlast_list_node (-> tptp.list_list_node tptp.list_list_node)) % 0.48/0.93 (declare-const tptp.inEdges (-> tptp.g tptp.node tptp.list_P561207620_edgeD)) % 0.48/0.93 (declare-const tptp.n tptp.node) % 0.48/0.93 (declare-const tptp.cons_list_node (-> tptp.list_node tptp.list_list_node tptp.list_list_node)) % 0.48/0.93 (declare-const tptp.ns tptp.list_node) % 0.48/0.93 (declare-const tptp.sSA_CF551432799de_val (-> (-> tptp.g tptp.list_node) (-> tptp.g tptp.node tptp.set_val) (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val) tptp.g tptp.val tptp.node)) % 0.48/0.93 (declare-const tptp.invar (-> tptp.g Bool)) % 0.48/0.93 (declare-const tptp.i tptp.node) % 0.48/0.93 (declare-const tptp.alpha_n (-> tptp.g tptp.list_node)) % 0.48/0.93 (declare-const tptp.tl_node (-> tptp.list_node tptp.list_node)) % 0.48/0.93 (declare-const tptp.defs (-> tptp.g tptp.node tptp.set_val)) % 0.48/0.93 (declare-const tptp.graph_1012773594_edgeD (-> (-> tptp.g tptp.list_node) (-> tptp.g Bool) (-> tptp.g tptp.node tptp.list_P561207620_edgeD) tptp.g tptp.node tptp.list_node tptp.node Bool)) % 0.48/0.93 (declare-const tptp.phis (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val)) % 0.48/0.93 (declare-const tptp.append_val (-> tptp.list_val tptp.list_val tptp.list_val)) % 0.48/0.93 (declare-const tptp.g2 tptp.g) % 0.48/0.93 (declare-const tptp.r tptp.val) % 0.48/0.93 (declare-const tptp.phi_r tptp.val) % 0.48/0.93 (declare-const tptp.cons_val (-> tptp.val tptp.list_val tptp.list_val)) % 0.48/0.93 (declare-const tptp.ri tptp.list_node) % 0.48/0.93 (declare-const tptp.cons_node (-> tptp.node tptp.list_node tptp.list_node)) % 0.48/0.93 (declare-const tptp.pred_phi_r tptp.node) % 0.48/0.93 (declare-const tptp.sSA_CF1252180629de_val (-> (-> tptp.g tptp.list_node) (-> tptp.g tptp.node tptp.set_val) (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val) tptp.g tptp.val tptp.val Bool)) % 0.48/0.93 (declare-const tptp.nil_list_node tptp.list_list_node) % 0.48/0.93 (declare-const tptp.rs tptp.list_node) % 0.48/0.93 (declare-const tptp.nil_node tptp.list_node) % 0.48/0.93 (declare-const tptp.rs2 tptp.list_node) % 0.48/0.93 (declare-const tptp.butlast_val (-> tptp.list_val tptp.list_val)) % 0.48/0.93 (declare-const tptp.ms2 tptp.list_node) % 0.48/0.93 (declare-const tptp.butlast_node (-> tptp.list_node tptp.list_node)) % 0.48/0.93 (declare-const tptp.m tptp.node) % 0.48/0.93 (declare-const tptp.sSA_CF848637139eD_val (-> (-> tptp.g tptp.list_node) (-> tptp.g tptp.node tptp.list_P561207620_edgeD) (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val) tptp.g tptp.node tptp.set_val)) % 0.48/0.93 (declare-const tptp.set_node2 (-> tptp.list_node tptp.set_node)) % 0.48/0.93 (declare-const tptp.graph_272749361_edgeD (-> (-> tptp.g tptp.node tptp.list_P561207620_edgeD) tptp.g tptp.node tptp.list_node)) % 0.48/0.93 (declare-const tptp.member_node (-> tptp.node tptp.set_node Bool)) % 0.48/0.93 (declare-const tptp.member_val (-> tptp.val tptp.set_val Bool)) % 0.48/0.93 (declare-const tptp.append_list_node (-> tptp.list_list_node tptp.list_list_node tptp.list_list_node)) % 0.48/0.93 (define tptp.suffix_node () (let ((_let_1 (@var "Xs3" tptp.list_node))) (let ((_let_2 (@var "Zs3" tptp.list_node))) (let ((_let_3 (@var "Ys3" tptp.list_node))) (lambda (@list _let_1 _let_3) (exists (@list _let_2) (= _let_3 (_ (_ tptp.append_node _let_2) _let_1)))))))) % 0.48/0.93 (define @t1 () (_ (_ (_ (_ tptp.sSA_CF551432799de_val tptp.alpha_n) tptp.defs) tptp.phis) tptp.g2)) % 0.48/0.93 (define @t2 () (_ @t1 tptp.phi_r)) % 0.48/0.93 (define @t3 () (= tptp.i @t2)) % 0.48/0.93 (define @t4 () (@var "G" tptp.g)) % 0.48/0.93 (define @t5 () (_ tptp.invar @t4)) % 0.48/0.93 (define @t6 () (_ @t1 tptp.r)) % 0.48/0.93 (define @t7 () (_ (_ (_ tptp.graph_1012773594_edgeD tptp.alpha_n) tptp.invar) tptp.inEdges)) % 0.48/0.93 (define @t8 () (_ @t7 tptp.g2)) % 0.48/0.93 (define @t9 () (_ @t8 tptp.n)) % 0.48/0.93 (define @t10 () (_ @t9 tptp.ns)) % 0.48/0.93 (define @t11 () (_ @t10 @t6)) % 0.48/0.93 (define @t12 () (_ @t8 @t6)) % 0.48/0.93 (define @t13 () (_ @t12 tptp.ri)) % 0.48/0.93 (define @t14 () (@var "L" tptp.node)) % 0.48/0.93 (define @t15 () (@var "Ms" tptp.list_node)) % 0.48/0.93 (define @t16 () (_ tptp.tl_node @t15)) % 0.48/0.93 (define @t17 () (@var "Ns" tptp.list_node)) % 0.48/0.93 (define @t18 () (_ tptp.append_node @t17)) % 0.48/0.93 (define @t19 () (_ @t18 @t16)) % 0.48/0.93 (define @t20 () (@var "N" tptp.node)) % 0.48/0.93 (define @t21 () (_ @t7 @t4)) % 0.48/0.93 (define @t22 () (_ @t21 @t20)) % 0.48/0.93 (define @t23 () (_ (_ @t22 @t19) @t14)) % 0.48/0.93 (define @t24 () (@var "M" tptp.node)) % 0.48/0.93 (define @t25 () (_ (_ (_ @t21 @t24) @t15) @t14)) % 0.48/0.93 (define @t26 () (=> @t25 @t23)) % 0.48/0.93 (define @t27 () (_ @t22 @t17)) % 0.48/0.93 (define @t28 () (_ @t27 @t24)) % 0.48/0.93 (define @t29 () (@list @t4 @t20 @t17 @t24 @t15 @t14)) % 0.48/0.93 (define @t30 () (forall @t29 (=> @t28 @t26))) % 0.48/0.93 (define @t31 () (_ @t8 tptp.m)) % 0.48/0.93 (define @t32 () (= tptp.m tptp.i)) % 0.48/0.93 (define @t33 () (not @t3)) % 0.48/0.93 (define @t34 () (@var "Ns2" tptp.list_node)) % 0.48/0.93 (define @t35 () (@var "N2" tptp.node)) % 0.48/0.93 (define @t36 () (_ tptp.cons_node @t35)) % 0.48/0.93 (define @t37 () (_ @t36 @t34)) % 0.48/0.93 (define @t38 () (_ @t21 @t35)) % 0.48/0.93 (define @t39 () (_ (_ @t22 (_ @t18 @t37)) @t24)) % 0.48/0.93 (define @t40 () (@list @t4 @t20 @t17 @t35 @t34 @t24)) % 0.48/0.93 (define @t41 () (not (= @t17 tptp.nil_node))) % 0.48/0.93 (define @t42 () (@list @t4 @t20 @t17 @t24)) % 0.48/0.93 (define @t43 () (_ (_ (_ tptp.sSA_CF848637139eD_val tptp.alpha_n) tptp.inEdges) tptp.phis)) % 0.48/0.93 (define @t44 () (_ tptp.set_node2 (_ tptp.alpha_n @t4))) % 0.48/0.93 (define @t45 () (_ tptp.member_node @t20)) % 0.48/0.93 (define @t46 () (_ @t45 @t44)) % 0.48/0.93 (define @t47 () (_ tptp.set_node2 @t17)) % 0.48/0.93 (define @t48 () (_ @t45 @t47)) % 0.48/0.93 (define @t49 () (_ tptp.member_node @t14)) % 0.48/0.93 (define @t50 () (@var "Xs" tptp.list_list_node)) % 0.48/0.93 (define @t51 () (@var "Y" tptp.list_node)) % 0.48/0.93 (define @t52 () (_ tptp.cons_list_node @t51)) % 0.48/0.93 (define @t53 () (@var "Ys" tptp.list_list_node)) % 0.48/0.93 (define @t54 () (_ tptp.append_list_node @t53)) % 0.48/0.93 (define @t55 () (@var "X" tptp.list_node)) % 0.48/0.93 (define @t56 () (_ tptp.member_list_node @t55)) % 0.48/0.93 (define @t57 () (@var "Xs" tptp.list_val)) % 0.48/0.93 (define @t58 () (@var "Y" tptp.val)) % 0.48/0.93 (define @t59 () (_ tptp.cons_val @t58)) % 0.48/0.93 (define @t60 () (@var "Ys" tptp.list_val)) % 0.48/0.93 (define @t61 () (_ tptp.append_val @t60)) % 0.48/0.93 (define @t62 () (@var "X" tptp.val)) % 0.48/0.93 (define @t63 () (_ tptp.member_val @t62)) % 0.48/0.93 (define @t64 () (_ tptp.set_val2 @t57)) % 0.48/0.93 (define @t65 () (_ @t63 @t64)) % 0.48/0.93 (define @t66 () (@var "Xs" tptp.list_node)) % 0.48/0.93 (define @t67 () (@var "Y" tptp.node)) % 0.48/0.93 (define @t68 () (_ tptp.cons_node @t67)) % 0.48/0.93 (define @t69 () (@var "Ys" tptp.list_node)) % 0.48/0.93 (define @t70 () (_ tptp.append_node @t69)) % 0.48/0.93 (define @t71 () (@var "X" tptp.node)) % 0.48/0.93 (define @t72 () (_ tptp.member_node @t71)) % 0.48/0.93 (define @t73 () (_ tptp.set_node2 @t66)) % 0.48/0.93 (define @t74 () (_ @t72 @t73)) % 0.48/0.93 (define @t75 () (_ tptp.set_node2 tptp.ms)) % 0.48/0.93 (define @t76 () (_ tptp.member_node tptp.i)) % 0.48/0.93 (define @t77 () (_ tptp.member_node @t24)) % 0.48/0.93 (define @t78 () (_ tptp.member_node @t6)) % 0.48/0.93 (define @t79 () (_ tptp.cons_node @t20)) % 0.48/0.93 (define @t80 () (_ @t79 tptp.nil_node)) % 0.48/0.93 (define @t81 () (@list @t20 @t4)) % 0.48/0.93 (define @t82 () (_ tptp.graph_272749361_edgeD tptp.inEdges)) % 0.48/0.93 (define @t83 () (_ tptp.append_list_node @t50)) % 0.48/0.93 (define @t84 () (_ @t83 @t53)) % 0.48/0.93 (define @t85 () (= @t50 tptp.nil_list_node)) % 0.48/0.93 (define @t86 () (not @t85)) % 0.48/0.93 (define @t87 () (@list @t50 @t53)) % 0.48/0.93 (define @t88 () (_ tptp.tl_val @t57)) % 0.48/0.93 (define @t89 () (_ tptp.append_val @t57)) % 0.48/0.93 (define @t90 () (_ @t89 @t60)) % 0.48/0.93 (define @t91 () (= @t57 tptp.nil_val)) % 0.48/0.93 (define @t92 () (not @t91)) % 0.48/0.93 (define @t93 () (@list @t57 @t60)) % 0.48/0.93 (define @t94 () (_ tptp.tl_node @t66)) % 0.48/0.93 (define @t95 () (_ tptp.append_node @t66)) % 0.48/0.93 (define @t96 () (_ @t95 @t69)) % 0.48/0.93 (define @t97 () (= @t66 tptp.nil_node)) % 0.48/0.93 (define @t98 () (not @t97)) % 0.48/0.93 (define @t99 () (@list @t66 @t69)) % 0.48/0.93 (define @t100 () (@var "L2" tptp.list_val)) % 0.48/0.93 (define @t101 () (= @t100 tptp.nil_val)) % 0.48/0.93 (define @t102 () (@var "E2" tptp.val)) % 0.48/0.93 (define @t103 () (@var "E" tptp.val)) % 0.48/0.93 (define @t104 () (@var "L1" tptp.list_val)) % 0.48/0.93 (define @t105 () (= @t104 tptp.nil_val)) % 0.48/0.93 (define @t106 () (and @t105 (= @t103 @t102) @t101)) % 0.48/0.93 (define @t107 () (_ tptp.cons_val @t102)) % 0.48/0.93 (define @t108 () (_ @t107 tptp.nil_val)) % 0.48/0.93 (define @t109 () (_ tptp.append_val @t104)) % 0.48/0.93 (define @t110 () (_ @t109 (_ (_ tptp.cons_val @t103) @t100))) % 0.48/0.93 (define @t111 () (@var "L2" tptp.list_list_node)) % 0.48/0.93 (define @t112 () (= @t111 tptp.nil_list_node)) % 0.48/0.93 (define @t113 () (@var "E2" tptp.list_node)) % 0.48/0.93 (define @t114 () (@var "E" tptp.list_node)) % 0.48/0.93 (define @t115 () (@var "L1" tptp.list_list_node)) % 0.48/0.93 (define @t116 () (= @t115 tptp.nil_list_node)) % 0.48/0.93 (define @t117 () (and @t116 (= @t114 @t113) @t112)) % 0.48/0.93 (define @t118 () (_ (_ tptp.cons_list_node @t113) tptp.nil_list_node)) % 0.48/0.93 (define @t119 () (_ tptp.append_list_node @t115)) % 0.48/0.93 (define @t120 () (_ @t119 (_ (_ tptp.cons_list_node @t114) @t111))) % 0.48/0.93 (define @t121 () (@var "L2" tptp.list_node)) % 0.48/0.93 (define @t122 () (= @t121 tptp.nil_node)) % 0.48/0.93 (define @t123 () (@var "E2" tptp.node)) % 0.48/0.93 (define @t124 () (@var "E" tptp.node)) % 0.48/0.93 (define @t125 () (@var "L1" tptp.list_node)) % 0.48/0.93 (define @t126 () (= @t125 tptp.nil_node)) % 0.48/0.93 (define @t127 () (and @t126 (= @t124 @t123) @t122)) % 0.48/0.93 (define @t128 () (_ tptp.cons_node @t123)) % 0.48/0.93 (define @t129 () (_ @t128 tptp.nil_node)) % 0.48/0.93 (define @t130 () (_ tptp.append_node @t125)) % 0.48/0.93 (define @t131 () (_ @t130 (_ (_ tptp.cons_node @t124) @t121))) % 0.48/0.93 (define @t132 () (@var "A" tptp.val)) % 0.48/0.93 (define @t133 () (_ (_ tptp.cons_val @t132) tptp.nil_val)) % 0.48/0.93 (define @t134 () (and @t105 (= @t100 @t133))) % 0.48/0.93 (define @t135 () (_ @t109 @t100)) % 0.48/0.93 (define @t136 () (= @t133 @t135)) % 0.48/0.93 (define @t137 () (not @t101)) % 0.48/0.93 (define @t138 () (@var "A" tptp.list_node)) % 0.48/0.93 (define @t139 () (_ (_ tptp.cons_list_node @t138) tptp.nil_list_node)) % 0.48/0.93 (define @t140 () (and @t116 (= @t111 @t139))) % 0.48/0.93 (define @t141 () (_ @t119 @t111)) % 0.48/0.93 (define @t142 () (= @t139 @t141)) % 0.48/0.93 (define @t143 () (not @t112)) % 0.48/0.93 (define @t144 () (@var "A" tptp.node)) % 0.48/0.93 (define @t145 () (_ (_ tptp.cons_node @t144) tptp.nil_node)) % 0.48/0.93 (define @t146 () (and @t126 (= @t121 @t145))) % 0.48/0.93 (define @t147 () (_ @t130 @t121)) % 0.48/0.93 (define @t148 () (= @t145 @t147)) % 0.48/0.93 (define @t149 () (not @t122)) % 0.48/0.93 (define @t150 () (and (= @t104 @t133) @t101)) % 0.48/0.93 (define @t151 () (not @t105)) % 0.48/0.93 (define @t152 () (and (= @t115 @t139) @t112)) % 0.48/0.93 (define @t153 () (not @t116)) % 0.48/0.93 (define @t154 () (and (= @t125 @t145) @t122)) % 0.48/0.93 (define @t155 () (not @t126)) % 0.48/0.93 (define @t156 () (= @t135 @t133)) % 0.48/0.93 (define @t157 () (= @t141 @t139)) % 0.48/0.93 (define @t158 () (= @t147 @t145)) % 0.48/0.93 (define @t159 () (@var "E22" tptp.val)) % 0.48/0.93 (define @t160 () (@var "E23" tptp.val)) % 0.48/0.93 (define @t161 () (@var "E1" tptp.val)) % 0.48/0.93 (define @t162 () (@var "E12" tptp.val)) % 0.48/0.93 (define @t163 () (and @t105 (= @t162 @t161) (= @t160 @t159) @t101)) % 0.48/0.93 (define @t164 () (_ (_ tptp.cons_val @t162) (_ (_ tptp.cons_val @t160) tptp.nil_val))) % 0.48/0.93 (define @t165 () (_ @t109 (_ (_ tptp.cons_val @t161) (_ (_ tptp.cons_val @t159) @t100)))) % 0.48/0.93 (define @t166 () (@var "E22" tptp.list_node)) % 0.48/0.93 (define @t167 () (@var "E23" tptp.list_node)) % 0.48/0.93 (define @t168 () (@var "E1" tptp.list_node)) % 0.48/0.93 (define @t169 () (@var "E12" tptp.list_node)) % 0.48/0.93 (define @t170 () (and @t116 (= @t169 @t168) (= @t167 @t166) @t112)) % 0.48/0.93 (define @t171 () (_ (_ tptp.cons_list_node @t169) (_ (_ tptp.cons_list_node @t167) tptp.nil_list_node))) % 0.48/0.93 (define @t172 () (_ @t119 (_ (_ tptp.cons_list_node @t168) (_ (_ tptp.cons_list_node @t166) @t111)))) % 0.48/0.93 (define @t173 () (@var "E22" tptp.node)) % 0.48/0.93 (define @t174 () (@var "E23" tptp.node)) % 0.48/0.93 (define @t175 () (@var "E1" tptp.node)) % 0.48/0.93 (define @t176 () (@var "E12" tptp.node)) % 0.48/0.93 (define @t177 () (and @t126 (= @t176 @t175) (= @t174 @t173) @t122)) % 0.48/0.93 (define @t178 () (_ (_ tptp.cons_node @t176) (_ (_ tptp.cons_node @t174) tptp.nil_node))) % 0.48/0.93 (define @t179 () (_ @t130 (_ (_ tptp.cons_node @t175) (_ (_ tptp.cons_node @t173) @t121)))) % 0.48/0.93 (define @t180 () (@var "X2" tptp.node)) % 0.48/0.93 (define @t181 () (_ tptp.member_node @t180)) % 0.48/0.93 (define @t182 () (not (_ @t181 @t75))) % 0.48/0.93 (define @t183 () (@list @t180)) % 0.48/0.93 (define @t184 () (@var "Y22" tptp.list_val)) % 0.48/0.93 (define @t185 () (@var "X22" tptp.list_val)) % 0.48/0.93 (define @t186 () (@var "Y21" tptp.val)) % 0.48/0.93 (define @t187 () (@var "X21" tptp.val)) % 0.48/0.93 (define @t188 () (_ (_ tptp.cons_val @t187) @t185)) % 0.48/0.93 (define @t189 () (@var "Y22" tptp.list_list_node)) % 0.48/0.93 (define @t190 () (@var "X22" tptp.list_list_node)) % 0.48/0.93 (define @t191 () (@var "Y21" tptp.list_node)) % 0.48/0.93 (define @t192 () (@var "X21" tptp.list_node)) % 0.48/0.93 (define @t193 () (@var "Y22" tptp.list_node)) % 0.48/0.93 (define @t194 () (@var "X22" tptp.list_node)) % 0.48/0.93 (define @t195 () (@var "Y21" tptp.node)) % 0.48/0.93 (define @t196 () (@var "X21" tptp.node)) % 0.48/0.93 (define @t197 () (_ (_ tptp.cons_node @t196) @t194)) % 0.48/0.93 (define @t198 () (@var "C" tptp.list_val)) % 0.48/0.93 (define @t199 () (@var "B" tptp.list_val)) % 0.48/0.93 (define @t200 () (@var "A" tptp.list_val)) % 0.48/0.93 (define @t201 () (_ tptp.append_val @t200)) % 0.48/0.93 (define @t202 () (@var "C" tptp.list_node)) % 0.48/0.93 (define @t203 () (@var "B" tptp.list_node)) % 0.48/0.93 (define @t204 () (_ tptp.append_node @t138)) % 0.48/0.93 (define @t205 () (@list @t138 @t203 @t202)) % 0.48/0.93 (define @t206 () (@var "P" (-> tptp.val Bool))) % 0.48/0.93 (define @t207 () (_ tptp.collect_val @t206)) % 0.48/0.93 (define @t208 () (@var "P" (-> tptp.node Bool))) % 0.48/0.93 (define @t209 () (_ tptp.collect_node @t208)) % 0.48/0.93 (define @t210 () (@var "A2" tptp.set_val)) % 0.48/0.93 (define @t211 () (@var "X3" tptp.val)) % 0.48/0.93 (define @t212 () (_ tptp.member_val @t211)) % 0.48/0.93 (define @t213 () (@list @t211)) % 0.48/0.93 (define @t214 () (@list @t210)) % 0.48/0.93 (define @t215 () (@var "A2" tptp.set_node)) % 0.48/0.93 (define @t216 () (@var "X3" tptp.node)) % 0.48/0.93 (define @t217 () (_ tptp.member_node @t216)) % 0.48/0.93 (define @t218 () (@list @t216)) % 0.48/0.93 (define @t219 () (@list @t215)) % 0.48/0.93 (define @t220 () (@var "Q" (-> tptp.node Bool))) % 0.48/0.93 (define @t221 () (@var "X4" tptp.node)) % 0.48/0.93 (define @t222 () (_ @t208 @t221)) % 0.48/0.93 (define @t223 () (@list @t221)) % 0.48/0.93 (define @t224 () (@var "Q" (-> tptp.val Bool))) % 0.48/0.93 (define @t225 () (@var "X4" tptp.val)) % 0.48/0.93 (define @t226 () (@var "Zs" tptp.list_val)) % 0.48/0.93 (define @t227 () (@list @t57 @t60 @t226)) % 0.48/0.93 (define @t228 () (@var "Zs" tptp.list_node)) % 0.48/0.93 (define @t229 () (_ @t70 @t228)) % 0.48/0.93 (define @t230 () (@list @t66 @t69 @t228)) % 0.48/0.93 (define @t231 () (= @t60 @t226)) % 0.48/0.93 (define @t232 () (_ tptp.append_val @t226)) % 0.48/0.93 (define @t233 () (= @t69 @t228)) % 0.48/0.93 (define @t234 () (_ tptp.append_node @t228)) % 0.48/0.93 (define @t235 () (_ @t234 @t66)) % 0.48/0.93 (define @t236 () (_ @t70 @t66)) % 0.48/0.93 (define @t237 () (@list @t69 @t66 @t228)) % 0.48/0.93 (define @t238 () (_ @t95 @t228)) % 0.48/0.93 (define @t239 () (=> @t5 @t46)) % 0.48/0.93 (define @t240 () (_ @t82 @t4)) % 0.48/0.93 (define @t241 () (_ @t45 (_ tptp.set_node2 (_ @t240 @t35)))) % 0.48/0.93 (define @t242 () (@list @t20 @t4 @t35)) % 0.48/0.93 (define @t243 () (_ tptp.member_node @t35)) % 0.48/0.93 (define @t244 () (_ @t240 @t20)) % 0.48/0.93 (define @t245 () (@list @t4 @t20)) % 0.48/0.93 (define @t246 () (@list @t57)) % 0.48/0.93 (define @t247 () (@list @t66)) % 0.48/0.93 (define @t248 () (= @t53 tptp.nil_list_node)) % 0.48/0.93 (define @t249 () (= @t60 tptp.nil_val)) % 0.48/0.93 (define @t250 () (= @t69 tptp.nil_node)) % 0.48/0.93 (define @t251 () (@list @t53 @t50)) % 0.48/0.93 (define @t252 () (@list @t60 @t57)) % 0.48/0.93 (define @t253 () (@list @t69 @t66)) % 0.48/0.93 (define @t254 () (and @t85 @t248)) % 0.48/0.93 (define @t255 () (and @t91 @t249)) % 0.48/0.93 (define @t256 () (and @t97 @t250)) % 0.48/0.93 (define @t257 () (@var "X3" tptp.list_list_node)) % 0.48/0.93 (define @t258 () (@var "X3" tptp.list_val)) % 0.48/0.93 (define @t259 () (@var "X3" tptp.list_node)) % 0.48/0.93 (define @t260 () (_ tptp.append_node tptp.nil_node)) % 0.48/0.93 (define @t261 () (@var "A" tptp.list_list_node)) % 0.48/0.93 (define @t262 () (@list @t200)) % 0.48/0.93 (define @t263 () (@list @t138)) % 0.48/0.93 (define @t264 () (@var "Ns_2" tptp.list_node)) % 0.48/0.93 (define @t265 () (@var "Ns_1" tptp.list_node)) % 0.48/0.93 (define @t266 () (not (= @t17 (_ (_ tptp.append_node (_ tptp.butlast_node @t265)) @t264)))) % 0.48/0.93 (define @t267 () (_ @t21 @t71)) % 0.48/0.93 (define @t268 () (_ (_ @t267 @t264) @t24)) % 0.48/0.93 (define @t269 () (@list @t264)) % 0.48/0.93 (define @t270 () (_ (_ @t22 @t265) @t71)) % 0.48/0.93 (define @t271 () (@list @t265)) % 0.48/0.93 (define @t272 () (_ @t72 @t47)) % 0.48/0.93 (define @t273 () (@list @t4 @t20 @t17 @t24 @t71)) % 0.48/0.93 (define @t274 () (@var "Ns3" tptp.list_node)) % 0.48/0.93 (define @t275 () (_ tptp.butlast_node @t274)) % 0.48/0.93 (define @t276 () (_ tptp.set_node2 @t275)) % 0.48/0.93 (define @t277 () (@var "M2" tptp.node)) % 0.48/0.93 (define @t278 () (_ tptp.member_node @t277)) % 0.48/0.93 (define @t279 () (_ (_ tptp.prefix_node @t274) @t17)) % 0.48/0.93 (define @t280 () (_ @t22 @t274)) % 0.48/0.93 (define @t281 () (@list @t274)) % 0.48/0.93 (define @t282 () (@list @t4 @t20 @t17 @t24 @t277)) % 0.48/0.93 (define @t283 () (_ @t208 @t180)) % 0.48/0.93 (define @t284 () (not @t283)) % 0.48/0.93 (define @t285 () (@var "M3" tptp.node)) % 0.48/0.93 (define @t286 () (exists @t183 (and (_ @t181 @t47) @t283))) % 0.48/0.93 (define @t287 () (@list @t4 @t20 @t17 @t24 @t208)) % 0.48/0.93 (define @t288 () (@var "P" (-> tptp.node tptp.list_node tptp.node Bool))) % 0.48/0.93 (define @t289 () (_ @t288 @t20)) % 0.48/0.93 (define @t290 () (_ (_ @t289 @t17) @t24)) % 0.48/0.93 (define @t291 () (@var "Ns4" tptp.list_node)) % 0.48/0.93 (define @t292 () (@var "N3" tptp.node)) % 0.48/0.93 (define @t293 () (_ (_ tptp.cons_node @t292) @t291)) % 0.48/0.93 (define @t294 () (@var "N4" tptp.node)) % 0.48/0.93 (define @t295 () (_ tptp.member_node @t292)) % 0.48/0.93 (define @t296 () (_ tptp.cons_node @t24)) % 0.48/0.93 (define @t297 () (_ @t296 tptp.nil_node)) % 0.48/0.93 (define @t298 () (@list @t4 @t20 @t17 @t24 @t288)) % 0.48/0.93 (define @t299 () (_ tptp.append_node @t265)) % 0.48/0.93 (define @t300 () (_ (_ tptp.cons_node @t277) tptp.nil_node)) % 0.48/0.93 (define @t301 () (_ (_ tptp.append_node @t34) @t300)) % 0.48/0.93 (define @t302 () (@var "M4" tptp.node)) % 0.48/0.93 (define @t303 () (= @t62 @t58)) % 0.48/0.93 (define @t304 () (_ tptp.cons_val @t62)) % 0.48/0.93 (define @t305 () (_ @t89 (_ @t304 tptp.nil_val))) % 0.48/0.93 (define @t306 () (= @t55 @t51)) % 0.48/0.93 (define @t307 () (_ tptp.cons_list_node @t55)) % 0.48/0.93 (define @t308 () (_ @t83 (_ @t307 tptp.nil_list_node))) % 0.48/0.93 (define @t309 () (= @t71 @t67)) % 0.48/0.93 (define @t310 () (= @t66 @t69)) % 0.48/0.93 (define @t311 () (_ @t68 tptp.nil_node)) % 0.48/0.93 (define @t312 () (_ @t70 @t311)) % 0.48/0.93 (define @t313 () (_ tptp.cons_node @t71)) % 0.48/0.93 (define @t314 () (_ @t313 tptp.nil_node)) % 0.48/0.93 (define @t315 () (_ @t95 @t314)) % 0.48/0.93 (define @t316 () (@list @t66 @t71 @t69 @t67)) % 0.48/0.93 (define @t317 () (@list @t57 @t62)) % 0.48/0.93 (define @t318 () (@list @t50 @t55)) % 0.48/0.93 (define @t319 () (@list @t66 @t71)) % 0.48/0.93 (define @t320 () (@var "Ms2" tptp.list_node)) % 0.48/0.93 (define @t321 () (@var "Ri" tptp.list_node)) % 0.48/0.93 (define @t322 () (@var "I" tptp.node)) % 0.48/0.93 (define @t323 () (_ @t36 @t17)) % 0.48/0.93 (define @t324 () (_ tptp.butlast_val @t57)) % 0.48/0.93 (define @t325 () (_ @t63 (_ tptp.set_val2 @t324))) % 0.48/0.93 (define @t326 () (@list @t62 @t57)) % 0.48/0.93 (define @t327 () (_ tptp.butlast_node @t66)) % 0.48/0.93 (define @t328 () (_ tptp.set_node2 @t327)) % 0.48/0.93 (define @t329 () (_ @t72 @t328)) % 0.48/0.93 (define @t330 () (@list @t71 @t66)) % 0.48/0.93 (define @t331 () (_ @t304 @t57)) % 0.48/0.93 (define @t332 () (_ tptp.butlast_val @t331)) % 0.48/0.93 (define @t333 () (_ tptp.butlast_list_node @t50)) % 0.48/0.93 (define @t334 () (_ @t307 @t50)) % 0.48/0.93 (define @t335 () (_ tptp.butlast_list_node @t334)) % 0.48/0.93 (define @t336 () (_ @t313 @t66)) % 0.48/0.93 (define @t337 () (_ tptp.butlast_node @t336)) % 0.48/0.93 (define @t338 () (_ tptp.butlast_list_node @t84)) % 0.48/0.93 (define @t339 () (_ tptp.butlast_val @t60)) % 0.48/0.93 (define @t340 () (_ tptp.butlast_val @t90)) % 0.48/0.93 (define @t341 () (_ tptp.butlast_node @t69)) % 0.48/0.93 (define @t342 () (_ tptp.butlast_node @t96)) % 0.48/0.93 (define @t343 () (not @t250)) % 0.48/0.93 (define @t344 () (@list @t71 @t66 @t69)) % 0.48/0.93 (define @t345 () (@var "Xl" tptp.val)) % 0.48/0.93 (define @t346 () (@var "L" tptp.list_val)) % 0.48/0.93 (define @t347 () (= (_ tptp.butlast_val @t346) @t331)) % 0.48/0.93 (define @t348 () (@list @t346 @t62 @t57)) % 0.48/0.93 (define @t349 () (@var "Xl" tptp.list_node)) % 0.48/0.93 (define @t350 () (@var "L" tptp.list_list_node)) % 0.48/0.93 (define @t351 () (= (_ tptp.butlast_list_node @t350) @t334)) % 0.48/0.93 (define @t352 () (@list @t350 @t55 @t50)) % 0.48/0.93 (define @t353 () (@var "Xl" tptp.node)) % 0.48/0.93 (define @t354 () (@var "L" tptp.list_node)) % 0.48/0.93 (define @t355 () (= (_ tptp.butlast_node @t354) @t336)) % 0.48/0.93 (define @t356 () (@list @t354 @t71 @t66)) % 0.48/0.93 (define @t357 () (@var "Xl2" tptp.val)) % 0.48/0.93 (define @t358 () (@var "Xl2" tptp.list_node)) % 0.48/0.93 (define @t359 () (@var "Xl2" tptp.node)) % 0.48/0.93 (define @t360 () (@var "R2" tptp.list_val)) % 0.48/0.93 (define @t361 () (@var "R1" tptp.list_val)) % 0.48/0.93 (define @t362 () (@var "N22" tptp.val)) % 0.48/0.93 (define @t363 () (@var "N1" tptp.val)) % 0.48/0.93 (define @t364 () (@var "R2" tptp.list_list_node)) % 0.48/0.93 (define @t365 () (@var "R1" tptp.list_list_node)) % 0.48/0.93 (define @t366 () (@var "N22" tptp.list_node)) % 0.48/0.93 (define @t367 () (@var "N1" tptp.list_node)) % 0.48/0.93 (define @t368 () (@var "R2" tptp.list_node)) % 0.48/0.93 (define @t369 () (@var "R1" tptp.list_node)) % 0.48/0.93 (define @t370 () (@var "N22" tptp.node)) % 0.48/0.93 (define @t371 () (@var "N1" tptp.node)) % 0.48/0.93 (define @t372 () (@var "Us" tptp.list_val)) % 0.48/0.93 (define @t373 () (@var "Xs1" tptp.list_val)) % 0.48/0.93 (define @t374 () (@var "Us" tptp.list_node)) % 0.48/0.93 (define @t375 () (@var "Xs1" tptp.list_node)) % 0.48/0.93 (define @t376 () (_ tptp.append_node @t375)) % 0.48/0.93 (define @t377 () (@var "Ts" tptp.list_val)) % 0.48/0.93 (define @t378 () (@var "Us2" tptp.list_val)) % 0.48/0.93 (define @t379 () (_ tptp.append_val @t378)) % 0.48/0.93 (define @t380 () (@var "Ts" tptp.list_node)) % 0.48/0.93 (define @t381 () (@var "Us2" tptp.list_node)) % 0.48/0.93 (define @t382 () (_ tptp.append_node @t381)) % 0.48/0.93 (define @t383 () (@var "A0" tptp.list_val)) % 0.48/0.93 (define @t384 () (@var "P" (-> tptp.list_val Bool))) % 0.48/0.93 (define @t385 () (@var "Ys2" tptp.list_val)) % 0.48/0.93 (define @t386 () (_ tptp.cons_val @t225)) % 0.48/0.93 (define @t387 () (@var "A0" tptp.list_node)) % 0.48/0.93 (define @t388 () (@var "P" (-> tptp.list_node Bool))) % 0.48/0.93 (define @t389 () (_ @t388 @t387)) % 0.48/0.93 (define @t390 () (@var "Ys2" tptp.list_node)) % 0.48/0.93 (define @t391 () (_ tptp.cons_node @t221)) % 0.48/0.93 (define @t392 () (_ @t391 @t390)) % 0.48/0.93 (define @t393 () (_ @t388 tptp.nil_node)) % 0.48/0.93 (define @t394 () (@list @t388 @t387)) % 0.48/0.93 (define @t395 () (@var "P" (-> tptp.list_node tptp.list_val Bool))) % 0.48/0.93 (define @t396 () (@var "Y2" tptp.val)) % 0.48/0.93 (define @t397 () (_ (_ tptp.cons_val @t396) @t385)) % 0.48/0.93 (define @t398 () (@var "Xs2" tptp.list_node)) % 0.48/0.93 (define @t399 () (_ @t391 @t398)) % 0.48/0.93 (define @t400 () (_ @t395 @t399)) % 0.48/0.93 (define @t401 () (_ @t400 @t397)) % 0.48/0.93 (define @t402 () (@var "R" (-> tptp.node tptp.val Bool))) % 0.48/0.93 (define @t403 () (_ (_ @t402 @t221) @t396)) % 0.48/0.93 (define @t404 () (@list @t221 @t398 @t396 @t385)) % 0.48/0.93 (define @t405 () (_ @t395 @t398)) % 0.48/0.93 (define @t406 () (@var "X_1" tptp.list_val)) % 0.48/0.93 (define @t407 () (@list @t406)) % 0.48/0.93 (define @t408 () (@list @t398)) % 0.48/0.93 (define @t409 () (@var "P" (-> tptp.list_val tptp.list_val Bool))) % 0.48/0.93 (define @t410 () (@var "Xs2" tptp.list_val)) % 0.48/0.93 (define @t411 () (_ @t386 @t410)) % 0.48/0.93 (define @t412 () (_ @t409 @t411)) % 0.48/0.93 (define @t413 () (_ @t412 @t397)) % 0.48/0.93 (define @t414 () (@var "R" (-> tptp.val tptp.val Bool))) % 0.48/0.93 (define @t415 () (_ (_ @t414 @t225) @t396)) % 0.48/0.93 (define @t416 () (@list @t225 @t410 @t396 @t385)) % 0.48/0.93 (define @t417 () (_ @t409 @t410)) % 0.48/0.93 (define @t418 () (@list @t410)) % 0.48/0.93 (define @t419 () (@var "P" (-> tptp.list_list_node tptp.list_val Bool))) % 0.48/0.93 (define @t420 () (@var "Xs2" tptp.list_list_node)) % 0.48/0.93 (define @t421 () (@var "X4" tptp.list_node)) % 0.48/0.93 (define @t422 () (_ (_ tptp.cons_list_node @t421) @t420)) % 0.48/0.93 (define @t423 () (_ @t419 @t422)) % 0.48/0.93 (define @t424 () (_ @t423 @t397)) % 0.48/0.93 (define @t425 () (@var "R" (-> tptp.list_node tptp.val Bool))) % 0.48/0.93 (define @t426 () (_ (_ @t425 @t421) @t396)) % 0.48/0.93 (define @t427 () (@list @t421 @t420 @t396 @t385)) % 0.48/0.93 (define @t428 () (_ @t419 @t420)) % 0.48/0.93 (define @t429 () (@list @t420)) % 0.48/0.93 (define @t430 () (@var "P" (-> tptp.list_node tptp.list_list_node Bool))) % 0.48/0.93 (define @t431 () (@var "Ys2" tptp.list_list_node)) % 0.48/0.93 (define @t432 () (@var "Y2" tptp.list_node)) % 0.48/0.93 (define @t433 () (_ (_ tptp.cons_list_node @t432) @t431)) % 0.48/0.93 (define @t434 () (_ @t430 @t399)) % 0.48/0.93 (define @t435 () (_ @t434 @t433)) % 0.48/0.93 (define @t436 () (@var "R" (-> tptp.node tptp.list_node Bool))) % 0.48/0.93 (define @t437 () (_ (_ @t436 @t221) @t432)) % 0.48/0.93 (define @t438 () (@list @t221 @t398 @t432 @t431)) % 0.48/0.93 (define @t439 () (_ @t430 @t398)) % 0.48/0.93 (define @t440 () (@var "X_1" tptp.list_list_node)) % 0.48/0.93 (define @t441 () (@list @t440)) % 0.48/0.93 (define @t442 () (@var "P" (-> tptp.list_val tptp.list_list_node Bool))) % 0.48/0.93 (define @t443 () (_ @t442 @t411)) % 0.48/0.93 (define @t444 () (_ @t443 @t433)) % 0.48/0.93 (define @t445 () (@var "R" (-> tptp.val tptp.list_node Bool))) % 0.48/0.93 (define @t446 () (_ (_ @t445 @t225) @t432)) % 0.48/0.93 (define @t447 () (@list @t225 @t410 @t432 @t431)) % 0.48/0.93 (define @t448 () (_ @t442 @t410)) % 0.48/0.93 (define @t449 () (@var "P" (-> tptp.list_list_node tptp.list_list_node Bool))) % 0.48/0.93 (define @t450 () (_ @t449 @t422)) % 0.48/0.93 (define @t451 () (_ @t450 @t433)) % 0.48/0.93 (define @t452 () (@var "R" (-> tptp.list_node tptp.list_node Bool))) % 0.48/0.93 (define @t453 () (_ (_ @t452 @t421) @t432)) % 0.48/0.93 (define @t454 () (@list @t421 @t420 @t432 @t431)) % 0.48/0.93 (define @t455 () (_ @t449 @t420)) % 0.48/0.93 (define @t456 () (@var "P" (-> tptp.list_node tptp.list_node Bool))) % 0.48/0.93 (define @t457 () (_ (_ @t456 @t66) @t69)) % 0.48/0.93 (define @t458 () (@var "Y2" tptp.node)) % 0.48/0.93 (define @t459 () (_ tptp.cons_node @t458)) % 0.48/0.93 (define @t460 () (_ @t459 @t390)) % 0.48/0.93 (define @t461 () (_ @t456 @t399)) % 0.48/0.93 (define @t462 () (_ @t461 @t460)) % 0.48/0.93 (define @t463 () (_ @t461 @t390)) % 0.48/0.93 (define @t464 () (=> @t463 @t462)) % 0.48/0.93 (define @t465 () (@var "R" (-> tptp.node tptp.node Bool))) % 0.48/0.93 (define @t466 () (_ (_ @t465 @t221) @t458)) % 0.48/0.93 (define @t467 () (@list @t221 @t398 @t458 @t390)) % 0.48/0.93 (define @t468 () (_ @t456 @t398)) % 0.48/0.93 (define @t469 () (_ @t468 @t460)) % 0.48/0.93 (define @t470 () (@var "X_1" tptp.list_node)) % 0.48/0.93 (define @t471 () (_ @t456 tptp.nil_node)) % 0.48/0.93 (define @t472 () (forall (@list @t470) (_ @t471 @t470))) % 0.48/0.93 (define @t473 () (forall @t408 (_ @t468 tptp.nil_node))) % 0.48/0.93 (define @t474 () (@var "A22" tptp.list_node)) % 0.48/0.93 (define @t475 () (@var "A1" tptp.list_node)) % 0.48/0.93 (define @t476 () (@var "A0" (-> tptp.node tptp.node Bool))) % 0.48/0.93 (define @t477 () (@var "P" (-> (-> tptp.node tptp.node Bool) tptp.list_node tptp.list_node Bool))) % 0.48/0.93 (define @t478 () (_ (_ (_ @t477 @t476) @t475) @t474)) % 0.48/0.93 (define @t479 () (@var "Va" tptp.list_node)) % 0.48/0.93 (define @t480 () (@var "V" tptp.node)) % 0.48/0.93 (define @t481 () (_ (_ tptp.cons_node @t480) @t479)) % 0.48/0.93 (define @t482 () (@var "R3" (-> tptp.node tptp.node Bool))) % 0.48/0.93 (define @t483 () (_ @t477 @t482)) % 0.48/0.93 (define @t484 () (_ @t483 @t398)) % 0.48/0.93 (define @t485 () (_ @t483 @t399)) % 0.48/0.93 (define @t486 () (_ (_ @t482 @t221) @t458)) % 0.48/0.93 (define @t487 () (@list @t477 @t476 @t475 @t474)) % 0.48/0.93 (define @t488 () (@var "A0" (-> tptp.node tptp.node))) % 0.48/0.93 (define @t489 () (@var "P" (-> (-> tptp.node tptp.node) tptp.list_node tptp.list_node Bool))) % 0.48/0.93 (define @t490 () (@var "Bs" tptp.list_node)) % 0.48/0.93 (define @t491 () (@var "As" tptp.list_node)) % 0.48/0.93 (define @t492 () (@var "A3" tptp.node)) % 0.48/0.93 (define @t493 () (_ tptp.cons_node @t492)) % 0.48/0.93 (define @t494 () (_ @t493 @t491)) % 0.48/0.93 (define @t495 () (@var "F" (-> tptp.node tptp.node))) % 0.48/0.93 (define @t496 () (_ @t489 @t495)) % 0.48/0.93 (define @t497 () (_ @t388 @t66)) % 0.48/0.93 (define @t498 () (_ @t388 @t399)) % 0.48/0.93 (define @t499 () (_ @t388 @t398)) % 0.48/0.93 (define @t500 () (not (= @t398 tptp.nil_node))) % 0.48/0.93 (define @t501 () (@list @t221 @t398)) % 0.48/0.93 (define @t502 () (_ @t391 tptp.nil_node)) % 0.48/0.93 (define @t503 () (forall @t223 (_ @t388 @t502))) % 0.48/0.93 (define @t504 () (@list @t66 @t388)) % 0.48/0.93 (define @t505 () (@var "P2" (-> tptp.node tptp.node Bool))) % 0.48/0.93 (define @t506 () (_ @t477 @t505)) % 0.48/0.93 (define @t507 () (_ @t506 tptp.nil_node)) % 0.48/0.93 (define @t508 () (@list @t505 @t480 @t479)) % 0.48/0.93 (define @t509 () (@var "B2" tptp.node)) % 0.48/0.93 (define @t510 () (@list @t505)) % 0.48/0.93 (define @t511 () (@var "P" (-> (-> tptp.node tptp.node Bool) tptp.list_node Bool))) % 0.48/0.93 (define @t512 () (_ (_ @t511 @t476) @t475)) % 0.48/0.93 (define @t513 () (_ @t459 @t398)) % 0.48/0.93 (define @t514 () (_ @t391 @t513)) % 0.48/0.93 (define @t515 () (_ @t511 @t505)) % 0.48/0.93 (define @t516 () (forall @t510 (_ @t515 tptp.nil_node))) % 0.48/0.93 (define @t517 () (@list @t511 @t476 @t475)) % 0.48/0.93 (define @t518 () (@var "X23" tptp.node)) % 0.48/0.93 (define @t519 () (@var "X1" tptp.node)) % 0.48/0.93 (define @t520 () (_ tptp.cons_node @t519)) % 0.48/0.93 (define @t521 () (@list @t388 @t66)) % 0.48/0.93 (define @t522 () (= @t221 @t458)) % 0.48/0.93 (define @t523 () (not @t522)) % 0.48/0.93 (define @t524 () (@list @t221 @t458 @t398)) % 0.48/0.93 (define @t525 () (= @t55 tptp.nil_node)) % 0.48/0.93 (define @t526 () (@list @t55)) % 0.48/0.93 (define @t527 () (@var "W2" tptp.list_node)) % 0.48/0.93 (define @t528 () (@var "W1" tptp.list_node)) % 0.48/0.93 (define @t529 () (@var "W23" tptp.list_node)) % 0.48/0.93 (define @t530 () (@var "E3" tptp.node)) % 0.48/0.93 (define @t531 () (_ tptp.cons_node @t530)) % 0.48/0.93 (define @t532 () (@var "W13" tptp.list_node)) % 0.48/0.93 (define @t533 () (_ @t456 @t532)) % 0.48/0.93 (define @t534 () (@var "W22" tptp.list_node)) % 0.48/0.93 (define @t535 () (@var "W12" tptp.list_node)) % 0.48/0.93 (define @t536 () (_ @t471 tptp.nil_node)) % 0.48/0.93 (define @t537 () (@var "Xss" tptp.list_list_node)) % 0.48/0.93 (define @t538 () (@var "X" tptp.list_list_node)) % 0.48/0.93 (define @t539 () (_ (_ @t456 @t387) @t475)) % 0.48/0.93 (define @t540 () (@list @t456 @t387 @t475)) % 0.48/0.93 (define @t541 () (@var "X222" tptp.list_node)) % 0.48/0.93 (define @t542 () (@var "X212" tptp.node)) % 0.48/0.93 (define @t543 () (@var "Zs2" tptp.list_node)) % 0.48/0.93 (define @t544 () (_ @t459 @t543)) % 0.48/0.93 (define @t545 () (_ @t468 @t390)) % 0.48/0.93 (define @t546 () (@list @t458 @t390)) % 0.48/0.93 (define @t547 () (@list @t456 @t66 @t69)) % 0.48/0.93 (define @t548 () (@var "Ys3" tptp.list_node)) % 0.48/0.93 (define @t549 () (@var "Y3" tptp.node)) % 0.48/0.93 (define @t550 () (@var "List" tptp.list_node)) % 0.48/0.93 (define @t551 () (@var "X23" tptp.list_node)) % 0.48/0.93 (define @t552 () (@var "X223" tptp.list_node)) % 0.48/0.93 (define @t553 () (@var "X213" tptp.node)) % 0.48/0.93 (define @t554 () (@var "B2" tptp.list_node)) % 0.48/0.93 (define @t555 () (= @t550 tptp.nil_node)) % 0.48/0.93 (define @t556 () (not @t555)) % 0.48/0.93 (define @t557 () (not (= @t354 tptp.nil_node))) % 0.48/0.93 (define @t558 () (@list @t354)) % 0.48/0.93 (define @t559 () (@list @t196 @t194)) % 0.48/0.93 (define @t560 () (@var "Z2" tptp.list_val)) % 0.48/0.93 (define @t561 () (_ tptp.member_val @t102)) % 0.48/0.93 (define @t562 () (@var "Z1" tptp.val)) % 0.48/0.93 (define @t563 () (_ tptp.set_val2 @t200)) % 0.48/0.93 (define @t564 () (@var "Z2" tptp.list_node)) % 0.48/0.93 (define @t565 () (_ tptp.member_node @t123)) % 0.48/0.93 (define @t566 () (@var "Z1" tptp.node)) % 0.48/0.93 (define @t567 () (_ tptp.set_node2 @t138)) % 0.48/0.93 (define @t568 () (_ tptp.member_val @t58)) % 0.48/0.93 (define @t569 () (_ tptp.member_node @t67)) % 0.48/0.93 (define @t570 () (_ tptp.set_node2 @t336)) % 0.48/0.93 (define @t571 () (_ tptp.set_val2 @t188)) % 0.48/0.93 (define @t572 () (_ tptp.set_node2 @t197)) % 0.48/0.93 (define @t573 () (= @t336 @t229)) % 0.48/0.93 (define @t574 () (@var "C22" tptp.list_node)) % 0.48/0.93 (define @t575 () (@var "Qs2" tptp.node)) % 0.48/0.93 (define @t576 () (_ tptp.cons_node @t575)) % 0.48/0.93 (define @t577 () (_ @t576 @t574)) % 0.48/0.93 (define @t578 () (@var "C212" tptp.list_node)) % 0.48/0.93 (define @t579 () (@var "C2" tptp.list_node)) % 0.48/0.93 (define @t580 () (@var "Qs" tptp.node)) % 0.48/0.93 (define @t581 () (_ tptp.cons_node @t580)) % 0.48/0.93 (define @t582 () (@var "C1" tptp.list_node)) % 0.48/0.93 (define @t583 () (_ tptp.append_node @t582)) % 0.48/0.93 (define @t584 () (@var "C12" tptp.list_node)) % 0.48/0.93 (define @t585 () (_ @t581 @t579)) % 0.48/0.93 (define @t586 () (@var "C21" tptp.list_node)) % 0.48/0.93 (define @t587 () (_ tptp.append_node @t584)) % 0.48/0.93 (define @t588 () (_ @t260 @t69)) % 0.48/0.93 (define @t589 () (@var "Ys4" tptp.list_node)) % 0.48/0.93 (define @t590 () (= @t228 @t336)) % 0.48/0.93 (define @t591 () (=> (=> @t250 (not @t590)) (not (forall (@list @t589) (=> (= @t69 (_ @t313 @t589)) (not (= (_ (_ tptp.append_node @t589) @t228) @t66))))))) % 0.48/0.93 (define @t592 () (= @t229 @t336)) % 0.48/0.93 (define @t593 () (@list @t69 @t228 @t71 @t66)) % 0.48/0.93 (define @t594 () (@list @t71 @t66 @t69 @t228)) % 0.48/0.93 (define @t595 () (_ @t459 tptp.nil_node)) % 0.48/0.93 (define @t596 () (_ tptp.append_node @t390)) % 0.48/0.93 (define @t597 () (_ @t596 @t595)) % 0.48/0.93 (define @t598 () (_ (_ tptp.append_node @t398) @t502)) % 0.48/0.93 (define @t599 () (_ @t456 @t598)) % 0.48/0.93 (define @t600 () (_ @t599 @t597)) % 0.48/0.93 (define @t601 () (not (= @t390 tptp.nil_node))) % 0.48/0.93 (define @t602 () (_ @t456 @t502)) % 0.48/0.93 (define @t603 () (=> @t499 (_ @t388 @t598))) % 0.48/0.93 (define @t604 () (@var "Ys5" tptp.list_node)) % 0.48/0.93 (define @t605 () (_ (_ tptp.append_node @t604) @t228)) % 0.48/0.93 (define @t606 () (_ @t313 @t604)) % 0.48/0.93 (define @t607 () (@list @t604)) % 0.48/0.93 (define @t608 () (_ tptp.cons_node @t216)) % 0.48/0.93 (define @t609 () (_ @t608 tptp.nil_node)) % 0.48/0.93 (define @t610 () (@var "Xs3" tptp.list_node)) % 0.48/0.93 (define @t611 () (=> @t545 @t600)) % 0.48/0.93 (define @t612 () (forall @t501 (_ @t599 tptp.nil_node))) % 0.48/0.93 (define @t613 () (_ @t531 tptp.nil_node)) % 0.48/0.93 (define @t614 () (@var "Ll" tptp.list_node)) % 0.48/0.93 (define @t615 () (not (_ @t208 @t549))) % 0.48/0.93 (define @t616 () (_ tptp.set_node2 @t548)) % 0.48/0.93 (define @t617 () (_ tptp.member_node @t549)) % 0.48/0.93 (define @t618 () (@list @t549)) % 0.48/0.93 (define @t619 () (_ @t208 @t216)) % 0.48/0.93 (define @t620 () (@var "Zs3" tptp.list_node)) % 0.48/0.93 (define @t621 () (_ tptp.append_node @t548)) % 0.48/0.93 (define @t622 () (= @t66 (_ @t621 (_ @t608 @t620)))) % 0.48/0.93 (define @t623 () (@list @t620)) % 0.48/0.93 (define @t624 () (_ @t217 @t73)) % 0.48/0.93 (define @t625 () (exists @t218 (and @t624 @t619))) % 0.48/0.93 (define @t626 () (@list @t66 @t208)) % 0.48/0.93 (define @t627 () (_ tptp.set_node2 @t620)) % 0.48/0.93 (define @t628 () (@var "Ys3" tptp.list_val)) % 0.48/0.93 (define @t629 () (@var "Zs3" tptp.list_val)) % 0.48/0.93 (define @t630 () (= @t57 (_ (_ tptp.append_val @t628) (_ @t304 @t629)))) % 0.48/0.93 (define @t631 () (@list @t628 @t629)) % 0.48/0.93 (define @t632 () (= @t66 (_ @t621 (_ @t313 @t620)))) % 0.48/0.93 (define @t633 () (@list @t548 @t620)) % 0.48/0.93 (define @t634 () (@var "Xa" tptp.node)) % 0.48/0.93 (define @t635 () (not (_ @t208 @t634))) % 0.48/0.93 (define @t636 () (_ tptp.set_node2 @t390)) % 0.48/0.93 (define @t637 () (_ tptp.member_node @t634)) % 0.48/0.93 (define @t638 () (@list @t634)) % 0.48/0.93 (define @t639 () (forall @t638 (=> (_ @t637 @t636) @t635))) % 0.48/0.93 (define @t640 () (= @t66 (_ @t596 (_ @t391 @t543)))) % 0.48/0.93 (define @t641 () (@list @t543)) % 0.48/0.93 (define @t642 () (exists @t641 @t640)) % 0.48/0.93 (define @t643 () (@list @t390 @t221)) % 0.48/0.93 (define @t644 () (exists @t183 (and (_ @t181 @t73) @t283))) % 0.48/0.93 (define @t645 () (_ tptp.set_node2 @t543)) % 0.48/0.93 (define @t646 () (forall @t638 (=> (_ @t637 @t645) @t635))) % 0.48/0.93 (define @t647 () (@list @t390 @t221 @t543)) % 0.48/0.93 (define @t648 () (@var "L22" tptp.list_val)) % 0.48/0.93 (define @t649 () (@var "L12" tptp.list_val)) % 0.48/0.93 (define @t650 () (_ tptp.append_val @t649)) % 0.48/0.93 (define @t651 () (@list @t649 @t648)) % 0.48/0.93 (define @t652 () (_ tptp.set_val2 @t346)) % 0.48/0.93 (define @t653 () (@var "L22" tptp.list_node)) % 0.48/0.93 (define @t654 () (@var "L12" tptp.list_node)) % 0.48/0.93 (define @t655 () (_ tptp.append_node @t654)) % 0.48/0.93 (define @t656 () (@list @t654 @t653)) % 0.48/0.93 (define @t657 () (_ tptp.set_node2 @t354)) % 0.48/0.93 (define @t658 () (@var "Ys6" tptp.list_val)) % 0.48/0.93 (define @t659 () (@var "Xs4" tptp.list_val)) % 0.48/0.93 (define @t660 () (@var "Ys6" tptp.list_node)) % 0.48/0.93 (define @t661 () (@var "Xs4" tptp.list_node)) % 0.48/0.93 (define @t662 () (_ tptp.set_node2 @t69)) % 0.48/0.93 (define @t663 () (@var "Zs2" tptp.list_val)) % 0.48/0.93 (define @t664 () (= @t57 (_ (_ tptp.append_val @t385) (_ @t304 @t663)))) % 0.48/0.93 (define @t665 () (@list @t385 @t663)) % 0.48/0.93 (define @t666 () (= @t66 (_ @t596 (_ @t313 @t543)))) % 0.48/0.93 (define @t667 () (@list @t390 @t543)) % 0.48/0.93 (define @t668 () (@var "L3" tptp.list_val)) % 0.48/0.93 (define @t669 () (_ tptp.append_val @t648)) % 0.48/0.93 (define @t670 () (@list @t649 @t648 @t668)) % 0.48/0.93 (define @t671 () (not @t303)) % 0.48/0.93 (define @t672 () (_ @t63 @t652)) % 0.48/0.93 (define @t673 () (@var "L3" tptp.list_node)) % 0.48/0.93 (define @t674 () (_ tptp.append_node @t653)) % 0.48/0.93 (define @t675 () (@list @t654 @t653 @t673)) % 0.48/0.93 (define @t676 () (not @t309)) % 0.48/0.93 (define @t677 () (_ @t72 @t657)) % 0.48/0.93 (define @t678 () (= @t94 tptp.nil_node)) % 0.48/0.93 (define @t679 () (or @t97 (exists @t218 (= @t66 @t609)))) % 0.48/0.93 (define @t680 () (not (= @t200 tptp.nil_val))) % 0.48/0.93 (define @t681 () (= @t138 tptp.nil_node)) % 0.48/0.93 (define @t682 () (not @t681)) % 0.48/0.93 (define @t683 () (_ tptp.prefix_node @t66)) % 0.48/0.93 (define @t684 () (_ @t683 @t69)) % 0.48/0.93 (define @t685 () (@list @t66 @t69 @t67)) % 0.48/0.93 (define @t686 () (_ @t313 @t264)) % 0.48/0.93 (define @t687 () (@var "Ns_3" tptp.list_node)) % 0.48/0.93 (define @t688 () (_ @t299 @t314)) % 0.48/0.93 (define @t689 () (_ tptp.prefix_node @t96)) % 0.48/0.93 (define @t690 () (_ tptp.set_node2 @t274)) % 0.48/0.93 (define @t691 () (_ tptp.tl_node @t17)) % 0.48/0.93 (define @t692 () (_ tptp.hd_node @t691)) % 0.48/0.93 (define @t693 () (_ (_ (_ (_ tptp.graph_435229452_edgeD tptp.alpha_n) tptp.invar) tptp.inEdges) @t4)) % 0.48/0.93 (define @t694 () (_ tptp.prefix_node @t55)) % 0.48/0.93 (define @t695 () (_ tptp.prefix_node @t138)) % 0.48/0.93 (define @t696 () (_ tptp.suffix_node @t55)) % 0.48/0.93 (define @t697 () (_ tptp.suffix_node @t138)) % 0.48/0.93 (define @t698 () (_ @t693 @t17)) % 0.48/0.93 (define @t699 () (@list @t4 @t17)) % 0.48/0.93 (define @t700 () (_ tptp.hd_node @t17)) % 0.48/0.93 (define @t701 () (_ @t693 @t80)) % 0.48/0.93 (define @t702 () (_ @t296 @t34)) % 0.48/0.93 (define @t703 () (_ @t693 (_ @t18 @t702))) % 0.48/0.93 (define @t704 () (@list @t4 @t17 @t24 @t34)) % 0.48/0.93 (define @t705 () (_ @t68 @t69)) % 0.48/0.93 (define @t706 () (@list @t71 @t66 @t67 @t69)) % 0.48/0.93 (define @t707 () (_ @t697 tptp.nil_node)) % 0.48/0.93 (define @t708 () (_ tptp.suffix_node @t66)) % 0.48/0.93 (define @t709 () (_ tptp.suffix_node @t236)) % 0.48/0.93 (define @t710 () (_ @t693 @t323)) % 0.48/0.93 (define @t711 () (@var "Ns5" tptp.list_node)) % 0.48/0.93 (define @t712 () (@var "N6" tptp.node)) % 0.48/0.93 (define @t713 () (@var "N5" tptp.node)) % 0.48/0.93 (define @t714 () (_ @t693 @t138)) % 0.48/0.93 (define @t715 () (@list @t4 @t138)) % 0.48/0.93 (define @t716 () (_ @t295 (_ tptp.set_node2 (_ @t240 (_ tptp.hd_node @t291))))) % 0.48/0.93 (define @t717 () (_ @t693 @t291)) % 0.48/0.93 (define @t718 () (@list @t291 @t292)) % 0.48/0.93 (define @t719 () (_ (_ tptp.cons_node @t294) tptp.nil_node)) % 0.48/0.93 (define @t720 () (_ (_ tptp.member_node @t294) @t44)) % 0.48/0.93 (define @t721 () (@list @t294)) % 0.48/0.93 (define @t722 () (_ tptp.hd_node @t66)) % 0.48/0.93 (define @t723 () (_ tptp.hd_node @t96)) % 0.48/0.93 (define @t724 () (=> @t98 (= @t723 @t722))) % 0.48/0.93 (define @t725 () (_ tptp.append_node @t620)) % 0.48/0.93 (define @t726 () (_ @t708 @t69)) % 0.48/0.93 (define @t727 () (_ tptp.tl_node @t550)) % 0.48/0.93 (define @t728 () (_ tptp.hd_node @t550)) % 0.48/0.93 (define @t729 () (_ (_ tptp.cons_node @t728) @t727)) % 0.48/0.93 (define @t730 () (@list @t550)) % 0.48/0.93 (define @t731 () (_ @t36 @t15)) % 0.48/0.93 (define @t732 () (_ tptp.ord_less_eq_set_node @t73)) % 0.48/0.93 (define @t733 () (_ @t732 @t662)) % 0.48/0.93 (define @t734 () (@var "S" tptp.set_node)) % 0.48/0.93 (define @t735 () (@var "D" tptp.set_node)) % 0.48/0.93 (define @t736 () (@var "A" tptp.set_node)) % 0.48/0.93 (define @t737 () (@var "C" tptp.set_node)) % 0.48/0.93 (define @t738 () (@var "B" tptp.set_node)) % 0.48/0.93 (define @t739 () (_ tptp.suffix_node @t336)) % 0.48/0.93 (define @t740 () (_ @t708 @t705)) % 0.48/0.93 (define @t741 () (_ tptp.suffix_node tptp.nil_node)) % 0.48/0.93 (define @t742 () (@var "Xs5" tptp.list_node)) % 0.48/0.93 (define @t743 () (@var "Xs_1" tptp.list_node)) % 0.48/0.93 (define @t744 () (@var "Xs_2" tptp.list_node)) % 0.48/0.93 (define @t745 () (_ tptp.suffix_node @t744)) % 0.48/0.93 (define @t746 () (_ tptp.suffix_node @t743)) % 0.48/0.93 (define @t747 () (@list @t743 @t69 @t744)) % 0.48/0.93 (define @t748 () (@var "Y3" tptp.list_node)) % 0.48/0.93 (define @t749 () (@list @t259 @t748)) % 0.48/0.93 (define @t750 () (@var "Z" tptp.list_node)) % 0.48/0.93 (define @t751 () (@var "Y4" tptp.list_node)) % 0.48/0.93 (define @t752 () (lambda (@list @t751 @t750) (= @t751 @t750))) % 0.48/0.93 (define @t753 () (_ tptp.suffix_node @t51)) % 0.48/0.93 (define @t754 () (_ @t753 @t55)) % 0.48/0.93 (define @t755 () (_ @t696 @t51)) % 0.48/0.93 (define @t756 () (@list @t55 @t51)) % 0.48/0.93 (define @t757 () (_ @t697 @t202)) % 0.48/0.93 (define @t758 () (_ tptp.suffix_node @t203)) % 0.48/0.93 (define @t759 () (=> (_ @t758 @t202) @t757)) % 0.48/0.93 (define @t760 () (_ @t697 @t203)) % 0.48/0.93 (define @t761 () (@var "Z3" tptp.list_node)) % 0.48/0.93 (define @t762 () (@var "A4" tptp.list_node)) % 0.48/0.93 (define @t763 () (@var "B3" tptp.list_node)) % 0.48/0.93 (define @t764 () (_ (_ tptp.suffix_node @t763) @t762)) % 0.48/0.93 (define @t765 () (_ (_ tptp.suffix_node @t762) @t763)) % 0.48/0.93 (define @t766 () (@list @t762 @t763)) % 0.48/0.93 (define @t767 () (= @t138 @t203)) % 0.48/0.93 (define @t768 () (_ @t758 @t138)) % 0.48/0.93 (define @t769 () (_ tptp.suffix_node @t202)) % 0.48/0.93 (define @t770 () (@var "B4" tptp.set_val)) % 0.48/0.93 (define @t771 () (@var "B4" tptp.set_node)) % 0.48/0.93 (define @t772 () (_ tptp.hd_val @t57)) % 0.48/0.93 (define @t773 () (@var "Xs6" tptp.list_node)) % 0.48/0.93 (define @t774 () (@var "Ps" tptp.list_node)) % 0.48/0.93 (define @t775 () (_ tptp.append_node @t774)) % 0.48/0.93 (define @t776 () (= @t221 @t492)) % 0.48/0.93 (define @t777 () (@var "Ls" tptp.list_node)) % 0.48/0.93 (define @t778 () (= @t777 @t598)) % 0.48/0.93 (define @t779 () (@var "Ps2" tptp.list_node)) % 0.48/0.93 (define @t780 () (= @t779 (_ (_ tptp.append_node @t491) (_ @t493 tptp.nil_node)))) % 0.48/0.93 (define @t781 () (not (_ (_ tptp.suffix_node @t779) @t777))) % 0.48/0.93 (define @t782 () (@var "List2" tptp.list_node)) % 0.48/0.93 (define @t783 () (= @t782 tptp.nil_node)) % 0.48/0.93 (define @t784 () (_ tptp.set_node2 @t94)) % 0.48/0.93 (define @t785 () (_ @t732 @t215)) % 0.48/0.93 (define @t786 () (@list @t66 @t215)) % 0.48/0.93 (define @t787 () (_ tptp.prefix_node @t744)) % 0.48/0.93 (define @t788 () (_ tptp.prefix_node @t743)) % 0.48/0.93 (define @t789 () (_ tptp.tl_node tptp.ri)) % 0.48/0.93 (define @t790 () (_ tptp.append_node tptp.ns)) % 0.48/0.93 (define @t791 () (_ @t790 @t789)) % 0.48/0.93 (define @t792 () (_ (_ @t9 @t791) @t2)) % 0.48/0.93 (define @t793 () (not @t792)) % 0.48/0.93 (define @t794 () (lambda (@list @t610 @t548) (exists @t623 (= @t548 (_ @t725 @t610))))) % 0.48/0.93 (define @t795 () (tptp.tl_node @t15)) % 0.48/0.93 (define @t796 () (tptp.append_node @t17 @t795)) % 0.48/0.93 (define @t797 () (tptp.graph_1012773594_edgeD tptp.alpha_n tptp.invar tptp.inEdges @t4 @t20 @t796 @t14)) % 0.48/0.93 (define @t798 () (tptp.graph_1012773594_edgeD tptp.alpha_n tptp.invar tptp.inEdges @t4 @t24 @t15 @t14)) % 0.48/0.93 (define @t799 () (not @t25)) % 0.48/0.93 (define @t800 () (tptp.graph_1012773594_edgeD tptp.alpha_n tptp.invar tptp.inEdges @t4 @t20 @t17 @t24)) % 0.48/0.93 (define @t801 () (not @t28)) % 0.48/0.93 (define @t802 () (or @t801 @t799 @t23)) % 0.48/0.93 (define @t803 () (tptp.sSA_CF551432799de_val tptp.alpha_n tptp.defs tptp.phis tptp.g2 tptp.phi_r)) % 0.48/0.93 (define @t804 () (tptp.sSA_CF551432799de_val tptp.alpha_n tptp.defs tptp.phis tptp.g2 tptp.r)) % 0.48/0.93 (define @t805 () (tptp.graph_1012773594_edgeD tptp.alpha_n tptp.invar tptp.inEdges tptp.g2 @t804 tptp.ri @t803)) % 0.48/0.93 (define @t806 () (tptp.graph_1012773594_edgeD tptp.alpha_n tptp.invar tptp.inEdges tptp.g2 tptp.n tptp.ns @t804)) % 0.48/0.93 (define @t807 () (tptp.tl_node tptp.ri)) % 0.48/0.93 (define @t808 () (tptp.append_node tptp.ns @t807)) % 0.48/0.93 (define @t809 () (tptp.graph_1012773594_edgeD tptp.alpha_n tptp.invar tptp.inEdges tptp.g2 tptp.n @t808 @t803)) % 0.48/0.93 (define @t810 () (not @t805)) % 0.48/0.93 (define @t811 () (not @t806)) % 0.48/0.93 (define @t812 () (or @t811 @t810 @t809)) % 0.48/0.93 (define @t813 () (not @t812)) % 0.48/0.93 (define @t814 () (forall @t29 (or (not @t800) (not @t798) @t797))) % 0.48/0.93 (assume @p1 (not (= tptp.r tptp.phi_r))) % 0.48/0.93 (assume @p2 @t3) % 0.48/0.93 (assume @p3 (forall (@list @t4) @t5)) % 0.48/0.93 (assume @p4 @t11) % 0.48/0.93 (assume @p5 (_ @t13 tptp.i)) % 0.48/0.93 (assume @p6 @t30) % 0.48/0.93 (assume @p7 (not (= @t2 @t6))) % 0.48/0.93 (assume @p8 (_ (_ @t12 tptp.rs) tptp.pred_phi_r)) % 0.48/0.93 (assume @p9 (_ (_ (_ (_ (_ (_ tptp.sSA_CF1252180629de_val tptp.alpha_n) tptp.defs) tptp.phis) tptp.g2) tptp.phi_r) tptp.r)) % 0.48/0.93 (assume @p10 (_ (_ @t12 tptp.rs2) @t2)) % 0.48/0.93 (assume @p11 (_ (_ @t31 tptp.ms2) tptp.i)) % 0.48/0.93 (assume @p12 (=> @t33 (=> (=> @t33 (not @t32)) (not (=> @t33 @t32))))) % 0.48/0.93 (assume @p13 (forall @t40 (=> @t39 (_ (_ @t38 @t37) @t24)))) % 0.48/0.93 (assume @p14 (forall @t42 (=> @t28 @t41))) % 0.48/0.93 (assume @p15 (forall (@list @t4 @t20 @t24) (not (_ (_ @t22 tptp.nil_node) @t24)))) % 0.48/0.93 (assume @p16 (_ (_ tptp.member_val tptp.r) (_ (_ @t43 tptp.g2) tptp.pred_phi_r))) % 0.48/0.93 (assume @p17 (forall @t42 (=> @t28 @t46))) % 0.48/0.93 (assume @p18 (forall @t42 (=> @t28 @t48))) % 0.48/0.93 (assume @p19 (forall (@list @t4 @t20 @t17 @t24 @t14) (=> @t28 (=> (_ @t49 @t47) (_ @t49 @t44))))) % 0.48/0.93 (assume @p20 (forall (@list @t55 @t50 @t53 @t51) (=> (_ @t56 (_ tptp.set_list_node2 @t50)) (_ @t56 (_ tptp.set_list_node2 (_ tptp.tl_list_node (_ @t54 (_ @t52 @t50)))))))) % 0.48/0.93 (assume @p21 (forall (@list @t62 @t57 @t60 @t58) (=> @t65 (_ @t63 (_ tptp.set_val2 (_ tptp.tl_val (_ @t61 (_ @t59 @t57)))))))) % 0.48/0.93 (assume @p22 (forall (@list @t71 @t66 @t69 @t67) (=> @t74 (_ @t72 (_ tptp.set_node2 (_ tptp.tl_node (_ @t70 (_ @t68 @t66)))))))) % 0.48/0.93 (assume @p23 (_ @t76 @t75)) % 0.48/0.93 (assume @p24 (forall @t42 (=> @t28 (_ @t77 @t44)))) % 0.48/0.93 (assume @p25 (forall @t42 (=> @t28 (_ @t77 @t47)))) % 0.48/0.93 (assume @p26 (forall @t40 (=> @t39 (_ (_ @t22 (_ @t18 (_ @t36 tptp.nil_node))) @t35)))) % 0.48/0.93 (assume @p27 (not (_ @t78 (_ tptp.set_node2 (_ tptp.tl_node tptp.rs2))))) % 0.48/0.93 (assume @p28 (not (_ @t78 (_ tptp.set_node2 (_ tptp.tl_node tptp.rs))))) % 0.48/0.93 (assume @p29 (= tptp.rs2 (_ (_ tptp.append_node tptp.rs) (_ (_ tptp.cons_node @t2) tptp.nil_node)))) % 0.48/0.93 (assume @p30 (_ (_ tptp.prefix_node tptp.ri) tptp.rs2)) % 0.48/0.93 (assume @p31 (forall @t81 (=> @t46 (=> @t5 (_ (_ @t22 @t80) @t20))))) % 0.48/0.93 (assume @p32 (not (_ @t76 (_ tptp.set_node2 (_ tptp.butlast_node tptp.ms2))))) % 0.48/0.93 (assume @p33 (_ (_ tptp.member_node tptp.pred_phi_r) (_ tptp.set_node2 (_ (_ @t82 tptp.g2) @t2)))) % 0.48/0.93 (assume @p34 (_ (_ @t31 tptp.ms) (_ @t1 tptp.s))) % 0.48/0.93 (assume @p35 (forall @t87 (=> @t86 (= (_ tptp.tl_list_node @t84) (_ (_ tptp.append_list_node (_ tptp.tl_list_node @t50)) @t53))))) % 0.48/0.93 (assume @p36 (forall @t93 (=> @t92 (= (_ tptp.tl_val @t90) (_ (_ tptp.append_val @t88) @t60))))) % 0.48/0.93 (assume @p37 (forall @t99 (=> @t98 (= (_ tptp.tl_node @t96) (_ (_ tptp.append_node @t94) @t69))))) % 0.48/0.93 (assume @p38 (forall (@list @t104 @t103 @t100 @t102) (= (= @t110 @t108) @t106))) % 0.48/0.93 (assume @p39 (forall (@list @t115 @t114 @t111 @t113) (= (= @t120 @t118) @t117))) % 0.48/0.93 (assume @p40 (forall (@list @t125 @t124 @t121 @t123) (= (= @t131 @t129) @t127))) % 0.48/0.93 (assume @p41 (forall (@list @t102 @t104 @t103 @t100) (= (= @t108 @t110) @t106))) % 0.48/0.93 (assume @p42 (forall (@list @t113 @t115 @t114 @t111) (= (= @t118 @t120) @t117))) % 0.48/0.93 (assume @p43 (forall (@list @t123 @t125 @t124 @t121) (= (= @t129 @t131) @t127))) % 0.48/0.93 (assume @p44 (forall (@list @t100 @t132 @t104) (=> @t137 (= @t136 @t134)))) % 0.48/0.93 (assume @p45 (forall (@list @t111 @t138 @t115) (=> @t143 (= @t142 @t140)))) % 0.48/0.93 (assume @p46 (forall (@list @t121 @t144 @t125) (=> @t149 (= @t148 @t146)))) % 0.48/0.93 (assume @p47 (forall (@list @t104 @t132 @t100) (=> @t151 (= @t136 @t150)))) % 0.48/0.93 (assume @p48 (forall (@list @t115 @t138 @t111) (=> @t153 (= @t142 @t152)))) % 0.48/0.93 (assume @p49 (forall (@list @t125 @t144 @t121) (=> @t155 (= @t148 @t154)))) % 0.48/0.93 (assume @p50 (forall (@list @t100 @t104 @t132) (=> @t137 (= @t156 @t134)))) % 0.48/0.93 (assume @p51 (forall (@list @t111 @t115 @t138) (=> @t143 (= @t157 @t140)))) % 0.48/0.93 (assume @p52 (forall (@list @t121 @t125 @t144) (=> @t149 (= @t158 @t146)))) % 0.48/0.93 (assume @p53 (forall (@list @t104 @t100 @t132) (=> @t151 (= @t156 @t150)))) % 0.48/0.93 (assume @p54 (forall (@list @t115 @t111 @t138) (=> @t153 (= @t157 @t152)))) % 0.48/0.93 (assume @p55 (forall (@list @t125 @t121 @t144) (=> @t155 (= @t158 @t154)))) % 0.48/0.93 (assume @p56 (forall (@list @t104 @t161 @t159 @t100 @t162 @t160) (= (= @t165 @t164) @t163))) % 0.48/0.93 (assume @p57 (forall (@list @t115 @t168 @t166 @t111 @t169 @t167) (= (= @t172 @t171) @t170))) % 0.48/0.93 (assume @p58 (forall (@list @t125 @t175 @t173 @t121 @t176 @t174) (= (= @t179 @t178) @t177))) % 0.48/0.93 (assume @p59 (forall (@list @t162 @t160 @t104 @t161 @t159 @t100) (= (= @t164 @t165) @t163))) % 0.48/0.93 (assume @p60 (forall (@list @t169 @t167 @t115 @t168 @t166 @t111) (= (= @t171 @t172) @t170))) % 0.48/0.93 (assume @p61 (forall (@list @t176 @t174 @t125 @t175 @t173 @t121) (= (= @t178 @t179) @t177))) % 0.48/0.93 (assume @p62 (_ (_ tptp.prefix_node tptp.ms2) tptp.ms)) % 0.48/0.93 (assume @p63 (forall @t183 (=> (_ @t181 (_ tptp.set_node2 (_ tptp.butlast_node tptp.ri))) @t182))) % 0.48/0.93 (assume @p64 (forall (@list @t187 @t185 @t186 @t184) (= (= @t188 (_ (_ tptp.cons_val @t186) @t184)) (and (= @t187 @t186) (= @t185 @t184))))) % 0.48/0.93 (assume @p65 (forall (@list @t192 @t190 @t191 @t189) (= (= (_ (_ tptp.cons_list_node @t192) @t190) (_ (_ tptp.cons_list_node @t191) @t189)) (and (= @t192 @t191) (= @t190 @t189))))) % 0.48/0.93 (assume @p66 (forall (@list @t196 @t194 @t195 @t193) (= (= @t197 (_ (_ tptp.cons_node @t195) @t193)) (and (= @t196 @t195) (= @t194 @t193))))) % 0.48/0.93 (assume @p67 (forall (@list @t200 @t199 @t198) (= (_ (_ tptp.append_val (_ @t201 @t199)) @t198) (_ @t201 (_ (_ tptp.append_val @t199) @t198))))) % 0.48/0.93 (assume @p68 (forall @t205 (= (_ (_ tptp.append_node (_ @t204 @t203)) @t202) (_ @t204 (_ (_ tptp.append_node @t203) @t202))))) % 0.48/0.93 (assume @p69 (forall (@list @t132 @t206) (= (_ (_ tptp.member_val @t132) @t207) (_ @t206 @t132)))) % 0.48/0.93 (assume @p70 (forall (@list @t144 @t208) (= (_ (_ tptp.member_node @t144) @t209) (_ @t208 @t144)))) % 0.48/0.93 (assume @p71 (forall @t214 (= (_ tptp.collect_val (lambda @t213 (_ @t212 @t210))) @t210))) % 0.48/0.93 (assume @p72 (forall @t219 (= (_ tptp.collect_node (lambda @t218 (_ @t217 @t215))) @t215))) % 0.48/0.93 (assume @p73 (forall (@list @t208 @t220) (=> (forall @t223 (= @t222 (_ @t220 @t221))) (= @t209 (_ tptp.collect_node @t220))))) % 0.48/0.93 (assume @p74 (forall (@list @t206 @t224) (=> (forall (@list @t225) (= (_ @t206 @t225) (_ @t224 @t225))) (= @t207 (_ tptp.collect_val @t224))))) % 0.48/0.93 (assume @p75 (forall @t227 (= (_ (_ tptp.append_val @t90) @t226) (_ @t89 (_ @t61 @t226))))) % 0.48/0.93 (assume @p76 (forall @t230 (= (_ (_ tptp.append_node @t96) @t228) (_ @t95 @t229)))) % 0.48/0.93 (assume @p77 (forall (@list @t60 @t57 @t226) (= (= (_ @t61 @t57) (_ @t232 @t57)) @t231))) % 0.48/0.93 (assume @p78 (forall @t237 (= (= @t236 @t235) @t233))) % 0.48/0.93 (assume @p79 (forall @t227 (= (= @t90 (_ @t89 @t226)) @t231))) % 0.48/0.93 (assume @p80 (forall @t230 (= (= @t96 @t238) @t233))) % 0.48/0.93 (assume @p81 (forall @t242 (=> @t241 @t239))) % 0.48/0.93 (assume @p82 (forall @t242 (=> @t241 (=> @t46 (=> @t5 (_ @t243 @t44)))))) % 0.48/0.93 (assume @p83 (forall @t245 (=> (not (= @t244 tptp.nil_node)) @t239))) % 0.48/0.93 (assume @p84 (forall @t29 (=> @t28 (=> @t25 (_ (_ @t22 (_ (_ tptp.append_node (_ tptp.butlast_node @t17)) @t15)) @t14))))) % 0.48/0.93 (assume @p85 (forall (@list @t50) (= (_ @t83 tptp.nil_list_node) @t50))) % 0.48/0.93 (assume @p86 (forall @t246 (= (_ @t89 tptp.nil_val) @t57))) % 0.48/0.93 (assume @p87 (forall @t247 (= (_ @t95 tptp.nil_node) @t66))) % 0.48/0.93 (assume @p88 (forall @t87 (= (= @t84 @t50) @t248))) % 0.48/0.93 (assume @p89 (forall @t93 (= (= @t90 @t57) @t249))) % 0.48/0.93 (assume @p90 (forall @t99 (= (= @t96 @t66) @t250))) % 0.48/0.93 (assume @p91 (forall @t87 (= (= @t50 @t84) @t248))) % 0.48/0.93 (assume @p92 (forall @t93 (= (= @t57 @t90) @t249))) % 0.48/0.93 (assume @p93 (forall @t99 (= (= @t66 @t96) @t250))) % 0.48/0.93 (assume @p94 (forall @t87 (= (= @t84 @t53) @t85))) % 0.48/0.93 (assume @p95 (forall @t93 (= (= @t90 @t60) @t91))) % 0.48/0.93 (assume @p96 (forall @t99 (= (= @t96 @t69) @t97))) % 0.48/0.93 (assume @p97 (forall @t251 (= (= @t53 @t84) @t85))) % 0.48/0.93 (assume @p98 (forall @t252 (= (= @t60 @t90) @t91))) % 0.48/0.93 (assume @p99 (forall @t253 (= (= @t69 @t96) @t97))) % 0.48/0.93 (assume @p100 (forall @t87 (= (= tptp.nil_list_node @t84) @t254))) % 0.48/0.93 (assume @p101 (forall @t93 (= (= tptp.nil_val @t90) @t255))) % 0.48/0.93 (assume @p102 (forall @t99 (= (= tptp.nil_node @t96) @t256))) % 0.48/0.93 (assume @p103 (forall @t87 (= (= @t84 tptp.nil_list_node) @t254))) % 0.48/0.93 (assume @p104 (forall @t93 (= (= @t90 tptp.nil_val) @t255))) % 0.48/0.93 (assume @p105 (forall @t99 (= (= @t96 tptp.nil_node) @t256))) % 0.48/0.93 (assume @p106 (= (_ tptp.append_list_node tptp.nil_list_node) (lambda (@list @t257) @t257))) % 0.48/0.93 (assume @p107 (= (_ tptp.append_val tptp.nil_val) (lambda (@list @t258) @t258))) % 0.48/0.93 (assume @p108 (= @t260 (lambda (@list @t259) @t259))) % 0.48/0.93 (assume @p109 (forall (@list @t261) (= (_ (_ tptp.append_list_node @t261) tptp.nil_list_node) @t261))) % 0.48/0.93 (assume @p110 (forall @t262 (= (_ @t201 tptp.nil_val) @t200))) % 0.48/0.93 (assume @p111 (forall @t263 (= (_ @t204 tptp.nil_node) @t138))) % 0.48/0.93 (assume @p112 (forall @t273 (=> @t28 (=> @t272 (not (forall @t271 (=> @t270 (forall @t269 (=> @t268 @t266))))))))) % 0.48/0.93 (assume @p113 (forall @t282 (=> @t28 (=> (_ @t278 @t47) (not (forall @t281 (=> (_ @t280 @t277) (=> @t279 (_ @t278 @t276))))))))) % 0.48/0.93 (assume @p114 (forall @t287 (=> @t28 (=> @t286 (not (forall (@list @t285 @t274) (=> (_ @t280 @t285) (=> (_ @t208 @t285) (=> (forall @t183 (=> (_ @t181 @t276) @t284)) (not @t279)))))))))) % 0.48/0.93 (assume @p115 (forall @t298 (=> @t28 (=> (=> @t5 (_ (_ (_ @t288 @t24) @t297) @t24)) (=> (forall (@list @t291 @t292 @t294) (=> (_ (_ (_ @t21 @t294) @t291) @t24) (=> (_ (_ (_ @t288 @t294) @t291) @t24) (=> (_ @t295 (_ tptp.set_node2 (_ @t240 @t294))) (_ (_ (_ @t288 @t292) @t293) @t24))))) @t290))))) % 0.48/0.93 (assume @p116 (forall @t273 (=> @t28 (=> @t272 (not (forall @t271 (=> @t270 (forall @t269 (=> @t268 (=> (= @t17 (_ @t299 (_ tptp.tl_node @t264))) @t266)))))))))) % 0.48/0.93 (assume @p117 (forall (@list @t4 @t20 @t17 @t24 @t34 @t277) (=> @t28 (=> (_ (_ tptp.prefix_node @t301) @t17) (_ (_ @t22 @t301) @t277))))) % 0.48/0.93 (assume @p118 (forall @t298 (=> @t28 (=> (=> @t46 (_ (_ @t289 @t80) @t20)) (=> (forall (@list @t291 @t285 @t302) (=> (_ (_ @t22 @t291) @t285) (=> (_ (_ @t289 @t291) @t285) (=> (_ (_ tptp.member_node @t285) (_ tptp.set_node2 (_ @t240 @t302))) (_ (_ @t289 (_ (_ tptp.append_node @t291) (_ (_ tptp.cons_node @t302) tptp.nil_node))) @t302))))) @t290))))) % 0.48/0.93 (assume @p119 (forall @t282 (=> @t28 (=> (_ @t77 (_ tptp.set_node2 (_ @t240 @t277))) (_ (_ @t22 (_ @t18 @t300)) @t277))))) % 0.48/0.93 (assume @p120 (forall (@list @t57 @t62 @t60 @t58) (= (= @t305 (_ @t61 (_ @t59 tptp.nil_val))) (and (= @t57 @t60) @t303)))) % 0.48/0.93 (assume @p121 (forall (@list @t50 @t55 @t53 @t51) (= (= @t308 (_ @t54 (_ @t52 tptp.nil_list_node))) (and (= @t50 @t53) @t306)))) % 0.48/0.93 (assume @p122 (forall @t316 (= (= @t315 @t312) (and @t310 @t309)))) % 0.48/0.93 (assume @p123 (forall @t317 (= (_ tptp.butlast_val @t305) @t57))) % 0.48/0.93 (assume @p124 (forall @t318 (= (_ tptp.butlast_list_node @t308) @t50))) % 0.48/0.93 (assume @p125 (forall @t319 (= (_ tptp.butlast_node @t315) @t66))) % 0.48/0.93 (assume @p126 (not (forall (@list @t320) (=> (_ (_ @t31 @t320) tptp.i) (=> (_ (_ tptp.prefix_node @t320) tptp.ms) (_ @t76 (_ tptp.set_node2 (_ tptp.butlast_node @t320)))))))) % 0.48/0.93 (assume @p127 (not (forall (@list @t322 @t321) (=> (_ (_ @t12 @t321) @t322) (=> (_ (_ tptp.member_node @t322) @t75) (=> (forall @t183 (=> (_ @t181 (_ tptp.set_node2 (_ tptp.butlast_node @t321))) @t182)) (not (_ (_ tptp.prefix_node @t321) tptp.rs2)))))))) % 0.48/0.93 (assume @p128 (forall (@list @t4 @t20 @t17 @t24 @t35) (=> @t28 (=> (_ @t243 (_ tptp.set_node2 @t244)) (_ (_ @t38 @t323) @t24))))) % 0.48/0.93 (assume @p129 (= (_ tptp.butlast_list_node tptp.nil_list_node) tptp.nil_list_node)) % 0.48/0.93 (assume @p130 (= (_ tptp.butlast_val tptp.nil_val) tptp.nil_val)) % 0.48/0.93 (assume @p131 (= (_ tptp.butlast_node tptp.nil_node) tptp.nil_node)) % 0.48/0.93 (assume @p132 (forall @t326 (=> @t325 @t65))) % 0.48/0.93 (assume @p133 (forall @t330 (=> @t329 @t74))) % 0.48/0.93 (assume @p134 (forall @t246 (= (_ tptp.butlast_val @t88) (_ tptp.tl_val @t324)))) % 0.48/0.93 (assume @p135 (forall @t247 (= (_ tptp.butlast_node @t94) (_ tptp.tl_node @t327)))) % 0.48/0.93 (assume @p136 (forall @t317 (and (=> @t91 (= @t332 tptp.nil_val)) (=> @t92 (= @t332 (_ @t304 @t324)))))) % 0.48/0.93 (assume @p137 (forall @t318 (and (=> @t85 (= @t335 tptp.nil_list_node)) (=> @t86 (= @t335 (_ @t307 @t333)))))) % 0.48/0.93 (assume @p138 (forall @t319 (and (=> @t97 (= @t337 tptp.nil_node)) (=> @t98 (= @t337 (_ @t313 @t327)))))) % 0.48/0.93 (assume @p139 (forall @t251 (and (=> @t248 (= @t338 @t333)) (=> (not @t248) (= @t338 (_ @t83 (_ tptp.butlast_list_node @t53))))))) % 0.48/0.93 (assume @p140 (forall @t252 (and (=> @t249 (= @t340 @t324)) (=> (not @t249) (= @t340 (_ @t89 @t339)))))) % 0.48/0.93 (assume @p141 (forall @t253 (and (=> @t250 (= @t342 @t327)) (=> @t343 (= @t342 (_ @t95 @t341)))))) % 0.48/0.93 (assume @p142 (forall (@list @t62 @t57 @t60) (=> (or @t325 (_ @t63 (_ tptp.set_val2 @t339))) (_ @t63 (_ tptp.set_val2 @t340))))) % 0.48/0.93 (assume @p143 (forall @t344 (=> (or @t329 (_ @t72 (_ tptp.set_node2 @t341))) (_ @t72 (_ tptp.set_node2 @t342))))) % 0.48/0.93 (assume @p144 (forall @t348 (= @t347 (exists (@list @t345) (= @t346 (_ @t304 (_ @t89 (_ (_ tptp.cons_val @t345) tptp.nil_val)))))))) % 0.48/0.93 (assume @p145 (forall @t352 (= @t351 (exists (@list @t349) (= @t350 (_ @t307 (_ @t83 (_ (_ tptp.cons_list_node @t349) tptp.nil_list_node)))))))) % 0.48/0.93 (assume @p146 (forall @t356 (= @t355 (exists (@list @t353) (= @t354 (_ @t313 (_ @t95 (_ (_ tptp.cons_node @t353) tptp.nil_node)))))))) % 0.48/0.93 (assume @p147 (forall @t348 (=> @t347 (not (forall (@list @t357) (not (= @t346 (_ @t304 (_ @t89 (_ (_ tptp.cons_val @t357) tptp.nil_val)))))))))) % 0.48/0.93 (assume @p148 (forall @t352 (=> @t351 (not (forall (@list @t358) (not (= @t350 (_ @t307 (_ @t83 (_ (_ tptp.cons_list_node @t358) tptp.nil_list_node)))))))))) % 0.48/0.93 (assume @p149 (forall @t356 (=> @t355 (not (forall (@list @t359) (not (= @t354 (_ @t313 (_ @t95 (_ (_ tptp.cons_node @t359) tptp.nil_node)))))))))) % 0.48/0.93 (assume @p150 (forall (@list @t363 @t361 @t362 @t360) (=> (= (_ (_ tptp.cons_val @t363) @t361) (_ (_ tptp.cons_val @t362) @t360)) (and (= @t363 @t362) (= @t361 @t360))))) % 0.48/0.93 (assume @p151 (forall (@list @t367 @t365 @t366 @t364) (=> (= (_ (_ tptp.cons_list_node @t367) @t365) (_ (_ tptp.cons_list_node @t366) @t364)) (and (= @t367 @t366) (= @t365 @t364))))) % 0.48/0.93 (assume @p152 (forall (@list @t371 @t369 @t370 @t368) (=> (= (_ (_ tptp.cons_node @t371) @t369) (_ (_ tptp.cons_node @t370) @t368)) (and (= @t371 @t370) (= @t369 @t368))))) % 0.48/0.93 (assume @p153 (forall @t326 (not (= @t331 @t57)))) % 0.48/0.93 (assume @p154 (forall (@list @t55 @t50) (not (= @t334 @t50)))) % 0.48/0.93 (assume @p155 (forall @t330 (not (= @t336 @t66)))) % 0.48/0.93 (assume @p156 (forall (@list @t57 @t373 @t226 @t60 @t372) (=> (= (_ @t89 @t373) @t226) (=> (= @t60 (_ (_ tptp.append_val @t373) @t372)) (= @t90 (_ @t232 @t372)))))) % 0.48/0.93 (assume @p157 (forall (@list @t66 @t375 @t228 @t69 @t374) (=> (= (_ @t95 @t375) @t228) (=> (= @t69 (_ @t376 @t374)) (= @t96 (_ @t234 @t374)))))) % 0.48/0.93 (assume @p158 (forall (@list @t57 @t60 @t226 @t377) (= (= @t90 (_ @t232 @t377)) (exists (@list @t378) (or (and (= @t57 (_ @t232 @t378)) (= (_ @t379 @t60) @t377)) (and (= (_ @t89 @t378) @t226) (= @t60 (_ @t379 @t377)))))))) % 0.48/0.93 (assume @p159 (forall (@list @t66 @t69 @t228 @t380) (= (= @t96 (_ @t234 @t380)) (exists (@list @t381) (or (and (= @t66 (_ @t234 @t381)) (= (_ @t382 @t69) @t380)) (and (= (_ @t95 @t381) @t228) (= @t69 (_ @t382 @t380)))))))) % 0.48/0.93 (assume @p160 (forall (@list @t384 @t383) (=> (_ @t384 tptp.nil_val) (=> (forall (@list @t225 @t385) (=> (_ @t384 @t385) (_ @t384 (_ @t386 @t385)))) (_ @t384 @t383))))) % 0.48/0.93 (assume @p161 (forall @t394 (=> @t393 (=> (forall (@list @t221 @t390) (=> (_ @t388 @t390) (_ @t388 @t392))) @t389)))) % 0.48/0.93 (assume @p162 (forall (@list @t395 @t402 @t66 @t60) (=> (forall @t408 (_ @t405 tptp.nil_val)) (=> (forall @t407 (_ (_ @t395 tptp.nil_node) @t406)) (=> (forall @t404 (=> @t403 (=> (_ @t405 @t397) @t401))) (=> (forall @t404 (=> (not @t403) (=> (_ @t400 @t385) @t401))) (_ (_ @t395 @t66) @t60))))))) % 0.48/0.93 (assume @p163 (forall (@list @t409 @t414 @t57 @t60) (=> (forall @t418 (_ @t417 tptp.nil_val)) (=> (forall @t407 (_ (_ @t409 tptp.nil_val) @t406)) (=> (forall @t416 (=> @t415 (=> (_ @t417 @t397) @t413))) (=> (forall @t416 (=> (not @t415) (=> (_ @t412 @t385) @t413))) (_ (_ @t409 @t57) @t60))))))) % 0.48/0.93 (assume @p164 (forall (@list @t419 @t425 @t50 @t60) (=> (forall @t429 (_ @t428 tptp.nil_val)) (=> (forall @t407 (_ (_ @t419 tptp.nil_list_node) @t406)) (=> (forall @t427 (=> @t426 (=> (_ @t428 @t397) @t424))) (=> (forall @t427 (=> (not @t426) (=> (_ @t423 @t385) @t424))) (_ (_ @t419 @t50) @t60))))))) % 0.48/0.93 (assume @p165 (forall (@list @t430 @t436 @t66 @t53) (=> (forall @t408 (_ @t439 tptp.nil_list_node)) (=> (forall @t441 (_ (_ @t430 tptp.nil_node) @t440)) (=> (forall @t438 (=> @t437 (=> (_ @t439 @t433) @t435))) (=> (forall @t438 (=> (not @t437) (=> (_ @t434 @t431) @t435))) (_ (_ @t430 @t66) @t53))))))) % 0.48/0.93 (assume @p166 (forall (@list @t442 @t445 @t57 @t53) (=> (forall @t418 (_ @t448 tptp.nil_list_node)) (=> (forall @t441 (_ (_ @t442 tptp.nil_val) @t440)) (=> (forall @t447 (=> @t446 (=> (_ @t448 @t433) @t444))) (=> (forall @t447 (=> (not @t446) (=> (_ @t443 @t431) @t444))) (_ (_ @t442 @t57) @t53))))))) % 0.48/0.93 (assume @p167 (forall (@list @t449 @t452 @t50 @t53) (=> (forall @t429 (_ @t455 tptp.nil_list_node)) (=> (forall @t441 (_ (_ @t449 tptp.nil_list_node) @t440)) (=> (forall @t454 (=> @t453 (=> (_ @t455 @t433) @t451))) (=> (forall @t454 (=> (not @t453) (=> (_ @t450 @t431) @t451))) (_ (_ @t449 @t50) @t53))))))) % 0.48/0.93 (assume @p168 (forall (@list @t456 @t465 @t66 @t69) (=> @t473 (=> @t472 (=> (forall @t467 (=> @t466 (=> @t469 @t462))) (=> (forall @t467 (=> (not @t466) @t464)) @t457)))))) % 0.48/0.93 (assume @p169 (forall @t487 (=> (forall (@list @t482 @t221 @t398 @t458 @t390) (=> (=> @t486 (_ @t484 @t460)) (=> (=> (not @t486) (_ @t485 @t390)) (_ @t485 @t460)))) (=> (forall (@list @t482 @t398) (_ @t484 tptp.nil_node)) (=> (forall (@list @t482 @t480 @t479) (_ (_ @t483 tptp.nil_node) @t481)) @t478))))) % 0.48/0.93 (assume @p170 (forall (@list @t489 @t488 @t475 @t474) (=> (forall (@list @t495 @t470) (_ (_ @t496 tptp.nil_node) @t470)) (=> (forall (@list @t495 @t492 @t491 @t490) (=> (_ (_ @t496 @t491) (_ (_ tptp.cons_node (_ @t495 @t492)) @t490)) (_ (_ @t496 @t494) @t490))) (_ (_ (_ @t489 @t488) @t475) @t474))))) % 0.48/0.93 (assume @p171 (forall @t504 (=> @t98 (=> @t503 (=> (forall @t501 (=> @t500 (=> @t499 @t498))) @t497))))) % 0.48/0.93 (assume @p172 (forall @t487 (=> (forall @t510 (_ @t507 tptp.nil_node)) (=> (forall (@list @t505 @t492 @t491 @t509 @t490) (=> (_ (_ @t506 @t491) @t490) (_ (_ @t506 @t494) (_ (_ tptp.cons_node @t509) @t490)))) (=> (forall @t508 (_ (_ @t506 @t481) tptp.nil_node)) (=> (forall @t508 (_ @t507 @t481)) @t478)))))) % 0.48/0.93 (assume @p173 (forall @t517 (=> @t516 (=> (forall (@list @t505 @t221) (_ @t515 @t502)) (=> (forall (@list @t505 @t221 @t458 @t398) (=> (_ @t515 @t513) (_ @t515 @t514))) @t512))))) % 0.48/0.93 (assume @p174 (forall @t521 (=> @t393 (=> @t503 (=> (forall (@list @t519 @t518 @t398) (=> @t499 (_ @t388 (_ @t520 (_ (_ tptp.cons_node @t518) @t398))))) @t497))))) % 0.48/0.93 (assume @p175 (forall @t394 (=> @t393 (=> @t503 (=> (forall @t524 (=> (=> @t522 @t498) (=> (=> @t523 (_ @t388 @t513)) (_ @t388 @t514)))) @t389))))) % 0.48/0.93 (assume @p176 (forall @t517 (=> @t516 (=> (forall (@list @t505 @t221 @t390) (=> (_ @t515 @t390) (_ @t515 @t392))) @t512)))) % 0.48/0.93 (assume @p177 (forall @t526 (=> (not @t525) (=> (forall @t223 (not (= @t55 @t502))) (not (forall @t524 (not (= @t55 @t514)))))))) % 0.48/0.93 (assume @p178 (forall (@list @t456 @t528 @t527) (=> @t536 (=> (forall (@list @t530 @t535 @t534) (=> (_ (_ @t456 @t535) @t534) (_ (_ @t456 (_ @t531 @t535)) @t534))) (=> (forall (@list @t530 @t532 @t529) (=> (_ @t533 @t529) (_ @t533 (_ @t531 @t529)))) (_ (_ @t456 @t528) @t527)))))) % 0.48/0.93 (assume @p179 (forall (@list @t538) (=> (not (= @t538 tptp.nil_list_node)) (=> (forall (@list @t537) (not (= @t538 (_ (_ tptp.cons_list_node tptp.nil_node) @t537)))) (not (forall (@list @t221 @t398 @t537) (not (= @t538 (_ (_ tptp.cons_list_node @t399) @t537))))))))) % 0.48/0.93 (assume @p180 (forall @t540 (=> @t472 (=> @t473 (=> (forall @t467 (=> @t469 @t464)) @t539))))) % 0.48/0.93 (assume @p181 (forall @t394 (=> (forall @t501 (=> (forall (@list @t542 @t541) (=> (= @t398 (_ (_ tptp.cons_node @t542) @t541)) @t499)) @t498)) (=> @t393 @t389)))) % 0.48/0.93 (assume @p182 (forall @t526 (=> (forall @t501 (not (= @t55 @t399))) @t525))) % 0.48/0.93 (assume @p183 (forall @t521 (=> @t393 (=> @t503 (=> (forall (@list @t221 @t458 @t543) (=> (_ @t388 @t543) (=> (_ @t388 @t544) (_ @t388 (_ @t391 @t544))))) @t497))))) % 0.48/0.93 (assume @p184 (forall @t540 (=> @t472 (=> (forall (@list @t221 @t398 @t390) (=> (_ (_ @t456 @t390) @t398) @t463)) @t539)))) % 0.48/0.93 (assume @p185 (forall @t547 (=> @t536 (=> (forall @t501 (_ @t461 tptp.nil_node)) (=> (forall @t546 (_ @t471 @t460)) (=> (forall @t467 (=> @t545 @t462)) @t457)))))) % 0.48/0.93 (assume @p186 (forall @t247 (= @t98 (exists (@list @t549 @t548) (= @t66 (_ (_ tptp.cons_node @t549) @t548)))))) % 0.48/0.93 (assume @p187 (forall (@list @t388 @t550) (=> @t393 (=> (forall (@list @t519 @t551) (=> (_ @t388 @t551) (_ @t388 (_ @t520 @t551)))) (_ @t388 @t550))))) % 0.48/0.93 (assume @p188 (forall (@list @t51) (=> (not (= @t51 tptp.nil_node)) (not (forall (@list @t553 @t552) (not (= @t51 (_ (_ tptp.cons_node @t553) @t552)))))))) % 0.48/0.93 (assume @p189 (forall @t540 (=> @t472 (=> (forall (@list @t492 @t491 @t554) (=> (_ (_ @t456 @t491) (_ @t493 @t554)) (_ (_ @t456 @t494) @t554))) @t539)))) % 0.48/0.93 (assume @p190 (forall (@list @t550 @t196 @t194) (=> (= @t550 @t197) @t556))) % 0.48/0.93 (assume @p191 (forall @t558 (=> @t557 (not (forall @t501 (not (= @t354 @t399))))))) % 0.48/0.93 (assume @p192 (forall @t559 (not (= tptp.nil_node @t197)))) % 0.48/0.93 (assume @p193 (forall (@list @t102 @t200) (=> (_ @t561 @t563) (=> (forall (@list @t560) (not (= @t200 (_ @t107 @t560)))) (not (forall (@list @t562 @t560) (=> (= @t200 (_ (_ tptp.cons_val @t562) @t560)) (not (_ @t561 (_ tptp.set_val2 @t560)))))))))) % 0.48/0.93 (assume @p194 (forall (@list @t123 @t138) (=> (_ @t565 @t567) (=> (forall (@list @t564) (not (= @t138 (_ @t128 @t564)))) (not (forall (@list @t566 @t564) (=> (= @t138 (_ (_ tptp.cons_node @t566) @t564)) (not (_ @t565 (_ tptp.set_node2 @t564)))))))))) % 0.48/0.93 (assume @p195 (forall (@list @t58 @t62 @t57) (=> (_ @t568 (_ tptp.set_val2 @t331)) (or (= @t58 @t62) (_ @t568 @t64))))) % 0.48/0.93 (assume @p196 (forall (@list @t67 @t71 @t66) (=> (_ @t569 @t570) (or (= @t67 @t71) (_ @t569 @t73))))) % 0.48/0.93 (assume @p197 (forall (@list @t187 @t185) (_ (_ tptp.member_val @t187) @t571))) % 0.48/0.93 (assume @p198 (forall @t559 (_ (_ tptp.member_node @t196) @t572))) % 0.48/0.93 (assume @p199 (forall (@list @t58 @t185 @t187) (=> (_ @t568 (_ tptp.set_val2 @t185)) (_ @t568 @t571)))) % 0.48/0.93 (assume @p200 (forall (@list @t67 @t194 @t196) (=> (_ @t569 (_ tptp.set_node2 @t194)) (_ @t569 @t572)))) % 0.48/0.93 (assume @p201 (forall (@list @t71 @t375 @t69 @t66 @t228) (=> (= (_ @t313 @t375) @t69) (=> (= @t66 (_ @t376 @t228)) @t573)))) % 0.48/0.93 (assume @p202 (forall @t344 (= (_ (_ tptp.append_node @t336) @t69) (_ @t313 @t96)))) % 0.48/0.93 (assume @p203 (forall (@list @t582 @t580 @t579 @t584 @t575 @t574) (=> (= (_ @t583 @t585) (_ @t587 @t577)) (=> (forall (@list @t586) (=> (= @t582 (_ @t587 (_ @t576 @t586))) (not (= @t574 (_ (_ tptp.append_node @t586) @t585))))) (=> (=> (= @t584 @t582) (=> (= @t575 @t580) (not (= @t574 @t579)))) (not (forall (@list @t578) (=> (= @t584 (_ @t583 (_ @t581 @t578))) (not (= @t579 (_ (_ tptp.append_node @t578) @t577))))))))))) % 0.48/0.93 (assume @p204 (forall @t99 (=> @t310 (= @t66 @t588)))) % 0.48/0.93 (assume @p205 (forall (@list @t69) (= @t588 @t69))) % 0.48/0.93 (assume @p206 (forall @t263 (= (_ @t260 @t138) @t138))) % 0.48/0.93 (assume @p207 (forall @t559 (= (_ tptp.tl_node @t197) @t194))) % 0.48/0.93 (assume @p208 (= (_ tptp.tl_node tptp.nil_node) tptp.nil_node)) % 0.48/0.93 (assume @p209 (forall @t593 (=> @t592 @t591))) % 0.48/0.93 (assume @p210 (forall @t594 (=> @t573 @t591))) % 0.48/0.93 (assume @p211 (forall (@list @t66 @t69 @t456) (=> @t98 (=> @t343 (=> (forall (@list @t221 @t458) (_ @t602 @t595)) (=> (forall (@list @t221 @t398 @t458) (=> @t500 (_ @t599 @t595))) (=> (forall (@list @t221 @t458 @t390) (=> @t601 (_ @t602 @t597))) (=> (forall @t467 (=> @t545 (=> @t500 (=> @t601 @t600)))) @t457)))))))) % 0.48/0.93 (assume @p212 (forall @t504 (=> @t98 (=> @t503 (=> (forall @t501 (=> @t500 @t603)) @t497))))) % 0.48/0.93 (assume @p213 (forall @t593 (= @t592 (or (and @t250 @t590) (exists @t607 (and (= @t69 @t606) (= @t605 @t66))))))) % 0.48/0.93 (assume @p214 (forall @t594 (= @t573 (or (and @t250 (= @t336 @t228)) (exists @t607 (and (= @t606 @t69) (= @t66 @t605))))))) % 0.48/0.93 (assume @p215 (forall @t558 (= @t557 (exists (@list @t610 @t216) (= @t354 (_ (_ tptp.append_node @t610) @t609)))))) % 0.48/0.93 (assume @p216 (forall @t547 (=> @t536 (=> @t612 (=> (forall @t546 (_ @t471 @t597)) (=> (forall @t467 @t611) @t457)))))) % 0.48/0.93 (assume @p217 (forall @t558 (=> @t557 (not (forall (@list @t614 @t530) (not (= @t354 (_ (_ tptp.append_node @t614) @t613)))))))) % 0.48/0.93 (assume @p218 (forall @t247 (=> @t98 (not (forall (@list @t390 @t458) (not (= @t66 @t597))))))) % 0.48/0.93 (assume @p219 (forall @t521 (=> @t393 (=> (forall @t501 @t603) @t497)))) % 0.48/0.93 (assume @p220 (forall @t626 (= @t625 (exists (@list @t548 @t216) (and (exists @t623 @t622) @t619 (forall @t618 (=> (_ @t617 @t616) @t615))))))) % 0.48/0.93 (assume @p221 (forall @t626 (= @t625 (exists (@list @t548 @t216 @t620) (and @t622 @t619 (forall @t618 (=> (_ @t617 @t627) @t615))))))) % 0.48/0.93 (assume @p222 (forall @t326 (= @t65 (exists @t631 (and @t630 (not (_ @t63 (_ tptp.set_val2 @t628)))))))) % 0.48/0.93 (assume @p223 (forall @t330 (= @t74 (exists @t633 (and @t632 (not (_ @t72 @t616))))))) % 0.48/0.93 (assume @p224 (forall @t326 (= @t65 (exists @t631 (and @t630 (not (_ @t63 (_ tptp.set_val2 @t629)))))))) % 0.48/0.93 (assume @p225 (forall @t330 (= @t74 (exists @t633 (and @t632 (not (_ @t72 @t627))))))) % 0.48/0.93 (assume @p226 (forall @t626 (=> @t644 (not (forall @t643 (=> @t642 (=> @t222 (not @t639)))))))) % 0.48/0.93 (assume @p227 (forall @t626 (=> @t644 (not (forall @t647 (=> @t640 (=> @t222 (not @t646)))))))) % 0.48/0.93 (assume @p228 (forall @t626 (=> @t644 (exists @t643 (and @t642 @t222 @t639))))) % 0.48/0.93 (assume @p229 (forall @t626 (=> @t644 (exists @t647 (and @t640 @t222 @t646))))) % 0.48/0.93 (assume @p230 (forall (@list @t102 @t346) (=> (_ @t561 @t652) (not (forall @t651 (not (= @t346 (_ @t650 (_ @t107 @t648))))))))) % 0.48/0.93 (assume @p231 (forall (@list @t123 @t354) (=> (_ @t565 @t657) (not (forall @t656 (not (= @t354 (_ @t655 (_ @t128 @t653))))))))) % 0.48/0.93 (assume @p232 (forall @t326 (= @t65 (exists @t631 @t630)))) % 0.48/0.93 (assume @p233 (forall @t330 (= @t74 (exists @t633 @t632)))) % 0.48/0.93 (assume @p234 (forall (@list @t62 @t57 @t60 @t659 @t658) (=> (not @t65) (=> (not (_ @t63 (_ tptp.set_val2 @t60))) (= (= (_ @t89 (_ @t304 @t60)) (_ (_ tptp.append_val @t659) (_ @t304 @t658))) (and (= @t57 @t659) (= @t60 @t658))))))) % 0.48/0.93 (assume @p235 (forall (@list @t71 @t66 @t69 @t661 @t660) (=> (not @t74) (=> (not (_ @t72 @t662)) (= (= (_ @t95 (_ @t313 @t69)) (_ (_ tptp.append_node @t661) (_ @t313 @t660))) (and (= @t66 @t661) (= @t69 @t660))))))) % 0.48/0.93 (assume @p236 (forall @t626 (=> @t644 (not (forall @t643 (=> @t642 (not @t222))))))) % 0.48/0.93 (assume @p237 (forall @t326 (=> @t65 (exists @t665 (and @t664 (not (_ @t63 (_ tptp.set_val2 @t385)))))))) % 0.48/0.93 (assume @p238 (forall @t330 (=> @t74 (exists @t667 (and @t666 (not (_ @t72 @t636))))))) % 0.48/0.93 (assume @p239 (forall (@list @t62 @t346 @t58) (=> @t672 (=> (_ @t568 @t652) (=> (=> @t303 (forall @t651 (not (= @t346 (_ @t650 (_ @t59 @t648)))))) (=> (=> @t671 (forall @t670 (not (= @t346 (_ @t650 (_ @t304 (_ @t669 (_ @t59 @t668)))))))) (not (=> @t671 (forall @t670 (not (= @t346 (_ @t650 (_ @t59 (_ @t669 (_ @t304 @t668))))))))))))))) % 0.48/0.93 (assume @p240 (forall (@list @t71 @t354 @t67) (=> @t677 (=> (_ @t569 @t657) (=> (=> @t309 (forall @t656 (not (= @t354 (_ @t655 (_ @t68 @t653)))))) (=> (=> @t676 (forall @t675 (not (= @t354 (_ @t655 (_ @t313 (_ @t674 (_ @t68 @t673)))))))) (not (=> @t676 (forall @t675 (not (= @t354 (_ @t655 (_ @t68 (_ @t674 (_ @t313 @t673))))))))))))))) % 0.48/0.93 (assume @p241 (forall @t626 (=> @t644 (exists @t643 (and @t642 @t222))))) % 0.48/0.93 (assume @p242 (forall @t326 (=> @t65 (exists @t665 (and @t664 (not (_ @t63 (_ tptp.set_val2 @t663)))))))) % 0.48/0.93 (assume @p243 (forall @t330 (=> @t74 (exists @t667 (and @t666 (not (_ @t72 @t645))))))) % 0.48/0.93 (assume @p244 (forall @t326 (=> @t65 (exists @t665 @t664)))) % 0.48/0.93 (assume @p245 (forall @t330 (=> @t74 (exists @t667 @t666)))) % 0.48/0.93 (assume @p246 (forall @t247 (=> @t98 (=> @t678 (not (forall (@list @t530) (not (= @t66 @t613)))))))) % 0.48/0.93 (assume @p247 (forall @t247 (= @t678 @t679))) % 0.48/0.93 (assume @p248 (forall @t247 (= (= tptp.nil_node @t94) @t679))) % 0.48/0.93 (assume @p249 (forall (@list @t200 @t62) (=> @t680 (=> (_ @t63 (_ tptp.set_val2 (_ tptp.tl_val @t200))) (_ @t63 @t563))))) % 0.48/0.93 (assume @p250 (forall (@list @t138 @t71) (=> @t682 (=> (_ @t72 (_ tptp.set_node2 (_ tptp.tl_node @t138))) (_ @t72 @t567))))) % 0.48/0.93 (assume @p251 (forall @t685 (= (_ @t683 @t312) (or (= @t66 @t312) @t684)))) % 0.48/0.93 (assume @p252 (forall @t273 (=> @t28 (=> @t272 (not (forall (@list @t265 @t687 @t264) (=> (= @t17 (_ @t299 (_ (_ tptp.append_node @t687) @t264))) (=> (_ (_ tptp.prefix_node @t688) @t17) (=> (_ (_ tptp.suffix_node @t686) @t17) (=> (_ (_ @t22 @t688) @t71) (=> (not (_ @t72 (_ tptp.set_node2 @t265))) (=> (_ (_ @t267 @t687) @t71) (=> (_ (_ @t267 @t686) @t24) (_ @t72 (_ tptp.set_node2 @t264))))))))))))))) % 0.48/0.93 (assume @p253 (forall @t99 (= (_ @t689 @t66) @t250))) % 0.48/0.93 (assume @p254 (forall (@list @t4 @t20 @t17 @t35) (=> (_ @t27 @t20) (=> (_ @t243 @t47) (not (forall @t281 (=> (_ @t280 @t20) (=> (_ @t243 @t690) (=> (not (_ @t45 (_ tptp.set_node2 (_ tptp.tl_node @t275)))) (not (_ (_ tptp.ord_less_eq_set_node @t690) @t47))))))))))) % 0.48/0.93 (assume @p255 (forall @t42 (=> @t28 (=> (=> (= @t17 @t80) (not (= @t24 @t20))) (not (=> (_ (_ (_ @t21 @t692) @t691) @t24) (not (_ @t45 (_ tptp.set_node2 (_ @t240 @t692)))))))))) % 0.48/0.93 (assume @p256 (forall (@list @t4 @t17 @t20 @t24) (=> (_ @t693 (_ @t18 @t80)) (=> (_ @t45 (_ tptp.set_node2 (_ @t240 @t24))) (_ @t693 (_ @t18 (_ @t79 @t297))))))) % 0.48/0.93 (assume @p257 (forall @t81 (=> @t46 (_ tptp.finite_finite_val (_ (_ @t43 @t4) @t20))))) % 0.48/0.93 (assume @p258 (forall @t287 (=> @t28 (=> @t286 (not (forall (@list @t292 @t274) (=> (_ (_ (_ @t21 @t292) @t274) @t24) (=> (_ @t208 @t292) (=> (forall @t183 (=> (_ @t181 (_ tptp.set_node2 (_ tptp.tl_node @t274))) @t284)) (not (_ (_ tptp.suffix_node @t274) @t17))))))))))) % 0.48/0.93 (assume @p259 (forall @t245 (_ tptp.finite_finite_val (_ (_ tptp.defs @t4) @t20)))) % 0.48/0.93 (assume @p260 (forall @t526 (_ @t694 @t55))) % 0.48/0.93 (assume @p261 (forall @t263 (_ @t695 @t138))) % 0.48/0.93 (assume @p262 (forall @t526 (_ @t696 @t55))) % 0.48/0.93 (assume @p263 (forall @t263 (_ @t697 @t138))) % 0.48/0.93 (assume @p264 (forall @t699 (=> @t698 @t41))) % 0.48/0.93 (assume @p265 (forall @t42 (=> @t28 (= @t20 @t700)))) % 0.48/0.93 (assume @p266 (forall @t42 (=> @t28 (_ (_ (_ @t21 @t700) @t17) @t24)))) % 0.48/0.93 (assume @p267 (forall (@list @t4 @t20 @t17) (=> (_ @t693 (_ @t79 @t17)) @t701))) % 0.48/0.93 (assume @p268 (forall @t704 (=> @t703 (_ @t693 @t702)))) % 0.48/0.93 (assume @p269 (forall @t247 (_ tptp.finite_finite_node @t73))) % 0.48/0.93 (assume @p270 (forall @t246 (_ tptp.finite_finite_val @t64))) % 0.48/0.93 (assume @p271 (forall @t706 (= (_ (_ tptp.prefix_node @t336) @t705) (and @t309 @t684)))) % 0.48/0.93 (assume @p272 (forall @t247 (_ (_ tptp.prefix_node tptp.nil_node) @t66))) % 0.48/0.93 (assume @p273 (forall @t247 (= (_ @t683 tptp.nil_node) @t97))) % 0.48/0.93 (assume @p274 (forall @t263 (= (_ @t695 tptp.nil_node) @t681))) % 0.48/0.93 (assume @p275 (forall @t263 (= @t707 @t681))) % 0.48/0.93 (assume @p276 (forall @t247 (= (_ @t708 tptp.nil_node) @t97))) % 0.48/0.93 (assume @p277 (forall @t230 (= (_ @t689 @t238) (_ (_ tptp.prefix_node @t69) @t228)))) % 0.48/0.93 (assume @p278 (forall @t237 (= (_ @t709 @t235) (_ (_ tptp.suffix_node @t69) @t228)))) % 0.48/0.93 (assume @p279 (forall @t81 (=> @t46 (=> @t5 @t701)))) % 0.48/0.93 (assume @p280 (forall @t704 (=> @t703 (_ @t693 (_ @t18 @t297))))) % 0.48/0.93 (assume @p281 (forall (@list @t4 @t17 @t35) (=> @t698 (=> (_ @t243 (_ tptp.set_node2 (_ @t240 @t700))) @t710)))) % 0.48/0.93 (assume @p282 (forall @t715 (= @t714 (or (exists (@list @t713) (and (= @t138 (_ (_ tptp.cons_node @t713) tptp.nil_node)) (_ (_ tptp.member_node @t713) @t44) @t5)) (exists (@list @t711 @t712) (and (= @t138 (_ (_ tptp.cons_node @t712) @t711)) (_ @t693 @t711) (_ (_ tptp.member_node @t712) (_ tptp.set_node2 (_ @t240 (_ tptp.hd_node @t711)))))))))) % 0.48/0.93 (assume @p283 (forall (@list @t4 @t55 @t388) (=> (_ @t693 @t55) (=> (forall @t721 (=> @t720 (=> @t5 (_ @t388 @t719)))) (=> (forall @t718 (=> @t717 (=> (_ @t388 @t291) (=> @t716 (_ @t388 @t293))))) (_ @t388 @t55)))))) % 0.48/0.93 (assume @p284 (forall @t715 (=> @t714 (=> (forall @t721 (=> (= @t138 @t719) (=> @t720 (not @t5)))) (not (forall @t718 (=> (= @t138 @t293) (=> @t717 (not @t716))))))))) % 0.48/0.93 (assume @p285 (forall @t253 (= (_ @t709 @t66) @t250))) % 0.48/0.93 (assume @p286 (forall @t99 @t724)) % 0.48/0.93 (assume @p287 (forall @t685 (= (_ @t708 @t312) (or @t97 (exists @t623 (and (= @t66 (_ @t725 @t311)) (_ (_ tptp.suffix_node @t620) @t69))))))) % 0.48/0.93 (assume @p288 (forall @t316 (= (_ (_ tptp.suffix_node @t315) @t312) (and @t309 @t726)))) % 0.48/0.93 (assume @p289 (forall @t247 (=> @t98 (= (_ (_ tptp.cons_node @t722) @t94) @t66)))) % 0.48/0.93 (assume @p290 (forall @t730 (=> @t556 (= @t729 @t550)))) % 0.48/0.93 (assume @p291 (forall (@list @t346 @t62) (=> (not (= @t346 tptp.nil_val)) (= (or (= @t62 (_ tptp.hd_val @t346)) (_ @t63 (_ tptp.set_val2 (_ tptp.tl_val @t346)))) @t672)))) % 0.48/0.93 (assume @p292 (forall (@list @t354 @t71) (=> @t557 (= (or (= @t71 (_ tptp.hd_node @t354)) (_ @t72 (_ tptp.set_node2 (_ tptp.tl_node @t354)))) @t677)))) % 0.48/0.93 (assume @p293 (forall @t699 (=> @t698 @t5))) % 0.48/0.93 (assume @p294 (forall (@list @t4 @t17 @t20) (=> @t698 (=> @t48 @t46)))) % 0.48/0.93 (assume @p295 (forall (@list @t4 @t20 @t35 @t17 @t15) (=> (_ @t693 (_ @t79 @t323)) (=> (=> @t710 (_ @t693 @t731)) (_ @t693 (_ @t79 @t731)))))) % 0.48/0.93 (assume @p296 (forall @t99 (=> @t726 @t733))) % 0.48/0.93 (assume @p297 (forall (@list @t734 @t208) (= (_ (_ tptp.ord_less_eq_set_node @t734) @t209) (forall @t218 (=> (_ @t217 @t734) @t619))))) % 0.48/0.93 (assume @p298 (forall (@list @t736 @t738 @t737 @t735) (=> (= @t736 @t738) (=> (_ (_ tptp.ord_less_eq_set_node @t738) @t737) (=> (= @t737 @t735) (_ (_ tptp.ord_less_eq_set_node @t736) @t735)))))) % 0.48/0.93 (assume @p299 (forall @t706 (=> (_ @t739 @t705) @t726))) % 0.48/0.93 (assume @p300 (forall @t685 (=> @t726 @t740))) % 0.48/0.93 (assume @p301 (forall @t344 (=> (_ @t739 @t69) @t726))) % 0.48/0.93 (assume @p302 (forall (@list @t66 @t67 @t69) (= @t740 (or (= @t66 @t705) @t726)))) % 0.48/0.93 (assume @p303 (forall @t263 (=> @t707 @t681))) % 0.48/0.93 (assume @p304 (forall @t263 (_ @t741 @t138))) % 0.48/0.93 (assume @p305 (forall @t247 (_ @t741 @t66))) % 0.48/0.93 (assume @p306 (forall @t99 (=> @t726 (not (forall @t641 (not (= @t69 (_ (_ tptp.append_node @t543) @t66)))))))) % 0.48/0.93 (assume @p307 (forall (@list @t69 @t228 @t66) (=> (= @t69 @t235) @t726))) % 0.48/0.93 (assume @p308 (forall @t230 (= (_ @t708 @t229) (or (_ @t708 @t228) (exists (@list @t742) (and (= @t66 (_ (_ tptp.append_node @t742) @t228)) (_ (_ tptp.suffix_node @t742) @t69))))))) % 0.48/0.93 (assume @p309 (forall (@list @t228 @t66 @t69) (=> (_ (_ tptp.suffix_node @t235) @t69) @t726))) % 0.48/0.93 (assume @p310 (forall @t230 (=> @t726 (_ @t708 (_ @t234 @t69))))) % 0.48/0.93 (assume @p311 (forall @t247 (_ (_ tptp.suffix_node @t94) @t66))) % 0.48/0.93 (assume @p312 (forall @t747 (=> (_ @t746 @t69) (=> (_ @t745 @t69) (or (_ @t746 @t744) (_ @t745 @t743)))))) % 0.48/0.93 (assume @p313 (= @t752 (lambda @t749 (and (_ (_ tptp.suffix_node @t259) @t748) (_ (_ tptp.suffix_node @t748) @t259))))) % 0.48/0.93 (assume @p314 (forall @t756 (=> @t755 (=> @t754 @t306)))) % 0.48/0.93 (assume @p315 (forall @t756 (=> @t306 @t755))) % 0.48/0.93 (assume @p316 (forall @t205 (=> @t760 @t759))) % 0.48/0.93 (assume @p317 (forall (@list @t55 @t51 @t761) (=> @t755 (=> (_ @t753 @t761) (_ @t696 @t761))))) % 0.48/0.93 (assume @p318 (forall (@list @t51 @t55) (=> @t754 (= @t755 @t306)))) % 0.48/0.93 (assume @p319 (= @t752 (lambda @t766 (and @t765 @t764)))) % 0.48/0.93 (assume @p320 (forall (@list @t138 @t203) (=> @t760 (=> @t768 @t767)))) % 0.48/0.93 (assume @p321 (forall @t205 (=> @t767 @t759))) % 0.48/0.93 (assume @p322 (forall @t205 (=> @t760 (=> (= @t203 @t202) @t757)))) % 0.48/0.93 (assume @p323 (forall (@list @t203 @t138 @t202) (=> @t768 (=> (_ @t769 @t203) (_ @t769 @t138))))) % 0.48/0.93 (assume @p324 (= @t752 (lambda @t766 (and @t764 @t765)))) % 0.48/0.93 (assume @p325 (forall (@list @t203 @t138) (=> @t768 (=> @t760 @t767)))) % 0.48/0.93 (assume @p326 (forall @t559 (= (_ tptp.hd_node @t197) @t196))) % 0.48/0.93 (assume @p327 (forall @t219 (=> (_ tptp.finite_finite_node @t215) (exists @t408 (= (_ tptp.set_node2 @t398) @t215))))) % 0.48/0.93 (assume @p328 (forall @t214 (=> (_ tptp.finite_finite_val @t210) (exists @t418 (= (_ tptp.set_val2 @t410) @t210))))) % 0.48/0.93 (assume @p329 (forall (@list @t57 @t770) (= (_ (_ tptp.ord_less_eq_set_val @t64) @t770) (forall @t213 (=> (_ @t212 @t64) (_ @t212 @t770)))))) % 0.48/0.93 (assume @p330 (forall (@list @t66 @t771) (= (_ @t732 @t771) (forall @t218 (=> @t624 (_ @t217 @t771)))))) % 0.48/0.93 (assume @p331 (forall @t99 (=> @t684 @t733))) % 0.48/0.93 (assume @p332 (forall @t262 (=> @t680 (_ (_ tptp.member_val (_ tptp.hd_val @t200)) @t563)))) % 0.48/0.93 (assume @p333 (forall @t263 (=> @t682 (_ (_ tptp.member_node (_ tptp.hd_node @t138)) @t567)))) % 0.48/0.93 (assume @p334 (forall @t246 (=> @t92 (_ (_ tptp.member_val @t772) @t64)))) % 0.48/0.93 (assume @p335 (forall @t247 (=> @t98 (_ (_ tptp.member_node @t722) @t73)))) % 0.48/0.93 (assume @p336 (forall @t99 (and (=> @t97 (= @t723 (_ tptp.hd_node @t69))) @t724))) % 0.48/0.93 (assume @p337 (forall @t99 (exists (@list @t774 @t773 @t589) (and (= @t66 (_ @t775 @t773)) (= @t69 (_ @t775 @t589)) (or (= @t773 tptp.nil_node) (= @t589 tptp.nil_node) (not (= (_ tptp.hd_node @t773) (_ tptp.hd_node @t589)))))))) % 0.48/0.93 (assume @p338 (forall (@list @t779 @t777) (=> @t781 (=> (=> (not (= @t779 tptp.nil_node)) (not (= @t777 tptp.nil_node))) (=> (forall (@list @t492 @t491) (=> @t780 (forall @t501 (=> @t778 (=> @t776 (_ (_ tptp.suffix_node @t491) @t398)))))) (not (forall (@list @t492) (=> (exists (@list @t491) @t780) (forall @t223 (=> (exists @t408 @t778) @t776)))))))))) % 0.48/0.93 (assume @p339 (forall (@list @t779 @t777 @t456) (=> @t781 (=> @t612 (=> (forall @t467 (=> @t523 @t600)) (=> (forall @t467 (=> @t522 (=> (not (_ (_ tptp.suffix_node @t398) @t390)) @t611))) (_ (_ @t456 @t779) @t777))))))) % 0.48/0.93 (assume @p340 (forall (@list @t550 @t782) (=> (= @t555 @t783) (=> (=> @t556 (=> (not @t783) (and (= @t728 (_ tptp.hd_node @t782)) (= @t727 (_ tptp.tl_node @t782))))) (= @t550 @t782))))) % 0.48/0.93 (assume @p341 (forall @t326 (=> (not (= @t62 @t772)) (=> @t65 (_ @t63 (_ tptp.set_val2 @t88)))))) % 0.48/0.93 (assume @p342 (forall @t330 (=> (not (= @t71 @t722)) (=> @t74 (_ @t72 @t784))))) % 0.48/0.93 (assume @p343 (forall @t319 (_ @t732 @t570))) % 0.48/0.93 (assume @p344 (forall @t730 (=> @t556 (= @t550 @t729)))) % 0.48/0.93 (assume @p345 (forall @t786 (=> @t98 (=> @t785 (_ (_ tptp.ord_less_eq_set_node @t784) @t215))))) % 0.48/0.93 (assume @p346 (forall @t786 (=> @t98 (=> @t785 (_ (_ tptp.ord_less_eq_set_node @t328) @t215))))) % 0.48/0.93 (assume @p347 (forall @t747 (=> (_ @t788 @t69) (=> (_ @t787 @t69) (or (_ @t788 @t744) (_ @t787 @t743)))))) % 0.48/0.93 (assume @p348 (= @t752 (lambda @t749 (and (_ (_ tptp.prefix_node @t259) @t748) (_ (_ tptp.prefix_node @t748) @t259))))) % 0.48/0.93 (assume @p349 (forall @t756 (=> (_ @t694 @t51) (=> (_ (_ tptp.prefix_node @t51) @t55) @t306)))) % 0.48/0.93 (assume @p350 @t793) % 0.48/0.93 (assume @p351 true) % 0.48/0.93 (step @p352 (= tptp.suffix_node @t794) :rule refl :args (@t794)) % 0.48/0.93 (step @p353 :rule refl :args ((tptp.graph_1012773594_edgeD tptp.alpha_n tptp.invar tptp.inEdges @t4 @t20 @t19 @t14))) % 0.48/0.93 (step @p354 :rule refl :args (@t14)) % 0.48/0.93 (step @p355 :rule refl :args ((tptp.append_node @t17 @t16))) % 0.48/0.93 (step @p356 :rule refl :args (@t795)) % 0.48/0.93 (step @p357 :rule refl :args (@t17)) % 0.48/0.93 (step @p358 :rule cong :premises (@p357 @p356) :args (@t796)) % 0.48/0.93 (step @p359 :rule trans :premises (@p358 @p355)) % 0.48/0.93 (step @p360 :rule refl :args (@t20)) % 0.48/0.93 (step @p361 :rule refl :args (@t4)) % 0.48/0.93 (step @p362 :rule refl :args (tptp.inEdges)) % 0.48/0.93 (step @p363 :rule refl :args (tptp.invar)) % 0.48/0.93 (step @p364 :rule refl :args (tptp.alpha_n)) % 0.48/0.93 (step @p365 :rule cong :premises (@p364 @p363 @p362 @p361 @p360 @p359 @p354) :args (@t797)) % 0.48/0.93 (step @p366 :rule trans :premises (@p365 @p353)) % 0.48/0.93 (step @p367 :rule refl :args (@t22)) % 0.48/0.93 (step @p368 :rule ho_cong :premises (@p367 @p359)) % 0.48/0.93 (step @p369 :rule ho_cong :premises (@p368 @p354)) % 0.48/0.93 (step @p370 :rule cong :premises (@p369 @p366) :args ((= (_ (_ @t22 @t796) @t14) @t797))) % 0.48/0.93 (step @p371 :rule symm :premises (@p370)) % 0.48/0.93 (step @p372 :rule refl :args (@t23)) % 0.48/0.93 (step @p373 :rule eq_resolve :premises (@p372 @p371)) % 0.48/0.93 (step @p374 :rule refl :args (@t18)) % 0.48/0.93 (step @p375 :rule ho_cong :premises (@p374 @p356)) % 0.48/0.93 (step @p376 :rule cong :premises (@p375 @p359) :args ((= (_ @t18 @t795) @t796))) % 0.48/0.93 (step @p377 :rule symm :premises (@p376)) % 0.48/0.93 (step @p378 :rule refl :args (@t19)) % 0.48/0.93 (step @p379 :rule eq_resolve :premises (@p378 @p377)) % 0.48/0.93 (step @p380 :rule refl :args (@t16)) % 0.48/0.93 (step @p381 :rule cong :premises (@p380 @p356) :args ((= @t16 @t795))) % 0.48/0.93 (step @p382 :rule symm :premises (@p381)) % 0.48/0.93 (step @p383 :rule eq_resolve :premises (@p380 @p382)) % 0.48/0.93 (step @p384 :rule ho_cong :premises (@p374 @p383)) % 0.48/0.93 (step @p385 :rule trans :premises (@p384 @p379)) % 0.48/0.93 (step @p386 :rule ho_cong :premises (@p367 @p385)) % 0.48/0.93 (step @p387 :rule ho_cong :premises (@p386 @p354)) % 0.48/0.93 (step @p388 :rule trans :premises (@p387 @p373)) % 0.48/0.93 (step @p389 :rule refl :args (@t798)) % 0.48/0.93 (step @p390 :rule refl :args (@t25)) % 0.48/0.93 (step @p391 :rule cong :premises (@p390 @p389) :args ((= @t25 @t798))) % 0.48/0.93 (step @p392 :rule symm :premises (@p391)) % 0.48/0.93 (step @p393 :rule eq_resolve :premises (@p390 @p392)) % 0.48/0.93 (step @p394 :rule cong :premises (@p393) :args (@t799)) % 0.48/0.93 (step @p395 :rule refl :args (@t800)) % 0.48/0.93 (step @p396 :rule refl :args (@t28)) % 0.48/0.93 (step @p397 :rule cong :premises (@p396 @p395) :args ((= @t28 @t800))) % 0.48/0.93 (step @p398 :rule symm :premises (@p397)) % 0.48/0.93 (step @p399 :rule eq_resolve :premises (@p396 @p398)) % 0.48/0.93 (step @p400 :rule cong :premises (@p399) :args (@t801)) % 0.48/0.93 (step @p401 :rule nary_cong :premises (@p400 @p394 @p388) :args (@t802)) % 0.48/0.93 (step @p402 :rule cong :premises (@p401) :args ((forall @t29 @t802))) % 0.48/0.93 (step @p403 :rule aci_norm :args ((= (or @t801 (or @t799 @t23)) @t802))) % 0.48/0.93 (step @p404 :rule bool-impl-elim :args (@t25 @t23)) % 0.48/0.93 (step @p405 :rule refl :args (@t801)) % 0.48/0.93 (step @p406 :rule nary_cong :premises (@p405 @p404) :args ((or @t801 @t26))) % 0.48/0.93 (step @p407 :rule trans :premises (@p406 @p403)) % 0.48/0.93 (step @p408 :rule bool-impl-elim :args (@t28 @t26)) % 0.48/0.93 (step @p409 :rule trans :premises (@p408 @p407)) % 0.48/0.93 (step @p410 :rule cong :premises (@p409) :args (@t30)) % 0.48/0.93 (step @p411 :rule trans :premises (@p410 @p402)) % 0.48/0.93 (step @p412 :rule eq_resolve :premises (@p6 @p411)) % 0.48/0.93 (step @p413 :rule refl :args ((tptp.graph_1012773594_edgeD tptp.alpha_n tptp.invar tptp.inEdges tptp.g2 @t6 tptp.ri @t2))) % 0.48/0.93 (step @p414 :rule refl :args (@t803)) % 0.48/0.93 (step @p415 :rule refl :args (tptp.ri)) % 0.48/0.93 (step @p416 :rule refl :args (@t804)) % 0.48/0.93 (step @p417 :rule refl :args (tptp.g2)) % 0.48/0.93 (step @p418 :rule cong :premises (@p364 @p363 @p362 @p417 @p416 @p415 @p414) :args (@t805)) % 0.48/0.93 (step @p419 :rule trans :premises (@p418 @p413)) % 0.48/0.93 (step @p420 :rule refl :args (@t8)) % 0.48/0.93 (step @p421 :rule ho_cong :premises (@p420 @p416)) % 0.48/0.93 (step @p422 :rule ho_cong :premises (@p421 @p415)) % 0.48/0.93 (step @p423 :rule ho_cong :premises (@p422 @p414)) % 0.48/0.93 (step @p424 :rule cong :premises (@p423 @p419) :args ((= (_ (_ (_ @t8 @t804) tptp.ri) @t803) @t805))) % 0.48/0.93 (step @p425 :rule symm :premises (@p424)) % 0.48/0.93 (step @p426 :rule refl :args ((_ @t13 @t2))) % 0.48/0.93 (step @p427 :rule eq_resolve :premises (@p426 @p425)) % 0.48/0.93 (step @p428 :rule refl :args (@t2)) % 0.48/0.93 (step @p429 :rule cong :premises (@p428 @p414) :args ((= @t2 @t803))) % 0.48/0.93 (step @p430 :rule symm :premises (@p429)) % 0.48/0.93 (step @p431 :rule eq_resolve :premises (@p428 @p430)) % 0.48/0.93 (step @p432 :rule refl :args (tptp.ri)) % 0.48/0.93 (step @p433 :rule refl :args (@t6)) % 0.48/0.93 (step @p434 :rule cong :premises (@p433 @p416) :args ((= @t6 @t804))) % 0.48/0.93 (step @p435 :rule symm :premises (@p434)) % 0.48/0.93 (step @p436 :rule eq_resolve :premises (@p433 @p435)) % 0.48/0.93 (step @p437 :rule refl :args (@t8)) % 0.48/0.93 (step @p438 :rule ho_cong :premises (@p437 @p436)) % 0.48/0.93 (step @p439 :rule ho_cong :premises (@p438 @p432)) % 0.48/0.93 (step @p440 :rule ho_cong :premises (@p439 @p431)) % 0.48/0.93 (step @p441 :rule trans :premises (@p440 @p427)) % 0.48/0.93 (step @p442 :rule refl :args (@t13)) % 0.48/0.93 (step @p443 :rule ho_cong :premises (@p442 @p2)) % 0.48/0.93 (step @p444 :rule trans :premises (@p443 @p441)) % 0.48/0.93 (step @p445 :rule eq_resolve :premises (@p5 @p444)) % 0.48/0.93 (step @p446 :rule refl :args ((tptp.graph_1012773594_edgeD tptp.alpha_n tptp.invar tptp.inEdges tptp.g2 tptp.n tptp.ns @t6))) % 0.48/0.93 (step @p447 :rule refl :args (tptp.ns)) % 0.48/0.93 (step @p448 :rule refl :args (tptp.n)) % 0.48/0.93 (step @p449 :rule cong :premises (@p364 @p363 @p362 @p417 @p448 @p447 @p416) :args (@t806)) % 0.48/0.93 (step @p450 :rule trans :premises (@p449 @p446)) % 0.48/0.93 (step @p451 :rule refl :args (@t10)) % 0.48/0.93 (step @p452 :rule ho_cong :premises (@p451 @p416)) % 0.48/0.93 (step @p453 :rule cong :premises (@p452 @p450) :args ((= (_ @t10 @t804) @t806))) % 0.48/0.93 (step @p454 :rule symm :premises (@p453)) % 0.48/0.93 (step @p455 :rule refl :args (@t11)) % 0.48/0.93 (step @p456 :rule eq_resolve :premises (@p455 @p454)) % 0.48/0.93 (step @p457 :rule refl :args (@t10)) % 0.48/0.93 (step @p458 :rule ho_cong :premises (@p457 @p436)) % 0.48/0.93 (step @p459 :rule trans :premises (@p458 @p456)) % 0.48/0.93 (step @p460 :rule eq_resolve :premises (@p4 @p459)) % 0.48/0.93 (step @p461 :rule refl :args ((tptp.graph_1012773594_edgeD tptp.alpha_n tptp.invar tptp.inEdges tptp.g2 tptp.n @t791 @t2))) % 0.48/0.93 (step @p462 :rule refl :args ((tptp.append_node tptp.ns @t789))) % 0.48/0.93 (step @p463 :rule refl :args (@t807)) % 0.48/0.93 (step @p464 :rule cong :premises (@p447 @p463) :args (@t808)) % 0.48/0.93 (step @p465 :rule trans :premises (@p464 @p462)) % 0.48/0.93 (step @p466 :rule cong :premises (@p364 @p363 @p362 @p417 @p448 @p465 @p414) :args (@t809)) % 0.48/0.93 (step @p467 :rule trans :premises (@p466 @p461)) % 0.48/0.93 (step @p468 :rule refl :args (@t9)) % 0.48/0.93 (step @p469 :rule ho_cong :premises (@p468 @p465)) % 0.48/0.93 (step @p470 :rule ho_cong :premises (@p469 @p414)) % 0.48/0.93 (step @p471 :rule cong :premises (@p470 @p467) :args ((= (_ (_ @t9 @t808) @t803) @t809))) % 0.48/0.93 (step @p472 :rule symm :premises (@p471)) % 0.48/0.93 (step @p473 :rule refl :args (@t792)) % 0.48/0.93 (step @p474 :rule eq_resolve :premises (@p473 @p472)) % 0.48/0.93 (step @p475 :rule refl :args (@t790)) % 0.48/0.93 (step @p476 :rule ho_cong :premises (@p475 @p463)) % 0.48/0.93 (step @p477 :rule cong :premises (@p476 @p465) :args ((= (_ @t790 @t807) @t808))) % 0.48/0.93 (step @p478 :rule symm :premises (@p477)) % 0.48/0.93 (step @p479 :rule refl :args (@t791)) % 0.48/0.93 (step @p480 :rule eq_resolve :premises (@p479 @p478)) % 0.48/0.93 (step @p481 :rule refl :args (@t789)) % 0.48/0.93 (step @p482 :rule cong :premises (@p481 @p463) :args ((= @t789 @t807))) % 0.48/0.93 (step @p483 :rule symm :premises (@p482)) % 0.48/0.93 (step @p484 :rule eq_resolve :premises (@p481 @p483)) % 0.48/0.93 (step @p485 :rule refl :args (@t790)) % 0.48/0.93 (step @p486 :rule ho_cong :premises (@p485 @p484)) % 0.48/0.93 (step @p487 :rule trans :premises (@p486 @p480)) % 0.48/0.93 (step @p488 :rule refl :args (@t9)) % 0.48/0.93 (step @p489 :rule ho_cong :premises (@p488 @p487)) % 0.48/0.93 (step @p490 :rule ho_cong :premises (@p489 @p431)) % 0.48/0.93 (step @p491 :rule trans :premises (@p490 @p474)) % 0.48/0.93 (step @p492 :rule cong :premises (@p491) :args (@t793)) % 0.48/0.93 (step @p493 :rule eq_resolve :premises (@p350 @p492)) % 0.48/0.93 (step @p494 :rule cnf_or_pos :args (@t812)) % 0.48/0.93 (step @p495 :rule reordering :premises (@p494) :args ((or @t809 @t811 @t810 @t813))) % 0.48/0.93 (step @p496 :rule chain_m_resolution :premises (@p495 @p493 @p460 @p445) :args (@t813 (@list true false false) (@list @t809 @t806 @t805))) % 0.48/0.93 (assume-push @p503 @t814) % 0.48/0.93 (step @p498 :rule instantiate :premises (@p412) :args ((@list tptp.g2 tptp.n tptp.ns @t804 tptp.ri @t803))) % 0.48/0.93 (step-pop @p504 :rule scope :premises (@p498)) % 0.48/0.93 (step @p499 :rule process_scope :premises (@p504) :args (@t812)) % 0.48/0.93 (step @p501 :rule implies_elim :premises (@p499)) % 0.48/0.93 (step @p502 false :rule chain_m_resolution :premises (@p501 @p496 @p412) :args (false (@list true false) (@list @t812 @t814))) % 0.48/0.93 ) % 0.48/0.93 % SZS output end Proof % 0.48/0.93 % cvc5 exiting %------------------------------------------------------------------------------