cvc5---1.3.4.THM-Prf.s

%------------------------------------------------------------------------------
% File     : cvc5---1.3.4
% Problem  : ITP039^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 : n024.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:24:52 AM UTC 2026

% Result   : Theorem 0.34s 0.53s
% Output   : Proof 0.34s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06  % Problem  : ITP039^1 : TPTP v9.2.1. Released v7.5.0.
% 0.00/0.06  % Command  : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.25  % Computer : n024.cluster.edu
% 0.08/0.25  % Model    : x86_64 x86_64
% 0.08/0.25  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.25  % Memory   : 8042.1875MB
% 0.08/0.25  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.08/0.25  % CPULimit : 300
% 0.08/0.25  % WCLimit  : 300
% 0.08/0.25  % DateTime : Mon Jun  1 23:11:15 EDT 2026
% 0.08/0.25  % CPUTime  : 
% 0.15/0.40  %----Proving TH0
% 0.34/0.53  --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s...
% 0.34/0.53  % SZS status Theorem
% 0.34/0.53  % SZS output start Proof
% 0.34/0.53  (
% 0.34/0.53  (declare-sort tptp.produc1821101996_sc_sz 0)
% 0.34/0.53  (declare-sort tptp.denota610675952t_unit 0)
% 0.34/0.53  (declare-sort tptp.set_Pr1169339874_sc_sz 0)
% 0.34/0.53  (declare-sort tptp.finite1398487019real_c 0)
% 0.34/0.53  (declare-sort tptp.produc866628903_sc_sz 0)
% 0.34/0.53  (declare-sort tptp.produc190496183real_c 0)
% 0.34/0.53  (declare-sort tptp.set_Pr1389752855real_c 0)
% 0.34/0.53  (declare-sort tptp.set_Fi1407883041real_c 0)
% 0.34/0.53  (declare-sort tptp.set_Pr1774599175_sc_sz 0)
% 0.34/0.53  (declare-sort tptp.set_De208295462t_unit 0)
% 0.34/0.53  (declare-sort tptp.set_Pr2041213564t_unit 0)
% 0.34/0.53  (declare-sort tptp.set_Pr754230471real_c 0)
% 0.34/0.53  (declare-sort tptp.produc999471430t_unit 0)
% 0.34/0.53  (declare-sort tptp.produc640052711real_c 0)
% 0.34/0.53  (declare-sort tptp.set_Sum_sum_c_c 0)
% 0.34/0.53  (declare-sort tptp.produc1149990247eal_sz 0)
% 0.34/0.53  (declare-sort tptp.set_Pr60491591eal_sz 0)
% 0.34/0.53  (declare-sort tptp.formula_sf_sc_sz 0)
% 0.34/0.53  (declare-sort tptp.list_f1238882004_sc_sz 0)
% 0.34/0.53  (declare-sort tptp.set_o 0)
% 0.34/0.53  (declare-sort tptp.sc 0)
% 0.34/0.53  (declare-sort tptp.denota231621370t_unit 0)
% 0.34/0.53  (declare-sort tptp.set_Su1783761653um_b_c 0)
% 0.34/0.53  (declare-sort tptp.sf 0)
% 0.34/0.53  (declare-sort tptp.formula_a_b_c 0)
% 0.34/0.53  (declare-sort tptp.sz 0)
% 0.34/0.53  (declare-const tptp.denota968303861_a_b_c (-> tptp.denota231621370t_unit tptp.formula_a_b_c tptp.set_Pr1389752855real_c))
% 0.34/0.53  (declare-const tptp.member1895684704real_c (-> tptp.produc190496183real_c tptp.set_Pr1389752855real_c Bool))
% 0.34/0.53  (declare-const tptp.static_FVF_a_b_c (-> tptp.formula_a_b_c tptp.set_Sum_sum_c_c))
% 0.34/0.53  (declare-const tptp.denota1997846518gree_c (-> tptp.produc190496183real_c tptp.produc190496183real_c tptp.set_Sum_sum_c_c Bool))
% 0.34/0.53  (declare-const tptp.static_SIGF_a_b_c (-> tptp.formula_a_b_c tptp.set_Su1783761653um_b_c))
% 0.34/0.53  (declare-const tptp.denota69106024_a_b_c (-> tptp.denota231621370t_unit tptp.denota231621370t_unit tptp.set_Su1783761653um_b_c Bool))
% 0.34/0.53  (declare-const tptp.produc789536734_sc_sz (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.produc1821101996_sc_sz))
% 0.34/0.53  (declare-const tptp.top_to226056039real_c tptp.set_Pr1389752855real_c)
% 0.34/0.53  (declare-const tptp.produc394644079real_c (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.produc190496183real_c))
% 0.34/0.53  (declare-const tptp.top_to1499569298_sc_sz tptp.set_Pr1169339874_sc_sz)
% 0.34/0.53  (declare-const tptp.member1057565379_sc_sz (-> tptp.produc1821101996_sc_sz tptp.set_Pr1169339874_sc_sz Bool))
% 0.34/0.53  (declare-const tptp.produc1503602930_sc_sz (-> tptp.produc1821101996_sc_sz tptp.denota610675952t_unit))
% 0.34/0.53  (declare-const tptp.image_1726193375_sc_sz (-> (-> tptp.produc1821101996_sc_sz tptp.produc1821101996_sc_sz) tptp.set_Pr1169339874_sc_sz tptp.set_Pr1169339874_sc_sz))
% 0.34/0.53  (declare-const tptp.produc1612557567real_c (-> (-> tptp.denota610675952t_unit tptp.finite1398487019real_c) (-> tptp.produc866628903_sc_sz tptp.finite1398487019real_c) tptp.produc1821101996_sc_sz tptp.produc190496183real_c))
% 0.34/0.53  (declare-const tptp.produc1784590311_sc_sz (-> (-> tptp.finite1398487019real_c tptp.denota610675952t_unit) (-> tptp.finite1398487019real_c tptp.produc866628903_sc_sz) tptp.produc190496183real_c tptp.produc1821101996_sc_sz))
% 0.34/0.53  (declare-const tptp.produc368345510real_c (-> (-> tptp.finite1398487019real_c tptp.finite1398487019real_c) (-> tptp.finite1398487019real_c tptp.finite1398487019real_c) tptp.produc190496183real_c tptp.produc190496183real_c))
% 0.34/0.53  (declare-const tptp.produc403791768_sc_sz (-> (-> tptp.denota610675952t_unit tptp.denota610675952t_unit) (-> tptp.produc866628903_sc_sz tptp.produc866628903_sc_sz) tptp.produc1821101996_sc_sz tptp.produc1821101996_sc_sz))
% 0.34/0.53  (declare-const tptp.produc3751594real_c (-> tptp.set_Fi1407883041real_c tptp.set_Fi1407883041real_c tptp.set_Pr1389752855real_c))
% 0.34/0.53  (declare-const tptp.produc2020166735t_unit (-> tptp.set_Pr1774599175_sc_sz (-> tptp.produc866628903_sc_sz tptp.set_De208295462t_unit) tptp.set_Pr2041213564t_unit))
% 0.34/0.53  (declare-const tptp.produc563345056real_c (-> tptp.set_Fi1407883041real_c (-> tptp.finite1398487019real_c tptp.set_Fi1407883041real_c) tptp.set_Pr1389752855real_c))
% 0.34/0.53  (declare-const tptp.image_226055310_sc_sz (-> (-> tptp.produc866628903_sc_sz tptp.produc1821101996_sc_sz) tptp.set_Pr1774599175_sc_sz tptp.set_Pr1169339874_sc_sz))
% 0.34/0.53  (declare-const tptp.image_1259833374_sc_sz (-> (-> tptp.produc190496183real_c tptp.produc1821101996_sc_sz) tptp.set_Pr1389752855real_c tptp.set_Pr1169339874_sc_sz))
% 0.34/0.53  (declare-const tptp.image_1746662005real_c (-> (-> tptp.finite1398487019real_c tptp.produc640052711real_c) tptp.set_Fi1407883041real_c tptp.set_Pr754230471real_c))
% 0.34/0.53  (declare-const tptp.image_290183605_sc_sz (-> (-> tptp.finite1398487019real_c tptp.produc866628903_sc_sz) tptp.set_Fi1407883041real_c tptp.set_Pr1774599175_sc_sz))
% 0.34/0.53  (declare-const tptp.image_1461287749real_c (-> (-> tptp.finite1398487019real_c tptp.produc190496183real_c) tptp.set_Fi1407883041real_c tptp.set_Pr1389752855real_c))
% 0.34/0.53  (declare-const tptp.image_1514048989real_c (-> (-> tptp.finite1398487019real_c tptp.finite1398487019real_c) tptp.set_Fi1407883041real_c tptp.set_Fi1407883041real_c))
% 0.34/0.53  (declare-const tptp.produc1753599960real_c (-> (-> tptp.produc866628903_sc_sz tptp.denota610675952t_unit tptp.finite1398487019real_c) tptp.produc999471430t_unit tptp.finite1398487019real_c))
% 0.34/0.53  (declare-const tptp.image_1268968350real_c (-> (-> tptp.produc1821101996_sc_sz tptp.finite1398487019real_c) tptp.set_Pr1169339874_sc_sz tptp.set_Fi1407883041real_c))
% 0.34/0.53  (declare-const tptp.member_o (-> Bool tptp.set_o Bool))
% 0.34/0.53  (declare-const tptp.produc344593239real_c (-> (-> tptp.produc190496183real_c tptp.produc190496183real_c tptp.finite1398487019real_c) tptp.produc640052711real_c tptp.finite1398487019real_c))
% 0.34/0.53  (declare-const tptp.produc1920474870real_c (-> (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.finite1398487019real_c) tptp.produc1821101996_sc_sz tptp.finite1398487019real_c))
% 0.34/0.53  (declare-const tptp.image_388766773_sc_sz (-> (-> tptp.produc190496183real_c tptp.produc866628903_sc_sz) tptp.set_Pr1389752855real_c tptp.set_Pr1774599175_sc_sz))
% 0.34/0.53  (declare-const tptp.image_1551908392t_unit (-> (-> tptp.produc866628903_sc_sz tptp.produc999471430t_unit) tptp.set_Pr1774599175_sc_sz tptp.set_Pr2041213564t_unit))
% 0.34/0.53  (declare-const tptp.produc1341776291_sc_sz (-> (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.produc866628903_sc_sz) tptp.produc190496183real_c tptp.produc866628903_sc_sz))
% 0.34/0.53  (declare-const tptp.image_1121381717real_c (-> (-> tptp.produc866628903_sc_sz tptp.produc190496183real_c) tptp.set_Pr1774599175_sc_sz tptp.set_Pr1389752855real_c))
% 0.34/0.53  (declare-const tptp.produc126255499real_c (-> (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz tptp.produc190496183real_c) tptp.produc866628903_sc_sz tptp.produc190496183real_c))
% 0.34/0.53  (declare-const tptp.produc236226839real_c (-> (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz tptp.finite1398487019real_c) tptp.produc866628903_sc_sz tptp.finite1398487019real_c))
% 0.34/0.53  (declare-const tptp.image_14429021real_c (-> (-> tptp.produc190496183real_c tptp.finite1398487019real_c) tptp.set_Pr1389752855real_c tptp.set_Fi1407883041real_c))
% 0.34/0.53  (declare-const tptp.produc567249007real_c (-> (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.finite1398487019real_c) tptp.produc190496183real_c tptp.finite1398487019real_c))
% 0.34/0.53  (declare-const tptp.image_386905412real_c (-> (-> tptp.produc1821101996_sc_sz tptp.produc190496183real_c) tptp.set_Pr1169339874_sc_sz tptp.set_Pr1389752855real_c))
% 0.34/0.53  (declare-const tptp.image_1332486093real_c (-> (-> tptp.produc866628903_sc_sz tptp.finite1398487019real_c) tptp.set_Pr1774599175_sc_sz tptp.set_Fi1407883041real_c))
% 0.34/0.53  (declare-const tptp.produc448466487_sc_sz (-> (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.produc1821101996_sc_sz) tptp.produc1821101996_sc_sz tptp.produc1821101996_sc_sz))
% 0.34/0.53  (declare-const tptp.produc593754858real_c (-> (-> tptp.produc866628903_sc_sz tptp.denota610675952t_unit tptp.set_Pr1389752855real_c) tptp.produc999471430t_unit tptp.set_Pr1389752855real_c))
% 0.34/0.53  (declare-const tptp.produc645763722real_c (-> (-> tptp.produc866628903_sc_sz tptp.denota610675952t_unit tptp.produc190496183real_c) tptp.produc999471430t_unit tptp.produc190496183real_c))
% 0.34/0.53  (declare-const tptp.produc295339066_sc_sz (-> (-> tptp.produc999471430t_unit tptp.produc1821101996_sc_sz) tptp.produc866628903_sc_sz tptp.denota610675952t_unit tptp.produc1821101996_sc_sz))
% 0.34/0.53  (declare-const tptp.inv_im1827249322real_c (-> tptp.set_Pr1389752855real_c (-> tptp.finite1398487019real_c tptp.finite1398487019real_c) tptp.set_Pr1389752855real_c))
% 0.34/0.53  (declare-const tptp.produc1827049067real_c (-> (-> tptp.produc1821101996_sc_sz tptp.set_Pr1389752855real_c) tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.set_Pr1389752855real_c))
% 0.34/0.53  (declare-const tptp.produc753314315real_c (-> (-> tptp.produc1821101996_sc_sz tptp.produc190496183real_c) tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.produc190496183real_c))
% 0.34/0.53  (declare-const tptp.produc1726730540al_c_o (-> (-> tptp.produc190496183real_c tptp.produc190496183real_c Bool) tptp.produc640052711real_c Bool))
% 0.34/0.53  (declare-const tptp.phi tptp.formula_a_b_c)
% 0.34/0.53  (declare-const tptp.produc1718498667unit_o (-> (-> tptp.produc866628903_sc_sz tptp.denota610675952t_unit Bool) tptp.produc999471430t_unit Bool))
% 0.34/0.53  (declare-const tptp.produc353381908al_c_o (-> (-> tptp.finite1398487019real_c tptp.finite1398487019real_c Bool) tptp.produc190496183real_c Bool))
% 0.34/0.53  (declare-const tptp.produc1368849166real_c (-> (-> tptp.produc866628903_sc_sz tptp.denota610675952t_unit tptp.set_Fi1407883041real_c) tptp.produc999471430t_unit tptp.set_Fi1407883041real_c))
% 0.34/0.53  (declare-const tptp.produc2068697644real_c (-> (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.set_Fi1407883041real_c) tptp.produc1821101996_sc_sz tptp.set_Fi1407883041real_c))
% 0.34/0.53  (declare-const tptp.produc245128480t_unit (-> tptp.produc999471430t_unit tptp.produc1821101996_sc_sz))
% 0.34/0.53  (declare-const tptp.produc1145837239_sc_sz (-> tptp.produc866628903_sc_sz tptp.produc866628903_sc_sz))
% 0.34/0.53  (declare-const tptp.image_1269062456real_c (-> (-> tptp.produc999471430t_unit tptp.finite1398487019real_c) tptp.set_Pr2041213564t_unit tptp.set_Fi1407883041real_c))
% 0.34/0.53  (declare-const tptp.denota1946510237_sc_sz (-> tptp.formula_sf_sc_sz Bool))
% 0.34/0.53  (declare-const tptp.produc237521996real_c (-> (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.set_Pr1389752855real_c) tptp.produc1821101996_sc_sz tptp.set_Pr1389752855real_c))
% 0.34/0.53  (declare-const tptp.produc880541325c_sz_o (-> (-> tptp.produc866628903_sc_sz Bool) tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz Bool))
% 0.34/0.53  (declare-const tptp.produc1017530376real_c (-> tptp.set_Pr1389752855real_c (-> tptp.produc190496183real_c tptp.set_Pr1389752855real_c) tptp.set_Pr754230471real_c))
% 0.34/0.53  (declare-const tptp.member235934813t_unit (-> tptp.produc999471430t_unit tptp.set_Pr2041213564t_unit Bool))
% 0.34/0.53  (declare-const tptp.collec377961627t_unit (-> (-> tptp.produc999471430t_unit Bool) tptp.set_Pr2041213564t_unit))
% 0.34/0.53  (declare-const tptp.produc383750338real_c (-> (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.produc190496183real_c) tptp.produc1821101996_sc_sz tptp.produc190496183real_c))
% 0.34/0.53  (declare-const tptp.produc704157711real_c (-> tptp.produc190496183real_c tptp.produc190496183real_c))
% 0.34/0.53  (declare-const tptp.implies_a_b_c (-> tptp.formula_a_b_c tptp.formula_a_b_c tptp.formula_a_b_c))
% 0.34/0.53  (declare-const tptp.collec1643251106real_c (-> (-> tptp.produc190496183real_c Bool) tptp.set_Pr1389752855real_c))
% 0.34/0.53  (declare-const tptp.produc1822718231_sc_sz (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz tptp.produc866628903_sc_sz))
% 0.34/0.53  (declare-const tptp.produc198687651c_sz_o (-> (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz Bool) tptp.produc1821101996_sc_sz Bool))
% 0.34/0.53  (declare-const tptp.produc1959054510t_unit (-> (-> tptp.produc866628903_sc_sz tptp.produc866628903_sc_sz) tptp.produc1821101996_sc_sz tptp.produc1821101996_sc_sz))
% 0.34/0.53  (declare-const tptp.produc532048446_sc_sz (-> tptp.produc1821101996_sc_sz tptp.produc999471430t_unit))
% 0.34/0.53  (declare-const tptp.image_768765061real_c (-> (-> tptp.produc866628903_sc_sz tptp.produc640052711real_c) tptp.set_Pr1774599175_sc_sz tptp.set_Pr754230471real_c))
% 0.34/0.53  (declare-const tptp.produc107375667real_c (-> (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.produc190496183real_c) tptp.produc190496183real_c tptp.produc190496183real_c))
% 0.34/0.53  (declare-const tptp.equiv_a_b_c (-> tptp.formula_a_b_c tptp.formula_a_b_c tptp.formula_a_b_c))
% 0.34/0.53  (declare-const tptp.produc2039065452c_sz_o (-> (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz Bool) tptp.produc866628903_sc_sz Bool))
% 0.34/0.53  (declare-const tptp.image_1313166277_sc_sz (-> (-> tptp.produc866628903_sc_sz tptp.produc866628903_sc_sz) tptp.set_Pr1774599175_sc_sz tptp.set_Pr1774599175_sc_sz))
% 0.34/0.53  (declare-const tptp.image_124598413real_c (-> (-> tptp.produc640052711real_c tptp.finite1398487019real_c) tptp.set_Pr754230471real_c tptp.set_Fi1407883041real_c))
% 0.34/0.53  (declare-const tptp.produc29022117real_c (-> (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.set_Fi1407883041real_c) tptp.produc190496183real_c tptp.set_Fi1407883041real_c))
% 0.34/0.53  (declare-const tptp.top_to1660572043um_c_c tptp.set_Sum_sum_c_c)
% 0.34/0.53  (declare-const tptp.predic913887884_sf_sz (-> tptp.sc tptp.formula_sf_sc_sz))
% 0.34/0.53  (declare-const tptp.produc38128778unit_o (-> (-> tptp.produc999471430t_unit Bool) tptp.produc866628903_sc_sz tptp.denota610675952t_unit Bool))
% 0.34/0.53  (declare-const tptp.produc1119115220real_c (-> (-> tptp.produc190496183real_c tptp.produc190496183real_c) tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.produc190496183real_c))
% 0.34/0.53  (declare-const tptp.collec1199592193_sc_sz (-> (-> tptp.produc1821101996_sc_sz Bool) tptp.set_Pr1169339874_sc_sz))
% 0.34/0.53  (declare-const tptp.produc1716060341al_c_o (-> (-> tptp.produc190496183real_c Bool) tptp.finite1398487019real_c tptp.finite1398487019real_c Bool))
% 0.34/0.53  (declare-const tptp.collec230941376real_c (-> (-> tptp.finite1398487019real_c Bool) tptp.set_Fi1407883041real_c))
% 0.34/0.53  (declare-const tptp.produc642283651_sc_sz (-> (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.set_Pr1774599175_sc_sz) tptp.produc190496183real_c tptp.set_Pr1774599175_sc_sz))
% 0.34/0.53  (declare-const tptp.produc350724343real_c (-> tptp.produc640052711real_c tptp.produc640052711real_c))
% 0.34/0.53  (declare-const tptp.image_1426741113_sc_sz (-> (-> tptp.produc999471430t_unit tptp.produc1821101996_sc_sz) tptp.set_Pr2041213564t_unit tptp.set_Pr1169339874_sc_sz))
% 0.34/0.53  (declare-const tptp.denota1579475975_sc_sz (-> tptp.denota610675952t_unit Bool))
% 0.34/0.53  (declare-const tptp.p_sc_sf_sz (-> tptp.sc tptp.formula_sf_sc_sz))
% 0.34/0.53  (declare-const tptp.member245028432_sc_sz (-> tptp.produc866628903_sc_sz tptp.set_Pr1774599175_sc_sz Bool))
% 0.34/0.53  (declare-const tptp.produc435149849_sc_sz (-> (-> tptp.produc866628903_sc_sz tptp.denota610675952t_unit tptp.produc1821101996_sc_sz) tptp.produc999471430t_unit tptp.produc1821101996_sc_sz))
% 0.34/0.53  (declare-const tptp.collec2036662930_sc_sz (-> (-> tptp.produc866628903_sc_sz Bool) tptp.set_Pr1774599175_sc_sz))
% 0.34/0.53  (declare-const tptp.produc1563580891_sc_sz (-> (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz tptp.set_Pr1774599175_sc_sz) tptp.produc866628903_sc_sz tptp.set_Pr1774599175_sc_sz))
% 0.34/0.53  (declare-const tptp.produc1687028567real_c (-> tptp.produc190496183real_c tptp.produc190496183real_c tptp.produc640052711real_c))
% 0.34/0.53  (declare-const tptp.member1261661570real_c (-> tptp.finite1398487019real_c tptp.set_Fi1407883041real_c Bool))
% 0.34/0.53  (declare-const tptp.produc793407943_sc_sz (-> (-> tptp.denota610675952t_unit tptp.denota610675952t_unit) tptp.produc999471430t_unit tptp.produc999471430t_unit))
% 0.34/0.53  (declare-const tptp.produc502616768t_unit (-> tptp.produc866628903_sc_sz tptp.denota610675952t_unit tptp.produc999471430t_unit))
% 0.34/0.53  (declare-const tptp.produc440529997al_c_o (-> (-> tptp.produc640052711real_c Bool) tptp.produc190496183real_c tptp.produc190496183real_c Bool))
% 0.34/0.53  (declare-const tptp.collec1126017874real_c (-> (-> tptp.produc640052711real_c Bool) tptp.set_Pr754230471real_c))
% 0.34/0.53  (declare-const tptp.produc159603053_sc_sz (-> tptp.set_De208295462t_unit (-> tptp.denota610675952t_unit tptp.set_Pr1774599175_sc_sz) tptp.set_Pr1169339874_sc_sz))
% 0.34/0.53  (declare-const tptp.member630771088eal_sz (-> tptp.produc1149990247eal_sz tptp.set_Pr60491591eal_sz Bool))
% 0.34/0.53  (declare-const tptp.image_904562809t_unit (-> (-> tptp.produc1821101996_sc_sz tptp.produc999471430t_unit) tptp.set_Pr1169339874_sc_sz tptp.set_Pr2041213564t_unit))
% 0.34/0.53  (declare-const tptp.produc233219286_sc_sz (-> (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz) tptp.produc866628903_sc_sz tptp.produc866628903_sc_sz))
% 0.34/0.53  (declare-const tptp.image_2041365445real_c (-> (-> tptp.produc640052711real_c tptp.produc640052711real_c) tptp.set_Pr754230471real_c tptp.set_Pr754230471real_c))
% 0.34/0.53  (declare-const tptp.produc1575513068real_c (-> (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.produc190496183real_c) tptp.produc1821101996_sc_sz tptp.produc190496183real_c))
% 0.34/0.53  (declare-const tptp.image_738229701real_c (-> (-> tptp.produc190496183real_c tptp.produc190496183real_c) tptp.set_Pr1389752855real_c tptp.set_Pr1389752855real_c))
% 0.34/0.53  (declare-const tptp.produc619560141c_sz_o (-> (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz Bool) tptp.produc1821101996_sc_sz Bool))
% 0.34/0.53  (declare-const tptp.image_1641704997c_sz_o (-> (-> tptp.produc1821101996_sc_sz Bool) tptp.set_Pr1169339874_sc_sz tptp.set_o))
% 0.34/0.53  (declare-const tptp.produc1894848802real_c (-> (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.set_Pr1389752855real_c) tptp.produc1821101996_sc_sz tptp.set_Pr1389752855real_c))
% 0.34/0.53  (declare-const tptp.produc1442549981real_c (-> (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.produc190496183real_c) tptp.produc190496183real_c tptp.produc190496183real_c))
% 0.34/0.53  (declare-const tptp.member754147591t_unit (-> tptp.denota610675952t_unit tptp.set_De208295462t_unit Bool))
% 0.34/0.53  (declare-const tptp.produc6841835real_c (-> (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz tptp.set_Pr1389752855real_c) tptp.produc866628903_sc_sz tptp.set_Pr1389752855real_c))
% 0.34/0.53  (declare-const tptp.produc2099580355_sc_sz (-> (-> tptp.produc866628903_sc_sz tptp.denota610675952t_unit tptp.produc1821101996_sc_sz) tptp.produc999471430t_unit tptp.produc1821101996_sc_sz))
% 0.34/0.53  (declare-const tptp.produc981295297real_c (-> (-> tptp.finite1398487019real_c tptp.finite1398487019real_c) tptp.produc190496183real_c tptp.produc190496183real_c))
% 0.34/0.53  (declare-const tptp.produc2089853305real_c (-> (-> tptp.produc190496183real_c tptp.produc190496183real_c) tptp.produc640052711real_c tptp.produc640052711real_c))
% 0.34/0.53  (declare-const tptp.produc1449736269real_c (-> (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz tptp.set_Fi1407883041real_c) tptp.produc866628903_sc_sz tptp.set_Fi1407883041real_c))
% 0.34/0.53  (declare-const tptp.denota1711272799_sc_sz (-> tptp.denota610675952t_unit tptp.formula_sf_sc_sz tptp.set_Pr60491591eal_sz))
% 0.34/0.53  (declare-const tptp.produc923381907real_c (-> (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.set_Pr1389752855real_c) tptp.produc190496183real_c tptp.set_Pr1389752855real_c))
% 0.34/0.53  (declare-const tptp.member346808080real_c (-> tptp.produc640052711real_c tptp.set_Pr754230471real_c Bool))
% 0.34/0.53  (declare-const tptp.produc1066779277real_c (-> (-> tptp.produc190496183real_c tptp.produc190496183real_c tptp.set_Fi1407883041real_c) tptp.produc640052711real_c tptp.set_Fi1407883041real_c))
% 0.34/0.53  (define tptp.coinci501627771_a_b_c () (let ((_let_1 (@var "Phi" tptp.formula_a_b_c))) (let ((_let_2 (@var "J" tptp.denota231621370t_unit))) (let ((_let_3 (@var "Nu2" tptp.produc190496183real_c))) (let ((_let_4 (@var "I" tptp.denota231621370t_unit))) (let ((_let_5 (@var "Nu" tptp.produc190496183real_c))) (lambda (@list _let_1) (forall (@list _let_5 _let_3 _let_4 _let_2) (=> (_ (_ (_ tptp.denota69106024_a_b_c _let_4) _let_2) (_ tptp.static_SIGF_a_b_c _let_1)) (=> (_ (_ (_ tptp.denota1997846518gree_c _let_5) _let_3) (_ tptp.static_FVF_a_b_c _let_1)) (= (_ (_ tptp.member1895684704real_c _let_5) (_ (_ tptp.denota968303861_a_b_c _let_4) _let_1)) (_ (_ tptp.member1895684704real_c _let_3) (_ (_ tptp.denota968303861_a_b_c _let_2) _let_1)))))))))))))
% 0.34/0.53  (define tptp.ids_sz_sf_sc () (let ((_let_1 (@var "Pid42" tptp.sc))) (let ((_let_2 (@var "Pid32" tptp.sc))) (let ((_let_3 (@var "Pid22" tptp.sc))) (let ((_let_4 (@var "Pid12" tptp.sc))) (let ((_let_5 (@var "Fid32" tptp.sf))) (let ((_let_6 (@var "Fid12" tptp.sf))) (let ((_let_7 (@var "Fid22" tptp.sf))) (let ((_let_8 (@var "Vid32" tptp.sz))) (let ((_let_9 (@var "Vid12" tptp.sz))) (let ((_let_10 (@var "Vid22" tptp.sz))) (lambda (@list _let_9 _let_10 _let_8 _let_6 _let_7 _let_5 _let_4 _let_3 _let_2 _let_1) (and (not (= _let_9 _let_10)) (not (= _let_10 _let_8)) (not (= _let_9 _let_8)) (not (= _let_6 _let_7)) (not (= _let_7 _let_5)) (not (= _let_6 _let_5)) (not (= _let_4 _let_3)) (not (= _let_3 _let_2)) (not (= _let_4 _let_2)) (not (= _let_4 _let_1)) (not (= _let_3 _let_1)) (not (= _let_2 _let_1)))))))))))))))
% 0.34/0.53  (define tptp.produc1086673900c_sz_o () (let ((_let_1 (@var "B5" tptp.produc866628903_sc_sz))) (let ((_let_2 (@var "A5" tptp.denota610675952t_unit))) (let ((_let_3 (@var "F" (-> tptp.produc1821101996_sc_sz Bool)))) (lambda (@list _let_3 _let_2 _let_1) (_ _let_3 (_ (_ tptp.produc789536734_sc_sz _let_2) _let_1)))))))
% 0.34/0.53  (define tptp.top_to964419200al_c_o () (let ((_let_1 (@var "Y4" tptp.finite1398487019real_c))) (let ((_let_2 (@var "X4" tptp.finite1398487019real_c))) (lambda (@list _let_2 _let_1) (_ (_ tptp.member1895684704real_c (_ (_ tptp.produc394644079real_c _let_2) _let_1)) tptp.top_to226056039real_c)))))
% 0.34/0.53  (define tptp.top_to1399053141c_sz_o () (let ((_let_1 (@var "Y4" tptp.produc866628903_sc_sz))) (let ((_let_2 (@var "X4" tptp.denota610675952t_unit))) (lambda (@list _let_2 _let_1) (_ (_ tptp.member1057565379_sc_sz (_ (_ tptp.produc789536734_sc_sz _let_2) _let_1)) tptp.top_to1499569298_sc_sz)))))
% 0.34/0.53  (define @t1 () (@var "Phi2" tptp.formula_a_b_c))
% 0.34/0.53  (define @t2 () (@var "J" tptp.denota231621370t_unit))
% 0.34/0.53  (define @t3 () (_ tptp.denota968303861_a_b_c @t2))
% 0.34/0.53  (define @t4 () (@var "Nu2" tptp.produc190496183real_c))
% 0.34/0.53  (define @t5 () (_ tptp.member1895684704real_c @t4))
% 0.34/0.53  (define @t6 () (@var "I" tptp.denota231621370t_unit))
% 0.34/0.53  (define @t7 () (_ tptp.denota968303861_a_b_c @t6))
% 0.34/0.53  (define @t8 () (@var "Nu" tptp.produc190496183real_c))
% 0.34/0.53  (define @t9 () (_ tptp.member1895684704real_c @t8))
% 0.34/0.53  (define @t10 () (_ (_ tptp.denota1997846518gree_c @t8) @t4))
% 0.34/0.53  (define @t11 () (_ (_ tptp.denota69106024_a_b_c @t6) @t2))
% 0.34/0.53  (define @t12 () (@list @t8 @t4 @t6 @t2))
% 0.34/0.53  (define @t13 () (@var "Pid4" tptp.sc))
% 0.34/0.53  (define @t14 () (@var "Pid3" tptp.sc))
% 0.34/0.53  (define @t15 () (@var "Pid2" tptp.sc))
% 0.34/0.53  (define @t16 () (@var "Pid1" tptp.sc))
% 0.34/0.53  (define @t17 () (@var "Fid3" tptp.sf))
% 0.34/0.53  (define @t18 () (@var "Fid2" tptp.sf))
% 0.34/0.53  (define @t19 () (@var "Fid1" tptp.sf))
% 0.34/0.53  (define @t20 () (@var "Vid3" tptp.sz))
% 0.34/0.53  (define @t21 () (@var "Vid2" tptp.sz))
% 0.34/0.53  (define @t22 () (@var "Vid1" tptp.sz))
% 0.34/0.53  (define @t23 () (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ tptp.ids_sz_sf_sc @t22) @t21) @t20) @t19) @t18) @t17) @t16) @t15) @t14) @t13))
% 0.34/0.53  (define @t24 () (@var "V" tptp.set_Su1783761653um_b_c))
% 0.34/0.53  (define @t25 () (@var "A" tptp.denota231621370t_unit))
% 0.34/0.53  (define @t26 () (@var "B" tptp.denota231621370t_unit))
% 0.34/0.53  (define @t27 () (@var "A" tptp.set_Su1783761653um_b_c))
% 0.34/0.53  (define @t28 () (@var "I2" tptp.denota231621370t_unit))
% 0.34/0.53  (define @t29 () (@var "V" tptp.set_Sum_sum_c_c))
% 0.34/0.53  (define @t30 () (@var "A" tptp.produc190496183real_c))
% 0.34/0.53  (define @t31 () (@var "B" tptp.produc190496183real_c))
% 0.34/0.53  (define @t32 () (@var "A" tptp.set_Sum_sum_c_c))
% 0.34/0.53  (define @t33 () (@var "Nu3" tptp.produc190496183real_c))
% 0.34/0.53  (define @t34 () (_ tptp.denota1997846518gree_c @t33))
% 0.34/0.53  (define @t35 () (@var "A" tptp.formula_a_b_c))
% 0.34/0.53  (define @t36 () (_ tptp.denota968303861_a_b_c @t28))
% 0.34/0.53  (define @t37 () (_ tptp.member1895684704real_c @t33))
% 0.34/0.53  (define @t38 () (_ @t37 (_ @t36 @t35)))
% 0.34/0.53  (define @t39 () (@var "B" tptp.formula_a_b_c))
% 0.34/0.53  (define @t40 () (_ @t37 (_ @t36 @t39)))
% 0.34/0.53  (define @t41 () (=> @t38 @t40))
% 0.34/0.53  (define @t42 () (= @t38 @t40))
% 0.34/0.53  (define @t43 () (@list @t33 @t28 @t35 @t39))
% 0.34/0.53  (define @t44 () (@var "S" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t45 () (@var "I3" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t46 () (@var "X" tptp.produc1821101996_sc_sz))
% 0.34/0.53  (define @t47 () (not (forall (@list @t45 @t44) (not (= @t46 (_ (_ tptp.produc789536734_sc_sz @t45) @t44))))))
% 0.34/0.53  (define @t48 () (@var "A1" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t49 () (@var "A0" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t50 () (@var "P" (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz Bool)))
% 0.34/0.53  (define @t51 () (@var "X_1" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t52 () (@var "P2" tptp.sc))
% 0.34/0.53  (define @t53 () (@var "Y2" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t54 () (@var "X2" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t55 () (@var "Y1" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t56 () (@var "X1" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t57 () (@var "Y2" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t58 () (@var "X2" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t59 () (@var "Y1" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t60 () (@var "X1" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t61 () (_ (_ tptp.produc394644079real_c @t60) @t58))
% 0.34/0.53  (define @t62 () (@var "Y2" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t63 () (@var "X2" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t64 () (@var "Y1" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t65 () (@var "X1" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t66 () (_ (_ tptp.produc502616768t_unit @t65) @t63))
% 0.34/0.53  (define @t67 () (@var "Y2" tptp.produc190496183real_c))
% 0.34/0.53  (define @t68 () (@var "X2" tptp.produc190496183real_c))
% 0.34/0.53  (define @t69 () (@var "Y1" tptp.produc190496183real_c))
% 0.34/0.53  (define @t70 () (@var "X1" tptp.produc190496183real_c))
% 0.34/0.53  (define @t71 () (@var "Y2" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t72 () (@var "X2" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t73 () (@var "Y1" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t74 () (@var "X1" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t75 () (_ (_ tptp.produc789536734_sc_sz @t74) @t72))
% 0.34/0.53  (define @t76 () (@var "B3" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t77 () (@var "B2" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t78 () (= @t77 @t76))
% 0.34/0.53  (define @t79 () (@var "A3" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t80 () (@var "A2" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t81 () (= @t80 @t79))
% 0.34/0.53  (define @t82 () (_ (_ tptp.produc1822718231_sc_sz @t80) @t77))
% 0.34/0.53  (define @t83 () (= @t82 (_ (_ tptp.produc1822718231_sc_sz @t79) @t76)))
% 0.34/0.53  (define @t84 () (@list @t80 @t77 @t79 @t76))
% 0.34/0.53  (define @t85 () (@var "B3" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t86 () (@var "B2" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t87 () (= @t86 @t85))
% 0.34/0.53  (define @t88 () (@var "A3" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t89 () (@var "A2" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t90 () (= @t89 @t88))
% 0.34/0.53  (define @t91 () (_ (_ tptp.produc394644079real_c @t89) @t86))
% 0.34/0.53  (define @t92 () (= @t91 (_ (_ tptp.produc394644079real_c @t88) @t85)))
% 0.34/0.53  (define @t93 () (@list @t89 @t86 @t88 @t85))
% 0.34/0.53  (define @t94 () (@var "B3" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t95 () (@var "B2" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t96 () (= @t95 @t94))
% 0.34/0.53  (define @t97 () (@var "A3" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t98 () (@var "A2" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t99 () (= @t98 @t97))
% 0.34/0.53  (define @t100 () (_ (_ tptp.produc502616768t_unit @t98) @t95))
% 0.34/0.53  (define @t101 () (= @t100 (_ (_ tptp.produc502616768t_unit @t97) @t94)))
% 0.34/0.53  (define @t102 () (@list @t98 @t95 @t97 @t94))
% 0.34/0.53  (define @t103 () (@var "B3" tptp.produc190496183real_c))
% 0.34/0.53  (define @t104 () (@var "B2" tptp.produc190496183real_c))
% 0.34/0.53  (define @t105 () (= @t104 @t103))
% 0.34/0.53  (define @t106 () (@var "A3" tptp.produc190496183real_c))
% 0.34/0.53  (define @t107 () (@var "A2" tptp.produc190496183real_c))
% 0.34/0.53  (define @t108 () (= @t107 @t106))
% 0.34/0.53  (define @t109 () (_ (_ tptp.produc1687028567real_c @t107) @t104))
% 0.34/0.53  (define @t110 () (= @t109 (_ (_ tptp.produc1687028567real_c @t106) @t103)))
% 0.34/0.53  (define @t111 () (@list @t107 @t104 @t106 @t103))
% 0.34/0.53  (define @t112 () (@var "B3" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t113 () (@var "B2" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t114 () (= @t113 @t112))
% 0.34/0.53  (define @t115 () (@var "A3" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t116 () (@var "A2" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t117 () (= @t116 @t115))
% 0.34/0.53  (define @t118 () (_ (_ tptp.produc789536734_sc_sz @t116) @t113))
% 0.34/0.53  (define @t119 () (= @t118 (_ (_ tptp.produc789536734_sc_sz @t115) @t112)))
% 0.34/0.53  (define @t120 () (@list @t116 @t113 @t115 @t112))
% 0.34/0.53  (define @t121 () (@var "C" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t122 () (@var "B4" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t123 () (@var "A4" tptp.produc190496183real_c))
% 0.34/0.53  (define @t124 () (_ tptp.produc1687028567real_c @t123))
% 0.34/0.53  (define @t125 () (_ @t124 (_ (_ tptp.produc394644079real_c @t122) @t121)))
% 0.34/0.53  (define @t126 () (@var "Y" tptp.produc640052711real_c))
% 0.34/0.53  (define @t127 () (@list @t123 @t122 @t121))
% 0.34/0.53  (define @t128 () (@list @t126))
% 0.34/0.53  (define @t129 () (@var "C" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t130 () (@var "B4" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t131 () (@var "A4" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t132 () (_ tptp.produc789536734_sc_sz @t131))
% 0.34/0.53  (define @t133 () (_ @t132 (_ (_ tptp.produc1822718231_sc_sz @t130) @t129)))
% 0.34/0.53  (define @t134 () (@var "Y" tptp.produc1821101996_sc_sz))
% 0.34/0.53  (define @t135 () (@list @t131 @t130 @t129))
% 0.34/0.53  (define @t136 () (@list @t134))
% 0.34/0.53  (define @t137 () (@var "Prod" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t138 () (@var "P" (-> tptp.produc866628903_sc_sz Bool)))
% 0.34/0.53  (define @t139 () (@var "A4" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t140 () (_ (_ tptp.produc1822718231_sc_sz @t139) @t130))
% 0.34/0.53  (define @t141 () (@list @t139 @t130))
% 0.34/0.53  (define @t142 () (forall @t141 (_ @t138 @t140)))
% 0.34/0.53  (define @t143 () (@var "Prod" tptp.produc190496183real_c))
% 0.34/0.53  (define @t144 () (@var "P" (-> tptp.produc190496183real_c Bool)))
% 0.34/0.53  (define @t145 () (@var "A4" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t146 () (_ (_ tptp.produc394644079real_c @t145) @t122))
% 0.34/0.53  (define @t147 () (@list @t145 @t122))
% 0.34/0.53  (define @t148 () (forall @t147 (_ @t144 @t146)))
% 0.34/0.53  (define @t149 () (@var "Prod" tptp.produc999471430t_unit))
% 0.34/0.53  (define @t150 () (@var "P" (-> tptp.produc999471430t_unit Bool)))
% 0.34/0.53  (define @t151 () (@var "B4" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t152 () (@var "A4" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t153 () (_ (_ tptp.produc502616768t_unit @t152) @t151))
% 0.34/0.53  (define @t154 () (@list @t152 @t151))
% 0.34/0.53  (define @t155 () (forall @t154 (_ @t150 @t153)))
% 0.34/0.53  (define @t156 () (@var "Prod" tptp.produc640052711real_c))
% 0.34/0.53  (define @t157 () (@var "P" (-> tptp.produc640052711real_c Bool)))
% 0.34/0.53  (define @t158 () (@var "B4" tptp.produc190496183real_c))
% 0.34/0.53  (define @t159 () (_ @t124 @t158))
% 0.34/0.53  (define @t160 () (@list @t123 @t158))
% 0.34/0.53  (define @t161 () (forall @t160 (_ @t157 @t159)))
% 0.34/0.53  (define @t162 () (@var "Prod" tptp.produc1821101996_sc_sz))
% 0.34/0.53  (define @t163 () (@var "P" (-> tptp.produc1821101996_sc_sz Bool)))
% 0.34/0.53  (define @t164 () (@var "B4" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t165 () (_ @t132 @t164))
% 0.34/0.53  (define @t166 () (@list @t131 @t164))
% 0.34/0.53  (define @t167 () (forall @t166 (_ @t163 @t165)))
% 0.34/0.53  (define @t168 () (@var "Y" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t169 () (@var "Y" tptp.produc190496183real_c))
% 0.34/0.53  (define @t170 () (@var "Y" tptp.produc999471430t_unit))
% 0.34/0.53  (define @t171 () (@var "P2" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t172 () (@var "P2" tptp.produc190496183real_c))
% 0.34/0.53  (define @t173 () (@var "P2" tptp.produc999471430t_unit))
% 0.34/0.53  (define @t174 () (@var "P2" tptp.produc640052711real_c))
% 0.34/0.53  (define @t175 () (@var "P2" tptp.produc1821101996_sc_sz))
% 0.34/0.53  (define @t176 () (@var "Y3" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t177 () (@var "X3" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t178 () (= @t171 (_ (_ tptp.produc1822718231_sc_sz @t177) @t176)))
% 0.34/0.53  (define @t179 () (@list @t177 @t176))
% 0.34/0.53  (define @t180 () (@var "Y3" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t181 () (@var "X3" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t182 () (_ (_ tptp.produc394644079real_c @t181) @t180))
% 0.34/0.53  (define @t183 () (= @t172 @t182))
% 0.34/0.53  (define @t184 () (@list @t181 @t180))
% 0.34/0.53  (define @t185 () (@list @t172))
% 0.34/0.53  (define @t186 () (@var "Y3" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t187 () (@var "X3" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t188 () (_ (_ tptp.produc502616768t_unit @t187) @t186))
% 0.34/0.53  (define @t189 () (= @t173 @t188))
% 0.34/0.53  (define @t190 () (@list @t187 @t186))
% 0.34/0.53  (define @t191 () (@list @t173))
% 0.34/0.53  (define @t192 () (@var "Y3" tptp.produc190496183real_c))
% 0.34/0.53  (define @t193 () (@var "X3" tptp.produc190496183real_c))
% 0.34/0.53  (define @t194 () (_ (_ tptp.produc1687028567real_c @t193) @t192))
% 0.34/0.53  (define @t195 () (= @t174 @t194))
% 0.34/0.53  (define @t196 () (@list @t193 @t192))
% 0.34/0.53  (define @t197 () (@var "Y3" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t198 () (@var "X3" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t199 () (_ (_ tptp.produc789536734_sc_sz @t198) @t197))
% 0.34/0.53  (define @t200 () (= @t175 @t199))
% 0.34/0.53  (define @t201 () (@list @t198 @t197))
% 0.34/0.53  (define @t202 () (@list @t175))
% 0.34/0.53  (define @t203 () (@var "X" tptp.produc640052711real_c))
% 0.34/0.53  (define @t204 () (@var "P" (-> tptp.finite1398487019real_c Bool)))
% 0.34/0.53  (define @t205 () (_ tptp.member1261661570real_c @t89))
% 0.34/0.53  (define @t206 () (@var "A2" tptp.produc1821101996_sc_sz))
% 0.34/0.53  (define @t207 () (@var "A2" tptp.produc640052711real_c))
% 0.34/0.53  (define @t208 () (@var "A2" tptp.produc999471430t_unit))
% 0.34/0.53  (define @t209 () (_ tptp.collec1643251106real_c @t144))
% 0.34/0.53  (define @t210 () (_ tptp.member1895684704real_c @t107))
% 0.34/0.53  (define @t211 () (@var "A" tptp.set_Fi1407883041real_c))
% 0.34/0.53  (define @t212 () (@var "X4" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t213 () (@var "A" tptp.set_Pr1169339874_sc_sz))
% 0.34/0.53  (define @t214 () (@var "X4" tptp.produc1821101996_sc_sz))
% 0.34/0.53  (define @t215 () (_ (_ tptp.member1057565379_sc_sz @t214) @t213))
% 0.34/0.53  (define @t216 () (@list @t214))
% 0.34/0.53  (define @t217 () (@var "A" tptp.set_Pr754230471real_c))
% 0.34/0.53  (define @t218 () (@var "X4" tptp.produc640052711real_c))
% 0.34/0.53  (define @t219 () (@var "A" tptp.set_Pr2041213564t_unit))
% 0.34/0.53  (define @t220 () (@var "X4" tptp.produc999471430t_unit))
% 0.34/0.53  (define @t221 () (_ (_ tptp.member235934813t_unit @t220) @t219))
% 0.34/0.53  (define @t222 () (@list @t220))
% 0.34/0.53  (define @t223 () (@var "A" tptp.set_Pr1774599175_sc_sz))
% 0.34/0.53  (define @t224 () (@var "X4" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t225 () (@var "A" tptp.set_Pr1389752855real_c))
% 0.34/0.53  (define @t226 () (@var "X4" tptp.produc190496183real_c))
% 0.34/0.53  (define @t227 () (_ tptp.member1895684704real_c @t226))
% 0.34/0.53  (define @t228 () (_ @t227 @t225))
% 0.34/0.53  (define @t229 () (@list @t226))
% 0.34/0.53  (define @t230 () (@var "Q" (-> tptp.produc190496183real_c Bool)))
% 0.34/0.53  (define @t231 () (_ @t144 @t193))
% 0.34/0.53  (define @t232 () (@list @t193))
% 0.34/0.53  (define @t233 () (not (= @t21 @t20)))
% 0.34/0.53  (define @t234 () (@list @t22 @t21 @t20 @t19 @t18 @t17 @t16 @t15 @t14 @t13))
% 0.34/0.53  (define @t235 () (not (= @t22 @t20)))
% 0.34/0.53  (define @t236 () (not (= @t22 @t21)))
% 0.34/0.53  (define @t237 () (not (= @t14 @t13)))
% 0.34/0.53  (define @t238 () (not (= @t15 @t13)))
% 0.34/0.53  (define @t239 () (not (= @t15 @t14)))
% 0.34/0.53  (define @t240 () (not (= @t16 @t13)))
% 0.34/0.53  (define @t241 () (not (= @t16 @t14)))
% 0.34/0.53  (define @t242 () (not (= @t16 @t15)))
% 0.34/0.53  (define @t243 () (not (= @t19 @t17)))
% 0.34/0.53  (define @t244 () (not (= @t18 @t17)))
% 0.34/0.53  (define @t245 () (not (= @t19 @t18)))
% 0.34/0.53  (define @t246 () (@var "R2" tptp.set_Pr1774599175_sc_sz))
% 0.34/0.53  (define @t247 () (@var "S3" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t248 () (@var "R" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t249 () (_ tptp.produc1822718231_sc_sz @t248))
% 0.34/0.53  (define @t250 () (@var "S2" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t251 () (@var "R2" tptp.set_Pr2041213564t_unit))
% 0.34/0.53  (define @t252 () (@var "S3" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t253 () (@var "R" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t254 () (_ tptp.produc502616768t_unit @t253))
% 0.34/0.53  (define @t255 () (@var "S2" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t256 () (@var "R2" tptp.set_Pr754230471real_c))
% 0.34/0.53  (define @t257 () (@var "S3" tptp.produc190496183real_c))
% 0.34/0.53  (define @t258 () (@var "R" tptp.produc190496183real_c))
% 0.34/0.53  (define @t259 () (_ tptp.produc1687028567real_c @t258))
% 0.34/0.53  (define @t260 () (@var "S2" tptp.produc190496183real_c))
% 0.34/0.53  (define @t261 () (@var "R2" tptp.set_Pr1389752855real_c))
% 0.34/0.53  (define @t262 () (@var "S3" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t263 () (@var "R" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t264 () (_ tptp.produc394644079real_c @t263))
% 0.34/0.53  (define @t265 () (@var "S2" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t266 () (@var "R2" tptp.set_Pr1169339874_sc_sz))
% 0.34/0.53  (define @t267 () (@var "S3" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t268 () (@var "R" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t269 () (_ tptp.produc789536734_sc_sz @t268))
% 0.34/0.53  (define @t270 () (@var "S2" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t271 () (@var "F2" (-> tptp.produc866628903_sc_sz Bool)))
% 0.34/0.53  (define @t272 () (_ (_ (_ tptp.produc880541325c_sz_o @t271) @t80) @t77))
% 0.34/0.53  (define @t273 () (_ @t271 @t82))
% 0.34/0.53  (define @t274 () (@list @t271 @t80 @t77))
% 0.34/0.53  (define @t275 () (@var "F2" (-> tptp.produc190496183real_c Bool)))
% 0.34/0.53  (define @t276 () (_ (_ (_ tptp.produc1716060341al_c_o @t275) @t89) @t86))
% 0.34/0.53  (define @t277 () (_ @t275 @t91))
% 0.34/0.53  (define @t278 () (@list @t275 @t89 @t86))
% 0.34/0.53  (define @t279 () (@var "F2" (-> tptp.produc999471430t_unit Bool)))
% 0.34/0.53  (define @t280 () (_ (_ (_ tptp.produc38128778unit_o @t279) @t98) @t95))
% 0.34/0.53  (define @t281 () (_ @t279 @t100))
% 0.34/0.53  (define @t282 () (@list @t279 @t98 @t95))
% 0.34/0.53  (define @t283 () (@var "F2" (-> tptp.produc640052711real_c Bool)))
% 0.34/0.53  (define @t284 () (_ (_ (_ tptp.produc440529997al_c_o @t283) @t107) @t104))
% 0.34/0.53  (define @t285 () (_ @t283 @t109))
% 0.34/0.53  (define @t286 () (@list @t283 @t107 @t104))
% 0.34/0.53  (define @t287 () (@var "F2" (-> tptp.produc1821101996_sc_sz Bool)))
% 0.34/0.53  (define @t288 () (_ tptp.produc1086673900c_sz_o @t287))
% 0.34/0.53  (define @t289 () (_ (_ @t288 @t116) @t113))
% 0.34/0.53  (define @t290 () (_ @t287 @t118))
% 0.34/0.53  (define @t291 () (@list @t287 @t116 @t113))
% 0.34/0.53  (define @t292 () (@var "X" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t293 () (@var "Y" tptp.list_f1238882004_sc_sz))
% 0.34/0.53  (define @t294 () (_ (_ tptp.produc1822718231_sc_sz @t293) @t292))
% 0.34/0.53  (define @t295 () (_ tptp.produc1822718231_sc_sz @t292))
% 0.34/0.53  (define @t296 () (_ @t295 @t293))
% 0.34/0.53  (define @t297 () (@var "X" tptp.produc190496183real_c))
% 0.34/0.53  (define @t298 () (_ (_ tptp.produc1687028567real_c @t169) @t297))
% 0.34/0.53  (define @t299 () (_ tptp.produc1687028567real_c @t297))
% 0.34/0.53  (define @t300 () (_ @t299 @t169))
% 0.34/0.53  (define @t301 () (@var "X" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t302 () (@var "Y" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t303 () (_ (_ tptp.produc394644079real_c @t302) @t301))
% 0.34/0.53  (define @t304 () (_ tptp.produc394644079real_c @t301))
% 0.34/0.53  (define @t305 () (_ @t304 @t302))
% 0.34/0.53  (define @t306 () (@var "X" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t307 () (@var "Y" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t308 () (_ (_ tptp.produc789536734_sc_sz @t307) @t306))
% 0.34/0.53  (define @t309 () (_ tptp.produc502616768t_unit @t306))
% 0.34/0.53  (define @t310 () (_ @t309 @t307))
% 0.34/0.53  (define @t311 () (@var "X" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t312 () (_ (_ tptp.produc502616768t_unit @t168) @t311))
% 0.34/0.53  (define @t313 () (_ tptp.produc789536734_sc_sz @t311))
% 0.34/0.53  (define @t314 () (_ @t313 @t168))
% 0.34/0.53  (define @t315 () (@var "Phi2" tptp.formula_sf_sc_sz))
% 0.34/0.53  (define @t316 () (@var "I" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t317 () (@var "Nu" tptp.produc1149990247eal_sz))
% 0.34/0.53  (define @t318 () (_ tptp.produc245128480t_unit @t173))
% 0.34/0.53  (define @t319 () (_ tptp.produc532048446_sc_sz @t175))
% 0.34/0.53  (define @t320 () (_ tptp.produc704157711real_c @t172))
% 0.34/0.53  (define @t321 () (_ tptp.member1895684704real_c @t305))
% 0.34/0.53  (define @t322 () (@var "F2" (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz)))
% 0.34/0.53  (define @t323 () (@var "F2" (-> tptp.finite1398487019real_c tptp.finite1398487019real_c)))
% 0.34/0.53  (define @t324 () (_ @t323 @t302))
% 0.34/0.53  (define @t325 () (@var "F2" (-> tptp.denota610675952t_unit tptp.denota610675952t_unit)))
% 0.34/0.53  (define @t326 () (@var "F2" (-> tptp.produc190496183real_c tptp.produc190496183real_c)))
% 0.34/0.53  (define @t327 () (@var "F2" (-> tptp.produc866628903_sc_sz tptp.produc866628903_sc_sz)))
% 0.34/0.53  (define @t328 () (@var "C2" (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.set_Pr1389752855real_c)))
% 0.34/0.53  (define @t329 () (_ tptp.produc237521996real_c @t328))
% 0.34/0.53  (define @t330 () (@var "Z" tptp.produc190496183real_c))
% 0.34/0.53  (define @t331 () (_ tptp.member1895684704real_c @t330))
% 0.34/0.53  (define @t332 () (_ @t331 (_ @t329 @t175)))
% 0.34/0.53  (define @t333 () (= @t175 @t165))
% 0.34/0.53  (define @t334 () (@var "C2" (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.set_Fi1407883041real_c)))
% 0.34/0.53  (define @t335 () (_ tptp.produc29022117real_c @t334))
% 0.34/0.53  (define @t336 () (@var "Z" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t337 () (_ tptp.member1261661570real_c @t336))
% 0.34/0.53  (define @t338 () (_ @t337 (_ @t335 @t172)))
% 0.34/0.53  (define @t339 () (= @t172 @t146))
% 0.34/0.53  (define @t340 () (@var "C2" (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz tptp.set_Fi1407883041real_c)))
% 0.34/0.53  (define @t341 () (_ tptp.produc1449736269real_c @t340))
% 0.34/0.53  (define @t342 () (_ @t337 (_ @t341 @t171)))
% 0.34/0.53  (define @t343 () (= @t171 @t140))
% 0.34/0.53  (define @t344 () (@var "C2" (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.set_Pr1389752855real_c)))
% 0.34/0.53  (define @t345 () (_ tptp.produc923381907real_c @t344))
% 0.34/0.53  (define @t346 () (_ @t331 (_ @t345 @t172)))
% 0.34/0.53  (define @t347 () (@var "C2" (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz tptp.set_Pr1389752855real_c)))
% 0.34/0.53  (define @t348 () (_ tptp.produc6841835real_c @t347))
% 0.34/0.53  (define @t349 () (_ @t331 (_ @t348 @t171)))
% 0.34/0.53  (define @t350 () (@var "C2" (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.set_Pr1774599175_sc_sz)))
% 0.34/0.53  (define @t351 () (_ tptp.produc642283651_sc_sz @t350))
% 0.34/0.53  (define @t352 () (@var "Z" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t353 () (_ tptp.member245028432_sc_sz @t352))
% 0.34/0.53  (define @t354 () (_ @t353 (_ @t351 @t172)))
% 0.34/0.53  (define @t355 () (@var "C2" (-> tptp.produc190496183real_c tptp.produc190496183real_c tptp.set_Fi1407883041real_c)))
% 0.34/0.53  (define @t356 () (_ tptp.produc1066779277real_c @t355))
% 0.34/0.53  (define @t357 () (_ @t337 (_ @t356 @t174)))
% 0.34/0.53  (define @t358 () (= @t174 @t159))
% 0.34/0.53  (define @t359 () (@var "C2" (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.set_Fi1407883041real_c)))
% 0.34/0.53  (define @t360 () (_ tptp.produc2068697644real_c @t359))
% 0.34/0.53  (define @t361 () (_ @t337 (_ @t360 @t175)))
% 0.34/0.53  (define @t362 () (@var "C2" (-> tptp.produc866628903_sc_sz tptp.denota610675952t_unit tptp.set_Fi1407883041real_c)))
% 0.34/0.53  (define @t363 () (_ tptp.produc1368849166real_c @t362))
% 0.34/0.53  (define @t364 () (_ @t337 (_ @t363 @t173)))
% 0.34/0.53  (define @t365 () (= @t173 @t153))
% 0.34/0.53  (define @t366 () (@var "C2" (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz tptp.set_Pr1774599175_sc_sz)))
% 0.34/0.53  (define @t367 () (_ tptp.produc1563580891_sc_sz @t366))
% 0.34/0.53  (define @t368 () (_ @t353 (_ @t367 @t171)))
% 0.34/0.53  (define @t369 () (@var "C2" (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz Bool)))
% 0.34/0.53  (define @t370 () (_ (_ tptp.produc2039065452c_sz_o @t369) @t171))
% 0.34/0.53  (define @t371 () (@var "C2" (-> tptp.finite1398487019real_c tptp.finite1398487019real_c Bool)))
% 0.34/0.53  (define @t372 () (_ (_ tptp.produc353381908al_c_o @t371) @t172))
% 0.34/0.53  (define @t373 () (@var "C2" (-> tptp.produc866628903_sc_sz tptp.denota610675952t_unit Bool)))
% 0.34/0.53  (define @t374 () (_ (_ tptp.produc1718498667unit_o @t373) @t173))
% 0.34/0.53  (define @t375 () (@var "C2" (-> tptp.produc190496183real_c tptp.produc190496183real_c Bool)))
% 0.34/0.53  (define @t376 () (_ (_ tptp.produc1726730540al_c_o @t375) @t174))
% 0.34/0.53  (define @t377 () (@var "C2" (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz Bool)))
% 0.34/0.53  (define @t378 () (_ (_ tptp.produc619560141c_sz_o @t377) @t175))
% 0.34/0.53  (define @t379 () (@var "F2" (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz Bool)))
% 0.34/0.53  (define @t380 () (_ (_ tptp.produc2039065452c_sz_o @t379) @t82))
% 0.34/0.53  (define @t381 () (_ (_ @t379 @t80) @t77))
% 0.34/0.53  (define @t382 () (@list @t379 @t80 @t77))
% 0.34/0.53  (define @t383 () (@var "F2" (-> tptp.finite1398487019real_c tptp.finite1398487019real_c Bool)))
% 0.34/0.53  (define @t384 () (_ (_ tptp.produc353381908al_c_o @t383) @t91))
% 0.34/0.53  (define @t385 () (_ (_ @t383 @t89) @t86))
% 0.34/0.53  (define @t386 () (@list @t383 @t89 @t86))
% 0.34/0.53  (define @t387 () (@var "F2" (-> tptp.produc866628903_sc_sz tptp.denota610675952t_unit Bool)))
% 0.34/0.53  (define @t388 () (_ tptp.produc1718498667unit_o @t387))
% 0.34/0.53  (define @t389 () (_ @t388 @t100))
% 0.34/0.53  (define @t390 () (_ (_ @t387 @t98) @t95))
% 0.34/0.53  (define @t391 () (@list @t387 @t98 @t95))
% 0.34/0.53  (define @t392 () (@var "F2" (-> tptp.produc190496183real_c tptp.produc190496183real_c Bool)))
% 0.34/0.53  (define @t393 () (_ (_ tptp.produc1726730540al_c_o @t392) @t109))
% 0.34/0.53  (define @t394 () (_ (_ @t392 @t107) @t104))
% 0.34/0.53  (define @t395 () (@list @t392 @t107 @t104))
% 0.34/0.53  (define @t396 () (@var "F2" (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz Bool)))
% 0.34/0.53  (define @t397 () (_ tptp.produc619560141c_sz_o @t396))
% 0.34/0.53  (define @t398 () (_ @t397 @t118))
% 0.34/0.53  (define @t399 () (_ (_ @t396 @t116) @t113))
% 0.34/0.53  (define @t400 () (@list @t396 @t116 @t113))
% 0.34/0.53  (define @t401 () (@var "F2" (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.produc190496183real_c)))
% 0.34/0.53  (define @t402 () (_ (_ @t401 @t116) @t113))
% 0.34/0.53  (define @t403 () (_ tptp.produc1575513068real_c @t401))
% 0.34/0.53  (define @t404 () (@var "F2" (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.set_Pr1389752855real_c)))
% 0.34/0.53  (define @t405 () (_ tptp.produc237521996real_c @t404))
% 0.34/0.53  (define @t406 () (@var "F2" (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.produc190496183real_c)))
% 0.34/0.53  (define @t407 () (_ (_ @t406 @t89) @t86))
% 0.34/0.53  (define @t408 () (_ tptp.produc107375667real_c @t406))
% 0.34/0.53  (define @t409 () (@var "F2" (-> tptp.produc866628903_sc_sz tptp.denota610675952t_unit tptp.produc1821101996_sc_sz)))
% 0.34/0.53  (define @t410 () (_ tptp.produc435149849_sc_sz @t409))
% 0.34/0.53  (define @t411 () (@var "F2" (-> tptp.produc1821101996_sc_sz tptp.produc190496183real_c)))
% 0.34/0.53  (define @t412 () (@list @t411))
% 0.34/0.53  (define @t413 () (@list @t287))
% 0.34/0.53  (define @t414 () (@var "F2" (-> tptp.produc1821101996_sc_sz tptp.set_Pr1389752855real_c)))
% 0.34/0.53  (define @t415 () (@list @t414))
% 0.34/0.53  (define @t416 () (@list @t326))
% 0.34/0.53  (define @t417 () (@var "F2" (-> tptp.produc999471430t_unit tptp.produc1821101996_sc_sz)))
% 0.34/0.53  (define @t418 () (@list @t417))
% 0.34/0.53  (define @t419 () (@var "Y4" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t420 () (@var "X4" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t421 () (@list @t419 @t420))
% 0.34/0.53  (define @t422 () (@var "Y4" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t423 () (@list @t422 @t224))
% 0.34/0.53  (define @t424 () (@var "F2" (-> tptp.produc866628903_sc_sz tptp.denota610675952t_unit tptp.produc190496183real_c)))
% 0.34/0.53  (define @t425 () (@var "F2" (-> tptp.produc866628903_sc_sz tptp.denota610675952t_unit tptp.set_Pr1389752855real_c)))
% 0.34/0.53  (define @t426 () (@var "Y4" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t427 () (@var "F2" (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.produc1821101996_sc_sz)))
% 0.34/0.53  (define @t428 () (_ tptp.member1895684704real_c @t91))
% 0.34/0.53  (define @t429 () (_ @t428 @t225))
% 0.34/0.53  (define @t430 () (_ tptp.member1057565379_sc_sz @t118))
% 0.34/0.53  (define @t431 () (_ @t430 @t213))
% 0.34/0.53  (define @t432 () (@var "F2" (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.finite1398487019real_c)))
% 0.34/0.53  (define @t433 () (@var "F2" (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz tptp.finite1398487019real_c)))
% 0.34/0.53  (define @t434 () (_ (_ tptp.member245028432_sc_sz @t82) @t223))
% 0.34/0.53  (define @t435 () (@var "F2" (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz tptp.produc190496183real_c)))
% 0.34/0.53  (define @t436 () (@var "F2" (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.produc866628903_sc_sz)))
% 0.34/0.53  (define @t437 () (@var "F2" (-> tptp.produc190496183real_c tptp.produc190496183real_c tptp.finite1398487019real_c)))
% 0.34/0.53  (define @t438 () (_ tptp.member346808080real_c @t109))
% 0.34/0.53  (define @t439 () (@var "F2" (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.finite1398487019real_c)))
% 0.34/0.53  (define @t440 () (@var "F2" (-> tptp.produc866628903_sc_sz tptp.denota610675952t_unit tptp.finite1398487019real_c)))
% 0.34/0.53  (define @t441 () (_ (_ tptp.produc789536734_sc_sz @t420) @t419))
% 0.34/0.53  (define @t442 () (@var "C3" (-> tptp.produc1821101996_sc_sz Bool)))
% 0.34/0.53  (define @t443 () (@var "C2" Bool))
% 0.34/0.53  (define @t444 () (@list @t420 @t419))
% 0.34/0.53  (define @t445 () (@var "X22" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t446 () (@var "X12" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t447 () (_ (_ @t396 @t446) @t445))
% 0.34/0.53  (define @t448 () (@var "H" (-> Bool Bool)))
% 0.34/0.53  (define @t449 () (@list @t446 @t445))
% 0.34/0.53  (define @t450 () (_ @t397 @t162))
% 0.34/0.53  (define @t451 () (@var "X22" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t452 () (@var "X12" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t453 () (@var "H" (-> tptp.produc190496183real_c tptp.produc190496183real_c)))
% 0.34/0.53  (define @t454 () (_ (_ @t401 @t446) @t445))
% 0.34/0.53  (define @t455 () (@var "H" (-> tptp.produc190496183real_c Bool)))
% 0.34/0.53  (define @t456 () (_ @t403 @t162))
% 0.34/0.53  (define @t457 () (@var "H" (-> Bool tptp.produc190496183real_c)))
% 0.34/0.53  (define @t458 () (@var "H" (-> Bool tptp.set_Pr1389752855real_c)))
% 0.34/0.53  (define @t459 () (_ (_ @t404 @t446) @t445))
% 0.34/0.53  (define @t460 () (@var "H" (-> tptp.set_Pr1389752855real_c Bool)))
% 0.34/0.53  (define @t461 () (_ @t405 @t162))
% 0.34/0.53  (define @t462 () (@var "H" (-> tptp.produc190496183real_c tptp.set_Pr1389752855real_c)))
% 0.34/0.53  (define @t463 () (@var "H" (-> tptp.set_Pr1389752855real_c tptp.produc190496183real_c)))
% 0.34/0.53  (define @t464 () (@var "H" (-> tptp.set_Pr1389752855real_c tptp.set_Pr1389752855real_c)))
% 0.34/0.53  (define @t465 () (@var "G" (-> tptp.produc1821101996_sc_sz tptp.produc190496183real_c)))
% 0.34/0.53  (define @t466 () (@var "G" (-> tptp.produc1821101996_sc_sz Bool)))
% 0.34/0.53  (define @t467 () (@var "G" (-> tptp.produc1821101996_sc_sz tptp.set_Pr1389752855real_c)))
% 0.34/0.53  (define @t468 () (@var "G" (-> tptp.produc190496183real_c tptp.produc190496183real_c)))
% 0.34/0.53  (define @t469 () (@var "G" (-> tptp.produc999471430t_unit tptp.produc1821101996_sc_sz)))
% 0.34/0.53  (define @t470 () (_ (_ tptp.produc394644079real_c @t212) @t426))
% 0.34/0.53  (define @t471 () (@list @t212 @t426))
% 0.34/0.53  (define @t472 () (@var "P" (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.produc190496183real_c)))
% 0.34/0.53  (define @t473 () (@var "Z" tptp.produc1821101996_sc_sz))
% 0.34/0.53  (define @t474 () (= @t473 @t199))
% 0.34/0.53  (define @t475 () (@var "Q" (-> Bool Bool)))
% 0.34/0.53  (define @t476 () (@var "P" (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.set_Pr1389752855real_c)))
% 0.34/0.53  (define @t477 () (@var "Q" (-> tptp.set_Pr1389752855real_c Bool)))
% 0.34/0.53  (define @t478 () (@var "P" (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.produc190496183real_c)))
% 0.34/0.53  (define @t479 () (@var "P" (-> tptp.produc866628903_sc_sz tptp.denota610675952t_unit tptp.produc1821101996_sc_sz)))
% 0.34/0.53  (define @t480 () (@var "Q" (-> tptp.produc1821101996_sc_sz Bool)))
% 0.34/0.53  (define @t481 () (@var "Z" tptp.produc999471430t_unit))
% 0.34/0.53  (define @t482 () (@var "Y5" tptp.set_Pr1389752855real_c))
% 0.34/0.53  (define @t483 () (_ tptp.image_738229701real_c @t326))
% 0.34/0.53  (define @t484 () (_ @t483 @t225))
% 0.34/0.53  (define @t485 () (_ tptp.member1895684704real_c @t104))
% 0.34/0.53  (define @t486 () (_ @t485 @t484))
% 0.34/0.53  (define @t487 () (_ tptp.member1895684704real_c @t297))
% 0.34/0.53  (define @t488 () (_ @t487 @t225))
% 0.34/0.53  (define @t489 () (_ @t326 @t297))
% 0.34/0.53  (define @t490 () (= @t104 @t489))
% 0.34/0.53  (define @t491 () (_ tptp.member1261661570real_c @t86))
% 0.34/0.53  (define @t492 () (_ @t491 (_ (_ tptp.image_1514048989real_c @t323) @t211)))
% 0.34/0.53  (define @t493 () (_ (_ tptp.member1261661570real_c @t301) @t211))
% 0.34/0.53  (define @t494 () (_ @t323 @t301))
% 0.34/0.53  (define @t495 () (= @t86 @t494))
% 0.34/0.53  (define @t496 () (@var "F2" (-> tptp.produc190496183real_c tptp.finite1398487019real_c)))
% 0.34/0.53  (define @t497 () (_ @t491 (_ (_ tptp.image_14429021real_c @t496) @t225)))
% 0.34/0.53  (define @t498 () (= @t86 (_ @t496 @t297)))
% 0.34/0.53  (define @t499 () (@var "F2" (-> tptp.finite1398487019real_c tptp.produc190496183real_c)))
% 0.34/0.53  (define @t500 () (_ @t485 (_ (_ tptp.image_1461287749real_c @t499) @t211)))
% 0.34/0.53  (define @t501 () (= @t104 (_ @t499 @t301)))
% 0.34/0.53  (define @t502 () (@var "F2" (-> tptp.finite1398487019real_c tptp.produc866628903_sc_sz)))
% 0.34/0.53  (define @t503 () (_ tptp.member245028432_sc_sz @t113))
% 0.34/0.53  (define @t504 () (_ @t503 (_ (_ tptp.image_290183605_sc_sz @t502) @t211)))
% 0.34/0.53  (define @t505 () (= @t113 (_ @t502 @t301)))
% 0.34/0.53  (define @t506 () (@var "F2" (-> tptp.produc866628903_sc_sz tptp.finite1398487019real_c)))
% 0.34/0.53  (define @t507 () (_ (_ tptp.image_1332486093real_c @t506) @t223))
% 0.34/0.53  (define @t508 () (_ @t491 @t507))
% 0.34/0.53  (define @t509 () (_ (_ tptp.member245028432_sc_sz @t306) @t223))
% 0.34/0.53  (define @t510 () (_ @t506 @t306))
% 0.34/0.53  (define @t511 () (= @t86 @t510))
% 0.34/0.53  (define @t512 () (@var "F2" (-> tptp.produc190496183real_c tptp.produc866628903_sc_sz)))
% 0.34/0.53  (define @t513 () (_ @t503 (_ (_ tptp.image_388766773_sc_sz @t512) @t225)))
% 0.34/0.53  (define @t514 () (= @t113 (_ @t512 @t297)))
% 0.34/0.53  (define @t515 () (@var "F2" (-> tptp.finite1398487019real_c tptp.produc640052711real_c)))
% 0.34/0.53  (define @t516 () (@var "B2" tptp.produc640052711real_c))
% 0.34/0.53  (define @t517 () (_ (_ tptp.member346808080real_c @t516) (_ (_ tptp.image_1746662005real_c @t515) @t211)))
% 0.34/0.53  (define @t518 () (= @t516 (_ @t515 @t301)))
% 0.34/0.53  (define @t519 () (@var "F2" (-> tptp.produc640052711real_c tptp.finite1398487019real_c)))
% 0.34/0.53  (define @t520 () (_ @t491 (_ (_ tptp.image_124598413real_c @t519) @t217)))
% 0.34/0.53  (define @t521 () (_ (_ tptp.member346808080real_c @t203) @t217))
% 0.34/0.53  (define @t522 () (= @t86 (_ @t519 @t203)))
% 0.34/0.53  (define @t523 () (@var "F2" (-> tptp.produc866628903_sc_sz tptp.produc190496183real_c)))
% 0.34/0.53  (define @t524 () (_ (_ tptp.image_1121381717real_c @t523) @t223))
% 0.34/0.53  (define @t525 () (_ @t485 @t524))
% 0.34/0.53  (define @t526 () (_ @t523 @t306))
% 0.34/0.53  (define @t527 () (= @t104 @t526))
% 0.34/0.53  (define @t528 () (@var "Ab" tptp.produc1821101996_sc_sz))
% 0.34/0.53  (define @t529 () (@var "Q" (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz Bool)))
% 0.34/0.53  (define @t530 () (@var "P" Bool))
% 0.34/0.53  (define @t531 () (@var "B5" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t532 () (@var "A5" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t533 () (@var "Uu" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t534 () (@var "X5" tptp.produc1821101996_sc_sz))
% 0.34/0.53  (define @t535 () (_ tptp.member1057565379_sc_sz @t534))
% 0.34/0.53  (define @t536 () (_ @t535 @t213))
% 0.34/0.53  (define @t537 () (@list @t534))
% 0.34/0.53  (define @t538 () (_ tptp.image_386905412real_c @t411))
% 0.34/0.53  (define @t539 () (_ @t538 @t213))
% 0.34/0.53  (define @t540 () (_ tptp.member1895684704real_c @t193))
% 0.34/0.53  (define @t541 () (@list @t411 @t213 @t144))
% 0.34/0.53  (define @t542 () (@var "F2" (-> tptp.produc1821101996_sc_sz tptp.produc999471430t_unit)))
% 0.34/0.53  (define @t543 () (@var "X3" tptp.produc999471430t_unit))
% 0.34/0.53  (define @t544 () (_ tptp.image_904562809t_unit @t542))
% 0.34/0.53  (define @t545 () (_ @t544 @t213))
% 0.34/0.53  (define @t546 () (_ tptp.member235934813t_unit @t543))
% 0.34/0.53  (define @t547 () (@list @t543))
% 0.34/0.53  (define @t548 () (@list @t542 @t213 @t150))
% 0.34/0.53  (define @t549 () (@var "X5" tptp.produc190496183real_c))
% 0.34/0.53  (define @t550 () (@var "F2" (-> tptp.produc190496183real_c tptp.produc1821101996_sc_sz)))
% 0.34/0.53  (define @t551 () (_ tptp.member1895684704real_c @t549))
% 0.34/0.53  (define @t552 () (_ @t551 @t225))
% 0.34/0.53  (define @t553 () (@list @t549))
% 0.34/0.53  (define @t554 () (@var "X3" tptp.produc1821101996_sc_sz))
% 0.34/0.53  (define @t555 () (_ @t163 @t554))
% 0.34/0.53  (define @t556 () (_ tptp.image_1259833374_sc_sz @t550))
% 0.34/0.53  (define @t557 () (_ @t556 @t225))
% 0.34/0.53  (define @t558 () (_ tptp.member1057565379_sc_sz @t554))
% 0.34/0.53  (define @t559 () (@list @t554))
% 0.34/0.53  (define @t560 () (@list @t550 @t225 @t163))
% 0.34/0.53  (define @t561 () (@list @t326 @t225 @t144))
% 0.34/0.53  (define @t562 () (@var "X5" tptp.produc999471430t_unit))
% 0.34/0.53  (define @t563 () (_ tptp.member235934813t_unit @t562))
% 0.34/0.53  (define @t564 () (@list @t562))
% 0.34/0.53  (define @t565 () (_ tptp.image_1426741113_sc_sz @t417))
% 0.34/0.53  (define @t566 () (_ @t565 @t219))
% 0.34/0.53  (define @t567 () (@list @t417 @t219 @t163))
% 0.34/0.53  (define @t568 () (@var "N" tptp.set_Pr1389752855real_c))
% 0.34/0.53  (define @t569 () (@var "G" (-> tptp.produc190496183real_c tptp.produc1821101996_sc_sz)))
% 0.34/0.53  (define @t570 () (@var "M" tptp.set_Pr1389752855real_c))
% 0.34/0.53  (define @t571 () (_ @t550 @t193))
% 0.34/0.53  (define @t572 () (_ @t540 @t568))
% 0.34/0.53  (define @t573 () (= @t570 @t568))
% 0.34/0.53  (define @t574 () (_ @t326 @t193))
% 0.34/0.53  (define @t575 () (@var "N" tptp.set_Pr1169339874_sc_sz))
% 0.34/0.53  (define @t576 () (@var "M" tptp.set_Pr1169339874_sc_sz))
% 0.34/0.53  (define @t577 () (_ @t411 @t554))
% 0.34/0.53  (define @t578 () (_ @t558 @t575))
% 0.34/0.53  (define @t579 () (= @t576 @t575))
% 0.34/0.53  (define @t580 () (@var "G" (-> tptp.produc1821101996_sc_sz tptp.produc999471430t_unit)))
% 0.34/0.53  (define @t581 () (_ @t542 @t554))
% 0.34/0.53  (define @t582 () (@var "N" tptp.set_Pr2041213564t_unit))
% 0.34/0.53  (define @t583 () (@var "M" tptp.set_Pr2041213564t_unit))
% 0.34/0.53  (define @t584 () (_ @t417 @t543))
% 0.34/0.53  (define @t585 () (_ @t558 @t213))
% 0.34/0.53  (define @t586 () (_ @t144 @t549))
% 0.34/0.53  (define @t587 () (_ @t540 @t225))
% 0.34/0.53  (define @t588 () (_ @t163 @t534))
% 0.34/0.53  (define @t589 () (_ @t326 @t226))
% 0.34/0.53  (define @t590 () (_ tptp.member1057565379_sc_sz @t473))
% 0.34/0.53  (define @t591 () (@var "F2" (-> tptp.produc866628903_sc_sz tptp.produc1821101996_sc_sz)))
% 0.34/0.53  (define @t592 () (@var "F2" (-> tptp.produc866628903_sc_sz tptp.produc640052711real_c)))
% 0.34/0.53  (define @t593 () (@var "F2" (-> tptp.produc866628903_sc_sz tptp.produc999471430t_unit)))
% 0.34/0.53  (define @t594 () (@var "S4" tptp.set_Pr1389752855real_c))
% 0.34/0.53  (define @t595 () (_ tptp.member1895684704real_c @t470))
% 0.34/0.53  (define @t596 () (@var "S4" tptp.set_Pr1169339874_sc_sz))
% 0.34/0.53  (define @t597 () (_ tptp.member1057565379_sc_sz @t441))
% 0.34/0.53  (define @t598 () (@var "B" (-> tptp.produc190496183real_c tptp.set_Pr1389752855real_c)))
% 0.34/0.53  (define @t599 () (_ @t485 (_ @t598 @t107)))
% 0.34/0.53  (define @t600 () (_ @t210 @t225))
% 0.34/0.53  (define @t601 () (_ (_ tptp.produc1017530376real_c @t225) @t598))
% 0.34/0.53  (define @t602 () (_ @t438 @t601))
% 0.34/0.53  (define @t603 () (@list @t107 @t104 @t225 @t598))
% 0.34/0.53  (define @t604 () (@var "B" (-> tptp.finite1398487019real_c tptp.set_Fi1407883041real_c)))
% 0.34/0.53  (define @t605 () (_ @t491 (_ @t604 @t89)))
% 0.34/0.53  (define @t606 () (_ @t205 @t211))
% 0.34/0.53  (define @t607 () (_ tptp.produc563345056real_c @t211))
% 0.34/0.53  (define @t608 () (_ @t607 @t604))
% 0.34/0.53  (define @t609 () (_ @t428 @t608))
% 0.34/0.53  (define @t610 () (@list @t89 @t86 @t211 @t604))
% 0.34/0.53  (define @t611 () (@var "B" (-> tptp.denota610675952t_unit tptp.set_Pr1774599175_sc_sz)))
% 0.34/0.53  (define @t612 () (_ @t503 (_ @t611 @t116)))
% 0.34/0.53  (define @t613 () (@var "A" tptp.set_De208295462t_unit))
% 0.34/0.53  (define @t614 () (_ (_ tptp.member754147591t_unit @t116) @t613))
% 0.34/0.53  (define @t615 () (_ (_ tptp.produc159603053_sc_sz @t613) @t611))
% 0.34/0.53  (define @t616 () (_ @t430 @t615))
% 0.34/0.53  (define @t617 () (@list @t116 @t113 @t613 @t611))
% 0.34/0.53  (define @t618 () (@var "C2" tptp.produc640052711real_c))
% 0.34/0.53  (define @t619 () (@var "C2" tptp.produc190496183real_c))
% 0.34/0.53  (define @t620 () (_ tptp.member1895684704real_c @t619))
% 0.34/0.53  (define @t621 () (@var "C2" tptp.produc1821101996_sc_sz))
% 0.34/0.53  (define @t622 () (_ tptp.member1057565379_sc_sz @t621))
% 0.34/0.53  (define @t623 () (@var "B" tptp.set_De208295462t_unit))
% 0.34/0.53  (define @t624 () (@var "I4" tptp.produc866628903_sc_sz))
% 0.34/0.53  (define @t625 () (@var "J2" tptp.denota610675952t_unit))
% 0.34/0.53  (define @t626 () (@var "B" tptp.set_Fi1407883041real_c))
% 0.34/0.53  (define @t627 () (@var "G" (-> tptp.produc866628903_sc_sz tptp.produc866628903_sc_sz)))
% 0.34/0.53  (define @t628 () (_ (_ tptp.produc789536734_sc_sz (_ @t325 @t116)) (_ @t627 @t113)))
% 0.34/0.53  (define @t629 () (_ (_ tptp.produc403791768_sc_sz @t325) @t627))
% 0.34/0.53  (define @t630 () (@var "R" tptp.set_Pr1389752855real_c))
% 0.34/0.53  (define @t631 () (@var "G" (-> tptp.finite1398487019real_c tptp.finite1398487019real_c)))
% 0.34/0.53  (define @t632 () (_ (_ tptp.image_738229701real_c (_ (_ tptp.produc368345510real_c @t323) @t631)) @t261))
% 0.34/0.53  (define @t633 () (_ @t428 @t261))
% 0.34/0.53  (define @t634 () (@var "G" (-> tptp.finite1398487019real_c tptp.produc866628903_sc_sz)))
% 0.34/0.53  (define @t635 () (@var "F2" (-> tptp.finite1398487019real_c tptp.denota610675952t_unit)))
% 0.34/0.53  (define @t636 () (_ (_ tptp.image_1259833374_sc_sz (_ (_ tptp.produc1784590311_sc_sz @t635) @t634)) @t261))
% 0.34/0.53  (define @t637 () (@var "G" (-> tptp.produc866628903_sc_sz tptp.finite1398487019real_c)))
% 0.34/0.53  (define @t638 () (@var "F2" (-> tptp.denota610675952t_unit tptp.finite1398487019real_c)))
% 0.34/0.53  (define @t639 () (_ (_ tptp.image_386905412real_c (_ (_ tptp.produc1612557567real_c @t638) @t637)) @t266))
% 0.34/0.53  (define @t640 () (_ @t430 @t266))
% 0.34/0.53  (define @t641 () (_ (_ tptp.image_1726193375_sc_sz @t629) @t266))
% 0.34/0.53  (define @t642 () (not (_ (_ tptp.member1895684704real_c @t182) @t261)))
% 0.34/0.53  (define @t643 () (not (_ (_ tptp.member1057565379_sc_sz @t199) @t266)))
% 0.34/0.53  (define @t644 () (@var "D" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t645 () (@var "C2" tptp.finite1398487019real_c))
% 0.34/0.53  (define @t646 () (@var "Omega" tptp.produc190496183real_c))
% 0.34/0.53  (define @t647 () (forall @t12 (=> (_ @t11 (_ tptp.static_SIGF_a_b_c tptp.phi)) (=> (_ @t10 (_ tptp.static_FVF_a_b_c tptp.phi)) (= (_ @t9 (_ @t7 tptp.phi)) (_ @t5 (_ @t3 tptp.phi)))))))
% 0.34/0.53  (define @t648 () (not (= @t647 @t647)))
% 0.34/0.53  (define @t649 () (@var "Phi" tptp.formula_a_b_c))
% 0.34/0.53  (define @t650 () (lambda (@list @t649) (forall @t12 (=> (_ @t11 (_ tptp.static_SIGF_a_b_c @t649)) (=> (_ @t10 (_ tptp.static_FVF_a_b_c @t649)) (= (_ @t9 (_ @t7 @t649)) (_ @t5 (_ @t3 @t649))))))))
% 0.34/0.53  (define @t651 () (@var "Pid42" tptp.sc))
% 0.34/0.53  (define @t652 () (@var "Pid32" tptp.sc))
% 0.34/0.53  (define @t653 () (@var "Pid22" tptp.sc))
% 0.34/0.53  (define @t654 () (@var "Pid12" tptp.sc))
% 0.34/0.53  (define @t655 () (@var "Fid32" tptp.sf))
% 0.34/0.53  (define @t656 () (@var "Fid12" tptp.sf))
% 0.34/0.53  (define @t657 () (@var "Fid22" tptp.sf))
% 0.34/0.53  (define @t658 () (@var "Vid32" tptp.sz))
% 0.34/0.53  (define @t659 () (@var "Vid12" tptp.sz))
% 0.34/0.53  (define @t660 () (@var "Vid22" tptp.sz))
% 0.34/0.53  (define @t661 () (lambda (@list @t659 @t660 @t658 @t656 @t657 @t655 @t654 @t653 @t652 @t651) (and (not (= @t659 @t660)) (not (= @t660 @t658)) (not (= @t659 @t658)) (not (= @t656 @t657)) (not (= @t657 @t655)) (not (= @t656 @t655)) (not (= @t654 @t653)) (not (= @t653 @t652)) (not (= @t654 @t652)) (not (= @t654 @t651)) (not (= @t653 @t651)) (not (= @t652 @t651)))))
% 0.34/0.53  (define @t662 () (@var "F" (-> tptp.produc1821101996_sc_sz Bool)))
% 0.34/0.53  (define @t663 () (lambda (@list @t662 @t532 @t531) (_ @t662 (_ (_ tptp.produc789536734_sc_sz @t532) @t531))))
% 0.34/0.53  (define @t664 () (lambda @t471 (_ @t595 tptp.top_to226056039real_c)))
% 0.34/0.53  (define @t665 () (lambda @t444 (_ @t597 tptp.top_to1499569298_sc_sz)))
% 0.34/0.53  (assume @p1 (forall (@list @t22 @t21 @t20 @t19 @t18 @t17 @t16 @t15 @t14 @t13 @t1) (=> @t23 (= (_ tptp.coinci501627771_a_b_c @t1) (forall @t12 (=> (_ @t11 (_ tptp.static_SIGF_a_b_c @t1)) (=> (_ @t10 (_ tptp.static_FVF_a_b_c @t1)) (= (_ @t9 (_ @t7 @t1)) (_ @t5 (_ @t3 @t1))))))))))
% 0.34/0.53  (assume @p2 (forall (@list @t25 @t26 @t24) (=> (_ (_ (_ tptp.denota69106024_a_b_c @t25) @t26) @t24) (_ (_ (_ tptp.denota69106024_a_b_c @t26) @t25) @t24))))
% 0.34/0.53  (assume @p3 (forall (@list @t28 @t27) (_ (_ (_ tptp.denota69106024_a_b_c @t28) @t28) @t27)))
% 0.34/0.53  (assume @p4 (forall (@list @t30 @t31 @t29) (=> (_ (_ (_ tptp.denota1997846518gree_c @t30) @t31) @t29) (_ (_ (_ tptp.denota1997846518gree_c @t31) @t30) @t29))))
% 0.34/0.53  (assume @p5 (forall (@list @t33 @t32) (_ (_ @t34 @t33) @t32)))
% 0.34/0.53  (assume @p6 (forall @t43 (= @t42 (and @t41 (=> @t40 @t38)))))
% 0.34/0.53  (assume @p7 (forall @t43 (= (_ @t37 (_ @t36 (_ (_ tptp.equiv_a_b_c @t35) @t39))) @t42)))
% 0.34/0.53  (assume @p8 (forall @t43 (= (_ @t37 (_ @t36 (_ (_ tptp.implies_a_b_c @t35) @t39))) @t41)))
% 0.34/0.53  (assume @p9 (= tptp.p_sc_sf_sz tptp.predic913887884_sf_sz))
% 0.34/0.53  (assume @p10 (forall (@list @t46) @t47))
% 0.34/0.53  (assume @p11 (forall (@list @t22 @t21 @t20 @t19 @t18 @t17 @t16 @t15 @t14 @t13 @t46) (=> @t23 @t47)))
% 0.34/0.53  (assume @p12 (forall (@list @t22 @t21 @t20 @t19 @t18 @t17 @t16 @t15 @t14 @t13 @t50 @t49 @t48) (=> @t23 (=> (forall (@list @t45 @t51) (_ (_ @t50 @t45) @t51)) (_ (_ @t50 @t49) @t48)))))
% 0.34/0.53  (assume @p13 (forall (@list @t22 @t21 @t20 @t19 @t18 @t17 @t16 @t15 @t14 @t13 @t52) (=> @t23 (= (_ tptp.p_sc_sf_sz @t52) (_ tptp.predic913887884_sf_sz @t52)))))
% 0.34/0.53  (assume @p14 (forall (@list @t56 @t54 @t55 @t53) (= (= (_ (_ tptp.produc1822718231_sc_sz @t56) @t54) (_ (_ tptp.produc1822718231_sc_sz @t55) @t53)) (and (= @t56 @t55) (= @t54 @t53)))))
% 0.34/0.53  (assume @p15 (forall (@list @t60 @t58 @t59 @t57) (= (= @t61 (_ (_ tptp.produc394644079real_c @t59) @t57)) (and (= @t60 @t59) (= @t58 @t57)))))
% 0.34/0.53  (assume @p16 (forall (@list @t65 @t63 @t64 @t62) (= (= @t66 (_ (_ tptp.produc502616768t_unit @t64) @t62)) (and (= @t65 @t64) (= @t63 @t62)))))
% 0.34/0.53  (assume @p17 (forall (@list @t70 @t68 @t69 @t67) (= (= (_ (_ tptp.produc1687028567real_c @t70) @t68) (_ (_ tptp.produc1687028567real_c @t69) @t67)) (and (= @t70 @t69) (= @t68 @t67)))))
% 0.34/0.53  (assume @p18 (forall (@list @t74 @t72 @t73 @t71) (= (= @t75 (_ (_ tptp.produc789536734_sc_sz @t73) @t71)) (and (= @t74 @t73) (= @t72 @t71)))))
% 0.34/0.53  (assume @p19 (forall @t84 (= @t83 (and @t81 @t78))))
% 0.34/0.53  (assume @p20 (forall @t93 (= @t92 (and @t90 @t87))))
% 0.34/0.53  (assume @p21 (forall @t102 (= @t101 (and @t99 @t96))))
% 0.34/0.53  (assume @p22 (forall @t111 (= @t110 (and @t108 @t105))))
% 0.34/0.53  (assume @p23 (forall @t120 (= @t119 (and @t117 @t114))))
% 0.34/0.53  (assume @p24 (forall @t128 (not (forall @t127 (not (= @t126 @t125))))))
% 0.34/0.53  (assume @p25 (forall @t136 (not (forall @t135 (not (= @t134 @t133))))))
% 0.34/0.53  (assume @p26 (forall (@list @t138 @t137) (=> @t142 (_ @t138 @t137))))
% 0.34/0.53  (assume @p27 (forall (@list @t144 @t143) (=> @t148 (_ @t144 @t143))))
% 0.34/0.53  (assume @p28 (forall (@list @t150 @t149) (=> @t155 (_ @t150 @t149))))
% 0.34/0.53  (assume @p29 (forall (@list @t157 @t156) (=> @t161 (_ @t157 @t156))))
% 0.34/0.53  (assume @p30 (forall (@list @t163 @t162) (=> @t167 (_ @t163 @t162))))
% 0.34/0.53  (assume @p31 (forall (@list @t168) (not (forall @t141 (not (= @t168 @t140))))))
% 0.34/0.53  (assume @p32 (forall (@list @t169) (not (forall @t147 (not (= @t169 @t146))))))
% 0.34/0.53  (assume @p33 (forall (@list @t170) (not (forall @t154 (not (= @t170 @t153))))))
% 0.34/0.53  (assume @p34 (forall @t128 (not (forall @t160 (not (= @t126 @t159))))))
% 0.34/0.53  (assume @p35 (forall @t136 (not (forall @t166 (not (= @t134 @t165))))))
% 0.34/0.53  (assume @p36 (forall @t84 (=> @t83 (not (=> @t81 (not @t78))))))
% 0.34/0.53  (assume @p37 (forall @t93 (=> @t92 (not (=> @t90 (not @t87))))))
% 0.34/0.53  (assume @p38 (forall @t102 (=> @t101 (not (=> @t99 (not @t96))))))
% 0.34/0.53  (assume @p39 (forall @t111 (=> @t110 (not (=> @t108 (not @t105))))))
% 0.34/0.53  (assume @p40 (forall @t120 (=> @t119 (not (=> @t117 (not @t114))))))
% 0.34/0.53  (assume @p41 (forall (@list @t138 @t171) (=> @t142 (_ @t138 @t171))))
% 0.34/0.53  (assume @p42 (forall (@list @t144 @t172) (=> @t148 (_ @t144 @t172))))
% 0.34/0.53  (assume @p43 (forall (@list @t150 @t173) (=> @t155 (_ @t150 @t173))))
% 0.34/0.53  (assume @p44 (forall (@list @t157 @t174) (=> @t161 (_ @t157 @t174))))
% 0.34/0.53  (assume @p45 (forall (@list @t163 @t175) (=> @t167 (_ @t163 @t175))))
% 0.34/0.53  (assume @p46 (forall (@list @t171) (exists @t179 @t178)))
% 0.34/0.53  (assume @p47 (forall @t185 (exists @t184 @t183)))
% 0.34/0.53  (assume @p48 (forall @t191 (exists @t190 @t189)))
% 0.34/0.53  (assume @p49 (forall (@list @t174) (exists @t196 @t195)))
% 0.34/0.53  (assume @p50 (forall @t202 (exists @t201 @t200)))
% 0.34/0.53  (assume @p51 (forall (@list @t157 @t203) (=> (forall @t127 (_ @t157 @t125)) (_ @t157 @t203))))
% 0.34/0.53  (assume @p52 (forall (@list @t163 @t46) (=> (forall @t135 (_ @t163 @t133)) (_ @t163 @t46))))
% 0.34/0.53  (assume @p53 (forall (@list @t89 @t204) (= (_ @t205 (_ tptp.collec230941376real_c @t204)) (_ @t204 @t89))))
% 0.34/0.53  (assume @p54 (forall (@list @t206 @t163) (= (_ (_ tptp.member1057565379_sc_sz @t206) (_ tptp.collec1199592193_sc_sz @t163)) (_ @t163 @t206))))
% 0.34/0.53  (assume @p55 (forall (@list @t207 @t157) (= (_ (_ tptp.member346808080real_c @t207) (_ tptp.collec1126017874real_c @t157)) (_ @t157 @t207))))
% 0.34/0.53  (assume @p56 (forall (@list @t208 @t150) (= (_ (_ tptp.member235934813t_unit @t208) (_ tptp.collec377961627t_unit @t150)) (_ @t150 @t208))))
% 0.34/0.53  (assume @p57 (forall (@list @t98 @t138) (= (_ (_ tptp.member245028432_sc_sz @t98) (_ tptp.collec2036662930_sc_sz @t138)) (_ @t138 @t98))))
% 0.34/0.53  (assume @p58 (forall (@list @t107 @t144) (= (_ @t210 @t209) (_ @t144 @t107))))
% 0.34/0.53  (assume @p59 (forall (@list @t211) (= (_ tptp.collec230941376real_c (lambda (@list @t212) (_ (_ tptp.member1261661570real_c @t212) @t211))) @t211)))
% 0.34/0.53  (assume @p60 (forall (@list @t213) (= (_ tptp.collec1199592193_sc_sz (lambda @t216 @t215)) @t213)))
% 0.34/0.53  (assume @p61 (forall (@list @t217) (= (_ tptp.collec1126017874real_c (lambda (@list @t218) (_ (_ tptp.member346808080real_c @t218) @t217))) @t217)))
% 0.34/0.53  (assume @p62 (forall (@list @t219) (= (_ tptp.collec377961627t_unit (lambda @t222 @t221)) @t219)))
% 0.34/0.53  (assume @p63 (forall (@list @t223) (= (_ tptp.collec2036662930_sc_sz (lambda (@list @t224) (_ (_ tptp.member245028432_sc_sz @t224) @t223))) @t223)))
% 0.34/0.53  (assume @p64 (forall (@list @t225) (= (_ tptp.collec1643251106real_c (lambda @t229 @t228)) @t225)))
% 0.34/0.53  (assume @p65 (forall (@list @t144 @t230) (=> (forall @t232 (= @t231 (_ @t230 @t193))) (= @t209 (_ tptp.collec1643251106real_c @t230)))))
% 0.34/0.53  (assume @p66 (forall @t234 (=> @t23 @t233)))
% 0.34/0.53  (assume @p67 (forall @t234 (=> @t23 @t235)))
% 0.34/0.53  (assume @p68 (forall @t234 (=> @t23 @t236)))
% 0.34/0.53  (assume @p69 (forall @t234 (=> @t23 @t237)))
% 0.34/0.53  (assume @p70 (forall @t234 (=> @t23 @t238)))
% 0.34/0.53  (assume @p71 (forall @t234 (=> @t23 @t239)))
% 0.34/0.53  (assume @p72 (forall @t234 (=> @t23 (not (= @t13 @t14)))))
% 0.34/0.53  (assume @p73 (forall @t234 (=> @t23 (not (= @t13 @t15)))))
% 0.34/0.53  (assume @p74 (forall @t234 (=> @t23 (not (= @t13 @t16)))))
% 0.34/0.53  (assume @p75 (forall @t234 (=> @t23 (not (= @t14 @t16)))))
% 0.34/0.53  (assume @p76 (forall @t234 (=> @t23 (not (= @t14 @t15)))))
% 0.34/0.53  (assume @p77 (forall @t234 (=> @t23 (not (= @t15 @t16)))))
% 0.34/0.53  (assume @p78 (forall @t234 (=> @t23 (not (= @t17 @t19)))))
% 0.34/0.53  (assume @p79 (forall @t234 (=> @t23 (not (= @t17 @t18)))))
% 0.34/0.53  (assume @p80 (forall @t234 (=> @t23 (not (= @t18 @t19)))))
% 0.34/0.53  (assume @p81 (forall @t234 (=> @t23 (not (= @t20 @t22)))))
% 0.34/0.53  (assume @p82 (forall @t234 (=> @t23 (not (= @t20 @t21)))))
% 0.34/0.53  (assume @p83 (forall @t234 (=> @t23 (not (= @t21 @t22)))))
% 0.34/0.53  (assume @p84 (forall @t234 (=> @t23 @t240)))
% 0.34/0.53  (assume @p85 (forall @t234 (=> @t23 @t241)))
% 0.34/0.53  (assume @p86 (forall @t234 (=> @t23 @t242)))
% 0.34/0.53  (assume @p87 (forall @t234 (=> @t23 @t243)))
% 0.34/0.53  (assume @p88 (forall @t234 (=> @t23 @t244)))
% 0.34/0.53  (assume @p89 (forall @t234 (=> @t23 @t245)))
% 0.34/0.53  (assume @p90 (forall @t234 (=> @t236 (=> @t233 (=> @t235 (=> @t245 (=> @t244 (=> @t243 (=> @t242 (=> @t239 (=> @t241 (=> @t240 (=> @t238 (=> @t237 @t23))))))))))))))
% 0.34/0.53  (assume @p91 (forall (@list @t248 @t250 @t246 @t247) (=> (_ (_ tptp.member245028432_sc_sz (_ @t249 @t250)) @t246) (=> (= @t247 @t250) (_ (_ tptp.member245028432_sc_sz (_ @t249 @t247)) @t246)))))
% 0.34/0.53  (assume @p92 (forall (@list @t253 @t255 @t251 @t252) (=> (_ (_ tptp.member235934813t_unit (_ @t254 @t255)) @t251) (=> (= @t252 @t255) (_ (_ tptp.member235934813t_unit (_ @t254 @t252)) @t251)))))
% 0.34/0.53  (assume @p93 (forall (@list @t258 @t260 @t256 @t257) (=> (_ (_ tptp.member346808080real_c (_ @t259 @t260)) @t256) (=> (= @t257 @t260) (_ (_ tptp.member346808080real_c (_ @t259 @t257)) @t256)))))
% 0.34/0.53  (assume @p94 (forall (@list @t263 @t265 @t261 @t262) (=> (_ (_ tptp.member1895684704real_c (_ @t264 @t265)) @t261) (=> (= @t262 @t265) (_ (_ tptp.member1895684704real_c (_ @t264 @t262)) @t261)))))
% 0.34/0.53  (assume @p95 (forall (@list @t268 @t270 @t266 @t267) (=> (_ (_ tptp.member1057565379_sc_sz (_ @t269 @t270)) @t266) (=> (= @t267 @t270) (_ (_ tptp.member1057565379_sc_sz (_ @t269 @t267)) @t266)))))
% 0.34/0.53  (assume @p96 (forall @t274 (=> @t273 @t272)))
% 0.34/0.53  (assume @p97 (forall @t278 (=> @t277 @t276)))
% 0.34/0.53  (assume @p98 (forall @t282 (=> @t281 @t280)))
% 0.34/0.53  (assume @p99 (forall @t286 (=> @t285 @t284)))
% 0.34/0.53  (assume @p100 (forall @t291 (=> @t290 @t289)))
% 0.34/0.53  (assume @p101 (forall (@list @t292 @t293) (= (_ tptp.produc1145837239_sc_sz @t296) @t294)))
% 0.34/0.53  (assume @p102 (forall (@list @t297 @t169) (= (_ tptp.produc350724343real_c @t300) @t298)))
% 0.34/0.53  (assume @p103 (forall (@list @t301 @t302) (= (_ tptp.produc704157711real_c @t305) @t303)))
% 0.34/0.53  (assume @p104 (forall (@list @t306 @t307) (= (_ tptp.produc245128480t_unit @t310) @t308)))
% 0.34/0.53  (assume @p105 (forall (@list @t311 @t168) (= (_ tptp.produc532048446_sc_sz @t314) @t312)))
% 0.34/0.53  (assume @p106 (forall (@list @t22 @t21 @t20 @t19 @t18 @t17 @t16 @t15 @t14 @t13 @t315) (=> @t23 (= (_ tptp.denota1946510237_sc_sz @t315) (forall (@list @t316 @t317) (=> (_ tptp.denota1579475975_sc_sz @t316) (_ (_ tptp.member630771088eal_sz @t317) (_ (_ tptp.denota1711272799_sc_sz @t316) @t315))))))))
% 0.34/0.53  (assume @p107 (forall @t191 (= (_ tptp.produc532048446_sc_sz @t318) @t173)))
% 0.34/0.53  (assume @p108 (forall @t202 (= (_ tptp.produc245128480t_unit @t319) @t175)))
% 0.34/0.53  (assume @p109 (forall @t185 (= (_ tptp.produc704157711real_c @t320) @t172)))
% 0.34/0.53  (assume @p110 (forall @t274 (=> @t272 @t273)))
% 0.34/0.53  (assume @p111 (forall @t278 (=> @t276 @t277)))
% 0.34/0.53  (assume @p112 (forall @t282 (=> @t280 @t281)))
% 0.34/0.53  (assume @p113 (forall @t286 (=> @t284 @t285)))
% 0.34/0.53  (assume @p114 (forall @t291 (=> @t289 @t290)))
% 0.34/0.53  (assume @p115 (forall (@list @t293 @t292 @t223) (= (_ (_ tptp.member245028432_sc_sz @t294) (_ (_ tptp.image_1313166277_sc_sz tptp.produc1145837239_sc_sz) @t223)) (_ (_ tptp.member245028432_sc_sz @t296) @t223))))
% 0.34/0.53  (assume @p116 (forall (@list @t169 @t297 @t217) (= (_ (_ tptp.member346808080real_c @t298) (_ (_ tptp.image_2041365445real_c tptp.produc350724343real_c) @t217)) (_ (_ tptp.member346808080real_c @t300) @t217))))
% 0.34/0.53  (assume @p117 (forall (@list @t302 @t301 @t225) (= (_ (_ tptp.member1895684704real_c @t303) (_ (_ tptp.image_738229701real_c tptp.produc704157711real_c) @t225)) (_ @t321 @t225))))
% 0.34/0.53  (assume @p118 (forall (@list @t168 @t311 @t213) (= (_ (_ tptp.member235934813t_unit @t312) (_ (_ tptp.image_904562809t_unit tptp.produc532048446_sc_sz) @t213)) (_ (_ tptp.member1057565379_sc_sz @t314) @t213))))
% 0.34/0.53  (assume @p119 (forall (@list @t307 @t306 @t219) (= (_ (_ tptp.member1057565379_sc_sz @t308) (_ (_ tptp.image_1426741113_sc_sz tptp.produc245128480t_unit) @t219)) (_ (_ tptp.member235934813t_unit @t310) @t219))))
% 0.34/0.53  (assume @p120 (= tptp.produc383750338real_c tptp.produc1575513068real_c))
% 0.34/0.53  (assume @p121 (= tptp.produc198687651c_sz_o tptp.produc619560141c_sz_o))
% 0.34/0.53  (assume @p122 (= tptp.produc1894848802real_c tptp.produc237521996real_c))
% 0.34/0.53  (assume @p123 (= tptp.produc1442549981real_c tptp.produc107375667real_c))
% 0.34/0.53  (assume @p124 (= tptp.produc2099580355_sc_sz tptp.produc435149849_sc_sz))
% 0.34/0.53  (assume @p125 (forall (@list @t322 @t292 @t293) (= (_ (_ tptp.produc233219286_sc_sz @t322) @t296) (_ @t295 (_ @t322 @t293)))))
% 0.34/0.53  (assume @p126 (forall (@list @t323 @t301 @t302) (= (_ (_ tptp.produc981295297real_c @t323) @t305) (_ @t304 @t324))))
% 0.34/0.53  (assume @p127 (forall (@list @t325 @t306 @t307) (= (_ (_ tptp.produc793407943_sc_sz @t325) @t310) (_ @t309 (_ @t325 @t307)))))
% 0.34/0.53  (assume @p128 (forall (@list @t326 @t297 @t169) (= (_ (_ tptp.produc2089853305real_c @t326) @t300) (_ @t299 (_ @t326 @t169)))))
% 0.34/0.53  (assume @p129 (forall (@list @t327 @t311 @t168) (= (_ (_ tptp.produc1959054510t_unit @t327) @t314) (_ @t313 (_ @t327 @t168)))))
% 0.34/0.53  (assume @p130 (forall (@list @t175 @t330 @t328) (=> (forall @t166 (=> @t333 (_ @t331 (_ (_ @t328 @t131) @t164)))) @t332)))
% 0.34/0.53  (assume @p131 (forall (@list @t172 @t336 @t334) (=> (forall @t147 (=> @t339 (_ @t337 (_ (_ @t334 @t145) @t122)))) @t338)))
% 0.34/0.53  (assume @p132 (forall (@list @t171 @t336 @t340) (=> (forall @t141 (=> @t343 (_ @t337 (_ (_ @t340 @t139) @t130)))) @t342)))
% 0.34/0.53  (assume @p133 (forall (@list @t172 @t330 @t344) (=> (forall @t147 (=> @t339 (_ @t331 (_ (_ @t344 @t145) @t122)))) @t346)))
% 0.34/0.53  (assume @p134 (forall (@list @t171 @t330 @t347) (=> (forall @t141 (=> @t343 (_ @t331 (_ (_ @t347 @t139) @t130)))) @t349)))
% 0.34/0.53  (assume @p135 (forall (@list @t172 @t352 @t350) (=> (forall @t147 (=> @t339 (_ @t353 (_ (_ @t350 @t145) @t122)))) @t354)))
% 0.34/0.53  (assume @p136 (forall (@list @t174 @t336 @t355) (=> (forall @t160 (=> @t358 (_ @t337 (_ (_ @t355 @t123) @t158)))) @t357)))
% 0.34/0.53  (assume @p137 (forall (@list @t175 @t336 @t359) (=> (forall @t166 (=> @t333 (_ @t337 (_ (_ @t359 @t131) @t164)))) @t361)))
% 0.34/0.53  (assume @p138 (forall (@list @t173 @t336 @t362) (=> (forall @t154 (=> @t365 (_ @t337 (_ (_ @t362 @t152) @t151)))) @t364)))
% 0.34/0.53  (assume @p139 (forall (@list @t171 @t352 @t366) (=> (forall @t141 (=> @t343 (_ @t353 (_ (_ @t366 @t139) @t130)))) @t368)))
% 0.34/0.53  (assume @p140 (forall (@list @t330 @t328 @t116 @t113) (=> (_ @t331 (_ (_ @t328 @t116) @t113)) (_ @t331 (_ @t329 @t118)))))
% 0.34/0.53  (assume @p141 (forall (@list @t336 @t334 @t89 @t86) (=> (_ @t337 (_ (_ @t334 @t89) @t86)) (_ @t337 (_ @t335 @t91)))))
% 0.34/0.53  (assume @p142 (forall (@list @t336 @t340 @t80 @t77) (=> (_ @t337 (_ (_ @t340 @t80) @t77)) (_ @t337 (_ @t341 @t82)))))
% 0.34/0.53  (assume @p143 (forall (@list @t330 @t344 @t89 @t86) (=> (_ @t331 (_ (_ @t344 @t89) @t86)) (_ @t331 (_ @t345 @t91)))))
% 0.34/0.53  (assume @p144 (forall (@list @t330 @t347 @t80 @t77) (=> (_ @t331 (_ (_ @t347 @t80) @t77)) (_ @t331 (_ @t348 @t82)))))
% 0.34/0.53  (assume @p145 (forall (@list @t352 @t350 @t89 @t86) (=> (_ @t353 (_ (_ @t350 @t89) @t86)) (_ @t353 (_ @t351 @t91)))))
% 0.34/0.53  (assume @p146 (forall (@list @t336 @t355 @t107 @t104) (=> (_ @t337 (_ (_ @t355 @t107) @t104)) (_ @t337 (_ @t356 @t109)))))
% 0.34/0.53  (assume @p147 (forall (@list @t336 @t359 @t116 @t113) (=> (_ @t337 (_ (_ @t359 @t116) @t113)) (_ @t337 (_ @t360 @t118)))))
% 0.34/0.53  (assume @p148 (forall (@list @t336 @t362 @t98 @t95) (=> (_ @t337 (_ (_ @t362 @t98) @t95)) (_ @t337 (_ @t363 @t100)))))
% 0.34/0.53  (assume @p149 (forall (@list @t352 @t366 @t80 @t77) (=> (_ @t353 (_ (_ @t366 @t80) @t77)) (_ @t353 (_ @t367 @t82)))))
% 0.34/0.53  (assume @p150 (forall (@list @t171 @t369) (=> (forall @t141 (=> @t343 (_ (_ @t369 @t139) @t130))) @t370)))
% 0.34/0.53  (assume @p151 (forall (@list @t172 @t371) (=> (forall @t147 (=> @t339 (_ (_ @t371 @t145) @t122))) @t372)))
% 0.34/0.53  (assume @p152 (forall (@list @t173 @t373) (=> (forall @t154 (=> @t365 (_ (_ @t373 @t152) @t151))) @t374)))
% 0.34/0.53  (assume @p153 (forall (@list @t174 @t375) (=> (forall @t160 (=> @t358 (_ (_ @t375 @t123) @t158))) @t376)))
% 0.34/0.53  (assume @p154 (forall (@list @t175 @t377) (=> (forall @t166 (=> @t333 (_ (_ @t377 @t131) @t164))) @t378)))
% 0.34/0.53  (assume @p155 (forall @t382 (=> @t381 @t380)))
% 0.34/0.53  (assume @p156 (forall @t386 (=> @t385 @t384)))
% 0.34/0.53  (assume @p157 (forall @t391 (=> @t390 @t389)))
% 0.34/0.53  (assume @p158 (forall @t395 (=> @t394 @t393)))
% 0.34/0.53  (assume @p159 (forall @t400 (=> @t399 @t398)))
% 0.34/0.53  (assume @p160 (forall (@list @t401 @t116 @t113) (= (_ @t403 @t118) @t402)))
% 0.34/0.53  (assume @p161 (forall @t400 (= @t398 @t399)))
% 0.34/0.53  (assume @p162 (forall (@list @t404 @t116 @t113) (= (_ @t405 @t118) (_ (_ @t404 @t116) @t113))))
% 0.34/0.53  (assume @p163 (forall (@list @t406 @t89 @t86) (= (_ @t408 @t91) @t407)))
% 0.34/0.53  (assume @p164 (forall (@list @t409 @t98 @t95) (= (_ @t410 @t100) (_ (_ @t409 @t98) @t95))))
% 0.34/0.53  (assume @p165 (forall (@list @t401) (= (_ tptp.produc753314315real_c @t403) @t401)))
% 0.34/0.53  (assume @p166 (forall (@list @t396) (= (_ tptp.produc1086673900c_sz_o @t397) @t396)))
% 0.34/0.53  (assume @p167 (forall (@list @t404) (= (_ tptp.produc1827049067real_c @t405) @t404)))
% 0.34/0.53  (assume @p168 (forall (@list @t406) (= (_ tptp.produc1119115220real_c @t408) @t406)))
% 0.34/0.53  (assume @p169 (forall (@list @t409) (= (_ tptp.produc295339066_sc_sz @t410) @t409)))
% 0.34/0.53  (assume @p170 (forall @t412 (= (_ tptp.produc1575513068real_c (_ tptp.produc753314315real_c @t411)) @t411)))
% 0.34/0.53  (assume @p171 (forall @t413 (= (_ tptp.produc619560141c_sz_o @t288) @t287)))
% 0.34/0.53  (assume @p172 (forall @t415 (= (_ tptp.produc237521996real_c (_ tptp.produc1827049067real_c @t414)) @t414)))
% 0.34/0.53  (assume @p173 (forall @t416 (= (_ tptp.produc107375667real_c (_ tptp.produc1119115220real_c @t326)) @t326)))
% 0.34/0.53  (assume @p174 (forall @t418 (= (_ tptp.produc435149849_sc_sz (_ tptp.produc295339066_sc_sz @t417)) @t417)))
% 0.34/0.53  (assume @p175 (forall (@list @t401 @t175) (= (_ (_ tptp.produc645763722real_c (lambda @t421 (_ (_ @t401 @t420) @t419))) @t319) (_ @t403 @t175))))
% 0.34/0.53  (assume @p176 (forall (@list @t396 @t175) (= (_ (_ tptp.produc1718498667unit_o (lambda @t421 (_ (_ @t396 @t420) @t419))) @t319) (_ @t397 @t175))))
% 0.34/0.53  (assume @p177 (forall (@list @t404 @t175) (= (_ (_ tptp.produc593754858real_c (lambda @t421 (_ (_ @t404 @t420) @t419))) @t319) (_ @t405 @t175))))
% 0.34/0.53  (assume @p178 (forall (@list @t409 @t173) (= (_ (_ tptp.produc448466487_sc_sz (lambda @t423 (_ (_ @t409 @t224) @t422))) @t318) (_ @t410 @t173))))
% 0.34/0.53  (assume @p179 (forall (@list @t424 @t173) (= (_ (_ tptp.produc1575513068real_c (lambda @t423 (_ (_ @t424 @t224) @t422))) @t318) (_ (_ tptp.produc645763722real_c @t424) @t173))))
% 0.34/0.53  (assume @p180 (forall (@list @t387 @t173) (= (_ (_ tptp.produc619560141c_sz_o (lambda @t423 (_ (_ @t387 @t224) @t422))) @t318) (_ @t388 @t173))))
% 0.34/0.53  (assume @p181 (forall (@list @t425 @t173) (= (_ (_ tptp.produc237521996real_c (lambda @t423 (_ (_ @t425 @t224) @t422))) @t318) (_ (_ tptp.produc593754858real_c @t425) @t173))))
% 0.34/0.53  (assume @p182 (forall (@list @t406 @t172) (= (_ (_ tptp.produc107375667real_c (lambda (@list @t426 @t212) (_ (_ @t406 @t212) @t426))) @t320) (_ @t408 @t172))))
% 0.34/0.53  (assume @p183 (forall (@list @t427 @t175) (= (_ (_ tptp.produc435149849_sc_sz (lambda @t421 (_ (_ @t427 @t420) @t419))) @t319) (_ (_ tptp.produc448466487_sc_sz @t427) @t175))))
% 0.34/0.53  (assume @p184 (forall (@list @t89 @t86 @t225 @t406) (=> @t429 (_ (_ tptp.member1895684704real_c @t407) (_ (_ tptp.image_738229701real_c @t408) @t225)))))
% 0.34/0.53  (assume @p185 (forall (@list @t116 @t113 @t213 @t401) (=> @t431 (_ (_ tptp.member1895684704real_c @t402) (_ (_ tptp.image_386905412real_c @t403) @t213)))))
% 0.34/0.53  (assume @p186 (forall (@list @t89 @t86 @t225 @t432) (=> @t429 (_ (_ tptp.member1261661570real_c (_ (_ @t432 @t89) @t86)) (_ (_ tptp.image_14429021real_c (_ tptp.produc567249007real_c @t432)) @t225)))))
% 0.34/0.53  (assume @p187 (forall (@list @t80 @t77 @t223 @t433) (=> @t434 (_ (_ tptp.member1261661570real_c (_ (_ @t433 @t80) @t77)) (_ (_ tptp.image_1332486093real_c (_ tptp.produc236226839real_c @t433)) @t223)))))
% 0.34/0.53  (assume @p188 (forall (@list @t80 @t77 @t223 @t435) (=> @t434 (_ (_ tptp.member1895684704real_c (_ (_ @t435 @t80) @t77)) (_ (_ tptp.image_1121381717real_c (_ tptp.produc126255499real_c @t435)) @t223)))))
% 0.34/0.53  (assume @p189 (forall (@list @t89 @t86 @t225 @t436) (=> @t429 (_ (_ tptp.member245028432_sc_sz (_ (_ @t436 @t89) @t86)) (_ (_ tptp.image_388766773_sc_sz (_ tptp.produc1341776291_sc_sz @t436)) @t225)))))
% 0.34/0.53  (assume @p190 (forall (@list @t107 @t104 @t217 @t437) (=> (_ @t438 @t217) (_ (_ tptp.member1261661570real_c (_ (_ @t437 @t107) @t104)) (_ (_ tptp.image_124598413real_c (_ tptp.produc344593239real_c @t437)) @t217)))))
% 0.34/0.53  (assume @p191 (forall (@list @t116 @t113 @t213 @t396) (=> @t431 (_ (_ tptp.member_o @t399) (_ (_ tptp.image_1641704997c_sz_o @t397) @t213)))))
% 0.34/0.53  (assume @p192 (forall (@list @t116 @t113 @t213 @t439) (=> @t431 (_ (_ tptp.member1261661570real_c (_ (_ @t439 @t116) @t113)) (_ (_ tptp.image_1268968350real_c (_ tptp.produc1920474870real_c @t439)) @t213)))))
% 0.34/0.53  (assume @p193 (forall (@list @t98 @t95 @t219 @t440) (=> (_ (_ tptp.member235934813t_unit @t100) @t219) (_ (_ tptp.member1261661570real_c (_ (_ @t440 @t98) @t95)) (_ (_ tptp.image_1269062456real_c (_ tptp.produc1753599960real_c @t440)) @t219)))))
% 0.34/0.53  (assume @p194 (= tptp.produc1086673900c_sz_o (lambda (@list @t442 @t420 @t419) (_ @t442 @t441))))
% 0.34/0.53  (assume @p195 (forall (@list @t443) (= (_ tptp.produc1086673900c_sz_o (lambda @t216 @t443)) (lambda @t444 @t443))))
% 0.34/0.53  (assume @p196 (forall (@list @t401 @t74 @t72) (= (_ @t403 @t75) (_ (_ @t401 @t74) @t72))))
% 0.34/0.53  (assume @p197 (forall (@list @t396 @t74 @t72) (= (_ @t397 @t75) (_ (_ @t396 @t74) @t72))))
% 0.34/0.53  (assume @p198 (forall (@list @t404 @t74 @t72) (= (_ @t405 @t75) (_ (_ @t404 @t74) @t72))))
% 0.34/0.53  (assume @p199 (forall (@list @t406 @t60 @t58) (= (_ @t408 @t61) (_ (_ @t406 @t60) @t58))))
% 0.34/0.53  (assume @p200 (forall (@list @t409 @t65 @t63) (= (_ @t410 @t66) (_ (_ @t409 @t65) @t63))))
% 0.34/0.53  (assume @p201 (forall (@list @t330 @t328 @t175) (=> @t332 (not (forall @t201 (=> @t200 (not (_ @t331 (_ (_ @t328 @t198) @t197)))))))))
% 0.34/0.53  (assume @p202 (forall (@list @t336 @t334 @t172) (=> @t338 (not (forall @t184 (=> @t183 (not (_ @t337 (_ (_ @t334 @t181) @t180)))))))))
% 0.34/0.53  (assume @p203 (forall (@list @t336 @t340 @t171) (=> @t342 (not (forall @t179 (=> @t178 (not (_ @t337 (_ (_ @t340 @t177) @t176)))))))))
% 0.34/0.53  (assume @p204 (forall (@list @t330 @t344 @t172) (=> @t346 (not (forall @t184 (=> @t183 (not (_ @t331 (_ (_ @t344 @t181) @t180)))))))))
% 0.34/0.53  (assume @p205 (forall (@list @t330 @t347 @t171) (=> @t349 (not (forall @t179 (=> @t178 (not (_ @t331 (_ (_ @t347 @t177) @t176)))))))))
% 0.34/0.53  (assume @p206 (forall (@list @t352 @t350 @t172) (=> @t354 (not (forall @t184 (=> @t183 (not (_ @t353 (_ (_ @t350 @t181) @t180)))))))))
% 0.34/0.53  (assume @p207 (forall (@list @t336 @t355 @t174) (=> @t357 (not (forall @t196 (=> @t195 (not (_ @t337 (_ (_ @t355 @t193) @t192)))))))))
% 0.34/0.53  (assume @p208 (forall (@list @t336 @t359 @t175) (=> @t361 (not (forall @t201 (=> @t200 (not (_ @t337 (_ (_ @t359 @t198) @t197)))))))))
% 0.34/0.53  (assume @p209 (forall (@list @t336 @t362 @t173) (=> @t364 (not (forall @t190 (=> @t189 (not (_ @t337 (_ (_ @t362 @t187) @t186)))))))))
% 0.34/0.53  (assume @p210 (forall (@list @t352 @t366 @t171) (=> @t368 (not (forall @t179 (=> @t178 (not (_ @t353 (_ (_ @t366 @t177) @t176)))))))))
% 0.34/0.53  (assume @p211 (forall (@list @t448 @t396 @t162) (= (_ @t448 @t450) (_ (_ tptp.produc619560141c_sz_o (lambda @t449 (_ @t448 @t447))) @t162))))
% 0.34/0.53  (assume @p212 (forall (@list @t453 @t406 @t143) (= (_ @t453 (_ @t408 @t143)) (_ (_ tptp.produc107375667real_c (lambda (@list @t452 @t451) (_ @t453 (_ (_ @t406 @t452) @t451)))) @t143))))
% 0.34/0.53  (assume @p213 (forall (@list @t455 @t401 @t162) (= (_ @t455 @t456) (_ (_ tptp.produc619560141c_sz_o (lambda @t449 (_ @t455 @t454))) @t162))))
% 0.34/0.53  (assume @p214 (forall (@list @t457 @t396 @t162) (= (_ @t457 @t450) (_ (_ tptp.produc1575513068real_c (lambda @t449 (_ @t457 @t447))) @t162))))
% 0.34/0.53  (assume @p215 (forall (@list @t458 @t396 @t162) (= (_ @t458 @t450) (_ (_ tptp.produc237521996real_c (lambda @t449 (_ @t458 @t447))) @t162))))
% 0.34/0.53  (assume @p216 (forall (@list @t460 @t404 @t162) (= (_ @t460 @t461) (_ (_ tptp.produc619560141c_sz_o (lambda @t449 (_ @t460 @t459))) @t162))))
% 0.34/0.53  (assume @p217 (forall (@list @t453 @t401 @t162) (= (_ @t453 @t456) (_ (_ tptp.produc1575513068real_c (lambda @t449 (_ @t453 @t454))) @t162))))
% 0.34/0.53  (assume @p218 (forall (@list @t462 @t401 @t162) (= (_ @t462 @t456) (_ (_ tptp.produc237521996real_c (lambda @t449 (_ @t462 @t454))) @t162))))
% 0.34/0.53  (assume @p219 (forall (@list @t463 @t404 @t162) (= (_ @t463 @t461) (_ (_ tptp.produc1575513068real_c (lambda @t449 (_ @t463 @t459))) @t162))))
% 0.34/0.53  (assume @p220 (forall (@list @t464 @t404 @t162) (= (_ @t464 @t461) (_ (_ tptp.produc237521996real_c (lambda @t449 (_ @t464 @t459))) @t162))))
% 0.34/0.53  (assume @p221 (forall (@list @t401 @t465) (=> (forall @t201 (= (_ (_ @t401 @t198) @t197) (_ @t465 @t199))) (= @t403 @t465))))
% 0.34/0.53  (assume @p222 (forall (@list @t396 @t466) (=> (forall @t201 (= (_ (_ @t396 @t198) @t197) (_ @t466 @t199))) (= @t397 @t466))))
% 0.34/0.53  (assume @p223 (forall (@list @t404 @t467) (=> (forall @t201 (= (_ (_ @t404 @t198) @t197) (_ @t467 @t199))) (= @t405 @t467))))
% 0.34/0.53  (assume @p224 (forall (@list @t406 @t468) (=> (forall @t184 (= (_ (_ @t406 @t181) @t180) (_ @t468 @t182))) (= @t408 @t468))))
% 0.34/0.53  (assume @p225 (forall (@list @t409 @t469) (=> (forall @t190 (= (_ (_ @t409 @t187) @t186) (_ @t469 @t188))) (= @t410 @t469))))
% 0.34/0.53  (assume @p226 (forall @t412 (= (_ tptp.produc1575513068real_c (lambda @t444 (_ @t411 @t441))) @t411)))
% 0.34/0.53  (assume @p227 (forall @t413 (= (_ tptp.produc619560141c_sz_o (lambda @t444 (_ @t287 @t441))) @t287)))
% 0.34/0.53  (assume @p228 (forall @t415 (= (_ tptp.produc237521996real_c (lambda @t444 (_ @t414 @t441))) @t414)))
% 0.34/0.53  (assume @p229 (forall @t416 (= (_ tptp.produc107375667real_c (lambda @t471 (_ @t326 @t470))) @t326)))
% 0.34/0.53  (assume @p230 (forall @t418 (= (_ tptp.produc435149849_sc_sz (lambda (@list @t224 @t422) (_ @t417 (_ (_ tptp.produc502616768t_unit @t224) @t422)))) @t417)))
% 0.34/0.53  (assume @p231 (forall (@list @t230 @t472 @t473) (=> (_ @t230 (_ (_ tptp.produc1575513068real_c @t472) @t473)) (not (forall @t201 (=> @t474 (not (_ @t230 (_ (_ @t472 @t198) @t197)))))))))
% 0.34/0.53  (assume @p232 (forall (@list @t475 @t50 @t473) (=> (_ @t475 (_ (_ tptp.produc619560141c_sz_o @t50) @t473)) (not (forall @t201 (=> @t474 (not (_ @t475 (_ (_ @t50 @t198) @t197)))))))))
% 0.34/0.53  (assume @p233 (forall (@list @t477 @t476 @t473) (=> (_ @t477 (_ (_ tptp.produc237521996real_c @t476) @t473)) (not (forall @t201 (=> @t474 (not (_ @t477 (_ (_ @t476 @t198) @t197)))))))))
% 0.34/0.53  (assume @p234 (forall (@list @t230 @t478 @t330) (=> (_ @t230 (_ (_ tptp.produc107375667real_c @t478) @t330)) (not (forall @t184 (=> (= @t330 @t182) (not (_ @t230 (_ (_ @t478 @t181) @t180)))))))))
% 0.34/0.53  (assume @p235 (forall (@list @t480 @t479 @t481) (=> (_ @t480 (_ (_ tptp.produc435149849_sc_sz @t479) @t481)) (not (forall @t190 (=> (= @t481 @t188) (not (_ @t480 (_ (_ @t479 @t187) @t186)))))))))
% 0.34/0.53  (assume @p236 (forall (@list @t369 @t171) (=> @t370 (not (forall @t179 (=> @t178 (not (_ (_ @t369 @t177) @t176))))))))
% 0.34/0.53  (assume @p237 (forall (@list @t371 @t172) (=> @t372 (not (forall @t184 (=> @t183 (not (_ (_ @t371 @t181) @t180))))))))
% 0.34/0.53  (assume @p238 (forall (@list @t373 @t173) (=> @t374 (not (forall @t190 (=> @t189 (not (_ (_ @t373 @t187) @t186))))))))
% 0.34/0.53  (assume @p239 (forall (@list @t375 @t174) (=> @t376 (not (forall @t196 (=> @t195 (not (_ (_ @t375 @t193) @t192))))))))
% 0.34/0.53  (assume @p240 (forall (@list @t377 @t175) (=> @t378 (not (forall @t201 (=> @t200 (not (_ (_ @t377 @t198) @t197))))))))
% 0.34/0.53  (assume @p241 (forall @t382 (=> @t380 @t381)))
% 0.34/0.53  (assume @p242 (forall @t386 (=> @t384 @t385)))
% 0.34/0.53  (assume @p243 (forall @t391 (=> @t389 @t390)))
% 0.34/0.53  (assume @p244 (forall @t395 (=> @t393 @t394)))
% 0.34/0.53  (assume @p245 (forall @t400 (=> @t398 @t399)))
% 0.34/0.53  (assume @p246 (forall (@list @t482) (= (_ (_ tptp.image_738229701real_c (lambda @t229 @t226)) @t482) @t482)))
% 0.34/0.53  (assume @p247 (forall (@list @t104 @t326 @t297 @t225) (=> @t490 (=> @t488 @t486))))
% 0.34/0.53  (assume @p248 (forall (@list @t86 @t323 @t301 @t211) (=> @t495 (=> @t493 @t492))))
% 0.34/0.53  (assume @p249 (forall (@list @t86 @t496 @t297 @t225) (=> @t498 (=> @t488 @t497))))
% 0.34/0.53  (assume @p250 (forall (@list @t104 @t499 @t301 @t211) (=> @t501 (=> @t493 @t500))))
% 0.34/0.53  (assume @p251 (forall (@list @t113 @t502 @t301 @t211) (=> @t505 (=> @t493 @t504))))
% 0.34/0.53  (assume @p252 (forall (@list @t86 @t506 @t306 @t223) (=> @t511 (=> @t509 @t508))))
% 0.34/0.53  (assume @p253 (forall (@list @t113 @t512 @t297 @t225) (=> @t514 (=> @t488 @t513))))
% 0.34/0.53  (assume @p254 (forall (@list @t516 @t515 @t301 @t211) (=> @t518 (=> @t493 @t517))))
% 0.34/0.53  (assume @p255 (forall (@list @t86 @t519 @t203 @t217) (=> @t522 (=> @t521 @t520))))
% 0.34/0.53  (assume @p256 (forall (@list @t104 @t523 @t306 @t223) (=> @t527 (=> @t509 @t525))))
% 0.34/0.53  (assume @p257 (forall (@list @t530 @t529) (= (_ tptp.produc619560141c_sz_o (lambda (@list @t532 @t531) (and @t530 (_ (_ @t529 @t532) @t531)))) (lambda (@list @t528) (and @t530 (_ (_ tptp.produc619560141c_sz_o @t529) @t528))))))
% 0.34/0.53  (assume @p258 (forall (@list @t162) (_ (_ tptp.produc619560141c_sz_o (lambda (@list @t533 (@var "Uv" tptp.produc866628903_sc_sz)) true)) @t162)))
% 0.34/0.53  (assume @p259 (forall (@list @t297 @t225 @t104 @t326) (=> @t488 (=> @t490 @t486))))
% 0.34/0.53  (assume @p260 (forall (@list @t301 @t211 @t86 @t323) (=> @t493 (=> @t495 @t492))))
% 0.34/0.53  (assume @p261 (forall (@list @t297 @t225 @t86 @t496) (=> @t488 (=> @t498 @t497))))
% 0.34/0.53  (assume @p262 (forall (@list @t301 @t211 @t104 @t499) (=> @t493 (=> @t501 @t500))))
% 0.34/0.53  (assume @p263 (forall (@list @t301 @t211 @t113 @t502) (=> @t493 (=> @t505 @t504))))
% 0.34/0.53  (assume @p264 (forall (@list @t306 @t223 @t86 @t506) (=> @t509 (=> @t511 @t508))))
% 0.34/0.53  (assume @p265 (forall (@list @t297 @t225 @t113 @t512) (=> @t488 (=> @t514 @t513))))
% 0.34/0.53  (assume @p266 (forall (@list @t301 @t211 @t516 @t515) (=> @t493 (=> @t518 @t517))))
% 0.34/0.53  (assume @p267 (forall (@list @t203 @t217 @t86 @t519) (=> @t521 (=> @t522 @t520))))
% 0.34/0.53  (assume @p268 (forall (@list @t306 @t223 @t104 @t523) (=> @t509 (=> @t527 @t525))))
% 0.34/0.53  (assume @p269 (forall @t541 (=> (forall @t232 (=> (_ @t540 @t539) @t231)) (forall @t537 (=> @t536 (_ @t144 (_ @t411 @t534)))))))
% 0.34/0.53  (assume @p270 (forall @t548 (=> (forall @t547 (=> (_ @t546 @t545) (_ @t150 @t543))) (forall @t537 (=> @t536 (_ @t150 (_ @t542 @t534)))))))
% 0.34/0.53  (assume @p271 (forall @t560 (=> (forall @t559 (=> (_ @t558 @t557) @t555)) (forall @t553 (=> @t552 (_ @t163 (_ @t550 @t549)))))))
% 0.34/0.53  (assume @p272 (forall @t561 (=> (forall @t232 (=> (_ @t540 @t484) @t231)) (forall @t553 (=> @t552 (_ @t144 (_ @t326 @t549)))))))
% 0.34/0.53  (assume @p273 (forall @t567 (=> (forall @t559 (=> (_ @t558 @t566) @t555)) (forall @t564 (=> (_ @t563 @t219) (_ @t163 (_ @t417 @t562)))))))
% 0.34/0.53  (assume @p274 (forall (@list @t570 @t568 @t550 @t569) (=> @t573 (=> (forall @t232 (=> @t572 (= @t571 (_ @t569 @t193)))) (= (_ @t556 @t570) (_ (_ tptp.image_1259833374_sc_sz @t569) @t568))))))
% 0.34/0.53  (assume @p275 (forall (@list @t570 @t568 @t326 @t468) (=> @t573 (=> (forall @t232 (=> @t572 (= @t574 (_ @t468 @t193)))) (= (_ @t483 @t570) (_ (_ tptp.image_738229701real_c @t468) @t568))))))
% 0.34/0.53  (assume @p276 (forall (@list @t576 @t575 @t411 @t465) (=> @t579 (=> (forall @t559 (=> @t578 (= @t577 (_ @t465 @t554)))) (= (_ @t538 @t576) (_ (_ tptp.image_386905412real_c @t465) @t575))))))
% 0.34/0.53  (assume @p277 (forall (@list @t576 @t575 @t542 @t580) (=> @t579 (=> (forall @t559 (=> @t578 (= @t581 (_ @t580 @t554)))) (= (_ @t544 @t576) (_ (_ tptp.image_904562809t_unit @t580) @t575))))))
% 0.34/0.53  (assume @p278 (forall (@list @t583 @t582 @t417 @t469) (=> (= @t583 @t582) (=> (forall @t547 (=> (_ @t546 @t582) (= @t584 (_ @t469 @t543)))) (= (_ @t565 @t583) (_ (_ tptp.image_1426741113_sc_sz @t469) @t582))))))
% 0.34/0.53  (assume @p279 (forall @t541 (=> (exists @t553 (and (_ @t551 @t539) @t586)) (exists @t559 (and @t585 (_ @t144 @t577))))))
% 0.34/0.53  (assume @p280 (forall @t548 (=> (exists @t564 (and (_ @t563 @t545) (_ @t150 @t562))) (exists @t559 (and @t585 (_ @t150 @t581))))))
% 0.34/0.53  (assume @p281 (forall @t560 (=> (exists @t537 (and (_ @t535 @t557) @t588)) (exists @t232 (and @t587 (_ @t163 @t571))))))
% 0.34/0.53  (assume @p282 (forall @t561 (=> (exists @t553 (and (_ @t551 @t484) @t586)) (exists @t232 (and @t587 (_ @t144 @t574))))))
% 0.34/0.53  (assume @p283 (forall @t567 (=> (exists @t537 (and (_ @t535 @t566) @t588)) (exists @t547 (and (_ @t546 @t219) (_ @t163 @t584))))))
% 0.34/0.53  (assume @p284 (forall (@list @t330 @t411 @t213) (= (_ @t331 @t539) (exists @t216 (and @t215 (= @t330 (_ @t411 @t214)))))))
% 0.34/0.53  (assume @p285 (forall (@list @t330 @t326 @t225) (= (_ @t331 @t484) (exists @t229 (and @t228 (= @t330 @t589))))))
% 0.34/0.53  (assume @p286 (forall (@list @t473 @t550 @t225) (= (_ @t590 @t557) (exists @t229 (and @t228 (= @t473 (_ @t550 @t226)))))))
% 0.34/0.53  (assume @p287 (forall (@list @t473 @t417 @t219) (= (_ @t590 @t566) (exists @t222 (and @t221 (= @t473 (_ @t417 @t220)))))))
% 0.34/0.53  (assume @p288 (forall (@list @t481 @t542 @t213) (= (_ (_ tptp.member235934813t_unit @t481) @t545) (exists @t216 (and @t215 (= @t481 (_ @t542 @t214)))))))
% 0.34/0.53  (assume @p289 (forall (@list @t306 @t223 @t523) (=> @t509 (_ (_ tptp.member1895684704real_c @t526) @t524))))
% 0.34/0.53  (assume @p290 (forall (@list @t306 @t223 @t506) (=> @t509 (_ (_ tptp.member1261661570real_c @t510) @t507))))
% 0.34/0.53  (assume @p291 (forall (@list @t306 @t223 @t591) (=> @t509 (_ (_ tptp.member1057565379_sc_sz (_ @t591 @t306)) (_ (_ tptp.image_226055310_sc_sz @t591) @t223)))))
% 0.34/0.53  (assume @p292 (forall (@list @t306 @t223 @t592) (=> @t509 (_ (_ tptp.member346808080real_c (_ @t592 @t306)) (_ (_ tptp.image_768765061real_c @t592) @t223)))))
% 0.34/0.53  (assume @p293 (forall (@list @t306 @t223 @t593) (=> @t509 (_ (_ tptp.member235934813t_unit (_ @t593 @t306)) (_ (_ tptp.image_1551908392t_unit @t593) @t223)))))
% 0.34/0.53  (assume @p294 (forall (@list @t306 @t223 @t327) (=> @t509 (_ (_ tptp.member245028432_sc_sz (_ @t327 @t306)) (_ (_ tptp.image_1313166277_sc_sz @t327) @t223)))))
% 0.34/0.53  (assume @p295 (forall (@list @t297 @t225 @t326) (=> @t488 (_ (_ tptp.member1895684704real_c @t489) @t484))))
% 0.34/0.53  (assume @p296 (forall @t561 (= (_ tptp.collec1643251106real_c (lambda @t229 (and (_ @t227 @t484) (_ @t144 @t226)))) (_ @t483 (_ tptp.collec1643251106real_c (lambda @t229 (and @t228 (_ @t144 @t589))))))))
% 0.34/0.53  (assume @p297 (forall (@list @t104 @t326 @t225) (=> @t486 (not (forall @t232 (=> (= @t104 @t574) (not @t587)))))))
% 0.34/0.53  (assume @p298 (forall @t202 (= (_ (_ tptp.produc448466487_sc_sz tptp.produc789536734_sc_sz) @t175) @t175)))
% 0.34/0.53  (assume @p299 (forall (@list @t261 @t594) (= (= (lambda @t471 (_ @t595 @t261)) (lambda @t471 (_ @t595 @t594))) (= @t261 @t594))))
% 0.34/0.53  (assume @p300 (forall (@list @t266 @t596) (= (= (lambda @t444 (_ @t597 @t266)) (lambda @t444 (_ @t597 @t596))) (= @t266 @t596))))
% 0.34/0.53  (assume @p301 (forall @t603 (= @t602 (and @t600 @t599))))
% 0.34/0.53  (assume @p302 (forall @t610 (= @t609 (and @t606 @t605))))
% 0.34/0.53  (assume @p303 (forall @t617 (= @t616 (and @t614 @t612))))
% 0.34/0.53  (assume @p304 (forall (@list @t89 @t211 @t86 @t604) (=> @t606 (=> @t605 @t609))))
% 0.34/0.53  (assume @p305 (forall (@list @t107 @t225 @t104 @t598) (=> @t600 (=> @t599 @t602))))
% 0.34/0.53  (assume @p306 (forall (@list @t116 @t613 @t113 @t611) (=> @t614 (=> @t612 @t616))))
% 0.34/0.53  (assume @p307 (forall @t603 (=> @t602 (not (=> @t600 (not @t599))))))
% 0.34/0.53  (assume @p308 (forall @t610 (=> @t609 (not (=> @t606 (not @t605))))))
% 0.34/0.53  (assume @p309 (forall @t617 (=> @t616 (not (=> @t614 (not @t612))))))
% 0.34/0.53  (assume @p310 (forall @t610 (=> @t609 @t605)))
% 0.34/0.53  (assume @p311 (forall @t617 (=> @t616 @t612)))
% 0.34/0.53  (assume @p312 (forall @t610 (=> @t609 @t606)))
% 0.34/0.53  (assume @p313 (forall @t617 (=> @t616 @t614)))
% 0.34/0.53  (assume @p314 (forall (@list @t618 @t225 @t598) (=> (_ (_ tptp.member346808080real_c @t618) @t601) (not (forall @t232 (=> @t587 (forall (@list @t192) (=> (_ (_ tptp.member1895684704real_c @t192) (_ @t598 @t193)) (not (= @t618 @t194))))))))))
% 0.34/0.53  (assume @p315 (forall (@list @t619 @t211 @t604) (=> (_ @t620 @t608) (not (forall (@list @t181) (=> (_ (_ tptp.member1261661570real_c @t181) @t211) (forall (@list @t180) (=> (_ (_ tptp.member1261661570real_c @t180) (_ @t604 @t181)) (not (= @t619 @t182))))))))))
% 0.34/0.53  (assume @p316 (forall (@list @t621 @t613 @t611) (=> (_ @t622 @t615) (not (forall (@list @t198) (=> (_ (_ tptp.member754147591t_unit @t198) @t613) (forall (@list @t197) (=> (_ (_ tptp.member245028432_sc_sz @t197) (_ @t611 @t198)) (not (= @t621 @t199))))))))))
% 0.34/0.53  (assume @p317 (forall (@list @t223 @t623) (= (_ (_ tptp.image_1426741113_sc_sz (_ tptp.produc435149849_sc_sz (lambda (@list @t624 @t625) (_ (_ tptp.produc789536734_sc_sz @t625) @t624)))) (_ (_ tptp.produc2020166735t_unit @t223) (lambda (@list (@var "Uu" tptp.produc866628903_sc_sz)) @t623))) (_ (_ tptp.produc159603053_sc_sz @t623) (lambda (@list @t533) @t223)))))
% 0.34/0.53  (assume @p318 (forall (@list @t297 @t211 @t626) (= (_ @t487 (_ (_ tptp.produc3751594real_c @t211) @t626)) (_ @t487 (_ @t607 (lambda (@list (@var "Uu" tptp.finite1398487019real_c)) @t626))))))
% 0.34/0.53  (assume @p319 (forall (@list @t325 @t627 @t116 @t113) (= (_ @t629 @t118) @t628)))
% 0.34/0.53  (assume @p320 (forall (@list @t301 @t302 @t630 @t323) (= (_ @t321 (_ (_ tptp.inv_im1827249322real_c @t630) @t323)) (_ (_ tptp.member1895684704real_c (_ (_ tptp.produc394644079real_c @t494) @t324)) @t630))))
% 0.34/0.53  (assume @p321 (forall (@list @t89 @t86 @t261 @t323 @t631) (=> @t633 (_ (_ tptp.member1895684704real_c (_ (_ tptp.produc394644079real_c (_ @t323 @t89)) (_ @t631 @t86))) @t632))))
% 0.34/0.53  (assume @p322 (forall (@list @t89 @t86 @t261 @t635 @t634) (=> @t633 (_ (_ tptp.member1057565379_sc_sz (_ (_ tptp.produc789536734_sc_sz (_ @t635 @t89)) (_ @t634 @t86))) @t636))))
% 0.34/0.53  (assume @p323 (forall (@list @t116 @t113 @t266 @t638 @t637) (=> @t640 (_ (_ tptp.member1895684704real_c (_ (_ tptp.produc394644079real_c (_ @t638 @t116)) (_ @t637 @t113))) @t639))))
% 0.34/0.53  (assume @p324 (forall (@list @t116 @t113 @t266 @t325 @t627) (=> @t640 (_ (_ tptp.member1057565379_sc_sz @t628) @t641))))
% 0.34/0.53  (assume @p325 (forall (@list @t619 @t323 @t631 @t261) (=> (_ @t620 @t632) (not (forall @t184 (=> (= @t619 (_ (_ tptp.produc394644079real_c (_ @t323 @t181)) (_ @t631 @t180))) @t642))))))
% 0.34/0.53  (assume @p326 (forall (@list @t619 @t638 @t637 @t266) (=> (_ @t620 @t639) (not (forall @t201 (=> (= @t619 (_ (_ tptp.produc394644079real_c (_ @t638 @t198)) (_ @t637 @t197))) @t643))))))
% 0.34/0.53  (assume @p327 (forall (@list @t621 @t635 @t634 @t261) (=> (_ @t622 @t636) (not (forall @t184 (=> (= @t621 (_ (_ tptp.produc789536734_sc_sz (_ @t635 @t181)) (_ @t634 @t180))) @t642))))))
% 0.34/0.53  (assume @p328 (forall (@list @t621 @t325 @t627 @t266) (=> (_ @t622 @t641) (not (forall @t201 (=> (= @t621 (_ (_ tptp.produc789536734_sc_sz (_ @t325 @t198)) (_ @t627 @t197))) @t643))))))
% 0.34/0.53  (assume @p329 (forall (@list @t89 @t86 @t645 @t644) (=> (_ (_ (_ tptp.denota1997846518gree_c @t91) (_ (_ tptp.produc394644079real_c @t645) @t644)) tptp.top_to1660572043um_c_c) (and (= @t89 @t645) (= @t86 @t644)))))
% 0.34/0.53  (assume @p330 (forall (@list @t33 @t646) (=> (_ (_ @t34 @t646) tptp.top_to1660572043um_c_c) (= @t33 @t646))))
% 0.34/0.53  (assume @p331 (forall (@list @t74 @t72) (= (_ tptp.produc1503602930_sc_sz @t75) @t74)))
% 0.34/0.53  (assume @p332 (forall (@list @t311 @t168 @t116) (=> (= (_ tptp.produc1503602930_sc_sz @t314) @t116) (= @t311 @t116))))
% 0.34/0.53  (assume @p333 @t648)
% 0.34/0.53  (assume @p334 true)
% 0.34/0.53  (step @p335 (= tptp.coinci501627771_a_b_c @t650) :rule refl :args (@t650))
% 0.34/0.53  (step @p336 (= tptp.ids_sz_sf_sc @t661) :rule refl :args (@t661))
% 0.34/0.53  (step @p337 (= tptp.produc1086673900c_sz_o @t663) :rule refl :args (@t663))
% 0.34/0.53  (step @p338 (= tptp.top_to964419200al_c_o @t664) :rule refl :args (@t664))
% 0.34/0.53  (step @p339 (= tptp.top_to1399053141c_sz_o @t665) :rule refl :args (@t665))
% 0.34/0.53  (step @p340 :rule evaluate :args ((not true)))
% 0.34/0.53  (step @p341 :rule eq-refl :args (@t647))
% 0.34/0.53  (step @p342 :rule cong :premises (@p341) :args (@t648))
% 0.34/0.53  (step @p343 :rule trans :premises (@p342 @p340))
% 0.34/0.53  (step @p344 false :rule eq_resolve :premises (@p333 @p343))
% 0.34/0.53  )
% 0.34/0.53  % SZS output end Proof
% 0.34/0.53  % cvc5 exiting
%------------------------------------------------------------------------------