%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUN073+1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n012.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.41s 1.37s
% Output : Proof 0.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : NUN073+1 : TPTP v8.1.2. Released v7.3.0.
% 0.06/0.11 % Command : nanocop.sh %s %d
% 0.11/0.32 % Computer : n012.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Thu May 18 21:09:32 EDT 2023
% 0.11/0.33 % CPUTime :
% 0.41/1.37
% 0.41/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.41/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.41/1.37 %-----------------------------------------------------
% 0.41/1.37 ncf(matrix, plain, [(227 ^ _45426) ^ [] : [-(r1(225 ^ []))], (229 ^ _45426) ^ [] : [-(r2(225 ^ [], 224 ^ []))], (231 ^ _45426) ^ [] : [-(id(224 ^ [], 223 ^ []))], (235 ^ _45426) ^ [] : [-(r1(233 ^ []))], (237 ^ _45426) ^ [] : [-(r2(233 ^ [], 232 ^ []))], (239 ^ _45426) ^ [] : [-(r2(232 ^ [], 223 ^ []))], (3 ^ _45426) ^ [_45587] : [4 ^ _45426 : [(5 ^ _45426) ^ [] : [-(id(_45587, 1 ^ []))], (7 ^ _45426) ^ [] : [-(r1(_45587))]], 8 ^ _45426 : [(9 ^ _45426) ^ [] : [r1(_45587)], (11 ^ _45426) ^ [] : [id(_45587, 1 ^ [])]]], (14 ^ _45426) ^ [_46002, _46004] : [15 ^ _45426 : [(16 ^ _45426) ^ [] : [-(id(_46002, 12 ^ [_46004]))], (18 ^ _45426) ^ [] : [-(r2(_46004, _46002))]], 19 ^ _45426 : [(20 ^ _45426) ^ [] : [r2(_46004, _46002)], (22 ^ _45426) ^ [] : [id(_46002, 12 ^ [_46004])]]], (25 ^ _45426) ^ [_46469, _46471, _46473] : [26 ^ _45426 : [(27 ^ _45426) ^ [] : [-(id(_46469, 23 ^ [_46471, _46473]))], (29 ^ _45426) ^ [] : [-(r3(_46473, _46471, _46469))]], 30 ^ _45426 : [(31 ^ _45426) ^ [] : [r3(_46473, _46471, _46469)], (33 ^ _45426) ^ [] : [id(_46469, 23 ^ [_46471, _46473])]]], (36 ^ _45426) ^ [_46958, _46960, _46962] : [37 ^ _45426 : [(38 ^ _45426) ^ [] : [-(id(_46958, 34 ^ [_46960, _46962]))], (40 ^ _45426) ^ [] : [-(r4(_46962, _46960, _46958))]], 41 ^ _45426 : [(42 ^ _45426) ^ [] : [r4(_46962, _46960, _46958)], (44 ^ _45426) ^ [] : [id(_46958, 34 ^ [_46960, _46962])]]], (46 ^ _45426) ^ [_47334] : [-(id(_47334, _47334))], (48 ^ _45426) ^ [_47441, _47443] : [id(_47443, _47441), -(id(_47441, _47443))], (54 ^ _45426) ^ [_47667, _47669, _47671] : [id(_47671, _47669), -(id(_47671, _47667)), id(_47669, _47667)], (64 ^ _45426) ^ [_47980, _47982] : [id(_47982, _47980), 69 ^ _45426 : [(70 ^ _45426) ^ [] : [r1(_47982)], (72 ^ _45426) ^ [] : [r1(_47980)]], 73 ^ _45426 : [(74 ^ _45426) ^ [] : [-(r1(_47982))], (76 ^ _45426) ^ [] : [-(r1(_47980))]]], (78 ^ _45426) ^ [_48454, _48456, _48458, _48460] : [id(_48460, _48456), id(_48458, _48454), 87 ^ _45426 : [(88 ^ _45426) ^ [] : [r2(_48460, _48458)], (90 ^ _45426) ^ [] : [r2(_48456, _48454)]], 91 ^ _45426 : [(92 ^ _45426) ^ [] : [-(r2(_48460, _48458))], (94 ^ _45426) ^ [] : [-(r2(_48456, _48454))]]], (96 ^ _45426) ^ [_49091, _49093, _49095, _49097, _49099, _49101] : [id(_49101, _49095), id(_49099, _49093), id(_49097, _49091), 109 ^ _45426 : [(110 ^ _45426) ^ [] : [r3(_49101, _49099, _49097)], (112 ^ _45426) ^ [] : [r3(_49095, _49093, _49091)]], 113 ^ _45426 : [(114 ^ _45426) ^ [] : [-(r3(_49101, _49099, _49097))], (116 ^ _45426) ^ [] : [-(r3(_49095, _49093, _49091))]]], (118 ^ _45426) ^ [_49879, _49881, _49883, _49885, _49887, _49889] : [id(_49889, _49883), id(_49887, _49881), id(_49885, _49879), 131 ^ _45426 : [(132 ^ _45426) ^ [] : [r4(_49889, _49887, _49885)], (134 ^ _45426) ^ [] : [r4(_49883, _49881, _49879)]], 135 ^ _45426 : [(136 ^ _45426) ^ [] : [-(r4(_49889, _49887, _49885))], (138 ^ _45426) ^ [] : [-(r4(_49883, _49881, _49879))]]], (142 ^ _45426) ^ [_50784, _50786] : [-(id(140 ^ [_50784, _50786], 139 ^ [_50784, _50786]))], (145 ^ _45426) ^ [_50919, _50921] : [-(r2(_50919, 143 ^ [_50919, _50921]))], (147 ^ _45426) ^ [_50972, _50974] : [-(r3(_50974, 143 ^ [_50972, _50974], 140 ^ [_50972, _50974]))], (150 ^ _45426) ^ [_51112, _51114] : [-(r2(148 ^ [_51112, _51114], 139 ^ [_51112, _51114]))], (152 ^ _45426) ^ [_51172, _51174] : [-(r3(_51174, _51172, 148 ^ [_51172, _51174]))], (156 ^ _45426) ^ [_51471, _51473] : [-(id(154 ^ [_51471, _51473], 153 ^ [_51471, _51473]))], (159 ^ _45426) ^ [_51606, _51608] : [-(r2(_51606, 157 ^ [_51606, _51608]))], (161 ^ _45426) ^ [_51659, _51661] : [-(r4(_51661, 157 ^ [_51659, _51661], 154 ^ [_51659, _51661]))], (164 ^ _45426) ^ [_51800, _51802] : [-(r3(162 ^ [_51800, _51802], _51802, 153 ^ [_51800, _51802]))], (166 ^ _45426) ^ [_51861, _51863] : [-(r4(_51863, _51861, 162 ^ [_51861, _51863]))], (168 ^ _45426) ^ [_51986, _51988] : [-(id(_51988, _51986)), 169 ^ _45426 : [(170 ^ _45426) ^ [_52095] : [r2(_51986, _52095), 171 ^ _45426 : [(172 ^ _45426) ^ [_52199] : [id(_52199, _52095), r2(_51988, _52199)]]]]], (183 ^ _45426) ^ [_52580] : [-(id(181 ^ [_52580], _52580))], (186 ^ _45426) ^ [_52699] : [-(r1(184 ^ [_52699]))], (188 ^ _45426) ^ [_52747] : [-(r3(_52747, 184 ^ [_52747], 181 ^ [_52747]))], (192 ^ _45426) ^ [_52996] : [-(r1(190 ^ [_52996]))], (194 ^ _45426) ^ [_53044] : [-(r4(_53044, 190 ^ [_53044], 189 ^ [_53044]))], (197 ^ _45426) ^ [_53170] : [-(id(189 ^ [_53170], 195 ^ [_53170]))], (199 ^ _45426) ^ [_53224] : [-(r1(195 ^ [_53224]))], (201 ^ _45426) ^ [_53327] : [203 ^ _45426 : [(204 ^ _45426) ^ [] : [-(id(_53327, 202 ^ [_53327]))], (206 ^ _45426) ^ [] : [-(r1(202 ^ [_53327]))]], 209 ^ _45426 : [(210 ^ _45426) ^ [] : [-(id(_53327, 208 ^ [_53327]))], (212 ^ _45426) ^ [] : [-(r2(207 ^ [_53327], 208 ^ [_53327]))]]], (214 ^ _45426) ^ [_53846, _53848] : [r2(_53848, _53846), 215 ^ _45426 : [(216 ^ _45426) ^ [_53943] : [id(_53943, _53846), r1(_53943)]]]], input).
% 0.41/1.37 ncf('1',plain,[r2(233 ^ [], 232 ^ []), 216 : id(225 ^ [], 232 ^ []), 216 : r1(225 ^ [])],start(214 ^ 0,bind([[_53846, _53848, _53943], [232 ^ [], 233 ^ [], 225 ^ []]]))).
% 0.41/1.37 ncf('1.1',plain,[-(r2(233 ^ [], 232 ^ []))],extension(237 ^ 1)).
% 0.41/1.37 ncf('1.2',plain,[-(id(225 ^ [], 232 ^ [])), 170 : r2(232 ^ [], 223 ^ []), 172 : id(224 ^ [], 223 ^ []), 172 : r2(225 ^ [], 224 ^ [])],extension(168 ^ 3,bind([[_51986, _51988, _52095, _52199], [232 ^ [], 225 ^ [], 223 ^ [], 224 ^ []]]))).
% 0.41/1.37 ncf('1.2.1',plain,[-(r2(232 ^ [], 223 ^ []))],extension(239 ^ 6)).
% 0.41/1.37 ncf('1.2.2',plain,[-(id(224 ^ [], 223 ^ []))],extension(231 ^ 8)).
% 0.41/1.37 ncf('1.2.3',plain,[-(r2(225 ^ [], 224 ^ []))],extension(229 ^ 8)).
% 0.41/1.37 ncf('1.3',plain,[-(r1(225 ^ []))],extension(227 ^ 3)).
% 0.41/1.37 %-----------------------------------------------------
% 0.41/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------