(NOTE-LIB "fortran" T) Loading ./basic/fortran.lib Finished loading ./basic/fortran.lib Loading ./basic/fortran.o Finished loading ./basic/fortran.o (#./basic/fortran.lib #./basic/fortran) (COMPILE-UNCOMPILED-DEFNS "tmp") Loading ./basic/tmp.o Finished loading ./basic/tmp.o /v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/tmp.lisp (PROVE-LEMMA ZPLUS-COMM1 (REWRITE) (EQUAL (ZPLUS X Y) (ZPLUS Y X))) WARNING: Note that the rewrite rule ZPLUS-COMM1 will be stored so as to apply only to terms with the nonrecursive function symbol ZPLUS. This formula simplifies, rewriting with COMMUTATIVITY-OF-PLUS, and expanding the function ZPLUS, to: T. Q.E.D. [ 0.0 0.0 0.0 ] ZPLUS-COMM1 (PROVE-LEMMA ZPLUS-COMM2 (REWRITE) (EQUAL (ZPLUS X (ZPLUS Y Z)) (ZPLUS Y (ZPLUS X Z)))) WARNING: Note that the rewrite rule ZPLUS-COMM2 will be stored so as to apply only to terms with the nonrecursive function symbol ZPLUS. WARNING: the previously added lemma, ZPLUS-COMM1, could be applied whenever the newly proposed ZPLUS-COMM2 could! This simplifies, unfolding the definition of ZPLUS, to the following 18 new goals: Case 18.(IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z)))) (EQUAL (ZPLUS X (DIFFERENCE Y (NEGATIVE-GUTS Z))) (ZPLUS Y (DIFFERENCE X (NEGATIVE-GUTS Z))))). This again simplifies, opening up the definition of ZPLUS, to the goal: (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z)))) (EQUAL (PLUS X (DIFFERENCE Y (NEGATIVE-GUTS Z))) (PLUS Y (DIFFERENCE X (NEGATIVE-GUTS Z))))). This again simplifies, using linear arithmetic, to: T. Case 17.(IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z))) (EQUAL (ZPLUS X (MINUS (DIFFERENCE (NEGATIVE-GUTS Z) Y))) (ZPLUS Y (DIFFERENCE X (NEGATIVE-GUTS Z))))), which again simplifies, applying the lemma NEGATIVE-GUTS-MINUS, and opening up the function ZPLUS, to two new goals: Case 17.2. (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z))) (EQUAL (DIFFERENCE X (DIFFERENCE (NEGATIVE-GUTS Z) Y)) (PLUS Y (DIFFERENCE X (NEGATIVE-GUTS Z))))), which again simplifies, using linear arithmetic, to two new formulas: Case 17.2.2. (IMPLIES (AND (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y)) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z))) (EQUAL (DIFFERENCE X (DIFFERENCE (NEGATIVE-GUTS Z) Y)) (PLUS Y (DIFFERENCE X (NEGATIVE-GUTS Z))))), which again simplifies, using linear arithmetic, to the goal: (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y) (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y)) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z))) (EQUAL (DIFFERENCE X (DIFFERENCE (NEGATIVE-GUTS Z) Y)) (PLUS Y (DIFFERENCE X (NEGATIVE-GUTS Z))))). This again simplifies, using linear arithmetic, to: T. Case 17.2.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z))) (EQUAL (DIFFERENCE X (DIFFERENCE (NEGATIVE-GUTS Z) Y)) (PLUS Y (DIFFERENCE X (NEGATIVE-GUTS Z))))), which again simplifies, using linear arithmetic, to: T. Case 17.1. (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z))) (NOT (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y)))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z))) (NOT (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y)))). This again simplifies, using linear arithmetic, to: T. Case 16.(IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NEGATIVEP Y)) (EQUAL (ZPLUS X (MINUS (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)))) (ZPLUS Y (DIFFERENCE X (NEGATIVE-GUTS Z))))), which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and expanding the definition of ZPLUS, to the following four new formulas: Case 16.4. (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NEGATIVEP Y) (LESSP (DIFFERENCE X (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS Y))) (EQUAL (MINUS (DIFFERENCE (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X)) (MINUS (DIFFERENCE (NEGATIVE-GUTS Y) (DIFFERENCE X (NEGATIVE-GUTS Z)))))). However this again simplifies, appealing to the lemmas NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to the formula: (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NEGATIVEP Y) (LESSP (DIFFERENCE X (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS Y))) (EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X) (DIFFERENCE (NEGATIVE-GUTS Y) (DIFFERENCE X (NEGATIVE-GUTS Z))))). This again simplifies, using linear arithmetic, to two new conjectures: Case 16.4.2. (IMPLIES (AND (LESSP (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NEGATIVEP Y) (LESSP (DIFFERENCE X (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS Y))) (EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X) (DIFFERENCE (NEGATIVE-GUTS Y) (DIFFERENCE X (NEGATIVE-GUTS Z))))), which again simplifies, using linear arithmetic, to: T. Case 16.4.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) (DIFFERENCE X (NEGATIVE-GUTS Z))) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NEGATIVEP Y) (LESSP (DIFFERENCE X (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS Y))) (EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X) (DIFFERENCE (NEGATIVE-GUTS Y) (DIFFERENCE X (NEGATIVE-GUTS Z))))), which again simplifies, using linear arithmetic, to: T. Case 16.3. (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NEGATIVEP Y) (NOT (LESSP X (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z))))) (EQUAL (DIFFERENCE X (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z))) (DIFFERENCE (DIFFERENCE X (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS Y)))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (DIFFERENCE X (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS Y)) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NEGATIVEP Y) (NOT (LESSP X (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z))))) (EQUAL (DIFFERENCE X (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z))) (DIFFERENCE (DIFFERENCE X (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS Y)))). However this again simplifies, using linear arithmetic, to: T. Case 16.2. (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NEGATIVEP Y) (NOT (LESSP (DIFFERENCE X (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS Y)))) (NOT (LESSP X (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z))))), which again simplifies, using linear arithmetic, to: T. Case 16.1. (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (NOT (LESSP X (NEGATIVE-GUTS Z))) (NEGATIVEP Y) (LESSP (DIFFERENCE X (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS Y))) (LESSP X (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)))), which again simplifies, using linear arithmetic, to: T. Case 15.(IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z)))) (EQUAL (ZPLUS X (DIFFERENCE Y (NEGATIVE-GUTS Z))) (ZPLUS Y (MINUS (DIFFERENCE (NEGATIVE-GUTS Z) X))))), which again simplifies, applying the lemma NEGATIVE-GUTS-MINUS, and opening up the function ZPLUS, to two new formulas: Case 15.2. (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z)))) (EQUAL (PLUS X (DIFFERENCE Y (NEGATIVE-GUTS Z))) (DIFFERENCE Y (DIFFERENCE (NEGATIVE-GUTS Z) X)))), which again simplifies, using linear arithmetic, to two new goals: Case 15.2.2. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z)))) (EQUAL (PLUS X (DIFFERENCE Y (NEGATIVE-GUTS Z))) (DIFFERENCE Y (DIFFERENCE (NEGATIVE-GUTS Z) X)))), which again simplifies, using linear arithmetic, to: T. Case 15.2.1. (IMPLIES (AND (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X)) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z)))) (EQUAL (PLUS X (DIFFERENCE Y (NEGATIVE-GUTS Z))) (DIFFERENCE Y (DIFFERENCE (NEGATIVE-GUTS Z) X)))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X)) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z)))) (EQUAL (PLUS X (DIFFERENCE Y (NEGATIVE-GUTS Z))) (DIFFERENCE Y (DIFFERENCE (NEGATIVE-GUTS Z) X)))). But this again simplifies, using linear arithmetic, to: T. Case 15.1. (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z)))) (NOT (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X)))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z)))) (NOT (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X)))). This again simplifies, using linear arithmetic, to: T. Case 14.(IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z))) (EQUAL (ZPLUS X (MINUS (DIFFERENCE (NEGATIVE-GUTS Z) Y))) (ZPLUS Y (MINUS (DIFFERENCE (NEGATIVE-GUTS Z) X))))), which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and expanding ZPLUS, to the following four new conjectures: Case 14.4. (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X))) (EQUAL (MINUS (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y) X)) (MINUS (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) X) Y)))). This again simplifies, applying NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to: (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X))) (EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y) X) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) X) Y))), which again simplifies, using linear arithmetic, to four new formulas: Case 14.4.4. (IMPLIES (AND (LESSP (DIFFERENCE (NEGATIVE-GUTS Z) Y) X) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X))) (EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y) X) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) X) Y))), which again simplifies, using linear arithmetic, to the goal: (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X) (LESSP (DIFFERENCE (NEGATIVE-GUTS Z) Y) X) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X))) (EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y) X) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) X) Y))). This again simplifies, using linear arithmetic, to: T. Case 14.4.3. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X))) (EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y) X) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) X) Y))), which again simplifies, using linear arithmetic, to: T. Case 14.4.2. (IMPLIES (AND (LESSP (DIFFERENCE (NEGATIVE-GUTS Z) X) Y) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X))) (EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y) X) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) X) Y))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X) (LESSP (DIFFERENCE (NEGATIVE-GUTS Z) X) Y) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X))) (EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y) X) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) X) Y))). This again simplifies, using linear arithmetic, to: T. Case 14.4.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X))) (EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y) X) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) X) Y))), which again simplifies, using linear arithmetic, to: T. Case 14.3. (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y)))) (EQUAL (DIFFERENCE X (DIFFERENCE (NEGATIVE-GUTS Z) Y)) (DIFFERENCE Y (DIFFERENCE (NEGATIVE-GUTS Z) X)))), which again simplifies, using linear arithmetic, to three new conjectures: Case 14.3.3. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y)))) (EQUAL (DIFFERENCE X (DIFFERENCE (NEGATIVE-GUTS Z) Y)) (DIFFERENCE Y (DIFFERENCE (NEGATIVE-GUTS Z) X)))), which again simplifies, using linear arithmetic, to: T. Case 14.3.2. (IMPLIES (AND (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X)) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y)))) (EQUAL (DIFFERENCE X (DIFFERENCE (NEGATIVE-GUTS Z) Y)) (DIFFERENCE Y (DIFFERENCE (NEGATIVE-GUTS Z) X)))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X)) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y)))) (EQUAL (DIFFERENCE X (DIFFERENCE (NEGATIVE-GUTS Z) Y)) (DIFFERENCE Y (DIFFERENCE (NEGATIVE-GUTS Z) X)))). However this again simplifies, using linear arithmetic, to: T. Case 14.3.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y)))) (EQUAL (DIFFERENCE X (DIFFERENCE (NEGATIVE-GUTS Z) Y)) (DIFFERENCE Y (DIFFERENCE (NEGATIVE-GUTS Z) X)))), which again simplifies, using linear arithmetic, to: T. Case 14.2. (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X)))) (NOT (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y)))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X)))) (NOT (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y)))). But this again simplifies, using linear arithmetic, to: T. Case 14.1. (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X))) (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS Z) X))) (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y))). But this again simplifies, using linear arithmetic, to: T. Case 13.(IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NEGATIVEP Y)) (EQUAL (ZPLUS X (MINUS (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)))) (ZPLUS Y (MINUS (DIFFERENCE (NEGATIVE-GUTS Z) X))))), which again simplifies, applying NEGATIVE-GUTS-MINUS, and opening up ZPLUS, to the following two new goals: Case 13.2. (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NEGATIVEP Y)) (EQUAL (MINUS (DIFFERENCE (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X)) (MINUS (PLUS (NEGATIVE-GUTS Y) (DIFFERENCE (NEGATIVE-GUTS Z) X))))). This again simplifies, rewriting with NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to: (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NEGATIVEP Y)) (EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X) (PLUS (NEGATIVE-GUTS Y) (DIFFERENCE (NEGATIVE-GUTS Z) X)))), which again simplifies, using linear arithmetic, to two new formulas: Case 13.2.2. (IMPLIES (AND (LESSP (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NEGATIVEP Y)) (EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X) (PLUS (NEGATIVE-GUTS Y) (DIFFERENCE (NEGATIVE-GUTS Z) X)))), which again simplifies, using linear arithmetic, to: T. Case 13.2.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X) (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NEGATIVEP Y)) (EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X) (PLUS (NEGATIVE-GUTS Y) (DIFFERENCE (NEGATIVE-GUTS Z) X)))), which again simplifies, using linear arithmetic, to: T. Case 13.1. (IMPLIES (AND (NOT (NEGATIVEP X)) (NEGATIVEP Z) (LESSP X (NEGATIVE-GUTS Z)) (NEGATIVEP Y)) (LESSP X (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)))), which again simplifies, using linear arithmetic, to: T. Case 12.(IMPLIES (AND (NOT (NEGATIVEP X)) (NOT (NEGATIVEP Z)) (NOT (NEGATIVEP Y))) (EQUAL (ZPLUS X (PLUS Y Z)) (ZPLUS Y (PLUS X Z)))), which again simplifies, appealing to the lemma COMMUTATIVITY2-OF-PLUS, and unfolding the function ZPLUS, to: T. Case 11.(IMPLIES (AND (NOT (NEGATIVEP X)) (NOT (NEGATIVEP Z)) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y)))) (EQUAL (ZPLUS X (DIFFERENCE Z (NEGATIVE-GUTS Y))) (ZPLUS Y (PLUS X Z)))), which again simplifies, unfolding the definition of ZPLUS, to two new formulas: Case 11.2. (IMPLIES (AND (NOT (NEGATIVEP X)) (NOT (NEGATIVEP Z)) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y)))) (EQUAL (PLUS X (DIFFERENCE Z (NEGATIVE-GUTS Y))) (DIFFERENCE (PLUS X Z) (NEGATIVE-GUTS Y)))), which again simplifies, using linear arithmetic, to the goal: (IMPLIES (AND (LESSP (PLUS X Z) (NEGATIVE-GUTS Y)) (NOT (NEGATIVEP X)) (NOT (NEGATIVEP Z)) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y)))) (EQUAL (PLUS X (DIFFERENCE Z (NEGATIVE-GUTS Y))) (DIFFERENCE (PLUS X Z) (NEGATIVE-GUTS Y)))). But this again simplifies, using linear arithmetic, to: T. Case 11.1. (IMPLIES (AND (NOT (NEGATIVEP X)) (NOT (NEGATIVEP Z)) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y)))) (NOT (LESSP (PLUS X Z) (NEGATIVE-GUTS Y)))), which again simplifies, using linear arithmetic, to: T. Case 10.(IMPLIES (AND (NOT (NEGATIVEP X)) (NOT (NEGATIVEP Z)) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y))) (EQUAL (ZPLUS X (MINUS (DIFFERENCE (NEGATIVE-GUTS Y) Z))) (ZPLUS Y (PLUS X Z)))), which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and opening up the definition of ZPLUS, to the following four new formulas: Case 10.4. (IMPLIES (AND (NOT (NEGATIVEP X)) (NOT (NEGATIVEP Z)) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y)) (LESSP (PLUS X Z) (NEGATIVE-GUTS Y))) (EQUAL (MINUS (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z) X)) (MINUS (DIFFERENCE (NEGATIVE-GUTS Y) (PLUS X Z))))). But this again simplifies, rewriting with the lemmas NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to the formula: (IMPLIES (AND (NOT (NEGATIVEP X)) (NOT (NEGATIVEP Z)) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y)) (LESSP (PLUS X Z) (NEGATIVE-GUTS Y))) (EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z) X) (DIFFERENCE (NEGATIVE-GUTS Y) (PLUS X Z)))). This again simplifies, using linear arithmetic, to three new goals: Case 10.4.3. (IMPLIES (AND (LESSP (DIFFERENCE (NEGATIVE-GUTS Y) Z) X) (NOT (NEGATIVEP X)) (NOT (NEGATIVEP Z)) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y)) (LESSP (PLUS X Z) (NEGATIVE-GUTS Y))) (EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z) X) (DIFFERENCE (NEGATIVE-GUTS Y) (PLUS X Z)))), which again simplifies, using linear arithmetic, to: T. Case 10.4.2. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z) (NOT (NEGATIVEP X)) (NOT (NEGATIVEP Z)) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y)) (LESSP (PLUS X Z) (NEGATIVE-GUTS Y))) (EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z) X) (DIFFERENCE (NEGATIVE-GUTS Y) (PLUS X Z)))), which again simplifies, using linear arithmetic, to: T. Case 10.4.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) (PLUS X Z)) (NOT (NEGATIVEP X)) (NOT (NEGATIVEP Z)) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y)) (LESSP (PLUS X Z) (NEGATIVE-GUTS Y))) (EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z) X) (DIFFERENCE (NEGATIVE-GUTS Y) (PLUS X Z)))), which again simplifies, using linear arithmetic, to: T. Case 10.3. (IMPLIES (AND (NOT (NEGATIVEP X)) (NOT (NEGATIVEP Z)) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y)) (NOT (LESSP X (DIFFERENCE (NEGATIVE-GUTS Y) Z)))) (EQUAL (DIFFERENCE X (DIFFERENCE (NEGATIVE-GUTS Y) Z)) (DIFFERENCE (PLUS X Z) (NEGATIVE-GUTS Y)))), which again simplifies, using linear arithmetic, to two new formulas: Case 10.3.2. (IMPLIES (AND (LESSP (PLUS X Z) (NEGATIVE-GUTS Y)) (NOT (NEGATIVEP X)) (NOT (NEGATIVEP Z)) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y)) (NOT (LESSP X (DIFFERENCE (NEGATIVE-GUTS Y) Z)))) (EQUAL (DIFFERENCE X (DIFFERENCE (NEGATIVE-GUTS Y) Z)) (DIFFERENCE (PLUS X Z) (NEGATIVE-GUTS Y)))), which again simplifies, using linear arithmetic, to: T. Case 10.3.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z) (NOT (NEGATIVEP X)) (NOT (NEGATIVEP Z)) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y)) (NOT (LESSP X (DIFFERENCE (NEGATIVE-GUTS Y) Z)))) (EQUAL (DIFFERENCE X (DIFFERENCE (NEGATIVE-GUTS Y) Z)) (DIFFERENCE (PLUS X Z) (NEGATIVE-GUTS Y)))), which again simplifies, using linear arithmetic, to: T. Case 10.2. (IMPLIES (AND (NOT (NEGATIVEP X)) (NOT (NEGATIVEP Z)) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y)) (NOT (LESSP (PLUS X Z) (NEGATIVE-GUTS Y)))) (NOT (LESSP X (DIFFERENCE (NEGATIVE-GUTS Y) Z)))), which again simplifies, using linear arithmetic, to the conjecture: (IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z) (NOT (NEGATIVEP X)) (NOT (NEGATIVEP Z)) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y)) (NOT (LESSP (PLUS X Z) (NEGATIVE-GUTS Y)))) (NOT (LESSP X (DIFFERENCE (NEGATIVE-GUTS Y) Z)))). But this again simplifies, using linear arithmetic, to: T. Case 10.1. (IMPLIES (AND (NOT (NEGATIVEP X)) (NOT (NEGATIVEP Z)) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y)) (LESSP (PLUS X Z) (NEGATIVE-GUTS Y))) (LESSP X (DIFFERENCE (NEGATIVE-GUTS Y) Z))), which again simplifies, using linear arithmetic, to: T. Case 9. (IMPLIES (AND (NEGATIVEP X) (NEGATIVEP Z) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z)))) (EQUAL (ZPLUS X (DIFFERENCE Y (NEGATIVE-GUTS Z))) (ZPLUS Y (MINUS (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)))))), which again simplifies, applying NEGATIVE-GUTS-MINUS, and expanding ZPLUS, to the following four new formulas: Case 9.4. (IMPLIES (AND (NEGATIVEP X) (NEGATIVEP Z) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (LESSP Y (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)))) (EQUAL (MINUS (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Y (NEGATIVE-GUTS Z)))) (MINUS (DIFFERENCE (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)) Y)))). However this again simplifies, rewriting with NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to the new formula: (IMPLIES (AND (NEGATIVEP X) (NEGATIVEP Z) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (LESSP Y (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Y (NEGATIVE-GUTS Z))) (DIFFERENCE (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)) Y))), which again simplifies, using linear arithmetic, to two new formulas: Case 9.4.2. (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) (DIFFERENCE Y (NEGATIVE-GUTS Z))) (NEGATIVEP X) (NEGATIVEP Z) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (LESSP Y (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Y (NEGATIVE-GUTS Z))) (DIFFERENCE (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)) Y))), which again simplifies, using linear arithmetic, to: T. Case 9.4.1. (IMPLIES (AND (LESSP (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)) Y) (NEGATIVEP X) (NEGATIVEP Z) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (LESSP Y (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Y (NEGATIVE-GUTS Z))) (DIFFERENCE (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)) Y))), which again simplifies, using linear arithmetic, to: T. Case 9.3. (IMPLIES (AND (NEGATIVEP X) (NEGATIVEP Z) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NOT (LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS X)))) (EQUAL (DIFFERENCE (DIFFERENCE Y (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS X)) (DIFFERENCE Y (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z))))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP Y (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z))) (NEGATIVEP X) (NEGATIVEP Z) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NOT (LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS X)))) (EQUAL (DIFFERENCE (DIFFERENCE Y (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS X)) (DIFFERENCE Y (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z))))). But this again simplifies, using linear arithmetic, to: T. Case 9.2. (IMPLIES (AND (NEGATIVEP X) (NEGATIVEP Z) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NOT (LESSP Y (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z))))) (NOT (LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS X)))), which again simplifies, using linear arithmetic, to: T. Case 9.1. (IMPLIES (AND (NEGATIVEP X) (NEGATIVEP Z) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (LESSP Y (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)))) (LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS X))), which again simplifies, using linear arithmetic, to: T. Case 8. (IMPLIES (AND (NEGATIVEP X) (NEGATIVEP Z) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z))) (EQUAL (ZPLUS X (MINUS (DIFFERENCE (NEGATIVE-GUTS Z) Y))) (ZPLUS Y (MINUS (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)))))), which again simplifies, applying NEGATIVE-GUTS-MINUS, and expanding ZPLUS, to the following two new conjectures: Case 8.2. (IMPLIES (AND (NEGATIVEP X) (NEGATIVEP Z) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z))) (EQUAL (MINUS (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Z) Y))) (MINUS (DIFFERENCE (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)) Y)))). But this again simplifies, rewriting with NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to: (IMPLIES (AND (NEGATIVEP X) (NEGATIVEP Z) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z))) (EQUAL (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Z) Y)) (DIFFERENCE (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)) Y))), which again simplifies, using linear arithmetic, to two new conjectures: Case 8.2.2. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y) (NEGATIVEP X) (NEGATIVEP Z) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z))) (EQUAL (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Z) Y)) (DIFFERENCE (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)) Y))), which again simplifies, using linear arithmetic, to: T. Case 8.2.1. (IMPLIES (AND (LESSP (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)) Y) (NEGATIVEP X) (NEGATIVEP Z) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z))) (EQUAL (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Z) Y)) (DIFFERENCE (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)) Y))), which again simplifies, using linear arithmetic, to: T. Case 8.1. (IMPLIES (AND (NEGATIVEP X) (NEGATIVEP Z) (NOT (NEGATIVEP Y)) (LESSP Y (NEGATIVE-GUTS Z))) (LESSP Y (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)))), which again simplifies, using linear arithmetic, to: T. Case 7. (IMPLIES (AND (NEGATIVEP X) (NEGATIVEP Z) (NEGATIVEP Y)) (EQUAL (ZPLUS X (MINUS (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)))) (ZPLUS Y (MINUS (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Z)))))), which again simplifies, applying NEGATIVE-GUTS-MINUS and COMMUTATIVITY2-OF-PLUS, and opening up the definition of ZPLUS, to: T. Case 6. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NOT (NEGATIVEP Y))) (EQUAL (ZPLUS X (PLUS Y Z)) (ZPLUS Y (DIFFERENCE Z (NEGATIVE-GUTS X))))). However this again simplifies, opening up the function ZPLUS, to two new conjectures: Case 6.2. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NOT (NEGATIVEP Y))) (EQUAL (DIFFERENCE (PLUS Y Z) (NEGATIVE-GUTS X)) (PLUS Y (DIFFERENCE Z (NEGATIVE-GUTS X))))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (PLUS Y Z) (NEGATIVE-GUTS X)) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NOT (NEGATIVEP Y))) (EQUAL (DIFFERENCE (PLUS Y Z) (NEGATIVE-GUTS X)) (PLUS Y (DIFFERENCE Z (NEGATIVE-GUTS X))))). This again simplifies, using linear arithmetic, to: T. Case 6.1. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NOT (NEGATIVEP Y))) (NOT (LESSP (PLUS Y Z) (NEGATIVE-GUTS X)))), which again simplifies, using linear arithmetic, to: T. Case 5. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y)))) (EQUAL (ZPLUS X (DIFFERENCE Z (NEGATIVE-GUTS Y))) (ZPLUS Y (DIFFERENCE Z (NEGATIVE-GUTS X))))), which again simplifies, expanding ZPLUS, to four new conjectures: Case 5.4. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (LESSP (DIFFERENCE Z (NEGATIVE-GUTS X)) (NEGATIVE-GUTS Y))) (EQUAL (MINUS (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Z (NEGATIVE-GUTS Y)))) (MINUS (DIFFERENCE (NEGATIVE-GUTS Y) (DIFFERENCE Z (NEGATIVE-GUTS X)))))), which again simplifies, applying NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to the new goal: (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (LESSP (DIFFERENCE Z (NEGATIVE-GUTS X)) (NEGATIVE-GUTS Y))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Z (NEGATIVE-GUTS Y))) (DIFFERENCE (NEGATIVE-GUTS Y) (DIFFERENCE Z (NEGATIVE-GUTS X))))), which again simplifies, using linear arithmetic, to two new conjectures: Case 5.4.2. (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) (DIFFERENCE Z (NEGATIVE-GUTS Y))) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (LESSP (DIFFERENCE Z (NEGATIVE-GUTS X)) (NEGATIVE-GUTS Y))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Z (NEGATIVE-GUTS Y))) (DIFFERENCE (NEGATIVE-GUTS Y) (DIFFERENCE Z (NEGATIVE-GUTS X))))), which again simplifies, using linear arithmetic, to: T. Case 5.4.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) (DIFFERENCE Z (NEGATIVE-GUTS X))) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (LESSP (DIFFERENCE Z (NEGATIVE-GUTS X)) (NEGATIVE-GUTS Y))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Z (NEGATIVE-GUTS Y))) (DIFFERENCE (NEGATIVE-GUTS Y) (DIFFERENCE Z (NEGATIVE-GUTS X))))), which again simplifies, using linear arithmetic, to: T. Case 5.3. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (NOT (LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y)) (NEGATIVE-GUTS X)))) (EQUAL (DIFFERENCE (DIFFERENCE Z (NEGATIVE-GUTS Y)) (NEGATIVE-GUTS X)) (DIFFERENCE (DIFFERENCE Z (NEGATIVE-GUTS X)) (NEGATIVE-GUTS Y)))), which again simplifies, using linear arithmetic, to the formula: (IMPLIES (AND (LESSP (DIFFERENCE Z (NEGATIVE-GUTS X)) (NEGATIVE-GUTS Y)) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (NOT (LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y)) (NEGATIVE-GUTS X)))) (EQUAL (DIFFERENCE (DIFFERENCE Z (NEGATIVE-GUTS Y)) (NEGATIVE-GUTS X)) (DIFFERENCE (DIFFERENCE Z (NEGATIVE-GUTS X)) (NEGATIVE-GUTS Y)))). But this again simplifies, using linear arithmetic, to: T. Case 5.2. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (NOT (LESSP (DIFFERENCE Z (NEGATIVE-GUTS X)) (NEGATIVE-GUTS Y)))) (NOT (LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y)) (NEGATIVE-GUTS X)))), which again simplifies, using linear arithmetic, to: T. Case 5.1. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (LESSP (DIFFERENCE Z (NEGATIVE-GUTS X)) (NEGATIVE-GUTS Y))) (LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y)) (NEGATIVE-GUTS X))), which again simplifies, using linear arithmetic, to: T. Case 4. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y))) (EQUAL (ZPLUS X (MINUS (DIFFERENCE (NEGATIVE-GUTS Y) Z))) (ZPLUS Y (DIFFERENCE Z (NEGATIVE-GUTS X))))), which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and opening up the function ZPLUS, to the following two new conjectures: Case 4.2. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y))) (EQUAL (MINUS (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Y) Z))) (MINUS (DIFFERENCE (NEGATIVE-GUTS Y) (DIFFERENCE Z (NEGATIVE-GUTS X)))))). However this again simplifies, applying NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to: (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y))) (EQUAL (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Y) Z)) (DIFFERENCE (NEGATIVE-GUTS Y) (DIFFERENCE Z (NEGATIVE-GUTS X))))), which again simplifies, using linear arithmetic, to two new formulas: Case 4.2.2. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y))) (EQUAL (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Y) Z)) (DIFFERENCE (NEGATIVE-GUTS Y) (DIFFERENCE Z (NEGATIVE-GUTS X))))), which again simplifies, using linear arithmetic, to: T. Case 4.2.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) (DIFFERENCE Z (NEGATIVE-GUTS X))) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y))) (EQUAL (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Y) Z)) (DIFFERENCE (NEGATIVE-GUTS Y) (DIFFERENCE Z (NEGATIVE-GUTS X))))), which again simplifies, using linear arithmetic, to: T. Case 4.1. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS X))) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y))) (LESSP (DIFFERENCE Z (NEGATIVE-GUTS X)) (NEGATIVE-GUTS Y))), which again simplifies, using linear arithmetic, to: T. Case 3. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y))) (EQUAL (ZPLUS X (PLUS Y Z)) (ZPLUS Y (MINUS (DIFFERENCE (NEGATIVE-GUTS X) Z))))), which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and unfolding the function ZPLUS, to the following four new conjectures: Case 3.4. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS X) Z))) (EQUAL (MINUS (DIFFERENCE (NEGATIVE-GUTS X) (PLUS Y Z))) (MINUS (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Z) Y)))). However this again simplifies, rewriting with NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to: (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS X) Z))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS X) (PLUS Y Z)) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Z) Y))), which again simplifies, using linear arithmetic, to three new conjectures: Case 3.4.3. (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) (PLUS Y Z)) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS X) Z))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS X) (PLUS Y Z)) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Z) Y))), which again simplifies, using linear arithmetic, to the goal: (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Z) (LESSP (NEGATIVE-GUTS X) (PLUS Y Z)) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS X) Z))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS X) (PLUS Y Z)) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Z) Y))). But this again simplifies, using linear arithmetic, to: T. Case 3.4.2. (IMPLIES (AND (LESSP (DIFFERENCE (NEGATIVE-GUTS X) Z) Y) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS X) Z))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS X) (PLUS Y Z)) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Z) Y))), which again simplifies, using linear arithmetic, to the conjecture: (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Z) (LESSP (DIFFERENCE (NEGATIVE-GUTS X) Z) Y) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS X) Z))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS X) (PLUS Y Z)) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Z) Y))). But this again simplifies, using linear arithmetic, to: T. Case 3.4.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Z) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS X) Z))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS X) (PLUS Y Z)) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Z) Y))), which again simplifies, using linear arithmetic, to: T. Case 3.3. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y)) (NOT (LESSP (PLUS Y Z) (NEGATIVE-GUTS X)))) (EQUAL (DIFFERENCE (PLUS Y Z) (NEGATIVE-GUTS X)) (DIFFERENCE Y (DIFFERENCE (NEGATIVE-GUTS X) Z)))), which again simplifies, using linear arithmetic, to two new goals: Case 3.3.2. (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Z) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y)) (NOT (LESSP (PLUS Y Z) (NEGATIVE-GUTS X)))) (EQUAL (DIFFERENCE (PLUS Y Z) (NEGATIVE-GUTS X)) (DIFFERENCE Y (DIFFERENCE (NEGATIVE-GUTS X) Z)))), which again simplifies, using linear arithmetic, to: T. Case 3.3.1. (IMPLIES (AND (LESSP Y (DIFFERENCE (NEGATIVE-GUTS X) Z)) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y)) (NOT (LESSP (PLUS Y Z) (NEGATIVE-GUTS X)))) (EQUAL (DIFFERENCE (PLUS Y Z) (NEGATIVE-GUTS X)) (DIFFERENCE Y (DIFFERENCE (NEGATIVE-GUTS X) Z)))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Z) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS X) Z)) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y)) (NOT (LESSP (PLUS Y Z) (NEGATIVE-GUTS X)))) (EQUAL (DIFFERENCE (PLUS Y Z) (NEGATIVE-GUTS X)) (DIFFERENCE Y (DIFFERENCE (NEGATIVE-GUTS X) Z)))). However this again simplifies, using linear arithmetic, to: T. Case 3.2. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y)) (NOT (LESSP Y (DIFFERENCE (NEGATIVE-GUTS X) Z)))) (NOT (LESSP (PLUS Y Z) (NEGATIVE-GUTS X)))), which again simplifies, using linear arithmetic, to: T. Case 3.1. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS X) Z))) (LESSP (PLUS Y Z) (NEGATIVE-GUTS X))), which again simplifies, using linear arithmetic, to the formula: (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Z) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y)) (LESSP Y (DIFFERENCE (NEGATIVE-GUTS X) Z))) (LESSP (PLUS Y Z) (NEGATIVE-GUTS X))). This again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y)))) (EQUAL (ZPLUS X (DIFFERENCE Z (NEGATIVE-GUTS Y))) (ZPLUS Y (MINUS (DIFFERENCE (NEGATIVE-GUTS X) Z))))), which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and unfolding the function ZPLUS, to the following two new formulas: Case 2.2. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y)))) (EQUAL (MINUS (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Z (NEGATIVE-GUTS Y)))) (MINUS (PLUS (NEGATIVE-GUTS Y) (DIFFERENCE (NEGATIVE-GUTS X) Z))))). But this again simplifies, appealing to the lemmas NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to: (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y)))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Z (NEGATIVE-GUTS Y))) (PLUS (NEGATIVE-GUTS Y) (DIFFERENCE (NEGATIVE-GUTS X) Z)))). But this again simplifies, using linear arithmetic, to two new conjectures: Case 2.2.2. (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) (DIFFERENCE Z (NEGATIVE-GUTS Y))) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y)))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Z (NEGATIVE-GUTS Y))) (PLUS (NEGATIVE-GUTS Y) (DIFFERENCE (NEGATIVE-GUTS X) Z)))), which again simplifies, using linear arithmetic, to: T. Case 2.2.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Z) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y)))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Z (NEGATIVE-GUTS Y))) (PLUS (NEGATIVE-GUTS Y) (DIFFERENCE (NEGATIVE-GUTS X) Z)))), which again simplifies, using linear arithmetic, to: T. Case 2.1. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NEGATIVEP Y) (NOT (LESSP Z (NEGATIVE-GUTS Y)))) (LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y)) (NEGATIVE-GUTS X))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y))) (EQUAL (ZPLUS X (MINUS (DIFFERENCE (NEGATIVE-GUTS Y) Z))) (ZPLUS Y (MINUS (DIFFERENCE (NEGATIVE-GUTS X) Z))))), which again simplifies, applying NEGATIVE-GUTS-MINUS and MINUS-EQUAL, and expanding the function ZPLUS, to: (IMPLIES (AND (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y))) (EQUAL (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Y) Z)) (PLUS (NEGATIVE-GUTS Y) (DIFFERENCE (NEGATIVE-GUTS X) Z)))), which again simplifies, using linear arithmetic, to two new conjectures: Case 1.2. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y))) (EQUAL (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Y) Z)) (PLUS (NEGATIVE-GUTS Y) (DIFFERENCE (NEGATIVE-GUTS X) Z)))), which again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Z) (NEGATIVEP X) (NOT (NEGATIVEP Z)) (LESSP Z (NEGATIVE-GUTS X)) (NEGATIVEP Y) (LESSP Z (NEGATIVE-GUTS Y))) (EQUAL (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Y) Z)) (PLUS (NEGATIVE-GUTS Y) (DIFFERENCE (NEGATIVE-GUTS X) Z)))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.1 0.1 ] ZPLUS-COMM2 (PROVE-LEMMA ZPLUS-ASSOC (REWRITE) (EQUAL (ZPLUS (ZPLUS X Y) Z) (ZPLUS X (ZPLUS Y Z)))) WARNING: Note that the rewrite rule ZPLUS-ASSOC will be stored so as to apply only to terms with the nonrecursive function symbol ZPLUS. WARNING: the previously added lemma, ZPLUS-COMM1, could be applied whenever the newly proposed ZPLUS-ASSOC could! This simplifies, rewriting with ZPLUS-COMM1, and expanding ZPLUS, to 18 new formulas: Case 18.(IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NOT (NEGATIVEP X))) (EQUAL (ZPLUS Z (PLUS X Y)) (ZPLUS X (DIFFERENCE Y (NEGATIVE-GUTS Z))))), which again simplifies, opening up the definition of ZPLUS, to two new conjectures: Case 18.2. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NOT (NEGATIVEP X))) (EQUAL (DIFFERENCE (PLUS X Y) (NEGATIVE-GUTS Z)) (PLUS X (DIFFERENCE Y (NEGATIVE-GUTS Z))))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (PLUS X Y) (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NOT (NEGATIVEP X))) (EQUAL (DIFFERENCE (PLUS X Y) (NEGATIVE-GUTS Z)) (PLUS X (DIFFERENCE Y (NEGATIVE-GUTS Z))))). However this again simplifies, using linear arithmetic, to: T. Case 18.1. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NOT (NEGATIVEP X))) (NOT (LESSP (PLUS X Y) (NEGATIVE-GUTS Z)))), which again simplifies, using linear arithmetic, to: T. Case 17.(IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X)))) (EQUAL (ZPLUS Z (DIFFERENCE Y (NEGATIVE-GUTS X))) (ZPLUS X (DIFFERENCE Y (NEGATIVE-GUTS Z))))), which again simplifies, unfolding the function ZPLUS, to four new conjectures: Case 17.4. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X))) (LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS X))) (EQUAL (MINUS (DIFFERENCE (NEGATIVE-GUTS Z) (DIFFERENCE Y (NEGATIVE-GUTS X)))) (MINUS (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Y (NEGATIVE-GUTS Z)))))), which again simplifies, applying NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to the new conjecture: (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X))) (LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS X))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS Z) (DIFFERENCE Y (NEGATIVE-GUTS X))) (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Y (NEGATIVE-GUTS Z))))), which again simplifies, using linear arithmetic, to two new conjectures: Case 17.4.2. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) (DIFFERENCE Y (NEGATIVE-GUTS X))) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X))) (LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS X))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS Z) (DIFFERENCE Y (NEGATIVE-GUTS X))) (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Y (NEGATIVE-GUTS Z))))), which again simplifies, using linear arithmetic, to: T. Case 17.4.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) (DIFFERENCE Y (NEGATIVE-GUTS Z))) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X))) (LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS X))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS Z) (DIFFERENCE Y (NEGATIVE-GUTS X))) (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Y (NEGATIVE-GUTS Z))))), which again simplifies, using linear arithmetic, to: T. Case 17.3. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X))) (NOT (LESSP (DIFFERENCE Y (NEGATIVE-GUTS X)) (NEGATIVE-GUTS Z)))) (EQUAL (DIFFERENCE (DIFFERENCE Y (NEGATIVE-GUTS X)) (NEGATIVE-GUTS Z)) (DIFFERENCE (DIFFERENCE Y (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS X)))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X))) (NOT (LESSP (DIFFERENCE Y (NEGATIVE-GUTS X)) (NEGATIVE-GUTS Z)))) (EQUAL (DIFFERENCE (DIFFERENCE Y (NEGATIVE-GUTS X)) (NEGATIVE-GUTS Z)) (DIFFERENCE (DIFFERENCE Y (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS X)))). However this again simplifies, using linear arithmetic, to: T. Case 17.2. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X))) (NOT (LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS X)))) (NOT (LESSP (DIFFERENCE Y (NEGATIVE-GUTS X)) (NEGATIVE-GUTS Z)))), which again simplifies, using linear arithmetic, to: T. Case 17.1. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X))) (LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS X))) (LESSP (DIFFERENCE Y (NEGATIVE-GUTS X)) (NEGATIVE-GUTS Z))), which again simplifies, using linear arithmetic, to: T. Case 16.(IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X))) (EQUAL (ZPLUS Z (MINUS (DIFFERENCE (NEGATIVE-GUTS X) Y))) (ZPLUS X (DIFFERENCE Y (NEGATIVE-GUTS Z))))), which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and expanding the function ZPLUS, to the following two new goals: Case 16.2. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X))) (EQUAL (MINUS (PLUS (NEGATIVE-GUTS Z) (DIFFERENCE (NEGATIVE-GUTS X) Y))) (MINUS (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Y (NEGATIVE-GUTS Z)))))). However this again simplifies, applying NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to: (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X))) (EQUAL (PLUS (NEGATIVE-GUTS Z) (DIFFERENCE (NEGATIVE-GUTS X) Y)) (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Y (NEGATIVE-GUTS Z))))), which again simplifies, using linear arithmetic, to two new goals: Case 16.2.2. (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Y) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X))) (EQUAL (PLUS (NEGATIVE-GUTS Z) (DIFFERENCE (NEGATIVE-GUTS X) Y)) (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Y (NEGATIVE-GUTS Z))))), which again simplifies, using linear arithmetic, to: T. Case 16.2.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) (DIFFERENCE Y (NEGATIVE-GUTS Z))) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X))) (EQUAL (PLUS (NEGATIVE-GUTS Z) (DIFFERENCE (NEGATIVE-GUTS X) Y)) (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Y (NEGATIVE-GUTS Z))))), which again simplifies, using linear arithmetic, to: T. Case 16.1. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (NOT (LESSP Y (NEGATIVE-GUTS Z))) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X))) (LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z)) (NEGATIVE-GUTS X))), which again simplifies, using linear arithmetic, to: T. Case 15.(IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP X))) (EQUAL (ZPLUS Z (PLUS X Y)) (ZPLUS X (MINUS (DIFFERENCE (NEGATIVE-GUTS Z) Y))))), which again simplifies, applying NEGATIVE-GUTS-MINUS, and expanding the function ZPLUS, to the following four new goals: Case 15.4. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP X)) (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y))) (EQUAL (MINUS (DIFFERENCE (NEGATIVE-GUTS Z) (PLUS X Y))) (MINUS (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y) X)))). But this again simplifies, appealing to the lemmas NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to: (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP X)) (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS Z) (PLUS X Y)) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y) X))). However this again simplifies, using linear arithmetic, to three new goals: Case 15.4.3. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) (PLUS X Y)) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP X)) (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS Z) (PLUS X Y)) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y) X))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y) (LESSP (NEGATIVE-GUTS Z) (PLUS X Y)) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP X)) (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS Z) (PLUS X Y)) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y) X))). This again simplifies, using linear arithmetic, to: T. Case 15.4.2. (IMPLIES (AND (LESSP (DIFFERENCE (NEGATIVE-GUTS Z) Y) X) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP X)) (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS Z) (PLUS X Y)) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y) X))), which again simplifies, using linear arithmetic, to the formula: (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y) (LESSP (DIFFERENCE (NEGATIVE-GUTS Z) Y) X) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP X)) (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS Z) (PLUS X Y)) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y) X))). This again simplifies, using linear arithmetic, to: T. Case 15.4.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP X)) (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS Z) (PLUS X Y)) (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y) X))), which again simplifies, using linear arithmetic, to: T. Case 15.3. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP X)) (NOT (LESSP (PLUS X Y) (NEGATIVE-GUTS Z)))) (EQUAL (DIFFERENCE (PLUS X Y) (NEGATIVE-GUTS Z)) (DIFFERENCE X (DIFFERENCE (NEGATIVE-GUTS Z) Y)))), which again simplifies, using linear arithmetic, to two new conjectures: Case 15.3.2. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP X)) (NOT (LESSP (PLUS X Y) (NEGATIVE-GUTS Z)))) (EQUAL (DIFFERENCE (PLUS X Y) (NEGATIVE-GUTS Z)) (DIFFERENCE X (DIFFERENCE (NEGATIVE-GUTS Z) Y)))), which again simplifies, using linear arithmetic, to: T. Case 15.3.1. (IMPLIES (AND (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y)) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP X)) (NOT (LESSP (PLUS X Y) (NEGATIVE-GUTS Z)))) (EQUAL (DIFFERENCE (PLUS X Y) (NEGATIVE-GUTS Z)) (DIFFERENCE X (DIFFERENCE (NEGATIVE-GUTS Z) Y)))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y) (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y)) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP X)) (NOT (LESSP (PLUS X Y) (NEGATIVE-GUTS Z)))) (EQUAL (DIFFERENCE (PLUS X Y) (NEGATIVE-GUTS Z)) (DIFFERENCE X (DIFFERENCE (NEGATIVE-GUTS Z) Y)))). But this again simplifies, using linear arithmetic, to: T. Case 15.2. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP X)) (NOT (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y)))) (NOT (LESSP (PLUS X Y) (NEGATIVE-GUTS Z)))), which again simplifies, using linear arithmetic, to: T. Case 15.1. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP X)) (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y))) (LESSP (PLUS X Y) (NEGATIVE-GUTS Z))), which again simplifies, using linear arithmetic, to the goal: (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NOT (NEGATIVEP X)) (LESSP X (DIFFERENCE (NEGATIVE-GUTS Z) Y))) (LESSP (PLUS X Y) (NEGATIVE-GUTS Z))). This again simplifies, using linear arithmetic, to: T. Case 14.(IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X)))) (EQUAL (ZPLUS Z (DIFFERENCE Y (NEGATIVE-GUTS X))) (ZPLUS X (MINUS (DIFFERENCE (NEGATIVE-GUTS Z) Y))))), which again simplifies, rewriting with the lemma NEGATIVE-GUTS-MINUS, and unfolding the function ZPLUS, to two new formulas: Case 14.2. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X)))) (EQUAL (MINUS (DIFFERENCE (NEGATIVE-GUTS Z) (DIFFERENCE Y (NEGATIVE-GUTS X)))) (MINUS (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Z) Y))))), which again simplifies, rewriting with NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to: (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X)))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS Z) (DIFFERENCE Y (NEGATIVE-GUTS X))) (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Z) Y)))), which again simplifies, using linear arithmetic, to two new goals: Case 14.2.2. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) (DIFFERENCE Y (NEGATIVE-GUTS X))) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X)))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS Z) (DIFFERENCE Y (NEGATIVE-GUTS X))) (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Z) Y)))), which again simplifies, using linear arithmetic, to: T. Case 14.2.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X)))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS Z) (DIFFERENCE Y (NEGATIVE-GUTS X))) (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Z) Y)))), which again simplifies, using linear arithmetic, to: T. Case 14.1. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X)))) (LESSP (DIFFERENCE Y (NEGATIVE-GUTS X)) (NEGATIVE-GUTS Z))), which again simplifies, using linear arithmetic, to: T. Case 13.(IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X))) (EQUAL (ZPLUS Z (MINUS (DIFFERENCE (NEGATIVE-GUTS X) Y))) (ZPLUS X (MINUS (DIFFERENCE (NEGATIVE-GUTS Z) Y))))), which again simplifies, applying NEGATIVE-GUTS-MINUS and MINUS-EQUAL, and opening up ZPLUS, to: (IMPLIES (AND (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X))) (EQUAL (PLUS (NEGATIVE-GUTS Z) (DIFFERENCE (NEGATIVE-GUTS X) Y)) (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Z) Y)))), which again simplifies, using linear arithmetic, to two new formulas: Case 13.2. (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Y) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X))) (EQUAL (PLUS (NEGATIVE-GUTS Z) (DIFFERENCE (NEGATIVE-GUTS X) Y)) (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Z) Y)))), which again simplifies, using linear arithmetic, to: T. Case 13.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y) (NOT (NEGATIVEP Y)) (NEGATIVEP Z) (LESSP Y (NEGATIVE-GUTS Z)) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X))) (EQUAL (PLUS (NEGATIVE-GUTS Z) (DIFFERENCE (NEGATIVE-GUTS X) Y)) (PLUS (NEGATIVE-GUTS X) (DIFFERENCE (NEGATIVE-GUTS Z) Y)))), which again simplifies, using linear arithmetic, to: T. Case 12.(IMPLIES (AND (NOT (NEGATIVEP Y)) (NOT (NEGATIVEP Z)) (NOT (NEGATIVEP X))) (EQUAL (ZPLUS Z (PLUS X Y)) (ZPLUS X (PLUS Y Z)))), which again simplifies, applying COMMUTATIVITY2-OF-PLUS and COMMUTATIVITY-OF-PLUS, and opening up ZPLUS, to: T. Case 11.(IMPLIES (AND (NOT (NEGATIVEP Y)) (NOT (NEGATIVEP Z)) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X)))) (EQUAL (ZPLUS Z (DIFFERENCE Y (NEGATIVE-GUTS X))) (ZPLUS X (PLUS Y Z)))). But this again simplifies, expanding ZPLUS, to two new formulas: Case 11.2. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NOT (NEGATIVEP Z)) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X)))) (EQUAL (PLUS Z (DIFFERENCE Y (NEGATIVE-GUTS X))) (DIFFERENCE (PLUS Y Z) (NEGATIVE-GUTS X)))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (PLUS Y Z) (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y)) (NOT (NEGATIVEP Z)) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X)))) (EQUAL (PLUS Z (DIFFERENCE Y (NEGATIVE-GUTS X))) (DIFFERENCE (PLUS Y Z) (NEGATIVE-GUTS X)))). However this again simplifies, using linear arithmetic, to: T. Case 11.1. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NOT (NEGATIVEP Z)) (NEGATIVEP X) (NOT (LESSP Y (NEGATIVE-GUTS X)))) (NOT (LESSP (PLUS Y Z) (NEGATIVE-GUTS X)))), which again simplifies, using linear arithmetic, to: T. Case 10.(IMPLIES (AND (NOT (NEGATIVEP Y)) (NOT (NEGATIVEP Z)) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X))) (EQUAL (ZPLUS Z (MINUS (DIFFERENCE (NEGATIVE-GUTS X) Y))) (ZPLUS X (PLUS Y Z)))), which again simplifies, applying NEGATIVE-GUTS-MINUS, and opening up the function ZPLUS, to the following four new formulas: Case 10.4. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NOT (NEGATIVEP Z)) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X)) (LESSP (PLUS Y Z) (NEGATIVE-GUTS X))) (EQUAL (MINUS (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Y) Z)) (MINUS (DIFFERENCE (NEGATIVE-GUTS X) (PLUS Y Z))))). This again simplifies, rewriting with NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to: (IMPLIES (AND (NOT (NEGATIVEP Y)) (NOT (NEGATIVEP Z)) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X)) (LESSP (PLUS Y Z) (NEGATIVE-GUTS X))) (EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Y) Z) (DIFFERENCE (NEGATIVE-GUTS X) (PLUS Y Z)))), which again simplifies, using linear arithmetic, to three new conjectures: Case 10.4.3. (IMPLIES (AND (LESSP (DIFFERENCE (NEGATIVE-GUTS X) Y) Z) (NOT (NEGATIVEP Y)) (NOT (NEGATIVEP Z)) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X)) (LESSP (PLUS Y Z) (NEGATIVE-GUTS X))) (EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Y) Z) (DIFFERENCE (NEGATIVE-GUTS X) (PLUS Y Z)))), which again simplifies, using linear arithmetic, to: T. Case 10.4.2. (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Y) (NOT (NEGATIVEP Y)) (NOT (NEGATIVEP Z)) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X)) (LESSP (PLUS Y Z) (NEGATIVE-GUTS X))) (EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Y) Z) (DIFFERENCE (NEGATIVE-GUTS X) (PLUS Y Z)))), which again simplifies, using linear arithmetic, to: T. Case 10.4.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) (PLUS Y Z)) (NOT (NEGATIVEP Y)) (NOT (NEGATIVEP Z)) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X)) (LESSP (PLUS Y Z) (NEGATIVE-GUTS X))) (EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Y) Z) (DIFFERENCE (NEGATIVE-GUTS X) (PLUS Y Z)))), which again simplifies, using linear arithmetic, to: T. Case 10.3. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NOT (NEGATIVEP Z)) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X)) (NOT (LESSP Z (DIFFERENCE (NEGATIVE-GUTS X) Y)))) (EQUAL (DIFFERENCE Z (DIFFERENCE (NEGATIVE-GUTS X) Y)) (DIFFERENCE (PLUS Y Z) (NEGATIVE-GUTS X)))), which again simplifies, using linear arithmetic, to two new conjectures: Case 10.3.2. (IMPLIES (AND (LESSP (PLUS Y Z) (NEGATIVE-GUTS X)) (NOT (NEGATIVEP Y)) (NOT (NEGATIVEP Z)) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X)) (NOT (LESSP Z (DIFFERENCE (NEGATIVE-GUTS X) Y)))) (EQUAL (DIFFERENCE Z (DIFFERENCE (NEGATIVE-GUTS X) Y)) (DIFFERENCE (PLUS Y Z) (NEGATIVE-GUTS X)))), which again simplifies, using linear arithmetic, to: T. Case 10.3.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Y) (NOT (NEGATIVEP Y)) (NOT (NEGATIVEP Z)) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X)) (NOT (LESSP Z (DIFFERENCE (NEGATIVE-GUTS X) Y)))) (EQUAL (DIFFERENCE Z (DIFFERENCE (NEGATIVE-GUTS X) Y)) (DIFFERENCE (PLUS Y Z) (NEGATIVE-GUTS X)))), which again simplifies, using linear arithmetic, to: T. Case 10.2. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NOT (NEGATIVEP Z)) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X)) (NOT (LESSP (PLUS Y Z) (NEGATIVE-GUTS X)))) (NOT (LESSP Z (DIFFERENCE (NEGATIVE-GUTS X) Y)))), which again simplifies, using linear arithmetic, to the goal: (IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Y) (NOT (NEGATIVEP Y)) (NOT (NEGATIVEP Z)) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X)) (NOT (LESSP (PLUS Y Z) (NEGATIVE-GUTS X)))) (NOT (LESSP Z (DIFFERENCE (NEGATIVE-GUTS X) Y)))). But this again simplifies, using linear arithmetic, to: T. Case 10.1. (IMPLIES (AND (NOT (NEGATIVEP Y)) (NOT (NEGATIVEP Z)) (NEGATIVEP X) (LESSP Y (NEGATIVE-GUTS X)) (LESSP (PLUS Y Z) (NEGATIVE-GUTS X))) (LESSP Z (DIFFERENCE (NEGATIVE-GUTS X) Y))), which again simplifies, using linear arithmetic, to: T. Case 9. (IMPLIES (AND (NEGATIVEP Y) (NEGATIVEP Z) (NOT (NEGATIVEP X)) (NOT (LESSP X (NEGATIVE-GUTS Y)))) (EQUAL (ZPLUS Z (DIFFERENCE X (NEGATIVE-GUTS Y))) (ZPLUS X (MINUS (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)))))), which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and opening up the definition of ZPLUS, to the following four new conjectures: Case 9.4. (IMPLIES (AND (NEGATIVEP Y) (NEGATIVEP Z) (NOT (NEGATIVEP X)) (NOT (LESSP X (NEGATIVE-GUTS Y))) (LESSP X (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)))) (EQUAL (MINUS (DIFFERENCE (NEGATIVE-GUTS Z) (DIFFERENCE X (NEGATIVE-GUTS Y)))) (MINUS (DIFFERENCE (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X)))). This again simplifies, applying NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to: (IMPLIES (AND (NEGATIVEP Y) (NEGATIVEP Z) (NOT (NEGATIVEP X)) (NOT (LESSP X (NEGATIVE-GUTS Y))) (LESSP X (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS Z) (DIFFERENCE X (NEGATIVE-GUTS Y))) (DIFFERENCE (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X))), which again simplifies, using linear arithmetic, to two new goals: Case 9.4.2. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) (DIFFERENCE X (NEGATIVE-GUTS Y))) (NEGATIVEP Y) (NEGATIVEP Z) (NOT (NEGATIVEP X)) (NOT (LESSP X (NEGATIVE-GUTS Y))) (LESSP X (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS Z) (DIFFERENCE X (NEGATIVE-GUTS Y))) (DIFFERENCE (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X))), which again simplifies, using linear arithmetic, to: T. Case 9.4.1. (IMPLIES (AND (LESSP (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X) (NEGATIVEP Y) (NEGATIVEP Z) (NOT (NEGATIVEP X)) (NOT (LESSP X (NEGATIVE-GUTS Y))) (LESSP X (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)))) (EQUAL (DIFFERENCE (NEGATIVE-GUTS Z) (DIFFERENCE X (NEGATIVE-GUTS Y))) (DIFFERENCE (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X))), which again simplifies, using linear arithmetic, to: T. Case 9.3. (IMPLIES (AND (NEGATIVEP Y) (NEGATIVEP Z) (NOT (NEGATIVEP X)) (NOT (LESSP X (NEGATIVE-GUTS Y))) (NOT (LESSP (DIFFERENCE X (NEGATIVE-GUTS Y)) (NEGATIVE-GUTS Z)))) (EQUAL (DIFFERENCE (DIFFERENCE X (NEGATIVE-GUTS Y)) (NEGATIVE-GUTS Z)) (DIFFERENCE X (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z))))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP X (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z))) (NEGATIVEP Y) (NEGATIVEP Z) (NOT (NEGATIVEP X)) (NOT (LESSP X (NEGATIVE-GUTS Y))) (NOT (LESSP (DIFFERENCE X (NEGATIVE-GUTS Y)) (NEGATIVE-GUTS Z)))) (EQUAL (DIFFERENCE (DIFFERENCE X (NEGATIVE-GUTS Y)) (NEGATIVE-GUTS Z)) (DIFFERENCE X (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z))))). But this again simplifies, using linear arithmetic, to: T. Case 9.2. (IMPLIES (AND (NEGATIVEP Y) (NEGATIVEP Z) (NOT (NEGATIVEP X)) (NOT (LESSP X (NEGATIVE-GUTS Y))) (NOT (LESSP X (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z))))) (NOT (LESSP (DIFFERENCE X (NEGATIVE-GUTS Y)) (NEGATIVE-GUTS Z)))), which again simplifies, using linear arithmetic, to: T. Case 9.1. (IMPLIES (AND (NEGATIVEP Y) (NEGATIVEP Z) (NOT (NEGATIVEP X)) (NOT (LESSP X (NEGATIVE-GUTS Y))) (LESSP X (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)))) (LESSP (DIFFERENCE X (NEGATIVE-GUTS Y)) (NEGATIVE-GUTS Z))), which again simplifies, using linear arithmetic, to: T. Case 8. (IMPLIES (AND (NEGATIVEP Y) (NEGATIVEP Z) (NOT (NEGATIVEP X)) (LESSP X (NEGATIVE-GUTS Y))) (EQUAL (ZPLUS Z (MINUS (DIFFERENCE (NEGATIVE-GUTS Y) X))) (ZPLUS X (MINUS (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)))))), which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and opening up ZPLUS, to the following two new formulas: Case 8.2. (IMPLIES (AND (NEGATIVEP Y) (NEGATIVEP Z) (NOT (NEGATIVEP X)) (LESSP X (NEGATIVE-GUTS Y))) (EQUAL (MINUS (PLUS (NEGATIVE-GUTS Z) (DIFFERENCE (NEGATIVE-GUTS Y) X))) (MINUS (DIFFERENCE (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X)))). However this again simplifies, rewriting with NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to: (IMPLIES (AND (NEGATIVEP Y) (NEGATIVEP Z) (NOT (NEGATIVEP X)) (LESSP X (NEGATIVE-GUTS Y))) (EQUAL (PLUS (NEGATIVE-GUTS Z) (DIFFERENCE (NEGATIVE-GUTS Y) X)) (DIFFERENCE (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X))), which again simplifies, using linear arithmetic, to two new formulas: Case 8.2.2. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) X) (NEGATIVEP Y) (NEGATIVEP Z) (NOT (NEGATIVEP X)) (LESSP X (NEGATIVE-GUTS Y))) (EQUAL (PLUS (NEGATIVE-GUTS Z) (DIFFERENCE (NEGATIVE-GUTS Y) X)) (DIFFERENCE (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X))), which again simplifies, using linear arithmetic, to: T. Case 8.2.1. (IMPLIES (AND (LESSP (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X) (NEGATIVEP Y) (NEGATIVEP Z) (NOT (NEGATIVEP X)) (LESSP X (NEGATIVE-GUTS Y))) (EQUAL (PLUS (NEGATIVE-GUTS Z) (DIFFERENCE (NEGATIVE-GUTS Y) X)) (DIFFERENCE (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)) X))), which again simplifies, using linear arithmetic, to: T. Case 8.1. (IMPLIES (AND (NEGATIVEP Y) (NEGATIVEP Z) (NOT (NEGATIVEP X)) (LESSP X (NEGATIVE-GUTS Y))) (LESSP X (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)))), which again simplifies, using linear arithmetic, to: T. Case 7. (IMPLIES (AND (NEGATIVEP Y) (NEGATIVEP Z) (NEGATIVEP X)) (EQUAL (ZPLUS Z (MINUS (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Y)))) (ZPLUS X (MINUS (PLUS (NEGATIVE-GUTS Y) (NEGATIVE-GUTS Z)))))), which again simplifies, appealing to the lemmas COMMUTATIVITY2-OF-PLUS, COMMUTATIVITY-OF-PLUS, and NEGATIVE-GUTS-MINUS, and unfolding ZPLUS, to: T. Case 6. (IMPLIES (AND (NEGATIVEP Y) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (NOT (NEGATIVEP X)) (NOT (LESSP X (NEGATIVE-GUTS Y)))) (EQUAL (ZPLUS Z (DIFFERENCE X (NEGATIVE-GUTS Y))) (ZPLUS X (DIFFERENCE Z (NEGATIVE-GUTS Y))))), which again simplifies, opening up ZPLUS, to: (IMPLIES (AND (NEGATIVEP Y) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (NOT (NEGATIVEP X)) (NOT (LESSP X (NEGATIVE-GUTS Y)))) (EQUAL (PLUS Z (DIFFERENCE X (NEGATIVE-GUTS Y))) (PLUS X (DIFFERENCE Z (NEGATIVE-GUTS Y))))). However this again simplifies, using linear arithmetic, to: T. Case 5. (IMPLIES (AND (NEGATIVEP Y) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (NOT (NEGATIVEP X)) (LESSP X (NEGATIVE-GUTS Y))) (EQUAL (ZPLUS Z (MINUS (DIFFERENCE (NEGATIVE-GUTS Y) X))) (ZPLUS X (DIFFERENCE Z (NEGATIVE-GUTS Y))))), which again simplifies, appealing to the lemma NEGATIVE-GUTS-MINUS, and unfolding the definition of ZPLUS, to two new conjectures: Case 5.2. (IMPLIES (AND (NEGATIVEP Y) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (NOT (NEGATIVEP X)) (LESSP X (NEGATIVE-GUTS Y))) (EQUAL (DIFFERENCE Z (DIFFERENCE (NEGATIVE-GUTS Y) X)) (PLUS X (DIFFERENCE Z (NEGATIVE-GUTS Y))))), which again simplifies, using linear arithmetic, to two new goals: Case 5.2.2. (IMPLIES (AND (LESSP Z (DIFFERENCE (NEGATIVE-GUTS Y) X)) (NEGATIVEP Y) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (NOT (NEGATIVEP X)) (LESSP X (NEGATIVE-GUTS Y))) (EQUAL (DIFFERENCE Z (DIFFERENCE (NEGATIVE-GUTS Y) X)) (PLUS X (DIFFERENCE Z (NEGATIVE-GUTS Y))))), which again simplifies, using linear arithmetic, to the formula: (IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) X) (LESSP Z (DIFFERENCE (NEGATIVE-GUTS Y) X)) (NEGATIVEP Y) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (NOT (NEGATIVEP X)) (LESSP X (NEGATIVE-GUTS Y))) (EQUAL (DIFFERENCE Z (DIFFERENCE (NEGATIVE-GUTS Y) X)) (PLUS X (DIFFERENCE Z (NEGATIVE-GUTS Y))))). This again simplifies, using linear arithmetic, to: T. Case 5.2.1. (IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) X) (NEGATIVEP Y) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (NOT (NEGATIVEP X)) (LESSP X (NEGATIVE-GUTS Y))) (EQUAL (DIFFERENCE Z (DIFFERENCE (NEGATIVE-GUTS Y) X)) (PLUS X (DIFFERENCE Z (NEGATIVE-GUTS Y))))), which again simplifies, using linear arithmetic, to: T. Case 5.1. (IMPLIES (AND (NEGATIVEP Y) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (NOT (NEGATIVEP X)) (LESSP X (NEGATIVE-GUTS Y))) (NOT (LESSP Z (DIFFERENCE (NEGATIVE-GUTS Y) X)))), which again simplifies, using linear arithmetic, to the goal: (IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) X) (NEGATIVEP Y) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (NOT (NEGATIVEP X)) (LESSP X (NEGATIVE-GUTS Y))) (NOT (LESSP Z (DIFFERENCE (NEGATIVE-GUTS Y) X)))). But this again simplifies, using linear arithmetic, to: T. Case 4. (IMPLIES (AND (NEGATIVEP Y) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (NEGATIVEP X)) (EQUAL (ZPLUS Z (MINUS (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Y)))) (ZPLUS X (DIFFERENCE Z (NEGATIVE-GUTS Y))))), which again simplifies, applying NEGATIVE-GUTS-MINUS, and expanding the definition of ZPLUS, to the following four new formulas: Case 4.4. (IMPLIES (AND (NEGATIVEP Y) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (NEGATIVEP X) (LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y)) (NEGATIVE-GUTS X))) (EQUAL (MINUS (DIFFERENCE (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Y)) Z)) (MINUS (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Z (NEGATIVE-GUTS Y)))))). This again simplifies, rewriting with NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to: (IMPLIES (AND (NEGATIVEP Y) (NOT (NEGATIVEP Z)) (NOT (LESSP Z (NEGATIVE-GUTS Y))) (NEGATIVEP X) (LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y)) (NEGATIVE-GUTS X))) (EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS X) (NEGATIVE-GUTS Y)) Z) (DIFFERENCE (NEGATIVE-GUTS X) (DIFFERENCE Z (NEGATIVE-GUTS Y))))), which again simplifies