cvc5---1.3.4.THM-Prf.s

%------------------------------------------------------------------------------
% File     : cvc5---1.3.4
% Problem  : ITP082^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 : n017.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.46s 0.90s
% Output   : Proof 0.46s
% Verified : 
% SZS Type : -

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