%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : RNG069+1 : TPTP v8.1.2. Released v4.0.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:49:44 EDT 2023
% Result : Theorem 123.38s 120.47s
% Output : Proof 123.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.09 % Problem : RNG069+1 : TPTP v8.1.2. Released v4.0.0.
% 0.05/0.09 % Command : nanocop.sh %s %d
% 0.09/0.28 % Computer : n032.cluster.edu
% 0.09/0.28 % Model : x86_64 x86_64
% 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.28 % Memory : 8042.1875MB
% 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.28 % CPULimit : 300
% 0.09/0.28 % WCLimit : 300
% 0.09/0.28 % DateTime : Thu May 18 20:22:04 EDT 2023
% 0.09/0.28 % CPUTime :
% 123.38/120.47
% 123.38/120.47 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 123.38/120.47 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 123.38/120.47 %-----------------------------------------------------
% 123.38/120.47 ncf(matrix, plain, [(762 ^ _113026) ^ [] : [sdtlseqdt0(sdtasdt0(sdtpldt0(xP, xP), sdtpldt0(xP, xP)), sdtasdt0(sdtpldt0(xR, xS), sdtpldt0(xR, xS)))], (78 ^ _113026) ^ [_115561, _115563] : [_115563 = _115561, -(smndt0(_115563) = smndt0(_115561))], (84 ^ _113026) ^ [_115779, _115781] : [_115781 = _115779, -(szszuzczcdt0(_115781) = szszuzczcdt0(_115779))], (90 ^ _113026) ^ [_115997, _115999] : [_115999 = _115997, -(sziznziztdt0(_115999) = sziznziztdt0(_115997))], (96 ^ _113026) ^ [_116243, _116245, _116247, _116249] : [-(sdtlbdtrb0(_116249, _116245) = sdtlbdtrb0(_116247, _116243)), _116249 = _116247, _116245 = _116243], (106 ^ _113026) ^ [_116574, _116576] : [_116576 = _116574, -(aDimensionOf0(_116576) = aDimensionOf0(_116574))], (112 ^ _113026) ^ [_116820, _116822, _116824, _116826] : [-(sdtasasdt0(_116826, _116822) = sdtasasdt0(_116824, _116820)), _116826 = _116824, _116822 = _116820], (122 ^ _113026) ^ [_117179, _117181, _117183, _117185] : [-(sdtasdt0(_117185, _117181) = sdtasdt0(_117183, _117179)), _117185 = _117183, _117181 = _117179], (132 ^ _113026) ^ [_117518, _117520, _117522, _117524] : [-(sdtpldt0(_117524, _117520) = sdtpldt0(_117522, _117518)), _117524 = _117522, _117520 = _117518], (2 ^ _113026) ^ [_113170] : [-(_113170 = _113170)], (4 ^ _113026) ^ [_113277, _113279] : [_113279 = _113277, -(_113277 = _113279)], (10 ^ _113026) ^ [_113481, _113483, _113485] : [-(_113485 = _113481), _113485 = _113483, _113483 = _113481], (20 ^ _113026) ^ [_113794, _113796] : [-(aNaturalNumber0(_113794)), _113796 = _113794, aNaturalNumber0(_113796)], (30 ^ _113026) ^ [_114117, _114119, _114121, _114123] : [-(iLess0(_114121, _114117)), iLess0(_114123, _114119), _114123 = _114121, _114119 = _114117], (44 ^ _113026) ^ [_114533, _114535] : [-(aVector0(_114533)), _114535 = _114533, aVector0(_114535)], (54 ^ _113026) ^ [_114828, _114830] : [-(aScalar0(_114828)), _114830 = _114828, aScalar0(_114830)], (64 ^ _113026) ^ [_115131, _115133, _115135, _115137] : [-(sdtlseqdt0(_115135, _115131)), sdtlseqdt0(_115137, _115133), _115137 = _115135, _115133 = _115131], (142 ^ _113026) ^ [_117865] : [aNaturalNumber0(_117865), true___, -(true___)], (152 ^ _113026) ^ [] : [-(aNaturalNumber0(sz00))], (154 ^ _113026) ^ [_118173] : [aNaturalNumber0(_118173), 157 ^ _113026 : [(158 ^ _113026) ^ [] : [-(aNaturalNumber0(szszuzczcdt0(_118173)))], (160 ^ _113026) ^ [] : [szszuzczcdt0(_118173) = sz00]]], (162 ^ _113026) ^ [_118441] : [170 ^ _113026 : [(171 ^ _113026) ^ [] : [-(aNaturalNumber0(169 ^ [_118441]))], (173 ^ _113026) ^ [] : [-(_118441 = szszuzczcdt0(169 ^ [_118441]))]], aNaturalNumber0(_118441), -(_118441 = sz00)], (175 ^ _113026) ^ [_118869, _118871] : [aNaturalNumber0(_118871), aNaturalNumber0(_118869), szszuzczcdt0(_118871) = szszuzczcdt0(_118869), -(_118871 = _118869)], (189 ^ _113026) ^ [_119263, _119265] : [aNaturalNumber0(_119265), aNaturalNumber0(_119263), iLess0(_119265, _119263), true___, -(true___)], (207 ^ _113026) ^ [_119709] : [aNaturalNumber0(_119709), -(iLess0(_119709, szszuzczcdt0(_119709)))], (213 ^ _113026) ^ [_119901] : [aScalar0(_119901), true___, -(true___)], (223 ^ _113026) ^ [] : [-(aScalar0(sz0z00))], (225 ^ _113026) ^ [_120223, _120225] : [-(aScalar0(sdtpldt0(_120225, _120223))), aScalar0(_120225), aScalar0(_120223)], (235 ^ _113026) ^ [_120522, _120524] : [-(aScalar0(sdtasdt0(_120524, _120522))), aScalar0(_120524), aScalar0(_120522)], (245 ^ _113026) ^ [_120807] : [aScalar0(_120807), -(aScalar0(smndt0(_120807)))], (251 ^ _113026) ^ [_120997] : [aScalar0(_120997), 254 ^ _113026 : [(255 ^ _113026) ^ [] : [-(sdtpldt0(_120997, sz0z00) = _120997)], (257 ^ _113026) ^ [] : [-(sdtpldt0(sz0z00, _120997) = _120997)], (259 ^ _113026) ^ [] : [-(sdtasdt0(_120997, sz0z00) = sz0z00)], (261 ^ _113026) ^ [] : [-(sdtasdt0(sz0z00, _120997) = sz0z00)], (263 ^ _113026) ^ [] : [-(sdtpldt0(_120997, smndt0(_120997)) = sz0z00)], (265 ^ _113026) ^ [] : [-(sdtpldt0(smndt0(_120997), _120997) = sz0z00)], (267 ^ _113026) ^ [] : [-(smndt0(smndt0(_120997)) = _120997)], (269 ^ _113026) ^ [] : [-(smndt0(sz0z00) = sz0z00)]]], (271 ^ _113026) ^ [_121764, _121766, _121768] : [282 ^ _113026 : [(283 ^ _113026) ^ [] : [-(sdtpldt0(sdtpldt0(_121768, _121766), _121764) = sdtpldt0(_121768, sdtpldt0(_121766, _121764)))], (285 ^ _113026) ^ [] : [-(sdtpldt0(_121768, _121766) = sdtpldt0(_121766, _121768))], (287 ^ _113026) ^ [] : [-(sdtasdt0(sdtasdt0(_121768, _121766), _121764) = sdtasdt0(_121768, sdtasdt0(_121766, _121764)))], (289 ^ _113026) ^ [] : [-(sdtasdt0(_121768, _121766) = sdtasdt0(_121766, _121768))]], aScalar0(_121768), aScalar0(_121766), aScalar0(_121764)], (291 ^ _113026) ^ [_122475, _122477, _122479] : [302 ^ _113026 : [(303 ^ _113026) ^ [] : [-(sdtasdt0(_122479, sdtpldt0(_122477, _122475)) = sdtpldt0(sdtasdt0(_122479, _122477), sdtasdt0(_122479, _122475)))], (305 ^ _113026) ^ [] : [-(sdtasdt0(sdtpldt0(_122479, _122477), _122475) = sdtpldt0(sdtasdt0(_122479, _122475), sdtasdt0(_122477, _122475)))]], aScalar0(_122479), aScalar0(_122477), aScalar0(_122475)], (307 ^ _113026) ^ [_123036, _123038, _123040, _123042] : [-(sdtasdt0(sdtpldt0(_123042, _123040), sdtpldt0(_123038, _123036)) = sdtpldt0(sdtpldt0(sdtasdt0(_123042, _123038), sdtasdt0(_123042, _123036)), sdtpldt0(sdtasdt0(_123040, _123038), sdtasdt0(_123040, _123036)))), aScalar0(_123042), aScalar0(_123040), aScalar0(_123038), aScalar0(_123036)], (325 ^ _113026) ^ [_123601, _123603] : [332 ^ _113026 : [(333 ^ _113026) ^ [] : [-(sdtasdt0(_123603, smndt0(_123601)) = smndt0(sdtasdt0(_123603, _123601)))], (335 ^ _113026) ^ [] : [-(sdtasdt0(smndt0(_123603), _123601) = smndt0(sdtasdt0(_123603, _123601)))]], aScalar0(_123603), aScalar0(_123601)], (337 ^ _113026) ^ [_124011, _124013] : [-(sdtasdt0(smndt0(_124013), smndt0(_124011)) = sdtasdt0(_124013, _124011)), aScalar0(_124013), aScalar0(_124011)], (347 ^ _113026) ^ [_124326, _124328] : [aScalar0(_124328), aScalar0(_124326), sdtlseqdt0(_124328, _124326), true___, -(true___)], (365 ^ _113026) ^ [_124772] : [aScalar0(_124772), -(sdtlseqdt0(_124772, _124772))], (371 ^ _113026) ^ [_124974, _124976] : [aScalar0(_124976), aScalar0(_124974), -(_124976 = _124974), sdtlseqdt0(_124976, _124974), sdtlseqdt0(_124974, _124976)], (389 ^ _113026) ^ [_125463, _125465, _125467] : [aScalar0(_125467), aScalar0(_125465), aScalar0(_125463), -(sdtlseqdt0(_125467, _125463)), sdtlseqdt0(_125467, _125465), sdtlseqdt0(_125465, _125463)], (411 ^ _113026) ^ [_126077, _126079, _126081, _126083] : [-(sdtlseqdt0(sdtpldt0(_126083, _126079), sdtpldt0(_126081, _126077))), sdtlseqdt0(_126083, _126081), sdtlseqdt0(_126079, _126077), aScalar0(_126083), aScalar0(_126081), aScalar0(_126079), aScalar0(_126077)], (437 ^ _113026) ^ [_126820, _126822, _126824, _126826] : [aScalar0(_126826), aScalar0(_126824), aScalar0(_126822), aScalar0(_126820), -(sdtlseqdt0(sdtasdt0(_126826, _126822), sdtasdt0(_126824, _126820))), sdtlseqdt0(_126826, _126824), sdtlseqdt0(sz0z00, _126822), sdtlseqdt0(_126822, _126820)], (467 ^ _113026) ^ [_127634, _127636] : [aScalar0(_127636), aScalar0(_127634), -(sdtlseqdt0(_127636, _127634)), -(sdtlseqdt0(_127634, _127636))], (481 ^ _113026) ^ [_128021, _128023] : [aScalar0(_128023), aScalar0(_128021), 496 ^ _113026 : [(497 ^ _113026) ^ [] : [-(sdtlseqdt0(sz0z00, sdtpldt0(_128023, _128021)))], (499 ^ _113026) ^ [] : [-(sdtlseqdt0(sz0z00, sdtasdt0(_128023, _128021)))]], sdtlseqdt0(sz0z00, _128023), sdtlseqdt0(sz0z00, _128021)], (501 ^ _113026) ^ [_128569] : [aScalar0(_128569), -(sdtlseqdt0(sz0z00, sdtasdt0(_128569, _128569)))], (507 ^ _113026) ^ [_128777, _128779] : [aScalar0(_128779), aScalar0(_128777), -(_128779 = _128777), sdtlseqdt0(sz0z00, _128779), sdtlseqdt0(sz0z00, _128777), sdtasdt0(_128779, _128779) = sdtasdt0(_128777, _128777)], (529 ^ _113026) ^ [_129339] : [aVector0(_129339), true___, -(true___)], (539 ^ _113026) ^ [_129594] : [aVector0(_129594), -(aNaturalNumber0(aDimensionOf0(_129594)))], (545 ^ _113026) ^ [_129798, _129800] : [-(aScalar0(sdtlbdtrb0(_129800, _129798))), aVector0(_129800), aNaturalNumber0(_129798)], (555 ^ _113026) ^ [_130083] : [aVector0(_130083), -(aDimensionOf0(_130083) = sz00), 562 ^ _113026 : [(563 ^ _113026) ^ [_130366] : [_130366 = sziznziztdt0(_130083), 566 ^ _113026 : [(567 ^ _113026) ^ [] : [-(aVector0(_130366))], (569 ^ _113026) ^ [] : [-(szszuzczcdt0(aDimensionOf0(_130366)) = aDimensionOf0(_130083))], (571 ^ _113026) ^ [_130668] : [aNaturalNumber0(_130668), -(sdtlbdtrb0(_130366, _130668) = sdtlbdtrb0(_130083, _130668))]]], (577 ^ _113026) ^ [_130859] : [-(_130859 = sziznziztdt0(_130083)), aVector0(_130859), szszuzczcdt0(aDimensionOf0(_130859)) = aDimensionOf0(_130083), 587 ^ _113026 : [(588 ^ _113026) ^ [] : [-(aNaturalNumber0(586 ^ [_130083, _130859]))], (590 ^ _113026) ^ [] : [sdtlbdtrb0(_130859, 586 ^ [_130083, _130859]) = sdtlbdtrb0(_130083, 586 ^ [_130083, _130859])]]]]], (594 ^ _113026) ^ [_131441, _131443] : [aVector0(_131443), aVector0(_131441), -(aDimensionOf0(sziznziztdt0(_131443)) = aDimensionOf0(sziznziztdt0(_131441))), aDimensionOf0(_131443) = aDimensionOf0(_131441), -(aDimensionOf0(_131441) = sz00)], (612 ^ _113026) ^ [_131947, _131949] : [aVector0(_131949), aVector0(_131947), aDimensionOf0(_131949) = aDimensionOf0(_131947), -(aScalar0(sdtasasdt0(_131949, _131947)))], (626 ^ _113026) ^ [_132345, _132347] : [aVector0(_132347), aVector0(_132345), -(sdtasasdt0(_132347, _132345) = sz0z00), aDimensionOf0(_132347) = aDimensionOf0(_132345), aDimensionOf0(_132345) = sz00], (644 ^ _113026) ^ [_132838, _132840] : [aVector0(_132840), aVector0(_132838), -(sdtasasdt0(_132840, _132838) = sdtpldt0(sdtasasdt0(sziznziztdt0(_132840), sziznziztdt0(_132838)), sdtasdt0(sdtlbdtrb0(_132840, aDimensionOf0(_132840)), sdtlbdtrb0(_132838, aDimensionOf0(_132838))))), aDimensionOf0(_132840) = aDimensionOf0(_132838), -(aDimensionOf0(_132838) = sz00)], (662 ^ _113026) ^ [_133366] : [aVector0(_133366), -(sdtlseqdt0(sz0z00, sdtasasdt0(_133366, _133366)))], (668 ^ _113026) ^ [] : [-(aVector0(xs))], (670 ^ _113026) ^ [] : [-(aVector0(xt))], (690 ^ _113026) ^ [] : [-(aDimensionOf0(xs) = aDimensionOf0(xt))], (692 ^ _113026) ^ [] : [aDimensionOf0(xs) = sz00], (694 ^ _113026) ^ [] : [-(aVector0(xp))], (696 ^ _113026) ^ [] : [-(xp = sziznziztdt0(xs))], (698 ^ _113026) ^ [] : [-(aVector0(xq))], (700 ^ _113026) ^ [] : [-(xq = sziznziztdt0(xt))], (702 ^ _113026) ^ [] : [-(aScalar0(xA))], (704 ^ _113026) ^ [] : [-(xA = sdtlbdtrb0(xs, aDimensionOf0(xs)))], (706 ^ _113026) ^ [] : [-(aScalar0(xB))], (708 ^ _113026) ^ [] : [-(xB = sdtlbdtrb0(xt, aDimensionOf0(xt)))], (710 ^ _113026) ^ [] : [-(aScalar0(xC))], (712 ^ _113026) ^ [] : [-(xC = sdtasasdt0(xp, xp))], (714 ^ _113026) ^ [] : [-(aScalar0(xD))], (716 ^ _113026) ^ [] : [-(xD = sdtasasdt0(xq, xq))], (718 ^ _113026) ^ [] : [-(aScalar0(xE))], (720 ^ _113026) ^ [] : [-(xE = sdtasasdt0(xp, xq))], (722 ^ _113026) ^ [] : [-(aScalar0(xF))], (724 ^ _113026) ^ [] : [-(xF = sdtasdt0(xA, xA))], (726 ^ _113026) ^ [] : [-(aScalar0(xG))], (728 ^ _113026) ^ [] : [-(xG = sdtasdt0(xB, xB))], (730 ^ _113026) ^ [] : [-(aScalar0(xH))], (732 ^ _113026) ^ [] : [-(xH = sdtasdt0(xA, xB))], (734 ^ _113026) ^ [] : [-(aScalar0(xR))], (736 ^ _113026) ^ [] : [-(xR = sdtasdt0(xC, xG))], (738 ^ _113026) ^ [] : [-(aScalar0(xP))], (740 ^ _113026) ^ [] : [-(xP = sdtasdt0(xE, xH))], (742 ^ _113026) ^ [] : [-(aScalar0(xS))], (744 ^ _113026) ^ [] : [-(xS = sdtasdt0(xF, xD))], (746 ^ _113026) ^ [] : [-(aScalar0(xN))], (748 ^ _113026) ^ [] : [-(xN = sdtasdt0(xR, xS))], (750 ^ _113026) ^ [] : [-(sdtlseqdt0(sdtasdt0(xE, xE), sdtasdt0(xC, xD)))], (752 ^ _113026) ^ [] : [-(sdtlseqdt0(sdtasdt0(xP, xP), xN))], (754 ^ _113026) ^ [] : [-(sdtlseqdt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xS, xS))))], (756 ^ _113026) ^ [] : [-(sdtlseqdt0(sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtasdt0(xP, xP)), sdtasdt0(xP, xP)), sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xS, xS)), xN), xN)))], (758 ^ _113026) ^ [] : [-(sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), xN), sdtasdt0(xS, xS)), xN) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), xN), sdtpldt0(sdtasdt0(xS, xS), xN)))], (760 ^ _113026) ^ [] : [-(sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP))), sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS)))))], (672 ^ _113026) ^ [_133682, _133684] : [aVector0(_133684), aVector0(_133682), aDimensionOf0(_133684) = aDimensionOf0(_133682), iLess0(aDimensionOf0(_133684), aDimensionOf0(xs)), -(sdtlseqdt0(sdtasdt0(sdtasasdt0(_133684, _133682), sdtasasdt0(_133684, _133682)), sdtasdt0(sdtasasdt0(_133684, _133684), sdtasasdt0(_133682, _133682))))]], input).
% 123.38/120.48 ncf('1',plain,[sdtlseqdt0(sdtasdt0(sdtpldt0(xP, xP), sdtpldt0(xP, xP)), sdtasdt0(sdtpldt0(xR, xS), sdtpldt0(xR, xS)))],start(762 ^ 0)).
% 123.38/120.48 ncf('1.1',plain,[-(sdtlseqdt0(sdtasdt0(sdtpldt0(xP, xP), sdtpldt0(xP, xP)), sdtasdt0(sdtpldt0(xR, xS), sdtpldt0(xR, xS)))), sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP))), sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS)))), sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP))) = sdtasdt0(sdtpldt0(xP, xP), sdtpldt0(xP, xP)), sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS))) = sdtasdt0(sdtpldt0(xR, xS), sdtpldt0(xR, xS))],extension(64 ^ 1,bind([[_115131, _115133, _115135, _115137], [sdtasdt0(sdtpldt0(xR, xS), sdtpldt0(xR, xS)), sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS))), sdtasdt0(sdtpldt0(xP, xP), sdtpldt0(xP, xP)), sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)))]]))).
% 123.38/120.48 ncf('1.1.1',plain,[-(sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP))), sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS))))), sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP))), sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS)))), sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP))) = sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP))), sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS)))],extension(64 ^ 2,bind([[_115131, _115133, _115135, _115137], [sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS))), sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS))), sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP))), sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)))]]))).
% 123.38/120.48 ncf('1.1.1.1',plain,[-(sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP))), sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS)))))],extension(760 ^ 3)).
% 123.38/120.48 ncf('1.1.1.2',plain,[-(sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP))) = sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP))))],extension(2 ^ 3,bind([[_113170], [sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)))]]))).
% 123.38/120.48 ncf('1.1.1.3',plain,[-(sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS))))],extension(2 ^ 3,bind([[_113170], [sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS)))]]))).
% 123.38/120.48 ncf('1.1.2',plain,[-(sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP))) = sdtasdt0(sdtpldt0(xP, xP), sdtpldt0(xP, xP))), sdtasdt0(sdtpldt0(xP, xP), sdtpldt0(xP, xP)) = sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)))],extension(4 ^ 2,bind([[_113277, _113279], [sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP))), sdtasdt0(sdtpldt0(xP, xP), sdtpldt0(xP, xP))]]))).
% 123.38/120.48 ncf('1.1.2.1',plain,[-(sdtasdt0(sdtpldt0(xP, xP), sdtpldt0(xP, xP)) = sdtpldt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)))), aScalar0(xP), aScalar0(xP), aScalar0(xP), aScalar0(xP)],extension(307 ^ 3,bind([[_123036, _123038, _123040, _123042], [xP, xP, xP, xP]]))).
% 123.38/120.48 ncf('1.1.2.1.1',plain,[-(aScalar0(xP))],extension(738 ^ 4)).
% 123.38/120.48 ncf('1.1.2.1.2',plain,[-(aScalar0(xP))],lemmata('[2, 1, 1].x')).
% 123.38/120.48 ncf('1.1.2.1.3',plain,[-(aScalar0(xP))],lemmata('[2, 1, 1].x')).
% 123.38/120.48 ncf('1.1.2.1.4',plain,[-(aScalar0(xP))],lemmata('[2, 1, 1].x')).
% 123.38/120.48 ncf('1.1.3',plain,[-(sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS))) = sdtasdt0(sdtpldt0(xR, xS), sdtpldt0(xR, xS))), sdtasdt0(sdtpldt0(xR, xS), sdtpldt0(xR, xS)) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS)))],extension(4 ^ 2,bind([[_113277, _113279], [sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS))), sdtasdt0(sdtpldt0(xR, xS), sdtpldt0(xR, xS))]]))).
% 123.38/120.48 ncf('1.1.3.1',plain,[-(sdtasdt0(sdtpldt0(xR, xS), sdtpldt0(xR, xS)) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xR, xS)), sdtpldt0(sdtasdt0(xS, xR), sdtasdt0(xS, xS)))), aScalar0(xR), aScalar0(xS), aScalar0(xR), aScalar0(xS)],extension(307 ^ 3,bind([[_123036, _123038, _123040, _123042], [xS, xR, xS, xR]]))).
% 123.38/120.48 ncf('1.1.3.1.1',plain,[-(aScalar0(xR))],extension(734 ^ 4)).
% 123.38/120.48 ncf('1.1.3.1.2',plain,[-(aScalar0(xS))],extension(742 ^ 4)).
% 123.38/120.48 ncf('1.1.3.1.3',plain,[-(aScalar0(xR))],lemmata('[3, 1, 1].x')).
% 123.38/120.48 ncf('1.1.3.1.4',plain,[-(aScalar0(xS))],lemmata('[3, 1, 1].x')).
% 123.38/120.48 %-----------------------------------------------------
% 123.38/120.48 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------