%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUN087+1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n032.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:32 EDT 2023
% Result : Theorem 1.06s 1.30s
% Output : Proof 1.06s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.08 % Problem : NUN087+1 : TPTP v8.1.2. Released v7.3.0.
% 0.04/0.08 % Command : nanocop.sh %s %d
% 0.07/0.27 % Computer : n032.cluster.edu
% 0.07/0.27 % Model : x86_64 x86_64
% 0.07/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.27 % Memory : 8042.1875MB
% 0.07/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.27 % CPULimit : 300
% 0.07/0.27 % WCLimit : 300
% 0.07/0.27 % DateTime : Thu May 18 21:17:19 EDT 2023
% 0.07/0.27 % CPUTime :
% 1.06/1.30
% 1.06/1.30 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 1.06/1.30 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.06/1.30 %-----------------------------------------------------
% 1.06/1.30 ncf(matrix, plain, [(224 ^ _46076) ^ [_54890] : [225 ^ _46076 : [(226 ^ _46076) ^ [_54990] : [r1(_54990), r4(_54990, _54990, _54890)]], 231 ^ _46076 : [(232 ^ _46076) ^ [_55167] : [id(_54890, _55167), r1(_55167)]]], (3 ^ _46076) ^ [_46237] : [4 ^ _46076 : [(5 ^ _46076) ^ [] : [-(id(_46237, 1 ^ []))], (7 ^ _46076) ^ [] : [-(r1(_46237))]], 8 ^ _46076 : [(9 ^ _46076) ^ [] : [r1(_46237)], (11 ^ _46076) ^ [] : [id(_46237, 1 ^ [])]]], (14 ^ _46076) ^ [_46652, _46654] : [15 ^ _46076 : [(16 ^ _46076) ^ [] : [-(id(_46652, 12 ^ [_46654]))], (18 ^ _46076) ^ [] : [-(r2(_46654, _46652))]], 19 ^ _46076 : [(20 ^ _46076) ^ [] : [r2(_46654, _46652)], (22 ^ _46076) ^ [] : [id(_46652, 12 ^ [_46654])]]], (25 ^ _46076) ^ [_47119, _47121, _47123] : [26 ^ _46076 : [(27 ^ _46076) ^ [] : [-(id(_47119, 23 ^ [_47121, _47123]))], (29 ^ _46076) ^ [] : [-(r3(_47123, _47121, _47119))]], 30 ^ _46076 : [(31 ^ _46076) ^ [] : [r3(_47123, _47121, _47119)], (33 ^ _46076) ^ [] : [id(_47119, 23 ^ [_47121, _47123])]]], (36 ^ _46076) ^ [_47608, _47610, _47612] : [37 ^ _46076 : [(38 ^ _46076) ^ [] : [-(id(_47608, 34 ^ [_47610, _47612]))], (40 ^ _46076) ^ [] : [-(r4(_47612, _47610, _47608))]], 41 ^ _46076 : [(42 ^ _46076) ^ [] : [r4(_47612, _47610, _47608)], (44 ^ _46076) ^ [] : [id(_47608, 34 ^ [_47610, _47612])]]], (46 ^ _46076) ^ [_47984] : [-(id(_47984, _47984))], (48 ^ _46076) ^ [_48091, _48093] : [id(_48093, _48091), -(id(_48091, _48093))], (54 ^ _46076) ^ [_48317, _48319, _48321] : [id(_48321, _48319), -(id(_48321, _48317)), id(_48319, _48317)], (64 ^ _46076) ^ [_48630, _48632] : [id(_48632, _48630), 69 ^ _46076 : [(70 ^ _46076) ^ [] : [r1(_48632)], (72 ^ _46076) ^ [] : [r1(_48630)]], 73 ^ _46076 : [(74 ^ _46076) ^ [] : [-(r1(_48632))], (76 ^ _46076) ^ [] : [-(r1(_48630))]]], (78 ^ _46076) ^ [_49104, _49106, _49108, _49110] : [id(_49110, _49106), id(_49108, _49104), 87 ^ _46076 : [(88 ^ _46076) ^ [] : [r2(_49110, _49108)], (90 ^ _46076) ^ [] : [r2(_49106, _49104)]], 91 ^ _46076 : [(92 ^ _46076) ^ [] : [-(r2(_49110, _49108))], (94 ^ _46076) ^ [] : [-(r2(_49106, _49104))]]], (96 ^ _46076) ^ [_49741, _49743, _49745, _49747, _49749, _49751] : [id(_49751, _49745), id(_49749, _49743), id(_49747, _49741), 109 ^ _46076 : [(110 ^ _46076) ^ [] : [r3(_49751, _49749, _49747)], (112 ^ _46076) ^ [] : [r3(_49745, _49743, _49741)]], 113 ^ _46076 : [(114 ^ _46076) ^ [] : [-(r3(_49751, _49749, _49747))], (116 ^ _46076) ^ [] : [-(r3(_49745, _49743, _49741))]]], (118 ^ _46076) ^ [_50529, _50531, _50533, _50535, _50537, _50539] : [id(_50539, _50533), id(_50537, _50531), id(_50535, _50529), 131 ^ _46076 : [(132 ^ _46076) ^ [] : [r4(_50539, _50537, _50535)], (134 ^ _46076) ^ [] : [r4(_50533, _50531, _50529)]], 135 ^ _46076 : [(136 ^ _46076) ^ [] : [-(r4(_50539, _50537, _50535))], (138 ^ _46076) ^ [] : [-(r4(_50533, _50531, _50529))]]], (142 ^ _46076) ^ [_51434, _51436] : [-(id(140 ^ [_51434, _51436], 139 ^ [_51434, _51436]))], (145 ^ _46076) ^ [_51569, _51571] : [-(r2(_51569, 143 ^ [_51569, _51571]))], (147 ^ _46076) ^ [_51622, _51624] : [-(r3(_51624, 143 ^ [_51622, _51624], 140 ^ [_51622, _51624]))], (150 ^ _46076) ^ [_51762, _51764] : [-(r2(148 ^ [_51762, _51764], 139 ^ [_51762, _51764]))], (152 ^ _46076) ^ [_51822, _51824] : [-(r3(_51824, _51822, 148 ^ [_51822, _51824]))], (156 ^ _46076) ^ [_52121, _52123] : [-(id(154 ^ [_52121, _52123], 153 ^ [_52121, _52123]))], (159 ^ _46076) ^ [_52256, _52258] : [-(r2(_52256, 157 ^ [_52256, _52258]))], (161 ^ _46076) ^ [_52309, _52311] : [-(r4(_52311, 157 ^ [_52309, _52311], 154 ^ [_52309, _52311]))], (164 ^ _46076) ^ [_52450, _52452] : [-(r3(162 ^ [_52450, _52452], _52452, 153 ^ [_52450, _52452]))], (166 ^ _46076) ^ [_52511, _52513] : [-(r4(_52513, _52511, 162 ^ [_52511, _52513]))], (168 ^ _46076) ^ [_52636, _52638] : [-(id(_52638, _52636)), 169 ^ _46076 : [(170 ^ _46076) ^ [_52745] : [r2(_52636, _52745), 171 ^ _46076 : [(172 ^ _46076) ^ [_52849] : [id(_52849, _52745), r2(_52638, _52849)]]]]], (183 ^ _46076) ^ [_53230] : [-(id(181 ^ [_53230], _53230))], (186 ^ _46076) ^ [_53349] : [-(r1(184 ^ [_53349]))], (188 ^ _46076) ^ [_53397] : [-(r3(_53397, 184 ^ [_53397], 181 ^ [_53397]))], (192 ^ _46076) ^ [_53646] : [-(r1(190 ^ [_53646]))], (194 ^ _46076) ^ [_53694] : [-(r4(_53694, 190 ^ [_53694], 189 ^ [_53694]))], (197 ^ _46076) ^ [_53820] : [-(id(189 ^ [_53820], 195 ^ [_53820]))], (199 ^ _46076) ^ [_53874] : [-(r1(195 ^ [_53874]))], (201 ^ _46076) ^ [_53977] : [203 ^ _46076 : [(204 ^ _46076) ^ [] : [-(id(_53977, 202 ^ [_53977]))], (206 ^ _46076) ^ [] : [-(r1(202 ^ [_53977]))]], 209 ^ _46076 : [(210 ^ _46076) ^ [] : [-(id(_53977, 208 ^ [_53977]))], (212 ^ _46076) ^ [] : [-(r2(207 ^ [_53977], 208 ^ [_53977]))]]], (214 ^ _46076) ^ [_54496, _54498] : [r2(_54498, _54496), 215 ^ _46076 : [(216 ^ _46076) ^ [_54593] : [id(_54593, _54496), r1(_54593)]]]], input).
% 1.06/1.30 ncf('1',plain,[226 : r1(181 ^ [190 ^ [1 ^ []]]), 226 : r4(181 ^ [190 ^ [1 ^ []]], 181 ^ [190 ^ [1 ^ []]], 189 ^ [1 ^ []]), 232 : id(189 ^ [1 ^ []], 189 ^ [1 ^ []]), 232 : r1(189 ^ [1 ^ []])],start(224 ^ 0,bind([[_54890, _54990, _55167], [189 ^ [1 ^ []], 181 ^ [190 ^ [1 ^ []]], 189 ^ [1 ^ []]]]))).
% 1.06/1.30 ncf('1.1',plain,[-(r1(181 ^ [190 ^ [1 ^ []]])), id(181 ^ [190 ^ [1 ^ []]], 190 ^ [1 ^ []]), 72 : r1(190 ^ [1 ^ []])],extension(64 ^ 3,bind([[_48630, _48632], [190 ^ [1 ^ []], 181 ^ [190 ^ [1 ^ []]]]]))).
% 1.06/1.30 ncf('1.1.1',plain,[-(id(181 ^ [190 ^ [1 ^ []]], 190 ^ [1 ^ []]))],extension(183 ^ 4,bind([[_53230], [190 ^ [1 ^ []]]]))).
% 1.06/1.30 ncf('1.1.2',plain,[-(r1(190 ^ [1 ^ []]))],extension(192 ^ 6,bind([[_53646], [1 ^ []]]))).
% 1.06/1.30 ncf('1.2',plain,[-(r4(181 ^ [190 ^ [1 ^ []]], 181 ^ [190 ^ [1 ^ []]], 189 ^ [1 ^ []])), id(181 ^ [190 ^ [1 ^ []]], 1 ^ []), id(181 ^ [190 ^ [1 ^ []]], 190 ^ [1 ^ []]), id(189 ^ [1 ^ []], 189 ^ [1 ^ []]), 134 : r4(1 ^ [], 190 ^ [1 ^ []], 189 ^ [1 ^ []])],extension(118 ^ 3,bind([[_50529, _50531, _50533, _50535, _50537, _50539], [189 ^ [1 ^ []], 190 ^ [1 ^ []], 1 ^ [], 189 ^ [1 ^ []], 181 ^ [190 ^ [1 ^ []]], 181 ^ [190 ^ [1 ^ []]]]]))).
% 1.06/1.30 ncf('1.2.1',plain,[-(id(181 ^ [190 ^ [1 ^ []]], 1 ^ [])), 9 : r1(181 ^ [190 ^ [1 ^ []]])],extension(3 ^ 4,bind([[_46237], [181 ^ [190 ^ [1 ^ []]]]]))).
% 1.06/1.30 ncf('1.2.1.1',plain,[-(r1(181 ^ [190 ^ [1 ^ []]]))],lemmata('x')).
% 1.06/1.30 ncf('1.2.2',plain,[-(id(181 ^ [190 ^ [1 ^ []]], 190 ^ [1 ^ []]))],extension(183 ^ 4,bind([[_53230], [190 ^ [1 ^ []]]]))).
% 1.06/1.30 ncf('1.2.3',plain,[-(id(189 ^ [1 ^ []], 189 ^ [1 ^ []]))],extension(46 ^ 4,bind([[_47984], [189 ^ [1 ^ []]]]))).
% 1.06/1.30 ncf('1.2.4',plain,[-(r4(1 ^ [], 190 ^ [1 ^ []], 189 ^ [1 ^ []]))],extension(194 ^ 6,bind([[_53694], [1 ^ []]]))).
% 1.06/1.30 ncf('1.3',plain,[-(id(189 ^ [1 ^ []], 189 ^ [1 ^ []]))],extension(46 ^ 3,bind([[_47984], [189 ^ [1 ^ []]]]))).
% 1.06/1.30 ncf('1.4',plain,[-(r1(189 ^ [1 ^ []])), id(189 ^ [1 ^ []], 195 ^ [1 ^ []]), 72 : r1(195 ^ [1 ^ []])],extension(64 ^ 3,bind([[_48630, _48632], [195 ^ [1 ^ []], 189 ^ [1 ^ []]]]))).
% 1.06/1.30 ncf('1.4.1',plain,[-(id(189 ^ [1 ^ []], 195 ^ [1 ^ []]))],extension(197 ^ 4,bind([[_53820], [1 ^ []]]))).
% 1.06/1.30 ncf('1.4.2',plain,[-(r1(195 ^ [1 ^ []]))],extension(199 ^ 6,bind([[_53874], [1 ^ []]]))).
% 1.06/1.30 %-----------------------------------------------------
% 1.06/1.30 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------