Below is the ME proof, followed by statistics.

Proof Chain -- 5 steps:

Root:
{ (not (< (+ (succ $MVI-1) $UI-1) (* (succ $MVI-1) $UI-1))) }

Extend:
{ (not (< ?Fl1-17p ?Y-17q));
(< ?X-17r ?Y-17q);
(not (= ?Fl1-17p (succ ?X-17r))) }

[ ?X-17r -> (+ (succ $MVI-1) $UI-1), ?Y-17q ->
(* (succ $MVI-1) $UI-1) ]

Clause:
{ [(not (< (+ (succ $MVI-1) $UI-1) (* (succ $MVI-1) $UI-1)))];
(not (< ?Fl1-17p (* (succ $MVI-1) $UI-1)));
(not (= ?Fl1-17p (succ (+ (succ $MVI-1) $UI-1)))) }

Extend:
{ (= ?Eq-2r0 ?Eq-2r0) }

[ ?Fl1-17p -> (succ (+ (succ $MVI-1) $UI-1)), ?Eq-2r0 ->
(succ (+ (succ $MVI-1) $UI-1)) ]

Clause:
{ [(not (< (+ (succ $MVI-1) $UI-1)
(* (succ $MVI-1) $UI-1)))];
(not (< (succ (+ (succ $MVI-1) $UI-1))
(* (succ $MVI-1) $UI-1))) }

Extend:
{ (not (< (succ 0) ?X-9tt));
(not (< (succ 0) ?Y-9tu));
(< (succ (+ ?X-9tt ?Y-9tu)) (* ?X-9tt ?Y-9tu)) }

[ ?X-9tt -> (succ $MVI-1), ?Y-9tu -> $UI-1 ]

Clause:
{ [(not (< (+ (succ $MVI-1) $UI-1) (* (succ $MVI-1) $UI-1)))];
[(not (< (succ (+ (succ $MVI-1) $UI-1))
(* (succ $MVI-1) $UI-1)))];
(not (< (succ 0) (succ $MVI-1)));
(not (< (succ 0) $UI-1)) }

Extend:
{ (< (succ 0) $UI-1) }

[ <empty> ]

Base step:

Clause:
{ [(not (< (+ (succ $MVI-1) $UI-1) (* (succ $MVI-1) $UI-1)))];
[(not (< (succ (+ (succ $MVI-1) $UI-1))
(* (succ $MVI-1) $UI-1)))];
(not (< (succ 0) (succ $MVI-1))) }

Extend:
{ (< (succ 0) (succ $MVI-1)) }
1
[ <empty> ]

Clause:
{ }

Proved

Step Stats: elapsedTime=1.133; cpuTime=0.0; steps=5; roots=1; inputs=8; hornInputs=8; definiteInputs=6; generalInputs=0; factors=0; premiseLiterals=337; rootLiterals=10; generated=189; predicates=6; functions=10; constants=6; skFunctions=4; skConstants=2; expanded=156; derivations=188; factorizations=0; reductions=0; extensions=189; symIDUnif=0; outOrder=1.2051282; maxQueue=8127; nResidual=8126; nTooDeep=0; nUnacceptable=35; nXUnacceptable=1; nSubsumed=0; nVacuous=0; proofLength=5

Proof Stats: proved=1; elapsedTime=1.264; cpuTime=0.0; subproofs=2; successes=2; steps=7; roots=4; inputs=129; hornInputs=121; definiteInputs=110; generalInputs=8; factors=0; premiseLiterals=648; rootLiterals=28; generated=201; predicates=6; functions=10; constants=6; skFunctions=4; skConstants=2; expanded=166; derivations=197; factorizations=0; reductions=0; extensions=199; symIDUnif=0; outOrder=1.186747; maxQueue=8127; nResidual=8594; nTooDeep=0; nUnacceptable=35; nXUnacceptable=1; nSubsumed=0; nVacuous=1; proofLength=5

Elapsed: 0m4s; User: 0m2.4s; System: 0m0.1s