%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM435+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n027.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 161.41s 158.57s
% Output : Proof 161.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM435+1 : TPTP v8.1.2. Released v4.0.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n027.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 18 17:43:35 EDT 2023
% 0.13/0.34 % CPUTime :
% 161.41/158.57
% 161.41/158.57 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 161.41/158.57 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 161.41/158.57 %-----------------------------------------------------
% 161.41/158.57 ncf(matrix, plain, [(397 ^ _82150) ^ [] : [sdtpldt0(xa, smndt0(xb)) = sdtasdt0(xq, sdtasdt0(xp, xm))], !, (98 ^ _69764) ^ [] : [-(aInteger0(sz00))], (10 ^ _69764) ^ [_70199, _70201, _70203] : [-(_70203 = _70199), _70203 = _70201, _70201 = _70199], (216 ^ _69764) ^ [_76767] : [aInteger0(_76767), 219 ^ _69764 : [(222 ^ _69764) ^ [] : [-(sz00 = sdtasdt0(sz00, _76767))], (220 ^ _69764) ^ [] : [-(sdtasdt0(_76767, sz00) = sz00)]]], (200 ^ _69764) ^ [_76248, _76250, _76252] : [211 ^ _69764 : [(214 ^ _69764) ^ [] : [-(sdtasdt0(sdtpldt0(_76252, _76250), _76248) = sdtpldt0(sdtasdt0(_76252, _76248), sdtasdt0(_76250, _76248)))], (212 ^ _69764) ^ [] : [-(sdtasdt0(_76252, sdtpldt0(_76250, _76248)) = sdtpldt0(sdtasdt0(_76252, _76250), sdtasdt0(_76252, _76248)))]], aInteger0(_76252), aInteger0(_76250), aInteger0(_76248)], (100 ^ _69764) ^ [] : [-(aInteger0(sz10))], (108 ^ _69764) ^ [_73327, _73329] : [-(aInteger0(sdtpldt0(_73329, _73327))), aInteger0(_73329), aInteger0(_73327)], (182 ^ _69764) ^ [_75654, _75656] : [-(sdtasdt0(_75656, _75654) = sdtasdt0(_75654, _75656)), aInteger0(_75656), aInteger0(_75654)], (389 ^ _69764) ^ [] : [xq = sz00], (391 ^ _69764) ^ [] : [-(sdteqdtlpzmzozddtrp0(xa, xb, sdtasdt0(xp, xq)))], (313 ^ _69764) ^ [_79797, _79799] : [-(sdteqdtlpzmzozddtrp0(_79799, _79799, _79797)), aInteger0(_79799), aInteger0(_79797), -(_79797 = sz00)], (224 ^ _69764) ^ [_77040] : [aInteger0(_77040), 227 ^ _69764 : [(230 ^ _69764) ^ [] : [-(smndt0(_77040) = sdtasdt0(_77040, smndt0(sz10)))], (228 ^ _69764) ^ [] : [-(sdtasdt0(smndt0(sz10), _77040) = smndt0(_77040))]]], (192 ^ _69764) ^ [_75947] : [aInteger0(_75947), 195 ^ _69764 : [(198 ^ _69764) ^ [] : [-(_75947 = sdtasdt0(sz10, _75947))], (196 ^ _69764) ^ [] : [-(sdtasdt0(_75947, sz10) = _75947)]]], (393 ^ _69764) ^ [] : [-(aInteger0(xm))], (34 ^ _69764) ^ [_71012, _71014, _71016, _71018, _71020, _71022] : [-(sdteqdtlpzmzozddtrp0(_71020, _71016, _71012)), sdteqdtlpzmzozddtrp0(_71022, _71018, _71014), _71022 = _71020, _71018 = _71016, _71014 = _71012], (128 ^ _69764) ^ [_73939, _73941, _73943] : [-(sdtpldt0(_73943, sdtpldt0(_73941, _73939)) = sdtpldt0(sdtpldt0(_73943, _73941), _73939)), aInteger0(_73943), aInteger0(_73941), aInteger0(_73939)], (142 ^ _69764) ^ [_74359, _74361] : [-(sdtpldt0(_74361, _74359) = sdtpldt0(_74359, _74361)), aInteger0(_74361), aInteger0(_74359)], (381 ^ _69764) ^ [] : [-(aInteger0(xb))], (232 ^ _69764) ^ [_77335, _77337] : [aInteger0(_77337), aInteger0(_77335), sdtasdt0(_77337, _77335) = sz00, -(_77337 = sz00), -(_77335 = sz00)], (52 ^ _69764) ^ [_71545, _71547] : [-(aInteger0(_71545)), _71547 = _71545, aInteger0(_71547)], (383 ^ _69764) ^ [] : [-(aInteger0(xp))], (72 ^ _69764) ^ [_72209, _72211] : [_72211 = _72209, -(smndt0(_72211) = smndt0(_72209))], (160 ^ _69764) ^ [_74925] : [aInteger0(_74925), 163 ^ _69764 : [(166 ^ _69764) ^ [] : [-(sz00 = sdtpldt0(smndt0(_74925), _74925))], (164 ^ _69764) ^ [] : [-(sdtpldt0(_74925, smndt0(_74925)) = sz00)]]], (102 ^ _69764) ^ [_73123] : [aInteger0(_73123), -(aInteger0(smndt0(_73123)))], (250 ^ _69764) ^ [_77803] : [aInteger0(_77803), 253 ^ _69764 : [(267 ^ _69764) ^ [_78451] : [-(aDivisorOf0(_78451, _77803)), aInteger0(_78451), -(_78451 = sz00), 276 ^ _69764 : [(277 ^ _69764) ^ [_78718] : [aInteger0(_78718), sdtasdt0(_78451, _78718) = _77803]]], (254 ^ _69764) ^ [_77989] : [aDivisorOf0(_77989, _77803), 257 ^ _69764 : [(265 ^ _69764) ^ [] : [-(sdtasdt0(_77989, 261 ^ [_77803, _77989]) = _77803)], (258 ^ _69764) ^ [] : [-(aInteger0(_77989))], (263 ^ _69764) ^ [] : [-(aInteger0(261 ^ [_77803, _77989]))], (260 ^ _69764) ^ [] : [_77989 = sz00]]]]], (349 ^ _69764) ^ [_80819, _80821, _80823, _80825] : [-(sdteqdtlpzmzozddtrp0(_80825, _80819, _80821)), sdteqdtlpzmzozddtrp0(_80825, _80823, _80821), sdteqdtlpzmzozddtrp0(_80823, _80819, _80821), aInteger0(_80825), aInteger0(_80823), aInteger0(_80821), -(_80821 = sz00), aInteger0(_80819)], (88 ^ _69764) ^ [_72762] : [aInteger0(_72762), true___, -(true___)], (20 ^ _69764) ^ [_70540, _70542, _70544, _70546] : [-(aDivisorOf0(_70544, _70540)), aDivisorOf0(_70546, _70542), _70546 = _70544, _70542 = _70540], (379 ^ _69764) ^ [] : [-(aInteger0(xa))], (152 ^ _69764) ^ [_74652] : [aInteger0(_74652), 155 ^ _69764 : [(158 ^ _69764) ^ [] : [-(_74652 = sdtpldt0(sz00, _74652))], (156 ^ _69764) ^ [] : [-(sdtpldt0(_74652, sz00) = _74652)]]], (327 ^ _69764) ^ [_80200, _80202, _80204] : [sdteqdtlpzmzozddtrp0(_80204, _80202, _80200), -(sdteqdtlpzmzozddtrp0(_80202, _80204, _80200)), aInteger0(_80204), aInteger0(_80202), aInteger0(_80200), -(_80200 = sz00)], (118 ^ _69764) ^ [_73626, _73628] : [-(aInteger0(sdtasdt0(_73628, _73626))), aInteger0(_73628), aInteger0(_73626)], (4 ^ _69764) ^ [_69995, _69997] : [_69997 = _69995, -(_69995 = _69997)], (78 ^ _69764) ^ [_72435, _72437, _72439, _72441] : [-(sdtasdt0(_72441, _72437) = sdtasdt0(_72439, _72435)), _72441 = _72439, _72437 = _72435], (285 ^ _69764) ^ [_79021, _79023, _79025] : [aInteger0(_79025), aInteger0(_79023), aInteger0(_79021), -(_79021 = sz00), 300 ^ _69764 : [(307 ^ _69764) ^ [] : [aDivisorOf0(_79021, sdtpldt0(_79025, smndt0(_79023))), -(sdteqdtlpzmzozddtrp0(_79025, _79023, _79021))], (301 ^ _69764) ^ [] : [sdteqdtlpzmzozddtrp0(_79025, _79023, _79021), -(aDivisorOf0(_79021, sdtpldt0(_79025, smndt0(_79023))))]]], (395 ^ _69764) ^ [] : [-(sdtasdt0(sdtasdt0(xp, xq), xm) = sdtpldt0(xa, smndt0(xb)))], (168 ^ _69764) ^ [_75234, _75236, _75238] : [-(sdtasdt0(_75238, sdtasdt0(_75236, _75234)) = sdtasdt0(sdtasdt0(_75238, _75236), _75234)), aInteger0(_75238), aInteger0(_75236), aInteger0(_75234)], (385 ^ _69764) ^ [] : [xp = sz00], (2 ^ _69764) ^ [_69888] : [-(_69888 = _69888)], (62 ^ _69764) ^ [_71878, _71880, _71882, _71884] : [-(sdtpldt0(_71884, _71880) = sdtpldt0(_71882, _71878)), _71884 = _71882, _71880 = _71878], (387 ^ _69764) ^ [] : [-(aInteger0(xq))]], input).
% 161.41/158.57 ncf('1',plain,[sdtpldt0(xa, smndt0(xb)) = sdtasdt0(xq, sdtasdt0(xp, xm))],start(397 ^ 0)).
% 161.41/158.57 ncf('1.1',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtasdt0(xq, sdtasdt0(xp, xm))), sdtpldt0(xa, smndt0(xb)) = sdtasdt0(xm, sdtasdt0(xp, xq)), sdtasdt0(xm, sdtasdt0(xp, xq)) = sdtasdt0(xq, sdtasdt0(xp, xm))],extension(10 ^ 1,bind([[_70199, _70201, _70203], [sdtasdt0(xq, sdtasdt0(xp, xm)), sdtasdt0(xm, sdtasdt0(xp, xq)), sdtpldt0(xa, smndt0(xb))]]))).
% 161.41/158.57 ncf('1.1.1',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtasdt0(xm, sdtasdt0(xp, xq))), sdtpldt0(xa, smndt0(xb)) = sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))), sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))) = sdtasdt0(xm, sdtasdt0(xp, xq))],extension(10 ^ 2,bind([[_70199, _70201, _70203], [sdtasdt0(xm, sdtasdt0(xp, xq)), sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))), sdtpldt0(xa, smndt0(xb))]]))).
% 161.41/158.57 ncf('1.1.1.1',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb)))), sdtpldt0(xa, smndt0(xb)) = sdtasdt0(sz10, sdtpldt0(xa, smndt0(xb))), sdtasdt0(sz10, sdtpldt0(xa, smndt0(xb))) = sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb)))],extension(10 ^ 3,bind([[_70199, _70201, _70203], [sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))), sdtasdt0(sz10, sdtpldt0(xa, smndt0(xb))), sdtpldt0(xa, smndt0(xb))]]))).
% 161.41/158.57 ncf('1.1.1.1.1',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtasdt0(sz10, sdtpldt0(xa, smndt0(xb)))), aInteger0(sdtpldt0(xa, smndt0(xb)))],extension(192 ^ 4,bind([[_75947], [sdtpldt0(xa, smndt0(xb))]]))).
% 161.41/158.57 ncf('1.1.1.1.1.1',plain,[-(aInteger0(sdtpldt0(xa, smndt0(xb)))), aInteger0(xa), aInteger0(smndt0(xb))],extension(108 ^ 5,bind([[_73327, _73329], [smndt0(xb), xa]]))).
% 161.41/158.57 ncf('1.1.1.1.1.1.1',plain,[-(aInteger0(xa))],extension(379 ^ 6)).
% 161.41/158.57 ncf('1.1.1.1.1.1.2',plain,[-(aInteger0(smndt0(xb))), aInteger0(xb)],extension(102 ^ 6,bind([[_73123], [xb]]))).
% 161.41/158.57 ncf('1.1.1.1.1.1.2.1',plain,[-(aInteger0(xb))],extension(381 ^ 7)).
% 161.41/158.57 ncf('1.1.1.1.2',plain,[-(sdtasdt0(sz10, sdtpldt0(xa, smndt0(xb))) = sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb)))), sdtasdt0(sz10, sdtpldt0(xa, smndt0(xb))) = sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))), sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))) = sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb)))],extension(10 ^ 4,bind([[_70199, _70201, _70203], [sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))), sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))), sdtasdt0(sz10, sdtpldt0(xa, smndt0(xb)))]]))).
% 161.41/158.57 ncf('1.1.1.1.2.1',plain,[-(sdtasdt0(sz10, sdtpldt0(xa, smndt0(xb))) = sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb)))), aInteger0(sz10), aInteger0(xa), aInteger0(smndt0(xb))],extension(200 ^ 5,bind([[_76248, _76250, _76252], [smndt0(xb), xa, sz10]]))).
% 161.41/158.57 ncf('1.1.1.1.2.1.1',plain,[-(aInteger0(sz10))],extension(100 ^ 6)).
% 161.41/158.57 ncf('1.1.1.1.2.1.2',plain,[-(aInteger0(xa))],extension(379 ^ 6)).
% 161.41/158.57 ncf('1.1.1.1.2.1.3',plain,[-(aInteger0(smndt0(xb))), aInteger0(xb)],extension(102 ^ 6,bind([[_73123], [xb]]))).
% 161.41/158.57 ncf('1.1.1.1.2.1.3.1',plain,[-(aInteger0(xb))],extension(381 ^ 7)).
% 161.41/158.57 ncf('1.1.1.1.2.2',plain,[-(sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))) = sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb)))), sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))) = sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb)))],extension(4 ^ 5,bind([[_69995, _69997], [sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))), sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb)))]]))).
% 161.41/158.57 ncf('1.1.1.1.2.2.1',plain,[-(sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))) = sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))))],extension(2 ^ 6,bind([[_69888], [sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb)))]]))).
% 161.41/158.57 ncf('1.1.1.2',plain,[-(sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))) = sdtasdt0(xm, sdtasdt0(xp, xq))), sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))) = sdtasdt0(sdtasdt0(xp, xq), xm), sdtasdt0(sdtasdt0(xp, xq), xm) = sdtasdt0(xm, sdtasdt0(xp, xq))],extension(10 ^ 3,bind([[_70199, _70201, _70203], [sdtasdt0(xm, sdtasdt0(xp, xq)), sdtasdt0(sdtasdt0(xp, xq), xm), sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb)))]]))).
% 161.41/158.57 ncf('1.1.1.2.1',plain,[-(sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))) = sdtasdt0(sdtasdt0(xp, xq), xm)), sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))) = sdtasdt0(sdtasdt0(xp, xq), xm), sdtasdt0(sdtasdt0(xp, xq), xm) = sdtasdt0(sdtasdt0(xp, xq), xm)],extension(10 ^ 4,bind([[_70199, _70201, _70203], [sdtasdt0(sdtasdt0(xp, xq), xm), sdtasdt0(sdtasdt0(xp, xq), xm), sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb)))]]))).
% 161.41/158.57 ncf('1.1.1.2.1.1',plain,[-(sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))) = sdtasdt0(sdtasdt0(xp, xq), xm)), sdtasdt0(sdtasdt0(xp, xq), xm) = sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb)))],extension(4 ^ 5,bind([[_69995, _69997], [sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))), sdtasdt0(sdtasdt0(xp, xq), xm)]]))).
% 161.41/158.57 ncf('1.1.1.2.1.1.1',plain,[-(sdtasdt0(sdtasdt0(xp, xq), xm) = sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb)))), sdtasdt0(sdtasdt0(xp, xq), xm) = sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb)) = sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb)))],extension(10 ^ 6,bind([[_70199, _70201, _70203], [sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))), sdtpldt0(xa, smndt0(xb)), sdtasdt0(sdtasdt0(xp, xq), xm)]]))).
% 161.41/158.57 ncf('1.1.1.2.1.1.1.1',plain,[-(sdtasdt0(sdtasdt0(xp, xq), xm) = sdtpldt0(xa, smndt0(xb)))],extension(395 ^ 7)).
% 161.41/158.57 ncf('1.1.1.2.1.1.1.2',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(sdtasdt0(sz10, xa), sdtasdt0(sz10, smndt0(xb))))],lemmata('[1, 1].x')).
% 161.41/158.57 ncf('1.1.1.2.1.2',plain,[-(sdtasdt0(sdtasdt0(xp, xq), xm) = sdtasdt0(sdtasdt0(xp, xq), xm)), sdtasdt0(sdtasdt0(xp, xq), xm) = sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb)) = sdtasdt0(sdtasdt0(xp, xq), xm)],extension(10 ^ 5,bind([[_70199, _70201, _70203], [sdtasdt0(sdtasdt0(xp, xq), xm), sdtpldt0(xa, smndt0(xb)), sdtasdt0(sdtasdt0(xp, xq), xm)]]))).
% 161.41/158.57 ncf('1.1.1.2.1.2.1',plain,[-(sdtasdt0(sdtasdt0(xp, xq), xm) = sdtpldt0(xa, smndt0(xb)))],extension(395 ^ 6)).
% 161.41/158.57 ncf('1.1.1.2.1.2.2',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtasdt0(sdtasdt0(xp, xq), xm)), sdtasdt0(sdtasdt0(xp, xq), xm) = sdtpldt0(xa, smndt0(xb))],extension(4 ^ 6,bind([[_69995, _69997], [sdtpldt0(xa, smndt0(xb)), sdtasdt0(sdtasdt0(xp, xq), xm)]]))).
% 161.41/158.57 ncf('1.1.1.2.1.2.2.1',plain,[-(sdtasdt0(sdtasdt0(xp, xq), xm) = sdtpldt0(xa, smndt0(xb)))],extension(395 ^ 7)).
% 161.41/158.57 ncf('1.1.1.2.2',plain,[-(sdtasdt0(sdtasdt0(xp, xq), xm) = sdtasdt0(xm, sdtasdt0(xp, xq))), aInteger0(sdtasdt0(xp, xq)), aInteger0(xm)],extension(182 ^ 4,bind([[_75654, _75656], [xm, sdtasdt0(xp, xq)]]))).
% 161.41/158.57 ncf('1.1.1.2.2.1',plain,[-(aInteger0(sdtasdt0(xp, xq))), sdtasdt0(xq, xp) = sdtasdt0(xp, xq), aInteger0(sdtasdt0(xq, xp))],extension(52 ^ 5,bind([[_71545, _71547], [sdtasdt0(xp, xq), sdtasdt0(xq, xp)]]))).
% 161.41/158.57 ncf('1.1.1.2.2.1.1',plain,[-(sdtasdt0(xq, xp) = sdtasdt0(xp, xq)), aInteger0(xq), aInteger0(xp)],extension(182 ^ 6,bind([[_75654, _75656], [xp, xq]]))).
% 161.41/158.57 ncf('1.1.1.2.2.1.1.1',plain,[-(aInteger0(xq))],extension(387 ^ 7)).
% 161.41/158.57 ncf('1.1.1.2.2.1.1.2',plain,[-(aInteger0(xp))],extension(383 ^ 7)).
% 161.41/158.57 ncf('1.1.1.2.2.1.2',plain,[-(aInteger0(sdtasdt0(xq, xp))), aInteger0(xq), aInteger0(xp)],extension(118 ^ 6,bind([[_73626, _73628], [xp, xq]]))).
% 161.41/158.57 ncf('1.1.1.2.2.1.2.1',plain,[-(aInteger0(xq))],extension(387 ^ 7)).
% 161.41/158.57 ncf('1.1.1.2.2.1.2.2',plain,[-(aInteger0(xp))],extension(383 ^ 7)).
% 161.41/158.57 ncf('1.1.1.2.2.2',plain,[-(aInteger0(xm))],extension(393 ^ 5)).
% 161.41/158.57 ncf('1.1.2',plain,[-(sdtasdt0(xm, sdtasdt0(xp, xq)) = sdtasdt0(xq, sdtasdt0(xp, xm))), sdtasdt0(xq, sdtasdt0(xp, xm)) = sdtasdt0(xm, sdtasdt0(xp, xq))],extension(4 ^ 2,bind([[_69995, _69997], [sdtasdt0(xm, sdtasdt0(xp, xq)), sdtasdt0(xq, sdtasdt0(xp, xm))]]))).
% 161.41/158.57 ncf('1.1.2.1',plain,[-(sdtasdt0(xq, sdtasdt0(xp, xm)) = sdtasdt0(xm, sdtasdt0(xp, xq))), sdtasdt0(xq, sdtasdt0(xp, xm)) = sdtasdt0(xm, sdtasdt0(xq, xp)), sdtasdt0(xm, sdtasdt0(xq, xp)) = sdtasdt0(xm, sdtasdt0(xp, xq))],extension(10 ^ 3,bind([[_70199, _70201, _70203], [sdtasdt0(xm, sdtasdt0(xp, xq)), sdtasdt0(xm, sdtasdt0(xq, xp)), sdtasdt0(xq, sdtasdt0(xp, xm))]]))).
% 161.41/158.57 ncf('1.1.2.1.1',plain,[-(sdtasdt0(xq, sdtasdt0(xp, xm)) = sdtasdt0(xm, sdtasdt0(xq, xp))), sdtasdt0(xq, sdtasdt0(xp, xm)) = sdtasdt0(sdtasdt0(xq, xp), xm), sdtasdt0(sdtasdt0(xq, xp), xm) = sdtasdt0(xm, sdtasdt0(xq, xp))],extension(10 ^ 4,bind([[_70199, _70201, _70203], [sdtasdt0(xm, sdtasdt0(xq, xp)), sdtasdt0(sdtasdt0(xq, xp), xm), sdtasdt0(xq, sdtasdt0(xp, xm))]]))).
% 161.41/158.57 ncf('1.1.2.1.1.1',plain,[-(sdtasdt0(xq, sdtasdt0(xp, xm)) = sdtasdt0(sdtasdt0(xq, xp), xm)), sdtasdt0(xq, sdtasdt0(xp, xm)) = sdtasdt0(sdtasdt0(xq, xp), xm), sdtasdt0(sdtasdt0(xq, xp), xm) = sdtasdt0(sdtasdt0(xq, xp), xm)],extension(10 ^ 5,bind([[_70199, _70201, _70203], [sdtasdt0(sdtasdt0(xq, xp), xm), sdtasdt0(sdtasdt0(xq, xp), xm), sdtasdt0(xq, sdtasdt0(xp, xm))]]))).
% 161.41/158.57 ncf('1.1.2.1.1.1.1',plain,[-(sdtasdt0(xq, sdtasdt0(xp, xm)) = sdtasdt0(sdtasdt0(xq, xp), xm)), aInteger0(xq), aInteger0(xp), aInteger0(xm)],extension(168 ^ 6,bind([[_75234, _75236, _75238], [xm, xp, xq]]))).
% 161.41/158.57 ncf('1.1.2.1.1.1.1.1',plain,[-(aInteger0(xq))],extension(387 ^ 7)).
% 161.41/158.57 ncf('1.1.2.1.1.1.1.2',plain,[-(aInteger0(xp))],extension(383 ^ 7)).
% 161.41/158.57 ncf('1.1.2.1.1.1.1.3',plain,[-(aInteger0(xm))],extension(393 ^ 7)).
% 161.41/158.57 ncf('1.1.2.1.1.1.2',plain,[-(sdtasdt0(sdtasdt0(xq, xp), xm) = sdtasdt0(sdtasdt0(xq, xp), xm))],extension(2 ^ 6,bind([[_69888], [sdtasdt0(sdtasdt0(xq, xp), xm)]]))).
% 161.41/158.57 ncf('1.1.2.1.1.2',plain,[-(sdtasdt0(sdtasdt0(xq, xp), xm) = sdtasdt0(xm, sdtasdt0(xq, xp))), aInteger0(sdtasdt0(xq, xp)), aInteger0(xm)],extension(182 ^ 5,bind([[_75654, _75656], [xm, sdtasdt0(xq, xp)]]))).
% 161.41/158.57 ncf('1.1.2.1.1.2.1',plain,[-(aInteger0(sdtasdt0(xq, xp))), aInteger0(xq), aInteger0(xp)],extension(118 ^ 6,bind([[_73626, _73628], [xp, xq]]))).
% 161.41/158.57 ncf('1.1.2.1.1.2.1.1',plain,[-(aInteger0(xq))],extension(387 ^ 7)).
% 161.41/158.57 ncf('1.1.2.1.1.2.1.2',plain,[-(aInteger0(xp))],extension(383 ^ 7)).
% 161.41/158.57 ncf('1.1.2.1.1.2.2',plain,[-(aInteger0(xm))],extension(393 ^ 6)).
% 161.41/158.57 ncf('1.1.2.1.2',plain,[-(sdtasdt0(xm, sdtasdt0(xq, xp)) = sdtasdt0(xm, sdtasdt0(xp, xq))), sdtasdt0(xm, sdtasdt0(xp, xq)) = sdtasdt0(xm, sdtasdt0(xq, xp))],extension(4 ^ 4,bind([[_69995, _69997], [sdtasdt0(xm, sdtasdt0(xq, xp)), sdtasdt0(xm, sdtasdt0(xp, xq))]]))).
% 161.41/158.57 ncf('1.1.2.1.2.1',plain,[-(sdtasdt0(xm, sdtasdt0(xp, xq)) = sdtasdt0(xm, sdtasdt0(xq, xp))), xm = xm, sdtasdt0(xp, xq) = sdtasdt0(xq, xp)],extension(78 ^ 5,bind([[_72435, _72437, _72439, _72441], [sdtasdt0(xq, xp), sdtasdt0(xp, xq), xm, xm]]))).
% 161.41/158.57 ncf('1.1.2.1.2.1.1',plain,[-(xm = xm)],extension(2 ^ 6,bind([[_69888], [xm]]))).
% 161.41/158.57 ncf('1.1.2.1.2.1.2',plain,[-(sdtasdt0(xp, xq) = sdtasdt0(xq, xp)), aInteger0(xp), aInteger0(xq)],extension(182 ^ 6,bind([[_75654, _75656], [xq, xp]]))).
% 161.41/158.57 ncf('1.1.2.1.2.1.2.1',plain,[-(aInteger0(xp))],extension(383 ^ 7)).
% 161.41/158.57 ncf('1.1.2.1.2.1.2.2',plain,[-(aInteger0(xq))],extension(387 ^ 7)).
% 161.41/158.57 %-----------------------------------------------------
% 161.41/158.57 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------