%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : NUM926^1 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:18:17 AM UTC 2026
% Result : Theorem 128.04s 29.82s
% Output : Refutation 128.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 11
% Syntax : Number of formulae : 43 ( 29 unt; 0 typ; 4 def)
% Number of atoms : 84 ( 61 equ; 0 cnn)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 540 ( 23 ~; 10 |; 5 &; 498 @)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 20 ( 17 usr; 10 con; 0-2 aty)
% Number of variables : 48 ( 0 ^; 28 !; 16 ?; 48 :)
% ( 0 !>; 0 ?*; 0 @-; 4 @+)
% Comments :
%------------------------------------------------------------------------------
thf(int_type,type,
int: $tType ).
thf(nat_type,type,
nat: $tType ).
thf(one_one_int_decl,type,
one_one_int: int ).
thf(plus_plus_int_decl,type,
plus_plus_int: int > int > int ).
thf(times_times_int_decl,type,
times_times_int: int > int > int ).
thf(bit0_decl,type,
bit0: int > int ).
thf(bit1_decl,type,
bit1: int > int ).
thf(pls_decl,type,
pls: int ).
thf(number_number_of_int_decl,type,
number_number_of_int: int > int ).
thf(number_number_of_nat_decl,type,
number_number_of_nat: int > nat ).
thf(ord_less_int_decl,type,
ord_less_int: int > int > $o ).
thf(ord_less_eq_int_decl,type,
ord_less_eq_int: int > int > $o ).
thf(power_power_int_decl,type,
power_power_int: int > nat > int ).
thf(m_decl,type,
m: int ).
thf(t_decl,type,
t: int ).
thf(sk2_decl,type,
sk2: int ).
thf(sk3_decl,type,
sk3: int ).
thf(sk4_decl,type,
sk4: int ).
thf(sk5_decl,type,
sk5: int ).
thf(sk2_def,definition,
( sk2
= ( @+[A: int] :
? [B: int] :
( ( plus_plus_int @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ B @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: int] :
( ( plus_plus_int @ ( power_power_int @ sk2 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: int] :
? [B: int] :
( ( plus_plus_int @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ B @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: int] :
( ( plus_plus_int @ ( power_power_int @ sk4 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ) ) ).
thf(78,axiom,
( ( ord_less_int @ one_one_int @ t )
=> ? [A: int,B: int] :
( ( plus_plus_int @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ B @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
thf(344,plain,
( ( ord_less_int @ one_one_int @ t )
=> ? [A: int,B: int] :
( ( plus_plus_int @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ B @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(345,plain,
( ~ ( ord_less_int @ one_one_int @ t )
| ( ( plus_plus_int @ ( power_power_int @ sk2 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ sk3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ),
inference(cnf,[status(esa)],[344]) ).
thf(346,plain,
( ( ( plus_plus_int @ ( power_power_int @ sk2 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ sk3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) )
| ~ ( ord_less_int @ one_one_int @ t ) ),
inference(lifteq,[status(thm)],[345]) ).
thf(97,axiom,
! [A: int] :
( ( number_number_of_int @ A )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_111_number__of__is__id) ).
thf(401,plain,
! [A: int] :
( ( number_number_of_int @ A )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[97]) ).
thf(402,plain,
! [A: int] :
( ( number_number_of_int @ A )
= A ),
inference(cnf,[status(esa)],[401]) ).
thf(403,plain,
! [A: int] :
( ( number_number_of_int @ A )
= A ),
inference(lifteq,[status(thm)],[402]) ).
thf(55,axiom,
! [A: int] :
( ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
= ( times_times_int @ A @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_18_power2__eq__square) ).
thf(282,plain,
! [A: int] :
( ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
= ( times_times_int @ A @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(283,plain,
! [A: int] :
( ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
= ( times_times_int @ A @ A ) ),
inference(cnf,[status(esa)],[282]) ).
thf(284,plain,
! [A: int] :
( ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )
= ( times_times_int @ A @ A ) ),
inference(lifteq,[status(thm)],[283]) ).
thf(111,axiom,
ord_less_eq_int @ one_one_int @ t,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_tpos) ).
thf(440,plain,
ord_less_eq_int @ one_one_int @ t,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[111]) ).
thf(25,axiom,
! [A: int,B: int] :
( ( ord_less_int @ A @ B )
= ( ( ord_less_eq_int @ A @ B )
& ( A != B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_28_zless__le) ).
thf(192,plain,
! [A: int,B: int] :
( ( ord_less_int @ A @ B )
= ( ( ord_less_eq_int @ A @ B )
& ( A != B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(193,plain,
! [B: int,A: int] :
( ( ord_less_int @ A @ B )
= ( ( ord_less_eq_int @ A @ B )
& ( A != B ) ) ),
inference(cnf,[status(esa)],[192]) ).
thf(194,plain,
! [B: int,A: int] :
( ( ord_less_int @ A @ B )
= ( ( ord_less_eq_int @ A @ B )
& ( A != B ) ) ),
inference(lifteq,[status(thm)],[193]) ).
thf(8107,plain,
! [B: int,A: int] :
( ( ( ord_less_int @ A @ B )
= ( $true
& ( A != B ) ) )
| ( ( ord_less_eq_int @ one_one_int @ t )
!= ( ord_less_eq_int @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[440,194]) ).
thf(8108,plain,
! [B: int,A: int] :
( ( ( ord_less_int @ A @ B )
= ( A != B ) )
| ( ( ord_less_eq_int @ one_one_int @ t )
!= ( ord_less_eq_int @ A @ B ) ) ),
inference(simp,[status(thm)],[8107]) ).
thf(8109,plain,
( ( ord_less_int @ one_one_int @ t )
= ( one_one_int != t ) ),
inference(pattern_uni,[status(thm)],[8108:[bind(A,$thf( one_one_int )),bind(B,$thf( t ))]]) ).
thf(31950,plain,
( ( ( plus_plus_int @ ( times_times_int @ sk2 @ sk2 ) @ ( times_times_int @ sk3 @ sk3 ) )
= ( plus_plus_int @ ( times_times_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) @ m ) @ one_one_int ) )
| ~ ( ( one_one_int != t ) ) ),
inference(rewrite,[status(thm)],[346,403,284,8109]) ).
thf(31951,plain,
( ( ( plus_plus_int @ ( times_times_int @ sk2 @ sk2 ) @ ( times_times_int @ sk3 @ sk3 ) )
= ( plus_plus_int @ ( times_times_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) @ m ) @ one_one_int ) )
| ( one_one_int = t ) ),
inference(simp,[status(thm)],[31950]) ).
thf(31952,plain,
( ( t = one_one_int )
| ( ( plus_plus_int @ ( times_times_int @ sk2 @ sk2 ) @ ( times_times_int @ sk3 @ sk3 ) )
= ( plus_plus_int @ ( times_times_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) @ m ) @ one_one_int ) ) ),
inference(lifteq,[status(thm)],[31951]) ).
thf(1,conjecture,
? [A: int,B: int] :
( ( plus_plus_int @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ B @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
thf(2,negated_conjecture,
~ ? [A: int,B: int] :
( ( plus_plus_int @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ B @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(126,plain,
~ ? [A: int,B: int] :
( ( plus_plus_int @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ B @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(127,plain,
! [B: int,A: int] :
( ( plus_plus_int @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ B @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
!= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ),
inference(cnf,[status(esa)],[126]) ).
thf(128,plain,
! [B: int,A: int] :
( ( plus_plus_int @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ B @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
!= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ),
inference(lifteq,[status(thm)],[127]) ).
thf(558,plain,
! [B: int,A: int] :
( ( plus_plus_int @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ B @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
!= ( plus_plus_int @ ( times_times_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) @ m ) @ one_one_int ) ),
inference(rewrite,[status(thm)],[128,403]) ).
thf(56943,plain,
! [B: int,A: int] :
( ( plus_plus_int @ ( times_times_int @ A @ A ) @ ( times_times_int @ B @ B ) )
!= ( plus_plus_int @ ( times_times_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) @ m ) @ one_one_int ) ),
inference(rewrite,[status(thm)],[558,284]) ).
thf(56945,plain,
t = one_one_int,
inference(simplifyReflect,[status(thm)],[31952,56943]) ).
thf(117,axiom,
( ( t = one_one_int )
=> ? [A: int,B: int] :
( ( plus_plus_int @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ B @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
thf(454,plain,
( ( t = one_one_int )
=> ? [A: int,B: int] :
( ( plus_plus_int @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ B @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[117]) ).
thf(455,plain,
( ( t != one_one_int )
| ( ( plus_plus_int @ ( power_power_int @ sk4 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ sk5 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ),
inference(cnf,[status(esa)],[454]) ).
thf(456,plain,
( ( t != one_one_int )
| ( ( plus_plus_int @ ( power_power_int @ sk4 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ sk5 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) )
= ( plus_plus_int @ ( times_times_int @ ( number_number_of_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ m ) @ one_one_int ) ) ),
inference(lifteq,[status(thm)],[455]) ).
thf(45149,plain,
( ( t != one_one_int )
| ( ( plus_plus_int @ ( times_times_int @ sk4 @ sk4 ) @ ( times_times_int @ sk5 @ sk5 ) )
= ( plus_plus_int @ ( times_times_int @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) @ m ) @ one_one_int ) ) ),
inference(rewrite,[status(thm)],[456,403,284]) ).
thf(56944,plain,
t != one_one_int,
inference(simplifyReflect,[status(thm)],[45149,56943]) ).
thf(57293,plain,
$false,
inference(simplifyReflect,[status(thm)],[56945,56944]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM926^1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.08/0.19 % Computer : n002.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 13:08:22 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.88/0.78 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.94/1.16 % [INFO] Parsing done (377ms).
% 1.94/1.17 % [INFO] Running in sequential loop mode.
% 2.70/1.57 % [INFO] eprover registered as external prover.
% 2.70/1.58 % [INFO] Scanning for conjecture ...
% 3.13/1.71 % [INFO] Found a conjecture (or negated_conjecture) and 123 axioms. Running axiom selection ...
% 3.36/1.82 % [INFO] Axiom selection finished. Selected 123 axioms (removed 0 axioms).
% 3.65/1.99 % [INFO] Problem is higher-order (TPTP THF).
% 3.65/2.01 % [INFO] Type checking passed.
% 3.65/2.01 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 128.04/29.82 % [INFO] Killing All external provers ...
% 128.04/29.82 % Time passed: 29484ms (effective reasoning time: 28641ms)
% 128.04/29.82 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 128.04/29.82 % Axioms used in derivation (6): fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06, fact_0_tpos, fact_28_zless__le, fact_18_power2__eq__square, fact_111_number__of__is__id, fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06
% 128.04/29.82 % No. of inferences in proof: 39
% 128.04/29.82 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 29484 ms resp. 28641 ms w/o parsing
% 128.04/29.87 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 128.04/29.87 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------