%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUN080+1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n007.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:46:31 EDT 2023
% Result : Theorem 0.35s 1.37s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUN080+1 : TPTP v8.1.2. Released v7.3.0.
% 0.00/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n007.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 20:58:38 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.35/1.37
% 0.35/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.35/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.35/1.37 %-----------------------------------------------------
% 0.35/1.37 ncf(matrix, plain, [(224 ^ _45505) ^ [_54347, _54349, _54351] : [id(_54347, _54349), 227 ^ _45505 : [(228 ^ _45505) ^ [_54510] : [r3(_54351, _54510, _54347), 231 ^ _45505 : [(232 ^ _45505) ^ [_54673] : [r2(_54673, _54510), 235 ^ _45505 : [(236 ^ _45505) ^ [_54829] : [r1(_54829), r2(_54829, _54673)]]]]]]], (3 ^ _45505) ^ [_45666] : [4 ^ _45505 : [(5 ^ _45505) ^ [] : [-(id(_45666, 1 ^ []))], (7 ^ _45505) ^ [] : [-(r1(_45666))]], 8 ^ _45505 : [(9 ^ _45505) ^ [] : [r1(_45666)], (11 ^ _45505) ^ [] : [id(_45666, 1 ^ [])]]], (14 ^ _45505) ^ [_46081, _46083] : [15 ^ _45505 : [(16 ^ _45505) ^ [] : [-(id(_46081, 12 ^ [_46083]))], (18 ^ _45505) ^ [] : [-(r2(_46083, _46081))]], 19 ^ _45505 : [(20 ^ _45505) ^ [] : [r2(_46083, _46081)], (22 ^ _45505) ^ [] : [id(_46081, 12 ^ [_46083])]]], (25 ^ _45505) ^ [_46548, _46550, _46552] : [26 ^ _45505 : [(27 ^ _45505) ^ [] : [-(id(_46548, 23 ^ [_46550, _46552]))], (29 ^ _45505) ^ [] : [-(r3(_46552, _46550, _46548))]], 30 ^ _45505 : [(31 ^ _45505) ^ [] : [r3(_46552, _46550, _46548)], (33 ^ _45505) ^ [] : [id(_46548, 23 ^ [_46550, _46552])]]], (36 ^ _45505) ^ [_47037, _47039, _47041] : [37 ^ _45505 : [(38 ^ _45505) ^ [] : [-(id(_47037, 34 ^ [_47039, _47041]))], (40 ^ _45505) ^ [] : [-(r4(_47041, _47039, _47037))]], 41 ^ _45505 : [(42 ^ _45505) ^ [] : [r4(_47041, _47039, _47037)], (44 ^ _45505) ^ [] : [id(_47037, 34 ^ [_47039, _47041])]]], (46 ^ _45505) ^ [_47413] : [-(id(_47413, _47413))], (48 ^ _45505) ^ [_47520, _47522] : [id(_47522, _47520), -(id(_47520, _47522))], (54 ^ _45505) ^ [_47746, _47748, _47750] : [id(_47750, _47748), -(id(_47750, _47746)), id(_47748, _47746)], (64 ^ _45505) ^ [_48059, _48061] : [id(_48061, _48059), 69 ^ _45505 : [(70 ^ _45505) ^ [] : [r1(_48061)], (72 ^ _45505) ^ [] : [r1(_48059)]], 73 ^ _45505 : [(74 ^ _45505) ^ [] : [-(r1(_48061))], (76 ^ _45505) ^ [] : [-(r1(_48059))]]], (78 ^ _45505) ^ [_48533, _48535, _48537, _48539] : [id(_48539, _48535), id(_48537, _48533), 87 ^ _45505 : [(88 ^ _45505) ^ [] : [r2(_48539, _48537)], (90 ^ _45505) ^ [] : [r2(_48535, _48533)]], 91 ^ _45505 : [(92 ^ _45505) ^ [] : [-(r2(_48539, _48537))], (94 ^ _45505) ^ [] : [-(r2(_48535, _48533))]]], (96 ^ _45505) ^ [_49170, _49172, _49174, _49176, _49178, _49180] : [id(_49180, _49174), id(_49178, _49172), id(_49176, _49170), 109 ^ _45505 : [(110 ^ _45505) ^ [] : [r3(_49180, _49178, _49176)], (112 ^ _45505) ^ [] : [r3(_49174, _49172, _49170)]], 113 ^ _45505 : [(114 ^ _45505) ^ [] : [-(r3(_49180, _49178, _49176))], (116 ^ _45505) ^ [] : [-(r3(_49174, _49172, _49170))]]], (118 ^ _45505) ^ [_49958, _49960, _49962, _49964, _49966, _49968] : [id(_49968, _49962), id(_49966, _49960), id(_49964, _49958), 131 ^ _45505 : [(132 ^ _45505) ^ [] : [r4(_49968, _49966, _49964)], (134 ^ _45505) ^ [] : [r4(_49962, _49960, _49958)]], 135 ^ _45505 : [(136 ^ _45505) ^ [] : [-(r4(_49968, _49966, _49964))], (138 ^ _45505) ^ [] : [-(r4(_49962, _49960, _49958))]]], (142 ^ _45505) ^ [_50863, _50865] : [-(id(140 ^ [_50863, _50865], 139 ^ [_50863, _50865]))], (145 ^ _45505) ^ [_50998, _51000] : [-(r2(_50998, 143 ^ [_50998, _51000]))], (147 ^ _45505) ^ [_51051, _51053] : [-(r3(_51053, 143 ^ [_51051, _51053], 140 ^ [_51051, _51053]))], (150 ^ _45505) ^ [_51191, _51193] : [-(r2(148 ^ [_51191, _51193], 139 ^ [_51191, _51193]))], (152 ^ _45505) ^ [_51251, _51253] : [-(r3(_51253, _51251, 148 ^ [_51251, _51253]))], (156 ^ _45505) ^ [_51550, _51552] : [-(id(154 ^ [_51550, _51552], 153 ^ [_51550, _51552]))], (159 ^ _45505) ^ [_51685, _51687] : [-(r2(_51685, 157 ^ [_51685, _51687]))], (161 ^ _45505) ^ [_51738, _51740] : [-(r4(_51740, 157 ^ [_51738, _51740], 154 ^ [_51738, _51740]))], (164 ^ _45505) ^ [_51879, _51881] : [-(r3(162 ^ [_51879, _51881], _51881, 153 ^ [_51879, _51881]))], (166 ^ _45505) ^ [_51940, _51942] : [-(r4(_51942, _51940, 162 ^ [_51940, _51942]))], (168 ^ _45505) ^ [_52065, _52067] : [-(id(_52067, _52065)), 169 ^ _45505 : [(170 ^ _45505) ^ [_52174] : [r2(_52065, _52174), 171 ^ _45505 : [(172 ^ _45505) ^ [_52278] : [id(_52278, _52174), r2(_52067, _52278)]]]]], (183 ^ _45505) ^ [_52659] : [-(id(181 ^ [_52659], _52659))], (186 ^ _45505) ^ [_52778] : [-(r1(184 ^ [_52778]))], (188 ^ _45505) ^ [_52826] : [-(r3(_52826, 184 ^ [_52826], 181 ^ [_52826]))], (192 ^ _45505) ^ [_53075] : [-(r1(190 ^ [_53075]))], (194 ^ _45505) ^ [_53123] : [-(r4(_53123, 190 ^ [_53123], 189 ^ [_53123]))], (197 ^ _45505) ^ [_53249] : [-(id(189 ^ [_53249], 195 ^ [_53249]))], (199 ^ _45505) ^ [_53303] : [-(r1(195 ^ [_53303]))], (201 ^ _45505) ^ [_53406] : [203 ^ _45505 : [(204 ^ _45505) ^ [] : [-(id(_53406, 202 ^ [_53406]))], (206 ^ _45505) ^ [] : [-(r1(202 ^ [_53406]))]], 209 ^ _45505 : [(210 ^ _45505) ^ [] : [-(id(_53406, 208 ^ [_53406]))], (212 ^ _45505) ^ [] : [-(r2(207 ^ [_53406], 208 ^ [_53406]))]]], (214 ^ _45505) ^ [_53925, _53927] : [r2(_53927, _53925), 215 ^ _45505 : [(216 ^ _45505) ^ [_54022] : [id(_54022, _53925), r1(_54022)]]]], input).
% 0.35/1.37 ncf('1',plain,[id(140 ^ [143 ^ [184 ^ [_32367], _32554], _31179], 140 ^ [143 ^ [184 ^ [_32367], _32554], _31179]), 228 : r3(_31179, 143 ^ [143 ^ [184 ^ [_32367], _32554], _31179], 140 ^ [143 ^ [184 ^ [_32367], _32554], _31179]), 232 : r2(143 ^ [184 ^ [_32367], _32554], 143 ^ [143 ^ [184 ^ [_32367], _32554], _31179]), 236 : r1(184 ^ [_32367]), 236 : r2(184 ^ [_32367], 143 ^ [184 ^ [_32367], _32554])],start(224 ^ 0,bind([[_54347, _54349, _54351, _54510, _54673, _54829], [140 ^ [143 ^ [184 ^ [_32367], _32554], _31179], 140 ^ [143 ^ [184 ^ [_32367], _32554], _31179], _31179, 143 ^ [143 ^ [184 ^ [_32367], _32554], _31179], 143 ^ [184 ^ [_32367], _32554], 184 ^ [_32367]]]))).
% 0.35/1.37 ncf('1.1',plain,[-(id(140 ^ [143 ^ [184 ^ [_32367], _32554], _31179], 140 ^ [143 ^ [184 ^ [_32367], _32554], _31179]))],extension(46 ^ 1,bind([[_47413], [140 ^ [143 ^ [184 ^ [_32367], _32554], _31179]]]))).
% 0.35/1.37 ncf('1.2',plain,[-(r3(_31179, 143 ^ [143 ^ [184 ^ [_32367], _32554], _31179], 140 ^ [143 ^ [184 ^ [_32367], _32554], _31179]))],extension(147 ^ 3,bind([[_51051, _51053], [143 ^ [184 ^ [_32367], _32554], _31179]]))).
% 0.35/1.37 ncf('1.3',plain,[-(r2(143 ^ [184 ^ [_32367], _32554], 143 ^ [143 ^ [184 ^ [_32367], _32554], _31179]))],extension(145 ^ 5,bind([[_50998, _51000], [143 ^ [184 ^ [_32367], _32554], _31179]]))).
% 0.35/1.37 ncf('1.4',plain,[-(r1(184 ^ [_32367]))],extension(186 ^ 7,bind([[_52778], [_32367]]))).
% 0.35/1.37 ncf('1.5',plain,[-(r2(184 ^ [_32367], 143 ^ [184 ^ [_32367], _32554]))],extension(145 ^ 7,bind([[_50998, _51000], [184 ^ [_32367], _32554]]))).
% 0.35/1.37 %-----------------------------------------------------
% 0.35/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------