%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUN070+2 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n005.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:30 EDT 2023
% Result : Theorem 0.58s 1.41s
% Output : Proof 0.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : NUN070+2 : TPTP v8.1.2. Released v7.3.0.
% 0.08/0.14 % Command : nanocop.sh %s %d
% 0.14/0.36 % Computer : n005.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 18 21:13:23 EDT 2023
% 0.14/0.36 % CPUTime :
% 0.58/1.41
% 0.58/1.41 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.58/1.41 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.58/1.41 %-----------------------------------------------------
% 0.58/1.41 ncf(matrix, plain, [(208 ^ _42590) ^ [_50780] : [223 ^ _42590 : [(224 ^ _42590) ^ [_51390] : [_50780 = _51390, 227 ^ _42590 : [(228 ^ _42590) ^ [_51528] : [r1(_51528), r2(_51528, _51390)]]]], 209 ^ _42590 : [(210 ^ _42590) ^ [_50912] : [211 ^ _42590 : [(212 ^ _42590) ^ [_51016] : [r1(_51016), r3(_50912, _51016, _50780)]], 217 ^ _42590 : [(218 ^ _42590) ^ [_51201] : [r1(_51201), r2(_51201, _50912)]]]]], (81 ^ _42590) ^ [_45335] : [82 ^ _42590 : [(83 ^ _42590) ^ [] : [r1(_45335)], (85 ^ _42590) ^ [] : [_45335 = 79 ^ []]], 86 ^ _42590 : [(87 ^ _42590) ^ [] : [-(r1(_45335))], (89 ^ _42590) ^ [] : [-(_45335 = 79 ^ [])]]], (92 ^ _42590) ^ [_45750, _45752] : [93 ^ _42590 : [(94 ^ _42590) ^ [] : [r2(_45752, _45750)], (96 ^ _42590) ^ [] : [_45750 = 90 ^ [_45752]]], 97 ^ _42590 : [(98 ^ _42590) ^ [] : [-(r2(_45752, _45750))], (100 ^ _42590) ^ [] : [-(_45750 = 90 ^ [_45752])]]], (103 ^ _42590) ^ [_46217, _46219, _46221] : [104 ^ _42590 : [(105 ^ _42590) ^ [] : [r3(_46221, _46219, _46217)], (107 ^ _42590) ^ [] : [_46217 = 101 ^ [_46219, _46221]]], 108 ^ _42590 : [(109 ^ _42590) ^ [] : [-(r3(_46221, _46219, _46217))], (111 ^ _42590) ^ [] : [-(_46217 = 101 ^ [_46219, _46221])]]], (114 ^ _42590) ^ [_46706, _46708, _46710] : [115 ^ _42590 : [(116 ^ _42590) ^ [] : [r4(_46710, _46708, _46706)], (118 ^ _42590) ^ [] : [_46706 = 112 ^ [_46708, _46710]]], 119 ^ _42590 : [(120 ^ _42590) ^ [] : [-(r4(_46710, _46708, _46706))], (122 ^ _42590) ^ [] : [-(_46706 = 112 ^ [_46708, _46710])]]], (127 ^ _42590) ^ [_47359, _47361] : [-(r2(_47359, 125 ^ [_47359, _47361]))], (129 ^ _42590) ^ [_47412, _47414] : [-(r3(_47414, 125 ^ [_47412, _47414], 124 ^ [_47412, _47414]))], (131 ^ _42590) ^ [_47475, _47477] : [-(124 ^ [_47475, _47477] = 123 ^ [_47475, _47477])], (134 ^ _42590) ^ [_47614, _47616] : [-(r2(132 ^ [_47614, _47616], 123 ^ [_47614, _47616]))], (136 ^ _42590) ^ [_47674, _47676] : [-(r3(_47676, _47674, 132 ^ [_47674, _47676]))], (141 ^ _42590) ^ [_48048, _48050] : [-(r2(_48048, 139 ^ [_48048, _48050]))], (143 ^ _42590) ^ [_48101, _48103] : [-(r4(_48103, 139 ^ [_48101, _48103], 138 ^ [_48101, _48103]))], (145 ^ _42590) ^ [_48164, _48166] : [-(138 ^ [_48164, _48166] = 137 ^ [_48164, _48166])], (148 ^ _42590) ^ [_48304, _48306] : [-(r3(146 ^ [_48304, _48306], _48306, 137 ^ [_48304, _48306]))], (150 ^ _42590) ^ [_48365, _48367] : [-(r4(_48367, _48365, 146 ^ [_48365, _48367]))], (152 ^ _42590) ^ [_48490, _48492] : [-(_48492 = _48490), 153 ^ _42590 : [(154 ^ _42590) ^ [_48599] : [r2(_48490, _48599), 155 ^ _42590 : [(156 ^ _42590) ^ [_48703] : [r2(_48492, _48703), _48703 = _48599]]]]], (168 ^ _42590) ^ [_49154] : [-(r1(166 ^ [_49154]))], (170 ^ _42590) ^ [_49202] : [-(r3(_49202, 166 ^ [_49202], 165 ^ [_49202]))], (172 ^ _42590) ^ [_49259] : [-(165 ^ [_49259] = _49259)], (176 ^ _42590) ^ [_49502] : [-(r1(174 ^ [_49502]))], (178 ^ _42590) ^ [_49550] : [-(r4(_49550, 174 ^ [_49550], 173 ^ [_49550]))], (181 ^ _42590) ^ [_49676] : [-(r1(179 ^ [_49676]))], (183 ^ _42590) ^ [_49724] : [-(173 ^ [_49724] = 179 ^ [_49724])], (185 ^ _42590) ^ [_49833] : [187 ^ _42590 : [(188 ^ _42590) ^ [] : [-(r1(186 ^ [_49833]))], (190 ^ _42590) ^ [] : [-(_49833 = 186 ^ [_49833])]], 193 ^ _42590 : [(194 ^ _42590) ^ [] : [-(r2(191 ^ [_49833], 192 ^ [_49833]))], (196 ^ _42590) ^ [] : [-(_49833 = 192 ^ [_49833])]]], (198 ^ _42590) ^ [_50352, _50354] : [r2(_50354, _50352), 199 ^ _42590 : [(200 ^ _42590) ^ [_50449] : [r1(_50449), _50449 = _50352]]], (2 ^ _42590) ^ [_42714] : [-(_42714 = _42714)], (4 ^ _42590) ^ [_42821, _42823] : [_42823 = _42821, -(_42821 = _42823)], (10 ^ _42590) ^ [_43025, _43027, _43029] : [-(_43029 = _43025), _43029 = _43027, _43027 = _43025], (20 ^ _42590) ^ [_43394, _43396, _43398, _43400, _43402, _43404] : [-(r4(_43402, _43398, _43394)), r4(_43404, _43400, _43396), _43404 = _43402, _43400 = _43398, _43396 = _43394], (38 ^ _42590) ^ [_44003, _44005, _44007, _44009, _44011, _44013] : [-(r3(_44011, _44007, _44003)), r3(_44013, _44009, _44005), _44013 = _44011, _44009 = _44007, _44005 = _44003], (56 ^ _42590) ^ [_44556, _44558] : [-(r1(_44556)), _44558 = _44556, r1(_44558)], (66 ^ _42590) ^ [_44859, _44861, _44863, _44865] : [-(r2(_44863, _44859)), r2(_44865, _44861), _44865 = _44863, _44861 = _44859]], input).
% 0.58/1.41 ncf('1',plain,[224 : 165 ^ [125 ^ [166 ^ [_30328], _30481]] = 125 ^ [166 ^ [_30328], _30481], 228 : r1(166 ^ [_30328]), 228 : r2(166 ^ [_30328], 125 ^ [166 ^ [_30328], _30481]), 212 : r1(166 ^ [125 ^ [166 ^ [_30328], _30481]]), 212 : r3(125 ^ [166 ^ [_30328], _30481], 166 ^ [125 ^ [166 ^ [_30328], _30481]], 165 ^ [125 ^ [166 ^ [_30328], _30481]]), 218 : r1(166 ^ [_30328]), 218 : r2(166 ^ [_30328], 125 ^ [166 ^ [_30328], _30481])],start(208 ^ 0,bind([[_50780, _51390, _51528, _50912, _51016, _51201], [165 ^ [125 ^ [166 ^ [_30328], _30481]], 125 ^ [166 ^ [_30328], _30481], 166 ^ [_30328], 125 ^ [166 ^ [_30328], _30481], 166 ^ [125 ^ [166 ^ [_30328], _30481]], 166 ^ [_30328]]]))).
% 0.58/1.41 ncf('1.1',plain,[-(165 ^ [125 ^ [166 ^ [_30328], _30481]] = 125 ^ [166 ^ [_30328], _30481])],extension(172 ^ 3,bind([[_49259], [125 ^ [166 ^ [_30328], _30481]]]))).
% 0.58/1.41 ncf('1.2',plain,[-(r1(166 ^ [_30328]))],extension(168 ^ 5,bind([[_49154], [_30328]]))).
% 0.58/1.41 ncf('1.3',plain,[-(r2(166 ^ [_30328], 125 ^ [166 ^ [_30328], _30481]))],extension(127 ^ 5,bind([[_47359, _47361], [166 ^ [_30328], _30481]]))).
% 0.58/1.41 ncf('1.4',plain,[-(r1(166 ^ [125 ^ [166 ^ [_30328], _30481]]))],extension(168 ^ 5,bind([[_49154], [125 ^ [166 ^ [_30328], _30481]]]))).
% 0.58/1.41 ncf('1.5',plain,[-(r3(125 ^ [166 ^ [_30328], _30481], 166 ^ [125 ^ [166 ^ [_30328], _30481]], 165 ^ [125 ^ [166 ^ [_30328], _30481]]))],extension(170 ^ 5,bind([[_49202], [125 ^ [166 ^ [_30328], _30481]]]))).
% 0.58/1.41 ncf('1.6',plain,[-(r1(166 ^ [_30328]))],extension(168 ^ 5,bind([[_49154], [_30328]]))).
% 0.58/1.41 ncf('1.7',plain,[-(r2(166 ^ [_30328], 125 ^ [166 ^ [_30328], _30481]))],extension(127 ^ 5,bind([[_47359, _47361], [166 ^ [_30328], _30481]]))).
% 0.58/1.41 %-----------------------------------------------------
% 0.58/1.41 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------