%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : ITP019+1 : 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:21 EDT 2023
% Result : Theorem 0.31s 1.37s
% Output : Proof 0.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.11 % Problem : ITP019+1 : TPTP v8.1.2. Bugfixed v7.5.0.
% 0.09/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:27:54 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.31/1.37
% 0.31/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.31/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.31/1.37 %-----------------------------------------------------
% 0.31/1.37 ncf(matrix, plain, [(485 ^ _91911) ^ [] : [s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), 483 ^ []) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum, c_2Enum_2E0_2E0)))], (487 ^ _91911) ^ [] : [-(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), 483 ^ []))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum, c_2Enum_2E0_2E0))))], (20 ^ _91911) ^ [_92659, _92661] : [-(p(_92659)), _92661 = _92659, p(_92661)], (2 ^ _91911) ^ [_92055] : [-(_92055 = _92055)], (4 ^ _91911) ^ [_92162, _92164] : [_92164 = _92162, -(_92162 = _92164)], (10 ^ _91911) ^ [_92366, _92368, _92370] : [-(_92370 = _92366), _92370 = _92368, _92368 = _92366], (30 ^ _91911) ^ [_92984, _92986, _92988, _92990] : [-(c_2Ebool_2E_2F_5C_2E2(_92990, _92986) = c_2Ebool_2E_2F_5C_2E2(_92988, _92984)), _92990 = _92988, _92986 = _92984], (40 ^ _91911) ^ [_93343, _93345, _93347, _93349] : [-(c_2Ebool_2E_5C_2F_2E2(_93349, _93345) = c_2Ebool_2E_5C_2F_2E2(_93347, _93343)), _93349 = _93347, _93345 = _93343], (50 ^ _91911) ^ [_93674, _93676] : [_93676 = _93674, -(c_2Ebool_2E_7E_2E1(_93676) = c_2Ebool_2E_7E_2E1(_93674))], (56 ^ _91911) ^ [_93920, _93922, _93924, _93926] : [-(c_2Emin_2E_3D_3D_3E_2E2(_93926, _93922) = c_2Emin_2E_3D_3D_3E_2E2(_93924, _93920)), _93926 = _93924, _93922 = _93920], (66 ^ _91911) ^ [_94279, _94281, _94283, _94285] : [-(c_2Emin_2E_3D_2E2(_94285, _94281) = c_2Emin_2E_3D_2E2(_94283, _94279)), _94285 = _94283, _94281 = _94279], (76 ^ _91911) ^ [_94610, _94612] : [_94612 = _94610, -(c_2Ebool_2E_21_2E1(_94612) = c_2Ebool_2E_21_2E1(_94610))], (82 ^ _91911) ^ [_94828, _94830] : [_94830 = _94828, -(c_2Ebool_2E_3F_2E1(_94830) = c_2Ebool_2E_3F_2E1(_94828))], (88 ^ _91911) ^ [_95074, _95076, _95078, _95080] : [-(app_2E2(_95080, _95076) = app_2E2(_95078, _95074)), _95080 = _95078, _95076 = _95074], (98 ^ _91911) ^ [_95433, _95435, _95437, _95439] : [-(tyop_2Emin_2Efun(_95439, _95435) = tyop_2Emin_2Efun(_95437, _95433)), _95439 = _95437, _95435 = _95433], (108 ^ _91911) ^ [_95764, _95766] : [_95766 = _95764, -(c_2Ecomplex_2Ecomplex__inv_2E1(_95766) = c_2Ecomplex_2Ecomplex__inv_2E1(_95764))], (114 ^ _91911) ^ [_96010, _96012, _96014, _96016] : [-(tyop_2Epair_2Eprod(_96016, _96012) = tyop_2Epair_2Eprod(_96014, _96010)), _96016 = _96014, _96012 = _96010], (124 ^ _91911) ^ [_96341, _96343] : [_96343 = _96341, -(c_2Ecomplex_2Ecomplex__of__num_2E1(_96343) = c_2Ecomplex_2Ecomplex__of__num_2E1(_96341))], (130 ^ _91911) ^ [_96567, _96569, _96571, _96573] : [-(s(_96573, _96569) = s(_96571, _96567)), _96573 = _96571, _96569 = _96567], (140 ^ _91911) ^ [_96958, _96960, _96962, _96964] : [s(_96962, app_2E2(s(tyop_2Emin_2Efun(_96964, _96962), _96960), s(_96964, 141 ^ [_96958, _96960, _96962, _96964]))) = s(_96962, app_2E2(s(tyop_2Emin_2Efun(_96964, _96962), _96958), s(_96964, 141 ^ [_96958, _96960, _96962, _96964]))), -(s(tyop_2Emin_2Efun(_96964, _96962), _96960) = s(tyop_2Emin_2Efun(_96964, _96962), _96958))], (147 ^ _91911) ^ [_97374, _97376] : [-(s(tyop_2Emin_2Ebool, _97376) = s(tyop_2Emin_2Ebool, _97374)), 150 ^ _91911 : [(151 ^ _91911) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _97376)))], (153 ^ _91911) ^ [] : [p(s(tyop_2Emin_2Ebool, _97374))]], 154 ^ _91911 : [(155 ^ _91911) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _97374)))], (157 ^ _91911) ^ [] : [p(s(tyop_2Emin_2Ebool, _97376))]]], (161 ^ _91911) ^ [] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)))], (163 ^ _91911) ^ [] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2EF_2E0))], (165 ^ _91911) ^ [_97935] : [-(s(tyop_2Emin_2Ebool, _97935) = s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)), -(s(tyop_2Emin_2Ebool, _97935) = s(tyop_2Emin_2Ebool, c_2Ebool_2EF_2E0))], (171 ^ _91911) ^ [_98137, _98139] : [-(s(_98139, app_2E2(s(tyop_2Emin_2Efun(_98139, _98139), combin_i_2E0), s(_98139, _98137))) = s(_98139, _98137))], (173 ^ _91911) ^ [_98277, _98279, _98281, _98283] : [-(s(_98283, app_2E2(s(tyop_2Emin_2Efun(_98281, _98283), app_2E2(s(tyop_2Emin_2Efun(_98283, tyop_2Emin_2Efun(_98281, _98283)), combin_k_2E0), s(_98283, _98279))), s(_98281, _98277))) = s(_98283, _98279))], (175 ^ _91911) ^ [_98464, _98466, _98468, _98470, _98472, _98474] : [-(s(_98470, app_2E2(s(tyop_2Emin_2Efun(_98474, _98470), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_98474, _98472), tyop_2Emin_2Efun(_98474, _98470)), app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_98474, tyop_2Emin_2Efun(_98472, _98470)), tyop_2Emin_2Efun(tyop_2Emin_2Efun(_98474, _98472), tyop_2Emin_2Efun(_98474, _98470))), combin_s_2E0), s(tyop_2Emin_2Efun(_98474, tyop_2Emin_2Efun(_98472, _98470)), _98468))), s(tyop_2Emin_2Efun(_98474, _98472), _98466))), s(_98474, _98464))) = s(_98470, app_2E2(s(tyop_2Emin_2Efun(_98472, _98470), app_2E2(s(tyop_2Emin_2Efun(_98474, tyop_2Emin_2Efun(_98472, _98470)), _98468), s(_98474, _98464))), s(_98472, app_2E2(s(tyop_2Emin_2Efun(_98474, _98472), _98466), s(_98474, _98464))))))], (177 ^ _91911) ^ [_98721, _98723] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool, _98723), s(tyop_2Emin_2Ebool, _98721)))), 180 ^ _91911 : [(181 ^ _91911) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _98723)))], (183 ^ _91911) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _98721)))]]], (185 ^ _91911) ^ [_98988, _98990] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool, _98990), s(tyop_2Emin_2Ebool, _98988))))), p(s(tyop_2Emin_2Ebool, _98990)), p(s(tyop_2Emin_2Ebool, _98988))], (205 ^ _91911) ^ [_99630, _99632] : [206 ^ _91911 : [(207 ^ _91911) ^ [] : [p(s(tyop_2Emin_2Ebool, _99632))], (209 ^ _91911) ^ [] : [p(s(tyop_2Emin_2Ebool, _99630))]], -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool, _99632), s(tyop_2Emin_2Ebool, _99630)))))], (195 ^ _91911) ^ [_99348, _99350] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool, _99350), s(tyop_2Emin_2Ebool, _99348)))), -(p(s(tyop_2Emin_2Ebool, _99350))), -(p(s(tyop_2Emin_2Ebool, _99348)))], (213 ^ _91911) ^ [_99961] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool, _99961)))), p(s(tyop_2Emin_2Ebool, _99961))], (219 ^ _91911) ^ [_100136] : [-(p(s(tyop_2Emin_2Ebool, _100136))), -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool, _100136)))))], (235 ^ _91911) ^ [_100673, _100675] : [236 ^ _91911 : [(237 ^ _91911) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _100675)))], (239 ^ _91911) ^ [] : [p(s(tyop_2Emin_2Ebool, _100673))]], -(p(s(tyop_2Emin_2Ebool, c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool, _100675), s(tyop_2Emin_2Ebool, _100673)))))], (225 ^ _91911) ^ [_100392, _100394] : [p(s(tyop_2Emin_2Ebool, c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool, _100394), s(tyop_2Emin_2Ebool, _100392)))), p(s(tyop_2Emin_2Ebool, _100394)), -(p(s(tyop_2Emin_2Ebool, _100392)))], (243 ^ _91911) ^ [_101033, _101035, _101037] : [p(s(tyop_2Emin_2Ebool, c_2Emin_2E_3D_2E2(s(_101037, _101035), s(_101037, _101033)))), -(s(_101037, _101035) = s(_101037, _101033))], (249 ^ _91911) ^ [_101235, _101237, _101239] : [s(_101239, _101237) = s(_101239, _101235), -(p(s(tyop_2Emin_2Ebool, c_2Emin_2E_3D_2E2(s(_101239, _101237), s(_101239, _101235)))))], (255 ^ _91911) ^ [_101516, _101518] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(_101518, tyop_2Emin_2Ebool), _101516)))), 258 ^ _91911 : [(259 ^ _91911) ^ [_101666] : [-(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_101518, tyop_2Emin_2Ebool), _101516), s(_101518, _101666)))))]]], (261 ^ _91911) ^ [_101748, _101750] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_101750, tyop_2Emin_2Ebool), _101748), s(_101750, 262 ^ [_101748, _101750])))), -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(_101750, tyop_2Emin_2Ebool), _101748)))))], (268 ^ _91911) ^ [_102108, _102110] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(_102110, tyop_2Emin_2Ebool), _102108)))), -(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_102110, tyop_2Emin_2Ebool), _102108), s(_102110, 271 ^ [_102108, _102110])))))], (275 ^ _91911) ^ [_102389, _102391] : [276 ^ _91911 : [(277 ^ _91911) ^ [_102483] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_102391, tyop_2Emin_2Ebool), _102389), s(_102391, _102483))))]], -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(_102391, tyop_2Emin_2Ebool), _102389)))))], (291 ^ _91911) ^ [_102993, _102995] : [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, _102995))), s(tyop_2Emin_2Ebool, _102993)))), 294 ^ _91911 : [(295 ^ _91911) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _102995)))], (297 ^ _91911) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _102993)))]]], (281 ^ _91911) ^ [_102700, _102702] : [-(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, _102702))), s(tyop_2Emin_2Ebool, _102700))))), p(s(tyop_2Emin_2Ebool, _102702)), p(s(tyop_2Emin_2Ebool, _102700))], (299 ^ _91911) ^ [_103351, _103353] : [300 ^ _91911 : [(301 ^ _91911) ^ [] : [p(s(tyop_2Emin_2Ebool, _103353))], (303 ^ _91911) ^ [] : [p(s(tyop_2Emin_2Ebool, _103351))]], -(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, _103353))), s(tyop_2Emin_2Ebool, _103351)))))], (307 ^ _91911) ^ [_103629, _103631] : [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, _103631))), s(tyop_2Emin_2Ebool, _103629)))), -(p(s(tyop_2Emin_2Ebool, _103631))), -(p(s(tyop_2Emin_2Ebool, _103629)))], (317 ^ _91911) ^ [_103988] : [-(p(s(tyop_2Emin_2Ebool, _103988))), -(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, _103988)))))], (323 ^ _91911) ^ [_104167] : [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, _104167)))), p(s(tyop_2Emin_2Ebool, _104167))], (329 ^ _91911) ^ [_104423, _104425] : [330 ^ _91911 : [(331 ^ _91911) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _104425)))], (333 ^ _91911) ^ [] : [p(s(tyop_2Emin_2Ebool, _104423))]], -(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, _104425))), s(tyop_2Emin_2Ebool, _104423)))))], (337 ^ _91911) ^ [_104702, _104704] : [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, _104704))), s(tyop_2Emin_2Ebool, _104702)))), p(s(tyop_2Emin_2Ebool, _104704)), -(p(s(tyop_2Emin_2Ebool, _104702)))], (347 ^ _91911) ^ [_105088, _105090, _105092] : [s(_105092, _105090) = s(_105092, _105088), -(p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_105092, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(_105092, tyop_2Emin_2Efun(_105092, tyop_2Emin_2Ebool)), c_2Emin_2E_3D_2E0), s(_105092, _105090))), s(_105092, _105088)))))], (353 ^ _91911) ^ [_105326, _105328, _105330] : [p(s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(_105330, tyop_2Emin_2Ebool), app_2E2(s(tyop_2Emin_2Efun(_105330, tyop_2Emin_2Efun(_105330, tyop_2Emin_2Ebool)), c_2Emin_2E_3D_2E0), s(_105330, _105328))), s(_105330, _105326)))), -(s(_105330, _105328) = s(_105330, _105326))], (359 ^ _91911) ^ [_105599, _105601] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(_105601, tyop_2Emin_2Ebool), _105599))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_105601, tyop_2Emin_2Ebool), tyop_2Emin_2Ebool), c_2Ebool_2E_21_2E0), s(tyop_2Emin_2Efun(_105601, tyop_2Emin_2Ebool), _105599))))], (361 ^ _91911) ^ [_105725, _105727] : [-(s(tyop_2Emin_2Ebool, c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(_105727, tyop_2Emin_2Ebool), _105725))) = s(tyop_2Emin_2Ebool, app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(_105727, tyop_2Emin_2Ebool), tyop_2Emin_2Ebool), c_2Ebool_2E_3F_2E0), s(tyop_2Emin_2Efun(_105727, tyop_2Emin_2Ebool), _105725))))], (363 ^ _91911) ^ [_105837] : [-(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), _105837))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), app_2E2(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal)), c_2Ecomplex_2Ecomplex__inv_2E0), s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), _105837))))], (365 ^ _91911) ^ [_105932] : [-(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum, _105932))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), app_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum, tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal)), c_2Ecomplex_2Ecomplex__of__num_2E0), s(tyop_2Enum_2Enum, _105932))))], (367 ^ _91911) ^ [] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)))], (369 ^ _91911) ^ [_106138, _106140] : [p(s(tyop_2Emin_2Ebool, _106138)), -(p(s(tyop_2Emin_2Ebool, _106138)))], (376 ^ _91911) ^ [_106360, _106362] : [p(s(tyop_2Emin_2Ebool, _106360)), 379 ^ _91911 : [(380 ^ _91911) ^ [_106482] : [-(p(s(tyop_2Emin_2Ebool, _106360)))]]], (472 ^ _91911) ^ [_109207] : [s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), _109207))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum, c_2Enum_2E0_2E0))), -(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), _109207) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum, c_2Enum_2E0_2E0))))], (478 ^ _91911) ^ [_109385] : [s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), _109385) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum, c_2Enum_2E0_2E0))), -(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), _109385))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum, c_2Enum_2E0_2E0))))], (382 ^ _91911) ^ [_106637] : [383 ^ _91911 : [(384 ^ _91911) ^ [] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)))], (386 ^ _91911) ^ [] : [p(s(tyop_2Emin_2Ebool, _106637))]], -(p(s(tyop_2Emin_2Ebool, _106637)))], (390 ^ _91911) ^ [_106868] : [p(s(tyop_2Emin_2Ebool, _106868)), p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)), -(p(s(tyop_2Emin_2Ebool, _106868)))], (400 ^ _91911) ^ [_107162] : [401 ^ _91911 : [(402 ^ _91911) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _107162)))], (404 ^ _91911) ^ [] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0))]], -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)))], (408 ^ _91911) ^ [_107380] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)), p(s(tyop_2Emin_2Ebool, _107380)), -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)))], (418 ^ _91911) ^ [_107664] : [419 ^ _91911 : [(420 ^ _91911) ^ [] : [-(p(s(tyop_2Emin_2Ebool, c_2Ebool_2EF_2E0)))], (422 ^ _91911) ^ [] : [p(s(tyop_2Emin_2Ebool, _107664))]], -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)))], (426 ^ _91911) ^ [_107882] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)), p(s(tyop_2Emin_2Ebool, c_2Ebool_2EF_2E0)), -(p(s(tyop_2Emin_2Ebool, _107882)))], (436 ^ _91911) ^ [_108166] : [437 ^ _91911 : [(438 ^ _91911) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _108166)))], (440 ^ _91911) ^ [] : [p(s(tyop_2Emin_2Ebool, _108166))]], -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)))], (444 ^ _91911) ^ [_108394] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2ET_2E0)), p(s(tyop_2Emin_2Ebool, _108394)), -(p(s(tyop_2Emin_2Ebool, _108394)))], (454 ^ _91911) ^ [_108668] : [455 ^ _91911 : [(456 ^ _91911) ^ [] : [-(p(s(tyop_2Emin_2Ebool, _108668)))], (458 ^ _91911) ^ [] : [p(s(tyop_2Emin_2Ebool, c_2Ebool_2EF_2E0))]], p(s(tyop_2Emin_2Ebool, _108668))], (462 ^ _91911) ^ [_108900] : [-(p(s(tyop_2Emin_2Ebool, _108900))), p(s(tyop_2Emin_2Ebool, _108900)), -(p(s(tyop_2Emin_2Ebool, c_2Ebool_2EF_2E0)))]], input).
% 0.31/1.37 ncf('1',plain,[s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), 483 ^ []) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum, c_2Enum_2E0_2E0)))],start(485 ^ 0)).
% 0.31/1.37 ncf('1.1',plain,[-(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), 483 ^ []) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum, c_2Enum_2E0_2E0)))), s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), 483 ^ []))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum, c_2Enum_2E0_2E0)))],extension(472 ^ 1,bind([[_109207], [483 ^ []]]))).
% 0.31/1.37 ncf('1.1.1',plain,[-(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), 483 ^ []))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum, c_2Enum_2E0_2E0))))],extension(487 ^ 2)).
% 0.31/1.37 %-----------------------------------------------------
% 0.31/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------