%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : RNG070+1 : TPTP v8.1.2. Released v4.0.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:49:44 EDT 2023
% Result : Theorem 0.37s 1.39s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : RNG070+1 : TPTP v8.1.2. Released v4.0.0.
% 0.06/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n012.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 18 20:19:16 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.37/1.39
% 0.37/1.39 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.37/1.39 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/1.39 %-----------------------------------------------------
% 0.37/1.39 ncf(matrix, plain, [(760 ^ _108752) ^ [] : [sdtlseqdt0(sdtpldt0(xR, xS), sdtpldt0(xP, xP))], (78 ^ _108752) ^ [_111287, _111289] : [_111289 = _111287, -(smndt0(_111289) = smndt0(_111287))], (84 ^ _108752) ^ [_111505, _111507] : [_111507 = _111505, -(szszuzczcdt0(_111507) = szszuzczcdt0(_111505))], (90 ^ _108752) ^ [_111723, _111725] : [_111725 = _111723, -(sziznziztdt0(_111725) = sziznziztdt0(_111723))], (96 ^ _108752) ^ [_111969, _111971, _111973, _111975] : [-(sdtlbdtrb0(_111975, _111971) = sdtlbdtrb0(_111973, _111969)), _111975 = _111973, _111971 = _111969], (106 ^ _108752) ^ [_112300, _112302] : [_112302 = _112300, -(aDimensionOf0(_112302) = aDimensionOf0(_112300))], (112 ^ _108752) ^ [_112546, _112548, _112550, _112552] : [-(sdtasasdt0(_112552, _112548) = sdtasasdt0(_112550, _112546)), _112552 = _112550, _112548 = _112546], (122 ^ _108752) ^ [_112905, _112907, _112909, _112911] : [-(sdtasdt0(_112911, _112907) = sdtasdt0(_112909, _112905)), _112911 = _112909, _112907 = _112905], (132 ^ _108752) ^ [_113244, _113246, _113248, _113250] : [-(sdtpldt0(_113250, _113246) = sdtpldt0(_113248, _113244)), _113250 = _113248, _113246 = _113244], (2 ^ _108752) ^ [_108896] : [-(_108896 = _108896)], (4 ^ _108752) ^ [_109003, _109005] : [_109005 = _109003, -(_109003 = _109005)], (10 ^ _108752) ^ [_109207, _109209, _109211] : [-(_109211 = _109207), _109211 = _109209, _109209 = _109207], (20 ^ _108752) ^ [_109520, _109522] : [-(aNaturalNumber0(_109520)), _109522 = _109520, aNaturalNumber0(_109522)], (30 ^ _108752) ^ [_109843, _109845, _109847, _109849] : [-(iLess0(_109847, _109843)), iLess0(_109849, _109845), _109849 = _109847, _109845 = _109843], (44 ^ _108752) ^ [_110259, _110261] : [-(aVector0(_110259)), _110261 = _110259, aVector0(_110261)], (54 ^ _108752) ^ [_110554, _110556] : [-(aScalar0(_110554)), _110556 = _110554, aScalar0(_110556)], (64 ^ _108752) ^ [_110857, _110859, _110861, _110863] : [-(sdtlseqdt0(_110861, _110857)), sdtlseqdt0(_110863, _110859), _110863 = _110861, _110859 = _110857], (142 ^ _108752) ^ [_113591] : [aNaturalNumber0(_113591), true___, -(true___)], (152 ^ _108752) ^ [] : [-(aNaturalNumber0(sz00))], (154 ^ _108752) ^ [_113899] : [aNaturalNumber0(_113899), 157 ^ _108752 : [(158 ^ _108752) ^ [] : [-(aNaturalNumber0(szszuzczcdt0(_113899)))], (160 ^ _108752) ^ [] : [szszuzczcdt0(_113899) = sz00]]], (162 ^ _108752) ^ [_114167] : [170 ^ _108752 : [(171 ^ _108752) ^ [] : [-(aNaturalNumber0(169 ^ [_114167]))], (173 ^ _108752) ^ [] : [-(_114167 = szszuzczcdt0(169 ^ [_114167]))]], aNaturalNumber0(_114167), -(_114167 = sz00)], (175 ^ _108752) ^ [_114595, _114597] : [aNaturalNumber0(_114597), aNaturalNumber0(_114595), szszuzczcdt0(_114597) = szszuzczcdt0(_114595), -(_114597 = _114595)], (189 ^ _108752) ^ [_114989, _114991] : [aNaturalNumber0(_114991), aNaturalNumber0(_114989), iLess0(_114991, _114989), true___, -(true___)], (207 ^ _108752) ^ [_115435] : [aNaturalNumber0(_115435), -(iLess0(_115435, szszuzczcdt0(_115435)))], (213 ^ _108752) ^ [_115627] : [aScalar0(_115627), true___, -(true___)], (223 ^ _108752) ^ [] : [-(aScalar0(sz0z00))], (225 ^ _108752) ^ [_115949, _115951] : [-(aScalar0(sdtpldt0(_115951, _115949))), aScalar0(_115951), aScalar0(_115949)], (235 ^ _108752) ^ [_116248, _116250] : [-(aScalar0(sdtasdt0(_116250, _116248))), aScalar0(_116250), aScalar0(_116248)], (245 ^ _108752) ^ [_116533] : [aScalar0(_116533), -(aScalar0(smndt0(_116533)))], (251 ^ _108752) ^ [_116723] : [aScalar0(_116723), 254 ^ _108752 : [(255 ^ _108752) ^ [] : [-(sdtpldt0(_116723, sz0z00) = _116723)], (257 ^ _108752) ^ [] : [-(sdtpldt0(sz0z00, _116723) = _116723)], (259 ^ _108752) ^ [] : [-(sdtasdt0(_116723, sz0z00) = sz0z00)], (261 ^ _108752) ^ [] : [-(sdtasdt0(sz0z00, _116723) = sz0z00)], (263 ^ _108752) ^ [] : [-(sdtpldt0(_116723, smndt0(_116723)) = sz0z00)], (265 ^ _108752) ^ [] : [-(sdtpldt0(smndt0(_116723), _116723) = sz0z00)], (267 ^ _108752) ^ [] : [-(smndt0(smndt0(_116723)) = _116723)], (269 ^ _108752) ^ [] : [-(smndt0(sz0z00) = sz0z00)]]], (271 ^ _108752) ^ [_117490, _117492, _117494] : [282 ^ _108752 : [(283 ^ _108752) ^ [] : [-(sdtpldt0(sdtpldt0(_117494, _117492), _117490) = sdtpldt0(_117494, sdtpldt0(_117492, _117490)))], (285 ^ _108752) ^ [] : [-(sdtpldt0(_117494, _117492) = sdtpldt0(_117492, _117494))], (287 ^ _108752) ^ [] : [-(sdtasdt0(sdtasdt0(_117494, _117492), _117490) = sdtasdt0(_117494, sdtasdt0(_117492, _117490)))], (289 ^ _108752) ^ [] : [-(sdtasdt0(_117494, _117492) = sdtasdt0(_117492, _117494))]], aScalar0(_117494), aScalar0(_117492), aScalar0(_117490)], (291 ^ _108752) ^ [_118201, _118203, _118205] : [302 ^ _108752 : [(303 ^ _108752) ^ [] : [-(sdtasdt0(_118205, sdtpldt0(_118203, _118201)) = sdtpldt0(sdtasdt0(_118205, _118203), sdtasdt0(_118205, _118201)))], (305 ^ _108752) ^ [] : [-(sdtasdt0(sdtpldt0(_118205, _118203), _118201) = sdtpldt0(sdtasdt0(_118205, _118201), sdtasdt0(_118203, _118201)))]], aScalar0(_118205), aScalar0(_118203), aScalar0(_118201)], (307 ^ _108752) ^ [_118762, _118764, _118766, _118768] : [-(sdtasdt0(sdtpldt0(_118768, _118766), sdtpldt0(_118764, _118762)) = sdtpldt0(sdtpldt0(sdtasdt0(_118768, _118764), sdtasdt0(_118768, _118762)), sdtpldt0(sdtasdt0(_118766, _118764), sdtasdt0(_118766, _118762)))), aScalar0(_118768), aScalar0(_118766), aScalar0(_118764), aScalar0(_118762)], (325 ^ _108752) ^ [_119327, _119329] : [332 ^ _108752 : [(333 ^ _108752) ^ [] : [-(sdtasdt0(_119329, smndt0(_119327)) = smndt0(sdtasdt0(_119329, _119327)))], (335 ^ _108752) ^ [] : [-(sdtasdt0(smndt0(_119329), _119327) = smndt0(sdtasdt0(_119329, _119327)))]], aScalar0(_119329), aScalar0(_119327)], (337 ^ _108752) ^ [_119737, _119739] : [-(sdtasdt0(smndt0(_119739), smndt0(_119737)) = sdtasdt0(_119739, _119737)), aScalar0(_119739), aScalar0(_119737)], (347 ^ _108752) ^ [_120052, _120054] : [aScalar0(_120054), aScalar0(_120052), sdtlseqdt0(_120054, _120052), true___, -(true___)], (365 ^ _108752) ^ [_120498] : [aScalar0(_120498), -(sdtlseqdt0(_120498, _120498))], (371 ^ _108752) ^ [_120700, _120702] : [aScalar0(_120702), aScalar0(_120700), -(_120702 = _120700), sdtlseqdt0(_120702, _120700), sdtlseqdt0(_120700, _120702)], (389 ^ _108752) ^ [_121189, _121191, _121193] : [aScalar0(_121193), aScalar0(_121191), aScalar0(_121189), -(sdtlseqdt0(_121193, _121189)), sdtlseqdt0(_121193, _121191), sdtlseqdt0(_121191, _121189)], (411 ^ _108752) ^ [_121803, _121805, _121807, _121809] : [-(sdtlseqdt0(sdtpldt0(_121809, _121805), sdtpldt0(_121807, _121803))), sdtlseqdt0(_121809, _121807), sdtlseqdt0(_121805, _121803), aScalar0(_121809), aScalar0(_121807), aScalar0(_121805), aScalar0(_121803)], (437 ^ _108752) ^ [_122546, _122548, _122550, _122552] : [aScalar0(_122552), aScalar0(_122550), aScalar0(_122548), aScalar0(_122546), -(sdtlseqdt0(sdtasdt0(_122552, _122548), sdtasdt0(_122550, _122546))), sdtlseqdt0(_122552, _122550), sdtlseqdt0(sz0z00, _122548), sdtlseqdt0(_122548, _122546)], (467 ^ _108752) ^ [_123360, _123362] : [aScalar0(_123362), aScalar0(_123360), -(sdtlseqdt0(_123362, _123360)), -(sdtlseqdt0(_123360, _123362))], (481 ^ _108752) ^ [_123747, _123749] : [aScalar0(_123749), aScalar0(_123747), 496 ^ _108752 : [(497 ^ _108752) ^ [] : [-(sdtlseqdt0(sz0z00, sdtpldt0(_123749, _123747)))], (499 ^ _108752) ^ [] : [-(sdtlseqdt0(sz0z00, sdtasdt0(_123749, _123747)))]], sdtlseqdt0(sz0z00, _123749), sdtlseqdt0(sz0z00, _123747)], (501 ^ _108752) ^ [_124295] : [aScalar0(_124295), -(sdtlseqdt0(sz0z00, sdtasdt0(_124295, _124295)))], (507 ^ _108752) ^ [_124503, _124505] : [aScalar0(_124505), aScalar0(_124503), -(_124505 = _124503), sdtlseqdt0(sz0z00, _124505), sdtlseqdt0(sz0z00, _124503), sdtasdt0(_124505, _124505) = sdtasdt0(_124503, _124503)], (529 ^ _108752) ^ [_125065] : [aVector0(_125065), true___, -(true___)], (539 ^ _108752) ^ [_125320] : [aVector0(_125320), -(aNaturalNumber0(aDimensionOf0(_125320)))], (545 ^ _108752) ^ [_125524, _125526] : [-(aScalar0(sdtlbdtrb0(_125526, _125524))), aVector0(_125526), aNaturalNumber0(_125524)], (555 ^ _108752) ^ [_125809] : [aVector0(_125809), -(aDimensionOf0(_125809) = sz00), 562 ^ _108752 : [(563 ^ _108752) ^ [_126092] : [_126092 = sziznziztdt0(_125809), 566 ^ _108752 : [(567 ^ _108752) ^ [] : [-(aVector0(_126092))], (569 ^ _108752) ^ [] : [-(szszuzczcdt0(aDimensionOf0(_126092)) = aDimensionOf0(_125809))], (571 ^ _108752) ^ [_126394] : [aNaturalNumber0(_126394), -(sdtlbdtrb0(_126092, _126394) = sdtlbdtrb0(_125809, _126394))]]], (577 ^ _108752) ^ [_126585] : [-(_126585 = sziznziztdt0(_125809)), aVector0(_126585), szszuzczcdt0(aDimensionOf0(_126585)) = aDimensionOf0(_125809), 587 ^ _108752 : [(588 ^ _108752) ^ [] : [-(aNaturalNumber0(586 ^ [_125809, _126585]))], (590 ^ _108752) ^ [] : [sdtlbdtrb0(_126585, 586 ^ [_125809, _126585]) = sdtlbdtrb0(_125809, 586 ^ [_125809, _126585])]]]]], (594 ^ _108752) ^ [_127167, _127169] : [aVector0(_127169), aVector0(_127167), -(aDimensionOf0(sziznziztdt0(_127169)) = aDimensionOf0(sziznziztdt0(_127167))), aDimensionOf0(_127169) = aDimensionOf0(_127167), -(aDimensionOf0(_127167) = sz00)], (612 ^ _108752) ^ [_127673, _127675] : [aVector0(_127675), aVector0(_127673), aDimensionOf0(_127675) = aDimensionOf0(_127673), -(aScalar0(sdtasasdt0(_127675, _127673)))], (626 ^ _108752) ^ [_128071, _128073] : [aVector0(_128073), aVector0(_128071), -(sdtasasdt0(_128073, _128071) = sz0z00), aDimensionOf0(_128073) = aDimensionOf0(_128071), aDimensionOf0(_128071) = sz00], (644 ^ _108752) ^ [_128564, _128566] : [aVector0(_128566), aVector0(_128564), -(sdtasasdt0(_128566, _128564) = sdtpldt0(sdtasasdt0(sziznziztdt0(_128566), sziznziztdt0(_128564)), sdtasdt0(sdtlbdtrb0(_128566, aDimensionOf0(_128566)), sdtlbdtrb0(_128564, aDimensionOf0(_128564))))), aDimensionOf0(_128566) = aDimensionOf0(_128564), -(aDimensionOf0(_128564) = sz00)], (662 ^ _108752) ^ [_129092] : [aVector0(_129092), -(sdtlseqdt0(sz0z00, sdtasasdt0(_129092, _129092)))], (668 ^ _108752) ^ [] : [-(aVector0(xs))], (670 ^ _108752) ^ [] : [-(aVector0(xt))], (690 ^ _108752) ^ [] : [-(aDimensionOf0(xs) = aDimensionOf0(xt))], (692 ^ _108752) ^ [] : [aDimensionOf0(xs) = sz00], (694 ^ _108752) ^ [] : [-(aVector0(xp))], (696 ^ _108752) ^ [] : [-(xp = sziznziztdt0(xs))], (698 ^ _108752) ^ [] : [-(aVector0(xq))], (700 ^ _108752) ^ [] : [-(xq = sziznziztdt0(xt))], (702 ^ _108752) ^ [] : [-(aScalar0(xA))], (704 ^ _108752) ^ [] : [-(xA = sdtlbdtrb0(xs, aDimensionOf0(xs)))], (706 ^ _108752) ^ [] : [-(aScalar0(xB))], (708 ^ _108752) ^ [] : [-(xB = sdtlbdtrb0(xt, aDimensionOf0(xt)))], (710 ^ _108752) ^ [] : [-(aScalar0(xC))], (712 ^ _108752) ^ [] : [-(xC = sdtasasdt0(xp, xp))], (714 ^ _108752) ^ [] : [-(aScalar0(xD))], (716 ^ _108752) ^ [] : [-(xD = sdtasasdt0(xq, xq))], (718 ^ _108752) ^ [] : [-(aScalar0(xE))], (720 ^ _108752) ^ [] : [-(xE = sdtasasdt0(xp, xq))], (722 ^ _108752) ^ [] : [-(aScalar0(xF))], (724 ^ _108752) ^ [] : [-(xF = sdtasdt0(xA, xA))], (726 ^ _108752) ^ [] : [-(aScalar0(xG))], (728 ^ _108752) ^ [] : [-(xG = sdtasdt0(xB, xB))], (730 ^ _108752) ^ [] : [-(aScalar0(xH))], (732 ^ _108752) ^ [] : [-(xH = sdtasdt0(xA, xB))], (734 ^ _108752) ^ [] : [-(aScalar0(xR))], (736 ^ _108752) ^ [] : [-(xR = sdtasdt0(xC, xG))], (738 ^ _108752) ^ [] : [-(aScalar0(xP))], (740 ^ _108752) ^ [] : [-(xP = sdtasdt0(xE, xH))], (742 ^ _108752) ^ [] : [-(aScalar0(xS))], (744 ^ _108752) ^ [] : [-(xS = sdtasdt0(xF, xD))], (746 ^ _108752) ^ [] : [-(aScalar0(xN))], (748 ^ _108752) ^ [] : [-(xN = sdtasdt0(xR, xS))], (750 ^ _108752) ^ [] : [-(sdtlseqdt0(sdtasdt0(xE, xE), sdtasdt0(xC, xD)))], (752 ^ _108752) ^ [] : [-(sdtlseqdt0(sdtasdt0(xP, xP), xN))], (754 ^ _108752) ^ [] : [-(sdtlseqdt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xS, xS))))], (756 ^ _108752) ^ [] : [-(sdtlseqdt0(sdtasdt0(sdtpldt0(xP, xP), sdtpldt0(xP, xP)), sdtasdt0(sdtpldt0(xR, xS), sdtpldt0(xR, xS))))], (758 ^ _108752) ^ [] : [sdtlseqdt0(sdtpldt0(xP, xP), sdtpldt0(xR, xS))], (672 ^ _108752) ^ [_129408, _129410] : [aVector0(_129410), aVector0(_129408), aDimensionOf0(_129410) = aDimensionOf0(_129408), iLess0(aDimensionOf0(_129410), aDimensionOf0(xs)), -(sdtlseqdt0(sdtasdt0(sdtasasdt0(_129410, _129408), sdtasasdt0(_129410, _129408)), sdtasdt0(sdtasasdt0(_129410, _129410), sdtasasdt0(_129408, _129408))))]], input).
% 0.37/1.39 ncf('1',plain,[sdtlseqdt0(sdtpldt0(xR, xS), sdtpldt0(xP, xP))],start(760 ^ 0)).
% 0.37/1.39 ncf('1.1',plain,[-(sdtlseqdt0(sdtpldt0(xR, xS), sdtpldt0(xP, xP))), aScalar0(sdtpldt0(xR, xS)), aScalar0(sdtpldt0(xP, xP)), -(sdtlseqdt0(sdtpldt0(xP, xP), sdtpldt0(xR, xS)))],extension(467 ^ 1,bind([[_123360, _123362], [sdtpldt0(xP, xP), sdtpldt0(xR, xS)]]))).
% 0.37/1.39 ncf('1.1.1',plain,[-(aScalar0(sdtpldt0(xR, xS))), aScalar0(xR), aScalar0(xS)],extension(225 ^ 2,bind([[_115949, _115951], [xS, xR]]))).
% 0.37/1.39 ncf('1.1.1.1',plain,[-(aScalar0(xR))],extension(734 ^ 3)).
% 0.37/1.39 ncf('1.1.1.2',plain,[-(aScalar0(xS))],extension(742 ^ 3)).
% 0.37/1.39 ncf('1.1.2',plain,[-(aScalar0(sdtpldt0(xP, xP))), aScalar0(xP), aScalar0(xP)],extension(225 ^ 2,bind([[_115949, _115951], [xP, xP]]))).
% 0.37/1.39 ncf('1.1.2.1',plain,[-(aScalar0(xP))],extension(738 ^ 3)).
% 0.37/1.39 ncf('1.1.2.2',plain,[-(aScalar0(xP))],lemmata('[1, 1].x')).
% 0.37/1.39 ncf('1.1.3',plain,[sdtlseqdt0(sdtpldt0(xP, xP), sdtpldt0(xR, xS))],extension(758 ^ 2)).
% 0.37/1.39 %-----------------------------------------------------
% 0.37/1.39 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------