cvc5---1.3.4.THM-Prf.s

%------------------------------------------------------------------------------
% File     : cvc5---1.3.4
% Problem  : ITP171^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 : n022.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:16 AM UTC 2026

% Result   : Theorem 48.28s 48.56s
% Output   : Proof 0.51s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : ITP171^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 : n022.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:17:23 EDT 2026
% 0.16/0.34  % CPUTime  : 
% 0.43/0.65  %----Proving TH0
% 48.28/48.56  --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s...
% 48.28/48.56  % SZS status Theorem
% 48.28/48.56  % SZS output start Proof
% 48.28/48.56  (
% 48.28/48.56  (declare-sort tptp.character_data_ptr_b 0)
% 48.28/48.56  (declare-sort tptp.option2061924698_ptr_b 0)
% 48.28/48.56  (declare-sort tptp.node_p1234578834tr_b_c 0)
% 48.28/48.56  (declare-sort tptp.docume1935157360tr_d_e 0)
% 48.28/48.56  (declare-sort tptp.heap_S1465075775_j_k_l 0)
% 48.28/48.56  (declare-sort tptp.option841825948on_j_k 0)
% 48.28/48.56  (declare-sort tptp.rObjec1617416918on_j_k 0)
% 48.28/48.56  (declare-sort tptp.m 0)
% 48.28/48.56  (declare-sort tptp.heap_E625070648t_unit 0)
% 48.28/48.56  (declare-sort tptp.n 0)
% 48.28/48.56  (declare-sort tptp.list_n282880152tr_b_c 0)
% 48.28/48.56  (declare-sort tptp.list_char 0)
% 48.28/48.56  (declare-sort tptp.rObjec1875798643tion_g 0)
% 48.28/48.56  (declare-sort tptp.element_ptr_a 0)
% 48.28/48.56  (declare-sort tptp.option392980921tion_g 0)
% 48.28/48.56  (declare-sort tptp.finite1621822014t_char 0)
% 48.28/48.56  (declare-sort tptp.option_element_ptr_a 0)
% 48.28/48.56  (declare-sort tptp.option147517124_ptr_d 0)
% 48.28/48.56  (declare-sort tptp.rObjec1922030987on_h_i 0)
% 48.28/48.56  (declare-sort tptp.option1128016977on_h_i 0)
% 48.28/48.56  (declare-sort tptp.option849832995tion_h 0)
% 48.28/48.56  (declare-sort tptp.rObjec1148923485tion_h 0)
% 48.28/48.56  (declare-sort tptp.option1344508504tr_b_c 0)
% 48.28/48.56  (declare-sort tptp.object945351580_d_e_f 0)
% 48.28/48.56  (declare-sort tptp.rObjec1413572695_j_k_l 0)
% 48.28/48.56  (declare-sort tptp.rObjec2068690451tion_j 0)
% 48.28/48.56  (declare-sort tptp.option1029218147tion_j 0)
% 48.28/48.56  (declare-sort tptp.heap_E834686006tion_n 0)
% 48.28/48.56  (declare-sort tptp.heap_E906991588_ptr_a 0)
% 48.28/48.56  (declare-sort tptp.heap_E1735400259tr_b_c 0)
% 48.28/48.56  (declare-sort tptp.heap_E434560396t_char 0)
% 48.28/48.56  (declare-sort tptp.product_unit 0)
% 48.28/48.56  (declare-sort tptp.heap_E1188946203tr_d_e 0)
% 48.28/48.56  (declare-sort tptp.heap_E826424501tion_m 0)
% 48.28/48.56  (declare-sort tptp.heap_E1996099391_ptr_b 0)
% 48.28/48.56  (declare-sort tptp.shadow_root_ptr_d 0)
% 48.28/48.56  (declare-sort tptp.heap_E1770015209t_char 0)
% 48.28/48.56  (declare-sort tptp.heap_E1661210526_ptr_a 0)
% 48.28/48.56  (declare-sort tptp.heap_E189844335_ptr_d 0)
% 48.28/48.56  (declare-const tptp.heap_E2101731758tr_d_e (-> tptp.heap_S1465075775_j_k_l tptp.heap_E1188946203tr_d_e tptp.docume1935157360tr_d_e Bool))
% 48.28/48.56  (declare-const tptp.heap_E1224694197_ptr_a (-> tptp.heap_S1465075775_j_k_l tptp.heap_E1661210526_ptr_a tptp.element_ptr_a Bool))
% 48.28/48.56  (declare-const tptp.heap_E667013711t_unit (-> tptp.heap_S1465075775_j_k_l tptp.heap_E625070648t_unit tptp.product_unit Bool))
% 48.28/48.56  (declare-const tptp.heap_E1038710092tion_m (-> tptp.heap_S1465075775_j_k_l tptp.heap_E826424501tion_m tptp.m Bool))
% 48.28/48.56  (declare-const tptp.heap_E1038710093tion_n (-> tptp.heap_S1465075775_j_k_l tptp.heap_E834686006tion_n tptp.n Bool))
% 48.28/48.56  (declare-const tptp.heap_E1982034951_ptr_b (-> tptp.heap_S1465075775_j_k_l tptp.heap_E1996099391_ptr_b tptp.heap_S1465075775_j_k_l Bool))
% 48.28/48.56  (declare-const tptp.heap_E1554207190_ptr_b (-> tptp.heap_S1465075775_j_k_l tptp.heap_E1996099391_ptr_b tptp.character_data_ptr_b Bool))
% 48.28/48.56  (declare-const tptp.heap_E2046843837tr_d_e (-> tptp.heap_S1465075775_j_k_l tptp.heap_E1188946203tr_d_e tptp.heap_S1465075775_j_k_l Bool))
% 48.28/48.56  (declare-const tptp.heap_E24690662_ptr_a (-> tptp.heap_S1465075775_j_k_l tptp.heap_E1661210526_ptr_a tptp.heap_S1465075775_j_k_l Bool))
% 48.28/48.56  (declare-const tptp.heap_E1553005822tion_n (-> tptp.heap_S1465075775_j_k_l tptp.heap_E834686006tion_n tptp.heap_S1465075775_j_k_l Bool))
% 48.28/48.56  (declare-const tptp.heap_E1553005821tion_m (-> tptp.heap_S1465075775_j_k_l tptp.heap_E826424501tion_m tptp.heap_S1465075775_j_k_l Bool))
% 48.28/48.56  (declare-const tptp.heap_E494191872t_unit (-> tptp.heap_S1465075775_j_k_l tptp.heap_E625070648t_unit tptp.heap_S1465075775_j_k_l Bool))
% 48.28/48.56  (declare-const tptp.none_R125524722tion_j tptp.option1029218147tion_j)
% 48.28/48.56  (declare-const tptp.cast_D1046746849_b_j_k (-> tptp.rObjec1617416918on_j_k tptp.option1029218147tion_j))
% 48.28/48.56  (declare-const tptp.new_ch829669006_j_k_l tptp.heap_E1996099391_ptr_b)
% 48.28/48.56  (declare-const tptp.new_el717272935_j_k_l tptp.heap_E1661210526_ptr_a)
% 48.28/48.56  (declare-const tptp.new_do4779043_j_k_l tptp.heap_E1188946203tr_d_e)
% 48.28/48.56  (declare-const tptp.cast_D1252964113_h_i_l (-> tptp.rObjec1617416918on_j_k tptp.rObjec1413572695_j_k_l))
% 48.28/48.56  (declare-const tptp.cast_d1608273229_b_c_f (-> tptp.docume1935157360tr_d_e tptp.object945351580_d_e_f))
% 48.28/48.56  (declare-const tptp.put_O_834343516_j_k_l (-> tptp.object945351580_d_e_f tptp.rObjec1413572695_j_k_l tptp.heap_S1465075775_j_k_l tptp.heap_S1465075775_j_k_l))
% 48.28/48.56  (declare-const tptp.getter (-> tptp.rObjec2068690451tion_j tptp.n))
% 48.28/48.56  (declare-const tptp.document_ptr tptp.docume1935157360tr_d_e)
% 48.28/48.56  (declare-const tptp.setter (-> (-> tptp.m tptp.m) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k))
% 48.28/48.56  (declare-const tptp.v tptp.m)
% 48.28/48.56  (declare-const tptp.h2 tptp.heap_S1465075775_j_k_l)
% 48.28/48.56  (declare-const tptp.some_c586507257_ptr_b (-> tptp.character_data_ptr_b tptp.option2061924698_ptr_b))
% 48.28/48.56  (declare-const tptp.cast_n1518532508_a_b_c (-> tptp.node_p1234578834tr_b_c tptp.option2061924698_ptr_b))
% 48.28/48.56  (declare-const tptp.l_put_1129034844_j_k_m (-> (-> tptp.docume1935157360tr_d_e tptp.heap_S1465075775_j_k_l tptp.option841825948on_j_k) (-> tptp.docume1935157360tr_d_e tptp.rObjec1617416918on_j_k tptp.heap_S1465075775_j_k_l tptp.heap_S1465075775_j_k_l) tptp.docume1935157360tr_d_e (-> (-> tptp.m tptp.m) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k) tptp.m tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.l_put_1129034845_j_k_n (-> (-> tptp.docume1935157360tr_d_e tptp.heap_S1465075775_j_k_l tptp.option841825948on_j_k) (-> tptp.docume1935157360tr_d_e tptp.rObjec1617416918on_j_k tptp.heap_S1465075775_j_k_l tptp.heap_S1465075775_j_k_l) tptp.docume1935157360tr_d_e (-> (-> tptp.n tptp.n) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k) tptp.n tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.l_put_38398219_ptr_a (-> (-> tptp.docume1935157360tr_d_e tptp.heap_S1465075775_j_k_l tptp.option841825948on_j_k) (-> tptp.docume1935157360tr_d_e tptp.rObjec1617416918on_j_k tptp.heap_S1465075775_j_k_l tptp.heap_S1465075775_j_k_l) tptp.docume1935157360tr_d_e (-> (-> tptp.option_element_ptr_a tptp.option_element_ptr_a) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k) tptp.option_element_ptr_a tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.l_put_893346794tr_b_c (-> (-> tptp.docume1935157360tr_d_e tptp.heap_S1465075775_j_k_l tptp.option841825948on_j_k) (-> tptp.docume1935157360tr_d_e tptp.rObjec1617416918on_j_k tptp.heap_S1465075775_j_k_l tptp.heap_S1465075775_j_k_l) tptp.docume1935157360tr_d_e (-> (-> tptp.list_n282880152tr_b_c tptp.list_n282880152tr_b_c) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k) tptp.list_n282880152tr_b_c tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.l_put_821218959t_char (-> (-> tptp.docume1935157360tr_d_e tptp.heap_S1465075775_j_k_l tptp.option841825948on_j_k) (-> tptp.docume1935157360tr_d_e tptp.rObjec1617416918on_j_k tptp.heap_S1465075775_j_k_l tptp.heap_S1465075775_j_k_l) tptp.docume1935157360tr_d_e (-> (-> tptp.list_char tptp.list_char) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k) tptp.list_char tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.l_put_1666965382t_char (-> (-> tptp.element_ptr_a tptp.heap_S1465075775_j_k_l tptp.option392980921tion_g) (-> tptp.element_ptr_a tptp.rObjec1875798643tion_g tptp.heap_S1465075775_j_k_l tptp.heap_S1465075775_j_k_l) tptp.element_ptr_a (-> (-> tptp.finite1621822014t_char tptp.finite1621822014t_char) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g) tptp.finite1621822014t_char tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.l_put_1449921049t_char (-> (-> tptp.element_ptr_a tptp.heap_S1465075775_j_k_l tptp.option392980921tion_g) (-> tptp.element_ptr_a tptp.rObjec1875798643tion_g tptp.heap_S1465075775_j_k_l tptp.heap_S1465075775_j_k_l) tptp.element_ptr_a (-> (-> tptp.list_char tptp.list_char) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g) tptp.list_char tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.l_put_2122145248tr_b_c (-> (-> tptp.element_ptr_a tptp.heap_S1465075775_j_k_l tptp.option392980921tion_g) (-> tptp.element_ptr_a tptp.rObjec1875798643tion_g tptp.heap_S1465075775_j_k_l tptp.heap_S1465075775_j_k_l) tptp.element_ptr_a (-> (-> tptp.list_n282880152tr_b_c tptp.list_n282880152tr_b_c) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g) tptp.list_n282880152tr_b_c tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.l_put_1103319052_ptr_d (-> (-> tptp.element_ptr_a tptp.heap_S1465075775_j_k_l tptp.option392980921tion_g) (-> tptp.element_ptr_a tptp.rObjec1875798643tion_g tptp.heap_S1465075775_j_k_l tptp.heap_S1465075775_j_k_l) tptp.element_ptr_a (-> (-> tptp.option147517124_ptr_d tptp.option147517124_ptr_d) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g) tptp.option147517124_ptr_d tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.get_E_312738192_j_k_l (-> tptp.element_ptr_a tptp.heap_S1465075775_j_k_l tptp.option392980921tion_g))
% 48.28/48.56  (declare-const tptp.put_E_1775770377_j_k_l (-> tptp.element_ptr_a tptp.rObjec1875798643tion_g tptp.heap_S1465075775_j_k_l tptp.heap_S1465075775_j_k_l))
% 48.28/48.56  (declare-const tptp.case_o1144239773on_h_i (-> tptp.option392980921tion_g (-> tptp.rObjec1922030987on_h_i tptp.option392980921tion_g) tptp.option1128016977on_h_i tptp.option392980921tion_g))
% 48.28/48.56  (declare-const tptp.cast_N1424394706on_h_i (-> tptp.rObjec1922030987on_h_i tptp.option392980921tion_g))
% 48.28/48.56  (declare-const tptp.l_put_1584770338t_char (-> (-> tptp.character_data_ptr_b tptp.heap_S1465075775_j_k_l tptp.option849832995tion_h) (-> tptp.character_data_ptr_b tptp.rObjec1148923485tion_h tptp.heap_S1465075775_j_k_l tptp.heap_S1465075775_j_k_l) tptp.character_data_ptr_b (-> (-> tptp.list_char tptp.list_char) tptp.rObjec1148923485tion_h tptp.rObjec1148923485tion_h) tptp.list_char tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.get_C_592656865_j_k_l (-> tptp.character_data_ptr_b tptp.heap_S1465075775_j_k_l tptp.option849832995tion_h))
% 48.28/48.56  (declare-const tptp.heap_E946351744t_char (-> tptp.heap_S1465075775_j_k_l tptp.heap_E1770015209t_char tptp.finite1621822014t_char Bool))
% 48.28/48.56  (declare-const tptp.heap_E258692314tr_b_c (-> tptp.heap_S1465075775_j_k_l tptp.heap_E1735400259tr_b_c tptp.list_n282880152tr_b_c Bool))
% 48.28/48.56  (declare-const tptp.heap_E1947147782_ptr_d (-> tptp.heap_S1465075775_j_k_l tptp.heap_E189844335_ptr_d tptp.option147517124_ptr_d Bool))
% 48.28/48.56  (declare-const tptp.put_M_1656033077_h_i_l (-> tptp.docume1935157360tr_d_e (-> (-> tptp.product_unit tptp.product_unit) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k) tptp.product_unit tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.get_M_1154267419_j_k_l (-> tptp.element_ptr_a (-> tptp.rObjec1875798643tion_g tptp.option147517124_ptr_d) tptp.heap_E189844335_ptr_d))
% 48.28/48.56  (declare-const tptp.put_M_2120900233_j_k_l (-> tptp.element_ptr_a (-> (-> tptp.n tptp.n) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g) tptp.n tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.put_M_1862598346_j_k_l (-> tptp.element_ptr_a (-> (-> tptp.m tptp.m) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g) tptp.m tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.shadow902827384_i_k_l (-> tptp.shadow_root_ptr_d (-> tptp.rObjec2068690451tion_j tptp.element_ptr_a) tptp.heap_E1661210526_ptr_a))
% 48.28/48.56  (declare-const tptp.doctyp814403297on_j_k (-> tptp.rObjec1617416918on_j_k tptp.list_char))
% 48.28/48.56  (declare-const tptp.get_M_220285781_j_k_l (-> tptp.element_ptr_a (-> tptp.rObjec1875798643tion_g tptp.m) tptp.heap_E826424501tion_m))
% 48.28/48.56  (declare-const tptp.case_o876177157tr_b_c (-> Bool (-> tptp.node_p1234578834tr_b_c Bool) tptp.option1344508504tr_b_c Bool))
% 48.28/48.56  (declare-const tptp.put_M_731120658_j_k_l (-> tptp.character_data_ptr_b (-> (-> tptp.element_ptr_a tptp.element_ptr_a) tptp.rObjec1148923485tion_h tptp.rObjec1148923485tion_h) tptp.element_ptr_a tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.put_M_1101791239_j_k_l (-> tptp.element_ptr_a (-> (-> tptp.product_unit tptp.product_unit) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g) tptp.product_unit tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.shadow1068876397_i_k_l (-> tptp.shadow_root_ptr_d (-> tptp.rObjec2068690451tion_j tptp.docume1935157360tr_d_e) tptp.heap_E1188946203tr_d_e))
% 48.28/48.56  (declare-const tptp.discon866287741on_j_k (-> tptp.rObjec1617416918on_j_k tptp.list_n282880152tr_b_c))
% 48.28/48.56  (declare-const tptp.get_M_1238860946_j_k_l (-> tptp.element_ptr_a (-> tptp.rObjec1875798643tion_g tptp.product_unit) tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.some_element_ptr_a (-> tptp.element_ptr_a tptp.option_element_ptr_a))
% 48.28/48.56  (declare-const tptp.put_M_1236788814_j_k_l (-> tptp.element_ptr_a (-> (-> tptp.docume1935157360tr_d_e tptp.docume1935157360tr_d_e) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g) tptp.docume1935157360tr_d_e tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.case_o18599603on_h_i (-> tptp.option849832995tion_h (-> tptp.rObjec1922030987on_h_i tptp.option849832995tion_h) tptp.option1128016977on_h_i tptp.option849832995tion_h))
% 48.28/48.56  (declare-const tptp.get_M_650077447_j_k_l (-> tptp.element_ptr_a (-> tptp.rObjec1875798643tion_g tptp.docume1935157360tr_d_e) tptp.heap_E1188946203tr_d_e))
% 48.28/48.56  (declare-const tptp.get_M_1903403023_j_k_l (-> tptp.character_data_ptr_b (-> tptp.rObjec1148923485tion_h tptp.product_unit) tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.shadow1030535182_i_k_l (-> tptp.shadow_root_ptr_d (-> (-> tptp.m tptp.m) tptp.rObjec2068690451tion_j tptp.rObjec2068690451tion_j) tptp.m tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.heap_E1876089495eption (-> tptp.heap_S1465075775_j_k_l tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.shadow1194684833_i_k_l (-> tptp.shadow_root_ptr_d (-> tptp.rObjec2068690451tion_j tptp.m) tptp.heap_E826424501tion_m))
% 48.28/48.56  (declare-const tptp.is_ele1129207902_t_r_a (-> tptp.element_ptr_a Bool))
% 48.28/48.56  (declare-const tptp.shadow1110190411_i_k_l (-> tptp.shadow_root_ptr_d (-> (-> tptp.product_unit tptp.product_unit) tptp.rObjec2068690451tion_j tptp.rObjec2068690451tion_j) tptp.product_unit tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.docume1175131570on_j_k (-> tptp.rObjec1617416918on_j_k tptp.option_element_ptr_a))
% 48.28/48.56  (declare-const tptp.shadow2050000606_i_k_l (-> tptp.shadow_root_ptr_d (-> tptp.rObjec2068690451tion_j tptp.product_unit) tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.heap_E804379039t_char (-> tptp.heap_S1465075775_j_k_l tptp.heap_E434560396t_char tptp.list_char Bool))
% 48.28/48.56  (declare-const tptp.discon442323090on_j_k (-> (-> tptp.list_n282880152tr_b_c tptp.list_n282880152tr_b_c) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k))
% 48.28/48.56  (declare-const tptp.docume244715269on_j_k (-> (-> tptp.option_element_ptr_a tptp.option_element_ptr_a) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k))
% 48.28/48.56  (declare-const tptp.shadow2015416421_i_k_l (-> tptp.shadow_root_ptr_d (-> (-> tptp.element_ptr_a tptp.element_ptr_a) tptp.rObjec2068690451tion_j tptp.rObjec2068690451tion_j) tptp.element_ptr_a tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.put_M_1937380872_j_k_l (-> tptp.character_data_ptr_b (-> (-> tptp.list_char tptp.list_char) tptp.rObjec1148923485tion_h tptp.rObjec1148923485tion_h) tptp.list_char tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.get_M_51280086_j_k_l (-> tptp.element_ptr_a (-> tptp.rObjec1875798643tion_g tptp.list_char) tptp.heap_E434560396t_char))
% 48.28/48.56  (declare-const tptp.get_M_544184404_h_i_l (-> tptp.docume1935157360tr_d_e (-> tptp.rObjec1617416918on_j_k tptp.n) tptp.heap_E834686006tion_n))
% 48.28/48.56  (declare-const tptp.get_M_88885319_j_k_l (-> tptp.element_ptr_a (-> tptp.rObjec1875798643tion_g tptp.list_n282880152tr_b_c) tptp.heap_E1735400259tr_b_c))
% 48.28/48.56  (declare-const tptp.cast_S988036065_b_j_k (-> tptp.rObjec2068690451tion_j tptp.rObjec1617416918on_j_k))
% 48.28/48.56  (declare-const tptp.is_cha330921893_a_b_c (-> tptp.node_p1234578834tr_b_c Bool))
% 48.28/48.56  (declare-const tptp.put_M_1198351521_j_k_l (-> tptp.element_ptr_a (-> (-> tptp.element_ptr_a tptp.element_ptr_a) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g) tptp.element_ptr_a tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.put_M_674497586_h_i_l (-> tptp.docume1935157360tr_d_e (-> (-> tptp.m tptp.m) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k) tptp.m tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.put_M_682984464_j_k_l (-> tptp.element_ptr_a (-> (-> tptp.option147517124_ptr_d tptp.option147517124_ptr_d) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g) tptp.option147517124_ptr_d tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.put_M_1098917052_j_k_l (-> tptp.element_ptr_a (-> (-> tptp.list_n282880152tr_b_c tptp.list_n282880152tr_b_c) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g) tptp.list_n282880152tr_b_c tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.cast_C1209085999_d_g_i (-> tptp.rObjec1148923485tion_h tptp.rObjec1922030987on_h_i))
% 48.28/48.56  (declare-const tptp.child_768225874tion_g (-> tptp.rObjec1875798643tion_g tptp.list_n282880152tr_b_c))
% 48.28/48.56  (declare-const tptp.put_M_1442125025_h_i_l (-> tptp.docume1935157360tr_d_e (-> (-> tptp.option_element_ptr_a tptp.option_element_ptr_a) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k) tptp.option_element_ptr_a tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.none_R509380180tion_g tptp.option392980921tion_g)
% 48.28/48.56  (declare-const tptp.get_M_1932781581_j_k_l (-> tptp.character_data_ptr_b (-> tptp.rObjec1148923485tion_h tptp.n) tptp.heap_E834686006tion_n))
% 48.28/48.56  (declare-const tptp.h tptp.heap_S1465075775_j_k_l)
% 48.28/48.56  (declare-const tptp.get_M_1965837010_h_i_l (-> tptp.docume1935157360tr_d_e (-> tptp.rObjec1617416918on_j_k tptp.product_unit) tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.put_M_257417239_h_i_l (-> tptp.docume1935157360tr_d_e (-> (-> tptp.list_char tptp.list_char) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k) tptp.list_char tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.get_M_90096148_j_k_l (-> tptp.element_ptr_a (-> tptp.rObjec1875798643tion_g tptp.n) tptp.heap_E834686006tion_n))
% 48.28/48.56  (declare-const tptp.cast_E1779426770on_h_i (-> tptp.rObjec1875798643tion_g tptp.rObjec1922030987on_h_i))
% 48.28/48.56  (declare-const tptp.put_C_229546338_j_k_l (-> tptp.character_data_ptr_b tptp.rObjec1148923485tion_h tptp.heap_S1465075775_j_k_l tptp.heap_S1465075775_j_k_l))
% 48.28/48.56  (declare-const tptp.cast_O1705702135_j_k_l (-> tptp.rObjec1413572695_j_k_l tptp.option1128016977on_h_i))
% 48.28/48.56  (declare-const tptp.cast_c164415100_b_a_c (-> tptp.character_data_ptr_b tptp.node_p1234578834tr_b_c))
% 48.28/48.56  (declare-const tptp.the_element_ptr_a (-> tptp.option_element_ptr_a tptp.element_ptr_a))
% 48.28/48.56  (declare-const tptp.get_M_1536717772_h_i_l (-> tptp.docume1935157360tr_d_e (-> tptp.rObjec1617416918on_j_k tptp.list_char) tptp.heap_E434560396t_char))
% 48.28/48.56  (declare-const tptp.shadow1843699917_i_k_l (-> tptp.shadow_root_ptr_d (-> (-> tptp.n tptp.n) tptp.rObjec2068690451tion_j tptp.rObjec2068690451tion_j) tptp.n tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.put_M_139724992_h_i_l (-> tptp.docume1935157360tr_d_e (-> (-> tptp.list_n282880152tr_b_c tptp.list_n282880152tr_b_c) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k) tptp.list_n282880152tr_b_c tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.type_w1479951274_j_k_l (-> tptp.heap_S1465075775_j_k_l Bool))
% 48.28/48.56  (declare-const tptp.cast_e316309897tr_b_c (-> tptp.element_ptr_a tptp.node_p1234578834tr_b_c))
% 48.28/48.56  (declare-const tptp.get_M_685446945_j_k_l (-> tptp.element_ptr_a (-> tptp.rObjec1875798643tion_g tptp.finite1621822014t_char) tptp.heap_E1770015209t_char))
% 48.28/48.56  (declare-const tptp.none_element_ptr_a tptp.option_element_ptr_a)
% 48.28/48.56  (declare-const tptp.get_M_986049031_h_i_l (-> tptp.docume1935157360tr_d_e (-> tptp.rObjec1617416918on_j_k tptp.list_n282880152tr_b_c) tptp.heap_E1735400259tr_b_c))
% 48.28/48.56  (declare-const tptp.get_D_1192261494_j_k_l (-> tptp.docume1935157360tr_d_e tptp.heap_S1465075775_j_k_l tptp.option841825948on_j_k))
% 48.28/48.56  (declare-const tptp.shadow569799008_i_k_l (-> tptp.shadow_root_ptr_d (-> tptp.rObjec2068690451tion_j tptp.n) tptp.heap_E834686006tion_n))
% 48.28/48.56  (declare-const tptp.heap_E1613639261eption tptp.heap_E625070648t_unit)
% 48.28/48.56  (declare-const tptp.shadow1464843188_i_k_l (-> tptp.shadow_root_ptr_d (-> (-> tptp.docume1935157360tr_d_e tptp.docume1935157360tr_d_e) tptp.rObjec2068690451tion_j tptp.rObjec2068690451tion_j) tptp.docume1935157360tr_d_e tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.l_type1130145226_j_k_l (-> tptp.heap_S1465075775_j_k_l Bool))
% 48.28/48.56  (declare-const tptp.get_M_1865279188_j_k_l (-> tptp.character_data_ptr_b (-> tptp.rObjec1148923485tion_h tptp.docume1935157360tr_d_e) tptp.heap_E1188946203tr_d_e))
% 48.28/48.56  (declare-const tptp.get_M_1644669866_j_k_l (-> tptp.node_p1234578834tr_b_c (-> tptp.rObjec1922030987on_h_i tptp.n) tptp.heap_E834686006tion_n))
% 48.28/48.56  (declare-const tptp.get_M_1186169077_j_k_l (-> tptp.character_data_ptr_b (-> tptp.rObjec1148923485tion_h tptp.element_ptr_a) tptp.heap_E1661210526_ptr_a))
% 48.28/48.56  (declare-const tptp.l_type85280056_j_k_l (-> tptp.heap_S1465075775_j_k_l Bool))
% 48.28/48.56  (declare-const tptp.doctyp68000440on_j_k (-> (-> tptp.list_char tptp.list_char) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k))
% 48.28/48.56  (declare-const tptp.put_M_1720094109_j_k_l (-> tptp.element_ptr_a (-> (-> tptp.list_char tptp.list_char) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g) tptp.list_char tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.shadow_root_ptr tptp.shadow_root_ptr_d)
% 48.28/48.56  (declare-const tptp.get_M_1422421269_h_i_l (-> tptp.docume1935157360tr_d_e (-> tptp.rObjec1617416918on_j_k tptp.m) tptp.heap_E826424501tion_m))
% 48.28/48.56  (declare-const tptp.put_M_168144691_h_i_l (-> tptp.docume1935157360tr_d_e (-> (-> tptp.n tptp.n) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k) tptp.n tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.put_M_1724091798_j_k_l (-> tptp.element_ptr_a (-> (-> tptp.finite1621822014t_char tptp.finite1621822014t_char) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g) tptp.finite1621822014t_char tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.get_M_1338284716_j_k_l (-> tptp.element_ptr_a (-> tptp.rObjec1875798643tion_g tptp.element_ptr_a) tptp.heap_E1661210526_ptr_a))
% 48.28/48.56  (declare-const tptp.none_R1587534007on_j_k tptp.option841825948on_j_k)
% 48.28/48.56  (declare-const tptp.get_M_1665432076_j_k_l (-> tptp.character_data_ptr_b (-> tptp.rObjec1148923485tion_h tptp.m) tptp.heap_E826424501tion_m))
% 48.28/48.56  (declare-const tptp.get_M_377480556_h_i_l (-> tptp.docume1935157360tr_d_e (-> tptp.rObjec1617416918on_j_k tptp.element_ptr_a) tptp.heap_E1661210526_ptr_a))
% 48.28/48.56  (declare-const tptp.put_M_1374331384_j_k_l (-> tptp.character_data_ptr_b (-> (-> tptp.product_unit tptp.product_unit) tptp.rObjec1148923485tion_h tptp.rObjec1148923485tion_h) tptp.product_unit tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.case_o1030391776tion_j (-> Bool (-> tptp.rObjec2068690451tion_j Bool) tptp.option1029218147tion_j Bool))
% 48.28/48.56  (declare-const tptp.the_ch963454248_ptr_b (-> tptp.option2061924698_ptr_b tptp.character_data_ptr_b))
% 48.28/48.56  (declare-const tptp.put_M_199545403_j_k_l (-> tptp.character_data_ptr_b (-> (-> tptp.m tptp.m) tptp.rObjec1148923485tion_h tptp.rObjec1148923485tion_h) tptp.m tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.put_M_243508858_j_k_l (-> tptp.character_data_ptr_b (-> (-> tptp.n tptp.n) tptp.rObjec1148923485tion_h tptp.rObjec1148923485tion_h) tptp.n tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.get_M_2088872005_j_k_l (-> tptp.character_data_ptr_b (-> tptp.rObjec1148923485tion_h tptp.list_char) tptp.heap_E434560396t_char))
% 48.28/48.56  (declare-const tptp.type_w697503069_j_k_l (-> tptp.heap_S1465075775_j_k_l Bool))
% 48.28/48.56  (declare-const tptp.cast_n552817316_d_e_f (-> tptp.node_p1234578834tr_b_c tptp.object945351580_d_e_f))
% 48.28/48.56  (declare-const tptp.get_M_462148605_h_i_l (-> tptp.docume1935157360tr_d_e (-> tptp.rObjec1617416918on_j_k tptp.docume1935157360tr_d_e) tptp.heap_E1188946203tr_d_e))
% 48.28/48.56  (declare-const tptp.put_M_2097930918_h_i_l (-> tptp.docume1935157360tr_d_e (-> (-> tptp.docume1935157360tr_d_e tptp.docume1935157360tr_d_e) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k) tptp.docume1935157360tr_d_e tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.put_M_1789706523_h_i_l (-> tptp.docume1935157360tr_d_e (-> (-> tptp.element_ptr_a tptp.element_ptr_a) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k) tptp.element_ptr_a tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.cast_s253715760_r_d_e (-> tptp.shadow_root_ptr_d tptp.docume1935157360tr_d_e))
% 48.28/48.56  (declare-const tptp.get_M_1723352102_h_i_l (-> tptp.docume1935157360tr_d_e (-> tptp.rObjec1617416918on_j_k tptp.option_element_ptr_a) tptp.heap_E906991588_ptr_a))
% 48.28/48.56  (declare-const tptp.heap_E1091541499_ptr_a (-> tptp.heap_S1465075775_j_k_l tptp.heap_E906991588_ptr_a tptp.option_element_ptr_a Bool))
% 48.28/48.56  (declare-const tptp.val_update_option_h (-> (-> tptp.list_char tptp.list_char) tptp.rObjec1148923485tion_h tptp.rObjec1148923485tion_h))
% 48.28/48.56  (declare-const tptp.attrs_1280717024tion_g (-> (-> tptp.finite1621822014t_char tptp.finite1621822014t_char) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g))
% 48.28/48.56  (declare-const tptp.shadow1606659473tion_g (-> (-> tptp.option147517124_ptr_d tptp.option147517124_ptr_d) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g))
% 48.28/48.56  (declare-const tptp.nil_no279930520tr_b_c tptp.list_n282880152tr_b_c)
% 48.28/48.56  (declare-const tptp.child_1596411111tion_g (-> (-> tptp.list_n282880152tr_b_c tptp.list_n282880152tr_b_c) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g))
% 48.28/48.56  (declare-const tptp.tag_na7058269tion_g (-> (-> tptp.list_char tptp.list_char) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g))
% 48.28/48.56  (declare-const tptp.type_w2078707819_j_k_l (-> tptp.heap_S1465075775_j_k_l Bool))
% 48.28/48.56  (declare-const tptp.type_w1771507213_j_k_l (-> tptp.heap_S1465075775_j_k_l Bool))
% 48.28/48.56  (declare-const tptp.cast_N1183075319_j_k_l (-> tptp.rObjec1922030987on_h_i tptp.rObjec1413572695_j_k_l))
% 48.28/48.56  (declare-const tptp.the_RO2055010943tion_j (-> tptp.option1029218147tion_j tptp.rObjec2068690451tion_j))
% 48.28/48.56  (declare-const tptp.l_type1003141153_j_k_l (-> tptp.heap_S1465075775_j_k_l Bool))
% 48.28/48.56  (declare-const tptp.none_s1706699231_ptr_d tptp.option147517124_ptr_d)
% 48.28/48.56  (declare-const tptp.shadow1820683706tion_g (-> tptp.rObjec1875798643tion_g tptp.option147517124_ptr_d))
% 48.28/48.56  (declare-const tptp.none_R417230014tion_h tptp.option849832995tion_h)
% 48.28/48.56  (declare-const tptp.is_cha504820986_t_r_b (-> tptp.character_data_ptr_b Bool))
% 48.28/48.56  (declare-const tptp.val_option_h (-> tptp.rObjec1148923485tion_h tptp.list_char))
% 48.28/48.56  (declare-const tptp.attrs_1151927177tion_g (-> tptp.rObjec1875798643tion_g tptp.finite1621822014t_char))
% 48.28/48.56  (declare-const tptp.get_M_421785767_k_l_n (-> tptp.object945351580_d_e_f (-> tptp.rObjec1413572695_j_k_l tptp.n) tptp.heap_E834686006tion_n))
% 48.28/48.56  (declare-const tptp.tag_na866435078tion_g (-> tptp.rObjec1875798643tion_g tptp.list_char))
% 48.28/48.56  (declare-const tptp.finite2103212841t_char tptp.finite1621822014t_char)
% 48.28/48.56  (declare-const tptp.is_doc1417632087_j_k_l (-> tptp.rObjec1413572695_j_k_l Bool))
% 48.28/48.56  (declare-const tptp.cast_O1034441233_j_k_l (-> tptp.rObjec1413572695_j_k_l tptp.option841825948on_j_k))
% 48.28/48.56  (declare-const tptp.is_doc2037328342tr_d_e (-> tptp.docume1935157360tr_d_e Bool))
% 48.28/48.56  (declare-const tptp.some_R700141678tion_j (-> tptp.rObjec2068690451tion_j tptp.option1029218147tion_j))
% 48.28/48.56  (declare-const tptp.put_M_726238649_j_k_l (-> tptp.character_data_ptr_b (-> (-> tptp.docume1935157360tr_d_e tptp.docume1935157360tr_d_e) tptp.rObjec1148923485tion_h tptp.rObjec1148923485tion_h) tptp.docume1935157360tr_d_e tptp.heap_E625070648t_unit))
% 48.28/48.56  (declare-const tptp.some_R67702331on_j_k (-> tptp.rObjec1617416918on_j_k tptp.option841825948on_j_k))
% 48.28/48.56  (declare-const tptp.cast_n269450313tr_b_c (-> tptp.node_p1234578834tr_b_c tptp.option_element_ptr_a))
% 48.28/48.56  (declare-const tptp.is_ele1259807012tr_b_c (-> tptp.node_p1234578834tr_b_c Bool))
% 48.28/48.56  (declare-const tptp.is_doc45233057_d_e_f (-> tptp.object945351580_d_e_f Bool))
% 48.28/48.56  (declare-const tptp.nil_char tptp.list_char)
% 48.28/48.56  (declare-const tptp.cast_N1374991725_g_h_i (-> tptp.rObjec1922030987on_h_i tptp.option849832995tion_h))
% 48.28/48.56  (declare-const tptp.cast_o664948310_d_e_f (-> tptp.object945351580_d_e_f tptp.option1344508504tr_b_c))
% 48.28/48.56  (define tptp.heap_E808638982tr_d_e () (let ((_let_1 (@var "X3" tptp.docume1935157360tr_d_e))) (let ((_let_2 (@var "F2" tptp.heap_E1188946203tr_d_e))) (let ((_let_3 (@var "H5" tptp.heap_S1465075775_j_k_l))) (let ((_let_4 (@var "H4" tptp.heap_S1465075775_j_k_l))) (lambda (@list _let_2 _let_4 _let_3) (forall (@list _let_1) (= (_ (_ (_ tptp.heap_E2101731758tr_d_e _let_4) _let_2) _let_1) (_ (_ (_ tptp.heap_E2101731758tr_d_e _let_3) _let_2) _let_1)))))))))
% 48.28/48.56  (define tptp.heap_E73132893_ptr_a () (let ((_let_1 (@var "X3" tptp.element_ptr_a))) (let ((_let_2 (@var "F2" tptp.heap_E1661210526_ptr_a))) (let ((_let_3 (@var "H5" tptp.heap_S1465075775_j_k_l))) (let ((_let_4 (@var "H4" tptp.heap_S1465075775_j_k_l))) (lambda (@list _let_2 _let_4 _let_3) (forall (@list _let_1) (= (_ (_ (_ tptp.heap_E1224694197_ptr_a _let_4) _let_2) _let_1) (_ (_ (_ tptp.heap_E1224694197_ptr_a _let_3) _let_2) _let_1)))))))))
% 48.28/48.56  (define tptp.heap_E1521571831t_unit () (let ((_let_1 (@var "X3" tptp.product_unit))) (let ((_let_2 (@var "F2" tptp.heap_E625070648t_unit))) (let ((_let_3 (@var "H5" tptp.heap_S1465075775_j_k_l))) (let ((_let_4 (@var "H4" tptp.heap_S1465075775_j_k_l))) (lambda (@list _let_2 _let_4 _let_3) (forall (@list _let_1) (= (_ (_ (_ tptp.heap_E667013711t_unit _let_4) _let_2) _let_1) (_ (_ (_ tptp.heap_E667013711t_unit _let_3) _let_2) _let_1)))))))))
% 48.28/48.56  (define tptp.heap_E1683112692tion_m () (let ((_let_1 (@var "X3" tptp.m))) (let ((_let_2 (@var "F2" tptp.heap_E826424501tion_m))) (let ((_let_3 (@var "H5" tptp.heap_S1465075775_j_k_l))) (let ((_let_4 (@var "H4" tptp.heap_S1465075775_j_k_l))) (lambda (@list _let_2 _let_4 _let_3) (forall (@list _let_1) (= (_ (_ (_ tptp.heap_E1038710092tion_m _let_4) _let_2) _let_1) (_ (_ (_ tptp.heap_E1038710092tion_m _let_3) _let_2) _let_1)))))))))
% 48.28/48.56  (define tptp.heap_E1683112693tion_n () (let ((_let_1 (@var "X3" tptp.n))) (let ((_let_2 (@var "F2" tptp.heap_E834686006tion_n))) (let ((_let_3 (@var "H5" tptp.heap_S1465075775_j_k_l))) (let ((_let_4 (@var "H4" tptp.heap_S1465075775_j_k_l))) (lambda (@list _let_2 _let_4 _let_3) (forall (@list _let_1) (= (_ (_ (_ tptp.heap_E1038710093tion_n _let_4) _let_2) _let_1) (_ (_ (_ tptp.heap_E1038710093tion_n _let_3) _let_2) _let_1)))))))))
% 48.28/48.56  (define tptp.heap_E1679280842_ptr_b () (let ((_let_1 (@var "H5" tptp.heap_S1465075775_j_k_l))) (let ((_let_2 (@var "P" tptp.heap_E1996099391_ptr_b))) (let ((_let_3 (@var "H4" tptp.heap_S1465075775_j_k_l))) (let ((_let_4 (@var "R" tptp.character_data_ptr_b))) (lambda (@list _let_3 _let_2 _let_4 _let_1) (and (_ (_ (_ tptp.heap_E1554207190_ptr_b _let_3) _let_2) _let_4) (_ (_ (_ tptp.heap_E1982034951_ptr_b _let_3) _let_2) _let_1))))))))
% 48.28/48.56  (define tptp.heap_E1720378810tr_d_e () (let ((_let_1 (@var "H5" tptp.heap_S1465075775_j_k_l))) (let ((_let_2 (@var "P" tptp.heap_E1188946203tr_d_e))) (let ((_let_3 (@var "H4" tptp.heap_S1465075775_j_k_l))) (let ((_let_4 (@var "R" tptp.docume1935157360tr_d_e))) (lambda (@list _let_3 _let_2 _let_4 _let_1) (and (_ (_ (_ tptp.heap_E2101731758tr_d_e _let_3) _let_2) _let_4) (_ (_ (_ tptp.heap_E2046843837tr_d_e _let_3) _let_2) _let_1))))))))
% 48.28/48.56  (define tptp.heap_E2092016297_ptr_a () (let ((_let_1 (@var "H5" tptp.heap_S1465075775_j_k_l))) (let ((_let_2 (@var "P" tptp.heap_E1661210526_ptr_a))) (let ((_let_3 (@var "H4" tptp.heap_S1465075775_j_k_l))) (let ((_let_4 (@var "R" tptp.element_ptr_a))) (lambda (@list _let_3 _let_2 _let_4 _let_1) (and (_ (_ (_ tptp.heap_E1224694197_ptr_a _let_3) _let_2) _let_4) (_ (_ (_ tptp.heap_E24690662_ptr_a _let_3) _let_2) _let_1))))))))
% 48.28/48.56  (define tptp.heap_E1940720705tion_n () (let ((_let_1 (@var "H5" tptp.heap_S1465075775_j_k_l))) (let ((_let_2 (@var "P" tptp.heap_E834686006tion_n))) (let ((_let_3 (@var "H4" tptp.heap_S1465075775_j_k_l))) (let ((_let_4 (@var "R" tptp.n))) (lambda (@list _let_3 _let_2 _let_4 _let_1) (and (_ (_ (_ tptp.heap_E1038710093tion_n _let_3) _let_2) _let_4) (_ (_ (_ tptp.heap_E1553005822tion_n _let_3) _let_2) _let_1))))))))
% 48.28/48.56  (define tptp.heap_E1940720704tion_m () (let ((_let_1 (@var "H5" tptp.heap_S1465075775_j_k_l))) (let ((_let_2 (@var "P" tptp.heap_E826424501tion_m))) (let ((_let_3 (@var "H4" tptp.heap_S1465075775_j_k_l))) (let ((_let_4 (@var "R" tptp.m))) (lambda (@list _let_3 _let_2 _let_4 _let_1) (and (_ (_ (_ tptp.heap_E1038710092tion_m _let_3) _let_2) _let_4) (_ (_ (_ tptp.heap_E1553005821tion_m _let_3) _let_2) _let_1))))))))
% 48.28/48.56  (define tptp.heap_E1993614659t_unit () (let ((_let_1 (@var "H5" tptp.heap_S1465075775_j_k_l))) (let ((_let_2 (@var "P" tptp.heap_E625070648t_unit))) (let ((_let_3 (@var "H4" tptp.heap_S1465075775_j_k_l))) (let ((_let_4 (@var "R" tptp.product_unit))) (lambda (@list _let_3 _let_2 _let_4 _let_1) (and (_ (_ (_ tptp.heap_E667013711t_unit _let_3) _let_2) _let_4) (_ (_ (_ tptp.heap_E494191872t_unit _let_3) _let_2) _let_1))))))))
% 48.28/48.56  (define tptp.is_sha1522929624_b_j_k () (let ((_let_1 (@var "Ptr" tptp.rObjec1617416918on_j_k))) (lambda (@list _let_1) (not (= (_ tptp.cast_D1046746849_b_j_k _let_1) tptp.none_R125524722tion_j)))))
% 48.28/48.56  (define tptp.l_new_410495338_j_k_l () (let ((_let_1 (@var "H5" tptp.heap_S1465075775_j_k_l))) (let ((_let_2 (@var "Type_wf" (-> tptp.heap_S1465075775_j_k_l Bool)))) (let ((_let_3 (@var "H4" tptp.heap_S1465075775_j_k_l))) (lambda (@list _let_2) (forall (@list _let_3 _let_1) (=> (_ (_ (_ tptp.heap_E1982034951_ptr_b _let_3) tptp.new_ch829669006_j_k_l) _let_1) (= (_ _let_2 _let_3) (_ _let_2 _let_1)))))))))
% 48.28/48.56  (define tptp.l_new_540233301_j_k_l () (let ((_let_1 (@var "H5" tptp.heap_S1465075775_j_k_l))) (let ((_let_2 (@var "Type_wf" (-> tptp.heap_S1465075775_j_k_l Bool)))) (let ((_let_3 (@var "H4" tptp.heap_S1465075775_j_k_l))) (lambda (@list _let_2) (forall (@list _let_3 _let_1) (=> (_ (_ (_ tptp.heap_E24690662_ptr_a _let_3) tptp.new_el717272935_j_k_l) _let_1) (= (_ _let_2 _let_3) (_ _let_2 _let_1)))))))))
% 48.28/48.56  (define tptp.l_new_1474790279_j_k_l () (let ((_let_1 (@var "H5" tptp.heap_S1465075775_j_k_l))) (let ((_let_2 (@var "Type_wf" (-> tptp.heap_S1465075775_j_k_l Bool)))) (let ((_let_3 (@var "H4" tptp.heap_S1465075775_j_k_l))) (lambda (@list _let_2) (forall (@list _let_3 _let_1) (=> (_ (_ (_ tptp.heap_E2046843837tr_d_e _let_3) tptp.new_do4779043_j_k_l) _let_1) (= (_ _let_2 _let_3) (_ _let_2 _let_1)))))))))
% 48.28/48.56  (define tptp.put_D_2126422573_h_i_l () (let ((_let_1 (@var "__flatten_var_0" tptp.heap_S1465075775_j_k_l))) (let ((_let_2 (@var "Document2" tptp.rObjec1617416918on_j_k))) (let ((_let_3 (@var "Document_ptr3" tptp.docume1935157360tr_d_e))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ (_ tptp.put_O_834343516_j_k_l (_ tptp.cast_d1608273229_b_c_f _let_3)) (_ tptp.cast_D1252964113_h_i_l _let_2)) _let_1))))))
% 48.28/48.56  (define @t1 () (@var "H2" tptp.heap_S1465075775_j_k_l))
% 48.28/48.56  (define @t2 () (@var "H" tptp.heap_S1465075775_j_k_l))
% 48.28/48.56  (define @t3 () (@var "Getter" (-> tptp.rObjec2068690451tion_j tptp.n)))
% 48.28/48.56  (define @t4 () (@var "Shadow_root_ptr" tptp.shadow_root_ptr_d))
% 48.28/48.56  (define @t5 () (_ (_ tptp.shadow569799008_i_k_l @t4) @t3))
% 48.28/48.56  (define @t6 () (_ (_ (_ tptp.heap_E1683112693tion_n @t5) @t2) @t1))
% 48.28/48.56  (define @t7 () (@var "V" tptp.list_char))
% 48.28/48.56  (define @t8 () (@var "Setter" (-> (-> tptp.list_char tptp.list_char) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k)))
% 48.28/48.56  (define @t9 () (@var "Document_ptr" tptp.docume1935157360tr_d_e))
% 48.28/48.56  (define @t10 () (_ tptp.put_M_257417239_h_i_l @t9))
% 48.28/48.56  (define @t11 () (_ tptp.heap_E494191872t_unit @t2))
% 48.28/48.56  (define @t12 () (_ (_ @t11 (_ (_ @t10 @t8) @t7)) @t1))
% 48.28/48.56  (define @t13 () (_ tptp.cast_s253715760_r_d_e @t4))
% 48.28/48.56  (define @t14 () (not (= @t13 @t9)))
% 48.28/48.56  (define @t15 () (@var "V" tptp.list_n282880152tr_b_c))
% 48.28/48.56  (define @t16 () (@var "Setter" (-> (-> tptp.list_n282880152tr_b_c tptp.list_n282880152tr_b_c) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k)))
% 48.28/48.56  (define @t17 () (_ tptp.put_M_139724992_h_i_l @t9))
% 48.28/48.56  (define @t18 () (_ (_ @t11 (_ (_ @t17 @t16) @t15)) @t1))
% 48.28/48.56  (define @t19 () (@var "V" tptp.option_element_ptr_a))
% 48.28/48.56  (define @t20 () (@var "Setter" (-> (-> tptp.option_element_ptr_a tptp.option_element_ptr_a) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k)))
% 48.28/48.56  (define @t21 () (_ tptp.put_M_1442125025_h_i_l @t9))
% 48.28/48.56  (define @t22 () (_ (_ @t11 (_ (_ @t21 @t20) @t19)) @t1))
% 48.28/48.56  (define @t23 () (@var "V" tptp.n))
% 48.28/48.56  (define @t24 () (@var "Setter" (-> (-> tptp.n tptp.n) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k)))
% 48.28/48.56  (define @t25 () (_ (_ @t11 (_ (_ (_ tptp.put_M_168144691_h_i_l @t9) @t24) @t23)) @t1))
% 48.28/48.56  (define @t26 () (@var "V" tptp.m))
% 48.28/48.56  (define @t27 () (@var "Setter" (-> (-> tptp.m tptp.m) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k)))
% 48.28/48.56  (define @t28 () (_ (_ (_ tptp.put_M_674497586_h_i_l @t9) @t27) @t26))
% 48.28/48.56  (define @t29 () (_ (_ @t11 @t28) @t1))
% 48.28/48.56  (define @t30 () (=> @t29 @t6))
% 48.28/48.56  (define @t31 () (=> @t14 @t30))
% 48.28/48.56  (define @t32 () (@list @t4 @t9 @t2 @t27 @t26 @t1 @t3))
% 48.28/48.56  (define @t33 () (forall @t32 @t31))
% 48.28/48.56  (define @t34 () (@var "Y" tptp.rObjec2068690451tion_j))
% 48.28/48.56  (define @t35 () (@var "X" tptp.rObjec2068690451tion_j))
% 48.28/48.56  (define @t36 () (@var "Y" tptp.shadow_root_ptr_d))
% 48.28/48.56  (define @t37 () (@var "X" tptp.shadow_root_ptr_d))
% 48.28/48.56  (define @t38 () (@var "Shadow_root_ptr2" tptp.shadow_root_ptr_d))
% 48.28/48.56  (define @t39 () (_ (_ (_ tptp.heap_E1683112693tion_n (_ (_ tptp.shadow569799008_i_k_l @t38) @t3)) @t2) @t1))
% 48.28/48.56  (define @t40 () (@var "X2" tptp.rObjec2068690451tion_j))
% 48.28/48.56  (define @t41 () (lambda (@list (@var "Uu" tptp.n)) @t23))
% 48.28/48.56  (define @t42 () (@var "Setter" (-> (-> tptp.n tptp.n) tptp.rObjec2068690451tion_j tptp.rObjec2068690451tion_j)))
% 48.28/48.56  (define @t43 () (_ (_ @t42 @t41) @t40))
% 48.28/48.56  (define @t44 () (_ @t3 @t43))
% 48.28/48.56  (define @t45 () (@list @t40))
% 48.28/48.56  (define @t46 () (_ (_ @t11 (_ (_ (_ tptp.shadow1843699917_i_k_l @t4) @t42) @t23)) @t1))
% 48.28/48.56  (define @t47 () (@var "Setter" (-> (-> tptp.list_char tptp.list_char) tptp.rObjec1148923485tion_h tptp.rObjec1148923485tion_h)))
% 48.28/48.56  (define @t48 () (@var "Character_data_ptr" tptp.character_data_ptr_b))
% 48.28/48.56  (define @t49 () (_ tptp.put_M_1937380872_j_k_l @t48))
% 48.28/48.56  (define @t50 () (_ (_ @t11 (_ (_ @t49 @t47) @t7)) @t1))
% 48.28/48.56  (define @t51 () (@var "V" tptp.option147517124_ptr_d))
% 48.28/48.56  (define @t52 () (@var "Setter" (-> (-> tptp.option147517124_ptr_d tptp.option147517124_ptr_d) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g)))
% 48.28/48.56  (define @t53 () (@var "Element_ptr" tptp.element_ptr_a))
% 48.28/48.56  (define @t54 () (_ tptp.put_M_682984464_j_k_l @t53))
% 48.28/48.56  (define @t55 () (_ (_ @t11 (_ (_ @t54 @t52) @t51)) @t1))
% 48.28/48.56  (define @t56 () (@var "Setter" (-> (-> tptp.list_n282880152tr_b_c tptp.list_n282880152tr_b_c) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g)))
% 48.28/48.56  (define @t57 () (_ tptp.put_M_1098917052_j_k_l @t53))
% 48.28/48.56  (define @t58 () (_ (_ @t11 (_ (_ @t57 @t56) @t15)) @t1))
% 48.28/48.56  (define @t59 () (@var "Setter" (-> (-> tptp.list_char tptp.list_char) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g)))
% 48.28/48.56  (define @t60 () (_ tptp.put_M_1720094109_j_k_l @t53))
% 48.28/48.56  (define @t61 () (_ (_ @t11 (_ (_ @t60 @t59) @t7)) @t1))
% 48.28/48.56  (define @t62 () (@var "V" tptp.finite1621822014t_char))
% 48.28/48.56  (define @t63 () (@var "Setter" (-> (-> tptp.finite1621822014t_char tptp.finite1621822014t_char) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g)))
% 48.28/48.56  (define @t64 () (_ tptp.put_M_1724091798_j_k_l @t53))
% 48.28/48.56  (define @t65 () (_ (_ @t11 (_ (_ @t64 @t63) @t62)) @t1))
% 48.28/48.56  (define @t66 () (@var "Getter" (-> tptp.rObjec1617416918on_j_k tptp.m)))
% 48.28/48.56  (define @t67 () (@var "Document_ptr2" tptp.docume1935157360tr_d_e))
% 48.28/48.56  (define @t68 () (_ (_ (_ tptp.heap_E1683112692tion_m (_ (_ tptp.get_M_1422421269_h_i_l @t67) @t66)) @t2) @t1))
% 48.28/48.56  (define @t69 () (@var "X2" tptp.rObjec1617416918on_j_k))
% 48.28/48.56  (define @t70 () (_ @t66 @t69))
% 48.28/48.56  (define @t71 () (@list (@var "Uu" tptp.m)))
% 48.28/48.56  (define @t72 () (lambda @t71 @t26))
% 48.28/48.56  (define @t73 () (_ (_ @t27 @t72) @t69))
% 48.28/48.56  (define @t74 () (_ @t66 @t73))
% 48.28/48.56  (define @t75 () (@list @t69))
% 48.28/48.56  (define @t76 () (@var "Getter" (-> tptp.rObjec1617416918on_j_k tptp.n)))
% 48.28/48.56  (define @t77 () (_ (_ (_ tptp.heap_E1683112693tion_n (_ (_ tptp.get_M_544184404_h_i_l @t67) @t76)) @t2) @t1))
% 48.28/48.56  (define @t78 () (_ @t76 @t69))
% 48.28/48.56  (define @t79 () (lambda (@list (@var "Uu" tptp.list_char)) @t7))
% 48.28/48.56  (define @t80 () (_ (_ @t8 @t79) @t69))
% 48.28/48.56  (define @t81 () (lambda (@list (@var "Uu" tptp.list_n282880152tr_b_c)) @t15))
% 48.28/48.56  (define @t82 () (_ (_ @t16 @t81) @t69))
% 48.28/48.56  (define @t83 () (lambda (@list (@var "Uu" tptp.option_element_ptr_a)) @t19))
% 48.28/48.56  (define @t84 () (_ (_ @t20 @t83) @t69))
% 48.28/48.56  (define @t85 () (_ (_ @t24 @t41) @t69))
% 48.28/48.56  (define @t86 () (_ @t76 @t85))
% 48.28/48.56  (define @t87 () (@var "H3" tptp.heap_S1465075775_j_k_l))
% 48.28/48.56  (define @t88 () (= @t1 @t87))
% 48.28/48.56  (define @t89 () (@var "F" tptp.heap_E1996099391_ptr_b))
% 48.28/48.56  (define @t90 () (_ tptp.heap_E1982034951_ptr_b @t2))
% 48.28/48.56  (define @t91 () (_ @t90 @t89))
% 48.28/48.56  (define @t92 () (@var "F" tptp.heap_E1661210526_ptr_a))
% 48.28/48.56  (define @t93 () (_ tptp.heap_E24690662_ptr_a @t2))
% 48.28/48.56  (define @t94 () (_ @t93 @t92))
% 48.28/48.56  (define @t95 () (@var "F" tptp.heap_E1188946203tr_d_e))
% 48.28/48.56  (define @t96 () (_ tptp.heap_E2046843837tr_d_e @t2))
% 48.28/48.56  (define @t97 () (_ @t96 @t95))
% 48.28/48.56  (define @t98 () (@var "F" tptp.heap_E625070648t_unit))
% 48.28/48.56  (define @t99 () (_ @t11 @t98))
% 48.28/48.56  (define @t100 () (not (= @t9 @t67)))
% 48.28/48.56  (define @t101 () (@var "Getter" (-> tptp.rObjec1148923485tion_h tptp.n)))
% 48.28/48.56  (define @t102 () (_ (_ tptp.get_M_1932781581_j_k_l @t48) @t101))
% 48.28/48.56  (define @t103 () (_ (_ (_ tptp.heap_E1683112693tion_n @t102) @t2) @t1))
% 48.28/48.56  (define @t104 () (@var "Getter" (-> tptp.rObjec1922030987on_h_i tptp.n)))
% 48.28/48.56  (define @t105 () (@var "Node_ptr" tptp.node_p1234578834tr_b_c))
% 48.28/48.56  (define @t106 () (_ (_ (_ tptp.heap_E1683112693tion_n (_ (_ tptp.get_M_1644669866_j_k_l @t105) @t104)) @t2) @t1))
% 48.28/48.56  (define @t107 () (@var "Getter" (-> tptp.rObjec1875798643tion_g tptp.n)))
% 48.28/48.56  (define @t108 () (_ (_ tptp.get_M_90096148_j_k_l @t53) @t107))
% 48.28/48.56  (define @t109 () (_ (_ (_ tptp.heap_E1683112693tion_n @t108) @t2) @t1))
% 48.28/48.56  (define @t110 () (_ (_ tptp.get_M_544184404_h_i_l @t9) @t76))
% 48.28/48.56  (define @t111 () (_ (_ (_ tptp.heap_E1683112693tion_n @t110) @t2) @t1))
% 48.28/48.56  (define @t112 () (_ (_ tptp.get_M_1422421269_h_i_l @t9) @t66))
% 48.28/48.56  (define @t113 () (_ (_ (_ tptp.heap_E1683112692tion_m @t112) @t2) @t1))
% 48.28/48.56  (define @t114 () (_ tptp.cast_S988036065_b_j_k @t40))
% 48.28/48.56  (define @t115 () (_ tptp.cast_S988036065_b_j_k @t43))
% 48.28/48.56  (define @t116 () (@var "Character_data_ptr2" tptp.character_data_ptr_b))
% 48.28/48.56  (define @t117 () (=> @t50 (_ (_ (_ tptp.heap_E1683112693tion_n (_ (_ tptp.get_M_1932781581_j_k_l @t116) @t101)) @t2) @t1)))
% 48.28/48.56  (define @t118 () (@var "X2" tptp.rObjec1148923485tion_h))
% 48.28/48.56  (define @t119 () (_ (_ @t47 @t79) @t118))
% 48.28/48.56  (define @t120 () (@list @t118))
% 48.28/48.56  (define @t121 () (@var "Element_ptr2" tptp.element_ptr_a))
% 48.28/48.56  (define @t122 () (_ (_ (_ tptp.heap_E1683112693tion_n (_ (_ tptp.get_M_90096148_j_k_l @t121) @t107)) @t2) @t1))
% 48.28/48.56  (define @t123 () (=> @t55 @t122))
% 48.28/48.56  (define @t124 () (@var "X2" tptp.rObjec1875798643tion_g))
% 48.28/48.56  (define @t125 () (_ @t107 @t124))
% 48.28/48.56  (define @t126 () (_ (_ @t52 (lambda (@list (@var "Uu" tptp.option147517124_ptr_d)) @t51)) @t124))
% 48.28/48.56  (define @t127 () (@list @t124))
% 48.28/48.56  (define @t128 () (=> @t58 @t122))
% 48.28/48.56  (define @t129 () (_ (_ @t56 @t81) @t124))
% 48.28/48.56  (define @t130 () (=> @t61 @t122))
% 48.28/48.56  (define @t131 () (_ (_ @t59 @t79) @t124))
% 48.28/48.56  (define @t132 () (=> @t65 @t122))
% 48.28/48.56  (define @t133 () (_ (_ @t63 (lambda (@list (@var "Uu" tptp.finite1621822014t_char)) @t62)) @t124))
% 48.28/48.56  (define @t134 () (not (= @t53 @t121)))
% 48.28/48.56  (define @t135 () (@list @t2 @t1))
% 48.28/48.56  (define @t136 () (_ tptp.cast_C1209085999_d_g_i @t118))
% 48.28/48.56  (define @t137 () (_ tptp.cast_C1209085999_d_g_i @t119))
% 48.28/48.56  (define @t138 () (forall @t120 (= (_ @t104 @t137) (_ @t104 @t136))))
% 48.28/48.56  (define @t139 () (=> @t50 @t106))
% 48.28/48.56  (define @t140 () (_ tptp.cast_E1779426770on_h_i @t124))
% 48.28/48.56  (define @t141 () (_ @t104 @t140))
% 48.28/48.56  (define @t142 () (_ tptp.cast_E1779426770on_h_i @t126))
% 48.28/48.56  (define @t143 () (forall @t127 (= (_ @t104 @t142) @t141)))
% 48.28/48.56  (define @t144 () (_ tptp.cast_E1779426770on_h_i @t129))
% 48.28/48.56  (define @t145 () (forall @t127 (= (_ @t104 @t144) @t141)))
% 48.28/48.56  (define @t146 () (_ tptp.cast_E1779426770on_h_i @t131))
% 48.28/48.56  (define @t147 () (forall @t127 (= (_ @t104 @t146) @t141)))
% 48.28/48.56  (define @t148 () (_ tptp.cast_E1779426770on_h_i @t133))
% 48.28/48.56  (define @t149 () (forall @t127 (= (_ @t104 @t148) @t141)))
% 48.28/48.56  (define @t150 () (=> @t55 @t106))
% 48.28/48.56  (define @t151 () (=> @t58 @t106))
% 48.28/48.56  (define @t152 () (=> @t61 @t106))
% 48.28/48.56  (define @t153 () (=> @t65 @t106))
% 48.28/48.56  (define @t154 () (_ tptp.cast_c164415100_b_a_c @t48))
% 48.28/48.56  (define @t155 () (= @t154 @t105))
% 48.28/48.56  (define @t156 () (_ tptp.cast_e316309897tr_b_c @t53))
% 48.28/48.56  (define @t157 () (= @t156 @t105))
% 48.28/48.56  (define @t158 () (not @t157))
% 48.28/48.56  (define @t159 () (@var "X3" tptp.rObjec1617416918on_j_k))
% 48.28/48.56  (define @t160 () (@list @t159))
% 48.28/48.56  (define @t161 () (@var "Y" tptp.element_ptr_a))
% 48.28/48.56  (define @t162 () (@var "X" tptp.element_ptr_a))
% 48.28/48.56  (define @t163 () (@var "Y" tptp.character_data_ptr_b))
% 48.28/48.56  (define @t164 () (@var "X" tptp.character_data_ptr_b))
% 48.28/48.56  (define @t165 () (@var "V" tptp.docume1935157360tr_d_e))
% 48.28/48.56  (define @t166 () (@var "Getter" (-> tptp.rObjec2068690451tion_j tptp.docume1935157360tr_d_e)))
% 48.28/48.56  (define @t167 () (_ tptp.heap_E2101731758tr_d_e @t1))
% 48.28/48.56  (define @t168 () (lambda (@list (@var "Uu" tptp.docume1935157360tr_d_e)) @t165))
% 48.28/48.56  (define @t169 () (@var "Setter" (-> (-> tptp.docume1935157360tr_d_e tptp.docume1935157360tr_d_e) tptp.rObjec2068690451tion_j tptp.rObjec2068690451tion_j)))
% 48.28/48.56  (define @t170 () (@var "V" tptp.element_ptr_a))
% 48.28/48.56  (define @t171 () (@var "Getter" (-> tptp.rObjec2068690451tion_j tptp.element_ptr_a)))
% 48.28/48.56  (define @t172 () (_ tptp.heap_E1224694197_ptr_a @t1))
% 48.28/48.56  (define @t173 () (lambda (@list (@var "Uu" tptp.element_ptr_a)) @t170))
% 48.28/48.56  (define @t174 () (@var "Setter" (-> (-> tptp.element_ptr_a tptp.element_ptr_a) tptp.rObjec2068690451tion_j tptp.rObjec2068690451tion_j)))
% 48.28/48.56  (define @t175 () (@var "V" tptp.product_unit))
% 48.28/48.56  (define @t176 () (@var "Getter" (-> tptp.rObjec2068690451tion_j tptp.product_unit)))
% 48.28/48.56  (define @t177 () (_ tptp.heap_E667013711t_unit @t1))
% 48.28/48.56  (define @t178 () (lambda (@list (@var "Uu" tptp.product_unit)) @t175))
% 48.28/48.56  (define @t179 () (@var "Setter" (-> (-> tptp.product_unit tptp.product_unit) tptp.rObjec2068690451tion_j tptp.rObjec2068690451tion_j)))
% 48.28/48.56  (define @t180 () (@var "Getter" (-> tptp.rObjec2068690451tion_j tptp.m)))
% 48.28/48.56  (define @t181 () (_ tptp.heap_E1038710092tion_m @t1))
% 48.28/48.56  (define @t182 () (@var "Setter" (-> (-> tptp.m tptp.m) tptp.rObjec2068690451tion_j tptp.rObjec2068690451tion_j)))
% 48.28/48.56  (define @t183 () (_ tptp.heap_E1038710093tion_n @t1))
% 48.28/48.56  (define @t184 () (_ tptp.type_w1479951274_j_k_l @t2))
% 48.28/48.56  (define @t185 () (= @t184 (_ tptp.type_w1479951274_j_k_l @t1)))
% 48.28/48.56  (define @t186 () (@var "Y2" tptp.docume1935157360tr_d_e))
% 48.28/48.56  (define @t187 () (@var "Y" tptp.docume1935157360tr_d_e))
% 48.28/48.56  (define @t188 () (_ tptp.heap_E2101731758tr_d_e @t2))
% 48.28/48.56  (define @t189 () (_ @t188 @t95))
% 48.28/48.56  (define @t190 () (@var "Y2" tptp.element_ptr_a))
% 48.28/48.56  (define @t191 () (_ tptp.heap_E1224694197_ptr_a @t2))
% 48.28/48.56  (define @t192 () (_ @t191 @t92))
% 48.28/48.56  (define @t193 () (@var "Y2" tptp.product_unit))
% 48.28/48.56  (define @t194 () (@var "Y" tptp.product_unit))
% 48.28/48.56  (define @t195 () (_ (_ tptp.heap_E667013711t_unit @t2) @t98))
% 48.28/48.56  (define @t196 () (@var "Y2" tptp.n))
% 48.28/48.56  (define @t197 () (@var "Y" tptp.n))
% 48.28/48.56  (define @t198 () (@var "F" tptp.heap_E834686006tion_n))
% 48.28/48.56  (define @t199 () (_ (_ tptp.heap_E1038710093tion_n @t2) @t198))
% 48.28/48.56  (define @t200 () (@var "Y2" tptp.m))
% 48.28/48.56  (define @t201 () (@var "Y" tptp.m))
% 48.28/48.56  (define @t202 () (@var "F" tptp.heap_E826424501tion_m))
% 48.28/48.56  (define @t203 () (_ (_ tptp.heap_E1038710092tion_m @t2) @t202))
% 48.28/48.56  (define @t204 () (@var "Getter" (-> tptp.rObjec1875798643tion_g tptp.docume1935157360tr_d_e)))
% 48.28/48.56  (define @t205 () (@var "Setter" (-> (-> tptp.docume1935157360tr_d_e tptp.docume1935157360tr_d_e) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g)))
% 48.28/48.56  (define @t206 () (@var "Getter" (-> tptp.rObjec1875798643tion_g tptp.element_ptr_a)))
% 48.28/48.56  (define @t207 () (@var "Setter" (-> (-> tptp.element_ptr_a tptp.element_ptr_a) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g)))
% 48.28/48.56  (define @t208 () (@var "Getter" (-> tptp.rObjec1875798643tion_g tptp.product_unit)))
% 48.28/48.56  (define @t209 () (@var "Setter" (-> (-> tptp.product_unit tptp.product_unit) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g)))
% 48.28/48.56  (define @t210 () (@var "Getter" (-> tptp.rObjec1875798643tion_g tptp.m)))
% 48.28/48.56  (define @t211 () (@var "Setter" (-> (-> tptp.m tptp.m) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g)))
% 48.28/48.56  (define @t212 () (@var "Setter" (-> (-> tptp.n tptp.n) tptp.rObjec1875798643tion_g tptp.rObjec1875798643tion_g)))
% 48.28/48.56  (define @t213 () (@var "Getter" (-> tptp.rObjec1875798643tion_g tptp.option147517124_ptr_d)))
% 48.28/48.56  (define @t214 () (_ tptp.heap_E1947147782_ptr_d @t1))
% 48.28/48.56  (define @t215 () (@var "Getter" (-> tptp.rObjec1875798643tion_g tptp.list_n282880152tr_b_c)))
% 48.28/48.56  (define @t216 () (_ tptp.heap_E258692314tr_b_c @t1))
% 48.28/48.56  (define @t217 () (@var "Getter" (-> tptp.rObjec1875798643tion_g tptp.list_char)))
% 48.28/48.56  (define @t218 () (_ tptp.heap_E804379039t_char @t1))
% 48.28/48.56  (define @t219 () (@var "Getter" (-> tptp.rObjec1875798643tion_g tptp.finite1621822014t_char)))
% 48.28/48.56  (define @t220 () (_ tptp.heap_E946351744t_char @t1))
% 48.28/48.56  (define @t221 () (@var "Getter" (-> tptp.rObjec1148923485tion_h tptp.docume1935157360tr_d_e)))
% 48.28/48.56  (define @t222 () (@var "Setter" (-> (-> tptp.docume1935157360tr_d_e tptp.docume1935157360tr_d_e) tptp.rObjec1148923485tion_h tptp.rObjec1148923485tion_h)))
% 48.28/48.56  (define @t223 () (@var "Getter" (-> tptp.rObjec1148923485tion_h tptp.element_ptr_a)))
% 48.28/48.56  (define @t224 () (@var "Setter" (-> (-> tptp.element_ptr_a tptp.element_ptr_a) tptp.rObjec1148923485tion_h tptp.rObjec1148923485tion_h)))
% 48.28/48.56  (define @t225 () (@var "Getter" (-> tptp.rObjec1148923485tion_h tptp.product_unit)))
% 48.28/48.56  (define @t226 () (@var "Setter" (-> (-> tptp.product_unit tptp.product_unit) tptp.rObjec1148923485tion_h tptp.rObjec1148923485tion_h)))
% 48.28/48.56  (define @t227 () (@var "Getter" (-> tptp.rObjec1148923485tion_h tptp.m)))
% 48.28/48.56  (define @t228 () (@var "Setter" (-> (-> tptp.m tptp.m) tptp.rObjec1148923485tion_h tptp.rObjec1148923485tion_h)))
% 48.28/48.56  (define @t229 () (@var "Setter" (-> (-> tptp.n tptp.n) tptp.rObjec1148923485tion_h tptp.rObjec1148923485tion_h)))
% 48.28/48.56  (define @t230 () (@var "Getter" (-> tptp.rObjec1148923485tion_h tptp.list_char)))
% 48.28/48.56  (define @t231 () (@var "Getter" (-> tptp.rObjec1617416918on_j_k tptp.docume1935157360tr_d_e)))
% 48.28/48.56  (define @t232 () (@var "Setter" (-> (-> tptp.docume1935157360tr_d_e tptp.docume1935157360tr_d_e) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k)))
% 48.28/48.56  (define @t233 () (@var "Getter" (-> tptp.rObjec1617416918on_j_k tptp.element_ptr_a)))
% 48.28/48.56  (define @t234 () (@var "Setter" (-> (-> tptp.element_ptr_a tptp.element_ptr_a) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k)))
% 48.28/48.56  (define @t235 () (@var "Getter" (-> tptp.rObjec1617416918on_j_k tptp.product_unit)))
% 48.28/48.56  (define @t236 () (@var "Setter" (-> (-> tptp.product_unit tptp.product_unit) tptp.rObjec1617416918on_j_k tptp.rObjec1617416918on_j_k)))
% 48.28/48.56  (define @t237 () (@var "Getter" (-> tptp.rObjec1617416918on_j_k tptp.list_char)))
% 48.28/48.56  (define @t238 () (@var "Getter" (-> tptp.rObjec1617416918on_j_k tptp.list_n282880152tr_b_c)))
% 48.28/48.56  (define @t239 () (@var "Getter" (-> tptp.rObjec1617416918on_j_k tptp.option_element_ptr_a)))
% 48.28/48.56  (define @t240 () (_ tptp.heap_E1091541499_ptr_a @t1))
% 48.28/48.56  (define @t241 () (_ (_ @t11 (_ (_ @t49 tptp.val_update_option_h) @t7)) @t1))
% 48.28/48.56  (define @t242 () (@list @t2 @t48 @t7 @t1))
% 48.28/48.56  (define @t243 () (_ (_ @t11 (_ (_ @t54 tptp.shadow1606659473tion_g) @t51)) @t1))
% 48.28/48.56  (define @t244 () (@list @t2 @t53 @t51 @t1))
% 48.28/48.56  (define @t245 () (_ (_ @t11 (_ (_ @t57 tptp.child_1596411111tion_g) @t15)) @t1))
% 48.28/48.56  (define @t246 () (@list @t2 @t53 @t15 @t1))
% 48.28/48.56  (define @t247 () (_ (_ @t11 (_ (_ @t60 tptp.tag_na7058269tion_g) @t7)) @t1))
% 48.28/48.56  (define @t248 () (@list @t2 @t53 @t7 @t1))
% 48.28/48.56  (define @t249 () (_ (_ @t11 (_ (_ @t64 tptp.attrs_1280717024tion_g) @t62)) @t1))
% 48.28/48.56  (define @t250 () (@list @t2 @t53 @t62 @t1))
% 48.28/48.56  (define @t251 () (@list @t2))
% 48.28/48.56  (define @t252 () (@var "Document" tptp.rObjec1617416918on_j_k))
% 48.28/48.56  (define @t253 () (@var "Shadow_root" tptp.rObjec2068690451tion_j))
% 48.28/48.56  (define @t254 () (_ tptp.cast_D1046746849_b_j_k @t252))
% 48.28/48.56  (define @t255 () (@list @t252))
% 48.28/48.56  (define @t256 () (@var "Option2" tptp.option1029218147tion_j))
% 48.28/48.56  (define @t257 () (@var "Option" tptp.option1029218147tion_j))
% 48.28/48.56  (define @t258 () (_ tptp.the_RO2055010943tion_j @t257))
% 48.28/48.56  (define @t259 () (= @t256 tptp.none_R125524722tion_j))
% 48.28/48.56  (define @t260 () (= @t257 tptp.none_R125524722tion_j))
% 48.28/48.56  (define @t261 () (not @t260))
% 48.28/48.56  (define @t262 () (_ tptp.type_w1771507213_j_k_l @t2))
% 48.28/48.56  (define @t263 () (= @t262 (_ tptp.type_w1771507213_j_k_l @t1)))
% 48.28/48.56  (define @t264 () (_ tptp.type_w697503069_j_k_l @t2))
% 48.28/48.56  (define @t265 () (= @t264 (_ tptp.type_w697503069_j_k_l @t1)))
% 48.28/48.56  (define @t266 () (@var "Ptr2" tptp.node_p1234578834tr_b_c))
% 48.28/48.56  (define @t267 () (_ (_ (_ tptp.heap_E1683112693tion_n (_ (_ tptp.get_M_1644669866_j_k_l @t266) @t104)) @t2) @t1))
% 48.28/48.56  (define @t268 () (@var "New_ch844909330ta_ptr" tptp.character_data_ptr_b))
% 48.28/48.56  (define @t269 () (_ tptp.cast_c164415100_b_a_c @t268))
% 48.28/48.56  (define @t270 () (_ (_ (_ tptp.heap_E1554207190_ptr_b @t2) tptp.new_ch829669006_j_k_l) @t268))
% 48.28/48.56  (define @t271 () (_ (_ @t90 tptp.new_ch829669006_j_k_l) @t1))
% 48.28/48.56  (define @t272 () (@var "New_element_ptr" tptp.element_ptr_a))
% 48.28/48.56  (define @t273 () (_ tptp.cast_e316309897tr_b_c @t272))
% 48.28/48.56  (define @t274 () (_ (_ @t191 tptp.new_el717272935_j_k_l) @t272))
% 48.28/48.56  (define @t275 () (_ (_ @t93 tptp.new_el717272935_j_k_l) @t1))
% 48.28/48.56  (define @t276 () (@var "Ptr2" tptp.element_ptr_a))
% 48.28/48.56  (define @t277 () (_ (_ (_ tptp.heap_E1683112693tion_n (_ (_ tptp.get_M_90096148_j_k_l @t276) @t107)) @t2) @t1))
% 48.28/48.56  (define @t278 () (@var "Ptr2" tptp.character_data_ptr_b))
% 48.28/48.56  (define @t279 () (_ (_ (_ tptp.heap_E1683112693tion_n (_ (_ tptp.get_M_1932781581_j_k_l @t278) @t101)) @t2) @t1))
% 48.28/48.56  (define @t280 () (@var "Ptr2" tptp.docume1935157360tr_d_e))
% 48.28/48.56  (define @t281 () (_ (_ (_ tptp.heap_E1683112692tion_m (_ (_ tptp.get_M_1422421269_h_i_l @t280) @t66)) @t2) @t1))
% 48.28/48.56  (define @t282 () (@list @t2 @t1 @t280 @t66))
% 48.28/48.56  (define @t283 () (_ (_ (_ tptp.heap_E1683112693tion_n (_ (_ tptp.get_M_544184404_h_i_l @t280) @t76)) @t2) @t1))
% 48.28/48.56  (define @t284 () (@list @t2 @t1 @t280 @t76))
% 48.28/48.56  (define @t285 () (@list @t2 @t1 @t272))
% 48.28/48.56  (define @t286 () (@var "Type_wf2" (-> tptp.heap_S1465075775_j_k_l Bool)))
% 48.28/48.56  (define @t287 () (_ tptp.l_new_410495338_j_k_l @t286))
% 48.28/48.56  (define @t288 () (@var "H7" tptp.heap_S1465075775_j_k_l))
% 48.28/48.56  (define @t289 () (@var "H6" tptp.heap_S1465075775_j_k_l))
% 48.28/48.56  (define @t290 () (= (_ @t286 @t289) (_ @t286 @t288)))
% 48.28/48.56  (define @t291 () (@list @t289 @t288))
% 48.28/48.56  (define @t292 () (@list @t286))
% 48.28/48.56  (define @t293 () (= (_ @t286 @t2) (_ @t286 @t1)))
% 48.28/48.56  (define @t294 () (@list @t286 @t2 @t1))
% 48.28/48.56  (define @t295 () (@var "R3" tptp.rObjec1875798643tion_g))
% 48.28/48.56  (define @t296 () (@var "F3" (-> tptp.option147517124_ptr_d tptp.option147517124_ptr_d)))
% 48.28/48.56  (define @t297 () (@var "R2" tptp.rObjec1875798643tion_g))
% 48.28/48.56  (define @t298 () (@var "F" (-> tptp.option147517124_ptr_d tptp.option147517124_ptr_d)))
% 48.28/48.56  (define @t299 () (= (_ (_ tptp.shadow1606659473tion_g @t298) @t297) (_ (_ tptp.shadow1606659473tion_g @t296) @t295)))
% 48.28/48.56  (define @t300 () (@var "V3" tptp.option147517124_ptr_d))
% 48.28/48.56  (define @t301 () (= (_ @t298 @t300) (_ @t296 @t300)))
% 48.28/48.56  (define @t302 () (@var "V2" tptp.option147517124_ptr_d))
% 48.28/48.56  (define @t303 () (@list @t300))
% 48.28/48.56  (define @t304 () (= (_ tptp.shadow1820683706tion_g @t295) @t302))
% 48.28/48.56  (define @t305 () (= @t297 @t295))
% 48.28/48.56  (define @t306 () (@list @t297 @t295 @t302 @t298 @t296))
% 48.28/48.56  (define @t307 () (_ tptp.l_new_540233301_j_k_l @t286))
% 48.28/48.56  (define @t308 () (@var "R3" tptp.rObjec1617416918on_j_k))
% 48.28/48.56  (define @t309 () (@var "F3" (-> tptp.list_char tptp.list_char)))
% 48.28/48.56  (define @t310 () (@var "R2" tptp.rObjec1617416918on_j_k))
% 48.28/48.56  (define @t311 () (@var "F" (-> tptp.list_char tptp.list_char)))
% 48.28/48.56  (define @t312 () (= (_ (_ tptp.doctyp68000440on_j_k @t311) @t310) (_ (_ tptp.doctyp68000440on_j_k @t309) @t308)))
% 48.28/48.56  (define @t313 () (@var "V3" tptp.list_char))
% 48.28/48.56  (define @t314 () (= (_ @t311 @t313) (_ @t309 @t313)))
% 48.28/48.56  (define @t315 () (@var "V2" tptp.list_char))
% 48.28/48.56  (define @t316 () (@list @t313))
% 48.28/48.56  (define @t317 () (forall @t316 (=> (= @t313 @t315) @t314)))
% 48.28/48.56  (define @t318 () (= (_ tptp.doctyp814403297on_j_k @t308) @t315))
% 48.28/48.56  (define @t319 () (= @t310 @t308))
% 48.28/48.56  (define @t320 () (@list @t310 @t308 @t315 @t311 @t309))
% 48.28/48.56  (define @t321 () (@var "F3" (-> tptp.option_element_ptr_a tptp.option_element_ptr_a)))
% 48.28/48.56  (define @t322 () (@var "F" (-> tptp.option_element_ptr_a tptp.option_element_ptr_a)))
% 48.28/48.56  (define @t323 () (= (_ (_ tptp.docume244715269on_j_k @t322) @t310) (_ (_ tptp.docume244715269on_j_k @t321) @t308)))
% 48.28/48.56  (define @t324 () (@var "V3" tptp.option_element_ptr_a))
% 48.28/48.56  (define @t325 () (= (_ @t322 @t324) (_ @t321 @t324)))
% 48.28/48.56  (define @t326 () (@var "V2" tptp.option_element_ptr_a))
% 48.28/48.56  (define @t327 () (@list @t324))
% 48.28/48.56  (define @t328 () (= (_ tptp.docume1175131570on_j_k @t308) @t326))
% 48.28/48.56  (define @t329 () (@list @t310 @t308 @t326 @t322 @t321))
% 48.28/48.56  (define @t330 () (forall @t316 (=> (= @t315 @t313) @t314)))
% 48.28/48.56  (define @t331 () (@var "R3" tptp.rObjec1148923485tion_h))
% 48.28/48.56  (define @t332 () (@var "R2" tptp.rObjec1148923485tion_h))
% 48.28/48.56  (define @t333 () (= (_ (_ tptp.val_update_option_h @t311) @t332) (_ (_ tptp.val_update_option_h @t309) @t331)))
% 48.28/48.56  (define @t334 () (= (_ tptp.val_option_h @t331) @t315))
% 48.28/48.56  (define @t335 () (= @t332 @t331))
% 48.28/48.56  (define @t336 () (@list @t332 @t331 @t315 @t311 @t309))
% 48.28/48.56  (define @t337 () (@var "F3" (-> tptp.list_n282880152tr_b_c tptp.list_n282880152tr_b_c)))
% 48.28/48.56  (define @t338 () (@var "F" (-> tptp.list_n282880152tr_b_c tptp.list_n282880152tr_b_c)))
% 48.28/48.56  (define @t339 () (= (_ (_ tptp.discon442323090on_j_k @t338) @t310) (_ (_ tptp.discon442323090on_j_k @t337) @t308)))
% 48.28/48.56  (define @t340 () (@var "V3" tptp.list_n282880152tr_b_c))
% 48.28/48.56  (define @t341 () (= (_ @t338 @t340) (_ @t337 @t340)))
% 48.28/48.56  (define @t342 () (@var "V2" tptp.list_n282880152tr_b_c))
% 48.28/48.56  (define @t343 () (@list @t340))
% 48.28/48.56  (define @t344 () (forall @t343 (=> (= @t342 @t340) @t341)))
% 48.28/48.56  (define @t345 () (= (_ tptp.discon866287741on_j_k @t308) @t342))
% 48.28/48.56  (define @t346 () (@list @t310 @t308 @t342 @t338 @t337))
% 48.28/48.56  (define @t347 () (forall @t343 (=> (= @t340 @t342) @t341)))
% 48.28/48.56  (define @t348 () (@var "Getter" (-> tptp.rObjec1413572695_j_k_l tptp.n)))
% 48.28/48.56  (define @t349 () (@var "Ptr2" tptp.object945351580_d_e_f))
% 48.28/48.56  (define @t350 () (_ (_ (_ tptp.heap_E1683112693tion_n (_ (_ tptp.get_M_421785767_k_l_n @t349) @t348)) @t2) @t1))
% 48.28/48.56  (define @t351 () (@var "F3" (-> tptp.finite1621822014t_char tptp.finite1621822014t_char)))
% 48.28/48.56  (define @t352 () (@var "F" (-> tptp.finite1621822014t_char tptp.finite1621822014t_char)))
% 48.28/48.56  (define @t353 () (= (_ (_ tptp.attrs_1280717024tion_g @t352) @t297) (_ (_ tptp.attrs_1280717024tion_g @t351) @t295)))
% 48.28/48.56  (define @t354 () (@var "V3" tptp.finite1621822014t_char))
% 48.28/48.56  (define @t355 () (= (_ @t352 @t354) (_ @t351 @t354)))
% 48.28/48.56  (define @t356 () (@var "V2" tptp.finite1621822014t_char))
% 48.28/48.56  (define @t357 () (@list @t354))
% 48.28/48.56  (define @t358 () (= (_ tptp.attrs_1151927177tion_g @t295) @t356))
% 48.28/48.56  (define @t359 () (@list @t297 @t295 @t356 @t352 @t351))
% 48.28/48.56  (define @t360 () (= (_ (_ tptp.child_1596411111tion_g @t338) @t297) (_ (_ tptp.child_1596411111tion_g @t337) @t295)))
% 48.28/48.56  (define @t361 () (= (_ tptp.child_768225874tion_g @t295) @t342))
% 48.28/48.56  (define @t362 () (@list @t297 @t295 @t342 @t338 @t337))
% 48.28/48.56  (define @t363 () (@var "Object_ptr" tptp.object945351580_d_e_f))
% 48.28/48.56  (define @t364 () (_ (_ (_ tptp.heap_E1683112693tion_n (_ (_ tptp.get_M_421785767_k_l_n @t363) @t348)) @t2) @t1))
% 48.28/48.56  (define @t365 () (=> @t50 @t364))
% 48.28/48.56  (define @t366 () (=> @t55 @t364))
% 48.28/48.56  (define @t367 () (not (= (_ tptp.cast_n552817316_d_e_f @t156) @t363)))
% 48.28/48.56  (define @t368 () (=> @t58 @t364))
% 48.28/48.56  (define @t369 () (=> @t61 @t364))
% 48.28/48.56  (define @t370 () (=> @t65 @t364))
% 48.28/48.56  (define @t371 () (_ @t348 (_ tptp.cast_N1183075319_j_k_l @t140)))
% 48.28/48.56  (define @t372 () (forall @t127 (= (_ @t348 (_ tptp.cast_N1183075319_j_k_l @t142)) @t371)))
% 48.28/48.56  (define @t373 () (forall @t127 (= (_ @t348 (_ tptp.cast_N1183075319_j_k_l @t144)) @t371)))
% 48.28/48.56  (define @t374 () (forall @t127 (= (_ @t348 (_ tptp.cast_N1183075319_j_k_l @t146)) @t371)))
% 48.28/48.56  (define @t375 () (forall @t127 (= (_ @t348 (_ tptp.cast_N1183075319_j_k_l @t148)) @t371)))
% 48.28/48.56  (define @t376 () (= (_ (_ tptp.tag_na7058269tion_g @t311) @t297) (_ (_ tptp.tag_na7058269tion_g @t309) @t295)))
% 48.28/48.56  (define @t377 () (= (_ tptp.tag_na866435078tion_g @t295) @t315))
% 48.28/48.56  (define @t378 () (@list @t297 @t295 @t315 @t311 @t309))
% 48.28/48.56  (define @t379 () (forall @t120 (= (_ @t348 (_ tptp.cast_N1183075319_j_k_l @t137)) (_ @t348 (_ tptp.cast_N1183075319_j_k_l @t136)))))
% 48.28/48.56  (define @t380 () (@var "Y" tptp.rObjec1617416918on_j_k))
% 48.28/48.56  (define @t381 () (@var "X" tptp.rObjec1617416918on_j_k))
% 48.28/48.56  (define @t382 () (_ tptp.cast_D1252964113_h_i_l @t252))
% 48.28/48.56  (define @t383 () (@var "Node" tptp.rObjec1922030987on_h_i))
% 48.28/48.56  (define @t384 () (_ tptp.cast_N1183075319_j_k_l @t383))
% 48.28/48.56  (define @t385 () (=> @t12 @t364))
% 48.28/48.56  (define @t386 () (_ @t348 (_ tptp.cast_D1252964113_h_i_l @t69)))
% 48.28/48.56  (define @t387 () (forall @t75 (= (_ @t348 (_ tptp.cast_D1252964113_h_i_l @t80)) @t386)))
% 48.28/48.56  (define @t388 () (=> @t18 @t364))
% 48.28/48.56  (define @t389 () (forall @t75 (= (_ @t348 (_ tptp.cast_D1252964113_h_i_l @t82)) @t386)))
% 48.28/48.56  (define @t390 () (=> @t22 @t364))
% 48.28/48.56  (define @t391 () (forall @t75 (= (_ @t348 (_ tptp.cast_D1252964113_h_i_l @t84)) @t386)))
% 48.28/48.56  (define @t392 () (=> @t25 @t364))
% 48.28/48.56  (define @t393 () (forall @t75 (= (_ @t348 (_ tptp.cast_D1252964113_h_i_l @t85)) @t386)))
% 48.28/48.56  (define @t394 () (=> @t29 @t364))
% 48.28/48.56  (define @t395 () (forall @t75 (= (_ @t348 (_ tptp.cast_D1252964113_h_i_l @t73)) @t386)))
% 48.28/48.56  (define @t396 () (_ tptp.cast_d1608273229_b_c_f @t9))
% 48.28/48.56  (define @t397 () (not (= @t396 @t363)))
% 48.28/48.56  (define @t398 () (@var "New_document_ptr" tptp.docume1935157360tr_d_e))
% 48.28/48.56  (define @t399 () (_ (_ @t188 tptp.new_do4779043_j_k_l) @t398))
% 48.28/48.56  (define @t400 () (_ (_ @t96 tptp.new_do4779043_j_k_l) @t1))
% 48.28/48.56  (define @t401 () (@var "Obj" tptp.rObjec1413572695_j_k_l))
% 48.28/48.56  (define @t402 () (@var "Document2" tptp.rObjec1617416918on_j_k))
% 48.28/48.56  (define @t403 () (_ tptp.cast_D1252964113_h_i_l @t402))
% 48.28/48.56  (define @t404 () (_ tptp.cast_O1034441233_j_k_l @t401))
% 48.28/48.56  (define @t405 () (@list @t2 @t1 @t398))
% 48.28/48.56  (define @t406 () (not (= @t280 @t398)))
% 48.28/48.56  (define @t407 () (_ tptp.l_new_1474790279_j_k_l @t286))
% 48.28/48.56  (define @t408 () (@var "Shadow_root2" tptp.rObjec2068690451tion_j))
% 48.28/48.56  (define @t409 () (_ tptp.cast_S988036065_b_j_k @t408))
% 48.28/48.56  (define @t410 () (_ tptp.some_R700141678tion_j @t408))
% 48.28/48.56  (define @t411 () (@var "X" tptp.option1029218147tion_j))
% 48.28/48.56  (define @t412 () (= @t411 tptp.none_R125524722tion_j))
% 48.28/48.56  (define @t413 () (@var "Y3" tptp.rObjec2068690451tion_j))
% 48.28/48.56  (define @t414 () (= @t411 (_ tptp.some_R700141678tion_j @t413)))
% 48.28/48.56  (define @t415 () (@list @t413))
% 48.28/48.56  (define @t416 () (@list @t411))
% 48.28/48.56  (define @t417 () (_ tptp.some_R700141678tion_j @t258))
% 48.28/48.56  (define @t418 () (@list @t257))
% 48.28/48.56  (define @t419 () (@var "X22" tptp.rObjec2068690451tion_j))
% 48.28/48.56  (define @t420 () (_ tptp.some_R700141678tion_j @t419))
% 48.28/48.56  (define @t421 () (@list @t419))
% 48.28/48.56  (define @t422 () (@var "X23" tptp.rObjec2068690451tion_j))
% 48.28/48.56  (define @t423 () (@var "Y" tptp.option1029218147tion_j))
% 48.28/48.56  (define @t424 () (= @t423 tptp.none_R125524722tion_j))
% 48.28/48.56  (define @t425 () (@var "P2" (-> tptp.option1029218147tion_j Bool)))
% 48.28/48.56  (define @t426 () (@var "X3" tptp.rObjec2068690451tion_j))
% 48.28/48.56  (define @t427 () (@var "P4" (-> tptp.option1029218147tion_j Bool)))
% 48.28/48.56  (define @t428 () (_ @t427 (_ tptp.some_R700141678tion_j @t426)))
% 48.28/48.56  (define @t429 () (@list @t426))
% 48.28/48.56  (define @t430 () (_ @t427 tptp.none_R125524722tion_j))
% 48.28/48.56  (define @t431 () (@list @t427))
% 48.28/48.56  (define @t432 () (@var "X4" tptp.option1029218147tion_j))
% 48.28/48.56  (define @t433 () (@var "P3" (-> tptp.option1029218147tion_j Bool)))
% 48.28/48.56  (define @t434 () (_ @t433 @t432))
% 48.28/48.56  (define @t435 () (@list @t432))
% 48.28/48.56  (define @t436 () (@list @t433))
% 48.28/48.56  (define @t437 () (@var "P2" (-> tptp.option1029218147tion_j tptp.option1029218147tion_j Bool)))
% 48.28/48.56  (define @t438 () (_ (_ @t437 @t411) @t423))
% 48.28/48.56  (define @t439 () (@var "B" tptp.rObjec2068690451tion_j))
% 48.28/48.56  (define @t440 () (@var "A" tptp.rObjec2068690451tion_j))
% 48.28/48.56  (define @t441 () (_ tptp.some_R67702331on_j_k @t252))
% 48.28/48.56  (define @t442 () (@list (@var "Uu" tptp.rObjec2068690451tion_j)))
% 48.28/48.56  (define @t443 () (@var "Y4" tptp.rObjec2068690451tion_j))
% 48.28/48.56  (define @t444 () (@var "Q" (-> tptp.rObjec2068690451tion_j Bool)))
% 48.28/48.56  (define @t445 () (@var "P2" Bool))
% 48.28/48.56  (define @t446 () (_ tptp.some_element_ptr_a @t53))
% 48.28/48.56  (define @t447 () (@list @t53))
% 48.28/48.56  (define @t448 () (_ tptp.cast_n269450313tr_b_c @t105))
% 48.28/48.56  (define @t449 () (_ tptp.is_ele1259807012tr_b_c @t105))
% 48.28/48.56  (define @t450 () (@list @t105))
% 48.28/48.56  (define @t451 () (@list @t48))
% 48.28/48.56  (define @t452 () (@var "Element_ptr3" tptp.element_ptr_a))
% 48.28/48.56  (define @t453 () (_ (_ (_ tptp.put_O_834343516_j_k_l @t349) @t401) @t2))
% 48.28/48.56  (define @t454 () (_ tptp.type_w1771507213_j_k_l @t453))
% 48.28/48.56  (define @t455 () (@list @t2 @t349 @t401))
% 48.28/48.56  (define @t456 () (_ tptp.cast_O1705702135_j_k_l @t401))
% 48.28/48.56  (define @t457 () (_ tptp.cast_o664948310_d_e_f @t349))
% 48.28/48.56  (define @t458 () (_ tptp.case_o876177157tr_b_c false))
% 48.28/48.56  (define @t459 () (_ tptp.type_w697503069_j_k_l @t453))
% 48.28/48.56  (define @t460 () (@var "Character_data_ptr3" tptp.character_data_ptr_b))
% 48.28/48.56  (define @t461 () (_ tptp.is_cha330921893_a_b_c @t105))
% 48.28/48.56  (define @t462 () (_ tptp.type_w2078707819_j_k_l @t2))
% 48.28/48.56  (define @t463 () (_ tptp.get_E_312738192_j_k_l @t53))
% 48.28/48.56  (define @t464 () (@var "F" tptp.rObjec1617416918on_j_k))
% 48.28/48.56  (define @t465 () (_ tptp.put_D_2126422573_h_i_l @t9))
% 48.28/48.56  (define @t466 () (_ (_ @t465 @t464) @t2))
% 48.28/48.56  (define @t467 () (_ tptp.get_C_592656865_j_k_l @t48))
% 48.28/48.56  (define @t468 () (_ tptp.get_D_1192261494_j_k_l @t9))
% 48.28/48.56  (define @t469 () (_ @t468 @t2))
% 48.28/48.56  (define @t470 () (_ @t468 @t453))
% 48.28/48.56  (define @t471 () (= @t349 @t396))
% 48.28/48.56  (define @t472 () (@var "F" tptp.rObjec1148923485tion_h))
% 48.28/48.56  (define @t473 () (@var "F" tptp.rObjec1875798643tion_g))
% 48.28/48.56  (define @t474 () (_ tptp.l_put_1129034844_j_k_m tptp.get_D_1192261494_j_k_l))
% 48.28/48.56  (define @t475 () (= tptp.put_M_674497586_h_i_l (_ @t474 tptp.put_D_2126422573_h_i_l)))
% 48.28/48.56  (define @t476 () (_ tptp.cast_n1518532508_a_b_c @t105))
% 48.28/48.56  (define @t477 () (_ tptp.some_c586507257_ptr_b @t48))
% 48.28/48.56  (define @t478 () (_ tptp.heap_E494191872t_unit tptp.h))
% 48.28/48.56  (define @t479 () (@var "X5" tptp.rObjec1617416918on_j_k))
% 48.28/48.56  (define @t480 () (_ tptp.setter (lambda @t71 tptp.v)))
% 48.28/48.56  (define @t481 () (@var "X5" tptp.rObjec2068690451tion_j))
% 48.28/48.56  (define @t482 () (_ tptp.cast_s253715760_r_d_e tptp.shadow_root_ptr))
% 48.28/48.56  (define @t483 () (not (= @t482 tptp.document_ptr)))
% 48.28/48.56  (define @t484 () (_ (_ tptp.shadow569799008_i_k_l tptp.shadow_root_ptr) tptp.getter))
% 48.28/48.56  (define @t485 () (not (_ (_ (_ tptp.heap_E1683112693tion_n @t484) tptp.h) tptp.h2)))
% 48.28/48.56  (define @t486 () (@var "X3" tptp.docume1935157360tr_d_e))
% 48.28/48.56  (define @t487 () (@var "F2" tptp.heap_E1188946203tr_d_e))
% 48.28/48.56  (define @t488 () (@var "H5" tptp.heap_S1465075775_j_k_l))
% 48.28/48.56  (define @t489 () (@var "H4" tptp.heap_S1465075775_j_k_l))
% 48.28/48.56  (define @t490 () (_ tptp.heap_E2101731758tr_d_e @t489))
% 48.28/48.56  (define @t491 () (lambda (@list @t487 @t489 @t488) (forall (@list @t486) (= (_ (_ @t490 @t487) @t486) (_ (_ (_ tptp.heap_E2101731758tr_d_e @t488) @t487) @t486)))))
% 48.28/48.56  (define @t492 () (@var "X3" tptp.element_ptr_a))
% 48.28/48.56  (define @t493 () (@var "F2" tptp.heap_E1661210526_ptr_a))
% 48.28/48.56  (define @t494 () (_ tptp.heap_E1224694197_ptr_a @t489))
% 48.28/48.56  (define @t495 () (lambda (@list @t493 @t489 @t488) (forall (@list @t492) (= (_ (_ @t494 @t493) @t492) (_ (_ (_ tptp.heap_E1224694197_ptr_a @t488) @t493) @t492)))))
% 48.28/48.56  (define @t496 () (@var "X3" tptp.product_unit))
% 48.28/48.56  (define @t497 () (@var "F2" tptp.heap_E625070648t_unit))
% 48.28/48.56  (define @t498 () (_ tptp.heap_E667013711t_unit @t489))
% 48.28/48.56  (define @t499 () (lambda (@list @t497 @t489 @t488) (forall (@list @t496) (= (_ (_ @t498 @t497) @t496) (_ (_ (_ tptp.heap_E667013711t_unit @t488) @t497) @t496)))))
% 48.28/48.56  (define @t500 () (@var "X3" tptp.m))
% 48.28/48.56  (define @t501 () (@var "F2" tptp.heap_E826424501tion_m))
% 48.28/48.56  (define @t502 () (_ tptp.heap_E1038710092tion_m @t489))
% 48.28/48.56  (define @t503 () (lambda (@list @t501 @t489 @t488) (forall (@list @t500) (= (_ (_ @t502 @t501) @t500) (_ (_ (_ tptp.heap_E1038710092tion_m @t488) @t501) @t500)))))
% 48.28/48.56  (define @t504 () (@var "X3" tptp.n))
% 48.28/48.56  (define @t505 () (@var "F2" tptp.heap_E834686006tion_n))
% 48.28/48.56  (define @t506 () (_ (_ (_ tptp.heap_E1038710093tion_n @t488) @t505) @t504))
% 48.28/48.56  (define @t507 () (_ tptp.heap_E1038710093tion_n @t489))
% 48.28/48.56  (define @t508 () (_ (_ @t507 @t505) @t504))
% 48.28/48.56  (define @t509 () (= @t508 @t506))
% 48.28/48.56  (define @t510 () (@list @t504))
% 48.28/48.56  (define @t511 () (forall @t510 @t509))
% 48.28/48.56  (define @t512 () (@list @t505 @t489 @t488))
% 48.28/48.56  (define @t513 () (lambda @t512 @t511))
% 48.28/48.56  (define @t514 () (@var "P" tptp.heap_E1996099391_ptr_b))
% 48.28/48.56  (define @t515 () (_ tptp.heap_E1982034951_ptr_b @t489))
% 48.28/48.56  (define @t516 () (@var "R" tptp.character_data_ptr_b))
% 48.28/48.56  (define @t517 () (lambda (@list @t489 @t514 @t516 @t488) (and (_ (_ (_ tptp.heap_E1554207190_ptr_b @t489) @t514) @t516) (_ (_ @t515 @t514) @t488))))
% 48.28/48.56  (define @t518 () (@var "P" tptp.heap_E1188946203tr_d_e))
% 48.28/48.56  (define @t519 () (_ tptp.heap_E2046843837tr_d_e @t489))
% 48.28/48.56  (define @t520 () (@var "R" tptp.docume1935157360tr_d_e))
% 48.28/48.56  (define @t521 () (lambda (@list @t489 @t518 @t520 @t488) (and (_ (_ @t490 @t518) @t520) (_ (_ @t519 @t518) @t488))))
% 48.28/48.56  (define @t522 () (@var "P" tptp.heap_E1661210526_ptr_a))
% 48.28/48.56  (define @t523 () (_ tptp.heap_E24690662_ptr_a @t489))
% 48.28/48.56  (define @t524 () (@var "R" tptp.element_ptr_a))
% 48.28/48.56  (define @t525 () (lambda (@list @t489 @t522 @t524 @t488) (and (_ (_ @t494 @t522) @t524) (_ (_ @t523 @t522) @t488))))
% 48.28/48.56  (define @t526 () (@var "P" tptp.heap_E834686006tion_n))
% 48.28/48.56  (define @t527 () (@var "R" tptp.n))
% 48.28/48.56  (define @t528 () (lambda (@list @t489 @t526 @t527 @t488) (and (_ (_ @t507 @t526) @t527) (_ (_ (_ tptp.heap_E1553005822tion_n @t489) @t526) @t488))))
% 48.28/48.56  (define @t529 () (@var "P" tptp.heap_E826424501tion_m))
% 48.28/48.56  (define @t530 () (@var "R" tptp.m))
% 48.28/48.56  (define @t531 () (lambda (@list @t489 @t529 @t530 @t488) (and (_ (_ @t502 @t529) @t530) (_ (_ (_ tptp.heap_E1553005821tion_m @t489) @t529) @t488))))
% 48.28/48.56  (define @t532 () (@var "P" tptp.heap_E625070648t_unit))
% 48.28/48.56  (define @t533 () (@var "R" tptp.product_unit))
% 48.28/48.56  (define @t534 () (lambda (@list @t489 @t532 @t533 @t488) (and (_ (_ @t498 @t532) @t533) (_ (_ (_ tptp.heap_E494191872t_unit @t489) @t532) @t488))))
% 48.28/48.56  (define @t535 () (@var "Ptr" tptp.rObjec1617416918on_j_k))
% 48.28/48.56  (define @t536 () (lambda (@list @t535) (not (= (_ tptp.cast_D1046746849_b_j_k @t535) tptp.none_R125524722tion_j))))
% 48.28/48.56  (define @t537 () (@var "Type_wf" (-> tptp.heap_S1465075775_j_k_l Bool)))
% 48.28/48.56  (define @t538 () (= (_ @t537 @t489) (_ @t537 @t488)))
% 48.28/48.56  (define @t539 () (@list @t489 @t488))
% 48.28/48.56  (define @t540 () (@list @t537))
% 48.28/48.56  (define @t541 () (lambda @t540 (forall @t539 (=> (_ (_ @t515 tptp.new_ch829669006_j_k_l) @t488) @t538))))
% 48.28/48.56  (define @t542 () (lambda @t540 (forall @t539 (=> (_ (_ @t523 tptp.new_el717272935_j_k_l) @t488) @t538))))
% 48.28/48.56  (define @t543 () (lambda @t540 (forall @t539 (=> (_ (_ @t519 tptp.new_do4779043_j_k_l) @t488) @t538))))
% 48.28/48.56  (define @t544 () (@var "__flatten_var_0" tptp.heap_S1465075775_j_k_l))
% 48.28/48.56  (define @t545 () (@var "Document_ptr3" tptp.docume1935157360tr_d_e))
% 48.28/48.56  (define @t546 () (_ tptp.cast_d1608273229_b_c_f @t545))
% 48.28/48.56  (define @t547 () (_ (_ (_ tptp.put_O_834343516_j_k_l @t546) @t403) @t544))
% 48.28/48.56  (define @t548 () (@list @t545 @t402 @t544))
% 48.28/48.56  (define @t549 () (lambda @t548 @t547))
% 48.28/48.56  (define @t550 () (@var "BOUND_VARIABLE_10934" tptp.n))
% 48.28/48.56  (define @t551 () (tptp.shadow569799008_i_k_l @t4 @t3))
% 48.28/48.56  (define @t552 () (= (tptp.heap_E1038710093tion_n @t2 @t551 @t550) (tptp.heap_E1038710093tion_n @t1 @t551 @t550)))
% 48.28/48.56  (define @t553 () (tptp.cast_D1252964113_h_i_l @t402))
% 48.28/48.56  (define @t554 () (tptp.cast_d1608273229_b_c_f @t545))
% 48.28/48.56  (define @t555 () (tptp.put_O_834343516_j_k_l @t554 @t553 @t544))
% 48.28/48.56  (define @t556 () (lambda @t548 @t555))
% 48.28/48.56  (define @t557 () (tptp.l_put_1129034844_j_k_m tptp.get_D_1192261494_j_k_l @t556 @t9 @t27 @t26))
% 48.28/48.56  (define @t558 () (_ @t474 @t549))
% 48.28/48.56  (define @t559 () (_ (_ (_ @t558 @t9) @t27) @t26))
% 48.28/48.56  (define @t560 () (tptp.heap_E494191872t_unit @t2 @t559 @t1))
% 48.28/48.56  (define @t561 () (not @t560))
% 48.28/48.56  (define @t562 () (tptp.cast_s253715760_r_d_e @t4))
% 48.28/48.56  (define @t563 () (= @t9 @t562))
% 48.28/48.56  (define @t564 () (or @t563 @t561 @t552))
% 48.28/48.56  (define @t565 () (@list @t4 @t9 @t2 @t27 @t26 @t1 @t3 @t550))
% 48.28/48.56  (define @t566 () (_ @t558 @t9 @t27 @t26))
% 48.28/48.56  (define @t567 () (tptp.heap_E494191872t_unit @t2 @t566 @t1))
% 48.28/48.56  (define @t568 () (not @t567))
% 48.28/48.56  (define @t569 () (or @t563 @t568 @t552))
% 48.28/48.56  (define @t570 () (tptp.put_M_674497586_h_i_l @t9 @t27 @t26))
% 48.28/48.56  (define @t571 () (tptp.heap_E494191872t_unit @t2 @t570 @t1))
% 48.28/48.56  (define @t572 () (not @t571))
% 48.28/48.56  (define @t573 () (or @t563 @t572 @t552))
% 48.28/48.56  (define @t574 () (forall @t565 @t573))
% 48.28/48.56  (define @t575 () (@list @t550))
% 48.28/48.56  (define @t576 () (forall @t575 @t573))
% 48.28/48.56  (define @t577 () (forall @t575 @t552))
% 48.28/48.56  (define @t578 () (or @t563 @t572 @t577))
% 48.28/48.56  (define @t579 () (tptp.heap_E1038710093tion_n @t1 @t551 @t504))
% 48.28/48.56  (define @t580 () (tptp.heap_E1038710093tion_n @t2 @t551 @t504))
% 48.28/48.56  (define @t581 () (forall @t510 (= @t580 @t579)))
% 48.28/48.56  (define @t582 () (not @t29))
% 48.28/48.56  (define @t583 () (= @t9 @t13))
% 48.28/48.56  (define @t584 () (or @t583 @t582 @t581))
% 48.28/48.56  (define @t585 () (=> @t29 @t581))
% 48.28/48.56  (define @t586 () (not @t583))
% 48.28/48.56  (define @t587 () (forall @t510 (= @t579 @t580)))
% 48.28/48.56  (define @t588 () (tptp.heap_E1038710093tion_n @t488 @t551 @t504))
% 48.28/48.56  (define @t589 () (@list @t488))
% 48.28/48.56  (define @t590 () (forall @t510 (= @t580 @t588)))
% 48.28/48.56  (define @t591 () (lambda @t589 @t590))
% 48.28/48.56  (define @t592 () (tptp.heap_E1038710093tion_n @t488 @t5 @t504))
% 48.28/48.56  (define @t593 () (tptp.heap_E1038710093tion_n @t489 @t5 @t504))
% 48.28/48.56  (define @t594 () (= @t593 @t592))
% 48.28/48.56  (define @t595 () (forall @t510 @t594))
% 48.28/48.56  (define @t596 () (lambda @t539 @t595))
% 48.28/48.56  (define @t597 () (tptp.heap_E1038710093tion_n @t488 @t505 @t504))
% 48.28/48.56  (define @t598 () (tptp.heap_E1038710093tion_n @t489 @t505 @t504))
% 48.28/48.56  (define @t599 () (lambda @t512 (forall @t510 (= @t598 @t597))))
% 48.28/48.56  (define @t600 () (_ @t599 @t5))
% 48.28/48.56  (define @t601 () (=> @t29 (_ (_ @t600 @t2) @t1)))
% 48.28/48.56  (define @t602 () (=> @t14 @t601))
% 48.28/48.56  (define @t603 () (tptp.shadow569799008_i_k_l tptp.shadow_root_ptr tptp.getter))
% 48.28/48.56  (define @t604 () (tptp.heap_E1038710093tion_n tptp.h2 @t603 @t504))
% 48.28/48.56  (define @t605 () (tptp.heap_E1038710093tion_n tptp.h @t603 @t504))
% 48.28/48.56  (define @t606 () (@quantifiers_skolemize (forall @t510 (= @t605 @t604)) 0))
% 48.28/48.56  (define @t607 () (= (tptp.heap_E1038710093tion_n tptp.h @t603 @t606) (tptp.heap_E1038710093tion_n tptp.h2 @t603 @t606)))
% 48.28/48.56  (define @t608 () (@purify @t556))
% 48.28/48.56  (define @t609 () (tptp.l_put_1129034844_j_k_m tptp.get_D_1192261494_j_k_l @t556 tptp.document_ptr tptp.setter tptp.v))
% 48.28/48.56  (define @t610 () (tptp.heap_E494191872t_unit tptp.h @t609 tptp.h2))
% 48.28/48.56  (define @t611 () (not @t610))
% 48.28/48.56  (define @t612 () (tptp.cast_s253715760_r_d_e tptp.shadow_root_ptr))
% 48.28/48.56  (define @t613 () (= tptp.document_ptr @t612))
% 48.28/48.56  (define @t614 () (or @t613 @t611 @t607))
% 48.28/48.56  (define @t615 () (forall @t565 (or @t563 (not (tptp.heap_E494191872t_unit @t2 @t557 @t1)) @t552)))
% 48.28/48.56  (define @t616 () (tptp.l_put_1129034844_j_k_m tptp.get_D_1192261494_j_k_l @t608 tptp.document_ptr tptp.setter tptp.v))
% 48.28/48.56  (define @t617 () (tptp.heap_E494191872t_unit tptp.h @t616 tptp.h2))
% 48.28/48.56  (define @t618 () (not @t617))
% 48.28/48.56  (define @t619 () (or @t613 @t618 @t607))
% 48.28/48.56  (define @t620 () (@list false))
% 48.28/48.56  (define @t621 () (forall @t510 (= @t604 @t605)))
% 48.28/48.56  (define @t622 () (tptp.heap_E1038710093tion_n @t488 @t603 @t504))
% 48.28/48.56  (define @t623 () (forall @t510 (= @t605 @t622)))
% 48.28/48.56  (define @t624 () (lambda @t589 @t623))
% 48.28/48.56  (define @t625 () (tptp.heap_E1038710093tion_n @t488 @t484 @t504))
% 48.28/48.56  (define @t626 () (tptp.heap_E1038710093tion_n @t489 @t484 @t504))
% 48.28/48.56  (define @t627 () (= @t626 @t625))
% 48.28/48.56  (define @t628 () (forall @t510 @t627))
% 48.28/48.56  (define @t629 () (lambda @t539 @t628))
% 48.28/48.56  (define @t630 () (_ @t599 @t484))
% 48.28/48.56  (define @t631 () (= tptp.document_ptr @t482))
% 48.28/48.56  (define @t632 () (@purify @t549))
% 48.28/48.56  (define @t633 () (_ (_ (_ (_ @t474 @t632) tptp.document_ptr) tptp.setter) tptp.v))
% 48.28/48.56  (define @t634 () (tptp.l_put_1129034844_j_k_m tptp.get_D_1192261494_j_k_l @t632 tptp.document_ptr tptp.setter tptp.v))
% 48.28/48.56  (define @t635 () (tptp.heap_E494191872t_unit tptp.h @t634 tptp.h2))
% 48.28/48.56  (define @t636 () (= @t632 @t608))
% 48.28/48.56  (define @t637 () (not @t636))
% 48.28/48.56  (define @t638 () (not @t635))
% 48.28/48.56  (define @t639 () (= false true))
% 48.28/48.56  (define @t640 () (@const 0 tptp.heap_S1465075775_j_k_l))
% 48.28/48.56  (define @t641 () (@const 1 tptp.rObjec1617416918on_j_k))
% 48.28/48.56  (define @t642 () (@const 2 tptp.docume1935157360tr_d_e))
% 48.28/48.56  (define @t643 () (_ @t608 @t642 @t641 @t640))
% 48.28/48.56  (define @t644 () (_ @t632 @t642 @t641 @t640))
% 48.28/48.56  (define @t645 () (= @t644 @t643))
% 48.28/48.56  (define @t646 () (not @t645))
% 48.28/48.56  (define @t647 () (_ (_ @t632 @t642) @t641))
% 48.28/48.56  (define @t648 () (@purify @t647))
% 48.28/48.56  (define @t649 () (_ @t648 @t640))
% 48.28/48.56  (define @t650 () (_ tptp.put_O_834343516_j_k_l (_ tptp.cast_d1608273229_b_c_f @t642)))
% 48.28/48.56  (define @t651 () (_ @t650 (_ tptp.cast_D1252964113_h_i_l @t641)))
% 48.28/48.56  (define @t652 () (_ @t651 @t640))
% 48.28/48.56  (define @t653 () (lambda (@list @t544) (_ @t651 @t544)))
% 48.28/48.56  (define @t654 () (lambda (@list @t402 @t544) (_ (_ @t650 @t403) @t544)))
% 48.28/48.56  (define @t655 () (_ @t549 @t642))
% 48.28/48.56  (define @t656 () (_ @t549 @t642 @t641 @t640))
% 48.28/48.56  (define @t657 () (_ @t655 @t641))
% 48.28/48.56  (define @t658 () (_ @t657 @t640))
% 48.28/48.56  (define @t659 () (_ @t647 @t640))
% 48.28/48.56  (define @t660 () (= @t659 @t649))
% 48.28/48.56  (define @t661 () (= @t647 @t648))
% 48.28/48.56  (define @t662 () (and @t661 @t660))
% 48.28/48.56  (define @t663 () (_ @t657 @t640))
% 48.28/48.56  (define @t664 () (= @t658 @t663))
% 48.28/48.56  (define @t665 () (_ @t632 @t545 @t402 @t544))
% 48.28/48.56  (define @t666 () (= @t547 @t665))
% 48.28/48.56  (define @t667 () (_ @t549 @t545 @t402 @t544))
% 48.28/48.56  (define @t668 () (= @t665 @t667))
% 48.28/48.56  (define @t669 () (forall @t548 @t668))
% 48.28/48.56  (define @t670 () (tptp.put_O_834343516_j_k_l (tptp.cast_d1608273229_b_c_f @t642) (tptp.cast_D1252964113_h_i_l @t641) @t640))
% 48.28/48.56  (define @t671 () (forall @t548 (= @t555 @t665)))
% 48.28/48.56  (define @t672 () (= @t670 @t644))
% 48.28/48.56  (define @t673 () (@list @t642 @t641 @t640))
% 48.28/48.56  (define @t674 () (= @t644 @t670))
% 48.28/48.56  (define @t675 () (_ @t608 @t545 @t402 @t544))
% 48.28/48.56  (define @t676 () (_ @t556 @t545 @t402 @t544))
% 48.28/48.56  (define @t677 () (= @t675 @t676))
% 48.28/48.56  (define @t678 () (forall @t548 @t677))
% 48.28/48.56  (define @t679 () (forall @t548 (= @t555 @t675)))
% 48.28/48.56  (define @t680 () (= @t670 @t643))
% 48.28/48.56  (define @t681 () (= @t643 @t670))
% 48.28/48.56  (define @t682 () (not @t681))
% 48.28/48.56  (define @t683 () (not @t674))
% 48.28/48.56  (define @t684 () (= @t644 @t649))
% 48.28/48.56  (define @t685 () (not @t684))
% 48.28/48.56  (define @t686 () (and @t684 @t674 @t681 @t646))
% 48.28/48.56  (assume @p1 (forall (@list @t4 @t9 @t2 @t8 @t7 @t1 @t3) (=> @t14 (=> @t12 @t6))))
% 48.28/48.56  (assume @p2 (forall (@list @t4 @t9 @t2 @t16 @t15 @t1 @t3) (=> @t14 (=> @t18 @t6))))
% 48.28/48.56  (assume @p3 (forall (@list @t4 @t9 @t2 @t20 @t19 @t1 @t3) (=> @t14 (=> @t22 @t6))))
% 48.28/48.56  (assume @p4 (forall (@list @t4 @t9 @t2 @t24 @t23 @t1 @t3) (=> @t14 (=> @t25 @t6))))
% 48.28/48.56  (assume @p5 @t33)
% 48.28/48.56  (assume @p6 (forall (@list @t35 @t34) (= (= (_ tptp.cast_S988036065_b_j_k @t35) (_ tptp.cast_S988036065_b_j_k @t34)) (= @t35 @t34))))
% 48.28/48.56  (assume @p7 (forall (@list @t37 @t36) (= (= (_ tptp.cast_s253715760_r_d_e @t37) (_ tptp.cast_s253715760_r_d_e @t36)) (= @t37 @t36))))
% 48.28/48.56  (assume @p8 (forall (@list @t2 @t4 @t42 @t23 @t1 @t3 @t38) (=> @t46 (=> (forall @t45 (= @t44 (_ @t3 @t40))) @t39))))
% 48.28/48.56  (assume @p9 (forall (@list @t4 @t38 @t2 @t42 @t23 @t1 @t3) (=> (not (= @t4 @t38)) (=> @t46 @t39))))
% 48.28/48.56  (assume @p10 (forall (@list @t2 @t48 @t47 @t7 @t1 @t4 @t3) (=> @t50 @t6)))
% 48.28/48.56  (assume @p11 (forall (@list @t2 @t53 @t52 @t51 @t1 @t4 @t3) (=> @t55 @t6)))
% 48.28/48.56  (assume @p12 (forall (@list @t2 @t53 @t56 @t15 @t1 @t4 @t3) (=> @t58 @t6)))
% 48.28/48.56  (assume @p13 (forall (@list @t2 @t53 @t59 @t7 @t1 @t4 @t3) (=> @t61 @t6)))
% 48.28/48.56  (assume @p14 (forall (@list @t2 @t53 @t63 @t62 @t1 @t4 @t3) (=> @t65 @t6)))
% 48.28/48.56  (assume @p15 (forall (@list @t2 @t9 @t27 @t26 @t1 @t66 @t67) (=> @t29 (=> (forall @t75 (= @t74 @t70)) @t68))))
% 48.28/48.56  (assume @p16 (forall (@list @t2 @t9 @t8 @t7 @t1 @t76 @t67) (=> @t12 (=> (forall @t75 (= (_ @t76 @t80) @t78)) @t77))))
% 48.28/48.56  (assume @p17 (forall (@list @t2 @t9 @t8 @t7 @t1 @t66 @t67) (=> @t12 (=> (forall @t75 (= (_ @t66 @t80) @t70)) @t68))))
% 48.28/48.56  (assume @p18 (forall (@list @t2 @t9 @t16 @t15 @t1 @t76 @t67) (=> @t18 (=> (forall @t75 (= (_ @t76 @t82) @t78)) @t77))))
% 48.28/48.56  (assume @p19 (forall (@list @t2 @t9 @t16 @t15 @t1 @t66 @t67) (=> @t18 (=> (forall @t75 (= (_ @t66 @t82) @t70)) @t68))))
% 48.28/48.56  (assume @p20 (forall (@list @t2 @t9 @t20 @t19 @t1 @t76 @t67) (=> @t22 (=> (forall @t75 (= (_ @t76 @t84) @t78)) @t77))))
% 48.28/48.56  (assume @p21 (forall (@list @t2 @t9 @t20 @t19 @t1 @t66 @t67) (=> @t22 (=> (forall @t75 (= (_ @t66 @t84) @t70)) @t68))))
% 48.28/48.56  (assume @p22 (forall (@list @t2 @t9 @t24 @t23 @t1 @t76 @t67) (=> @t25 (=> (forall @t75 (= @t86 @t78)) @t77))))
% 48.28/48.56  (assume @p23 (forall (@list @t2 @t9 @t24 @t23 @t1 @t66 @t67) (=> @t25 (=> (forall @t75 (= (_ @t66 @t85) @t70)) @t68))))
% 48.28/48.56  (assume @p24 (forall (@list @t2 @t9 @t27 @t26 @t1 @t76 @t67) (=> @t29 (=> (forall @t75 (= (_ @t76 @t73) @t78)) @t77))))
% 48.28/48.56  (assume @p25 (forall (@list @t2 @t89 @t1 @t87) (=> (_ @t91 @t1) (=> (_ @t91 @t87) @t88))))
% 48.28/48.56  (assume @p26 (forall (@list @t2 @t92 @t1 @t87) (=> (_ @t94 @t1) (=> (_ @t94 @t87) @t88))))
% 48.28/48.56  (assume @p27 (forall (@list @t2 @t95 @t1 @t87) (=> (_ @t97 @t1) (=> (_ @t97 @t87) @t88))))
% 48.28/48.56  (assume @p28 (forall (@list @t2 @t98 @t1 @t87) (=> (_ @t99 @t1) (=> (_ @t99 @t87) @t88))))
% 48.28/48.56  (assume @p29 (forall (@list @t9 @t67 @t2 @t27 @t26 @t1 @t66) (=> @t100 (=> @t29 @t68))))
% 48.28/48.56  (assume @p30 (forall (@list @t9 @t67 @t2 @t8 @t7 @t1 @t76) (=> @t100 (=> @t12 @t77))))
% 48.28/48.56  (assume @p31 (forall (@list @t9 @t67 @t2 @t8 @t7 @t1 @t66) (=> @t100 (=> @t12 @t68))))
% 48.28/48.56  (assume @p32 (forall (@list @t9 @t67 @t2 @t16 @t15 @t1 @t76) (=> @t100 (=> @t18 @t77))))
% 48.28/48.56  (assume @p33 (forall (@list @t9 @t67 @t2 @t16 @t15 @t1 @t66) (=> @t100 (=> @t18 @t68))))
% 48.28/48.56  (assume @p34 (forall (@list @t9 @t67 @t2 @t20 @t19 @t1 @t76) (=> @t100 (=> @t22 @t77))))
% 48.28/48.56  (assume @p35 (forall (@list @t9 @t67 @t2 @t20 @t19 @t1 @t66) (=> @t100 (=> @t22 @t68))))
% 48.28/48.56  (assume @p36 (forall (@list @t9 @t67 @t2 @t24 @t23 @t1 @t76) (=> @t100 (=> @t25 @t77))))
% 48.28/48.56  (assume @p37 (forall (@list @t9 @t67 @t2 @t24 @t23 @t1 @t66) (=> @t100 (=> @t25 @t68))))
% 48.28/48.56  (assume @p38 (forall (@list @t9 @t67 @t2 @t27 @t26 @t1 @t76) (=> @t100 (=> @t29 @t77))))
% 48.28/48.56  (assume @p39 (forall (@list @t2 @t9 @t8 @t7 @t1 @t48 @t101) (=> @t12 @t103)))
% 48.28/48.56  (assume @p40 (forall (@list @t2 @t9 @t16 @t15 @t1 @t48 @t101) (=> @t18 @t103)))
% 48.28/48.56  (assume @p41 (forall (@list @t2 @t9 @t20 @t19 @t1 @t48 @t101) (=> @t22 @t103)))
% 48.28/48.56  (assume @p42 (forall (@list @t2 @t9 @t24 @t23 @t1 @t48 @t101) (=> @t25 @t103)))
% 48.28/48.56  (assume @p43 (forall (@list @t2 @t9 @t27 @t26 @t1 @t48 @t101) (=> @t29 @t103)))
% 48.28/48.56  (assume @p44 (forall (@list @t2 @t9 @t8 @t7 @t1 @t105 @t104) (=> @t12 @t106)))
% 48.28/48.56  (assume @p45 (forall (@list @t2 @t9 @t16 @t15 @t1 @t105 @t104) (=> @t18 @t106)))
% 48.28/48.56  (assume @p46 (forall (@list @t2 @t9 @t20 @t19 @t1 @t105 @t104) (=> @t22 @t106)))
% 48.28/48.56  (assume @p47 (forall (@list @t2 @t9 @t24 @t23 @t1 @t105 @t104) (=> @t25 @t106)))
% 48.28/48.56  (assume @p48 (forall (@list @t2 @t9 @t27 @t26 @t1 @t105 @t104) (=> @t29 @t106)))
% 48.28/48.56  (assume @p49 (forall (@list @t2 @t9 @t8 @t7 @t1 @t53 @t107) (=> @t12 @t109)))
% 48.28/48.56  (assume @p50 (forall (@list @t2 @t9 @t16 @t15 @t1 @t53 @t107) (=> @t18 @t109)))
% 48.28/48.56  (assume @p51 (forall (@list @t2 @t9 @t20 @t19 @t1 @t53 @t107) (=> @t22 @t109)))
% 48.28/48.56  (assume @p52 (forall (@list @t2 @t9 @t24 @t23 @t1 @t53 @t107) (=> @t25 @t109)))
% 48.28/48.56  (assume @p53 (forall (@list @t2 @t9 @t27 @t26 @t1 @t53 @t107) (=> @t29 @t109)))
% 48.28/48.56  (assume @p54 (forall (@list @t2 @t53 @t52 @t51 @t1 @t9 @t76) (=> @t55 @t111)))
% 48.28/48.56  (assume @p55 (forall (@list @t2 @t53 @t56 @t15 @t1 @t9 @t76) (=> @t58 @t111)))
% 48.28/48.56  (assume @p56 (forall (@list @t2 @t53 @t59 @t7 @t1 @t9 @t76) (=> @t61 @t111)))
% 48.28/48.56  (assume @p57 (forall (@list @t2 @t53 @t63 @t62 @t1 @t9 @t76) (=> @t65 @t111)))
% 48.28/48.56  (assume @p58 (forall (@list @t2 @t53 @t52 @t51 @t1 @t9 @t66) (=> @t55 @t113)))
% 48.28/48.56  (assume @p59 (forall (@list @t2 @t53 @t56 @t15 @t1 @t9 @t66) (=> @t58 @t113)))
% 48.28/48.56  (assume @p60 (forall (@list @t2 @t53 @t59 @t7 @t1 @t9 @t66) (=> @t61 @t113)))
% 48.28/48.56  (assume @p61 (forall (@list @t2 @t53 @t63 @t62 @t1 @t9 @t66) (=> @t65 @t113)))
% 48.28/48.56  (assume @p62 (forall (@list @t2 @t48 @t47 @t7 @t1 @t9 @t76) (=> @t50 @t111)))
% 48.28/48.56  (assume @p63 (forall (@list @t2 @t48 @t47 @t7 @t1 @t9 @t66) (=> @t50 @t113)))
% 48.28/48.56  (assume @p64 (forall (@list @t2 @t4 @t42 @t23 @t1 @t53 @t107) (=> @t46 @t109)))
% 48.28/48.56  (assume @p65 (forall (@list @t2 @t4 @t42 @t23 @t1 @t105 @t104) (=> @t46 @t106)))
% 48.28/48.56  (assume @p66 (forall (@list @t2 @t4 @t42 @t23 @t1 @t48 @t101) (=> @t46 @t103)))
% 48.28/48.56  (assume @p67 (forall (@list @t4 @t9 @t2 @t42 @t23 @t1 @t76) (=> @t14 (=> @t46 @t111))))
% 48.28/48.56  (assume @p68 (forall (@list @t4 @t9 @t2 @t42 @t23 @t1 @t66) (=> @t14 (=> @t46 @t113))))
% 48.28/48.56  (assume @p69 (forall (@list @t2 @t4 @t42 @t23 @t1 @t76 @t9) (=> @t46 (=> (forall @t45 (= (_ @t76 @t115) (_ @t76 @t114))) @t111))))
% 48.28/48.56  (assume @p70 (forall (@list @t2 @t4 @t42 @t23 @t1 @t66 @t9) (=> @t46 (=> (forall @t45 (= (_ @t66 @t115) (_ @t66 @t114))) @t113))))
% 48.28/48.56  (assume @p71 (forall (@list @t101 @t47 @t7 @t2 @t48 @t1 @t116) (=> (forall @t120 (= (_ @t101 @t119) (_ @t101 @t118))) @t117)))
% 48.28/48.56  (assume @p72 (forall (@list @t107 @t52 @t51 @t2 @t53 @t1 @t121) (=> (forall @t127 (= (_ @t107 @t126) @t125)) @t123)))
% 48.28/48.56  (assume @p73 (forall (@list @t107 @t56 @t15 @t2 @t53 @t1 @t121) (=> (forall @t127 (= (_ @t107 @t129) @t125)) @t128)))
% 48.28/48.56  (assume @p74 (forall (@list @t107 @t59 @t7 @t2 @t53 @t1 @t121) (=> (forall @t127 (= (_ @t107 @t131) @t125)) @t130)))
% 48.28/48.56  (assume @p75 (forall (@list @t107 @t63 @t62 @t2 @t53 @t1 @t121) (=> (forall @t127 (= (_ @t107 @t133) @t125)) @t132)))
% 48.28/48.56  (assume @p76 (forall (@list @t2 @t48 @t47 @t7 @t1 @t53 @t107) (=> @t50 @t109)))
% 48.28/48.56  (assume @p77 (forall (@list @t2 @t53 @t52 @t51 @t1 @t48 @t101) (=> @t55 @t103)))
% 48.28/48.56  (assume @p78 (forall (@list @t2 @t53 @t56 @t15 @t1 @t48 @t101) (=> @t58 @t103)))
% 48.28/48.56  (assume @p79 (forall (@list @t2 @t53 @t59 @t7 @t1 @t48 @t101) (=> @t61 @t103)))
% 48.28/48.56  (assume @p80 (forall (@list @t2 @t53 @t63 @t62 @t1 @t48 @t101) (=> @t65 @t103)))
% 48.28/48.56  (assume @p81 (forall (@list @t48 @t116 @t2 @t47 @t7 @t1 @t101) (=> (not (= @t48 @t116)) @t117)))
% 48.28/48.56  (assume @p82 (forall (@list @t53 @t121 @t2 @t52 @t51 @t1 @t107) (=> @t134 @t123)))
% 48.28/48.56  (assume @p83 (forall (@list @t53 @t121 @t2 @t56 @t15 @t1 @t107) (=> @t134 @t128)))
% 48.28/48.56  (assume @p84 (forall (@list @t53 @t121 @t2 @t59 @t7 @t1 @t107) (=> @t134 @t130)))
% 48.28/48.56  (assume @p85 (forall (@list @t53 @t121 @t2 @t63 @t62 @t1 @t107) (=> @t134 @t132)))
% 48.28/48.56  (assume @p86 (forall (@list @t2 @t1 @t87) (= (_ (_ @t11 (_ tptp.heap_E1876089495eption @t1)) @t87) (= @t87 @t1))))
% 48.28/48.56  (assume @p87 (forall @t135 (= (_ (_ @t11 tptp.heap_E1613639261eption) @t1) (= @t2 @t1))))
% 48.28/48.56  (assume @p88 (forall (@list @t2 @t48 @t47 @t7 @t1 @t104 @t105) (=> @t50 (=> @t138 @t106))))
% 48.28/48.56  (assume @p89 (forall (@list @t104 @t47 @t7 @t2 @t48 @t1 @t105) (=> @t138 @t139)))
% 48.28/48.56  (assume @p90 (forall (@list @t2 @t53 @t52 @t51 @t1 @t104 @t105) (=> @t55 (=> @t143 @t106))))
% 48.28/48.56  (assume @p91 (forall (@list @t2 @t53 @t56 @t15 @t1 @t104 @t105) (=> @t58 (=> @t145 @t106))))
% 48.28/48.56  (assume @p92 (forall (@list @t2 @t53 @t59 @t7 @t1 @t104 @t105) (=> @t61 (=> @t147 @t106))))
% 48.28/48.56  (assume @p93 (forall (@list @t2 @t53 @t63 @t62 @t1 @t104 @t105) (=> @t65 (=> @t149 @t106))))
% 48.28/48.56  (assume @p94 (forall (@list @t104 @t52 @t51 @t2 @t53 @t1 @t105) (=> @t143 @t150)))
% 48.28/48.56  (assume @p95 (forall (@list @t104 @t56 @t15 @t2 @t53 @t1 @t105) (=> @t145 @t151)))
% 48.28/48.56  (assume @p96 (forall (@list @t104 @t59 @t7 @t2 @t53 @t1 @t105) (=> @t147 @t152)))
% 48.28/48.56  (assume @p97 (forall (@list @t104 @t63 @t62 @t2 @t53 @t1 @t105) (=> @t149 @t153)))
% 48.28/48.56  (assume @p98 (forall (@list @t48 @t105 @t2 @t47 @t7 @t1 @t104) (=> (not @t155) @t139)))
% 48.28/48.56  (assume @p99 (forall (@list @t53 @t105 @t2 @t52 @t51 @t1 @t104) (=> @t158 @t150)))
% 48.28/48.56  (assume @p100 (forall (@list @t53 @t105 @t2 @t56 @t15 @t1 @t104) (=> @t158 @t151)))
% 48.28/48.56  (assume @p101 (forall (@list @t53 @t105 @t2 @t59 @t7 @t1 @t104) (=> @t158 @t152)))
% 48.28/48.56  (assume @p102 (forall (@list @t53 @t105 @t2 @t63 @t62 @t1 @t104) (=> @t158 @t153)))
% 48.28/48.56  (assume @p103 (forall (@list @t7) (= tptp.is_sha1522929624_b_j_k (lambda @t160 (_ tptp.is_sha1522929624_b_j_k (_ (_ tptp.doctyp68000440on_j_k @t79) @t159))))))
% 48.28/48.56  (assume @p104 (forall (@list @t19) (= tptp.is_sha1522929624_b_j_k (lambda @t160 (_ tptp.is_sha1522929624_b_j_k (_ (_ tptp.docume244715269on_j_k @t83) @t159))))))
% 48.28/48.56  (assume @p105 (forall (@list @t15) (= tptp.is_sha1522929624_b_j_k (lambda @t160 (_ tptp.is_sha1522929624_b_j_k (_ (_ tptp.discon442323090on_j_k @t81) @t159))))))
% 48.28/48.56  (assume @p106 (forall (@list @t162 @t161) (= (= (_ tptp.cast_e316309897tr_b_c @t162) (_ tptp.cast_e316309897tr_b_c @t161)) (= @t162 @t161))))
% 48.28/48.56  (assume @p107 (forall (@list @t164 @t163) (= (= (_ tptp.cast_c164415100_b_a_c @t164) (_ tptp.cast_c164415100_b_a_c @t163)) (= @t164 @t163))))
% 48.28/48.56  (assume @p108 (forall (@list @t48 @t53) (not (= @t154 @t156))))
% 48.28/48.56  (assume @p109 (forall (@list @t53 @t48) (not (= @t156 @t154))))
% 48.28/48.56  (assume @p110 (forall (@list @t2 @t4 @t169 @t165 @t1 @t166) (=> (_ (_ @t11 (_ (_ (_ tptp.shadow1464843188_i_k_l @t4) @t169) @t165)) @t1) (=> (forall @t45 (= (_ @t166 (_ (_ @t169 @t168) @t40)) @t165)) (_ (_ @t167 (_ (_ tptp.shadow1068876397_i_k_l @t4) @t166)) @t165)))))
% 48.28/48.56  (assume @p111 (forall (@list @t2 @t4 @t174 @t170 @t1 @t171) (=> (_ (_ @t11 (_ (_ (_ tptp.shadow2015416421_i_k_l @t4) @t174) @t170)) @t1) (=> (forall @t45 (= (_ @t171 (_ (_ @t174 @t173) @t40)) @t170)) (_ (_ @t172 (_ (_ tptp.shadow902827384_i_k_l @t4) @t171)) @t170)))))
% 48.28/48.56  (assume @p112 (forall (@list @t2 @t4 @t179 @t175 @t1 @t176) (=> (_ (_ @t11 (_ (_ (_ tptp.shadow1110190411_i_k_l @t4) @t179) @t175)) @t1) (=> (forall @t45 (= (_ @t176 (_ (_ @t179 @t178) @t40)) @t175)) (_ (_ @t177 (_ (_ tptp.shadow2050000606_i_k_l @t4) @t176)) @t175)))))
% 48.28/48.56  (assume @p113 (forall (@list @t2 @t4 @t182 @t26 @t1 @t180) (=> (_ (_ @t11 (_ (_ (_ tptp.shadow1030535182_i_k_l @t4) @t182) @t26)) @t1) (=> (forall @t45 (= (_ @t180 (_ (_ @t182 @t72) @t40)) @t26)) (_ (_ @t181 (_ (_ tptp.shadow1194684833_i_k_l @t4) @t180)) @t26)))))
% 48.28/48.56  (assume @p114 (forall (@list @t2 @t4 @t42 @t23 @t1 @t3) (=> @t46 (=> (forall @t45 (= @t44 @t23)) (_ (_ @t183 @t5) @t23)))))
% 48.28/48.56  (assume @p115 (forall (@list @t2 @t9 @t7 @t1) (=> (_ (_ @t11 (_ (_ @t10 tptp.doctyp68000440on_j_k) @t7)) @t1) @t185)))
% 48.28/48.56  (assume @p116 (forall (@list @t2 @t9 @t15 @t1) (=> (_ (_ @t11 (_ (_ @t17 tptp.discon442323090on_j_k) @t15)) @t1) @t185)))
% 48.28/48.56  (assume @p117 (forall (@list @t2 @t9 @t19 @t1) (=> (_ (_ @t11 (_ (_ @t21 tptp.docume244715269on_j_k) @t19)) @t1) @t185)))
% 48.28/48.56  (assume @p118 (forall (@list @t2 @t95 @t187 @t186) (=> (_ @t189 @t187) (=> (_ @t189 @t186) (= @t187 @t186)))))
% 48.28/48.56  (assume @p119 (forall (@list @t2 @t92 @t161 @t190) (=> (_ @t192 @t161) (=> (_ @t192 @t190) (= @t161 @t190)))))
% 48.28/48.56  (assume @p120 (forall (@list @t2 @t98 @t194 @t193) (=> (_ @t195 @t194) (=> (_ @t195 @t193) (= @t194 @t193)))))
% 48.28/48.56  (assume @p121 (forall (@list @t2 @t198 @t197 @t196) (=> (_ @t199 @t197) (=> (_ @t199 @t196) (= @t197 @t196)))))
% 48.28/48.56  (assume @p122 (forall (@list @t2 @t202 @t201 @t200) (=> (_ @t203 @t201) (=> (_ @t203 @t200) (= @t201 @t200)))))
% 48.28/48.56  (assume @p123 (forall (@list @t2 @t53 @t205 @t165 @t1 @t204) (=> (_ (_ @t11 (_ (_ (_ tptp.put_M_1236788814_j_k_l @t53) @t205) @t165)) @t1) (=> (forall @t127 (= (_ @t204 (_ (_ @t205 @t168) @t124)) @t165)) (_ (_ @t167 (_ (_ tptp.get_M_650077447_j_k_l @t53) @t204)) @t165)))))
% 48.28/48.56  (assume @p124 (forall (@list @t2 @t53 @t207 @t170 @t1 @t206) (=> (_ (_ @t11 (_ (_ (_ tptp.put_M_1198351521_j_k_l @t53) @t207) @t170)) @t1) (=> (forall @t127 (= (_ @t206 (_ (_ @t207 @t173) @t124)) @t170)) (_ (_ @t172 (_ (_ tptp.get_M_1338284716_j_k_l @t53) @t206)) @t170)))))
% 48.28/48.56  (assume @p125 (forall (@list @t2 @t53 @t209 @t175 @t1 @t208) (=> (_ (_ @t11 (_ (_ (_ tptp.put_M_1101791239_j_k_l @t53) @t209) @t175)) @t1) (=> (forall @t127 (= (_ @t208 (_ (_ @t209 @t178) @t124)) @t175)) (_ (_ @t177 (_ (_ tptp.get_M_1238860946_j_k_l @t53) @t208)) @t175)))))
% 48.28/48.56  (assume @p126 (forall (@list @t2 @t53 @t211 @t26 @t1 @t210) (=> (_ (_ @t11 (_ (_ (_ tptp.put_M_1862598346_j_k_l @t53) @t211) @t26)) @t1) (=> (forall @t127 (= (_ @t210 (_ (_ @t211 @t72) @t124)) @t26)) (_ (_ @t181 (_ (_ tptp.get_M_220285781_j_k_l @t53) @t210)) @t26)))))
% 48.28/48.56  (assume @p127 (forall (@list @t2 @t53 @t212 @t23 @t1 @t107) (=> (_ (_ @t11 (_ (_ (_ tptp.put_M_2120900233_j_k_l @t53) @t212) @t23)) @t1) (=> (forall @t127 (= (_ @t107 (_ (_ @t212 @t41) @t124)) @t23)) (_ (_ @t183 @t108) @t23)))))
% 48.28/48.56  (assume @p128 (forall (@list @t2 @t53 @t52 @t51 @t1 @t213) (=> @t55 (=> (forall @t127 (= (_ @t213 @t126) @t51)) (_ (_ @t214 (_ (_ tptp.get_M_1154267419_j_k_l @t53) @t213)) @t51)))))
% 48.28/48.56  (assume @p129 (forall (@list @t2 @t53 @t56 @t15 @t1 @t215) (=> @t58 (=> (forall @t127 (= (_ @t215 @t129) @t15)) (_ (_ @t216 (_ (_ tptp.get_M_88885319_j_k_l @t53) @t215)) @t15)))))
% 48.28/48.56  (assume @p130 (forall (@list @t2 @t53 @t59 @t7 @t1 @t217) (=> @t61 (=> (forall @t127 (= (_ @t217 @t131) @t7)) (_ (_ @t218 (_ (_ tptp.get_M_51280086_j_k_l @t53) @t217)) @t7)))))
% 48.28/48.56  (assume @p131 (forall (@list @t2 @t53 @t63 @t62 @t1 @t219) (=> @t65 (=> (forall @t127 (= (_ @t219 @t133) @t62)) (_ (_ @t220 (_ (_ tptp.get_M_685446945_j_k_l @t53) @t219)) @t62)))))
% 48.28/48.56  (assume @p132 (forall (@list @t221 @t222 @t165 @t2 @t48 @t1) (=> (forall @t120 (= (_ @t221 (_ (_ @t222 @t168) @t118)) @t165)) (=> (_ (_ @t11 (_ (_ (_ tptp.put_M_726238649_j_k_l @t48) @t222) @t165)) @t1) (_ (_ @t167 (_ (_ tptp.get_M_1865279188_j_k_l @t48) @t221)) @t165)))))
% 48.28/48.56  (assume @p133 (forall (@list @t223 @t224 @t170 @t2 @t48 @t1) (=> (forall @t120 (= (_ @t223 (_ (_ @t224 @t173) @t118)) @t170)) (=> (_ (_ @t11 (_ (_ (_ tptp.put_M_731120658_j_k_l @t48) @t224) @t170)) @t1) (_ (_ @t172 (_ (_ tptp.get_M_1186169077_j_k_l @t48) @t223)) @t170)))))
% 48.28/48.57  (assume @p134 (forall (@list @t225 @t226 @t175 @t2 @t48 @t1) (=> (forall @t120 (= (_ @t225 (_ (_ @t226 @t178) @t118)) @t175)) (=> (_ (_ @t11 (_ (_ (_ tptp.put_M_1374331384_j_k_l @t48) @t226) @t175)) @t1) (_ (_ @t177 (_ (_ tptp.get_M_1903403023_j_k_l @t48) @t225)) @t175)))))
% 48.28/48.57  (assume @p135 (forall (@list @t227 @t228 @t26 @t2 @t48 @t1) (=> (forall @t120 (= (_ @t227 (_ (_ @t228 @t72) @t118)) @t26)) (=> (_ (_ @t11 (_ (_ (_ tptp.put_M_199545403_j_k_l @t48) @t228) @t26)) @t1) (_ (_ @t181 (_ (_ tptp.get_M_1665432076_j_k_l @t48) @t227)) @t26)))))
% 48.28/48.57  (assume @p136 (forall (@list @t101 @t229 @t23 @t2 @t48 @t1) (=> (forall @t120 (= (_ @t101 (_ (_ @t229 @t41) @t118)) @t23)) (=> (_ (_ @t11 (_ (_ (_ tptp.put_M_243508858_j_k_l @t48) @t229) @t23)) @t1) (_ (_ @t183 @t102) @t23)))))
% 48.28/48.57  (assume @p137 (forall (@list @t230 @t47 @t7 @t2 @t48 @t1) (=> (forall @t120 (= (_ @t230 @t119) @t7)) (=> @t50 (_ (_ @t218 (_ (_ tptp.get_M_2088872005_j_k_l @t48) @t230)) @t7)))))
% 48.28/48.57  (assume @p138 (forall (@list @t2 @t9 @t232 @t165 @t1 @t231) (=> (_ (_ @t11 (_ (_ (_ tptp.put_M_2097930918_h_i_l @t9) @t232) @t165)) @t1) (=> (forall @t75 (= (_ @t231 (_ (_ @t232 @t168) @t69)) @t165)) (_ (_ @t167 (_ (_ tptp.get_M_462148605_h_i_l @t9) @t231)) @t165)))))
% 48.28/48.57  (assume @p139 (forall (@list @t2 @t9 @t234 @t170 @t1 @t233) (=> (_ (_ @t11 (_ (_ (_ tptp.put_M_1789706523_h_i_l @t9) @t234) @t170)) @t1) (=> (forall @t75 (= (_ @t233 (_ (_ @t234 @t173) @t69)) @t170)) (_ (_ @t172 (_ (_ tptp.get_M_377480556_h_i_l @t9) @t233)) @t170)))))
% 48.28/48.57  (assume @p140 (forall (@list @t2 @t9 @t236 @t175 @t1 @t235) (=> (_ (_ @t11 (_ (_ (_ tptp.put_M_1656033077_h_i_l @t9) @t236) @t175)) @t1) (=> (forall @t75 (= (_ @t235 (_ (_ @t236 @t178) @t69)) @t175)) (_ (_ @t177 (_ (_ tptp.get_M_1965837010_h_i_l @t9) @t235)) @t175)))))
% 48.28/48.57  (assume @p141 (forall (@list @t2 @t9 @t8 @t7 @t1 @t237) (=> @t12 (=> (forall @t75 (= (_ @t237 @t80) @t7)) (_ (_ @t218 (_ (_ tptp.get_M_1536717772_h_i_l @t9) @t237)) @t7)))))
% 48.28/48.57  (assume @p142 (forall (@list @t2 @t9 @t16 @t15 @t1 @t238) (=> @t18 (=> (forall @t75 (= (_ @t238 @t82) @t15)) (_ (_ @t216 (_ (_ tptp.get_M_986049031_h_i_l @t9) @t238)) @t15)))))
% 48.28/48.57  (assume @p143 (forall (@list @t2 @t9 @t20 @t19 @t1 @t239) (=> @t22 (=> (forall @t75 (= (_ @t239 @t84) @t19)) (_ (_ @t240 (_ (_ tptp.get_M_1723352102_h_i_l @t9) @t239)) @t19)))))
% 48.28/48.57  (assume @p144 (forall (@list @t2 @t9 @t24 @t23 @t1 @t76) (=> @t25 (=> (forall @t75 (= @t86 @t23)) (_ (_ @t183 @t110) @t23)))))
% 48.28/48.57  (assume @p145 (forall (@list @t2 @t9 @t27 @t26 @t1 @t66) (=> @t29 (=> (forall @t75 (= @t74 @t26)) (_ (_ @t181 @t112) @t26)))))
% 48.28/48.57  (assume @p146 (forall @t242 (=> @t241 @t185)))
% 48.28/48.57  (assume @p147 (forall @t244 (=> @t243 @t185)))
% 48.28/48.57  (assume @p148 (forall @t246 (=> @t245 @t185)))
% 48.28/48.57  (assume @p149 (forall @t248 (=> @t247 @t185)))
% 48.28/48.57  (assume @p150 (forall @t250 (=> @t249 @t185)))
% 48.28/48.57  (assume @p151 (forall @t251 (=> @t184 @t184)))
% 48.28/48.57  (assume @p152 (forall @t255 (= (= @t254 tptp.none_R125524722tion_j) (not (exists (@list @t253) (= (_ tptp.cast_S988036065_b_j_k @t253) @t252))))))
% 48.28/48.57  (assume @p153 (forall (@list @t257 @t256) (=> (= @t260 @t259) (=> (=> @t261 (=> (not @t259) (= @t258 (_ tptp.the_RO2055010943tion_j @t256)))) (= @t257 @t256)))))
% 48.28/48.57  (assume @p154 (forall @t242 (=> @t241 @t263)))
% 48.28/48.57  (assume @p155 (forall @t244 (=> @t243 @t265)))
% 48.28/48.57  (assume @p156 (forall @t246 (=> @t245 @t265)))
% 48.28/48.57  (assume @p157 (forall @t248 (=> @t247 @t265)))
% 48.28/48.57  (assume @p158 (forall @t250 (=> @t249 @t265)))
% 48.28/48.57  (assume @p159 (forall @t244 (=> @t243 @t263)))
% 48.28/48.57  (assume @p160 (forall @t250 (=> @t249 @t263)))
% 48.28/48.57  (assume @p161 (forall @t248 (=> @t247 @t263)))
% 48.28/48.57  (assume @p162 (forall @t246 (=> @t245 @t263)))
% 48.28/48.57  (assume @p163 (forall @t251 (=> @t264 @t264)))
% 48.28/48.57  (assume @p164 (forall @t251 (=> @t262 @t264)))
% 48.28/48.57  (assume @p165 (forall @t251 (=> @t262 @t262)))
% 48.28/48.57  (assume @p166 (forall @t251 (=> @t184 @t262)))
% 48.28/48.57  (assume @p167 (forall @t251 (=> @t184 @t264)))
% 48.28/48.57  (assume @p168 (= tptp.type_w697503069_j_k_l tptp.l_type85280056_j_k_l))
% 48.28/48.57  (assume @p169 (= tptp.type_w1771507213_j_k_l tptp.l_type1003141153_j_k_l))
% 48.28/48.57  (assume @p170 (= tptp.type_w1479951274_j_k_l tptp.l_type1130145226_j_k_l))
% 48.28/48.57  (assume @p171 (forall (@list @t2 @t1 @t268 @t266 @t104) (=> @t271 (=> @t270 (=> (not (= @t266 @t269)) @t267)))))
% 48.28/48.57  (assume @p172 (forall (@list @t2 @t1 @t272 @t266 @t104) (=> @t275 (=> @t274 (=> (not (= @t266 @t273)) @t267)))))
% 48.28/48.57  (assume @p173 (forall @t135 (=> @t275 @t185)))
% 48.28/48.57  (assume @p174 (forall @t135 (=> @t271 @t185)))
% 48.28/48.57  (assume @p175 (forall @t135 (=> @t275 @t263)))
% 48.28/48.57  (assume @p176 (forall @t135 (=> @t275 @t265)))
% 48.28/48.57  (assume @p177 (forall @t135 (=> @t271 @t263)))
% 48.28/48.57  (assume @p178 (forall (@list @t2 @t1 @t272 @t276 @t107) (=> @t275 (=> @t274 (=> (not (= @t276 @t272)) @t277)))))
% 48.28/48.57  (assume @p179 (forall (@list @t2 @t1 @t278 @t101) (=> @t275 @t279)))
% 48.28/48.57  (assume @p180 (forall @t282 (=> @t275 @t281)))
% 48.28/48.57  (assume @p181 (forall @t284 (=> @t275 @t283)))
% 48.28/48.57  (assume @p182 (forall @t282 (=> @t271 @t281)))
% 48.28/48.57  (assume @p183 (forall @t284 (=> @t271 @t283)))
% 48.28/48.57  (assume @p184 (forall (@list @t2 @t1 @t268 @t278 @t101) (=> @t271 (=> @t270 (=> (not (= @t278 @t268)) @t279)))))
% 48.28/48.57  (assume @p185 (forall (@list @t2 @t1 @t268 @t276 @t107) (=> @t271 (=> @t270 @t277))))
% 48.28/48.57  (assume @p186 (forall @t285 (=> @t275 (=> @t274 (_ (_ @t214 (_ (_ tptp.get_M_1154267419_j_k_l @t272) tptp.shadow1820683706tion_g)) tptp.none_s1706699231_ptr_d)))))
% 48.28/48.57  (assume @p187 (forall @t292 (=> (forall @t291 (=> (_ (_ (_ tptp.heap_E1982034951_ptr_b @t289) tptp.new_ch829669006_j_k_l) @t288) @t290)) @t287)))
% 48.28/48.57  (assume @p188 (forall @t294 (=> @t287 (=> @t271 @t293))))
% 48.28/48.57  (assume @p189 (_ tptp.l_new_540233301_j_k_l tptp.type_w1479951274_j_k_l))
% 48.28/48.57  (assume @p190 (_ tptp.l_new_410495338_j_k_l tptp.type_w1479951274_j_k_l))
% 48.28/48.57  (assume @p191 (_ tptp.l_new_540233301_j_k_l tptp.type_w1771507213_j_k_l))
% 48.28/48.57  (assume @p192 (_ tptp.l_new_410495338_j_k_l tptp.type_w1771507213_j_k_l))
% 48.28/48.57  (assume @p193 (_ tptp.l_new_540233301_j_k_l tptp.type_w697503069_j_k_l))
% 48.28/48.57  (assume @p194 (forall @t306 (=> @t305 (=> @t304 (=> (forall @t303 (=> (= @t302 @t300) @t301)) @t299)))))
% 48.28/48.57  (assume @p195 (forall @t306 (=> @t305 (=> @t304 (=> (forall @t303 (=> (= @t300 @t302) @t301)) @t299)))))
% 48.28/48.57  (assume @p196 (forall @t294 (=> @t307 (=> @t275 @t293))))
% 48.28/48.57  (assume @p197 (forall @t292 (=> (forall @t291 (=> (_ (_ (_ tptp.heap_E24690662_ptr_a @t289) tptp.new_el717272935_j_k_l) @t288) @t290)) @t307)))
% 48.28/48.57  (assume @p198 (forall (@list @t2 @t268) (=> @t270 (_ tptp.is_cha504820986_t_r_b @t268))))
% 48.28/48.57  (assume @p199 (forall (@list @t2 @t272) (=> @t274 (_ tptp.is_ele1129207902_t_r_a @t272))))
% 48.28/48.57  (assume @p200 (forall @t320 (=> @t319 (=> @t318 (=> @t317 @t312)))))
% 48.28/48.57  (assume @p201 (forall @t329 (=> @t319 (=> @t328 (=> (forall @t327 (=> (= @t324 @t326) @t325)) @t323)))))
% 48.28/48.57  (assume @p202 (forall @t329 (=> @t319 (=> @t328 (=> (forall @t327 (=> (= @t326 @t324) @t325)) @t323)))))
% 48.28/48.57  (assume @p203 (forall @t320 (=> @t319 (=> @t318 (=> @t330 @t312)))))
% 48.28/48.57  (assume @p204 (forall @t336 (=> @t335 (=> @t334 (=> @t317 @t333)))))
% 48.28/48.57  (assume @p205 (forall @t336 (=> @t335 (=> @t334 (=> @t330 @t333)))))
% 48.28/48.57  (assume @p206 (forall @t346 (=> @t319 (=> @t345 (=> @t344 @t339)))))
% 48.28/48.57  (assume @p207 (forall @t346 (=> @t319 (=> @t345 (=> @t347 @t339)))))
% 48.28/48.57  (assume @p208 (forall (@list @t2 @t1 @t268) (=> @t271 (=> @t270 (_ (_ @t218 (_ (_ tptp.get_M_2088872005_j_k_l @t268) tptp.val_option_h)) tptp.nil_char)))))
% 48.28/48.57  (assume @p209 (forall (@list @t2 @t1 @t272 @t349 @t348) (=> @t275 (=> @t274 (=> (not (= @t349 (_ tptp.cast_n552817316_d_e_f @t273))) @t350)))))
% 48.28/48.57  (assume @p210 (forall @t359 (=> @t305 (=> @t358 (=> (forall @t357 (=> (= @t356 @t354) @t355)) @t353)))))
% 48.28/48.57  (assume @p211 (forall @t362 (=> @t305 (=> @t361 (=> @t344 @t360)))))
% 48.28/48.57  (assume @p212 (forall (@list @t48 @t363 @t2 @t47 @t7 @t1 @t348) (=> (not (= (_ tptp.cast_n552817316_d_e_f @t154) @t363)) @t365)))
% 48.28/48.57  (assume @p213 (forall (@list @t53 @t363 @t2 @t52 @t51 @t1 @t348) (=> @t367 @t366)))
% 48.28/48.57  (assume @p214 (forall (@list @t53 @t363 @t2 @t56 @t15 @t1 @t348) (=> @t367 @t368)))
% 48.28/48.57  (assume @p215 (forall (@list @t53 @t363 @t2 @t59 @t7 @t1 @t348) (=> @t367 @t369)))
% 48.28/48.57  (assume @p216 (forall (@list @t53 @t363 @t2 @t63 @t62 @t1 @t348) (=> @t367 @t370)))
% 48.28/48.57  (assume @p217 (forall (@list @t2 @t1 @t268 @t349 @t348) (=> @t271 (=> @t270 (=> (not (= @t349 (_ tptp.cast_n552817316_d_e_f @t269))) @t350)))))
% 48.28/48.57  (assume @p218 (forall @t362 (=> @t305 (=> @t361 (=> @t347 @t360)))))
% 48.28/48.57  (assume @p219 (forall @t359 (=> @t305 (=> @t358 (=> (forall @t357 (=> (= @t354 @t356) @t355)) @t353)))))
% 48.28/48.57  (assume @p220 (forall @t285 (=> @t275 (=> @t274 (_ (_ @t218 (_ (_ tptp.get_M_51280086_j_k_l @t272) tptp.tag_na866435078tion_g)) tptp.nil_char)))))
% 48.28/48.57  (assume @p221 (forall (@list @t2 @t53 @t52 @t51 @t1 @t348 @t363) (=> @t55 (=> @t372 @t364))))
% 48.28/48.57  (assume @p222 (forall (@list @t2 @t53 @t56 @t15 @t1 @t348 @t363) (=> @t58 (=> @t373 @t364))))
% 48.28/48.57  (assume @p223 (forall (@list @t2 @t53 @t59 @t7 @t1 @t348 @t363) (=> @t61 (=> @t374 @t364))))
% 48.28/48.57  (assume @p224 (forall (@list @t2 @t53 @t63 @t62 @t1 @t348 @t363) (=> @t65 (=> @t375 @t364))))
% 48.28/48.57  (assume @p225 (forall (@list @t348 @t52 @t51 @t2 @t53 @t1 @t363) (=> @t372 @t366)))
% 48.28/48.57  (assume @p226 (forall (@list @t348 @t56 @t15 @t2 @t53 @t1 @t363) (=> @t373 @t368)))
% 48.28/48.57  (assume @p227 (forall (@list @t348 @t59 @t7 @t2 @t53 @t1 @t363) (=> @t374 @t369)))
% 48.28/48.57  (assume @p228 (forall (@list @t348 @t63 @t62 @t2 @t53 @t1 @t363) (=> @t375 @t370)))
% 48.28/48.57  (assume @p229 (forall @t378 (=> @t305 (=> @t377 (=> @t330 @t376)))))
% 48.28/48.57  (assume @p230 (forall @t378 (=> @t305 (=> @t377 (=> @t317 @t376)))))
% 48.28/48.57  (assume @p231 (forall (@list @t348 @t47 @t7 @t2 @t48 @t1 @t363) (=> @t379 @t365)))
% 48.28/48.57  (assume @p232 (forall (@list @t2 @t48 @t47 @t7 @t1 @t348 @t363) (=> @t50 (=> @t379 @t364))))
% 48.28/48.57  (assume @p233 (forall (@list @t2 @t4 @t42 @t23 @t1 @t348 @t363) (=> @t46 (=> (forall @t45 (= (_ @t348 (_ tptp.cast_D1252964113_h_i_l @t115)) (_ @t348 (_ tptp.cast_D1252964113_h_i_l @t114)))) @t364))))
% 48.28/48.57  (assume @p234 (forall (@list @t381 @t380) (= (= (_ tptp.cast_D1252964113_h_i_l @t381) (_ tptp.cast_D1252964113_h_i_l @t380)) (= @t381 @t380))))
% 48.28/48.57  (assume @p235 (forall (@list @t383 @t252) (not (= @t384 @t382))))
% 48.28/48.57  (assume @p236 (forall (@list @t252 @t383) (not (= @t382 @t384))))
% 48.28/48.57  (assume @p237 (forall (@list @t348 @t8 @t7 @t2 @t9 @t1 @t363) (=> @t387 @t385)))
% 48.28/48.57  (assume @p238 (forall (@list @t348 @t16 @t15 @t2 @t9 @t1 @t363) (=> @t389 @t388)))
% 48.28/48.57  (assume @p239 (forall (@list @t348 @t20 @t19 @t2 @t9 @t1 @t363) (=> @t391 @t390)))
% 48.28/48.57  (assume @p240 (forall (@list @t348 @t24 @t23 @t2 @t9 @t1 @t363) (=> @t393 @t392)))
% 48.28/48.57  (assume @p241 (forall (@list @t348 @t27 @t26 @t2 @t9 @t1 @t363) (=> @t395 @t394)))
% 48.28/48.57  (assume @p242 (forall (@list @t2 @t9 @t8 @t7 @t1 @t348 @t363) (=> @t12 (=> @t387 @t364))))
% 48.28/48.57  (assume @p243 (forall (@list @t2 @t9 @t16 @t15 @t1 @t348 @t363) (=> @t18 (=> @t389 @t364))))
% 48.28/48.57  (assume @p244 (forall (@list @t2 @t9 @t20 @t19 @t1 @t348 @t363) (=> @t22 (=> @t391 @t364))))
% 48.28/48.57  (assume @p245 (forall (@list @t2 @t9 @t24 @t23 @t1 @t348 @t363) (=> @t25 (=> @t393 @t364))))
% 48.28/48.57  (assume @p246 (forall (@list @t2 @t9 @t27 @t26 @t1 @t348 @t363) (=> @t29 (=> @t395 @t364))))
% 48.28/48.57  (assume @p247 (forall (@list @t4 @t363 @t2 @t42 @t23 @t1 @t348) (=> (not (= (_ tptp.cast_d1608273229_b_c_f @t13) @t363)) (=> @t46 @t364))))
% 48.28/48.57  (assume @p248 (forall (@list @t9 @t363 @t2 @t8 @t7 @t1 @t348) (=> @t397 @t385)))
% 48.28/48.57  (assume @p249 (forall (@list @t9 @t363 @t2 @t16 @t15 @t1 @t348) (=> @t397 @t388)))
% 48.28/48.57  (assume @p250 (forall (@list @t9 @t363 @t2 @t20 @t19 @t1 @t348) (=> @t397 @t390)))
% 48.28/48.57  (assume @p251 (forall (@list @t9 @t363 @t2 @t24 @t23 @t1 @t348) (=> @t397 @t392)))
% 48.28/48.57  (assume @p252 (forall (@list @t9 @t363 @t2 @t27 @t26 @t1 @t348) (=> @t397 @t394)))
% 48.28/48.57  (assume @p253 (forall (@list @t2 @t1 @t398 @t349 @t348) (=> @t400 (=> @t399 (=> (not (= @t349 (_ tptp.cast_d1608273229_b_c_f @t398))) @t350)))))
% 48.28/48.57  (assume @p254 (forall @t285 (=> @t275 (=> @t274 (_ (_ @t220 (_ (_ tptp.get_M_685446945_j_k_l @t272) tptp.attrs_1151927177tion_g)) tptp.finite2103212841t_char)))))
% 48.28/48.57  (assume @p255 (forall (@list @t401) (= (= @t404 tptp.none_R1587534007on_j_k) (not (exists (@list @t402) (= @t403 @t401))))))
% 48.28/48.57  (assume @p256 (forall @t135 (=> @t400 @t185)))
% 48.28/48.57  (assume @p257 (forall @t405 (=> @t400 (=> @t399 (_ (_ @t240 (_ (_ tptp.get_M_1723352102_h_i_l @t398) tptp.docume1175131570on_j_k)) tptp.none_element_ptr_a)))))
% 48.28/48.57  (assume @p258 (forall @t405 (=> @t400 (=> @t399 (_ (_ @t218 (_ (_ tptp.get_M_1536717772_h_i_l @t398) tptp.doctyp814403297on_j_k)) tptp.nil_char)))))
% 48.28/48.57  (assume @p259 (forall (@list @t2 @t1 @t398 @t280 @t66) (=> @t400 (=> @t399 (=> @t406 @t281)))))
% 48.28/48.57  (assume @p260 (forall (@list @t2 @t1 @t398 @t280 @t76) (=> @t400 (=> @t399 (=> @t406 @t283)))))
% 48.28/48.57  (assume @p261 (forall (@list @t2 @t1 @t398 @t276 @t107) (=> @t400 (=> @t399 @t277))))
% 48.28/48.57  (assume @p262 (forall (@list @t2 @t1 @t398 @t266 @t104) (=> @t400 (=> @t399 @t267))))
% 48.28/48.57  (assume @p263 (forall (@list @t2 @t1 @t398 @t278 @t101) (=> @t400 (=> @t399 @t279))))
% 48.28/48.57  (assume @p264 (forall @t294 (=> @t407 (=> @t400 @t293))))
% 48.28/48.57  (assume @p265 (forall @t292 (=> (forall @t291 (=> (_ (_ (_ tptp.heap_E2046843837tr_d_e @t289) tptp.new_do4779043_j_k_l) @t288) @t290)) @t407)))
% 48.28/48.57  (assume @p266 (_ tptp.l_new_1474790279_j_k_l tptp.type_w1479951274_j_k_l))
% 48.28/48.57  (assume @p267 (forall (@list @t2 @t398) (=> @t399 (_ tptp.is_doc2037328342tr_d_e @t398))))
% 48.28/48.57  (assume @p268 (forall @t405 (=> @t400 (=> @t399 (_ (_ @t216 (_ (_ tptp.get_M_986049031_h_i_l @t398) tptp.discon866287741on_j_k)) tptp.nil_no279930520tr_b_c)))))
% 48.28/48.57  (assume @p269 (forall @t285 (=> @t275 (=> @t274 (_ (_ @t216 (_ (_ tptp.get_M_88885319_j_k_l @t272) tptp.child_768225874tion_g)) tptp.nil_no279930520tr_b_c)))))
% 48.28/48.57  (assume @p270 (forall (@list @t252 @t408) (= (= @t254 @t410) (= @t409 @t252))))
% 48.28/48.57  (assume @p271 (forall (@list @t408) (= (_ tptp.cast_D1046746849_b_j_k @t409) @t410)))
% 48.28/48.57  (assume @p272 (forall @t416 (= (forall @t415 (not @t414)) @t412)))
% 48.28/48.57  (assume @p273 (forall @t416 (= (not @t412) (exists @t415 @t414))))
% 48.28/48.57  (assume @p274 (forall @t418 (=> @t261 (= @t417 @t257))))
% 48.28/48.57  (assume @p275 (forall @t421 (= (_ tptp.the_RO2055010943tion_j @t420) @t419)))
% 48.28/48.57  (assume @p276 (forall @t421 (not (= tptp.none_R125524722tion_j @t420))))
% 48.28/48.57  (assume @p277 (forall (@list @t257 @t419) (=> (= @t257 @t420) @t261)))
% 48.28/48.57  (assume @p278 (forall (@list @t423) (=> (not @t424) (not (forall (@list @t422) (not (= @t423 (_ tptp.some_R700141678tion_j @t422))))))))
% 48.28/48.57  (assume @p279 (forall (@list @t425 @t257) (=> (_ @t425 tptp.none_R125524722tion_j) (=> (forall @t45 (_ @t425 (_ tptp.some_R700141678tion_j @t40))) (_ @t425 @t257)))))
% 48.28/48.57  (assume @p280 (= (lambda @t436 (exists @t435 @t434)) (lambda @t431 (or @t430 (exists @t429 @t428)))))
% 48.28/48.57  (assume @p281 (= (lambda @t436 (forall @t435 @t434)) (lambda @t431 (and @t430 (forall @t429 @t428)))))
% 48.28/48.57  (assume @p282 (forall (@list @t411 @t437 @t423) (=> (=> @t412 @t438) (=> (=> @t424 @t438) (=> (forall (@list @t440 @t439) (=> (= @t411 (_ tptp.some_R700141678tion_j @t440)) (=> (= @t423 (_ tptp.some_R700141678tion_j @t439)) @t438))) @t438)))))
% 48.28/48.57  (assume @p283 (forall @t418 (=> @t261 (= @t257 @t417))))
% 48.28/48.57  (assume @p284 (forall (@list @t401 @t252) (= (= @t404 @t441) (= @t382 @t401))))
% 48.28/48.57  (assume @p285 (forall @t255 (= (_ tptp.cast_O1034441233_j_k_l @t382) @t441)))
% 48.28/48.57  (assume @p286 (forall @t418 (= @t260 (_ (_ (_ tptp.case_o1030391776tion_j true) (lambda @t442 false)) @t257))))
% 48.28/48.57  (assume @p287 (forall @t418 (= @t261 (_ (_ (_ tptp.case_o1030391776tion_j false) (lambda @t442 true)) @t257))))
% 48.28/48.57  (assume @p288 (forall (@list @t445 @t444 @t411) (=> (_ (_ (_ tptp.case_o1030391776tion_j @t445) @t444) @t411) (=> (=> @t412 (not @t445)) (not (forall (@list @t443) (=> (= @t411 (_ tptp.some_R700141678tion_j @t443)) (not (_ @t444 @t443)))))))))
% 48.28/48.57  (assume @p289 (forall @t447 (= (_ tptp.cast_n269450313tr_b_c @t156) @t446)))
% 48.28/48.57  (assume @p290 (forall (@list @t105 @t53) (= (= @t448 @t446) @t157)))
% 48.28/48.57  (assume @p291 (forall @t450 (=> @t449 (= (_ tptp.cast_e316309897tr_b_c (_ tptp.the_element_ptr_a @t448)) @t105))))
% 48.28/48.57  (assume @p292 (forall @t451 (not (_ tptp.is_ele1259807012tr_b_c @t154))))
% 48.28/48.57  (assume @p293 (forall @t447 (_ tptp.is_ele1259807012tr_b_c @t156)))
% 48.28/48.57  (assume @p294 (forall @t450 (=> @t449 (not (forall (@list @t452) (not (= @t105 (_ tptp.cast_e316309897tr_b_c @t452))))))))
% 48.28/48.57  (assume @p295 (forall @t455 (=> @t184 (=> @t454 (=> (=> (_ tptp.is_doc45233057_d_e_f @t349) (_ tptp.is_doc1417632087_j_k_l @t401)) (_ tptp.type_w1479951274_j_k_l @t453))))))
% 48.28/48.57  (assume @p296 (forall @t455 (=> @t262 (=> @t459 (=> (=> (_ (_ @t458 tptp.is_cha330921893_a_b_c) @t457) (not (= (_ (_ (_ tptp.case_o18599603on_h_i tptp.none_R417230014tion_h) tptp.cast_N1374991725_g_h_i) @t456) tptp.none_R417230014tion_h))) @t454)))))
% 48.28/48.57  (assume @p297 (= tptp.put_M_1937380872_j_k_l (_ (_ tptp.l_put_1584770338t_char tptp.get_C_592656865_j_k_l) tptp.put_C_229546338_j_k_l)))
% 48.28/48.57  (assume @p298 (forall @t451 (_ tptp.is_cha330921893_a_b_c @t154)))
% 48.28/48.57  (assume @p299 (forall @t450 (=> @t461 (not (forall (@list @t460) (not (= (_ tptp.cast_c164415100_b_a_c @t460) @t105)))))))
% 48.28/48.57  (assume @p300 (forall @t447 (not (_ tptp.is_cha330921893_a_b_c @t156))))
% 48.28/48.57  (assume @p301 (forall @t455 (=> @t264 (=> (_ tptp.type_w2078707819_j_k_l @t453) (=> (=> (_ (_ @t458 tptp.is_ele1259807012tr_b_c) @t457) (not (= (_ (_ (_ tptp.case_o1144239773on_h_i tptp.none_R509380180tion_g) tptp.cast_N1424394706on_h_i) @t456) tptp.none_R509380180tion_g))) @t459)))))
% 48.28/48.57  (assume @p302 (forall @t251 (=> @t262 @t462)))
% 48.28/48.57  (assume @p303 (forall @t251 (=> @t264 @t462)))
% 48.28/48.57  (assume @p304 (forall @t251 (=> @t184 @t462)))
% 48.28/48.57  (assume @p305 (= tptp.put_M_682984464_j_k_l (_ (_ tptp.l_put_1103319052_ptr_d tptp.get_E_312738192_j_k_l) tptp.put_E_1775770377_j_k_l)))
% 48.28/48.57  (assume @p306 (= tptp.put_M_1098917052_j_k_l (_ (_ tptp.l_put_2122145248tr_b_c tptp.get_E_312738192_j_k_l) tptp.put_E_1775770377_j_k_l)))
% 48.28/48.57  (assume @p307 (= tptp.put_M_1720094109_j_k_l (_ (_ tptp.l_put_1449921049t_char tptp.get_E_312738192_j_k_l) tptp.put_E_1775770377_j_k_l)))
% 48.28/48.57  (assume @p308 (= tptp.put_M_1724091798_j_k_l (_ (_ tptp.l_put_1666965382t_char tptp.get_E_312738192_j_k_l) tptp.put_E_1775770377_j_k_l)))
% 48.28/48.57  (assume @p309 (forall (@list @t53 @t9 @t464 @t2) (= (_ @t463 @t466) (_ @t463 @t2))))
% 48.28/48.57  (assume @p310 (forall (@list @t48 @t9 @t464 @t2) (= (_ @t467 @t466) (_ @t467 @t2))))
% 48.28/48.57  (assume @p311 (forall (@list @t349 @t9 @t401 @t2) (and (=> @t471 (= @t470 @t404)) (=> (not @t471) (= @t470 @t469)))))
% 48.28/48.57  (assume @p312 (forall (@list @t9 @t48 @t472 @t2) (= (_ @t468 (_ (_ (_ tptp.put_C_229546338_j_k_l @t48) @t472) @t2)) @t469)))
% 48.28/48.57  (assume @p313 (forall (@list @t9 @t53 @t473 @t2) (= (_ @t468 (_ (_ (_ tptp.put_E_1775770377_j_k_l @t53) @t473) @t2)) @t469)))
% 48.28/48.57  (assume @p314 (forall (@list @t9 @t67 @t252 @t2) (=> @t100 (= (_ @t468 (_ (_ (_ tptp.put_D_2126422573_h_i_l @t67) @t252) @t2)) @t469))))
% 48.28/48.57  (assume @p315 (forall (@list @t9 @t252 @t2) (= (_ @t468 (_ (_ @t465 @t252) @t2)) @t441)))
% 48.28/48.57  (assume @p316 (= tptp.put_M_257417239_h_i_l (_ (_ tptp.l_put_821218959t_char tptp.get_D_1192261494_j_k_l) tptp.put_D_2126422573_h_i_l)))
% 48.28/48.57  (assume @p317 (= tptp.put_M_139724992_h_i_l (_ (_ tptp.l_put_893346794tr_b_c tptp.get_D_1192261494_j_k_l) tptp.put_D_2126422573_h_i_l)))
% 48.28/48.57  (assume @p318 (= tptp.put_M_1442125025_h_i_l (_ (_ tptp.l_put_38398219_ptr_a tptp.get_D_1192261494_j_k_l) tptp.put_D_2126422573_h_i_l)))
% 48.28/48.57  (assume @p319 (= tptp.put_M_168144691_h_i_l (_ (_ tptp.l_put_1129034845_j_k_n tptp.get_D_1192261494_j_k_l) tptp.put_D_2126422573_h_i_l)))
% 48.28/48.57  (assume @p320 @t475)
% 48.28/48.57  (assume @p321 (forall @t450 (=> @t461 (= (_ tptp.cast_c164415100_b_a_c (_ tptp.the_ch963454248_ptr_b @t476)) @t105))))
% 48.28/48.57  (assume @p322 (forall @t451 (= (_ tptp.cast_n1518532508_a_b_c @t154) @t477)))
% 48.28/48.57  (assume @p323 (forall (@list @t105 @t48) (= (= @t476 @t477) @t155)))
% 48.28/48.57  (assume @p324 (_ (_ @t478 (_ (_ (_ tptp.put_M_674497586_h_i_l tptp.document_ptr) tptp.setter) tptp.v)) tptp.h2))
% 48.28/48.57  (assume @p325 (forall (@list @t479) (= (_ tptp.is_sha1522929624_b_j_k @t479) (_ tptp.is_sha1522929624_b_j_k (_ @t480 @t479)))))
% 48.28/48.57  (assume @p326 (forall (@list @t481) (= (_ tptp.getter (_ tptp.the_RO2055010943tion_j (_ tptp.cast_D1046746849_b_j_k (_ @t480 (_ tptp.cast_S988036065_b_j_k @t481))))) (_ tptp.getter @t481))))
% 48.28/48.57  (assume @p327 @t483)
% 48.28/48.57  (assume @p328 @t485)
% 48.28/48.57  (assume @p329 true)
% 48.28/48.57  (step @p330 (= tptp.heap_E808638982tr_d_e @t491) :rule refl :args (@t491))
% 48.28/48.57  (step @p331 (= tptp.heap_E73132893_ptr_a @t495) :rule refl :args (@t495))
% 48.28/48.57  (step @p332 (= tptp.heap_E1521571831t_unit @t499) :rule refl :args (@t499))
% 48.28/48.57  (step @p333 (= tptp.heap_E1683112692tion_m @t503) :rule refl :args (@t503))
% 48.28/48.57  (step @p334 (= tptp.heap_E1683112693tion_n @t513) :rule refl :args (@t513))
% 48.28/48.57  (step @p335 (= tptp.heap_E1679280842_ptr_b @t517) :rule refl :args (@t517))
% 48.28/48.57  (step @p336 (= tptp.heap_E1720378810tr_d_e @t521) :rule refl :args (@t521))
% 48.28/48.57  (step @p337 (= tptp.heap_E2092016297_ptr_a @t525) :rule refl :args (@t525))
% 48.28/48.57  (step @p338 (= tptp.heap_E1940720705tion_n @t528) :rule refl :args (@t528))
% 48.28/48.57  (step @p339 (= tptp.heap_E1940720704tion_m @t531) :rule refl :args (@t531))
% 48.28/48.57  (step @p340 (= tptp.heap_E1993614659t_unit @t534) :rule refl :args (@t534))
% 48.28/48.57  (step @p341 (= tptp.is_sha1522929624_b_j_k @t536) :rule refl :args (@t536))
% 48.28/48.57  (step @p342 (= tptp.l_new_410495338_j_k_l @t541) :rule refl :args (@t541))
% 48.28/48.57  (step @p343 (= tptp.l_new_540233301_j_k_l @t542) :rule refl :args (@t542))
% 48.28/48.57  (step @p344 (= tptp.l_new_1474790279_j_k_l @t543) :rule refl :args (@t543))
% 48.28/48.57  (step @p345 (= tptp.put_D_2126422573_h_i_l @t549) :rule refl :args (@t549))
% 48.28/48.57  (step @p346 :rule refl :args (@t552))
% 48.28/48.57  (step @p347 :rule refl :args (@t1))
% 48.28/48.57  (step @p348 :rule refl :args ((tptp.l_put_1129034844_j_k_m tptp.get_D_1192261494_j_k_l @t549 @t9 @t27 @t26)))
% 48.28/48.57  (step @p349 :rule refl :args (@t26))
% 48.28/48.57  (step @p350 :rule refl :args (@t27))
% 48.28/48.57  (step @p351 :rule refl :args (@t9))
% 48.28/48.57  (step @p352 :rule refl :args ((tptp.put_O_834343516_j_k_l @t546 @t403 @t544)))
% 48.28/48.57  (step @p353 :rule refl :args (@t544))
% 48.28/48.57  (step @p354 :rule refl :args (@t553))
% 48.28/48.57  (step @p355 :rule refl :args (@t554))
% 48.28/48.57  (step @p356 :rule cong :premises (@p355 @p354 @p353) :args (@t555))
% 48.28/48.57  (step @p357 :rule trans :premises (@p356 @p352))
% 48.28/48.57  (step @p358 :rule cong :premises (@p357) :args (@t556))
% 48.28/48.57  (step @p359 :rule refl :args (tptp.get_D_1192261494_j_k_l))
% 48.28/48.57  (step @p360 :rule cong :premises (@p359 @p358 @p351 @p350 @p349) :args (@t557))
% 48.28/48.57  (step @p361 :rule trans :premises (@p360 @p348))
% 48.28/48.57  (step @p362 :rule refl :args (@t474))
% 48.28/48.57  (step @p363 :rule ho_cong :premises (@p362 @p358))
% 48.28/48.57  (step @p364 :rule ho_cong :premises (@p363 @p351))
% 48.28/48.57  (step @p365 :rule ho_cong :premises (@p364 @p350))
% 48.28/48.57  (step @p366 :rule ho_cong :premises (@p365 @p349))
% 48.28/48.57  (step @p367 :rule cong :premises (@p366 @p361) :args ((= (_ (_ (_ (_ @t474 @t556) @t9) @t27) @t26) @t557)))
% 48.28/48.57  (step @p368 :rule symm :premises (@p367))
% 48.28/48.57  (step @p369 :rule refl :args (@t559))
% 48.28/48.57  (step @p370 :rule eq_resolve :premises (@p369 @p368))
% 48.28/48.57  (step @p371 :rule refl :args (tptp.put_O_834343516_j_k_l))
% 48.28/48.57  (step @p372 :rule ho_cong :premises (@p371 @p355))
% 48.28/48.57  (step @p373 :rule ho_cong :premises (@p372 @p354))
% 48.28/48.57  (step @p374 :rule ho_cong :premises (@p373 @p353))
% 48.28/48.57  (step @p375 :rule cong :premises (@p374 @p357) :args ((= (_ (_ (_ tptp.put_O_834343516_j_k_l @t554) @t553) @t544) @t555)))
% 48.28/48.57  (step @p376 :rule symm :premises (@p375))
% 48.28/48.57  (step @p377 :rule refl :args (@t547))
% 48.28/48.57  (step @p378 :rule eq_resolve :premises (@p377 @p376))
% 48.28/48.57  (step @p379 :rule refl :args (@t403))
% 48.28/48.57  (step @p380 :rule cong :premises (@p379 @p354) :args ((= @t403 @t553)))
% 48.28/48.57  (step @p381 :rule symm :premises (@p380))
% 48.28/48.57  (step @p382 :rule eq_resolve :premises (@p379 @p381))
% 48.28/48.57  (step @p383 :rule refl :args (@t546))
% 48.28/48.57  (step @p384 :rule cong :premises (@p383 @p355) :args ((= @t546 @t554)))
% 48.28/48.57  (step @p385 :rule symm :premises (@p384))
% 48.28/48.57  (step @p386 :rule eq_resolve :premises (@p383 @p385))
% 48.28/48.57  (step @p387 :rule ho_cong :premises (@p371 @p386))
% 48.28/48.57  (step @p388 :rule ho_cong :premises (@p387 @p382))
% 48.28/48.57  (step @p389 :rule ho_cong :premises (@p388 @p353))
% 48.28/48.57  (step @p390 :rule trans :premises (@p389 @p378))
% 48.28/48.57  (step @p391 :rule cong :premises (@p390) :args (@t549))
% 48.28/48.57  (step @p392 :rule ho_cong :premises (@p362 @p391))
% 48.28/48.57  (step @p393 :rule ho_cong :premises (@p392 @p351))
% 48.28/48.57  (step @p394 :rule ho_cong :premises (@p393 @p350))
% 48.28/48.57  (step @p395 :rule ho_cong :premises (@p394 @p349))
% 48.28/48.57  (step @p396 :rule trans :premises (@p395 @p370))
% 48.28/48.57  (step @p397 :rule refl :args (@t2))
% 48.28/48.57  (step @p398 :rule cong :premises (@p397 @p396 @p347) :args (@t560))
% 48.28/48.57  (step @p399 :rule cong :premises (@p398) :args (@t561))
% 48.28/48.57  (step @p400 :rule refl :args (@t563))
% 48.28/48.57  (step @p401 :rule nary_cong :premises (@p400 @p399 @p346) :args (@t564))
% 48.28/48.57  (step @p402 :rule cong :premises (@p401) :args ((forall @t565 @t564)))
% 48.28/48.57  (step @p403 :rule refl :args (@t552))
% 48.28/48.57  (step @p404 :rule refl :args (@t1))
% 48.28/48.57  (step @p405 :rule refl :args (@t566))
% 48.28/48.57  (step @p406 :rule refl :args (@t2))
% 48.28/48.57  (step @p407 :rule cong :premises (@p406 @p405 @p404) :args (@t567))
% 48.28/48.57  (step @p408 :rule cong :premises (@p407) :args (@t568))
% 48.28/48.57  (step @p409 :rule refl :args (@t563))
% 48.28/48.57  (step @p410 :rule nary_cong :premises (@p409 @p408 @p403) :args (@t569))
% 48.28/48.57  (step @p411 :rule cong :premises (@p410) :args ((forall @t565 @t569)))
% 48.28/48.57  (step @p412 :rule trans :premises (@p411 @p402))
% 48.28/48.57  (step @p413 :rule refl :args (@t26))
% 48.28/48.57  (step @p414 :rule refl :args (@t27))
% 48.28/48.57  (step @p415 :rule refl :args (@t9))
% 48.28/48.57  (step @p416 :rule refl :args (@t474))
% 48.28/48.57  (step @p417 :rule ho_cong :premises (@p416 @p345))
% 48.28/48.57  (step @p418 :rule refl :args (tptp.put_M_674497586_h_i_l))
% 48.28/48.57  (step @p419 :rule cong :premises (@p418 @p417) :args (@t475))
% 48.28/48.57  (step @p420 :rule eq_resolve :premises (@p320 @p419))
% 48.28/48.57  (step @p421 :rule ho_cong :premises (@p420 @p415 @p414 @p413))
% 48.28/48.57  (step @p422 :rule cong :premises (@p406 @p421 @p404) :args (@t571))
% 48.28/48.57  (step @p423 :rule cong :premises (@p422) :args (@t572))
% 48.28/48.57  (step @p424 :rule nary_cong :premises (@p409 @p423 @p403) :args (@t573))
% 48.28/48.57  (step @p425 :rule cong :premises (@p424) :args (@t574))
% 48.28/48.57  (step @p426 :rule trans :premises (@p425 @p412))
% 48.28/48.57  (step @p427 :rule quant-merge-prenex :args ((= (forall @t32 @t576) @t574)))
% 48.28/48.57  (step @p428 :rule alpha_equiv :args (@t577 (@list @t550) (@list @t504)))
% 48.28/48.57  (step @p429 :rule refl :args (@t572))
% 48.28/48.57  (step @p430 :rule nary_cong :premises (@p400 @p429 @p428) :args (@t578))
% 48.28/48.57  (step @p431 :rule quant-miniscope-or :args ((= @t576 @t578)))
% 48.28/48.57  (step @p432 :rule trans :premises (@p431 @p430))
% 48.28/48.57  (step @p433 :rule symm :premises (@p432))
% 48.28/48.57  (step @p434 :rule cong :premises (@p433) :args ((forall @t32 (or @t563 @t572 @t581))))
% 48.28/48.57  (step @p435 :rule trans :premises (@p434 @p427))
% 48.28/48.57  (step @p436 :rule refl :args (@t581))
% 48.28/48.57  (step @p437 :rule refl :args ((tptp.heap_E494191872t_unit @t2 @t28 @t1)))
% 48.28/48.57  (step @p438 :rule refl :args (@t570))
% 48.28/48.57  (step @p439 :rule cong :premises (@p397 @p438 @p347) :args (@t571))
% 48.28/48.57  (step @p440 :rule trans :premises (@p439 @p437))
% 48.28/48.57  (step @p441 :rule refl :args (@t11))
% 48.28/48.57  (step @p442 :rule ho_cong :premises (@p441 @p438))
% 48.28/48.57  (step @p443 :rule ho_cong :premises (@p442 @p347))
% 48.28/48.57  (step @p444 :rule cong :premises (@p443 @p440) :args ((= (_ (_ @t11 @t570) @t1) @t571)))
% 48.28/48.57  (step @p445 :rule symm :premises (@p444))
% 48.28/48.57  (step @p446 :rule refl :args (@t29))
% 48.28/48.57  (step @p447 :rule eq_resolve :premises (@p446 @p445))
% 48.28/48.57  (step @p448 :rule refl :args (@t28))
% 48.28/48.57  (step @p449 :rule cong :premises (@p448 @p438) :args ((= @t28 @t570)))
% 48.28/48.57  (step @p450 :rule symm :premises (@p449))
% 48.28/48.57  (step @p451 :rule eq_resolve :premises (@p448 @p450))
% 48.28/48.57  (step @p452 :rule ho_cong :premises (@p441 @p451))
% 48.28/48.57  (step @p453 :rule ho_cong :premises (@p452 @p347))
% 48.28/48.57  (step @p454 :rule trans :premises (@p453 @p447))
% 48.28/48.57  (step @p455 :rule cong :premises (@p454) :args (@t582))
% 48.28/48.57  (step @p456 :rule refl :args (@t562))
% 48.28/48.57  (step @p457 :rule refl :args (@t13))
% 48.28/48.57  (step @p458 :rule cong :premises (@p457 @p456) :args ((= @t13 @t562)))
% 48.28/48.57  (step @p459 :rule symm :premises (@p458))
% 48.28/48.57  (step @p460 :rule eq_resolve :premises (@p457 @p459))
% 48.28/48.57  (step @p461 :rule cong :premises (@p351 @p460) :args (@t583))
% 48.28/48.57  (step @p462 :rule nary_cong :premises (@p461 @p455 @p436) :args (@t584))
% 48.28/48.57  (step @p463 :rule cong :premises (@p462) :args ((forall @t32 @t584)))
% 48.28/48.57  (step @p464 :rule trans :premises (@p463 @p435))
% 48.28/48.57  (step @p465 :rule aci_norm :args ((= (or @t583 (or @t582 @t581)) @t584)))
% 48.28/48.57  (step @p466 :rule bool-impl-elim :args (@t29 @t581))
% 48.28/48.57  (step @p467 :rule refl :args (@t583))
% 48.28/48.57  (step @p468 :rule nary_cong :premises (@p467 @p466) :args ((or @t583 @t585)))
% 48.28/48.57  (step @p469 :rule trans :premises (@p468 @p465))
% 48.28/48.57  (step @p470 :rule refl :args (@t585))
% 48.28/48.57  (step @p471 :rule bool-double-not-elim :args (@t583))
% 48.28/48.57  (step @p472 :rule nary_cong :premises (@p471 @p470) :args ((or (not @t586) @t585)))
% 48.28/48.57  (step @p473 :rule bool-impl-elim :args (@t586 @t585))
% 48.28/48.57  (step @p474 :rule trans :premises (@p473 @p472))
% 48.28/48.57  (step @p475 :rule trans :premises (@p474 @p469))
% 48.28/48.57  (step @p476 :rule cong :premises (@p475) :args ((forall @t32 (=> @t586 @t585))))
% 48.28/48.57  (step @p477 :rule trans :premises (@p476 @p464))
% 48.28/48.57  (step @p478 :rule eq-symm :args (@t579 @t580))
% 48.28/48.57  (step @p479 :rule cong :premises (@p478) :args (@t587))
% 48.28/48.57  (step @p480 :rule beta-reduce :args ((= (_ (lambda @t589 (forall @t510 (= @t588 @t580))) @t1) @t587)))
% 48.28/48.57  (step @p481 :rule trans :premises (@p480 @p479))
% 48.28/48.57  (step @p482 :rule eq-symm :args (@t580 @t588))
% 48.28/48.57  (step @p483 :rule cong :premises (@p482) :args (@t590))
% 48.28/48.57  (step @p484 :rule cong :premises (@p483) :args (@t591))
% 48.28/48.57  (step @p485 :rule beta-reduce :args ((= (_ (lambda @t539 (forall @t510 (= (tptp.heap_E1038710093tion_n @t489 @t551 @t504) @t588))) @t2) @t591)))
% 48.28/48.57  (step @p486 :rule trans :premises (@p485 @p484))
% 48.28/48.57  (step @p487 :rule refl :args (@t504))
% 48.28/48.57  (step @p488 :rule refl :args (@t551))
% 48.28/48.57  (step @p489 :rule refl :args (@t5))
% 48.28/48.57  (step @p490 :rule cong :premises (@p489 @p488) :args ((= @t5 @t551)))
% 48.28/48.57  (step @p491 :rule symm :premises (@p490))
% 48.28/48.57  (step @p492 :rule eq_resolve :premises (@p489 @p491))
% 48.28/48.57  (step @p493 :rule refl :args (@t488))
% 48.28/48.57  (step @p494 :rule cong :premises (@p493 @p492 @p487) :args (@t592))
% 48.28/48.57  (step @p495 :rule refl :args (@t489))
% 48.28/48.57  (step @p496 :rule cong :premises (@p495 @p492 @p487) :args (@t593))
% 48.28/48.57  (step @p497 :rule cong :premises (@p496 @p494) :args (@t594))
% 48.28/48.57  (step @p498 :rule cong :premises (@p497) :args (@t595))
% 48.28/48.57  (step @p499 :rule cong :premises (@p498) :args (@t596))
% 48.28/48.57  (step @p500 :rule beta-reduce :args ((= @t600 @t596)))
% 48.28/48.57  (step @p501 :rule trans :premises (@p500 @p499))
% 48.28/48.57  (step @p502 :rule ho_cong :premises (@p501 @p406))
% 48.28/48.57  (step @p503 :rule trans :premises (@p502 @p486))
% 48.28/48.57  (step @p504 :rule ho_cong :premises (@p503 @p404))
% 48.28/48.57  (step @p505 :rule trans :premises (@p504 @p481))
% 48.28/48.57  (step @p506 :rule refl :args (@t29))
% 48.28/48.57  (step @p507 :rule cong :premises (@p506 @p505) :args (@t601))
% 48.28/48.57  (step @p508 :rule eq-symm :args (@t13 @t9))
% 48.28/48.57  (step @p509 :rule cong :premises (@p508) :args (@t14))
% 48.28/48.57  (step @p510 :rule cong :premises (@p509 @p507) :args (@t602))
% 48.28/48.57  (step @p511 :rule cong :premises (@p510) :args ((forall @t32 @t602)))
% 48.28/48.57  (step @p512 :rule trans :premises (@p511 @p477))
% 48.28/48.57  (step @p513 :rule refl :args (@t5))
% 48.28/48.57  (step @p514 :rule refl :args (@t597))
% 48.28/48.57  (step @p515 :rule refl :args (@t506))
% 48.28/48.57  (step @p516 :rule cong :premises (@p515 @p514) :args ((= @t506 @t597)))
% 48.28/48.57  (step @p517 :rule symm :premises (@p516))
% 48.28/48.57  (step @p518 :rule eq_resolve :premises (@p515 @p517))
% 48.28/48.57  (step @p519 :rule refl :args (@t598))
% 48.28/48.57  (step @p520 :rule refl :args (@t508))
% 48.28/48.57  (step @p521 :rule cong :premises (@p520 @p519) :args ((= @t508 @t598)))
% 48.28/48.57  (step @p522 :rule symm :premises (@p521))
% 48.28/48.57  (step @p523 :rule eq_resolve :premises (@p520 @p522))
% 48.28/48.57  (step @p524 :rule cong :premises (@p523 @p518) :args (@t509))
% 48.28/48.57  (step @p525 :rule cong :premises (@p524) :args (@t511))
% 48.28/48.57  (step @p526 :rule cong :premises (@p525) :args (@t513))
% 48.28/48.57  (step @p527 :rule trans :premises (@p334 @p526))
% 48.28/48.57  (step @p528 :rule ho_cong :premises (@p527 @p513))
% 48.28/48.57  (step @p529 :rule ho_cong :premises (@p528 @p406))
% 48.28/48.57  (step @p530 :rule ho_cong :premises (@p529 @p404))
% 48.28/48.57  (step @p531 :rule cong :premises (@p506 @p530) :args (@t30))
% 48.28/48.57  (step @p532 :rule refl :args (@t14))
% 48.28/48.57  (step @p533 :rule cong :premises (@p532 @p531) :args (@t31))
% 48.28/48.57  (step @p534 :rule cong :premises (@p533) :args (@t33))
% 48.28/48.57  (step @p535 :rule trans :premises (@p534 @p512))
% 48.28/48.57  (step @p536 :rule trans :premises (@p535 @p426))
% 48.28/48.57  (step @p537 :rule eq_resolve :premises (@p5 @p536))
% 48.28/48.57  (step @p538 :rule refl :args (@t607))
% 48.28/48.57  (step @p539 :rule refl :args (tptp.h2))
% 48.28/48.57  (step @p540 :rule refl :args (tptp.v))
% 48.28/48.57  (step @p541 :rule refl :args (tptp.setter))
% 48.28/48.57  (step @p542 :rule refl :args (tptp.document_ptr))
% 48.28/48.57  (step @p543 :rule eq-refl :args (@t556))
% 48.28/48.57  (step @p544 :rule skolem_intro :args (@t608))
% 48.28/48.57  (step @p545 :rule refl :args (@t556))
% 48.28/48.57  (step @p546 :rule cong :premises (@p545 @p544) :args ((= @t556 @t608)))
% 48.28/48.57  (step @p547 :rule trans :premises (@p546 @p543))
% 48.28/48.57  (step @p548 :rule true_elim :premises (@p547))
% 48.28/48.57  (step @p549 :rule refl :args (tptp.get_D_1192261494_j_k_l))
% 48.28/48.57  (step @p550 :rule cong :premises (@p549 @p548 @p542 @p541 @p540) :args (@t609))
% 48.28/48.57  (step @p551 :rule refl :args (tptp.h))
% 48.28/48.57  (step @p552 :rule cong :premises (@p551 @p550 @p539) :args (@t610))
% 48.28/48.57  (step @p553 :rule cong :premises (@p552) :args (@t611))
% 48.28/48.57  (step @p554 :rule refl :args (@t613))
% 48.28/48.57  (step @p555 :rule nary_cong :premises (@p554 @p553 @p538) :args (@t614))
% 48.28/48.57  (step @p556 :rule refl :args (@t615))
% 48.28/48.57  (step @p557 :rule cong :premises (@p556 @p555) :args ((=> @t615 @t614)))
% 48.28/48.57  (assume-push @p822 @t615)
% 48.28/48.57  (step @p559 :rule instantiate :premises (@p537) :args ((@list tptp.shadow_root_ptr tptp.document_ptr tptp.h tptp.setter tptp.v tptp.h2 tptp.getter @t606)))
% 48.28/48.57  (step-pop @p823 :rule scope :premises (@p559))
% 48.28/48.57  (step @p560 :rule process_scope :premises (@p823) :args (@t614))
% 48.28/48.57  (step @p562 :rule eq_resolve :premises (@p560 @p557))
% 48.28/48.57  (step @p563 :rule implies_elim :premises (@p562))
% 48.28/48.57  (step @p564 :rule chain_m_resolution :premises (@p563 @p537) :args (@t619 @t620 (@list @t615)))
% 48.28/48.57  (step @p565 :rule eq-symm :args (@t604 @t605))
% 48.28/48.57  (step @p566 :rule cong :premises (@p565) :args (@t621))
% 48.28/48.57  (step @p567 :rule beta-reduce :args ((= (_ (lambda @t589 (forall @t510 (= @t622 @t605))) tptp.h2) @t621)))
% 48.28/48.57  (step @p568 :rule trans :premises (@p567 @p566))
% 48.28/48.57  (step @p569 :rule eq-symm :args (@t605 @t622))
% 48.28/48.57  (step @p570 :rule cong :premises (@p569) :args (@t623))
% 48.28/48.57  (step @p571 :rule cong :premises (@p570) :args (@t624))
% 48.28/48.57  (step @p572 :rule beta-reduce :args ((= (_ (lambda @t539 (forall @t510 (= (tptp.heap_E1038710093tion_n @t489 @t603 @t504) @t622))) tptp.h) @t624)))
% 48.28/48.57  (step @p573 :rule trans :premises (@p572 @p571))
% 48.28/48.57  (step @p574 :rule refl :args (@t603))
% 48.28/48.57  (step @p575 :rule refl :args (@t484))
% 48.28/48.57  (step @p576 :rule cong :premises (@p575 @p574) :args ((= @t484 @t603)))
% 48.28/48.57  (step @p577 :rule symm :premises (@p576))
% 48.28/48.57  (step @p578 :rule eq_resolve :premises (@p575 @p577))
% 48.28/48.57  (step @p579 :rule cong :premises (@p493 @p578 @p487) :args (@t625))
% 48.28/48.57  (step @p580 :rule cong :premises (@p495 @p578 @p487) :args (@t626))
% 48.28/48.57  (step @p581 :rule cong :premises (@p580 @p579) :args (@t627))
% 48.28/48.57  (step @p582 :rule cong :premises (@p581) :args (@t628))
% 48.28/48.57  (step @p583 :rule cong :premises (@p582) :args (@t629))
% 48.28/48.57  (step @p584 :rule beta-reduce :args ((= @t630 @t629)))
% 48.28/48.57  (step @p585 :rule trans :premises (@p584 @p583))
% 48.28/48.57  (step @p586 :rule ho_cong :premises (@p585 @p551))
% 48.28/48.57  (step @p587 :rule trans :premises (@p586 @p573))
% 48.28/48.57  (step @p588 :rule ho_cong :premises (@p587 @p539))
% 48.28/48.57  (step @p589 :rule trans :premises (@p588 @p568))
% 48.28/48.57  (step @p590 :rule cong :premises (@p589) :args ((not (_ (_ @t630 tptp.h) tptp.h2))))
% 48.28/48.57  (step @p591 :rule refl :args (@t484))
% 48.28/48.57  (step @p592 :rule ho_cong :premises (@p527 @p591))
% 48.28/48.57  (step @p593 :rule ho_cong :premises (@p592 @p551))
% 48.28/48.57  (step @p594 :rule ho_cong :premises (@p593 @p539))
% 48.28/48.57  (step @p595 :rule cong :premises (@p594) :args (@t485))
% 48.28/48.57  (step @p596 :rule trans :premises (@p595 @p590))
% 48.28/48.57  (step @p597 :rule eq_resolve :premises (@p328 @p596))
% 48.28/48.57  (step @p598 :rule skolemize :premises (@p597))
% 48.28/48.57  (step @p599 :rule refl :args (@t612))
% 48.28/48.57  (step @p600 :rule refl :args (@t482))
% 48.28/48.57  (step @p601 :rule cong :premises (@p600 @p599) :args ((= @t482 @t612)))
% 48.28/48.57  (step @p602 :rule symm :premises (@p601))
% 48.28/48.57  (step @p603 :rule eq_resolve :premises (@p600 @p602))
% 48.28/48.57  (step @p604 :rule cong :premises (@p542 @p603) :args (@t631))
% 48.28/48.57  (step @p605 :rule cong :premises (@p604) :args ((not @t631)))
% 48.28/48.57  (step @p606 :rule eq-symm :args (@t482 tptp.document_ptr))
% 48.28/48.57  (step @p607 :rule cong :premises (@p606) :args (@t483))
% 48.28/48.57  (step @p608 :rule trans :premises (@p607 @p605))
% 48.28/48.57  (step @p609 :rule eq_resolve :premises (@p327 @p608))
% 48.28/48.57  (step @p610 :rule cnf_or_pos :args (@t619))
% 48.28/48.57  (step @p611 :rule reordering :premises (@p610) :args ((or @t613 @t607 @t618 (not @t619))))
% 48.28/48.57  (step @p612 :rule chain_m_resolution :premises (@p611 @p609 @p598 @p564) :args (@t618 (@list true true false) (@list @t613 @t607 @t619)))
% 48.28/48.57  (step @p613 :rule refl :args ((tptp.heap_E494191872t_unit tptp.h @t633 tptp.h2)))
% 48.28/48.57  (step @p614 :rule refl :args (tptp.h2))
% 48.28/48.57  (step @p615 :rule refl :args (@t634))
% 48.28/48.57  (step @p616 :rule refl :args (tptp.h))
% 48.28/48.57  (step @p617 :rule cong :premises (@p616 @p615 @p614) :args (@t635))
% 48.28/48.57  (step @p618 :rule trans :premises (@p617 @p613))
% 48.28/48.57  (step @p619 :rule refl :args (@t478))
% 48.28/48.57  (step @p620 :rule ho_cong :premises (@p619 @p615))
% 48.28/48.57  (step @p621 :rule ho_cong :premises (@p620 @p614))
% 48.28/48.57  (step @p622 :rule cong :premises (@p621 @p618) :args ((= (_ (_ @t478 @t634) tptp.h2) @t635)))
% 48.28/48.57  (step @p623 :rule symm :premises (@p622))
% 48.28/48.57  (step @p624 :rule refl :args ((_ (_ @t478 @t633) tptp.h2)))
% 48.28/48.57  (step @p625 :rule eq_resolve :premises (@p624 @p623))
% 48.28/48.57  (step @p626 :rule refl :args (@t633))
% 48.28/48.57  (step @p627 :rule cong :premises (@p626 @p615) :args ((= @t633 @t634)))
% 48.28/48.57  (step @p628 :rule symm :premises (@p627))
% 48.28/48.57  (step @p629 :rule eq_resolve :premises (@p626 @p628))
% 48.28/48.57  (step @p630 :rule eq-refl :args (@t549))
% 48.28/48.57  (step @p631 :rule skolem_intro :args (@t632))
% 48.28/48.57  (step @p632 :rule refl :args (@t549))
% 48.28/48.57  (step @p633 :rule cong :premises (@p632 @p631) :args ((= @t549 @t632)))
% 48.28/48.57  (step @p634 :rule trans :premises (@p633 @p630))
% 48.28/48.57  (step @p635 :rule true_elim :premises (@p634))
% 48.28/48.57  (step @p636 :rule ho_cong :premises (@p416 @p635))
% 48.28/48.57  (step @p637 :rule ho_cong :premises (@p636 @p542))
% 48.28/48.57  (step @p638 :rule ho_cong :premises (@p637 @p541))
% 48.28/48.57  (step @p639 :rule ho_cong :premises (@p638 @p540))
% 48.28/48.57  (step @p640 :rule trans :premises (@p639 @p629))
% 48.28/48.57  (step @p641 :rule refl :args (@t478))
% 48.28/48.57  (step @p642 :rule ho_cong :premises (@p641 @p640))
% 48.28/48.57  (step @p643 :rule ho_cong :premises (@p642 @p539))
% 48.28/48.57  (step @p644 :rule trans :premises (@p643 @p625))
% 48.28/48.57  (step @p645 :rule ho_cong :premises (@p420 @p542))
% 48.28/48.57  (step @p646 :rule ho_cong :premises (@p645 @p541))
% 48.28/48.57  (step @p647 :rule ho_cong :premises (@p646 @p540))
% 48.28/48.57  (step @p648 :rule ho_cong :premises (@p641 @p647))
% 48.28/48.57  (step @p649 :rule ho_cong :premises (@p648 @p539))
% 48.28/48.57  (step @p650 :rule trans :premises (@p649 @p644))
% 48.28/48.57  (step @p651 :rule eq_resolve :premises (@p324 @p650))
% 48.28/48.57  (step @p652 :rule bool-double-not-elim :args (@t617))
% 48.28/48.57  (step @p653 :rule refl :args (@t637))
% 48.28/48.57  (step @p654 :rule refl :args (@t638))
% 48.28/48.57  (step @p655 :rule nary_cong :premises (@p654 @p653 @p652) :args ((or @t638 @t637 (not @t618))))
% 48.28/48.57  (assume-push @p824 @t635)
% 48.28/48.57  (assume-push @p825 @t636)
% 48.28/48.57  (assume-push @p826 @t618)
% 48.28/48.57  (step @p659 :rule evaluate :args (@t639))
% 48.28/48.57  (step @p660 :rule true_intro :premises (@p651))
% 48.28/48.57  (step @p661 :rule symm :premises (@p825))
% 48.28/48.57  (step @p662 :rule cong :premises (@p549 @p661 @p542 @p541 @p540) :args (@t616))
% 48.28/48.57  (step @p663 :rule cong :premises (@p551 @p662 @p539) :args (@t617))
% 48.28/48.57  (step @p664 :rule false_intro :premises (@p612))
% 48.28/48.57  (step @p665 :rule symm :premises (@p664))
% 48.28/48.57  (step @p666 :rule trans :premises (@p665 @p663 @p660))
% 48.28/48.57  (step @p667 false :rule eq_resolve :premises (@p666 @p659))
% 48.28/48.57  (step-pop @p827 :rule scope :premises (@p667))
% 48.28/48.57  (step-pop @p828 :rule scope :premises (@p827))
% 48.28/48.57  (step-pop @p829 :rule scope :premises (@p828))
% 48.28/48.57  (step @p668 :rule process_scope :premises (@p829) :args (false))
% 48.28/48.57  (step @p672 :rule not_and :premises (@p668))
% 48.28/48.57  (step @p673 :rule eq_resolve :premises (@p672 @p655))
% 48.28/48.57  (step @p674 :rule chain_m_resolution :premises (@p673 @p651 @p612) :args (@t637 (@list false true) (@list @t635 @t617)))
% 48.28/48.57  ; WARNING: add trust step for TRUST
% 48.28/48.57  ; trust TRUST THEORY_LEMMA
% 48.28/48.57  (step @p675 :rule trust :premises () :args ((or @t636 @t646)))
% 48.28/48.57  (step @p676 :rule chain_m_resolution :premises (@p675 @p674) :args (@t646 (@list true) (@list @t636)))
% 48.28/48.57  (step @p677 :rule refl :args (@t649))
% 48.28/48.57  (step @p678 :rule eq-refl :args (@t652))
% 48.28/48.57  (step @p679 :rule beta-reduce :args ((= (_ @t653 @t640) @t652)))
% 48.28/48.57  (step @p680 :rule refl :args (@t640))
% 48.28/48.57  (step @p681 :rule beta-reduce :args ((= (_ @t654 @t641) @t653)))
% 48.28/48.57  (step @p682 :rule refl :args (@t641))
% 48.28/48.57  (step @p683 :rule beta-reduce :args ((= @t655 @t654)))
% 48.28/48.57  (step @p684 :rule ho_cong :premises (@p683 @p682))
% 48.28/48.57  (step @p685 :rule trans :premises (@p684 @p681))
% 48.28/48.57  (step @p686 :rule ho_cong :premises (@p685 @p680))
% 48.28/48.57  (step @p687 :rule trans :premises (@p686 @p679))
% 48.28/48.57  (step @p688 :rule beta-reduce :args ((= @t656 @t652)))
% 48.28/48.57  (step @p689 :rule cong :premises (@p688 @p687) :args ((= @t656 @t658)))
% 48.28/48.57  (step @p690 :rule trans :premises (@p689 @p678))
% 48.28/48.57  (step @p691 :rule refl :args (@t642))
% 48.28/48.57  (step @p692 :rule ho_cong :premises (@p631 @p691))
% 48.28/48.57  (step @p693 :rule ho_cong :premises (@p692 @p682))
% 48.28/48.57  (step @p694 :rule ho_cong :premises (@p693 @p680))
% 48.28/48.57  (step @p695 :rule ho_cong :premises (@p631 @p691 @p682 @p680))
% 48.28/48.57  (step @p696 :rule cong :premises (@p695 @p694) :args ((= @t644 @t659)))
% 48.28/48.57  (step @p697 :rule eq-symm :args (@t659 @t644))
% 48.28/48.57  (step @p698 :rule trans :premises (@p697 @p696 @p690))
% 48.28/48.57  (step @p699 :rule true_elim :premises (@p698))
% 48.28/48.57  (step @p700 :rule cong :premises (@p699 @p677) :args (@t660))
% 48.28/48.57  (step @p701 :rule refl :args (@t661))
% 48.28/48.57  (step @p702 :rule nary_cong :premises (@p701 @p700) :args (@t662))
% 48.28/48.57  (step @p703 :rule eq-symm :args (@t649 @t659))
% 48.28/48.57  (step @p704 :rule eq-symm :args (@t648 @t647))
% 48.28/48.57  (step @p705 :rule nary_cong :premises (@p704 @p703) :args ((and (= @t648 @t647) (= @t649 @t659))))
% 48.28/48.57  (step @p706 :rule trans :premises (@p705 @p702))
% 48.28/48.57  (step @p707 :rule evaluate :args ((and true true)))
% 48.28/48.57  (step @p708 :rule refl :args (@t663))
% 48.28/48.57  (step @p709 :rule trans :premises (@p708 @p687))
% 48.28/48.57  (step @p710 :rule cong :premises (@p687 @p709) :args (@t664))
% 48.28/48.57  (step @p711 :rule trans :premises (@p710 @p678))
% 48.28/48.57  (step @p712 :rule eq-refl :args (@t657))
% 48.28/48.57  (step @p713 :rule nary_cong :premises (@p712 @p711) :args ((and (= @t657 @t657) @t664)))
% 48.28/48.57  (step @p714 :rule trans :premises (@p713 @p707))
% 48.28/48.57  (step @p715 :rule skolem_intro :args (@t648))
% 48.28/48.57  (step @p716 :rule trans :premises (@p715 @p693))
% 48.28/48.57  (step @p717 :rule ho_cong :premises (@p716 @p680))
% 48.28/48.57  (step @p718 :rule cong :premises (@p694 @p717) :args (@t660))
% 48.28/48.57  (step @p719 :rule cong :premises (@p693 @p716) :args (@t661))
% 48.28/48.57  (step @p720 :rule nary_cong :premises (@p719 @p718) :args (@t662))
% 48.28/48.57  (step @p721 :rule trans :premises (@p705 @p720 @p714))
% 48.28/48.57  (step @p722 :rule true_elim :premises (@p721))
% 48.28/48.57  (step @p723 :rule eq_resolve :premises (@p722 @p706))
% 48.28/48.57  (step @p724 :rule and_elim :premises (@p723) :args (1))
% 48.28/48.57  (step @p725 :rule refl :args (@t665))
% 48.28/48.57  (step @p726 :rule cong :premises (@p390 @p725) :args (@t666))
% 48.28/48.57  (step @p727 :rule cong :premises (@p726) :args ((forall @t548 @t666)))
% 48.28/48.57  (step @p728 :rule eq-symm :args (@t665 @t547))
% 48.28/48.57  (step @p729 :rule beta-reduce :args ((= @t667 @t547)))
% 48.28/48.57  (step @p730 :rule refl :args (@t665))
% 48.28/48.57  (step @p731 :rule cong :premises (@p730 @p729) :args (@t668))
% 48.28/48.57  (step @p732 :rule trans :premises (@p731 @p728))
% 48.28/48.57  (step @p733 :rule cong :premises (@p732) :args (@t669))
% 48.28/48.57  (step @p734 :rule trans :premises (@p733 @p727))
% 48.28/48.57  (step @p735 :rule quant-unused-vars :args ((= (forall @t548 true) true)))
% 48.28/48.57  (step @p736 :rule eq-refl :args (@t667))
% 48.28/48.57  (step @p737 :rule cong :premises (@p736) :args ((forall @t548 (= @t667 @t667))))
% 48.28/48.57  (step @p738 :rule trans :premises (@p737 @p735))
% 48.28/48.57  (step @p739 :rule refl :args (@t667))
% 48.28/48.57  (step @p740 :rule refl :args (@t544))
% 48.28/48.57  (step @p741 :rule refl :args (@t402))
% 48.28/48.57  (step @p742 :rule refl :args (@t545))
% 48.28/48.57  (step @p743 :rule ho_cong :premises (@p631 @p742 @p741 @p740))
% 48.28/48.57  (step @p744 :rule cong :premises (@p743 @p739) :args (@t668))
% 48.28/48.57  (step @p745 :rule cong :premises (@p744) :args (@t669))
% 48.28/48.57  (step @p746 :rule trans :premises (@p745 @p738))
% 48.28/48.57  (step @p747 :rule true_elim :premises (@p746))
% 48.28/48.57  (step @p748 :rule eq_resolve :premises (@p747 @p734))
% 48.28/48.57  (step @p749 :rule eq-symm :args (@t670 @t644))
% 48.28/48.57  (step @p750 :rule refl :args (@t671))
% 48.28/48.57  (step @p751 :rule cong :premises (@p750 @p749) :args ((=> @t671 @t672)))
% 48.28/48.57  (assume-push @p830 @t671)
% 48.28/48.57  (step @p753 :rule instantiate :premises (@p748) :args (@t673))
% 48.28/48.57  (step-pop @p831 :rule scope :premises (@p753))
% 48.28/48.57  (step @p754 :rule process_scope :premises (@p831) :args (@t672))
% 48.28/48.57  (step @p756 :rule eq_resolve :premises (@p754 @p751))
% 48.28/48.57  (step @p757 :rule implies_elim :premises (@p756))
% 48.28/48.57  (step @p758 :rule chain_m_resolution :premises (@p757 @p748) :args (@t674 @t620 (@list @t671)))
% 48.28/48.57  (step @p759 :rule eq-symm :args (@t675 @t555))
% 48.28/48.57  (step @p760 :rule beta-reduce :args ((= @t676 @t555)))
% 48.28/48.57  (step @p761 :rule refl :args (@t675))
% 48.28/48.57  (step @p762 :rule cong :premises (@p761 @p760) :args (@t677))
% 48.28/48.57  (step @p763 :rule trans :premises (@p762 @p759))
% 48.28/48.57  (step @p764 :rule cong :premises (@p763) :args (@t678))
% 48.28/48.57  (step @p765 :rule eq-refl :args (@t676))
% 48.28/48.57  (step @p766 :rule cong :premises (@p765) :args ((forall @t548 (= @t676 @t676))))
% 48.28/48.57  (step @p767 :rule trans :premises (@p766 @p735))
% 48.28/48.57  (step @p768 :rule refl :args (@t676))
% 48.28/48.57  (step @p769 :rule ho_cong :premises (@p544 @p742 @p741 @p740))
% 0.51/48.71  (step @p770 :rule cong :premises (@p769 @p768) :args (@t677))
% 0.51/48.71  (step @p771 :rule cong :premises (@p770) :args (@t678))
% 0.51/48.71  (step @p772 :rule trans :premises (@p771 @p767))
% 0.51/48.71  (step @p773 :rule true_elim :premises (@p772))
% 0.51/48.71  (step @p774 :rule eq_resolve :premises (@p773 @p764))
% 0.51/48.71  (step @p775 :rule eq-symm :args (@t670 @t643))
% 0.51/48.71  (step @p776 :rule refl :args (@t679))
% 0.51/48.71  (step @p777 :rule cong :premises (@p776 @p775) :args ((=> @t679 @t680)))
% 0.51/48.71  (assume-push @p832 @t679)
% 0.51/48.71  (step @p779 :rule instantiate :premises (@p774) :args (@t673))
% 0.51/48.71  (step-pop @p833 :rule scope :premises (@p779))
% 0.51/48.71  (step @p780 :rule process_scope :premises (@p833) :args (@t680))
% 0.51/48.71  (step @p782 :rule eq_resolve :premises (@p780 @p777))
% 0.51/48.71  (step @p783 :rule implies_elim :premises (@p782))
% 0.51/48.71  (step @p784 :rule chain_m_resolution :premises (@p783 @p774) :args (@t681 @t620 (@list @t679)))
% 0.51/48.71  (step @p785 :rule refl :args (@t682))
% 0.51/48.71  (step @p786 :rule refl :args (@t683))
% 0.51/48.71  (step @p787 :rule refl :args (@t685))
% 0.51/48.71  (step @p788 :rule bool-double-not-elim :args (@t645))
% 0.51/48.71  (step @p789 :rule nary_cong :premises (@p788 @p787 @p786 @p785) :args ((or (not @t646) @t685 @t683 @t682)))
% 0.51/48.71  (assume-push @p834 @t684)
% 0.51/48.71  (assume-push @p835 @t674)
% 0.51/48.71  (assume-push @p836 @t681)
% 0.51/48.71  (assume-push @p837 @t646)
% 0.51/48.71  (step @p659 :rule evaluate :args (@t639))
% 0.51/48.71  (step @p753 :rule instantiate :premises (@p748) :args (@t673))
% 0.51/48.71  (step @p794 :rule trans :premises (@p784 @p753 @p724))
% 0.51/48.71  (step @p795 :rule symm :premises (@p794))
% 0.51/48.71  (step @p796 :rule trans :premises (@p724 @p795))
% 0.51/48.71  (step @p797 :rule true_intro :premises (@p796))
% 0.51/48.71  (step @p798 :rule false_intro :premises (@p837))
% 0.51/48.71  (step @p799 :rule symm :premises (@p798))
% 0.51/48.71  (step @p800 :rule trans :premises (@p799 @p797))
% 0.51/48.71  (step @p801 false :rule eq_resolve :premises (@p800 @p659))
% 0.51/48.71  (step-pop @p838 :rule scope :premises (@p801))
% 0.51/48.71  (step-pop @p839 :rule scope :premises (@p838))
% 0.51/48.71  (step-pop @p840 :rule scope :premises (@p839))
% 0.51/48.71  (step-pop @p841 :rule scope :premises (@p840))
% 0.51/48.71  (step @p802 :rule process_scope :premises (@p841) :args (false))
% 0.51/48.71  (assume-push @p842 @t646)
% 0.51/48.71  (assume-push @p843 @t684)
% 0.51/48.71  (assume-push @p844 @t674)
% 0.51/48.71  (assume-push @p845 @t681)
% 0.51/48.71  (step @p811 :rule and_intro :premises (@p724 @p758 @p784 @p842))
% 0.51/48.71  (step-pop @p846 :rule scope :premises (@p811))
% 0.51/48.71  (step-pop @p847 :rule scope :premises (@p846))
% 0.51/48.71  (step-pop @p848 :rule scope :premises (@p847))
% 0.51/48.71  (step-pop @p849 :rule scope :premises (@p848))
% 0.51/48.71  (step @p812 :rule process_scope :premises (@p849) :args (@t686))
% 0.51/48.71  (step @p817 :rule implies_elim :premises (@p812))
% 0.51/48.71  (step @p818 :rule resolution :premises (@p817 @p802) :args (true @t686))
% 0.51/48.71  (step @p819 :rule not_and :premises (@p818))
% 0.51/48.71  (step @p820 :rule eq_resolve :premises (@p819 @p789))
% 0.51/48.71  (step @p821 false :rule chain_m_resolution :premises (@p820 @p784 @p758 @p724 @p676) :args (false (@list false false false true) (@list @t681 @t674 @t684 @t645)))
% 0.51/48.71  )
% 0.51/48.71  % SZS output end Proof
% 0.51/48.71  % cvc5 exiting
%------------------------------------------------------------------------------