%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM432+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n011.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:44:37 EDT 2023
% Result : Theorem 4.54s 5.51s
% Output : Proof 4.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM432+3 : TPTP v8.1.2. Released v4.0.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n011.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 18 17:00:48 EDT 2023
% 0.12/0.33 % CPUTime :
% 4.54/5.51
% 4.54/5.51 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 4.54/5.51 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.54/5.51 %-----------------------------------------------------
% 4.54/5.51 ncf(matrix, plain, [(393 ^ _73512) ^ [] : [aDivisorOf0(xq, sdtpldt0(xa, smndt0(xc)))], (395 ^ _73512) ^ [] : [sdteqdtlpzmzozddtrp0(xa, xc, xq)], (387 ^ _73512) ^ [_85774] : [aInteger0(_85774), sdtasdt0(xq, _85774) = sdtpldt0(xa, smndt0(xc))], (62 ^ _73512) ^ [_75646, _75648, _75650, _75652] : [-(sdtasdt0(_75652, _75648) = sdtasdt0(_75650, _75646)), _75652 = _75650, _75648 = _75646], (82 ^ _73512) ^ [_76316, _76318] : [_76318 = _76316, -(smndt0(_76318) = smndt0(_76316))], (72 ^ _73512) ^ [_76005, _76007, _76009, _76011] : [-(sdtpldt0(_76011, _76007) = sdtpldt0(_76009, _76005)), _76011 = _76009, _76007 = _76005], (2 ^ _73512) ^ [_73656] : [-(_73656 = _73656)], (4 ^ _73512) ^ [_73763, _73765] : [_73765 = _73763, -(_73763 = _73765)], (10 ^ _73512) ^ [_73967, _73969, _73971] : [-(_73971 = _73967), _73971 = _73969, _73969 = _73967], (20 ^ _73512) ^ [_74280, _74282] : [-(aInteger0(_74280)), _74282 = _74280, aInteger0(_74282)], (30 ^ _73512) ^ [_74603, _74605, _74607, _74609] : [-(aDivisorOf0(_74607, _74603)), aDivisorOf0(_74609, _74605), _74609 = _74607, _74605 = _74603], (44 ^ _73512) ^ [_75055, _75057, _75059, _75061, _75063, _75065] : [-(sdteqdtlpzmzozddtrp0(_75063, _75059, _75055)), sdteqdtlpzmzozddtrp0(_75065, _75061, _75057), _75065 = _75063, _75061 = _75059, _75057 = _75055], (88 ^ _73512) ^ [_76530] : [aInteger0(_76530), true___, -(true___)], (98 ^ _73512) ^ [] : [-(aInteger0(sz00))], (100 ^ _73512) ^ [] : [-(aInteger0(sz10))], (102 ^ _73512) ^ [_76891] : [aInteger0(_76891), -(aInteger0(smndt0(_76891)))], (108 ^ _73512) ^ [_77095, _77097] : [-(aInteger0(sdtpldt0(_77097, _77095))), aInteger0(_77097), aInteger0(_77095)], (118 ^ _73512) ^ [_77394, _77396] : [-(aInteger0(sdtasdt0(_77396, _77394))), aInteger0(_77396), aInteger0(_77394)], (128 ^ _73512) ^ [_77707, _77709, _77711] : [-(sdtpldt0(_77711, sdtpldt0(_77709, _77707)) = sdtpldt0(sdtpldt0(_77711, _77709), _77707)), aInteger0(_77711), aInteger0(_77709), aInteger0(_77707)], (142 ^ _73512) ^ [_78127, _78129] : [-(sdtpldt0(_78129, _78127) = sdtpldt0(_78127, _78129)), aInteger0(_78129), aInteger0(_78127)], (152 ^ _73512) ^ [_78420] : [aInteger0(_78420), 155 ^ _73512 : [(156 ^ _73512) ^ [] : [-(sdtpldt0(_78420, sz00) = _78420)], (158 ^ _73512) ^ [] : [-(_78420 = sdtpldt0(sz00, _78420))]]], (160 ^ _73512) ^ [_78693] : [aInteger0(_78693), 163 ^ _73512 : [(164 ^ _73512) ^ [] : [-(sdtpldt0(_78693, smndt0(_78693)) = sz00)], (166 ^ _73512) ^ [] : [-(sz00 = sdtpldt0(smndt0(_78693), _78693))]]], (168 ^ _73512) ^ [_79002, _79004, _79006] : [-(sdtasdt0(_79006, sdtasdt0(_79004, _79002)) = sdtasdt0(sdtasdt0(_79006, _79004), _79002)), aInteger0(_79006), aInteger0(_79004), aInteger0(_79002)], (182 ^ _73512) ^ [_79422, _79424] : [-(sdtasdt0(_79424, _79422) = sdtasdt0(_79422, _79424)), aInteger0(_79424), aInteger0(_79422)], (192 ^ _73512) ^ [_79715] : [aInteger0(_79715), 195 ^ _73512 : [(196 ^ _73512) ^ [] : [-(sdtasdt0(_79715, sz10) = _79715)], (198 ^ _73512) ^ [] : [-(_79715 = sdtasdt0(sz10, _79715))]]], (200 ^ _73512) ^ [_80016, _80018, _80020] : [211 ^ _73512 : [(212 ^ _73512) ^ [] : [-(sdtasdt0(_80020, sdtpldt0(_80018, _80016)) = sdtpldt0(sdtasdt0(_80020, _80018), sdtasdt0(_80020, _80016)))], (214 ^ _73512) ^ [] : [-(sdtasdt0(sdtpldt0(_80020, _80018), _80016) = sdtpldt0(sdtasdt0(_80020, _80016), sdtasdt0(_80018, _80016)))]], aInteger0(_80020), aInteger0(_80018), aInteger0(_80016)], (216 ^ _73512) ^ [_80535] : [aInteger0(_80535), 219 ^ _73512 : [(220 ^ _73512) ^ [] : [-(sdtasdt0(_80535, sz00) = sz00)], (222 ^ _73512) ^ [] : [-(sz00 = sdtasdt0(sz00, _80535))]]], (224 ^ _73512) ^ [_80808] : [aInteger0(_80808), 227 ^ _73512 : [(228 ^ _73512) ^ [] : [-(sdtasdt0(smndt0(sz10), _80808) = smndt0(_80808))], (230 ^ _73512) ^ [] : [-(smndt0(_80808) = sdtasdt0(_80808, smndt0(sz10)))]]], (232 ^ _73512) ^ [_81103, _81105] : [aInteger0(_81105), aInteger0(_81103), sdtasdt0(_81105, _81103) = sz00, -(_81105 = sz00), -(_81103 = sz00)], (250 ^ _73512) ^ [_81571] : [aInteger0(_81571), 253 ^ _73512 : [(254 ^ _73512) ^ [_81757] : [aDivisorOf0(_81757, _81571), 257 ^ _73512 : [(258 ^ _73512) ^ [] : [-(aInteger0(_81757))], (260 ^ _73512) ^ [] : [_81757 = sz00], (263 ^ _73512) ^ [] : [-(aInteger0(261 ^ [_81571, _81757]))], (265 ^ _73512) ^ [] : [-(sdtasdt0(_81757, 261 ^ [_81571, _81757]) = _81571)]]], (267 ^ _73512) ^ [_82219] : [-(aDivisorOf0(_82219, _81571)), aInteger0(_82219), -(_82219 = sz00), 276 ^ _73512 : [(277 ^ _73512) ^ [_82486] : [aInteger0(_82486), sdtasdt0(_82219, _82486) = _81571]]]]], (285 ^ _73512) ^ [_82789, _82791, _82793] : [aInteger0(_82793), aInteger0(_82791), aInteger0(_82789), -(_82789 = sz00), 300 ^ _73512 : [(301 ^ _73512) ^ [] : [sdteqdtlpzmzozddtrp0(_82793, _82791, _82789), -(aDivisorOf0(_82789, sdtpldt0(_82793, smndt0(_82791))))], (307 ^ _73512) ^ [] : [aDivisorOf0(_82789, sdtpldt0(_82793, smndt0(_82791))), -(sdteqdtlpzmzozddtrp0(_82793, _82791, _82789))]]], (313 ^ _73512) ^ [_83565, _83567] : [-(sdteqdtlpzmzozddtrp0(_83567, _83567, _83565)), aInteger0(_83567), aInteger0(_83565), -(_83565 = sz00)], (349 ^ _73512) ^ [] : [-(aInteger0(xa))], (351 ^ _73512) ^ [] : [-(aInteger0(xb))], (353 ^ _73512) ^ [] : [-(aInteger0(xq))], (355 ^ _73512) ^ [] : [xq = sz00], (357 ^ _73512) ^ [] : [-(aInteger0(xc))], (360 ^ _73512) ^ [] : [-(aInteger0(358 ^ []))], (362 ^ _73512) ^ [] : [-(sdtasdt0(xq, 358 ^ []) = sdtpldt0(xa, smndt0(xb)))], (364 ^ _73512) ^ [] : [-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))))], (366 ^ _73512) ^ [] : [-(sdteqdtlpzmzozddtrp0(xa, xb, xq))], (369 ^ _73512) ^ [] : [-(aInteger0(367 ^ []))], (371 ^ _73512) ^ [] : [-(sdtasdt0(xq, 367 ^ []) = sdtpldt0(xb, smndt0(xc)))], (373 ^ _73512) ^ [] : [-(aDivisorOf0(xq, sdtpldt0(xb, smndt0(xc))))], (375 ^ _73512) ^ [] : [-(sdteqdtlpzmzozddtrp0(xb, xc, xq))], (377 ^ _73512) ^ [] : [-(aInteger0(xn))], (379 ^ _73512) ^ [] : [-(sdtasdt0(xq, xn) = sdtpldt0(xa, smndt0(xb)))], (381 ^ _73512) ^ [] : [-(aInteger0(xm))], (383 ^ _73512) ^ [] : [-(sdtasdt0(xq, xm) = sdtpldt0(xb, smndt0(xc)))], (385 ^ _73512) ^ [] : [-(sdtasdt0(xq, sdtpldt0(xn, xm)) = sdtpldt0(xa, smndt0(xc)))], (327 ^ _73512) ^ [_83968, _83970, _83972] : [sdteqdtlpzmzozddtrp0(_83972, _83970, _83968), -(sdteqdtlpzmzozddtrp0(_83970, _83972, _83968)), aInteger0(_83972), aInteger0(_83970), aInteger0(_83968), -(_83968 = sz00)]], input).
% 4.54/5.51 ncf('1',plain,[aInteger0(sz00), 254 : aDivisorOf0(xq, sz00), 260 : xq = sz00],start(250 ^ 0,bind([[_81571, _81757], [sz00, xq]]))).
% 4.54/5.51 ncf('1.1',plain,[-(aInteger0(sz00))],extension(98 ^ 1)).
% 4.54/5.51 ncf('1.2',plain,[-(aDivisorOf0(xq, sz00)), aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))), xq = xq, sdtpldt0(xa, smndt0(xb)) = sz00],extension(30 ^ 3,bind([[_74603, _74605, _74607, _74609], [sz00, sdtpldt0(xa, smndt0(xb)), xq, xq]]))).
% 4.54/5.51 ncf('1.2.1',plain,[-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb)))), aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))), xq = xq, sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))],extension(30 ^ 4,bind([[_74603, _74605, _74607, _74609], [sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb)), xq, xq]]))).
% 4.54/5.51 ncf('1.2.1.1',plain,[-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb)))), aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))), xq = xq, sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))],extension(30 ^ 5,bind([[_74603, _74605, _74607, _74609], [sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb)), xq, xq]]))).
% 4.54/5.51 ncf('1.2.1.1.1',plain,[-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb)))), aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))), xq = xq, sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))],extension(30 ^ 6,bind([[_74603, _74605, _74607, _74609], [sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb)), xq, xq]]))).
% 4.54/5.51 ncf('1.2.1.1.1.1',plain,[-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb)))), aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))), xq = xq, sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))],extension(30 ^ 7,bind([[_74603, _74605, _74607, _74609], [sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb)), xq, xq]]))).
% 4.54/5.51 ncf('1.2.1.1.1.1.1',plain,[-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb)))), 301 : sdteqdtlpzmzozddtrp0(xa, xb, xq), 301 : aInteger0(xa), 301 : aInteger0(xb), 301 : aInteger0(xq), 301 : -(xq = sz00)],extension(285 ^ 8,bind([[_82789, _82791, _82793], [xq, xb, xa]]))).
% 4.54/5.51 ncf('1.2.1.1.1.1.1.1',plain,[-(sdteqdtlpzmzozddtrp0(xa, xb, xq))],extension(366 ^ 11)).
% 4.54/5.51 ncf('1.2.1.1.1.1.1.2',plain,[-(aInteger0(xa))],extension(349 ^ 9)).
% 4.54/5.51 ncf('1.2.1.1.1.1.1.3',plain,[-(aInteger0(xb))],extension(351 ^ 9)).
% 4.54/5.51 ncf('1.2.1.1.1.1.1.4',plain,[-(aInteger0(xq))],extension(353 ^ 9)).
% 4.54/5.51 ncf('1.2.1.1.1.1.1.5',plain,[xq = sz00],extension(355 ^ 9)).
% 4.54/5.51 ncf('1.2.1.1.1.1.2',plain,[-(xq = xq)],extension(2 ^ 8,bind([[_73656], [xq]]))).
% 4.54/5.51 ncf('1.2.1.1.1.1.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb)))],extension(2 ^ 8,bind([[_73656], [sdtpldt0(xa, smndt0(xb))]]))).
% 4.54/5.51 ncf('1.2.1.1.1.2',plain,[-(xq = xq)],extension(2 ^ 7,bind([[_73656], [xq]]))).
% 4.54/5.51 ncf('1.2.1.1.1.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))), xa = xa, smndt0(xb) = smndt0(xb)],extension(72 ^ 7,bind([[_76005, _76007, _76009, _76011], [smndt0(xb), smndt0(xb), xa, xa]]))).
% 4.54/5.51 ncf('1.2.1.1.1.3.1',plain,[-(xa = xa)],extension(2 ^ 8,bind([[_73656], [xa]]))).
% 4.54/5.51 ncf('1.2.1.1.1.3.2',plain,[-(smndt0(xb) = smndt0(xb))],extension(2 ^ 8,bind([[_73656], [smndt0(xb)]]))).
% 4.54/5.51 ncf('1.2.1.1.2',plain,[-(xq = xq)],extension(2 ^ 6,bind([[_73656], [xq]]))).
% 4.54/5.51 ncf('1.2.1.1.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))), xa = xa, smndt0(xb) = smndt0(xb)],extension(72 ^ 6,bind([[_76005, _76007, _76009, _76011], [smndt0(xb), smndt0(xb), xa, xa]]))).
% 4.54/5.51 ncf('1.2.1.1.3.1',plain,[-(xa = xa)],extension(2 ^ 7,bind([[_73656], [xa]]))).
% 4.54/5.51 ncf('1.2.1.1.3.2',plain,[-(smndt0(xb) = smndt0(xb)), xb = xb],extension(82 ^ 7,bind([[_76316, _76318], [xb, xb]]))).
% 4.54/5.51 ncf('1.2.1.1.3.2.1',plain,[-(xb = xb)],extension(2 ^ 8,bind([[_73656], [xb]]))).
% 4.54/5.51 ncf('1.2.1.2',plain,[-(xq = xq)],extension(2 ^ 5,bind([[_73656], [xq]]))).
% 4.54/5.51 ncf('1.2.1.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))), xa = xa, smndt0(xb) = smndt0(xb)],extension(72 ^ 5,bind([[_76005, _76007, _76009, _76011], [smndt0(xb), smndt0(xb), xa, xa]]))).
% 4.54/5.51 ncf('1.2.1.3.1',plain,[-(xa = xa)],extension(2 ^ 6,bind([[_73656], [xa]]))).
% 4.54/5.51 ncf('1.2.1.3.2',plain,[-(smndt0(xb) = smndt0(xb)), xb = xb],extension(82 ^ 6,bind([[_76316, _76318], [xb, xb]]))).
% 4.54/5.51 ncf('1.2.1.3.2.1',plain,[-(xb = xb)],extension(2 ^ 7,bind([[_73656], [xb]]))).
% 4.54/5.51 ncf('1.2.2',plain,[-(xq = xq)],extension(2 ^ 4,bind([[_73656], [xq]]))).
% 4.54/5.51 ncf('1.2.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sz00), aInteger0(sdtpldt0(xa, smndt0(xb))), aInteger0(sz00), sdtasdt0(sdtpldt0(xa, smndt0(xb)), sz00) = sz00, -(sz00 = sz00)],extension(232 ^ 4,bind([[_81103, _81105], [sz00, sdtpldt0(xa, smndt0(xb))]]))).
% 4.54/5.51 ncf('1.2.3.1',plain,[-(aInteger0(sdtpldt0(xa, smndt0(xb)))), aInteger0(xa), aInteger0(smndt0(xb))],extension(108 ^ 5,bind([[_77095, _77097], [smndt0(xb), xa]]))).
% 4.54/5.51 ncf('1.2.3.1.1',plain,[-(aInteger0(xa))],extension(349 ^ 6)).
% 4.54/5.51 ncf('1.2.3.1.2',plain,[-(aInteger0(smndt0(xb))), aInteger0(xb)],extension(102 ^ 6,bind([[_76891], [xb]]))).
% 4.54/5.51 ncf('1.2.3.1.2.1',plain,[-(aInteger0(xb))],extension(351 ^ 7)).
% 4.54/5.51 ncf('1.2.3.2',plain,[-(aInteger0(sz00))],extension(98 ^ 5)).
% 4.54/5.51 ncf('1.2.3.3',plain,[-(sdtasdt0(sdtpldt0(xa, smndt0(xb)), sz00) = sz00), aInteger0(sdtpldt0(xa, smndt0(xb)))],extension(216 ^ 5,bind([[_80535], [sdtpldt0(xa, smndt0(xb))]]))).
% 4.54/5.51 ncf('1.2.3.3.1',plain,[-(aInteger0(sdtpldt0(xa, smndt0(xb))))],lemmata('[2, 1].x')).
% 4.54/5.51 ncf('1.2.3.4',plain,[sz00 = sz00, -(sdtasdt0(xq, sz00) = sdtasdt0(sz00, sz00)), xq = sz00],extension(62 ^ 5,bind([[_75646, _75648, _75650, _75652], [sz00, sz00, sz00, xq]]))).
% 4.54/5.51 ncf('1.2.3.4.1',plain,[sdtasdt0(xq, sz00) = sdtasdt0(sz00, sz00), 277 : aInteger0(sz00), 277 : -(aDivisorOf0(xq, sdtasdt0(sz00, sz00))), 277 : aInteger0(xq), 277 : -(xq = sz00), 267 : aInteger0(sdtasdt0(sz00, sz00))],extension(250 ^ 6,bind([[_81571, _82219, _82486], [sdtasdt0(sz00, sz00), xq, sz00]]))).
% 4.54/5.51 ncf('1.2.3.4.1.1',plain,[-(aInteger0(sz00))],lemmata('[2, 1].x')).
% 4.54/5.51 ncf('1.2.3.4.1.2',plain,[aDivisorOf0(xq, sdtasdt0(sz00, sz00)), -(aDivisorOf0(xq, sz00)), xq = xq, sdtasdt0(sz00, sz00) = sz00],extension(30 ^ 9,bind([[_74603, _74605, _74607, _74609], [sz00, sdtasdt0(sz00, sz00), xq, xq]]))).
% 4.54/5.51 ncf('1.2.3.4.1.2.1',plain,[aDivisorOf0(xq, sz00)],reduction('1')).
% 4.54/5.51 ncf('1.2.3.4.1.2.2',plain,[-(xq = xq)],extension(2 ^ 10,bind([[_73656], [xq]]))).
% 4.54/5.51 ncf('1.2.3.4.1.2.3',plain,[-(sdtasdt0(sz00, sz00) = sz00), aInteger0(sz00)],extension(216 ^ 10,bind([[_80535], [sz00]]))).
% 4.54/5.51 ncf('1.2.3.4.1.2.3.1',plain,[-(aInteger0(sz00))],extension(98 ^ 11)).
% 4.54/5.51 ncf('1.2.3.4.1.3',plain,[-(aInteger0(xq)), 254 : aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))), 254 : aInteger0(sdtpldt0(xa, smndt0(xb)))],extension(250 ^ 9,bind([[_81571, _81757], [sdtpldt0(xa, smndt0(xb)), xq]]))).
% 4.54/5.51 ncf('1.2.3.4.1.3.1',plain,[-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))))],extension(364 ^ 12)).
% 4.54/5.51 ncf('1.2.3.4.1.3.2',plain,[-(aInteger0(sdtpldt0(xa, smndt0(xb))))],lemmata('[2, 1].x')).
% 4.54/5.51 ncf('1.2.3.4.1.4',plain,[xq = sz00, -(xq = xq), sz00 = xq],extension(10 ^ 9,bind([[_73967, _73969, _73971], [xq, sz00, xq]]))).
% 4.54/5.51 ncf('1.2.3.4.1.4.1',plain,[xq = xq, -(xq = sz00), xq = sz00],extension(10 ^ 10,bind([[_73967, _73969, _73971], [sz00, xq, xq]]))).
% 4.54/5.51 ncf('1.2.3.4.1.4.1.1',plain,[xq = sz00],extension(355 ^ 11)).
% 4.54/5.51 ncf('1.2.3.4.1.4.1.2',plain,[-(xq = sz00)],reduction('1.2.3.4.1')).
% 4.54/5.51 ncf('1.2.3.4.1.4.2',plain,[-(sz00 = xq), xq = sz00],extension(4 ^ 10,bind([[_73763, _73765], [sz00, xq]]))).
% 4.54/5.51 ncf('1.2.3.4.1.4.2.1',plain,[-(xq = sz00)],reduction('1.2.3.4.1')).
% 4.54/5.51 ncf('1.2.3.4.1.5',plain,[-(aInteger0(sdtasdt0(sz00, sz00))), sdtasdt0(xq, sz00) = sdtasdt0(sz00, sz00), aInteger0(sdtasdt0(xq, sz00))],extension(20 ^ 7,bind([[_74280, _74282], [sdtasdt0(sz00, sz00), sdtasdt0(xq, sz00)]]))).
% 4.54/5.51 ncf('1.2.3.4.1.5.1',plain,[-(sdtasdt0(xq, sz00) = sdtasdt0(sz00, sz00))],reduction('1.2.3.4')).
% 4.54/5.51 ncf('1.2.3.4.1.5.2',plain,[-(aInteger0(sdtasdt0(xq, sz00))), aInteger0(xq), aInteger0(sz00)],extension(118 ^ 8,bind([[_77394, _77396], [sz00, xq]]))).
% 4.54/5.51 ncf('1.2.3.4.1.5.2.1',plain,[-(aInteger0(xq))],extension(353 ^ 9)).
% 4.54/5.51 ncf('1.2.3.4.1.5.2.2',plain,[-(aInteger0(sz00))],lemmata('[2, 1].x')).
% 4.54/5.51 ncf('1.2.3.4.2',plain,[-(xq = sz00), -(aDivisorOf0(xq, sz00)), aInteger0(xq), 277 : aInteger0(sz00), 277 : sdtasdt0(xq, sz00) = sz00],extension(267 ^ 6,bind([[_82219, _82486], [xq, sz00]]))).
% 4.54/5.51 ncf('1.2.3.4.2.1',plain,[aDivisorOf0(xq, sz00)],reduction('1')).
% 4.54/5.51 ncf('1.2.3.4.2.2',plain,[-(aInteger0(xq)), 254 : aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))), 254 : aInteger0(sdtpldt0(xa, smndt0(xb)))],extension(250 ^ 7,bind([[_81571, _81757], [sdtpldt0(xa, smndt0(xb)), xq]]))).
% 4.54/5.51 ncf('1.2.3.4.2.2.1',plain,[-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))))],extension(364 ^ 10)).
% 4.54/5.51 ncf('1.2.3.4.2.2.2',plain,[-(aInteger0(sdtpldt0(xa, smndt0(xb))))],lemmata('[2, 1].x')).
% 4.54/5.51 ncf('1.2.3.4.2.3',plain,[-(aInteger0(sz00))],extension(98 ^ 9)).
% 4.54/5.51 ncf('1.2.3.4.2.4',plain,[-(sdtasdt0(xq, sz00) = sz00), aInteger0(xq)],extension(216 ^ 9,bind([[_80535], [xq]]))).
% 4.54/5.51 ncf('1.2.3.4.2.4.1',plain,[-(aInteger0(xq))],lemmata('[4, 3, 2, 1].x')).
% 4.54/5.51 ncf('1.3',plain,[-(xq = sz00), aInteger0(xq), aInteger0(sz00), sdtasdt0(xq, sz00) = sz00, -(sz00 = sz00)],extension(232 ^ 5,bind([[_81103, _81105], [sz00, xq]]))).
% 4.54/5.51 ncf('1.3.1',plain,[-(aInteger0(xq))],extension(258 ^ 6)).
% 4.54/5.51 ncf('1.3.2',plain,[-(aInteger0(sz00))],extension(98 ^ 6)).
% 4.54/5.51 ncf('1.3.3',plain,[-(sdtasdt0(xq, sz00) = sz00), aInteger0(xq)],extension(216 ^ 6,bind([[_80535], [xq]]))).
% 4.54/5.51 ncf('1.3.3.1',plain,[-(aInteger0(xq))],lemmata('[1].x')).
% 4.54/5.51 ncf('1.3.4',plain,[sz00 = sz00, -(sdtasdt0(sdtpldt0(xn, xm), sz00) = sdtasdt0(sdtpldt0(xn, xm), sz00)), sdtpldt0(xn, xm) = sdtpldt0(xn, xm)],extension(62 ^ 6,bind([[_75646, _75648, _75650, _75652], [sz00, sz00, sdtpldt0(xn, xm), sdtpldt0(xn, xm)]]))).
% 4.54/5.51 ncf('1.3.4.1',plain,[sdtasdt0(sdtpldt0(xn, xm), sz00) = sdtasdt0(sdtpldt0(xn, xm), sz00), 277 : aInteger0(sz00), 277 : -(aDivisorOf0(sdtpldt0(xn, xm), sdtasdt0(sdtpldt0(xn, xm), sz00))), 277 : aInteger0(sdtpldt0(xn, xm)), 277 : -(sdtpldt0(xn, xm) = sz00), 267 : aInteger0(sdtasdt0(sdtpldt0(xn, xm), sz00))],extension(250 ^ 7,bind([[_81571, _82219, _82486], [sdtasdt0(sdtpldt0(xn, xm), sz00), sdtpldt0(xn, xm), sz00]]))).
% 4.54/5.51 ncf('1.3.4.1.1',plain,[-(aInteger0(sz00))],lemmata('[1].x')).
% 4.54/5.51 ncf('1.3.4.1.2',plain,[aDivisorOf0(sdtpldt0(xn, xm), sdtasdt0(sdtpldt0(xn, xm), sz00)), 258 : -(aInteger0(sdtpldt0(xn, xm)))],extension(254 ^ 10,bind([[_81757], [sdtpldt0(xn, xm)]]))).
% 4.54/5.51 ncf('1.3.4.1.2.1',plain,[aInteger0(sdtpldt0(xn, xm)), sdtasdt0(xq, sdtpldt0(xn, xm)) = sdtpldt0(xa, smndt0(xc))],extension(387 ^ 13,bind([[_85774], [sdtpldt0(xn, xm)]]))).
% 4.54/5.51 ncf('1.3.4.1.2.1.1',plain,[-(sdtasdt0(xq, sdtpldt0(xn, xm)) = sdtpldt0(xa, smndt0(xc)))],extension(385 ^ 14)).
% 4.54/5.51 ncf('1.3.4.1.3',plain,[-(aInteger0(sdtpldt0(xn, xm))), aInteger0(xn), aInteger0(xm)],extension(108 ^ 10,bind([[_77095, _77097], [xm, xn]]))).
% 4.54/5.51 ncf('1.3.4.1.3.1',plain,[-(aInteger0(xn))],extension(377 ^ 11)).
% 4.54/5.51 ncf('1.3.4.1.3.2',plain,[-(aInteger0(xm))],extension(381 ^ 11)).
% 4.54/5.51 ncf('1.3.4.1.4',plain,[sdtpldt0(xn, xm) = sz00, -(sz00 = sdtpldt0(xn, xm))],extension(4 ^ 10,bind([[_73763, _73765], [sz00, sdtpldt0(xn, xm)]]))).
% 4.54/5.51 ncf('1.3.4.1.4.1',plain,[sz00 = sdtpldt0(xn, xm), -(aInteger0(sdtpldt0(xn, xm))), aInteger0(sz00)],extension(20 ^ 11,bind([[_74280, _74282], [sdtpldt0(xn, xm), sz00]]))).
% 4.54/5.51 ncf('1.3.4.1.4.1.1',plain,[aInteger0(sdtpldt0(xn, xm)), sdtasdt0(xq, sdtpldt0(xn, xm)) = sdtpldt0(xa, smndt0(xc))],extension(387 ^ 12,bind([[_85774], [sdtpldt0(xn, xm)]]))).
% 4.54/5.51 ncf('1.3.4.1.4.1.1.1',plain,[-(sdtasdt0(xq, sdtpldt0(xn, xm)) = sdtpldt0(xa, smndt0(xc)))],extension(385 ^ 13)).
% 4.54/5.51 ncf('1.3.4.1.4.1.2',plain,[-(aInteger0(sz00))],lemmata('[1].x')).
% 4.54/5.51 ncf('1.3.4.1.5',plain,[-(aInteger0(sdtasdt0(sdtpldt0(xn, xm), sz00))), sdtasdt0(sdtpldt0(xn, xm), sz00) = sdtasdt0(sdtpldt0(xn, xm), sz00), aInteger0(sdtasdt0(sdtpldt0(xn, xm), sz00))],extension(20 ^ 8,bind([[_74280, _74282], [sdtasdt0(sdtpldt0(xn, xm), sz00), sdtasdt0(sdtpldt0(xn, xm), sz00)]]))).
% 4.54/5.51 ncf('1.3.4.1.5.1',plain,[-(sdtasdt0(sdtpldt0(xn, xm), sz00) = sdtasdt0(sdtpldt0(xn, xm), sz00))],reduction('1.3.4')).
% 4.54/5.51 ncf('1.3.4.1.5.2',plain,[-(aInteger0(sdtasdt0(sdtpldt0(xn, xm), sz00))), aInteger0(sdtpldt0(xn, xm)), aInteger0(sz00)],extension(118 ^ 9,bind([[_77394, _77396], [sz00, sdtpldt0(xn, xm)]]))).
% 4.54/5.51 ncf('1.3.4.1.5.2.1',plain,[-(aInteger0(sdtpldt0(xn, xm))), aInteger0(xn), aInteger0(xm)],extension(108 ^ 10,bind([[_77095, _77097], [xm, xn]]))).
% 4.54/5.51 ncf('1.3.4.1.5.2.1.1',plain,[-(aInteger0(xn))],extension(377 ^ 11)).
% 4.54/5.51 ncf('1.3.4.1.5.2.1.2',plain,[-(aInteger0(xm))],extension(381 ^ 11)).
% 4.54/5.51 ncf('1.3.4.1.5.2.2',plain,[-(aInteger0(sz00))],lemmata('[1].x')).
% 4.54/5.51 ncf('1.3.4.2',plain,[-(sdtpldt0(xn, xm) = sdtpldt0(xn, xm)), xn = xn, xm = xm],extension(72 ^ 7,bind([[_76005, _76007, _76009, _76011], [xm, xm, xn, xn]]))).
% 4.54/5.51 ncf('1.3.4.2.1',plain,[-(xn = xn)],extension(2 ^ 8,bind([[_73656], [xn]]))).
% 4.54/5.51 ncf('1.3.4.2.2',plain,[-(xm = xm)],extension(2 ^ 8,bind([[_73656], [xm]]))).
% 4.54/5.51 %-----------------------------------------------------
% 4.54/5.51 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------