%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP036^1 : TPTP v9.3.1. Released v7.5.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 : n001.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:06:30 AM UTC 2026
% Result : Theorem 107.05s 46.98s
% Output : Refutation 107.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 3
% Syntax : Number of formulae : 13 ( 7 unt; 0 typ; 0 def)
% Number of atoms : 24 ( 2 equ; 0 cnn)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 207 ( 10 ~; 4 |; 3 &; 190 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 8 avg)
% Number of types : 22 ( 21 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 20 ( 17 usr; 11 con; 0-3 aty)
% Number of variables : 6 ( 0 ^; 3 !; 3 ?; 6 :)
% Comments :
%------------------------------------------------------------------------------
thf(set_Pr242060487real_c_type,type,
set_Pr242060487real_c: $tType ).
thf(produc1037099239real_c_type,type,
produc1037099239real_c: $tType ).
thf(set_Pr754230471real_c_type,type,
set_Pr754230471real_c: $tType ).
thf(produc640052711real_c_type,type,
produc640052711real_c: $tType ).
thf(produc1360640805um_b_c_type,type,
produc1360640805um_b_c: $tType ).
thf(produc1470506001real_c_type,type,
produc1470506001real_c: $tType ).
thf(produc793920321um_c_c_type,type,
produc793920321um_c_c: $tType ).
thf(produc777402865um_c_c_type,type,
produc777402865um_c_c: $tType ).
thf(produc1415638375um_b_c_type,type,
produc1415638375um_b_c: $tType ).
thf(set_Pr1389752855real_c_type,type,
set_Pr1389752855real_c: $tType ).
thf(produc263671631um_b_c_type,type,
produc263671631um_b_c: $tType ).
thf(produc1573491071um_c_c_type,type,
produc1573491071um_c_c: $tType ).
thf(produc190496183real_c_type,type,
produc190496183real_c: $tType ).
thf(produc214722967um_c_c_type,type,
produc214722967um_c_c: $tType ).
thf(denota231621370t_unit_type,type,
denota231621370t_unit: $tType ).
thf(set_Su1783761653um_b_c_type,type,
set_Su1783761653um_b_c: $tType ).
thf(sum_su737395349um_b_c_type,type,
sum_su737395349um_b_c: $tType ).
thf(finite1398487019real_c_type,type,
finite1398487019real_c: $tType ).
thf(set_Sum_sum_c_c_type,type,
set_Sum_sum_c_c: $tType ).
thf(hp_a_b_c_type,type,
hp_a_b_c: $tType ).
thf(sum_sum_c_c_type,type,
sum_sum_c_c: $tType ).
thf(denota1997846518gree_c_decl,type,
denota1997846518gree_c: produc190496183real_c > produc190496183real_c > set_Sum_sum_c_c > $o ).
thf(denota904684656_a_b_c_decl,type,
denota904684656_a_b_c: denota231621370t_unit > hp_a_b_c > set_Pr754230471real_c ).
thf(sup_su1349021703um_c_c_decl,type,
sup_su1349021703um_c_c: set_Sum_sum_c_c > set_Sum_sum_c_c > set_Sum_sum_c_c ).
thf(produc394644079real_c_decl,type,
produc394644079real_c: finite1398487019real_c > finite1398487019real_c > produc190496183real_c ).
thf(produc1687028567real_c_decl,type,
produc1687028567real_c: produc190496183real_c > produc190496183real_c > produc640052711real_c ).
thf(static_MBV_a_b_c_decl,type,
static_MBV_a_b_c: hp_a_b_c > set_Sum_sum_c_c ).
thf(choice_a_b_c_decl,type,
choice_a_b_c: hp_a_b_c > hp_a_b_c > hp_a_b_c ).
thf(member346808080real_c_decl,type,
member346808080real_c: produc640052711real_c > set_Pr754230471real_c > $o ).
thf(j_decl,type,
j: denota231621370t_unit ).
thf(v_decl,type,
v: set_Sum_sum_c_c ).
thf(mu_decl,type,
mu: produc190496183real_c ).
thf(mu2_decl,type,
mu2: finite1398487019real_c ).
thf(mu3_decl,type,
mu3: finite1398487019real_c ).
thf(nu_2_decl,type,
nu_2: finite1398487019real_c ).
thf(nu_22_decl,type,
nu_22: finite1398487019real_c ).
thf(a_decl,type,
a: hp_a_b_c ).
thf(b_decl,type,
b: hp_a_b_c ).
thf(291,axiom,
member346808080real_c @ ( produc1687028567real_c @ ( produc394644079real_c @ nu_22 @ nu_2 ) @ mu ) @ ( denota904684656_a_b_c @ j @ ( choice_a_b_c @ a @ b ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_prog__sem_H) ).
thf(1339,plain,
member346808080real_c @ ( produc1687028567real_c @ ( produc394644079real_c @ nu_22 @ nu_2 ) @ mu ) @ ( denota904684656_a_b_c @ j @ ( choice_a_b_c @ a @ b ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[291]) ).
thf(195,axiom,
denota1997846518gree_c @ ( produc394644079real_c @ mu3 @ mu2 ) @ mu @ ( sup_su1349021703um_c_c @ ( static_MBV_a_b_c @ ( choice_a_b_c @ a @ b ) ) @ v ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_agree_H) ).
thf(1034,plain,
denota1997846518gree_c @ ( produc394644079real_c @ mu3 @ mu2 ) @ mu @ ( sup_su1349021703um_c_c @ ( static_MBV_a_b_c @ ( choice_a_b_c @ a @ b ) ) @ v ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[195]) ).
thf(1,conjecture,
? [A: produc190496183real_c] :
( ( member346808080real_c @ ( produc1687028567real_c @ ( produc394644079real_c @ nu_22 @ nu_2 ) @ A ) @ ( denota904684656_a_b_c @ j @ ( choice_a_b_c @ a @ b ) ) )
& ( denota1997846518gree_c @ ( produc394644079real_c @ mu3 @ mu2 ) @ A @ ( sup_su1349021703um_c_c @ ( static_MBV_a_b_c @ ( choice_a_b_c @ a @ b ) ) @ v ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
thf(2,negated_conjecture,
~ ? [A: produc190496183real_c] :
( ( member346808080real_c @ ( produc1687028567real_c @ ( produc394644079real_c @ nu_22 @ nu_2 ) @ A ) @ ( denota904684656_a_b_c @ j @ ( choice_a_b_c @ a @ b ) ) )
& ( denota1997846518gree_c @ ( produc394644079real_c @ mu3 @ mu2 ) @ A @ ( sup_su1349021703um_c_c @ ( static_MBV_a_b_c @ ( choice_a_b_c @ a @ b ) ) @ v ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(350,plain,
~ ? [A: produc190496183real_c] :
( ( member346808080real_c @ ( produc1687028567real_c @ ( produc394644079real_c @ nu_22 @ nu_2 ) @ A ) @ ( denota904684656_a_b_c @ j @ ( choice_a_b_c @ a @ b ) ) )
& ( denota1997846518gree_c @ ( produc394644079real_c @ mu3 @ mu2 ) @ A @ ( sup_su1349021703um_c_c @ ( static_MBV_a_b_c @ ( choice_a_b_c @ a @ b ) ) @ v ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(351,plain,
! [A: produc190496183real_c] :
( ~ ( member346808080real_c @ ( produc1687028567real_c @ ( produc394644079real_c @ nu_22 @ nu_2 ) @ A ) @ ( denota904684656_a_b_c @ j @ ( choice_a_b_c @ a @ b ) ) )
| ~ ( denota1997846518gree_c @ ( produc394644079real_c @ mu3 @ mu2 ) @ A @ ( sup_su1349021703um_c_c @ ( static_MBV_a_b_c @ ( choice_a_b_c @ a @ b ) ) @ v ) ) ),
inference(cnf,[status(esa)],[350]) ).
thf(5277,plain,
! [A: produc190496183real_c] :
( ~ ( member346808080real_c @ ( produc1687028567real_c @ ( produc394644079real_c @ nu_22 @ nu_2 ) @ A ) @ ( denota904684656_a_b_c @ j @ ( choice_a_b_c @ a @ b ) ) )
| ~ $true
| ( ( denota1997846518gree_c @ ( produc394644079real_c @ mu3 @ mu2 ) @ mu @ ( sup_su1349021703um_c_c @ ( static_MBV_a_b_c @ ( choice_a_b_c @ a @ b ) ) @ v ) )
!= ( denota1997846518gree_c @ ( produc394644079real_c @ mu3 @ mu2 ) @ A @ ( sup_su1349021703um_c_c @ ( static_MBV_a_b_c @ ( choice_a_b_c @ a @ b ) ) @ v ) ) ) ),
inference(paramod_ordered,[status(thm)],[1034,351]) ).
thf(5278,plain,
! [A: produc190496183real_c] :
( ~ ( member346808080real_c @ ( produc1687028567real_c @ ( produc394644079real_c @ nu_22 @ nu_2 ) @ A ) @ ( denota904684656_a_b_c @ j @ ( choice_a_b_c @ a @ b ) ) )
| ( ( denota1997846518gree_c @ ( produc394644079real_c @ mu3 @ mu2 ) @ mu @ ( sup_su1349021703um_c_c @ ( static_MBV_a_b_c @ ( choice_a_b_c @ a @ b ) ) @ v ) )
!= ( denota1997846518gree_c @ ( produc394644079real_c @ mu3 @ mu2 ) @ A @ ( sup_su1349021703um_c_c @ ( static_MBV_a_b_c @ ( choice_a_b_c @ a @ b ) ) @ v ) ) ) ),
inference(simp,[status(thm)],[5277]) ).
thf(5279,plain,
~ ( member346808080real_c @ ( produc1687028567real_c @ ( produc394644079real_c @ nu_22 @ nu_2 ) @ mu ) @ ( denota904684656_a_b_c @ j @ ( choice_a_b_c @ a @ b ) ) ),
inference(pattern_uni,[status(thm)],[5278:[bind(A,$thf( mu ))]]) ).
thf(5928,plain,
$false,
inference(rewrite,[status(thm)],[1339,5279]) ).
thf(5929,plain,
$false,
inference(simp,[status(thm)],[5928]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP036^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.08 % 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.10/0.21 % Computer : n001.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Tue Sep 29 19:46:06 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 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.87/0.79 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 2.91/1.34 % [INFO] Parsing done (548ms).
% 2.91/1.36 % [INFO] Running in sequential loop mode.
% 4.16/1.76 % [INFO] eprover registered as external prover.
% 4.16/1.77 % [INFO] Scanning for conjecture ...
% 4.65/1.93 % [INFO] Found a conjecture (or negated_conjecture) and 354 axioms. Running axiom selection ...
% 5.03/2.09 % [INFO] Axiom selection finished. Selected 347 axioms (removed 7 axioms).
% 5.93/2.33 % [INFO] Problem is higher-order (TPTP THF).
% 5.93/2.36 % [INFO] Type checking passed.
% 5.93/2.36 % [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 ...
% 107.05/46.97 % [INFO] Killing All external provers ...
% 107.05/46.97 % Time passed: 46616ms (effective reasoning time: 45603ms)
% 107.05/46.97 % 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)>
% 107.05/46.97 % Axioms used in derivation (2): fact_2_prog__sem_H, fact_3_agree_H
% 107.05/46.97 % No. of inferences in proof: 13
% 107.05/46.98 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 46616 ms resp. 45603 ms w/o parsing
% 107.05/47.01 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 107.05/47.01 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------