diff --git a/UnitTests/sat/QF_NIA/From_AProVE_2014__PastaA10.jar-obl-8__p11616_terminationG_0.smt2 b/UnitTests/sat/QF_NIA/From_AProVE_2014__PastaA10.jar-obl-8__p11616_terminationG_0.smt2
deleted file mode 100644
index bd4568da21653fce3d4bb0c059d9769082a009d0..0000000000000000000000000000000000000000
--- a/UnitTests/sat/QF_NIA/From_AProVE_2014__PastaA10.jar-obl-8__p11616_terminationG_0.smt2
+++ /dev/null
@@ -1,90 +0,0 @@
-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |
-Generated by: Cristina Borralleras, Daniel Larraz, Albert Oliveras, Enric Rodriguez-Carbonell, Albert Rubio
-Generated on: 2017-04-27
-Generator: VeryMax
-Application: Termination proving
-Target solver: barcelogic
-|)
-(set-info :license "https://creativecommons.org/licenses/by/4.0/")
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun Nl2arg11 () Int)
-(declare-fun Nl2arg21 () Int)
-(declare-fun Nl2arg12 () Int)
-(declare-fun Nl2arg22 () Int)
-(declare-fun lam0n0 () Int)
-(declare-fun lam0n1 () Int)
-(declare-fun lam0n2 () Int)
-(declare-fun Nl2CT1 () Int)
-(declare-fun Nl2CT2 () Int)
-(declare-fun lam1n0 () Int)
-(declare-fun lam1n1 () Int)
-(declare-fun lam1n2 () Int)
-(declare-fun lam2n0 () Int)
-(declare-fun lam2n1 () Int)
-(declare-fun lam2n2 () Int)
-(declare-fun lam3n0 () Int)
-(declare-fun lam3n1 () Int)
-(declare-fun lam3n2 () Int)
-(declare-fun lam4n0 () Int)
-(declare-fun lam4n1 () Int)
-(declare-fun lam4n2 () Int)
-(declare-fun lam5n0 () Int)
-(declare-fun lam5n1 () Int)
-(declare-fun lam5n2 () Int)
-(declare-fun lam6n0 () Int)
-(declare-fun lam6n1 () Int)
-(declare-fun lam6n2 () Int)
-(declare-fun lam6n3 () Int)
-(declare-fun lam6n4 () Int)
-(declare-fun lam6n5 () Int)
-(declare-fun lam7n0 () Int)
-(declare-fun lam7n1 () Int)
-(declare-fun lam7n2 () Int)
-(declare-fun lam7n3 () Int)
-(declare-fun lam7n4 () Int)
-(declare-fun lam7n5 () Int)
-(declare-fun undef7 () Int)
-(declare-fun undef1 () Int)
-(declare-fun undef2 () Int)
-(declare-fun undef8 () Int)
-(declare-fun arg1 () Int)
-(declare-fun arg2 () Int)
-(declare-fun lam11n0 () Int)
-(declare-fun lam11n1 () Int)
-(declare-fun lam11n2 () Int)
-(declare-fun RFN1_CT () Int)
-(declare-fun RFN1_arg1 () Int)
-(declare-fun RFN1_arg2 () Int)
-(declare-fun lam15n0 () Int)
-(declare-fun lam15n1 () Int)
-(declare-fun lam15n2 () Int)
-(declare-fun lam9n0 () Int)
-(declare-fun lam9n1 () Int)
-(declare-fun lam9n2 () Int)
-(declare-fun lam10n0 () Int)
-(declare-fun lam10n1 () Int)
-(declare-fun lam10n2 () Int)
-(declare-fun lam13n0 () Int)
-(declare-fun lam13n1 () Int)
-(declare-fun lam13n2 () Int)
-(declare-fun lam14n0 () Int)
-(declare-fun lam14n1 () Int)
-(declare-fun lam14n2 () Int)
-(declare-fun lam8n0 () Int)
-(declare-fun lam8n1 () Int)
-(declare-fun lam8n2 () Int)
-(declare-fun lam12n0 () Int)
-(declare-fun lam12n1 () Int)
-(declare-fun lam12n2 () Int)
-(assert ( and ( <= ( - 1 ) Nl2arg11 ) ( <= Nl2arg11 1 ) ( <= ( - 1 ) Nl2arg21 ) ( <= Nl2arg21 1 ) ( <= ( - 1 ) Nl2arg12 ) ( <= Nl2arg12 1 ) ( <= ( - 1 ) Nl2arg22 ) ( <= Nl2arg22 1 ) ))
-(assert ( or ( and ( >= lam0n0 0 ) ( >= lam0n1 0 ) ( >= lam0n2 0 ) ( > ( + ( * 1 lam0n0 ) ( * Nl2CT1 lam0n1 ) ( * Nl2CT2 lam0n2 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * Nl2arg11 lam0n1 ) ( * Nl2arg12 lam0n2 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * Nl2arg21 lam0n1 ) ( * Nl2arg22 lam0n2 ) ) 0 ) ) ( and ( >= lam1n0 0 ) ( >= lam1n1 0 ) ( >= lam1n2 0 ) ( > ( + ( * 1 lam1n0 ) ( * Nl2CT1 lam1n1 ) ( * Nl2CT2 lam1n2 ) ( - 1 ( + Nl2CT1 ( * Nl2arg11 1 ) ) ) ) 0 ) ( = ( + ( * 1 lam1n0 ) ( * Nl2arg11 lam1n1 ) ( * Nl2arg12 lam1n2 ) ( - ( + 0 ( * Nl2arg11 1 ) ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam1n0 ) ( * Nl2arg21 lam1n1 ) ( * Nl2arg22 lam1n2 ) ( - ( + 0 Nl2arg21 ) ) ) 0 ) ) ))
-(assert ( or ( and ( >= lam0n0 0 ) ( >= lam0n1 0 ) ( >= lam0n2 0 ) ( > ( + ( * 1 lam0n0 ) ( * Nl2CT1 lam0n1 ) ( * Nl2CT2 lam0n2 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * Nl2arg11 lam0n1 ) ( * Nl2arg12 lam0n2 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * Nl2arg21 lam0n1 ) ( * Nl2arg22 lam0n2 ) ) 0 ) ) ( and ( >= lam2n0 0 ) ( >= lam2n1 0 ) ( >= lam2n2 0 ) ( > ( + ( * 1 lam2n0 ) ( * Nl2CT1 lam2n1 ) ( * Nl2CT2 lam2n2 ) ( - 1 ( + Nl2CT2 ( * Nl2arg12 1 ) ) ) ) 0 ) ( = ( + ( * 1 lam2n0 ) ( * Nl2arg11 lam2n1 ) ( * Nl2arg12 lam2n2 ) ( - ( + 0 ( * Nl2arg12 1 ) ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam2n0 ) ( * Nl2arg21 lam2n1 ) ( * Nl2arg22 lam2n2 ) ( - ( + 0 Nl2arg22 ) ) ) 0 ) ) ))
-(assert ( or ( and ( >= lam3n0 0 ) ( >= lam3n1 0 ) ( >= lam3n2 0 ) ( > ( + ( * 1 lam3n0 ) ( * Nl2CT1 lam3n1 ) ( * Nl2CT2 lam3n2 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam3n0 ) ( * Nl2arg11 lam3n1 ) ( * Nl2arg12 lam3n2 ) ) 0 ) ( = ( + ( * 1 lam3n0 ) ( * Nl2arg21 lam3n1 ) ( * Nl2arg22 lam3n2 ) ) 0 ) ) ( and ( >= lam4n0 0 ) ( >= lam4n1 0 ) ( >= lam4n2 0 ) ( > ( + ( * 1 lam4n0 ) ( * Nl2CT1 lam4n1 ) ( * Nl2CT2 lam4n2 ) ( - 1 ( + Nl2CT1 ( * Nl2arg21 1 ) ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam4n0 ) ( * Nl2arg11 lam4n1 ) ( * Nl2arg12 lam4n2 ) ( - ( + 0 Nl2arg11 ) ) ) 0 ) ( = ( + ( * 1 lam4n0 ) ( * Nl2arg21 lam4n1 ) ( * Nl2arg22 lam4n2 ) ( - ( + 0 ( * Nl2arg21 1 ) ) ) ) 0 ) ) ))
-(assert ( or ( and ( >= lam3n0 0 ) ( >= lam3n1 0 ) ( >= lam3n2 0 ) ( > ( + ( * 1 lam3n0 ) ( * Nl2CT1 lam3n1 ) ( * Nl2CT2 lam3n2 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam3n0 ) ( * Nl2arg11 lam3n1 ) ( * Nl2arg12 lam3n2 ) ) 0 ) ( = ( + ( * 1 lam3n0 ) ( * Nl2arg21 lam3n1 ) ( * Nl2arg22 lam3n2 ) ) 0 ) ) ( and ( >= lam5n0 0 ) ( >= lam5n1 0 ) ( >= lam5n2 0 ) ( > ( + ( * 1 lam5n0 ) ( * Nl2CT1 lam5n1 ) ( * Nl2CT2 lam5n2 ) ( - 1 ( + Nl2CT2 ( * Nl2arg22 1 ) ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam5n0 ) ( * Nl2arg11 lam5n1 ) ( * Nl2arg12 lam5n2 ) ( - ( + 0 Nl2arg12 ) ) ) 0 ) ( = ( + ( * 1 lam5n0 ) ( * Nl2arg21 lam5n1 ) ( * Nl2arg22 lam5n2 ) ( - ( + 0 ( * Nl2arg22 1 ) ) ) ) 0 ) ) ))
-(assert ( and ( <= ( + 1 ( * ( - 1 ) undef7 ) ) 0 ) ( <= ( * ( - 1 ) undef1 ) 0 ) ( <= ( * ( - 1 ) undef2 ) 0 ) ( <= ( * ( - 1 ) undef8 ) 0 ) ( = ( + arg1 ( * ( - 1 ) undef1 ) ) 0 ) ( = ( + arg2 ( * ( - 1 ) undef2 ) ) 0 ) ( <= ( + Nl2CT1 ( * ( + 0 Nl2arg11 ) arg1 ) ( * ( + 0 Nl2arg21 ) arg2 ) ) 0 ) ( <= ( + Nl2CT2 ( * ( + 0 Nl2arg12 ) arg1 ) ( * ( + 0 Nl2arg22 ) arg2 ) ) 0 ) ))
-(assert ( or ( and ( and ( and ( >= lam11n0 0 ) ( >= lam11n1 0 ) ( >= lam11n2 0 ) ( > ( + ( * 1 lam11n0 ) ( * Nl2CT1 lam11n1 ) ( * Nl2CT2 lam11n2 ) ( - 1 ( - ( + RFN1_CT ( * RFN1_arg1 1 ) ) RFN1_CT ) ) ) 0 ) ( = ( + ( * 1 lam11n0 ) ( * Nl2arg11 lam11n1 ) ( * Nl2arg12 lam11n2 ) ( - ( - ( + 0 ( * RFN1_arg1 1 ) ) RFN1_arg1 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam11n0 ) ( * Nl2arg21 lam11n1 ) ( * Nl2arg22 lam11n2 ) ( - ( - ( + 0 RFN1_arg2 ) RFN1_arg2 ) ) ) 0 ) ) ( and ( >= lam15n0 0 ) ( >= lam15n1 0 ) ( >= lam15n2 0 ) ( > ( + ( * 1 lam15n0 ) ( * Nl2CT1 lam15n1 ) ( * Nl2CT2 lam15n2 ) ( - 1 ( - ( + RFN1_CT ( * RFN1_arg2 1 ) ) RFN1_CT ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam15n0 ) ( * Nl2arg11 lam15n1 ) ( * Nl2arg12 lam15n2 ) ( - ( - ( + 0 RFN1_arg1 ) RFN1_arg1 ) ) ) 0 ) ( = ( + ( * 1 lam15n0 ) ( * Nl2arg21 lam15n1 ) ( * Nl2arg22 lam15n2 ) ( - ( - ( + 0 ( * RFN1_arg2 1 ) ) RFN1_arg2 ) ) ) 0 ) ) ) ( or ( and ( and ( >= lam9n0 0 ) ( >= lam9n1 0 ) ( >= lam9n2 0 ) ( > ( + ( * 1 lam9n0 ) ( * Nl2CT1 lam9n1 ) ( * Nl2CT2 lam9n2 ) ( - 1 ( - RFN1_CT ) ) ) 0 ) ( = ( + ( * 1 lam9n0 ) ( * Nl2arg11 lam9n1 ) ( * Nl2arg12 lam9n2 ) ( - ( - RFN1_arg1 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam9n0 ) ( * Nl2arg21 lam9n1 ) ( * Nl2arg22 lam9n2 ) ( - ( - RFN1_arg2 ) ) ) 0 ) ) ( and ( >= lam10n0 0 ) ( >= lam10n1 0 ) ( >= lam10n2 0 ) ( > ( + ( * 1 lam10n0 ) ( * Nl2CT1 lam10n1 ) ( * Nl2CT2 lam10n2 ) ( - 1 ( + ( - ( + RFN1_CT ( * RFN1_arg1 1 ) ) RFN1_CT ) 1 ) ) ) 0 ) ( = ( + ( * 1 lam10n0 ) ( * Nl2arg11 lam10n1 ) ( * Nl2arg12 lam10n2 ) ( - ( - ( + 0 ( * RFN1_arg1 1 ) ) RFN1_arg1 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam10n0 ) ( * Nl2arg21 lam10n1 ) ( * Nl2arg22 lam10n2 ) ( - ( - ( + 0 RFN1_arg2 ) RFN1_arg2 ) ) ) 0 ) ) ) ( and ( and ( >= lam13n0 0 ) ( >= lam13n1 0 ) ( >= lam13n2 0 ) ( > ( + ( * 1 lam13n0 ) ( * Nl2CT1 lam13n1 ) ( * Nl2CT2 lam13n2 ) ( - 1 ( - RFN1_CT ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam13n0 ) ( * Nl2arg11 lam13n1 ) ( * Nl2arg12 lam13n2 ) ( - ( - RFN1_arg1 ) ) ) 0 ) ( = ( + ( * 1 lam13n0 ) ( * Nl2arg21 lam13n1 ) ( * Nl2arg22 lam13n2 ) ( - ( - RFN1_arg2 ) ) ) 0 ) ) ( and ( >= lam14n0 0 ) ( >= lam14n1 0 ) ( >= lam14n2 0 ) ( > ( + ( * 1 lam14n0 ) ( * Nl2CT1 lam14n1 ) ( * Nl2CT2 lam14n2 ) ( - 1 ( + ( - ( + RFN1_CT ( * RFN1_arg2 1 ) ) RFN1_CT ) 1 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam14n0 ) ( * Nl2arg11 lam14n1 ) ( * Nl2arg12 lam14n2 ) ( - ( - ( + 0 RFN1_arg1 ) RFN1_arg1 ) ) ) 0 ) ( = ( + ( * 1 lam14n0 ) ( * Nl2arg21 lam14n1 ) ( * Nl2arg22 lam14n2 ) ( - ( - ( + 0 ( * RFN1_arg2 1 ) ) RFN1_arg2 ) ) ) 0 ) ) ) ) ) ( or ( and ( >= lam8n0 0 ) ( >= lam8n1 0 ) ( >= lam8n2 0 ) ( > ( + ( * 1 lam8n0 ) ( * Nl2CT1 lam8n1 ) ( * Nl2CT2 lam8n2 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam8n0 ) ( * Nl2arg11 lam8n1 ) ( * Nl2arg12 lam8n2 ) ) 0 ) ( = ( + ( * ( - 1 ) lam8n0 ) ( * Nl2arg21 lam8n1 ) ( * Nl2arg22 lam8n2 ) ) 0 ) ) ( and ( >= lam12n0 0 ) ( >= lam12n1 0 ) ( >= lam12n2 0 ) ( > ( + ( * 1 lam12n0 ) ( * Nl2CT1 lam12n1 ) ( * Nl2CT2 lam12n2 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam12n0 ) ( * Nl2arg11 lam12n1 ) ( * Nl2arg12 lam12n2 ) ) 0 ) ( = ( + ( * 1 lam12n0 ) ( * Nl2arg21 lam12n1 ) ( * Nl2arg22 lam12n2 ) ) 0 ) ) ) ))
-(check-sat)
-(exit)
diff --git a/UnitTests/sat/QF_NIA/From_T2__consts3nt.t2__p18166_terminationG_0.smt2 b/UnitTests/sat/QF_NIA/From_T2__consts3nt.t2__p18166_terminationG_0.smt2
deleted file mode 100644
index b902b51c4086dc6f0fb307caff4e084dca3720e1..0000000000000000000000000000000000000000
--- a/UnitTests/sat/QF_NIA/From_T2__consts3nt.t2__p18166_terminationG_0.smt2
+++ /dev/null
@@ -1,74 +0,0 @@
-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |
-Generated by: Cristina Borralleras, Daniel Larraz, Albert Oliveras, Enric Rodriguez-Carbonell, Albert Rubio
-Generated on: 2017-04-27
-Generator: VeryMax
-Application: Termination proving
-Target solver: barcelogic
-|)
-(set-info :license "https://creativecommons.org/licenses/by/4.0/")
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun Nl1__const_200^01 () Int)
-(declare-fun Nl1x^01 () Int)
-(declare-fun Nl1__const_200^02 () Int)
-(declare-fun Nl1x^02 () Int)
-(declare-fun Nl1__const_200^03 () Int)
-(declare-fun Nl1x^03 () Int)
-(declare-fun lam0n0 () Int)
-(declare-fun lam0n2 () Int)
-(declare-fun lam0n3 () Int)
-(declare-fun lam0n4 () Int)
-(declare-fun lam0n1 () Int)
-(declare-fun Nl1CT1 () Int)
-(declare-fun Nl1CT2 () Int)
-(declare-fun Nl1CT3 () Int)
-(declare-fun lam1n0 () Int)
-(declare-fun lam1n2 () Int)
-(declare-fun lam1n3 () Int)
-(declare-fun lam1n4 () Int)
-(declare-fun lam1n1 () Int)
-(declare-fun lam2n0 () Int)
-(declare-fun lam2n2 () Int)
-(declare-fun lam2n3 () Int)
-(declare-fun lam2n4 () Int)
-(declare-fun lam2n1 () Int)
-(declare-fun lam3n0 () Int)
-(declare-fun lam3n2 () Int)
-(declare-fun lam3n3 () Int)
-(declare-fun lam3n4 () Int)
-(declare-fun lam3n1 () Int)
-(declare-fun __const_200^0 () Int)
-(declare-fun x^0 () Int)
-(declare-fun lam10n0 () Int)
-(declare-fun lam10n2 () Int)
-(declare-fun lam10n3 () Int)
-(declare-fun lam10n4 () Int)
-(declare-fun lam10n1 () Int)
-(declare-fun RFN1_CT () Int)
-(declare-fun RFN1_x^0 () Int)
-(declare-fun RFN1___const_200^0 () Int)
-(declare-fun lam8n0 () Int)
-(declare-fun lam8n2 () Int)
-(declare-fun lam8n3 () Int)
-(declare-fun lam8n4 () Int)
-(declare-fun lam8n1 () Int)
-(declare-fun lam9n0 () Int)
-(declare-fun lam9n2 () Int)
-(declare-fun lam9n3 () Int)
-(declare-fun lam9n4 () Int)
-(declare-fun lam9n1 () Int)
-(declare-fun lam7n0 () Int)
-(declare-fun lam7n2 () Int)
-(declare-fun lam7n3 () Int)
-(declare-fun lam7n4 () Int)
-(declare-fun lam7n1 () Int)
-(assert ( and ( <= ( - 1 ) Nl1__const_200^01 ) ( <= Nl1__const_200^01 1 ) ( <= ( - 1 ) Nl1x^01 ) ( <= Nl1x^01 1 ) ( <= ( - 1 ) Nl1__const_200^02 ) ( <= Nl1__const_200^02 1 ) ( <= ( - 1 ) Nl1x^02 ) ( <= Nl1x^02 1 ) ( <= ( - 1 ) Nl1__const_200^03 ) ( <= Nl1__const_200^03 1 ) ( <= ( - 1 ) Nl1x^03 ) ( <= Nl1x^03 1 ) ))
-(assert ( or ( and ( >= lam0n0 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( >= lam0n4 0 ) ( > ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * Nl1CT1 lam0n2 ) ( * Nl1CT2 lam0n3 ) ( * Nl1CT3 lam0n4 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * Nl1__const_200^01 lam0n2 ) ( * Nl1__const_200^02 lam0n3 ) ( * Nl1__const_200^03 lam0n4 ) ) 0 ) ( = ( + ( * 1 lam0n1 ) ( * Nl1x^01 lam0n2 ) ( * Nl1x^02 lam0n3 ) ( * Nl1x^03 lam0n4 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * ( - 1 ) lam0n1 ) ) 0 ) ) ( and ( >= lam1n0 0 ) ( >= lam1n2 0 ) ( >= lam1n3 0 ) ( >= lam1n4 0 ) ( > ( + ( * 1 lam1n0 ) ( * 1 lam1n1 ) ( * Nl1CT1 lam1n2 ) ( * Nl1CT2 lam1n3 ) ( * Nl1CT3 lam1n4 ) ( - 1 ( + Nl1CT1 ( * Nl1x^01 0 ) ) ) ) 0 ) ( = ( + ( * 1 lam1n0 ) ( * Nl1__const_200^01 lam1n2 ) ( * Nl1__const_200^02 lam1n3 ) ( * Nl1__const_200^03 lam1n4 ) ( - ( + 0 Nl1__const_200^01 ) ) ) 0 ) ( = ( + ( * 1 lam1n1 ) ( * Nl1x^01 lam1n2 ) ( * Nl1x^02 lam1n3 ) ( * Nl1x^03 lam1n4 ) ) 0 ) ( = ( + ( * ( - 1 ) lam1n0 ) ( * ( - 1 ) lam1n1 ) ( - ( + 0 ( * Nl1x^01 1 ) ) ) ) 0 ) ) ))
-(assert ( or ( and ( >= lam0n0 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( >= lam0n4 0 ) ( > ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * Nl1CT1 lam0n2 ) ( * Nl1CT2 lam0n3 ) ( * Nl1CT3 lam0n4 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * Nl1__const_200^01 lam0n2 ) ( * Nl1__const_200^02 lam0n3 ) ( * Nl1__const_200^03 lam0n4 ) ) 0 ) ( = ( + ( * 1 lam0n1 ) ( * Nl1x^01 lam0n2 ) ( * Nl1x^02 lam0n3 ) ( * Nl1x^03 lam0n4 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * ( - 1 ) lam0n1 ) ) 0 ) ) ( and ( >= lam2n0 0 ) ( >= lam2n2 0 ) ( >= lam2n3 0 ) ( >= lam2n4 0 ) ( > ( + ( * 1 lam2n0 ) ( * 1 lam2n1 ) ( * Nl1CT1 lam2n2 ) ( * Nl1CT2 lam2n3 ) ( * Nl1CT3 lam2n4 ) ( - 1 ( + Nl1CT2 ( * Nl1x^02 0 ) ) ) ) 0 ) ( = ( + ( * 1 lam2n0 ) ( * Nl1__const_200^01 lam2n2 ) ( * Nl1__const_200^02 lam2n3 ) ( * Nl1__const_200^03 lam2n4 ) ( - ( + 0 Nl1__const_200^02 ) ) ) 0 ) ( = ( + ( * 1 lam2n1 ) ( * Nl1x^01 lam2n2 ) ( * Nl1x^02 lam2n3 ) ( * Nl1x^03 lam2n4 ) ) 0 ) ( = ( + ( * ( - 1 ) lam2n0 ) ( * ( - 1 ) lam2n1 ) ( - ( + 0 ( * Nl1x^02 1 ) ) ) ) 0 ) ) ))
-(assert ( or ( and ( >= lam0n0 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( >= lam0n4 0 ) ( > ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * Nl1CT1 lam0n2 ) ( * Nl1CT2 lam0n3 ) ( * Nl1CT3 lam0n4 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * Nl1__const_200^01 lam0n2 ) ( * Nl1__const_200^02 lam0n3 ) ( * Nl1__const_200^03 lam0n4 ) ) 0 ) ( = ( + ( * 1 lam0n1 ) ( * Nl1x^01 lam0n2 ) ( * Nl1x^02 lam0n3 ) ( * Nl1x^03 lam0n4 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * ( - 1 ) lam0n1 ) ) 0 ) ) ( and ( >= lam3n0 0 ) ( >= lam3n2 0 ) ( >= lam3n3 0 ) ( >= lam3n4 0 ) ( > ( + ( * 1 lam3n0 ) ( * 1 lam3n1 ) ( * Nl1CT1 lam3n2 ) ( * Nl1CT2 lam3n3 ) ( * Nl1CT3 lam3n4 ) ( - 1 ( + Nl1CT3 ( * Nl1x^03 0 ) ) ) ) 0 ) ( = ( + ( * 1 lam3n0 ) ( * Nl1__const_200^01 lam3n2 ) ( * Nl1__const_200^02 lam3n3 ) ( * Nl1__const_200^03 lam3n4 ) ( - ( + 0 Nl1__const_200^03 ) ) ) 0 ) ( = ( + ( * 1 lam3n1 ) ( * Nl1x^01 lam3n2 ) ( * Nl1x^02 lam3n3 ) ( * Nl1x^03 lam3n4 ) ) 0 ) ( = ( + ( * ( - 1 ) lam3n0 ) ( * ( - 1 ) lam3n1 ) ( - ( + 0 ( * Nl1x^03 1 ) ) ) ) 0 ) ) ))
-(assert ( and ( <= ( + Nl1CT1 ( * ( + 0 Nl1__const_200^01 ) __const_200^0 ) ( * ( + 0 Nl1x^01 ) x^0 ) ) 0 ) ( <= ( + Nl1CT2 ( * ( + 0 Nl1__const_200^02 ) __const_200^0 ) ( * ( + 0 Nl1x^02 ) x^0 ) ) 0 ) ( <= ( + Nl1CT3 ( * ( + 0 Nl1__const_200^03 ) __const_200^0 ) ( * ( + 0 Nl1x^03 ) x^0 ) ) 0 ) ))
-(assert ( or ( and ( and ( >= lam10n0 0 ) ( >= lam10n2 0 ) ( >= lam10n3 0 ) ( >= lam10n4 0 ) ( > ( + ( * 1 lam10n0 ) ( * 1 lam10n1 ) ( * Nl1CT1 lam10n2 ) ( * Nl1CT2 lam10n3 ) ( * Nl1CT3 lam10n4 ) ( - 1 ( - ( + RFN1_CT ( * RFN1_x^0 0 ) ) RFN1_CT ) ) ) 0 ) ( = ( + ( * 1 lam10n0 ) ( * Nl1__const_200^01 lam10n2 ) ( * Nl1__const_200^02 lam10n3 ) ( * Nl1__const_200^03 lam10n4 ) ( - ( - ( + 0 RFN1___const_200^0 ) RFN1___const_200^0 ) ) ) 0 ) ( = ( + ( * 1 lam10n1 ) ( * Nl1x^01 lam10n2 ) ( * Nl1x^02 lam10n3 ) ( * Nl1x^03 lam10n4 ) ( - ( - RFN1_x^0 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam10n0 ) ( * ( - 1 ) lam10n1 ) ( - ( + 0 ( * RFN1_x^0 1 ) ) ) ) 0 ) ) ( and ( and ( >= lam8n0 0 ) ( >= lam8n2 0 ) ( >= lam8n3 0 ) ( >= lam8n4 0 ) ( > ( + ( * 1 lam8n0 ) ( * 1 lam8n1 ) ( * Nl1CT1 lam8n2 ) ( * Nl1CT2 lam8n3 ) ( * Nl1CT3 lam8n4 ) ( - 1 ( - RFN1_CT ) ) ) 0 ) ( = ( + ( * 1 lam8n0 ) ( * Nl1__const_200^01 lam8n2 ) ( * Nl1__const_200^02 lam8n3 ) ( * Nl1__const_200^03 lam8n4 ) ( - ( - RFN1___const_200^0 ) ) ) 0 ) ( = ( + ( * 1 lam8n1 ) ( * Nl1x^01 lam8n2 ) ( * Nl1x^02 lam8n3 ) ( * Nl1x^03 lam8n4 ) ( - ( - RFN1_x^0 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam8n0 ) ( * ( - 1 ) lam8n1 ) ) 0 ) ) ( and ( >= lam9n0 0 ) ( >= lam9n2 0 ) ( >= lam9n3 0 ) ( >= lam9n4 0 ) ( > ( + ( * 1 lam9n0 ) ( * 1 lam9n1 ) ( * Nl1CT1 lam9n2 ) ( * Nl1CT2 lam9n3 ) ( * Nl1CT3 lam9n4 ) ( - 1 ( + ( - ( + RFN1_CT ( * RFN1_x^0 0 ) ) RFN1_CT ) 1 ) ) ) 0 ) ( = ( + ( * 1 lam9n0 ) ( * Nl1__const_200^01 lam9n2 ) ( * Nl1__const_200^02 lam9n3 ) ( * Nl1__const_200^03 lam9n4 ) ( - ( - ( + 0 RFN1___const_200^0 ) RFN1___const_200^0 ) ) ) 0 ) ( = ( + ( * 1 lam9n1 ) ( * Nl1x^01 lam9n2 ) ( * Nl1x^02 lam9n3 ) ( * Nl1x^03 lam9n4 ) ( - ( - RFN1_x^0 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam9n0 ) ( * ( - 1 ) lam9n1 ) ( - ( + 0 ( * RFN1_x^0 1 ) ) ) ) 0 ) ) ) ) ( and ( >= lam7n0 0 ) ( >= lam7n2 0 ) ( >= lam7n3 0 ) ( >= lam7n4 0 ) ( > ( + ( * 1 lam7n0 ) ( * 1 lam7n1 ) ( * Nl1CT1 lam7n2 ) ( * Nl1CT2 lam7n3 ) ( * Nl1CT3 lam7n4 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam7n0 ) ( * Nl1__const_200^01 lam7n2 ) ( * Nl1__const_200^02 lam7n3 ) ( * Nl1__const_200^03 lam7n4 ) ) 0 ) ( = ( + ( * 1 lam7n1 ) ( * Nl1x^01 lam7n2 ) ( * Nl1x^02 lam7n3 ) ( * Nl1x^03 lam7n4 ) ) 0 ) ( = ( + ( * ( - 1 ) lam7n0 ) ( * ( - 1 ) lam7n1 ) ) 0 ) ) ))
-(check-sat)
-(exit)
diff --git a/UnitTests/sat/QF_NIA/From_T2__ex36.t2__p26546_safety_0.smt2 b/UnitTests/sat/QF_NIA/From_T2__ex36.t2__p26546_safety_0.smt2
deleted file mode 100644
index ac732449cb20e09c94d6d1ca2d3f77920b5c4296..0000000000000000000000000000000000000000
--- a/UnitTests/sat/QF_NIA/From_T2__ex36.t2__p26546_safety_0.smt2
+++ /dev/null
@@ -1,84 +0,0 @@
-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |
-Generated by: Cristina Borralleras, Daniel Larraz, Albert Oliveras, Enric Rodriguez-Carbonell, Albert Rubio
-Generated on: 2017-04-27
-Generator: VeryMax
-Application: Termination proving
-Target solver: barcelogic
-|)
-(set-info :license "https://creativecommons.org/licenses/by/4.0/")
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun Nl37__const_1132^01 () Int)
-(declare-fun Nl37__const_15^01 () Int)
-(declare-fun Nl37__const_1872^01 () Int)
-(declare-fun Nl37cmd1^01 () Int)
-(declare-fun Nl37cmd2^01 () Int)
-(declare-fun Nl37i16^01 () Int)
-(declare-fun Nl37zer^01 () Int)
-(declare-fun Nl37__const_1132^02 () Int)
-(declare-fun Nl37__const_15^02 () Int)
-(declare-fun Nl37__const_1872^02 () Int)
-(declare-fun Nl37cmd1^02 () Int)
-(declare-fun Nl37cmd2^02 () Int)
-(declare-fun Nl37i16^02 () Int)
-(declare-fun Nl37zer^02 () Int)
-(declare-fun lam0n0 () Int)
-(declare-fun lam0n1 () Int)
-(declare-fun lam0n2 () Int)
-(declare-fun lam0n3 () Int)
-(declare-fun lam0n4 () Int)
-(declare-fun lam0n5 () Int)
-(declare-fun Nl37CT1 () Int)
-(declare-fun Nl37CT2 () Int)
-(declare-fun lam1n0 () Int)
-(declare-fun lam1n1 () Int)
-(declare-fun lam1n2 () Int)
-(declare-fun lam1n3 () Int)
-(declare-fun lam1n4 () Int)
-(declare-fun lam1n5 () Int)
-(declare-fun lam2n0 () Int)
-(declare-fun lam2n1 () Int)
-(declare-fun lam2n2 () Int)
-(declare-fun lam2n3 () Int)
-(declare-fun lam2n4 () Int)
-(declare-fun lam2n5 () Int)
-(declare-fun lam3n0 () Int)
-(declare-fun lam3n1 () Int)
-(declare-fun lam3n2 () Int)
-(declare-fun lam3n3 () Int)
-(declare-fun lam4n0 () Int)
-(declare-fun lam4n1 () Int)
-(declare-fun lam4n2 () Int)
-(declare-fun lam4n3 () Int)
-(declare-fun __const_1132^0 () Int)
-(declare-fun __const_1872^0 () Int)
-(declare-fun zer^0 () Int)
-(declare-fun undef2038 () Int)
-(declare-fun __const_15^0 () Int)
-(declare-fun cmd2^0 () Int)
-(declare-fun i16^0 () Int)
-(declare-fun undef12771 () Int)
-(declare-fun cmd1^0 () Int)
-(declare-fun lam5n0 () Int)
-(declare-fun lam5n1 () Int)
-(declare-fun lam5n2 () Int)
-(declare-fun lam5n3 () Int)
-(declare-fun lam5n5 () Int)
-(declare-fun lam5n6 () Int)
-(declare-fun lam5n4 () Int)
-(declare-fun lam6n0 () Int)
-(declare-fun lam6n1 () Int)
-(declare-fun lam6n2 () Int)
-(declare-fun lam6n3 () Int)
-(declare-fun lam6n5 () Int)
-(declare-fun lam6n6 () Int)
-(declare-fun lam6n4 () Int)
-(assert ( and ( <= ( - 1 ) Nl37__const_1132^01 ) ( <= Nl37__const_1132^01 1 ) ( <= ( - 1 ) Nl37__const_15^01 ) ( <= Nl37__const_15^01 1 ) ( <= ( - 1 ) Nl37__const_1872^01 ) ( <= Nl37__const_1872^01 1 ) ( <= ( - 1 ) Nl37cmd1^01 ) ( <= Nl37cmd1^01 1 ) ( <= ( - 1 ) Nl37cmd2^01 ) ( <= Nl37cmd2^01 1 ) ( <= ( - 1 ) Nl37i16^01 ) ( <= Nl37i16^01 1 ) ( <= ( - 1 ) Nl37zer^01 ) ( <= Nl37zer^01 1 ) ( <= ( - 1 ) Nl37__const_1132^02 ) ( <= Nl37__const_1132^02 1 ) ( <= ( - 1 ) Nl37__const_15^02 ) ( <= Nl37__const_15^02 1 ) ( <= ( - 1 ) Nl37__const_1872^02 ) ( <= Nl37__const_1872^02 1 ) ( <= ( - 1 ) Nl37cmd1^02 ) ( <= Nl37cmd1^02 1 ) ( <= ( - 1 ) Nl37cmd2^02 ) ( <= Nl37cmd2^02 1 ) ( <= ( - 1 ) Nl37i16^02 ) ( <= Nl37i16^02 1 ) ( <= ( - 1 ) Nl37zer^02 ) ( <= Nl37zer^02 1 ) ))
-(assert ( or ( and ( >= lam0n0 0 ) ( >= lam0n1 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( >= lam0n4 0 ) ( >= lam0n5 0 ) ( > ( + ( * Nl37CT1 lam0n4 ) ( * Nl37CT2 lam0n5 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * ( - 1 ) lam0n1 ) ( * Nl37__const_1132^01 lam0n4 ) ( * Nl37__const_1132^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n2 ) ( * Nl37__const_15^01 lam0n4 ) ( * Nl37__const_15^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * Nl37__const_1872^01 lam0n4 ) ( * Nl37__const_1872^02 lam0n5 ) ) 0 ) ( = ( + ( * Nl37cmd1^01 lam0n4 ) ( * Nl37cmd1^02 lam0n5 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n2 ) ( * Nl37cmd2^01 lam0n4 ) ( * Nl37cmd2^02 lam0n5 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n3 ) ( * Nl37i16^01 lam0n4 ) ( * Nl37i16^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * 1 lam0n2 ) ( * Nl37zer^01 lam0n4 ) ( * Nl37zer^02 lam0n5 ) ) 0 ) ( = ( * ( - 1 ) lam0n1 ) 0 ) ) ( and ( >= lam1n0 0 ) ( >= lam1n1 0 ) ( >= lam1n2 0 ) ( >= lam1n3 0 ) ( >= lam1n4 0 ) ( >= lam1n5 0 ) ( > ( + ( * Nl37CT1 lam1n4 ) ( * Nl37CT2 lam1n5 ) ( - 1 ( + Nl37CT1 ( * Nl37i16^01 ( - 1 ) ) ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam1n0 ) ( * ( - 1 ) lam1n1 ) ( * Nl37__const_1132^01 lam1n4 ) ( * Nl37__const_1132^02 lam1n5 ) ( - ( + 0 Nl37__const_1132^01 ) ) ) 0 ) ( = ( + ( * 1 lam1n2 ) ( * Nl37__const_15^01 lam1n4 ) ( * Nl37__const_15^02 lam1n5 ) ( - ( + 0 Nl37__const_15^01 ) ) ) 0 ) ( = ( + ( * 1 lam1n0 ) ( * 1 lam1n1 ) ( * Nl37__const_1872^01 lam1n4 ) ( * Nl37__const_1872^02 lam1n5 ) ( - ( + 0 Nl37__const_1872^01 ) ) ) 0 ) ( = ( + ( * Nl37cmd1^01 lam1n4 ) ( * Nl37cmd1^02 lam1n5 ) ( - ( + 0 Nl37cmd1^01 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam1n2 ) ( * Nl37cmd2^01 lam1n4 ) ( * Nl37cmd2^02 lam1n5 ) ( - ( + 0 Nl37cmd2^01 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam1n3 ) ( * Nl37i16^01 lam1n4 ) ( * Nl37i16^02 lam1n5 ) ( - ( + 0 ( * Nl37i16^01 1 ) ) ) ) 0 ) ( = ( + ( * 1 lam1n0 ) ( * 1 lam1n1 ) ( * 1 lam1n2 ) ( * Nl37zer^01 lam1n4 ) ( * Nl37zer^02 lam1n5 ) ( - ( + 0 Nl37zer^01 ) ) ) 0 ) ( = ( * ( - 1 ) lam1n1 ) 0 ) ) ))
-(assert ( or ( and ( >= lam0n0 0 ) ( >= lam0n1 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( >= lam0n4 0 ) ( >= lam0n5 0 ) ( > ( + ( * Nl37CT1 lam0n4 ) ( * Nl37CT2 lam0n5 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * ( - 1 ) lam0n1 ) ( * Nl37__const_1132^01 lam0n4 ) ( * Nl37__const_1132^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n2 ) ( * Nl37__const_15^01 lam0n4 ) ( * Nl37__const_15^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * Nl37__const_1872^01 lam0n4 ) ( * Nl37__const_1872^02 lam0n5 ) ) 0 ) ( = ( + ( * Nl37cmd1^01 lam0n4 ) ( * Nl37cmd1^02 lam0n5 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n2 ) ( * Nl37cmd2^01 lam0n4 ) ( * Nl37cmd2^02 lam0n5 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n3 ) ( * Nl37i16^01 lam0n4 ) ( * Nl37i16^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * 1 lam0n2 ) ( * Nl37zer^01 lam0n4 ) ( * Nl37zer^02 lam0n5 ) ) 0 ) ( = ( * ( - 1 ) lam0n1 ) 0 ) ) ( and ( >= lam2n0 0 ) ( >= lam2n1 0 ) ( >= lam2n2 0 ) ( >= lam2n3 0 ) ( >= lam2n4 0 ) ( >= lam2n5 0 ) ( > ( + ( * Nl37CT1 lam2n4 ) ( * Nl37CT2 lam2n5 ) ( - 1 ( + Nl37CT2 ( * Nl37i16^02 ( - 1 ) ) ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam2n0 ) ( * ( - 1 ) lam2n1 ) ( * Nl37__const_1132^01 lam2n4 ) ( * Nl37__const_1132^02 lam2n5 ) ( - ( + 0 Nl37__const_1132^02 ) ) ) 0 ) ( = ( + ( * 1 lam2n2 ) ( * Nl37__const_15^01 lam2n4 ) ( * Nl37__const_15^02 lam2n5 ) ( - ( + 0 Nl37__const_15^02 ) ) ) 0 ) ( = ( + ( * 1 lam2n0 ) ( * 1 lam2n1 ) ( * Nl37__const_1872^01 lam2n4 ) ( * Nl37__const_1872^02 lam2n5 ) ( - ( + 0 Nl37__const_1872^02 ) ) ) 0 ) ( = ( + ( * Nl37cmd1^01 lam2n4 ) ( * Nl37cmd1^02 lam2n5 ) ( - ( + 0 Nl37cmd1^02 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam2n2 ) ( * Nl37cmd2^01 lam2n4 ) ( * Nl37cmd2^02 lam2n5 ) ( - ( + 0 Nl37cmd2^02 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam2n3 ) ( * Nl37i16^01 lam2n4 ) ( * Nl37i16^02 lam2n5 ) ( - ( + 0 ( * Nl37i16^02 1 ) ) ) ) 0 ) ( = ( + ( * 1 lam2n0 ) ( * 1 lam2n1 ) ( * 1 lam2n2 ) ( * Nl37zer^01 lam2n4 ) ( * Nl37zer^02 lam2n5 ) ( - ( + 0 Nl37zer^02 ) ) ) 0 ) ( = ( * ( - 1 ) lam2n1 ) 0 ) ) ))
-(assert ( and ( not ( <= ( + 1 __const_1132^0 ( * ( - 1 ) __const_1872^0 ) ( * ( - 1 ) zer^0 ) ) 0 ) ) ( not ( <= ( + 1 __const_1132^0 ( * ( - 1 ) __const_1872^0 ) ( * ( - 1 ) zer^0 ) undef2038 ) 0 ) ) ( <= ( + __const_15^0 ( * ( - 1 ) cmd2^0 ) zer^0 ) 0 ) ( = ( + i16^0 ( * ( - 1 ) undef12771 ) ) 0 ) ( <= ( + Nl37CT1 ( * ( + 0 Nl37__const_1132^01 ) __const_1132^0 ) ( * ( + 0 Nl37__const_15^01 ) __const_15^0 ) ( * ( + 0 Nl37__const_1872^01 ) __const_1872^0 ) ( * ( + 0 Nl37cmd1^01 ) cmd1^0 ) ( * ( + 0 Nl37cmd2^01 ) cmd2^0 ) ( * ( + 0 Nl37i16^01 ) i16^0 ) ( * ( + 0 Nl37zer^01 ) zer^0 ) ) 0 ) ( <= ( + Nl37CT2 ( * ( + 0 Nl37__const_1132^02 ) __const_1132^0 ) ( * ( + 0 Nl37__const_15^02 ) __const_15^0 ) ( * ( + 0 Nl37__const_1872^02 ) __const_1872^0 ) ( * ( + 0 Nl37cmd1^02 ) cmd1^0 ) ( * ( + 0 Nl37cmd2^02 ) cmd2^0 ) ( * ( + 0 Nl37i16^02 ) i16^0 ) ( * ( + 0 Nl37zer^02 ) zer^0 ) ) 0 ) ))
-(assert ( or ( or ( and ( >= lam5n0 0 ) ( >= lam5n1 0 ) ( >= lam5n2 0 ) ( >= lam5n3 0 ) ( >= lam5n5 0 ) ( >= lam5n6 0 ) ( > ( + ( * 1 lam5n2 ) ( * 1 lam5n3 ) ( * Nl37CT1 lam5n5 ) ( * Nl37CT2 lam5n6 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam5n2 ) ( * Nl37__const_1132^01 lam5n5 ) ( * Nl37__const_1132^02 lam5n6 ) ) 0 ) ( = ( + ( * 1 lam5n0 ) ( * Nl37__const_15^01 lam5n5 ) ( * Nl37__const_15^02 lam5n6 ) ) 0 ) ( = ( + ( * 1 lam5n4 ) ( * Nl37__const_1872^01 lam5n5 ) ( * Nl37__const_1872^02 lam5n6 ) ) 0 ) ( = ( + ( * 1 lam5n2 ) ( * ( - 1 ) lam5n4 ) ( * Nl37cmd1^01 lam5n5 ) ( * Nl37cmd1^02 lam5n6 ) ) 0 ) ( = ( + ( * ( - 1 ) lam5n0 ) ( * Nl37cmd2^01 lam5n5 ) ( * Nl37cmd2^02 lam5n6 ) ) 0 ) ( = ( + ( * 1 lam5n3 ) ( * Nl37i16^01 lam5n5 ) ( * Nl37i16^02 lam5n6 ) ) 0 ) ( = ( + ( * 1 lam5n0 ) ( * 1 lam5n1 ) ( * Nl37zer^01 lam5n5 ) ( * Nl37zer^02 lam5n6 ) ) 0 ) ) ( and ( >= lam6n0 0 ) ( >= lam6n1 0 ) ( >= lam6n2 0 ) ( >= lam6n3 0 ) ( >= lam6n5 0 ) ( >= lam6n6 0 ) ( > ( + ( * 1 lam6n2 ) ( * 1 lam6n3 ) ( * Nl37CT1 lam6n5 ) ( * Nl37CT2 lam6n6 ) ) 0 ) ( = ( + ( * ( - 1 ) lam6n2 ) ( * Nl37__const_1132^01 lam6n5 ) ( * Nl37__const_1132^02 lam6n6 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam6n0 ) ( * Nl37__const_15^01 lam6n5 ) ( * Nl37__const_15^02 lam6n6 ) ) 0 ) ( = ( + ( * 1 lam6n4 ) ( * Nl37__const_1872^01 lam6n5 ) ( * Nl37__const_1872^02 lam6n6 ) 1 ) 0 ) ( = ( + ( * 1 lam6n2 ) ( * ( - 1 ) lam6n4 ) ( * Nl37cmd1^01 lam6n5 ) ( * Nl37cmd1^02 lam6n6 ) ) 0 ) ( = ( + ( * ( - 1 ) lam6n0 ) ( * Nl37cmd2^01 lam6n5 ) ( * Nl37cmd2^02 lam6n6 ) ) 0 ) ( = ( + ( * 1 lam6n3 ) ( * Nl37i16^01 lam6n5 ) ( * Nl37i16^02 lam6n6 ) ) 0 ) ( = ( + ( * 1 lam6n0 ) ( * 1 lam6n1 ) ( * Nl37zer^01 lam6n5 ) ( * Nl37zer^02 lam6n6 ) 1 ) 0 ) ( = ( - 1 ) 0 ) ) ) ( and ( and ( and ( >= lam3n0 0 ) ( >= lam3n1 0 ) ( >= lam3n2 0 ) ( > ( - 1 Nl37CT1 ) 0 ) ( = ( + ( * ( - 1 ) lam3n0 ) ( * ( - 1 ) lam3n1 ) ( - ( + 0 Nl37__const_1132^01 ) ) ) 0 ) ( = ( + ( * 1 lam3n2 ) ( - ( + 0 Nl37__const_15^01 ) ) ) 0 ) ( = ( + ( * 1 lam3n0 ) ( * 1 lam3n1 ) ( - ( + 0 Nl37__const_1872^01 ) ) ) 0 ) ( = ( - ( + 0 Nl37cmd1^01 ) ) 0 ) ( = ( + ( * ( - 1 ) lam3n2 ) ( - ( + 0 Nl37cmd2^01 ) ) ) 0 ) ( = ( + ( * 1 lam3n3 ) ( - ( + 0 Nl37i16^01 ) ) ) 0 ) ( = ( + ( * 1 lam3n0 ) ( * 1 lam3n1 ) ( * 1 lam3n2 ) ( - ( + 0 Nl37zer^01 ) ) ) 0 ) ( = ( * ( - 1 ) lam3n1 ) 0 ) ( = ( * ( - 1 ) lam3n3 ) 0 ) ) ( and ( >= lam4n0 0 ) ( >= lam4n1 0 ) ( >= lam4n2 0 ) ( > ( - 1 Nl37CT2 ) 0 ) ( = ( + ( * ( - 1 ) lam4n0 ) ( * ( - 1 ) lam4n1 ) ( - ( + 0 Nl37__const_1132^02 ) ) ) 0 ) ( = ( + ( * 1 lam4n2 ) ( - ( + 0 Nl37__const_15^02 ) ) ) 0 ) ( = ( + ( * 1 lam4n0 ) ( * 1 lam4n1 ) ( - ( + 0 Nl37__const_1872^02 ) ) ) 0 ) ( = ( - ( + 0 Nl37cmd1^02 ) ) 0 ) ( = ( + ( * ( - 1 ) lam4n2 ) ( - ( + 0 Nl37cmd2^02 ) ) ) 0 ) ( = ( + ( * 1 lam4n3 ) ( - ( + 0 Nl37i16^02 ) ) ) 0 ) ( = ( + ( * 1 lam4n0 ) ( * 1 lam4n1 ) ( * 1 lam4n2 ) ( - ( + 0 Nl37zer^02 ) ) ) 0 ) ( = ( * ( - 1 ) lam4n1 ) 0 ) ( = ( * ( - 1 ) lam4n3 ) 0 ) ) ) ( and ( >= lam0n0 0 ) ( >= lam0n1 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( >= lam0n4 0 ) ( >= lam0n5 0 ) ( > ( + ( * Nl37CT1 lam0n4 ) ( * Nl37CT2 lam0n5 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * ( - 1 ) lam0n1 ) ( * Nl37__const_1132^01 lam0n4 ) ( * Nl37__const_1132^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n2 ) ( * Nl37__const_15^01 lam0n4 ) ( * Nl37__const_15^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * Nl37__const_1872^01 lam0n4 ) ( * Nl37__const_1872^02 lam0n5 ) ) 0 ) ( = ( + ( * Nl37cmd1^01 lam0n4 ) ( * Nl37cmd1^02 lam0n5 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n2 ) ( * Nl37cmd2^01 lam0n4 ) ( * Nl37cmd2^02 lam0n5 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n3 ) ( * Nl37i16^01 lam0n4 ) ( * Nl37i16^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * 1 lam0n2 ) ( * Nl37zer^01 lam0n4 ) ( * Nl37zer^02 lam0n5 ) ) 0 ) ( = ( * ( - 1 ) lam0n1 ) 0 ) ) ) ))
-(check-sat)
-(exit)
diff --git a/UnitTests/sat/QF_NIA/From_T2__small29.t2__p23958_edge_closing_0.smt2 b/UnitTests/sat/QF_NIA/From_T2__small29.t2__p23958_edge_closing_0.smt2
deleted file mode 100644
index b5ba88173fe437ca9eb45621bfefc16a9d075bca..0000000000000000000000000000000000000000
--- a/UnitTests/sat/QF_NIA/From_T2__small29.t2__p23958_edge_closing_0.smt2
+++ /dev/null
@@ -1,56 +0,0 @@
-(set-info :smt-lib-version 2.6)
-(set-logic QF_NIA)
-(set-info :source |
-Generated by: Cristina Borralleras, Daniel Larraz, Albert Oliveras, Enric Rodriguez-Carbonell, Albert Rubio
-Generated on: 2017-04-27
-Generator: VeryMax
-Application: Termination proving
-Target solver: barcelogic
-|)
-(set-info :license "https://creativecommons.org/licenses/by/4.0/")
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun Nl1x^01 () Int)
-(declare-fun Nl1y^01 () Int)
-(declare-fun Nl1x^02 () Int)
-(declare-fun Nl1y^02 () Int)
-(declare-fun Nl1x^03 () Int)
-(declare-fun Nl1y^03 () Int)
-(declare-fun lam0n1 () Int)
-(declare-fun lam0n2 () Int)
-(declare-fun lam0n3 () Int)
-(declare-fun Nl1CT1 () Int)
-(declare-fun Nl1CT2 () Int)
-(declare-fun Nl1CT3 () Int)
-(declare-fun lam0n0 () Int)
-(declare-fun lam1n1 () Int)
-(declare-fun lam1n2 () Int)
-(declare-fun lam1n3 () Int)
-(declare-fun lam1n0 () Int)
-(declare-fun lam2n1 () Int)
-(declare-fun lam2n2 () Int)
-(declare-fun lam2n3 () Int)
-(declare-fun lam2n0 () Int)
-(declare-fun lam3n1 () Int)
-(declare-fun lam3n2 () Int)
-(declare-fun lam3n3 () Int)
-(declare-fun lam3n0 () Int)
-(declare-fun x^0 () Int)
-(declare-fun y^0 () Int)
-(declare-fun FV_x^0_1 () Int)
-(declare-fun FV_y^0_1 () Int)
-(declare-fun lam7n0 () Int)
-(declare-fun lam7n1 () Int)
-(declare-fun lam7n2 () Int)
-(declare-fun lam7n3 () Int)
-(declare-fun FV_x^0_2 () Int)
-(declare-fun FV_y^0_2 () Int)
-(assert ( and ( <= ( - 1 ) Nl1x^01 ) ( <= Nl1x^01 1 ) ( <= ( - 1 ) Nl1y^01 ) ( <= Nl1y^01 1 ) ( <= ( - 1 ) Nl1x^02 ) ( <= Nl1x^02 1 ) ( <= ( - 1 ) Nl1y^02 ) ( <= Nl1y^02 1 ) ( <= ( - 1 ) Nl1x^03 ) ( <= Nl1x^03 1 ) ( <= ( - 1 ) Nl1y^03 ) ( <= Nl1y^03 1 ) ))
-(assert ( or ( and ( >= lam0n1 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( > ( + ( * Nl1CT1 lam0n1 ) ( * Nl1CT2 lam0n2 ) ( * Nl1CT3 lam0n3 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * Nl1x^01 lam0n1 ) ( * Nl1x^02 lam0n2 ) ( * Nl1x^03 lam0n3 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * Nl1y^01 lam0n1 ) ( * Nl1y^02 lam0n2 ) ( * Nl1y^03 lam0n3 ) ) 0 ) ) ( and ( >= lam1n1 0 ) ( >= lam1n2 0 ) ( >= lam1n3 0 ) ( > ( + ( * Nl1CT1 lam1n1 ) ( * Nl1CT2 lam1n2 ) ( * Nl1CT3 lam1n3 ) ( - 1 Nl1CT1 ) ) 0 ) ( = ( + ( * 1 lam1n0 ) ( * Nl1x^01 lam1n1 ) ( * Nl1x^02 lam1n2 ) ( * Nl1x^03 lam1n3 ) ( - ( + 0 Nl1x^01 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam1n0 ) ( * Nl1y^01 lam1n1 ) ( * Nl1y^02 lam1n2 ) ( * Nl1y^03 lam1n3 ) ( - ( + 0 Nl1y^01 ) ) ) 0 ) ) ))
-(assert ( or ( and ( >= lam0n1 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( > ( + ( * Nl1CT1 lam0n1 ) ( * Nl1CT2 lam0n2 ) ( * Nl1CT3 lam0n3 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * Nl1x^01 lam0n1 ) ( * Nl1x^02 lam0n2 ) ( * Nl1x^03 lam0n3 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * Nl1y^01 lam0n1 ) ( * Nl1y^02 lam0n2 ) ( * Nl1y^03 lam0n3 ) ) 0 ) ) ( and ( >= lam2n1 0 ) ( >= lam2n2 0 ) ( >= lam2n3 0 ) ( > ( + ( * Nl1CT1 lam2n1 ) ( * Nl1CT2 lam2n2 ) ( * Nl1CT3 lam2n3 ) ( - 1 Nl1CT2 ) ) 0 ) ( = ( + ( * 1 lam2n0 ) ( * Nl1x^01 lam2n1 ) ( * Nl1x^02 lam2n2 ) ( * Nl1x^03 lam2n3 ) ( - ( + 0 Nl1x^02 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam2n0 ) ( * Nl1y^01 lam2n1 ) ( * Nl1y^02 lam2n2 ) ( * Nl1y^03 lam2n3 ) ( - ( + 0 Nl1y^02 ) ) ) 0 ) ) ))
-(assert ( or ( and ( >= lam0n1 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( > ( + ( * Nl1CT1 lam0n1 ) ( * Nl1CT2 lam0n2 ) ( * Nl1CT3 lam0n3 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * Nl1x^01 lam0n1 ) ( * Nl1x^02 lam0n2 ) ( * Nl1x^03 lam0n3 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * Nl1y^01 lam0n1 ) ( * Nl1y^02 lam0n2 ) ( * Nl1y^03 lam0n3 ) ) 0 ) ) ( and ( >= lam3n1 0 ) ( >= lam3n2 0 ) ( >= lam3n3 0 ) ( > ( + ( * Nl1CT1 lam3n1 ) ( * Nl1CT2 lam3n2 ) ( * Nl1CT3 lam3n3 ) ( - 1 Nl1CT3 ) ) 0 ) ( = ( + ( * 1 lam3n0 ) ( * Nl1x^01 lam3n1 ) ( * Nl1x^02 lam3n2 ) ( * Nl1x^03 lam3n3 ) ( - ( + 0 Nl1x^03 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam3n0 ) ( * Nl1y^01 lam3n1 ) ( * Nl1y^02 lam3n2 ) ( * Nl1y^03 lam3n3 ) ( - ( + 0 Nl1y^03 ) ) ) 0 ) ) ))
-(assert ( and ( <= ( + Nl1CT1 ( * Nl1x^01 FV_x^0_1 ) ( * Nl1y^01 FV_y^0_1 ) ) 0 ) ( <= ( + Nl1CT2 ( * Nl1x^02 FV_x^0_1 ) ( * Nl1y^02 FV_y^0_1 ) ) 0 ) ( <= ( + Nl1CT3 ( * Nl1x^03 FV_x^0_1 ) ( * Nl1y^03 FV_y^0_1 ) ) 0 ) ( <= ( + ( * ( - 1 ) FV_x^0_1 ) FV_y^0_1 ) 0 ) ))
-(assert ( and ( >= lam7n0 0 ) ( >= lam7n1 0 ) ( >= lam7n2 0 ) ( >= lam7n3 0 ) ( > ( + ( * 1 lam7n0 ) ( * Nl1CT1 lam7n1 ) ( * Nl1CT2 lam7n2 ) ( * Nl1CT3 lam7n3 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam7n0 ) ( * Nl1x^01 lam7n1 ) ( * Nl1x^02 lam7n2 ) ( * Nl1x^03 lam7n3 ) ) 0 ) ( = ( + ( * 1 lam7n0 ) ( * Nl1y^01 lam7n1 ) ( * Nl1y^02 lam7n2 ) ( * Nl1y^03 lam7n3 ) ) 0 ) ))
-(assert ( and ( and ( <= ( + Nl1CT1 ( * Nl1x^01 FV_x^0_2 ) ( * Nl1y^01 FV_y^0_2 ) ) 0 ) ( <= ( + Nl1CT2 ( * Nl1x^02 FV_x^0_2 ) ( * Nl1y^02 FV_y^0_2 ) ) 0 ) ( <= ( + Nl1CT3 ( * Nl1x^03 FV_x^0_2 ) ( * Nl1y^03 FV_y^0_2 ) ) 0 ) ) ( = ( + FV_x^0_2 ( * ( - 1 ) FV_y^0_2 ) ) 0 ) ))
-(check-sat)
-(exit)