↑ Up

nanoCoP---2.0.THM-Prf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : nanoCoP---2.0
% Problem  : ITP001+4 : TPTP v8.1.2. Bugfixed v7.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : nanocop.sh %s %d

% Computer : n008.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 : Fri May 19 11:23:03 EDT 2023

% Result   : Theorem 0.33s 1.37s
% Output   : Proof 0.33s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12  % Problem  : ITP001+4 : TPTP v8.1.2. Bugfixed v7.5.0.
% 0.11/0.12  % Command  : nanocop.sh %s %d
% 0.12/0.33  % Computer : n008.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33  % CPULimit : 300
% 0.12/0.33  % WCLimit  : 300
% 0.12/0.33  % DateTime : Thu May 18 21:39:24 EDT 2023
% 0.12/0.33  % CPUTime  : 
% 0.33/1.37  
% 0.33/1.37  /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.33/1.37  Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/1.37  %-----------------------------------------------------
% 0.33/1.37  ncf(matrix, plain, [(1164 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0))], (20 ^ _309628) ^ [_310376, _310378] : [-(p(_310376)), _310378 = _310376, p(_310378)], (2 ^ _309628) ^ [_309772] : [-(_309772 = _309772)], (4 ^ _309628) ^ [_309879, _309881] : [_309881 = _309879, -(_309879 = _309881)], (10 ^ _309628) ^ [_310083, _310085, _310087] : [-(_310087 = _310083), _310087 = _310085, _310085 = _310083], (30 ^ _309628) ^ [_310701, _310703, _310705, _310707] : [-(c_2Ebool_2E_2F_5C_2E2(_310707, _310703) = c_2Ebool_2E_2F_5C_2E2(_310705, _310701)), _310707 = _310705, _310703 = _310701], (40 ^ _309628) ^ [_311060, _311062, _311064, _311066] : [-(c_2Ebool_2E_5C_2F_2E2(_311066, _311062) = c_2Ebool_2E_5C_2F_2E2(_311064, _311060)), _311066 = _311064, _311062 = _311060], (50 ^ _309628) ^ [_311391, _311393] : [_311393 = _311391, -(c_2Ebool_2E_7E_2E1(_311393) = c_2Ebool_2E_7E_2E1(_311391))], (56 ^ _309628) ^ [_311637, _311639, _311641, _311643] : [-(c_2Emin_2E_3D_3D_3E_2E2(_311643, _311639) = c_2Emin_2E_3D_3D_3E_2E2(_311641, _311637)), _311643 = _311641, _311639 = _311637], (66 ^ _309628) ^ [_311996, _311998, _312000, _312002] : [-(c_2Emin_2E_3D_2E2(_312002, _311998) = c_2Emin_2E_3D_2E2(_312000, _311996)), _312002 = _312000, _311998 = _311996], (76 ^ _309628) ^ [_312327, _312329] : [_312329 = _312327, -(c_2Ebool_2E_21_2E1(_312329) = c_2Ebool_2E_21_2E1(_312327))], (82 ^ _309628) ^ [_312545, _312547] : [_312547 = _312545, -(c_2Ebool_2E_3F_21_2E1(_312547) = c_2Ebool_2E_3F_21_2E1(_312545))], (88 ^ _309628) ^ [_312763, _312765] : [_312765 = _312763, -(c_2Ebool_2E_3F_2E1(_312765) = c_2Ebool_2E_3F_2E1(_312763))], (94 ^ _309628) ^ [_313009, _313011, _313013, _313015] : [-(c_2Ebool_2ELET_2E2(_313015, _313011) = c_2Ebool_2ELET_2E2(_313013, _313009)), _313015 = _313013, _313011 = _313009], (104 ^ _309628) ^ [_313396, _313398, _313400, _313402, _313404, _313406] : [-(c_2Ebool_2ECOND_2E3(_313406, _313402, _313398) = c_2Ebool_2ECOND_2E3(_313404, _313400, _313396)), _313406 = _313404, _313402 = _313400, _313398 = _313396], (118 ^ _309628) ^ [_313856, _313858] : [_313858 = _313856, -(c_2Ebool_2EONE__ONE_2E1(_313858) = c_2Ebool_2EONE__ONE_2E1(_313856))], (124 ^ _309628) ^ [_314074, _314076] : [_314076 = _314074, -(c_2Ebool_2EONTO_2E1(_314076) = c_2Ebool_2EONTO_2E1(_314074))], (130 ^ _309628) ^ [_314320, _314322, _314324, _314326] : [-(c_2Ebool_2ETYPE__DEFINITION_2E2(_314326, _314322) = c_2Ebool_2ETYPE__DEFINITION_2E2(_314324, _314320)), _314326 = _314324, _314322 = _314320], (140 ^ _309628) ^ [_314679, _314681, _314683, _314685] : [-(c_2Ebool_2Eliteral__case_2E2(_314685, _314681) = c_2Ebool_2Eliteral__case_2E2(_314683, _314679)), _314685 = _314683, _314681 = _314679], (150 ^ _309628) ^ [_315038, _315040, _315042, _315044] : [-(c_2Ebool_2ERES__EXISTS__UNIQUE_2E2(_315044, _315040) = c_2Ebool_2ERES__EXISTS__UNIQUE_2E2(_315042, _315038)), _315044 = _315042, _315040 = _315038], (160 ^ _309628) ^ [_315397, _315399, _315401, _315403] : [-(c_2Ebool_2ERES__EXISTS_2E2(_315403, _315399) = c_2Ebool_2ERES__EXISTS_2E2(_315401, _315397)), _315403 = _315401, _315399 = _315397], (170 ^ _309628) ^ [_315756, _315758, _315760, _315762] : [-(c_2Ebool_2ERES__FORALL_2E2(_315762, _315758) = c_2Ebool_2ERES__FORALL_2E2(_315760, _315756)), _315762 = _315760, _315758 = _315756], (180 ^ _309628) ^ [_316115, _316117, _316119, _316121] : [-(c_2Ebool_2EIN_2E2(_316121, _316117) = c_2Ebool_2EIN_2E2(_316119, _316115)), _316121 = _316119, _316117 = _316115], (190 ^ _309628) ^ [_316474, _316476, _316478, _316480] : [-(c_2Ebool_2ERES__SELECT_2E2(_316480, _316476) = c_2Ebool_2ERES__SELECT_2E2(_316478, _316474)), _316480 = _316478, _316476 = _316474], (200 ^ _309628) ^ [_316805, _316807] : [_316807 = _316805, -(c_2Emin_2E_40_2E1(_316807) = c_2Emin_2E_40_2E1(_316805))], (206 ^ _309628) ^ [_317051, _317053, _317055, _317057] : [-(app_2E2(_317057, _317053) = app_2E2(_317055, _317051)), _317057 = _317055, _317053 = _317051], (216 ^ _309628) ^ [_317410, _317412, _317414, _317416] : [-(tyop_2Emin_2Efun(_317416, _317412) = tyop_2Emin_2Efun(_317414, _317410)), _317416 = _317414, _317412 = _317410], (226 ^ _309628) ^ [_317741, _317743] : [_317743 = _317741, -(c_2Ebool_2EBOUNDED_2E1(_317743) = c_2Ebool_2EBOUNDED_2E1(_317741))], (232 ^ _309628) ^ [_317959, _317961] : [_317961 = _317959, -(c_2Ebool_2EDATATYPE_2E1(_317961) = c_2Ebool_2EDATATYPE_2E1(_317959))], (238 ^ _309628) ^ [_318185, _318187, _318189, _318191] : [-(s(_318191, _318187) = s(_318189, _318185)), _318191 = _318189, _318187 = _318185], (248 ^ _309628) ^ [_318664, _318666, _318668, _318670] : [s(_318668, app_2E2(s(tyop_2Emin_2Efun(_318670, _318668), _318666), s(_318670, 249 ^ [_318664, _318666, _318668, _318670]))) = s(_318668, app_2E2(s(tyop_2Emin_2Efun(_318670, _318668), _318664), s(_318670, 249 ^ [_318664, _318666, _318668, _318670]))), -(s(tyop_2Emin_2Efun(_318670, _318668), _318666) = s(tyop_2Emin_2Efun(_318670, _318668), _318664))], (255 ^ _309628) ^ [_319080, _319082] : [-(s(tyop_2Emin_2Ebool, _319082) = s(tyop_2Emin_2Ebool, _319080)), 258 ^ _309628 : [(259 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _319082)))], (261 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _319080))]], 262 ^ _309628 : [(263 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _319080)))], (265 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _319082))]]], (269 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)))], (271 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2EF_2E0))], (273 ^ _309628) ^ [_319641] : [-(s(tyop_2Emin_2Ebool, _319641) = s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)), -(s(tyop_2Emin_2Ebool, _319641) = s(tyop_2Emin_2Ebool, c_2Ebool_2EF_2E0))], (279 ^ _309628) ^ [_319843, _319845] : [-(s(_319845, app_2E2(s(tyop_2Emin_2Efun(_319845, _319845), combin_i_2E0), s(_319845, _319843))) = s(_319845, _319843))], (281 ^ _309628) ^ [_319983, _319985, _319987, _319989] : [-(s(_319989, app_2E2(s(tyop_2Emin_2Efun(_319987, _319989), app_2E2(s(tyop_2Emin_2Efun(_319989, tyop_2Emin_2Efun(_319987, _319989)), combin_k_2E0), s(_319989, _319985))), s(_319987, _319983))) = s(_319989, _319985))], (283 ^ _309628) ^ [_320170, _320172, _320174, _320176, _320178, _320180] : [-(s(_320176, app_2E2(s(tyop_2Emin_2Efun(_320180, _320176), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_320180, _320178), tyop_2Emin_2Efun(_320180, _320176)), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_320180, tyop_2Emin_2Efun(_320178, _320176)), tyop_2Emin_2Efun(tyop_2Emin_2Efun(_320180, _320178), tyop_2Emin_2Efun(_320180, _320176))), combin_s_2E0), s(tyop_2Emin_2Efun(_320180, tyop_2Emin_2Efun(_320178, _320176)), _320174))), s(tyop_2Emin_2Efun(_320180, _320178), _320172))), s(_320180, _320170))) = s(_320176, app_2E2(s(tyop_2Emin_2Efun(_320178, _320176), app_2E2(s(tyop_2Emin_2Efun(_320180, tyop_2Emin_2Efun(_320178, _320176)), _320174), s(_320180, _320170))), s(_320178, app_2E2(s(tyop_2Emin_2Efun(_320180, _320178), _320172), s(_320180, _320170))))))], (285 ^ _309628) ^ [_320427, _320429] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool, _320429), s(tyop_2Emin_2Ebool, _320427)))), 288 ^ _309628 : [(289 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _320429)))], (291 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _320427)))]]], (293 ^ _309628) ^ [_320694, _320696] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool, _320696), s(tyop_2Emin_2Ebool, _320694))))), p(s(tyop_2Emin_2Ebool, _320696)), p(s(tyop_2Emin_2Ebool, _320694))], (313 ^ _309628) ^ [_321336, _321338] : [314 ^ _309628 : [(315 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _321338))], (317 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _321336))]], -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool, _321338), s(tyop_2Emin_2Ebool, _321336)))))], (303 ^ _309628) ^ [_321054, _321056] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool, _321056), s(tyop_2Emin_2Ebool, _321054)))), -(p(s(tyop_2Emin_2Ebool, _321056))), -(p(s(tyop_2Emin_2Ebool, _321054)))], (321 ^ _309628) ^ [_321667] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool, _321667)))), p(s(tyop_2Emin_2Ebool, _321667))], (327 ^ _309628) ^ [_321842] : [-(p(s(tyop_2Emin_2Ebool, _321842))), -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool, _321842)))))], (343 ^ _309628) ^ [_322379, _322381] : [344 ^ _309628 : [(345 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _322381)))], (347 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _322379))]], -(p(s(tyop_2Emin_2Ebool, c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool, _322381), s(tyop_2Emin_2Ebool, _322379)))))], (333 ^ _309628) ^ [_322098, _322100] : [p(s(tyop_2Emin_2Ebool, c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool, _322100), s(tyop_2Emin_2Ebool, _322098)))), p(s(tyop_2Emin_2Ebool, _322100)), -(p(s(tyop_2Emin_2Ebool, _322098)))], (351 ^ _309628) ^ [_322739, _322741, _322743] : [p(s(tyop_2Emin_2Ebool, c_2Emin_2E_3D_2E2(s(_322743, _322741), s(_322743, _322739)))), -(s(_322743, _322741) = s(_322743, _322739))], (357 ^ _309628) ^ [_322941, _322943, _322945] : [s(_322945, _322943) = s(_322945, _322941), -(p(s(tyop_2Emin_2Ebool, c_2Emin_2E_3D_2E2(s(_322945, _322943), s(_322945, _322941)))))], (363 ^ _309628) ^ [_323222, _323224] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(_323224, tyop_2Emin_2Ebool), _323222)))), 366 ^ _309628 : [(367 ^ _309628) ^ [_323372] : [-(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_323224, tyop_2Emin_2Ebool), _323222), s(_323224, _323372)))))]]], (369 ^ _309628) ^ [_323454, _323456] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_323456, tyop_2Emin_2Ebool), _323454), s(_323456, 370 ^ [_323454, _323456])))), -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(_323456, tyop_2Emin_2Ebool), _323454)))))], (376 ^ _309628) ^ [_323814, _323816] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(_323816, tyop_2Emin_2Ebool), _323814)))), -(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_323816, tyop_2Emin_2Ebool), _323814), s(_323816, 379 ^ [_323814, _323816])))))], (383 ^ _309628) ^ [_324095, _324097] : [384 ^ _309628 : [(385 ^ _309628) ^ [_324189] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_324097, tyop_2Emin_2Ebool), _324095), s(_324097, _324189))))]], -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(_324097, tyop_2Emin_2Ebool), _324095)))))], (399 ^ _309628) ^ [_324699, _324701] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool)), c_2Ebool_2E_2F_5C_2E0), s(tyop_2Emin_2Ebool, _324701))), s(tyop_2Emin_2Ebool, _324699)))), 402 ^ _309628 : [(403 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _324701)))], (405 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _324699)))]]], (389 ^ _309628) ^ [_324406, _324408] : [-(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool)), c_2Ebool_2E_2F_5C_2E0), s(tyop_2Emin_2Ebool, _324408))), s(tyop_2Emin_2Ebool, _324406))))), p(s(tyop_2Emin_2Ebool, _324408)), p(s(tyop_2Emin_2Ebool, _324406))], (407 ^ _309628) ^ [_325057, _325059] : [408 ^ _309628 : [(409 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _325059))], (411 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _325057))]], -(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool)), c_2Ebool_2E_5C_2F_2E0), s(tyop_2Emin_2Ebool, _325059))), s(tyop_2Emin_2Ebool, _325057)))))], (415 ^ _309628) ^ [_325335, _325337] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool)), c_2Ebool_2E_5C_2F_2E0), s(tyop_2Emin_2Ebool, _325337))), s(tyop_2Emin_2Ebool, _325335)))), -(p(s(tyop_2Emin_2Ebool, _325337))), -(p(s(tyop_2Emin_2Ebool, _325335)))], (425 ^ _309628) ^ [_325694] : [-(p(s(tyop_2Emin_2Ebool, _325694))), -(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool), c_2Ebool_2E_7E_2E0), s(tyop_2Emin_2Ebool, _325694)))))], (431 ^ _309628) ^ [_325873] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool), c_2Ebool_2E_7E_2E0), s(tyop_2Emin_2Ebool, _325873)))), p(s(tyop_2Emin_2Ebool, _325873))], (467 ^ _309628) ^ [_327305, _327307] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(_327307, tyop_2Emin_2Ebool), _327305))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_327307, tyop_2Emin_2Ebool), tyop_2Emin_2Ebool), c_2Ebool_2E_21_2E0), s(tyop_2Emin_2Efun(_327307, tyop_2Emin_2Ebool), _327305))))], (469 ^ _309628) ^ [_327411, _327413] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(_327413, tyop_2Emin_2Ebool), _327411))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_327413, tyop_2Emin_2Ebool), tyop_2Emin_2Ebool), c_2Ebool_2E_3F_2E0), s(tyop_2Emin_2Efun(_327413, tyop_2Emin_2Ebool), _327411))))], (455 ^ _309628) ^ [_326794, _326796, _326798] : [s(_326798, _326796) = s(_326798, _326794), -(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_326798, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(_326798, tyop_2Emin_2Efun(_326798, tyop_2Emin_2Ebool)), c_2Emin_2E_3D_2E0), s(_326798, _326796))), s(_326798, _326794)))))], (461 ^ _309628) ^ [_327032, _327034, _327036] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_327036, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(_327036, tyop_2Emin_2Efun(_327036, tyop_2Emin_2Ebool)), c_2Emin_2E_3D_2E0), s(_327036, _327034))), s(_327036, _327032)))), -(s(_327036, _327034) = s(_327036, _327032))], (437 ^ _309628) ^ [_326129, _326131] : [438 ^ _309628 : [(439 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _326131)))], (441 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _326129))]], -(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool)), c_2Emin_2E_3D_3D_3E_2E0), s(tyop_2Emin_2Ebool, _326131))), s(tyop_2Emin_2Ebool, _326129)))))], (445 ^ _309628) ^ [_326408, _326410] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool)), c_2Emin_2E_3D_3D_3E_2E0), s(tyop_2Emin_2Ebool, _326410))), s(tyop_2Emin_2Ebool, _326408)))), p(s(tyop_2Emin_2Ebool, _326410)), -(p(s(tyop_2Emin_2Ebool, _326408)))], (471 ^ _309628) ^ [_327682, _327684, _327686, _327688] : [s(_327686, app_2E2(s(tyop_2Emin_2Efun(_327688, _327686), _327684), s(_327688, 472 ^ [_327682, _327684, _327686, _327688]))) = s(_327686, app_2E2(s(tyop_2Emin_2Efun(_327688, _327686), _327682), s(_327688, 472 ^ [_327682, _327684, _327686, _327688]))), -(s(tyop_2Emin_2Efun(_327688, _327686), _327684) = s(tyop_2Emin_2Efun(_327688, _327686), _327682))], (478 ^ _309628) ^ [_328098, _328100] : [-(s(tyop_2Emin_2Ebool, _328100) = s(tyop_2Emin_2Ebool, _328098)), 481 ^ _309628 : [(482 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _328100)))], (484 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _328098))]], 485 ^ _309628 : [(486 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _328098)))], (488 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _328100))]]], (492 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)))], (494 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2EF_2E0))], (496 ^ _309628) ^ [_328659] : [-(s(tyop_2Emin_2Ebool, _328659) = s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)), -(s(tyop_2Emin_2Ebool, _328659) = s(tyop_2Emin_2Ebool, c_2Ebool_2EF_2E0))], (502 ^ _309628) ^ [_328861, _328863] : [-(s(_328863, app_2E2(s(tyop_2Emin_2Efun(_328863, _328863), combin_i_2E0), s(_328863, _328861))) = s(_328863, _328861))], (504 ^ _309628) ^ [_329001, _329003, _329005, _329007] : [-(s(_329007, app_2E2(s(tyop_2Emin_2Efun(_329005, _329007), app_2E2(s(tyop_2Emin_2Efun(_329007, tyop_2Emin_2Efun(_329005, _329007)), combin_k_2E0), s(_329007, _329003))), s(_329005, _329001))) = s(_329007, _329003))], (506 ^ _309628) ^ [_329188, _329190, _329192, _329194, _329196, _329198] : [-(s(_329194, app_2E2(s(tyop_2Emin_2Efun(_329198, _329194), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_329198, _329196), tyop_2Emin_2Efun(_329198, _329194)), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_329198, tyop_2Emin_2Efun(_329196, _329194)), tyop_2Emin_2Efun(tyop_2Emin_2Efun(_329198, _329196), tyop_2Emin_2Efun(_329198, _329194))), combin_s_2E0), s(tyop_2Emin_2Efun(_329198, tyop_2Emin_2Efun(_329196, _329194)), _329192))), s(tyop_2Emin_2Efun(_329198, _329196), _329190))), s(_329198, _329188))) = s(_329194, app_2E2(s(tyop_2Emin_2Efun(_329196, _329194), app_2E2(s(tyop_2Emin_2Efun(_329198, tyop_2Emin_2Efun(_329196, _329194)), _329192), s(_329198, _329188))), s(_329196, app_2E2(s(tyop_2Emin_2Efun(_329198, _329196), _329190), s(_329198, _329188))))))], (508 ^ _309628) ^ [_329445, _329447] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool, _329447), s(tyop_2Emin_2Ebool, _329445)))), 511 ^ _309628 : [(512 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _329447)))], (514 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _329445)))]]], (516 ^ _309628) ^ [_329712, _329714] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool, _329714), s(tyop_2Emin_2Ebool, _329712))))), p(s(tyop_2Emin_2Ebool, _329714)), p(s(tyop_2Emin_2Ebool, _329712))], (536 ^ _309628) ^ [_330354, _330356] : [537 ^ _309628 : [(538 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _330356))], (540 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _330354))]], -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool, _330356), s(tyop_2Emin_2Ebool, _330354)))))], (526 ^ _309628) ^ [_330072, _330074] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool, _330074), s(tyop_2Emin_2Ebool, _330072)))), -(p(s(tyop_2Emin_2Ebool, _330074))), -(p(s(tyop_2Emin_2Ebool, _330072)))], (544 ^ _309628) ^ [_330685] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool, _330685)))), p(s(tyop_2Emin_2Ebool, _330685))], (550 ^ _309628) ^ [_330860] : [-(p(s(tyop_2Emin_2Ebool, _330860))), -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool, _330860)))))], (566 ^ _309628) ^ [_331397, _331399] : [567 ^ _309628 : [(568 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _331399)))], (570 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _331397))]], -(p(s(tyop_2Emin_2Ebool, c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool, _331399), s(tyop_2Emin_2Ebool, _331397)))))], (556 ^ _309628) ^ [_331116, _331118] : [p(s(tyop_2Emin_2Ebool, c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool, _331118), s(tyop_2Emin_2Ebool, _331116)))), p(s(tyop_2Emin_2Ebool, _331118)), -(p(s(tyop_2Emin_2Ebool, _331116)))], (574 ^ _309628) ^ [_331757, _331759, _331761] : [p(s(tyop_2Emin_2Ebool, c_2Emin_2E_3D_2E2(s(_331761, _331759), s(_331761, _331757)))), -(s(_331761, _331759) = s(_331761, _331757))], (580 ^ _309628) ^ [_331959, _331961, _331963] : [s(_331963, _331961) = s(_331963, _331959), -(p(s(tyop_2Emin_2Ebool, c_2Emin_2E_3D_2E2(s(_331963, _331961), s(_331963, _331959)))))], (586 ^ _309628) ^ [_332240, _332242] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(_332242, tyop_2Emin_2Ebool), _332240)))), 589 ^ _309628 : [(590 ^ _309628) ^ [_332390] : [-(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_332242, tyop_2Emin_2Ebool), _332240), s(_332242, _332390)))))]]], (592 ^ _309628) ^ [_332472, _332474] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_332474, tyop_2Emin_2Ebool), _332472), s(_332474, 593 ^ [_332472, _332474])))), -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(_332474, tyop_2Emin_2Ebool), _332472)))))], (599 ^ _309628) ^ [_332832, _332834] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(_332834, tyop_2Emin_2Ebool), _332832)))), -(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_332834, tyop_2Emin_2Ebool), _332832), s(_332834, 602 ^ [_332832, _332834])))))], (606 ^ _309628) ^ [_333113, _333115] : [607 ^ _309628 : [(608 ^ _309628) ^ [_333207] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_333115, tyop_2Emin_2Ebool), _333113), s(_333115, _333207))))]], -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(_333115, tyop_2Emin_2Ebool), _333113)))))], (622 ^ _309628) ^ [_333717, _333719] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool)), c_2Ebool_2E_2F_5C_2E0), s(tyop_2Emin_2Ebool, _333719))), s(tyop_2Emin_2Ebool, _333717)))), 625 ^ _309628 : [(626 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _333719)))], (628 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _333717)))]]], (612 ^ _309628) ^ [_333424, _333426] : [-(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool)), c_2Ebool_2E_2F_5C_2E0), s(tyop_2Emin_2Ebool, _333426))), s(tyop_2Emin_2Ebool, _333424))))), p(s(tyop_2Emin_2Ebool, _333426)), p(s(tyop_2Emin_2Ebool, _333424))], (630 ^ _309628) ^ [_334075, _334077] : [631 ^ _309628 : [(632 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _334077))], (634 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _334075))]], -(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool)), c_2Ebool_2E_5C_2F_2E0), s(tyop_2Emin_2Ebool, _334077))), s(tyop_2Emin_2Ebool, _334075)))))], (638 ^ _309628) ^ [_334353, _334355] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool)), c_2Ebool_2E_5C_2F_2E0), s(tyop_2Emin_2Ebool, _334355))), s(tyop_2Emin_2Ebool, _334353)))), -(p(s(tyop_2Emin_2Ebool, _334355))), -(p(s(tyop_2Emin_2Ebool, _334353)))], (648 ^ _309628) ^ [_334712] : [-(p(s(tyop_2Emin_2Ebool, _334712))), -(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool), c_2Ebool_2E_7E_2E0), s(tyop_2Emin_2Ebool, _334712)))))], (654 ^ _309628) ^ [_334891] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool), c_2Ebool_2E_7E_2E0), s(tyop_2Emin_2Ebool, _334891)))), p(s(tyop_2Emin_2Ebool, _334891))], (660 ^ _309628) ^ [_335147, _335149] : [661 ^ _309628 : [(662 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _335149)))], (664 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _335147))]], -(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool)), c_2Emin_2E_3D_3D_3E_2E0), s(tyop_2Emin_2Ebool, _335149))), s(tyop_2Emin_2Ebool, _335147)))))], (668 ^ _309628) ^ [_335426, _335428] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool)), c_2Emin_2E_3D_3D_3E_2E0), s(tyop_2Emin_2Ebool, _335428))), s(tyop_2Emin_2Ebool, _335426)))), p(s(tyop_2Emin_2Ebool, _335428)), -(p(s(tyop_2Emin_2Ebool, _335426)))], (678 ^ _309628) ^ [_335812, _335814, _335816] : [s(_335816, _335814) = s(_335816, _335812), -(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_335816, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(_335816, tyop_2Emin_2Efun(_335816, tyop_2Emin_2Ebool)), c_2Emin_2E_3D_2E0), s(_335816, _335814))), s(_335816, _335812)))))], (684 ^ _309628) ^ [_336050, _336052, _336054] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_336054, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(_336054, tyop_2Emin_2Efun(_336054, tyop_2Emin_2Ebool)), c_2Emin_2E_3D_2E0), s(_336054, _336052))), s(_336054, _336050)))), -(s(_336054, _336052) = s(_336054, _336050))], (690 ^ _309628) ^ [_336323, _336325] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(_336325, tyop_2Emin_2Ebool), _336323))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_336325, tyop_2Emin_2Ebool), tyop_2Emin_2Ebool), c_2Ebool_2E_21_2E0), s(tyop_2Emin_2Efun(_336325, tyop_2Emin_2Ebool), _336323))))], (692 ^ _309628) ^ [_336449, _336451] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(_336451, tyop_2Emin_2Ebool), _336449))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_336451, tyop_2Emin_2Ebool), tyop_2Emin_2Ebool), c_2Ebool_2E_3F_2E0), s(tyop_2Emin_2Efun(_336451, tyop_2Emin_2Ebool), _336449))))], (694 ^ _309628) ^ [_336575, _336577] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2E_3F_21_2E1(s(tyop_2Emin_2Efun(_336577, tyop_2Emin_2Ebool), _336575))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_336577, tyop_2Emin_2Ebool), tyop_2Emin_2Ebool), c_2Ebool_2E_3F_21_2E0), s(tyop_2Emin_2Efun(_336577, tyop_2Emin_2Ebool), _336575))))], (696 ^ _309628) ^ [_336701, _336703] : [-(s(_336703, c_2Emin_2E_40_2E1(s(tyop_2Emin_2Efun(_336703, tyop_2Emin_2Ebool), _336701))) = s(_336703, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_336703, tyop_2Emin_2Ebool), _336703), c_2Emin_2E_40_2E0), s(tyop_2Emin_2Efun(_336703, tyop_2Emin_2Ebool), _336701))))], (698 ^ _309628) ^ [_336813] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2EBOUNDED_2E1(s(tyop_2Emin_2Ebool, _336813))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Ebool), c_2Ebool_2EBOUNDED_2E0), s(tyop_2Emin_2Ebool, _336813))))], (700 ^ _309628) ^ [_336922, _336924] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2EDATATYPE_2E1(s(_336924, _336922))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_336924, tyop_2Emin_2Ebool), c_2Ebool_2EDATATYPE_2E0), s(_336924, _336922))))], (702 ^ _309628) ^ [_337053, _337055, _337057] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2EONE__ONE_2E1(s(tyop_2Emin_2Efun(_337057, _337055), _337053))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_337057, _337055), tyop_2Emin_2Ebool), c_2Ebool_2EONE__ONE_2E0), s(tyop_2Emin_2Efun(_337057, _337055), _337053))))], (704 ^ _309628) ^ [_337167] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2EONE__ONE_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Eind, tyop_2Emin_2Eind), _337167))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Emin_2Eind, tyop_2Emin_2Eind), tyop_2Emin_2Ebool), c_2Ebool_2EONE__ONE_2E0), s(tyop_2Emin_2Efun(tyop_2Emin_2Eind, tyop_2Emin_2Eind), _337167))))], (706 ^ _309628) ^ [_337290, _337292, _337294] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2EONTO_2E1(s(tyop_2Emin_2Efun(_337294, _337292), _337290))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_337294, _337292), tyop_2Emin_2Ebool), c_2Ebool_2EONTO_2E0), s(tyop_2Emin_2Efun(_337294, _337292), _337290))))], (708 ^ _309628) ^ [_337404] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2EONTO_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Eind, tyop_2Emin_2Eind), _337404))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Emin_2Eind, tyop_2Emin_2Eind), tyop_2Emin_2Ebool), c_2Ebool_2EONTO_2E0), s(tyop_2Emin_2Efun(tyop_2Emin_2Eind, tyop_2Emin_2Eind), _337404))))], (710 ^ _309628) ^ [_337527, _337529, _337531] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2EIN_2E2(s(_337531, _337529), s(tyop_2Emin_2Efun(_337531, tyop_2Emin_2Ebool), _337527))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_337531, tyop_2Emin_2Ebool), tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(_337531, tyop_2Emin_2Efun(tyop_2Emin_2Efun(_337531, tyop_2Emin_2Ebool), tyop_2Emin_2Ebool)), c_2Ebool_2EIN_2E0), s(_337531, _337529))), s(tyop_2Emin_2Efun(_337531, tyop_2Emin_2Ebool), _337527))))], (712 ^ _309628) ^ [_337705, _337707, _337709, _337711] : [-(s(_337709, c_2Ebool_2ELET_2E2(s(tyop_2Emin_2Efun(_337711, _337709), _337707), s(_337711, _337705))) = s(_337709, app_2E2(s(tyop_2Emin_2Efun(_337711, _337709), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_337711, _337709), tyop_2Emin_2Efun(_337711, _337709)), c_2Ebool_2ELET_2E0), s(tyop_2Emin_2Efun(_337711, _337709), _337707))), s(_337711, _337705))))], (714 ^ _309628) ^ [_337868, _337870, _337872] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2ERES__EXISTS_2E2(s(tyop_2Emin_2Efun(_337872, tyop_2Emin_2Ebool), _337870), s(tyop_2Emin_2Efun(_337872, tyop_2Emin_2Ebool), _337868))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_337872, tyop_2Emin_2Ebool), tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_337872, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(tyop_2Emin_2Efun(_337872, tyop_2Emin_2Ebool), tyop_2Emin_2Ebool)), c_2Ebool_2ERES__EXISTS_2E0), s(tyop_2Emin_2Efun(_337872, tyop_2Emin_2Ebool), _337870))), s(tyop_2Emin_2Efun(_337872, tyop_2Emin_2Ebool), _337868))))], (716 ^ _309628) ^ [_338041, _338043, _338045] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2ERES__EXISTS__UNIQUE_2E2(s(tyop_2Emin_2Efun(_338045, tyop_2Emin_2Ebool), _338043), s(tyop_2Emin_2Efun(_338045, tyop_2Emin_2Ebool), _338041))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_338045, tyop_2Emin_2Ebool), tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_338045, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(tyop_2Emin_2Efun(_338045, tyop_2Emin_2Ebool), tyop_2Emin_2Ebool)), c_2Ebool_2ERES__EXISTS__UNIQUE_2E0), s(tyop_2Emin_2Efun(_338045, tyop_2Emin_2Ebool), _338043))), s(tyop_2Emin_2Efun(_338045, tyop_2Emin_2Ebool), _338041))))], (718 ^ _309628) ^ [_338214, _338216, _338218] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2ERES__FORALL_2E2(s(tyop_2Emin_2Efun(_338218, tyop_2Emin_2Ebool), _338216), s(tyop_2Emin_2Efun(_338218, tyop_2Emin_2Ebool), _338214))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_338218, tyop_2Emin_2Ebool), tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_338218, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(tyop_2Emin_2Efun(_338218, tyop_2Emin_2Ebool), tyop_2Emin_2Ebool)), c_2Ebool_2ERES__FORALL_2E0), s(tyop_2Emin_2Efun(_338218, tyop_2Emin_2Ebool), _338216))), s(tyop_2Emin_2Efun(_338218, tyop_2Emin_2Ebool), _338214))))], (720 ^ _309628) ^ [_338387, _338389, _338391] : [-(s(_338391, c_2Ebool_2ERES__SELECT_2E2(s(tyop_2Emin_2Efun(_338391, tyop_2Emin_2Ebool), _338389), s(tyop_2Emin_2Efun(_338391, tyop_2Emin_2Ebool), _338387))) = s(_338391, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_338391, tyop_2Emin_2Ebool), _338391), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_338391, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(tyop_2Emin_2Efun(_338391, tyop_2Emin_2Ebool), _338391)), c_2Ebool_2ERES__SELECT_2E0), s(tyop_2Emin_2Efun(_338391, tyop_2Emin_2Ebool), _338389))), s(tyop_2Emin_2Efun(_338391, tyop_2Emin_2Ebool), _338387))))], (722 ^ _309628) ^ [_338574, _338576, _338578, _338580] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2ETYPE__DEFINITION_2E2(s(tyop_2Emin_2Efun(_338580, tyop_2Emin_2Ebool), _338576), s(tyop_2Emin_2Efun(_338578, _338580), _338574))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_338578, _338580), tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_338580, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(tyop_2Emin_2Efun(_338578, _338580), tyop_2Emin_2Ebool)), c_2Ebool_2ETYPE__DEFINITION_2E0), s(tyop_2Emin_2Efun(_338580, tyop_2Emin_2Ebool), _338576))), s(tyop_2Emin_2Efun(_338578, _338580), _338574))))], (724 ^ _309628) ^ [_338763, _338765, _338767, _338769] : [-(s(_338767, c_2Ebool_2Eliteral__case_2E2(s(tyop_2Emin_2Efun(_338769, _338767), _338765), s(_338769, _338763))) = s(_338767, app_2E2(s(tyop_2Emin_2Efun(_338769, _338767), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_338769, _338767), tyop_2Emin_2Efun(_338769, _338767)), c_2Ebool_2Eliteral__case_2E0), s(tyop_2Emin_2Efun(_338769, _338767), _338765))), s(_338769, _338763))))], (726 ^ _309628) ^ [_338940, _338942, _338944, _338946] : [-(s(_338946, c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool, _338944), s(_338946, _338942), s(_338946, _338940))) = s(_338946, app_2E2(s(tyop_2Emin_2Efun(_338946, _338946), app_2E2(s(tyop_2Emin_2Efun(_338946, tyop_2Emin_2Efun(_338946, _338946)), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Efun(_338946, tyop_2Emin_2Efun(_338946, _338946))), c_2Ebool_2ECOND_2E0), s(tyop_2Emin_2Ebool, _338944))), s(_338946, _338942))), s(_338946, _338940))))], (728 ^ _309628) ^ [_339103] : [-(s(tyop_2Emin_2Ebool, _339103) = s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)), -(s(tyop_2Emin_2Ebool, _339103) = s(tyop_2Emin_2Ebool, c_2Ebool_2EF_2E0))], (734 ^ _309628) ^ [_339333, _339335, _339337, _339339] : [-(s(_339337, app_2E2(s(tyop_2Emin_2Efun(_339339, _339337), _339335), s(_339339, _339333))) = s(_339337, app_2E2(s(tyop_2Emin_2Efun(_339339, _339337), _339335), s(_339339, _339333))))], (736 ^ _309628) ^ [_339490, _339492, _339494] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_339494, tyop_2Emin_2Ebool), _339492), s(_339494, _339490)))), -(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_339494, tyop_2Emin_2Ebool), _339492), s(_339494, c_2Emin_2E_40_2E1(s(tyop_2Emin_2Efun(_339494, tyop_2Emin_2Ebool), _339492)))))))], (743 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2EONE__ONE_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Eind, tyop_2Emin_2Eind), 741 ^ [])))))], (745 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2EONTO_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Eind, tyop_2Emin_2Eind), 741 ^ []))))], (747 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)), 750 ^ _309628 : [(751 ^ _309628) ^ [_340006] : [-(s(tyop_2Emin_2Ebool, _340006) = s(tyop_2Emin_2Ebool, _340006))]]], (753 ^ _309628) ^ [] : [s(tyop_2Emin_2Ebool, 754 ^ []) = s(tyop_2Emin_2Ebool, 754 ^ []), -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)))], (760 ^ _309628) ^ [_340297, _340299] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(_340299, tyop_2Emin_2Ebool), _340297)))), 763 ^ _309628 : [(764 ^ _309628) ^ [_340448] : [-(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_340299, tyop_2Emin_2Ebool), _340297), s(_340299, _340448))) = s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0))]]], (766 ^ _309628) ^ [_340531, _340533] : [s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_340533, tyop_2Emin_2Ebool), _340531), s(_340533, 767 ^ [_340531, _340533]))) = s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0), -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(_340533, tyop_2Emin_2Ebool), _340531)))))], (773 ^ _309628) ^ [_340850, _340852] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(_340852, tyop_2Emin_2Ebool), _340850))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_340852, tyop_2Emin_2Ebool), _340850), s(_340852, c_2Emin_2E_40_2E1(s(tyop_2Emin_2Efun(_340852, tyop_2Emin_2Ebool), _340850))))))], (775 ^ _309628) ^ [_341022, _341024] : [p(s(tyop_2Emin_2Ebool, _341024)), p(s(tyop_2Emin_2Ebool, _341022)), 782 ^ _309628 : [(783 ^ _309628) ^ [_341276] : [784 ^ _309628 : [(785 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _341024)))], (787 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _341022)))], (789 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _341276))]], -(p(s(tyop_2Emin_2Ebool, _341276)))]]], (793 ^ _309628) ^ [_341624, _341626] : [807 ^ _309628 : [(808 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _341626)))], (810 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _341624)))]], 795 ^ _309628 : [(806 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, 794 ^ [_341624, _341626]))], (796 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _341626)), p(s(tyop_2Emin_2Ebool, _341624)), -(p(s(tyop_2Emin_2Ebool, 794 ^ [_341624, _341626])))]]], (812 ^ _309628) ^ [_342307, _342309] : [813 ^ _309628 : [(814 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _342309))], (816 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _342307))]], 817 ^ _309628 : [(818 ^ _309628) ^ [_342553] : [819 ^ _309628 : [(820 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _342309)))], (822 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _342553))]], 825 ^ _309628 : [(826 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _342307)))], (828 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _342553))]], -(p(s(tyop_2Emin_2Ebool, _342553)))]]], (832 ^ _309628) ^ [_342998, _343000] : [-(p(s(tyop_2Emin_2Ebool, _343000))), -(p(s(tyop_2Emin_2Ebool, _342998))), 834 ^ _309628 : [(835 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _343000)), -(p(s(tyop_2Emin_2Ebool, 833 ^ [_342998, _343000])))], (847 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, 833 ^ [_342998, _343000]))], (841 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, _342998)), -(p(s(tyop_2Emin_2Ebool, 833 ^ [_342998, _343000])))]]], (855 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2EF_2E0)), 858 ^ _309628 : [(859 ^ _309628) ^ [_343824] : [-(p(s(tyop_2Emin_2Ebool, _343824)))]]], (861 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, 862 ^ [])), -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2EF_2E0)))], (878 ^ _309628) ^ [_344339] : [879 ^ _309628 : [(880 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _344339)))], (882 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2EF_2E0))]], p(s(tyop_2Emin_2Ebool, _344339))], (868 ^ _309628) ^ [_344093] : [-(p(s(tyop_2Emin_2Ebool, _344093))), p(s(tyop_2Emin_2Ebool, _344093)), -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2EF_2E0)))], (902 ^ _309628) ^ [_345308, _345310] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_3F_21_2E1(s(tyop_2Emin_2Efun(_345310, tyop_2Emin_2Ebool), _345308))))), p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(_345310, tyop_2Emin_2Ebool), _345308)))), 909 ^ _309628 : [(910 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_345310, tyop_2Emin_2Ebool), _345308), s(_345310, 907 ^ [_345308, _345310])))))], (912 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_345310, tyop_2Emin_2Ebool), _345308), s(_345310, 908 ^ [_345308, _345310])))))], (914 ^ _309628) ^ [] : [s(_345310, 907 ^ [_345308, _345310]) = s(_345310, 908 ^ [_345308, _345310])]]], (886 ^ _309628) ^ [_344650, _344652] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_3F_21_2E1(s(tyop_2Emin_2Efun(_344652, tyop_2Emin_2Ebool), _344650)))), 889 ^ _309628 : [(890 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(_344652, tyop_2Emin_2Ebool), _344650)))))], (892 ^ _309628) ^ [_344958, _344960] : [-(s(_344652, _344960) = s(_344652, _344958)), p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_344652, tyop_2Emin_2Ebool), _344650), s(_344652, _344960)))), p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_344652, tyop_2Emin_2Ebool), _344650), s(_344652, _344958))))]]], (918 ^ _309628) ^ [_346120, _346122, _346124, _346126] : [-(s(_346124, c_2Ebool_2ELET_2E2(s(tyop_2Emin_2Efun(_346126, _346124), _346122), s(_346126, _346120))) = s(_346124, app_2E2(s(tyop_2Emin_2Efun(_346126, _346124), _346122), s(_346126, _346120))))], (920 ^ _309628) ^ [_346263, _346265] : [953 ^ _309628 : [(954 ^ _309628) ^ [_348380, _348382, _348384] : [-(s(_346265, c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool, _348384), s(_346265, _348382), s(_346265, _348380))) = s(_346265, c_2Emin_2E_40_2E1(s(tyop_2Emin_2Efun(_346265, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(_346265, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Ebool)), app_2E2(s(tyop_2Emin_2Efun(_346265, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Ebool))), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Ebool)))), _346263), s(tyop_2Emin_2Ebool, _348384))), s(_346265, _348382))), s(_346265, _348380))))))]], 927 ^ _309628 : [(928 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_346265, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(_346265, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Ebool)), app_2E2(s(tyop_2Emin_2Efun(_346265, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Ebool))), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Ebool)))), _346263), s(tyop_2Emin_2Ebool, 921 ^ [_346263, _346265]))), s(_346265, 922 ^ [_346263, _346265]))), s(_346265, 923 ^ [_346263, _346265]))), s(_346265, 924 ^ [_346263, _346265])))))], (930 ^ _309628) ^ [] : [931 ^ _309628 : [(932 ^ _309628) ^ [] : [-(s(tyop_2Emin_2Ebool, 921 ^ [_346263, _346265]) = s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0))], (934 ^ _309628) ^ [] : [s(_346265, 924 ^ [_346263, _346265]) = s(_346265, 922 ^ [_346263, _346265])]], 935 ^ _309628 : [(936 ^ _309628) ^ [] : [-(s(tyop_2Emin_2Ebool, 921 ^ [_346263, _346265]) = s(tyop_2Emin_2Ebool, c_2Ebool_2EF_2E0))], (938 ^ _309628) ^ [] : [s(_346265, 924 ^ [_346263, _346265]) = s(_346265, 923 ^ [_346263, _346265])]]]], 939 ^ _309628 : [(952 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_346265, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(_346265, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Ebool)), app_2E2(s(tyop_2Emin_2Efun(_346265, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Ebool))), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Efun(_346265, tyop_2Emin_2Ebool)))), _346263), s(tyop_2Emin_2Ebool, 921 ^ [_346263, _346265]))), s(_346265, 922 ^ [_346263, _346265]))), s(_346265, 923 ^ [_346263, _346265]))), s(_346265, 924 ^ [_346263, _346265]))))], (940 ^ _309628) ^ [] : [s(tyop_2Emin_2Ebool, 921 ^ [_346263, _346265]) = s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0), -(s(_346265, 924 ^ [_346263, _346265]) = s(_346265, 922 ^ [_346263, _346265]))], (946 ^ _309628) ^ [] : [s(tyop_2Emin_2Ebool, 921 ^ [_346263, _346265]) = s(tyop_2Emin_2Ebool, c_2Ebool_2EF_2E0), -(s(_346265, 924 ^ [_346263, _346265]) = s(_346265, 923 ^ [_346263, _346265]))]]], (966 ^ _309628) ^ [_349103, _349105, _349107] : [969 ^ _309628 : [(970 ^ _309628) ^ [] : [-(s(_349105, app_2E2(s(tyop_2Emin_2Efun(_349107, _349105), _349103), s(_349107, 967 ^ [_349103, _349105, _349107]))) = s(_349105, app_2E2(s(tyop_2Emin_2Efun(_349107, _349105), _349103), s(_349107, 968 ^ [_349103, _349105, _349107]))))], (972 ^ _309628) ^ [] : [s(_349107, 967 ^ [_349103, _349105, _349107]) = s(_349107, 968 ^ [_349103, _349105, _349107])]], -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2EONE__ONE_2E1(s(tyop_2Emin_2Efun(_349107, _349105), _349103)))))], (956 ^ _309628) ^ [_348624, _348626, _348628] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2EONE__ONE_2E1(s(tyop_2Emin_2Efun(_348628, _348626), _348624)))), 959 ^ _309628 : [(960 ^ _309628) ^ [_348840, _348842] : [s(_348626, app_2E2(s(tyop_2Emin_2Efun(_348628, _348626), _348624), s(_348628, _348842))) = s(_348626, app_2E2(s(tyop_2Emin_2Efun(_348628, _348626), _348624), s(_348628, _348840))), -(s(_348628, _348842) = s(_348628, _348840))]]], (976 ^ _309628) ^ [_349784, _349786, _349788] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2EONTO_2E1(s(tyop_2Emin_2Efun(_349788, _349786), _349784)))), 980 ^ _309628 : [(981 ^ _309628) ^ [_350016] : [-(s(_349786, _350016) = s(_349786, app_2E2(s(tyop_2Emin_2Efun(_349788, _349786), _349784), s(_349788, 979 ^ [_349784, _349786, _349788, _350016]))))]]], (983 ^ _309628) ^ [_350115, _350117, _350119] : [985 ^ _309628 : [(986 ^ _309628) ^ [_350292] : [s(_350117, 984 ^ [_350115, _350117, _350119]) = s(_350117, app_2E2(s(tyop_2Emin_2Efun(_350119, _350117), _350115), s(_350119, _350292)))]], -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2EONTO_2E1(s(tyop_2Emin_2Efun(_350119, _350117), _350115)))))], (1013 ^ _309628) ^ [_351799, _351801, _351803, _351805] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2ETYPE__DEFINITION_2E2(s(tyop_2Emin_2Efun(_351805, tyop_2Emin_2Ebool), _351801), s(tyop_2Emin_2Efun(_351803, _351805), _351799))))), 1018 ^ _309628 : [(1019 ^ _309628) ^ [] : [-(s(_351805, app_2E2(s(tyop_2Emin_2Efun(_351803, _351805), _351799), s(_351803, 1016 ^ [_351799, _351801, _351803, _351805]))) = s(_351805, app_2E2(s(tyop_2Emin_2Efun(_351803, _351805), _351799), s(_351803, 1017 ^ [_351799, _351801, _351803, _351805]))))], (1021 ^ _309628) ^ [] : [s(_351803, 1016 ^ [_351799, _351801, _351803, _351805]) = s(_351803, 1017 ^ [_351799, _351801, _351803, _351805])]], 1025 ^ _309628 : [(1026 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_351805, tyop_2Emin_2Ebool), _351801), s(_351805, 1022 ^ [_351799, _351801, _351803, _351805])))))], (1028 ^ _309628) ^ [_352685] : [s(_351805, 1022 ^ [_351799, _351801, _351803, _351805]) = s(_351805, app_2E2(s(tyop_2Emin_2Efun(_351803, _351805), _351799), s(_351803, _352685)))]], 1030 ^ _309628 : [(1031 ^ _309628) ^ [] : [-(s(_351805, 1022 ^ [_351799, _351801, _351803, _351805]) = s(_351805, app_2E2(s(tyop_2Emin_2Efun(_351803, _351805), _351799), s(_351803, 1029 ^ [_351799, _351801, _351803, _351805]))))], (1033 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_351805, tyop_2Emin_2Ebool), _351801), s(_351805, 1022 ^ [_351799, _351801, _351803, _351805]))))]]], (990 ^ _309628) ^ [_350554, _350556, _350558, _350560] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2ETYPE__DEFINITION_2E2(s(tyop_2Emin_2Efun(_350560, tyop_2Emin_2Ebool), _350556), s(tyop_2Emin_2Efun(_350558, _350560), _350554)))), 993 ^ _309628 : [(994 ^ _309628) ^ [_350862, _350864] : [s(_350560, app_2E2(s(tyop_2Emin_2Efun(_350558, _350560), _350554), s(_350558, _350864))) = s(_350560, app_2E2(s(tyop_2Emin_2Efun(_350558, _350560), _350554), s(_350558, _350862))), -(s(_350558, _350864) = s(_350558, _350862))], (1000 ^ _309628) ^ [_351171] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_350560, tyop_2Emin_2Ebool), _350556), s(_350560, _351171)))), -(s(_350560, _351171) = s(_350560, app_2E2(s(tyop_2Emin_2Efun(_350558, _350560), _350554), s(_350558, 1003 ^ [_350554, _350556, _350558, _350560, _351171]))))], (1007 ^ _309628) ^ [_351516] : [1008 ^ _309628 : [(1009 ^ _309628) ^ [_351632] : [s(_350560, _351516) = s(_350560, app_2E2(s(tyop_2Emin_2Efun(_350558, _350560), _350554), s(_350558, _351632)))]], -(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_350560, tyop_2Emin_2Ebool), _350556), s(_350560, _351516)))))]]], (1037 ^ _309628) ^ [_353196, _353198, _353200, _353202] : [-(s(_353200, c_2Ebool_2Eliteral__case_2E2(s(tyop_2Emin_2Efun(_353202, _353200), _353198), s(_353202, _353196))) = s(_353200, app_2E2(s(tyop_2Emin_2Efun(_353202, _353200), _353198), s(_353202, _353196))))], (1039 ^ _309628) ^ [_353338, _353340, _353342] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2EIN_2E2(s(_353342, _353340), s(tyop_2Emin_2Efun(_353342, tyop_2Emin_2Ebool), _353338))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_353342, tyop_2Emin_2Ebool), _353338), s(_353342, _353340))))], (1051 ^ _309628) ^ [_353966, _353968, _353970] : [1053 ^ _309628 : [(1054 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2EIN_2E2(s(_353970, 1052 ^ [_353966, _353968, _353970]), s(tyop_2Emin_2Efun(_353970, tyop_2Emin_2Ebool), _353968)))))], (1056 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_353970, tyop_2Emin_2Ebool), _353966), s(_353970, 1052 ^ [_353966, _353968, _353970]))))]], -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2ERES__FORALL_2E2(s(tyop_2Emin_2Efun(_353970, tyop_2Emin_2Ebool), _353968), s(tyop_2Emin_2Efun(_353970, tyop_2Emin_2Ebool), _353966)))))], (1041 ^ _309628) ^ [_353522, _353524, _353526] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2ERES__FORALL_2E2(s(tyop_2Emin_2Efun(_353526, tyop_2Emin_2Ebool), _353524), s(tyop_2Emin_2Efun(_353526, tyop_2Emin_2Ebool), _353522)))), 1044 ^ _309628 : [(1045 ^ _309628) ^ [_353725] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2EIN_2E2(s(_353526, _353725), s(tyop_2Emin_2Efun(_353526, tyop_2Emin_2Ebool), _353524)))), -(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_353526, tyop_2Emin_2Ebool), _353522), s(_353526, _353725)))))]]], (1060 ^ _309628) ^ [_354500, _354502, _354504] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2ERES__EXISTS_2E2(s(tyop_2Emin_2Efun(_354504, tyop_2Emin_2Ebool), _354502), s(tyop_2Emin_2Efun(_354504, tyop_2Emin_2Ebool), _354500)))), 1064 ^ _309628 : [(1065 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2EIN_2E2(s(_354504, 1063 ^ [_354500, _354502, _354504]), s(tyop_2Emin_2Efun(_354504, tyop_2Emin_2Ebool), _354502)))))], (1067 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_354504, tyop_2Emin_2Ebool), _354500), s(_354504, 1063 ^ [_354500, _354502, _354504])))))]]], (1069 ^ _309628) ^ [_354941, _354943, _354945] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2ERES__EXISTS_2E2(s(tyop_2Emin_2Efun(_354945, tyop_2Emin_2Ebool), _354943), s(tyop_2Emin_2Efun(_354945, tyop_2Emin_2Ebool), _354941))))), 1070 ^ _309628 : [(1071 ^ _309628) ^ [_355080] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2EIN_2E2(s(_354945, _355080), s(tyop_2Emin_2Efun(_354945, tyop_2Emin_2Ebool), _354943)))), p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_354945, tyop_2Emin_2Ebool), _354941), s(_354945, _355080))))]]], (1160 ^ _309628) ^ [_361709] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2EBOUNDED_2E1(s(tyop_2Emin_2Ebool, _361709))) = s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0))], (1162 ^ _309628) ^ [_361789, _361791] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2EDATATYPE_2E1(s(_361791, _361789))) = s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0))], (1137 ^ _309628) ^ [_360055, _360057] : [1157 ^ _309628 : [(1158 ^ _309628) ^ [_361543, _361545] : [-(s(_360057, c_2Ebool_2ERES__SELECT_2E2(s(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), _361545), s(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), _361543))) = s(_360057, c_2Emin_2E_40_2E1(s(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool)), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool))), _360055), s(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), _361545))), s(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), _361543))))))]], 1151 ^ _309628 : [(1152 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2EIN_2E2(s(_360057, 1140 ^ [_360055, _360057]), s(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), 1138 ^ [_360055, _360057])))))], (1154 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), 1139 ^ [_360055, _360057]), s(_360057, 1140 ^ [_360055, _360057])))))], (1156 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool)), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool))), _360055), s(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), 1138 ^ [_360055, _360057]))), s(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), 1139 ^ [_360055, _360057]))), s(_360057, 1140 ^ [_360055, _360057]))))]], 1143 ^ _309628 : [(1144 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool)), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool))), _360055), s(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), 1138 ^ [_360055, _360057]))), s(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), 1139 ^ [_360055, _360057]))), s(_360057, 1140 ^ [_360055, _360057])))))], (1146 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2EIN_2E2(s(_360057, 1140 ^ [_360055, _360057]), s(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), 1138 ^ [_360055, _360057])))), p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_360057, tyop_2Emin_2Ebool), 1139 ^ [_360055, _360057]), s(_360057, 1140 ^ [_360055, _360057]))))]]], (1079 ^ _309628) ^ [_355463, _355465, _355467, _355469] : [1085 ^ _309628 : [(1086 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool)), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_355469, tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool))), _355467), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), 1080 ^ [_355463, _355465, _355467, _355469]))), s(_355469, 1081 ^ [_355463, _355465, _355467, _355469]))), s(_355469, 1082 ^ [_355463, _355465, _355467, _355469])))))], (1088 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), 1080 ^ [_355463, _355465, _355467, _355469]), s(_355469, 1081 ^ [_355463, _355465, _355467, _355469])))))], (1090 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), 1080 ^ [_355463, _355465, _355467, _355469]), s(_355469, 1082 ^ [_355463, _355465, _355467, _355469])))))], (1092 ^ _309628) ^ [] : [s(_355469, 1081 ^ [_355463, _355465, _355467, _355469]) = s(_355469, 1082 ^ [_355463, _355465, _355467, _355469])]], 1093 ^ _309628 : [(1104 ^ _309628) ^ [] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool)), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_355469, tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool))), _355467), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), 1080 ^ [_355463, _355465, _355467, _355469]))), s(_355469, 1081 ^ [_355463, _355465, _355467, _355469]))), s(_355469, 1082 ^ [_355463, _355465, _355467, _355469]))))], (1094 ^ _309628) ^ [] : [-(s(_355469, 1081 ^ [_355463, _355465, _355467, _355469]) = s(_355469, 1082 ^ [_355463, _355465, _355467, _355469])), p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), 1080 ^ [_355463, _355465, _355467, _355469]), s(_355469, 1081 ^ [_355463, _355465, _355467, _355469])))), p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), 1080 ^ [_355463, _355465, _355467, _355469]), s(_355469, 1082 ^ [_355463, _355465, _355467, _355469]))))]], s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool)), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool))), _355465), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), 1107 ^ [_355463, _355465, _355467, _355469]))), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), 1108 ^ [_355463, _355465, _355467, _355469]))), s(_355469, 1109 ^ [_355463, _355465, _355467, _355469]))) = s(tyop_2Emin_2Ebool, c_2Ebool_2ERES__FORALL_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), 1107 ^ [_355463, _355465, _355467, _355469]), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool)), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_355469, tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool))), _355467), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), 1108 ^ [_355463, _355465, _355467, _355469]))), s(_355469, 1109 ^ [_355463, _355465, _355467, _355469]))))), s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool)), _355463), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), 1114 ^ [_355463, _355465, _355467, _355469]))), s(_355469, 1115 ^ [_355463, _355465, _355467, _355469]))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), 1114 ^ [_355463, _355465, _355467, _355469]), s(_355469, 1115 ^ [_355463, _355465, _355467, _355469]))), 1118 ^ _309628 : [(1119 ^ _309628) ^ [_358934, _358936] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2ERES__EXISTS__UNIQUE_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), _358936), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), _358934)))), 1122 ^ _309628 : [(1123 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2ERES__EXISTS_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), _358936), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool)), _355463), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), _358934)))))))], (1125 ^ _309628) ^ [] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2ERES__FORALL_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), _358936), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool)), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool))), _355465), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), _358936))), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), _358934)))))))]]], (1127 ^ _309628) ^ [_359451, _359453] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2ERES__EXISTS__UNIQUE_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), _359453), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), _359451))))), p(s(tyop_2Emin_2Ebool, c_2Ebool_2ERES__EXISTS_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), _359453), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool)), _355463), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), _359451)))))), p(s(tyop_2Emin_2Ebool, c_2Ebool_2ERES__FORALL_2E2(s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), _359453), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool)), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool))), _355465), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), _359453))), s(tyop_2Emin_2Efun(_355469, tyop_2Emin_2Ebool), _359451))))))]]]], input).
% 0.33/1.37  ncf('1',plain,[p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0))],start(1164 ^ 0)).
% 0.33/1.37  ncf('1.1',plain,[-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)))],extension(269 ^ 1)).
% 0.33/1.37  %-----------------------------------------------------
% 0.33/1.37  End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------