%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP038^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n009.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 11.97s 3.94s
% Output : Refutation 12.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 85
% Syntax : Number of formulae : 172 ( 82 unt; 0 typ; 0 def)
% Number of atoms : 404 ( 178 equ; 2 cnn)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1318 ( 20 ~; 0 |; 54 &;1110 @)
% ( 0 <=>; 134 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Number of types : 45 ( 44 usr)
% Number of type conns : 56 ( 56 >; 0 *; 0 +; 0 <<)
% Number of symbols : 37 ( 34 usr; 11 con; 0-4 aty)
% Number of variables : 480 ( 44 ^; 410 !; 26 ?; 480 :)
% Comments :
%------------------------------------------------------------------------------
thf(set_Pr1169339874_sc_sz_type,type,
set_Pr1169339874_sc_sz: $tType ).
thf(produc1821101996_sc_sz_type,type,
produc1821101996_sc_sz: $tType ).
thf(produc1892666919z_real_type,type,
produc1892666919z_real: $tType ).
thf(produc1241881959eal_sz_type,type,
produc1241881959eal_sz: $tType ).
thf(produc1149990247eal_sz_type,type,
produc1149990247eal_sz: $tType ).
thf(produc190496183real_c_type,type,
produc190496183real_c: $tType ).
thf(produc866628903_sc_sz_type,type,
produc866628903_sc_sz: $tType ).
thf(produc1144880887f_sz_o_type,type,
produc1144880887f_sz_o: $tType ).
thf(produc903182423_set_a_type,type,
produc903182423_set_a: $tType ).
thf(produc1553439972f_sz_o_type,type,
produc1553439972f_sz_o: $tType ).
thf(produc1065634396_o_a_o_type,type,
produc1065634396_o_a_o: $tType ).
thf(bounde472938360z_real_type,type,
bounde472938360z_real: $tType ).
thf(set_De208295462t_unit_type,type,
set_De208295462t_unit: $tType ).
thf(set_De455519194t_unit_type,type,
set_De455519194t_unit: $tType ).
thf(denota610675952t_unit_type,type,
denota610675952t_unit: $tType ).
thf(denota231621370t_unit_type,type,
denota231621370t_unit: $tType ).
thf(set_Su1783761653um_b_c_type,type,
set_Su1783761653um_b_c: $tType ).
thf(set_Fi291318197eal_sz_type,type,
set_Fi291318197eal_sz: $tType ).
thf(freche2095075217_sc_sz_type,type,
freche2095075217_sc_sz: $tType ).
thf(produc1691597095_set_a_type,type,
produc1691597095_set_a: $tType ).
thf(freche914690577_a_b_c_type,type,
freche914690577_a_b_c: $tType ).
thf(produc1989635468_a_a_o_type,type,
produc1989635468_a_a_o: $tType ).
thf(produc1561113620_set_a_type,type,
produc1561113620_set_a: $tType ).
thf(sum_su737395349um_b_c_type,type,
sum_su737395349um_b_c: $tType ).
thf(product_prod_a_o_a_o_type,type,
product_prod_a_o_a_o: $tType ).
thf(finite824932053eal_sz_type,type,
finite824932053eal_sz: $tType ).
thf(finite1398487019real_c_type,type,
finite1398487019real_c: $tType ).
thf(list_f1238882004_sc_sz_type,type,
list_f1238882004_sc_sz: $tType ).
thf(frechet_strm_sf_sz_type,type,
frechet_strm_sf_sz: $tType ).
thf(set_Sum_sum_sz_sz_type,type,
set_Sum_sum_sz_sz: $tType ).
thf(frechet_strm_a_c_type,type,
frechet_strm_a_c: $tType ).
thf(set_Sum_sum_c_c_type,type,
set_Sum_sum_c_c: $tType ).
thf(set_trm_sf_sz_type,type,
set_trm_sf_sz: $tType ).
thf(set_trm_a_c_type,type,
set_trm_a_c: $tType ).
thf(formula_sf_sc_sz_type,type,
formula_sf_sc_sz: $tType ).
thf(trm_sf_sz_type,type,
trm_sf_sz: $tType ).
thf(trm_a_c_type,type,
trm_a_c: $tType ).
thf(set_a_type,type,
set_a: $tType ).
thf(real_type,type,
real: $tType ).
thf(sz_type,type,
sz: $tType ).
thf(sf_type,type,
sf: $tType ).
thf(sc_type,type,
sc: $tType ).
thf(c_type,type,
c: $tType ).
thf(a_type,type,
a: $tType ).
thf(denota69106024_a_b_c_decl,type,
denota69106024_a_b_c: denota231621370t_unit > denota231621370t_unit > set_Su1783761653um_b_c > $o ).
thf(denota1997846518gree_c_decl,type,
denota1997846518gree_c: produc190496183real_c > produc190496183real_c > set_Sum_sum_c_c > $o ).
thf(denota2112424896_a_b_c_decl,type,
denota2112424896_a_b_c: denota231621370t_unit > trm_a_c > produc190496183real_c > real ).
thf(denota229585092_a_b_c_decl,type,
denota229585092_a_b_c: denota231621370t_unit > trm_a_c > finite1398487019real_c > finite1398487019real_c > real ).
thf(denota258389581_a_b_c_decl,type,
denota258389581_a_b_c: denota231621370t_unit > $o ).
thf(denota2042094639_a_b_c_decl,type,
denota2042094639_a_b_c: denota231621370t_unit > trm_a_c > finite1398487019real_c > real ).
thf(ord_le775706699real_c_decl,type,
ord_le775706699real_c: finite1398487019real_c > finite1398487019real_c > $o ).
thf(ord_le850691415real_c_decl,type,
ord_le850691415real_c: produc190496183real_c > produc190496183real_c > $o ).
thf(ord_le929608341um_b_c_decl,type,
ord_le929608341um_b_c: set_Su1783761653um_b_c > set_Su1783761653um_b_c > $o ).
thf(ord_le1772180283um_c_c_decl,type,
ord_le1772180283um_c_c: set_Sum_sum_c_c > set_Sum_sum_c_c > $o ).
thf(top_to1201357528_b_c_o_decl,type,
top_to1201357528_b_c_o: sum_su737395349um_b_c > $o ).
thf(top_to524132421um_b_c_decl,type,
top_to524132421um_b_c: set_Su1783761653um_b_c ).
thf(top_to1660572043um_c_c_decl,type,
top_to1660572043um_c_c: set_Sum_sum_c_c ).
thf(top_top_set_a_decl,type,
top_top_set_a: set_a ).
thf(produc394644079real_c_decl,type,
produc394644079real_c: finite1398487019real_c > finite1398487019real_c > produc190496183real_c ).
thf(produc2010422875real_c_decl,type,
produc2010422875real_c: produc190496183real_c > finite1398487019real_c ).
thf(produc314122909real_c_decl,type,
produc314122909real_c: produc190496183real_c > finite1398487019real_c ).
thf(collec2086029184um_b_c_decl,type,
collec2086029184um_b_c: ( sum_su737395349um_b_c > $o ) > set_Su1783761653um_b_c ).
thf(static_FVDiff_a_c_decl,type,
static_FVDiff_a_c: trm_a_c > set_Sum_sum_c_c ).
thf(static_FVT_a_c_decl,type,
static_FVT_a_c: trm_a_c > set_Sum_sum_c_c ).
thf(static_SIGT_a_c_decl,type,
static_SIGT_a_c: trm_a_c > set_a ).
thf(sum_In2139678582um_b_c_decl,type,
sum_In2139678582um_b_c: a > sum_su737395349um_b_c ).
thf(dfree_a_c_decl,type,
dfree_a_c: trm_a_c > $o ).
thf(function_a_c_decl,type,
function_a_c: a > ( c > trm_a_c ) > trm_a_c ).
thf(plus_a_c_decl,type,
plus_a_c: trm_a_c > trm_a_c > trm_a_c ).
thf(times_a_c_decl,type,
times_a_c: trm_a_c > trm_a_c > trm_a_c ).
thf(member1893232190um_b_c_decl,type,
member1893232190um_b_c: sum_su737395349um_b_c > set_Su1783761653um_b_c > $o ).
thf(member_a_decl,type,
member_a: a > set_a > $o ).
thf(i_decl,type,
i: denota231621370t_unit ).
thf(j_decl,type,
j: denota231621370t_unit ).
thf(nu_decl,type,
nu: produc190496183real_c ).
thf(nu2_decl,type,
nu2: produc190496183real_c ).
thf(t1_decl,type,
t1: trm_a_c ).
thf(t2_decl,type,
t2: trm_a_c ).
thf(21,axiom,
! [A: a,B: c > trm_a_c,C: a,D: c > trm_a_c] :
( ( ( function_a_c @ A @ B )
= ( function_a_c @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_trm_Oinject_I3_J) ).
thf(142,plain,
! [A: a,B: c > trm_a_c,C: a,D: c > trm_a_c] :
( ( ( function_a_c @ A @ B )
= ( function_a_c @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(11,axiom,
! [A: trm_a_c,B: trm_a_c,C: trm_a_c,D: trm_a_c] :
( ( plus_a_c @ A @ B )
!= ( times_a_c @ C @ D ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_174_trm_Odistinct_I31_J) ).
thf(110,plain,
! [A: trm_a_c,B: trm_a_c,C: trm_a_c,D: trm_a_c] :
( ( plus_a_c @ A @ B )
!= ( times_a_c @ C @ D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(5,axiom,
! [A: produc190496183real_c,B: produc190496183real_c] :
( ( ord_le850691415real_c @ A @ B )
=> ( ord_le775706699real_c @ ( produc2010422875real_c @ A ) @ ( produc2010422875real_c @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_254_fst__mono) ).
thf(93,plain,
! [A: produc190496183real_c,B: produc190496183real_c] :
( ( ord_le850691415real_c @ A @ B )
=> ( ord_le775706699real_c @ ( produc2010422875real_c @ A ) @ ( produc2010422875real_c @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(44,axiom,
( ord_le850691415real_c
= ( ^ [A: produc190496183real_c,B: produc190496183real_c] :
( ( ord_le775706699real_c @ ( produc2010422875real_c @ A ) @ ( produc2010422875real_c @ B ) )
& ( ord_le775706699real_c @ ( produc314122909real_c @ A ) @ ( produc314122909real_c @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_less__eq__prod__def) ).
thf(224,plain,
( ord_le850691415real_c
= ( ^ [A: produc190496183real_c,B: produc190496183real_c] :
( ( ord_le775706699real_c @ ( produc2010422875real_c @ A ) @ ( produc2010422875real_c @ B ) )
& ( ord_le775706699real_c @ ( produc314122909real_c @ A ) @ ( produc314122909real_c @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(64,axiom,
denota1997846518gree_c @ nu @ nu2 @ ( static_FVDiff_a_c @ t1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_agree1) ).
thf(291,plain,
denota1997846518gree_c @ nu @ nu2 @ ( static_FVDiff_a_c @ t1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(27,axiom,
! [A: produc190496183real_c > $o,B: produc190496183real_c] :
( ! [C: finite1398487019real_c,D: finite1398487019real_c] : ( A @ ( produc394644079real_c @ C @ D ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_prod__cases) ).
thf(159,plain,
! [A: produc190496183real_c > $o,B: produc190496183real_c] :
( ! [C: finite1398487019real_c,D: finite1398487019real_c] : ( A @ ( produc394644079real_c @ C @ D ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(35,axiom,
! [A: finite1398487019real_c,B: finite1398487019real_c] :
( ( produc314122909real_c @ ( produc394644079real_c @ A @ B ) )
= B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_147_snd__conv) ).
thf(182,plain,
! [A: finite1398487019real_c,B: finite1398487019real_c] :
( ( produc314122909real_c @ ( produc394644079real_c @ A @ B ) )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(51,axiom,
! [A: a,B: c > trm_a_c,C: trm_a_c,D: trm_a_c] :
( ( function_a_c @ A @ B )
!= ( times_a_c @ C @ D ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_171_trm_Odistinct_I25_J) ).
thf(246,plain,
! [A: a,B: c > trm_a_c,C: trm_a_c,D: trm_a_c] :
( ( function_a_c @ A @ B )
!= ( times_a_c @ C @ D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(20,axiom,
! [A: set_Su1783761653um_b_c,B: set_Su1783761653um_b_c,C: sum_su737395349um_b_c > $o] :
( ( ord_le929608341um_b_c @ A @ B )
=> ( ( ord_le929608341um_b_c @ A
@ ( collec2086029184um_b_c
@ ^ [D: sum_su737395349um_b_c] :
( ( member1893232190um_b_c @ D @ B )
& ( C @ D ) ) ) )
= ( ! [D: sum_su737395349um_b_c] :
( ( member1893232190um_b_c @ D @ A )
=> ( C @ D ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_subset__Collect__iff) ).
thf(138,plain,
! [A: set_Su1783761653um_b_c,B: set_Su1783761653um_b_c,C: sum_su737395349um_b_c > $o] :
( ( ord_le929608341um_b_c @ A @ B )
=> ( ( ord_le929608341um_b_c @ A
@ ( collec2086029184um_b_c
@ ^ [D: sum_su737395349um_b_c] :
( ( member1893232190um_b_c @ D @ B )
& ( C @ D ) ) ) )
= ( ! [D: sum_su737395349um_b_c] :
( ( member1893232190um_b_c @ D @ A )
=> ( C @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(8,axiom,
! [A: a,B: a] :
( ( ( sum_In2139678582um_b_c @ A )
= ( sum_In2139678582um_b_c @ B ) )
= ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_260_sum_Oinject_I1_J) ).
thf(101,plain,
! [A: a,B: a] :
( ( ( sum_In2139678582um_b_c @ A )
= ( sum_In2139678582um_b_c @ B ) )
= ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(82,axiom,
! [A: set_Sum_sum_c_c,B: set_Sum_sum_c_c,C: produc190496183real_c,D: produc190496183real_c] :
( ( ord_le1772180283um_c_c @ A @ B )
=> ( ( denota1997846518gree_c @ C @ D @ B )
=> ( denota1997846518gree_c @ C @ D @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_agree__supset) ).
thf(333,plain,
! [A: set_Sum_sum_c_c,B: set_Sum_sum_c_c,C: produc190496183real_c,D: produc190496183real_c] :
( ( ord_le1772180283um_c_c @ A @ B )
=> ( ( denota1997846518gree_c @ C @ D @ B )
=> ( denota1997846518gree_c @ C @ D @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(3,axiom,
! [A: finite1398487019real_c,B: finite1398487019real_c,C: finite1398487019real_c,D: finite1398487019real_c] :
( ( ord_le850691415real_c @ ( produc394644079real_c @ A @ B ) @ ( produc394644079real_c @ C @ D ) )
= ( ( ord_le775706699real_c @ A @ C )
& ( ord_le775706699real_c @ B @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_Pair__le) ).
thf(88,plain,
! [A: finite1398487019real_c,B: finite1398487019real_c,C: finite1398487019real_c,D: finite1398487019real_c] :
( ( ord_le850691415real_c @ ( produc394644079real_c @ A @ B ) @ ( produc394644079real_c @ C @ D ) )
= ( ( ord_le775706699real_c @ A @ C )
& ( ord_le775706699real_c @ B @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(30,axiom,
? [A: a] : ( member_a @ A @ top_top_set_a ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_329_UNIV__witness) ).
thf(170,plain,
? [A: a] : ( member_a @ A @ top_top_set_a ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(60,axiom,
! [A: sum_su737395349um_b_c > $o,B: sum_su737395349um_b_c > $o] :
( ! [C: sum_su737395349um_b_c] :
( ( A @ C )
=> ( B @ C ) )
=> ( ord_le929608341um_b_c @ ( collec2086029184um_b_c @ A ) @ ( collec2086029184um_b_c @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_296_Collect__mono) ).
thf(276,plain,
! [A: sum_su737395349um_b_c > $o,B: sum_su737395349um_b_c > $o] :
( ! [C: sum_su737395349um_b_c] :
( ( A @ C )
=> ( B @ C ) )
=> ( ord_le929608341um_b_c @ ( collec2086029184um_b_c @ A ) @ ( collec2086029184um_b_c @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(73,axiom,
( denota69106024_a_b_c @ i @ j
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ ( plus_a_c @ t1 @ t2 ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_IA) ).
thf(308,plain,
( denota69106024_a_b_c @ i @ j
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ ( plus_a_c @ t1 @ t2 ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(14,axiom,
! [A: set_Su1783761653um_b_c,B: set_Su1783761653um_b_c,C: sum_su737395349um_b_c > $o,D: sum_su737395349um_b_c > $o] :
( ( ord_le929608341um_b_c @ A @ B )
=> ( ! [E: sum_su737395349um_b_c] :
( ( member1893232190um_b_c @ E @ A )
=> ( ( C @ E )
=> ( D @ E ) ) )
=> ( ord_le929608341um_b_c
@ ( collec2086029184um_b_c
@ ^ [E: sum_su737395349um_b_c] :
( ( member1893232190um_b_c @ E @ A )
& ( C @ E ) ) )
@ ( collec2086029184um_b_c
@ ^ [E: sum_su737395349um_b_c] :
( ( member1893232190um_b_c @ E @ B )
& ( D @ E ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_subset__CollectI) ).
thf(120,plain,
! [A: set_Su1783761653um_b_c,B: set_Su1783761653um_b_c,C: sum_su737395349um_b_c > $o,D: sum_su737395349um_b_c > $o] :
( ( ord_le929608341um_b_c @ A @ B )
=> ( ! [E: sum_su737395349um_b_c] :
( ( member1893232190um_b_c @ E @ A )
=> ( ( C @ E )
=> ( D @ E ) ) )
=> ( ord_le929608341um_b_c
@ ( collec2086029184um_b_c
@ ^ [E: sum_su737395349um_b_c] :
( ( member1893232190um_b_c @ E @ A )
& ( C @ E ) ) )
@ ( collec2086029184um_b_c
@ ^ [E: sum_su737395349um_b_c] :
( ( member1893232190um_b_c @ E @ B )
& ( D @ E ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(58,axiom,
! [A: a,B: c > trm_a_c,C: trm_a_c,D: trm_a_c] :
( ( function_a_c @ A @ B )
!= ( plus_a_c @ C @ D ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_169_trm_Odistinct_I23_J) ).
thf(269,plain,
! [A: a,B: c > trm_a_c,C: trm_a_c,D: trm_a_c] :
( ( function_a_c @ A @ B )
!= ( plus_a_c @ C @ D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(36,axiom,
! [A: finite1398487019real_c,B: finite1398487019real_c,C: finite1398487019real_c,D: finite1398487019real_c] :
( ( ( produc394644079real_c @ A @ B )
= ( produc394644079real_c @ C @ D ) )
=> ~ ( ( A = C )
=> ( B != D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_Pair__inject) ).
thf(185,plain,
! [A: finite1398487019real_c,B: finite1398487019real_c,C: finite1398487019real_c,D: finite1398487019real_c] :
( ( ( produc394644079real_c @ A @ B )
= ( produc394644079real_c @ C @ D ) )
=> ~ ( ( A = C )
=> ( B != D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(63,axiom,
! [A: finite1398487019real_c,B: finite1398487019real_c,C: finite1398487019real_c,D: finite1398487019real_c] :
( ( ( produc394644079real_c @ A @ B )
= ( produc394644079real_c @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_prod_Oinject) ).
thf(288,plain,
! [A: finite1398487019real_c,B: finite1398487019real_c,C: finite1398487019real_c,D: finite1398487019real_c] :
( ( ( produc394644079real_c @ A @ B )
= ( produc394644079real_c @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(54,axiom,
! [A: trm_a_c,B: trm_a_c] :
( ( dfree_a_c @ ( times_a_c @ A @ B ) )
= ( ( dfree_a_c @ A )
& ( dfree_a_c @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_dfree__Times__simps) ).
thf(257,plain,
! [A: trm_a_c,B: trm_a_c] :
( ( dfree_a_c @ ( times_a_c @ A @ B ) )
= ( ( dfree_a_c @ A )
& ( dfree_a_c @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(28,axiom,
! [A: set_a] :
( ! [B: a] : ( member_a @ B @ A )
=> ( top_top_set_a = A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_331_UNIV__eq__I) ).
thf(164,plain,
! [A: set_a] :
( ! [B: a] : ( member_a @ B @ A )
=> ( top_top_set_a = A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(78,axiom,
! [A: trm_a_c] : ( ord_le1772180283um_c_c @ ( static_FVT_a_c @ A ) @ ( static_FVDiff_a_c @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_315_FVDiff__sub) ).
thf(321,plain,
! [A: trm_a_c] : ( ord_le1772180283um_c_c @ ( static_FVT_a_c @ A ) @ ( static_FVDiff_a_c @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(53,axiom,
! [A: denota231621370t_unit,B: denota231621370t_unit,C: trm_a_c,D: trm_a_c,E: produc190496183real_c] :
( ( denota258389581_a_b_c @ A )
=> ( ( denota258389581_a_b_c @ B )
=> ( ( dfree_a_c @ C )
=> ( ( dfree_a_c @ D )
=> ( ( ( denota2042094639_a_b_c @ A @ C )
= ( denota2042094639_a_b_c @ B @ D ) )
=> ( ( denota229585092_a_b_c @ A @ C @ ( produc2010422875real_c @ E ) @ ( produc314122909real_c @ E ) )
= ( denota229585092_a_b_c @ B @ D @ ( produc2010422875real_c @ E ) @ ( produc314122909real_c @ E ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_305_sterm__determines__frechet) ).
thf(253,plain,
! [A: denota231621370t_unit,B: denota231621370t_unit,C: trm_a_c,D: trm_a_c,E: produc190496183real_c] :
( ( denota258389581_a_b_c @ A )
=> ( ( denota258389581_a_b_c @ B )
=> ( ( dfree_a_c @ C )
=> ( ( dfree_a_c @ D )
=> ( ( ( denota2042094639_a_b_c @ A @ C )
= ( denota2042094639_a_b_c @ B @ D ) )
=> ( ( denota229585092_a_b_c @ A @ C @ ( produc2010422875real_c @ E ) @ ( produc314122909real_c @ E ) )
= ( denota229585092_a_b_c @ B @ D @ ( produc2010422875real_c @ E ) @ ( produc314122909real_c @ E ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(23,axiom,
! [A: set_Su1783761653um_b_c,B: set_Su1783761653um_b_c] :
( ! [C: sum_su737395349um_b_c] :
( ( member1893232190um_b_c @ C @ A )
=> ( member1893232190um_b_c @ C @ B ) )
=> ( ord_le929608341um_b_c @ A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_267_subsetI) ).
thf(147,plain,
! [A: set_Su1783761653um_b_c,B: set_Su1783761653um_b_c] :
( ! [C: sum_su737395349um_b_c] :
( ( member1893232190um_b_c @ C @ A )
=> ( member1893232190um_b_c @ C @ B ) )
=> ( ord_le929608341um_b_c @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(61,axiom,
! [A: trm_a_c,B: trm_a_c] :
( ( dfree_a_c @ ( plus_a_c @ A @ B ) )
= ( ( dfree_a_c @ A )
& ( dfree_a_c @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_dfree__Plus__simps) ).
thf(280,plain,
! [A: trm_a_c,B: trm_a_c] :
( ( dfree_a_c @ ( plus_a_c @ A @ B ) )
= ( ( dfree_a_c @ A )
& ( dfree_a_c @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(43,axiom,
! [A: finite1398487019real_c,B: finite1398487019real_c,C: finite1398487019real_c,D: finite1398487019real_c] :
( ( ( produc394644079real_c @ A @ B )
= ( produc394644079real_c @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_old_Oprod_Oinject) ).
thf(221,plain,
! [A: finite1398487019real_c,B: finite1398487019real_c,C: finite1398487019real_c,D: finite1398487019real_c] :
( ( ( produc394644079real_c @ A @ B )
= ( produc394644079real_c @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(18,axiom,
! [A: denota231621370t_unit,B: set_Su1783761653um_b_c] : ( denota69106024_a_b_c @ A @ A @ B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_Iagree__refl) ).
thf(133,plain,
! [A: denota231621370t_unit,B: set_Su1783761653um_b_c] : ( denota69106024_a_b_c @ A @ A @ B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(56,axiom,
( denota69106024_a_b_c @ i @ j
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ t1 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_IA1) ).
thf(265,plain,
( denota69106024_a_b_c @ i @ j
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ t1 ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(72,axiom,
( ord_le929608341um_b_c
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ t2 ) ) ) )
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ ( plus_a_c @ t1 @ t2 ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_subs_I2_J) ).
thf(307,plain,
( ord_le929608341um_b_c
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ t2 ) ) ) )
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ ( plus_a_c @ t1 @ t2 ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(65,axiom,
! [A: produc190496183real_c,B: produc190496183real_c,C: trm_a_c,D: trm_a_c] :
( ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ ( times_a_c @ C @ D ) ) )
=> ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_agree__times2) ).
thf(292,plain,
! [A: produc190496183real_c,B: produc190496183real_c,C: trm_a_c,D: trm_a_c] :
( ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ ( times_a_c @ C @ D ) ) )
=> ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(47,axiom,
! [A: finite1398487019real_c,B: finite1398487019real_c,C: finite1398487019real_c] :
( ( ( produc2010422875real_c @ ( produc394644079real_c @ A @ B ) )
= C )
=> ( A = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_fst__eqD) ).
thf(233,plain,
! [A: finite1398487019real_c,B: finite1398487019real_c,C: finite1398487019real_c] :
( ( ( produc2010422875real_c @ ( produc394644079real_c @ A @ B ) )
= C )
=> ( A = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(13,axiom,
! [A: a,B: c > trm_a_c] :
( ( dfree_a_c @ ( function_a_c @ A @ B ) )
= ( ! [C: c] : ( dfree_a_c @ ( B @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_dfree__Fun__simps) ).
thf(117,plain,
! [A: a,B: c > trm_a_c] :
( ( dfree_a_c @ ( function_a_c @ A @ B ) )
= ( ! [C: c] : ( dfree_a_c @ ( B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(55,axiom,
! [A: finite1398487019real_c > finite1398487019real_c > $o,B: finite1398487019real_c,C: finite1398487019real_c,D: produc190496183real_c] :
( ( A @ B @ C )
=> ( ( D
= ( produc394644079real_c @ B @ C ) )
=> ( A @ ( produc2010422875real_c @ D ) @ ( produc314122909real_c @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_BNF__Greatest__Fixpoint_Osubst__Pair) ).
thf(260,plain,
! [A: finite1398487019real_c > finite1398487019real_c > $o,B: finite1398487019real_c,C: finite1398487019real_c,D: produc190496183real_c] :
( ( A @ B @ C )
=> ( ( D
= ( produc394644079real_c @ B @ C ) )
=> ( A @ ( produc2010422875real_c @ D ) @ ( produc314122909real_c @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(68,axiom,
! [A: produc190496183real_c,B: produc190496183real_c] :
( ( denota1997846518gree_c @ A @ B @ top_to1660572043um_c_c )
=> ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_340_agree__UNIV__eq) ).
thf(297,plain,
! [A: produc190496183real_c,B: produc190496183real_c] :
( ( denota1997846518gree_c @ A @ B @ top_to1660572043um_c_c )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(85,axiom,
! [A: finite1398487019real_c,B: finite1398487019real_c,C: finite1398487019real_c,D: finite1398487019real_c] :
( ( denota1997846518gree_c @ ( produc394644079real_c @ A @ B ) @ ( produc394644079real_c @ C @ D ) @ top_to1660572043um_c_c )
=> ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_339_Vagree__univ) ).
thf(339,plain,
! [A: finite1398487019real_c,B: finite1398487019real_c,C: finite1398487019real_c,D: finite1398487019real_c] :
( ( denota1997846518gree_c @ ( produc394644079real_c @ A @ B ) @ ( produc394644079real_c @ C @ D ) @ top_to1660572043um_c_c )
=> ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(40,axiom,
! [A: set_Su1783761653um_b_c,B: set_Su1783761653um_b_c,C: denota231621370t_unit,D: denota231621370t_unit] :
( ( ord_le929608341um_b_c @ A @ B )
=> ( ( denota69106024_a_b_c @ C @ D @ B )
=> ( denota69106024_a_b_c @ C @ D @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_Iagree__sub) ).
thf(212,plain,
! [A: set_Su1783761653um_b_c,B: set_Su1783761653um_b_c,C: denota231621370t_unit,D: denota231621370t_unit] :
( ( ord_le929608341um_b_c @ A @ B )
=> ( ( denota69106024_a_b_c @ C @ D @ B )
=> ( denota69106024_a_b_c @ C @ D @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(50,axiom,
! [A: set_Su1783761653um_b_c,B: sum_su737395349um_b_c > $o] :
( ord_le929608341um_b_c
@ ( collec2086029184um_b_c
@ ^ [C: sum_su737395349um_b_c] :
( ( member1893232190um_b_c @ C @ A )
& ( B @ C ) ) )
@ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_303_Collect__subset) ).
thf(244,plain,
! [A: set_Su1783761653um_b_c,B: sum_su737395349um_b_c > $o] :
( ord_le929608341um_b_c
@ ( collec2086029184um_b_c
@ ^ [C: sum_su737395349um_b_c] :
( ( member1893232190um_b_c @ C @ A )
& ( B @ C ) ) )
@ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(57,axiom,
! [A: trm_a_c,B: trm_a_c,C: trm_a_c,D: trm_a_c] :
( ( ( plus_a_c @ A @ B )
= ( plus_a_c @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_trm_Oinject_I4_J) ).
thf(266,plain,
! [A: trm_a_c,B: trm_a_c,C: trm_a_c,D: trm_a_c] :
( ( ( plus_a_c @ A @ B )
= ( plus_a_c @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(75,axiom,
! [A: set_Sum_sum_c_c,B: set_Sum_sum_c_c,C: produc190496183real_c,D: produc190496183real_c] :
( ( ord_le1772180283um_c_c @ A @ B )
=> ( ( denota1997846518gree_c @ C @ D @ B )
=> ( denota1997846518gree_c @ C @ D @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_agree__sub) ).
thf(311,plain,
! [A: set_Sum_sum_c_c,B: set_Sum_sum_c_c,C: produc190496183real_c,D: produc190496183real_c] :
( ( ord_le1772180283um_c_c @ A @ B )
=> ( ( denota1997846518gree_c @ C @ D @ B )
=> ( denota1997846518gree_c @ C @ D @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(16,axiom,
! [A: produc190496183real_c] :
( A
= ( produc394644079real_c @ ( produc2010422875real_c @ A ) @ ( produc314122909real_c @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_prod_Oexhaust__sel) ).
thf(128,plain,
! [A: produc190496183real_c] :
( A
= ( produc394644079real_c @ ( produc2010422875real_c @ A ) @ ( produc314122909real_c @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(48,axiom,
( denota2112424896_a_b_c
= ( ^ [A: denota231621370t_unit,B: trm_a_c,C: produc190496183real_c] : ( denota229585092_a_b_c @ A @ B @ ( produc2010422875real_c @ C ) @ ( produc314122909real_c @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_directional__derivative__def) ).
thf(237,plain,
( denota2112424896_a_b_c
= ( ^ [A: denota231621370t_unit,B: trm_a_c,C: produc190496183real_c] : ( denota229585092_a_b_c @ A @ B @ ( produc2010422875real_c @ C ) @ ( produc314122909real_c @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(34,axiom,
( top_to524132421um_b_c
= ( collec2086029184um_b_c @ top_to1201357528_b_c_o ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_337_top__set__def) ).
thf(180,plain,
( top_to524132421um_b_c
= ( collec2086029184um_b_c @ top_to1201357528_b_c_o ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(67,axiom,
denota1997846518gree_c @ nu @ nu2 @ ( static_FVDiff_a_c @ ( plus_a_c @ t1 @ t2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_agree) ).
thf(296,plain,
denota1997846518gree_c @ nu @ nu2 @ ( static_FVDiff_a_c @ ( plus_a_c @ t1 @ t2 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(31,axiom,
! [A: produc190496183real_c] :
( A
= ( produc394644079real_c @ ( produc2010422875real_c @ A ) @ ( produc314122909real_c @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_180_surjective__pairing) ).
thf(172,plain,
! [A: produc190496183real_c] :
( A
= ( produc394644079real_c @ ( produc2010422875real_c @ A ) @ ( produc314122909real_c @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(46,axiom,
! [A: produc190496183real_c,B: produc190496183real_c] :
( ( ( produc2010422875real_c @ A )
= ( produc2010422875real_c @ B ) )
=> ( ( ( produc314122909real_c @ A )
= ( produc314122909real_c @ B ) )
=> ( A = B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_162_prod__eqI) ).
thf(230,plain,
! [A: produc190496183real_c,B: produc190496183real_c] :
( ( ( produc2010422875real_c @ A )
= ( produc2010422875real_c @ B ) )
=> ( ( ( produc314122909real_c @ A )
= ( produc314122909real_c @ B ) )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(77,axiom,
( ( denota1997846518gree_c @ nu @ nu2 @ ( static_FVDiff_a_c @ t2 ) )
=> ( ( denota69106024_a_b_c @ i @ j
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ t2 ) ) ) ) )
=> ( ( denota229585092_a_b_c @ i @ t2 @ ( produc2010422875real_c @ nu ) @ ( produc314122909real_c @ nu ) )
= ( denota229585092_a_b_c @ j @ t2 @ ( produc2010422875real_c @ nu2 ) @ ( produc314122909real_c @ nu2 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_IH2) ).
thf(318,plain,
( ( denota1997846518gree_c @ nu @ nu2 @ ( static_FVDiff_a_c @ t2 ) )
=> ( ( denota69106024_a_b_c @ i @ j
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ t2 ) ) ) ) )
=> ( ( denota229585092_a_b_c @ i @ t2 @ ( produc2010422875real_c @ nu ) @ ( produc314122909real_c @ nu ) )
= ( denota229585092_a_b_c @ j @ t2 @ ( produc2010422875real_c @ nu2 ) @ ( produc314122909real_c @ nu2 ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(7,axiom,
! [A: trm_a_c,B: trm_a_c] :
( ( dfree_a_c @ A )
=> ( ( dfree_a_c @ B )
=> ( dfree_a_c @ ( times_a_c @ A @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_167_dfree__Times) ).
thf(98,plain,
! [A: trm_a_c,B: trm_a_c] :
( ( dfree_a_c @ A )
=> ( ( dfree_a_c @ B )
=> ( dfree_a_c @ ( times_a_c @ A @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(70,axiom,
( ord_le929608341um_b_c
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ t1 ) ) ) )
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ ( plus_a_c @ t1 @ t2 ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_subs_I1_J) ).
thf(303,plain,
( ord_le929608341um_b_c
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ t1 ) ) ) )
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ ( plus_a_c @ t1 @ t2 ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(86,axiom,
( denota69106024_a_b_c @ i @ j
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ t2 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_IA2) ).
thf(345,plain,
( denota69106024_a_b_c @ i @ j
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ t2 ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(79,axiom,
! [A: trm_a_c,B: produc190496183real_c,C: produc190496183real_c,D: denota231621370t_unit] :
( ( dfree_a_c @ A )
=> ( ( denota1997846518gree_c @ B @ C @ ( static_FVDiff_a_c @ A ) )
=> ( ( denota229585092_a_b_c @ D @ A @ ( produc2010422875real_c @ B ) @ ( produc314122909real_c @ B ) )
= ( denota229585092_a_b_c @ D @ A @ ( produc2010422875real_c @ C ) @ ( produc314122909real_c @ C ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_coincidence__frechet) ).
thf(323,plain,
! [A: trm_a_c,B: produc190496183real_c,C: produc190496183real_c,D: denota231621370t_unit] :
( ( dfree_a_c @ A )
=> ( ( denota1997846518gree_c @ B @ C @ ( static_FVDiff_a_c @ A ) )
=> ( ( denota229585092_a_b_c @ D @ A @ ( produc2010422875real_c @ B ) @ ( produc314122909real_c @ B ) )
= ( denota229585092_a_b_c @ D @ A @ ( produc2010422875real_c @ C ) @ ( produc314122909real_c @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(4,axiom,
! [A: produc190496183real_c,B: produc190496183real_c] :
( ( ord_le850691415real_c @ A @ B )
=> ( ord_le775706699real_c @ ( produc314122909real_c @ A ) @ ( produc314122909real_c @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_256_snd__mono) ).
thf(91,plain,
! [A: produc190496183real_c,B: produc190496183real_c] :
( ( ord_le850691415real_c @ A @ B )
=> ( ord_le775706699real_c @ ( produc314122909real_c @ A ) @ ( produc314122909real_c @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(25,axiom,
! [A: sum_su737395349um_b_c > $o,B: sum_su737395349um_b_c > $o] :
( ( ord_le929608341um_b_c @ ( collec2086029184um_b_c @ A ) @ ( collec2086029184um_b_c @ B ) )
= ( ! [C: sum_su737395349um_b_c] :
( ( A @ C )
=> ( B @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_289_Collect__mono__iff) ).
thf(155,plain,
! [A: sum_su737395349um_b_c > $o,B: sum_su737395349um_b_c > $o] :
( ( ord_le929608341um_b_c @ ( collec2086029184um_b_c @ A ) @ ( collec2086029184um_b_c @ B ) )
= ( ! [C: sum_su737395349um_b_c] :
( ( A @ C )
=> ( B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(38,axiom,
! [A: finite1398487019real_c > $o,B: finite1398487019real_c,C: finite1398487019real_c > $o,D: finite1398487019real_c] :
( ( A @ B )
=> ( ( C @ D )
=> ( ( A @ ( produc2010422875real_c @ ( produc394644079real_c @ B @ D ) ) )
& ( C @ ( produc314122909real_c @ ( produc394644079real_c @ B @ D ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_213_conjI__realizer) ).
thf(198,plain,
! [A: finite1398487019real_c > $o,B: finite1398487019real_c,C: finite1398487019real_c > $o,D: finite1398487019real_c] :
( ( A @ B )
=> ( ( C @ D )
=> ( ( A @ ( produc2010422875real_c @ ( produc394644079real_c @ B @ D ) ) )
& ( C @ ( produc314122909real_c @ ( produc394644079real_c @ B @ D ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(81,axiom,
! [A: produc190496183real_c,B: produc190496183real_c,C: a,D: c > trm_a_c,E: c] :
( ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ ( function_a_c @ C @ D ) ) )
=> ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ ( D @ E ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_agree__func) ).
thf(330,plain,
! [A: produc190496183real_c,B: produc190496183real_c,C: a,D: c > trm_a_c,E: c] :
( ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ ( function_a_c @ C @ D ) ) )
=> ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ ( D @ E ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(19,axiom,
! [A: a,B: a] :
( ( ( sum_In2139678582um_b_c @ A )
= ( sum_In2139678582um_b_c @ B ) )
= ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_261_old_Osum_Oinject_I1_J) ).
thf(135,plain,
! [A: a,B: a] :
( ( ( sum_In2139678582um_b_c @ A )
= ( sum_In2139678582um_b_c @ B ) )
= ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(45,axiom,
! [A: finite1398487019real_c,B: finite1398487019real_c,C: finite1398487019real_c] :
( ( ( produc314122909real_c @ ( produc394644079real_c @ A @ B ) )
= C )
=> ( B = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_153_snd__eqD) ).
thf(226,plain,
! [A: finite1398487019real_c,B: finite1398487019real_c,C: finite1398487019real_c] :
( ( ( produc314122909real_c @ ( produc394644079real_c @ A @ B ) )
= C )
=> ( B = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(29,axiom,
! [A: finite1398487019real_c,B: finite1398487019real_c] :
( ( produc2010422875real_c @ ( produc394644079real_c @ A @ B ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_fst__conv) ).
thf(167,plain,
! [A: finite1398487019real_c,B: finite1398487019real_c] :
( ( produc2010422875real_c @ ( produc394644079real_c @ A @ B ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(39,axiom,
! [A: produc190496183real_c] :
( ( produc394644079real_c @ ( produc2010422875real_c @ A ) @ ( produc314122909real_c @ A ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_prod_Ocollapse) ).
thf(209,plain,
! [A: produc190496183real_c] :
( ( produc394644079real_c @ ( produc2010422875real_c @ A ) @ ( produc314122909real_c @ A ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(22,axiom,
! [A: finite1398487019real_c > finite1398487019real_c > $o,B: finite1398487019real_c,C: finite1398487019real_c] :
( ( A @ B @ C )
=> ( A @ ( produc314122909real_c @ ( produc394644079real_c @ C @ B ) ) @ ( produc2010422875real_c @ ( produc394644079real_c @ C @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_exI__realizer) ).
thf(145,plain,
! [A: finite1398487019real_c > finite1398487019real_c > $o,B: finite1398487019real_c,C: finite1398487019real_c] :
( ( A @ B @ C )
=> ( A @ ( produc314122909real_c @ ( produc394644079real_c @ C @ B ) ) @ ( produc2010422875real_c @ ( produc394644079real_c @ C @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(6,axiom,
! [A: finite1398487019real_c,B: finite1398487019real_c,C: finite1398487019real_c,D: finite1398487019real_c] :
( ( ord_le775706699real_c @ A @ B )
=> ( ( ord_le775706699real_c @ C @ D )
=> ( ord_le850691415real_c @ ( produc394644079real_c @ A @ C ) @ ( produc394644079real_c @ B @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_Pair__mono) ).
thf(95,plain,
! [A: finite1398487019real_c,B: finite1398487019real_c,C: finite1398487019real_c,D: finite1398487019real_c] :
( ( ord_le775706699real_c @ A @ B )
=> ( ( ord_le775706699real_c @ C @ D )
=> ( ord_le850691415real_c @ ( produc394644079real_c @ A @ C ) @ ( produc394644079real_c @ B @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(80,axiom,
! [A: produc190496183real_c,B: produc190496183real_c,C: trm_a_c,D: trm_a_c] :
( ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ ( plus_a_c @ C @ D ) ) )
=> ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_agree__plus1) ).
thf(327,plain,
! [A: produc190496183real_c,B: produc190496183real_c,C: trm_a_c,D: trm_a_c] :
( ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ ( plus_a_c @ C @ D ) ) )
=> ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(83,axiom,
dfree_a_c @ t2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_dfree2) ).
thf(336,plain,
dfree_a_c @ t2,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(32,axiom,
! [A: trm_a_c,B: trm_a_c,C: trm_a_c,D: trm_a_c] :
( ( ( times_a_c @ A @ B )
= ( times_a_c @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_trm_Oinject_I5_J) ).
thf(175,plain,
! [A: trm_a_c,B: trm_a_c,C: trm_a_c,D: trm_a_c] :
( ( ( times_a_c @ A @ B )
= ( times_a_c @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(76,axiom,
! [A: trm_a_c,B: produc190496183real_c,C: produc190496183real_c,D: denota231621370t_unit,E: denota231621370t_unit] :
( ( dfree_a_c @ A )
=> ( ( denota1997846518gree_c @ B @ C @ ( static_FVT_a_c @ A ) )
=> ( ( denota69106024_a_b_c @ D @ E
@ ( collec2086029184um_b_c
@ ^ [F: sum_su737395349um_b_c] :
? [G: a] :
( ( F
= ( sum_In2139678582um_b_c @ G ) )
& ( member_a @ G @ ( static_SIGT_a_c @ A ) ) ) ) )
=> ( ( denota2042094639_a_b_c @ D @ A @ ( produc2010422875real_c @ B ) )
= ( denota2042094639_a_b_c @ E @ A @ ( produc2010422875real_c @ C ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_310_coincidence__sterm_H) ).
thf(314,plain,
! [A: trm_a_c,B: produc190496183real_c,C: produc190496183real_c,D: denota231621370t_unit,E: denota231621370t_unit] :
( ( dfree_a_c @ A )
=> ( ( denota1997846518gree_c @ B @ C @ ( static_FVT_a_c @ A ) )
=> ( ( denota69106024_a_b_c @ D @ E
@ ( collec2086029184um_b_c
@ ^ [F: sum_su737395349um_b_c] :
? [G: a] :
( ( F
= ( sum_In2139678582um_b_c @ G ) )
& ( member_a @ G @ ( static_SIGT_a_c @ A ) ) ) ) )
=> ( ( denota2042094639_a_b_c @ D @ A @ ( produc2010422875real_c @ B ) )
= ( denota2042094639_a_b_c @ E @ A @ ( produc2010422875real_c @ C ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(52,axiom,
! [A: trm_a_c,B: trm_a_c] :
( ( dfree_a_c @ A )
=> ( ( dfree_a_c @ B )
=> ( dfree_a_c @ ( plus_a_c @ A @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_166_dfree_Odfree__Plus) ).
thf(250,plain,
! [A: trm_a_c,B: trm_a_c] :
( ( dfree_a_c @ A )
=> ( ( dfree_a_c @ B )
=> ( dfree_a_c @ ( plus_a_c @ A @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(1,conjecture,
denota1997846518gree_c @ nu @ nu2 @ ( static_FVDiff_a_c @ t2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
thf(2,negated_conjecture,
~ ( denota1997846518gree_c @ nu @ nu2 @ ( static_FVDiff_a_c @ t2 ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(87,plain,
~ ( denota1997846518gree_c @ nu @ nu2 @ ( static_FVDiff_a_c @ t2 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(42,axiom,
! [A: produc190496183real_c] :
? [B: finite1398487019real_c,C: finite1398487019real_c] :
( A
= ( produc394644079real_c @ B @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_surj__pair) ).
thf(218,plain,
! [A: produc190496183real_c] :
? [B: finite1398487019real_c,C: finite1398487019real_c] :
( A
= ( produc394644079real_c @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(9,axiom,
! [A: c > trm_a_c,B: a] :
( ! [C: c] : ( dfree_a_c @ ( A @ C ) )
=> ( dfree_a_c @ ( function_a_c @ B @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_163_dfree__Fun) ).
thf(104,plain,
! [A: c > trm_a_c,B: a] :
( ! [C: c] : ( dfree_a_c @ ( A @ C ) )
=> ( dfree_a_c @ ( function_a_c @ B @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(71,axiom,
! [A: produc190496183real_c,B: produc190496183real_c,C: trm_a_c,D: trm_a_c] :
( ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ ( times_a_c @ C @ D ) ) )
=> ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_agree__times1) ).
thf(304,plain,
! [A: produc190496183real_c,B: produc190496183real_c,C: trm_a_c,D: trm_a_c] :
( ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ ( times_a_c @ C @ D ) ) )
=> ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(26,axiom,
dfree_a_c @ t1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_dfree1) ).
thf(158,plain,
dfree_a_c @ t1,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(12,axiom,
! [A: sum_su737395349um_b_c > $o,B: sum_su737395349um_b_c > $o] :
( ! [C: sum_su737395349um_b_c] :
( ( A @ C )
= ( B @ C ) )
=> ( ( collec2086029184um_b_c @ A )
= ( collec2086029184um_b_c @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_Collect__cong) ).
thf(114,plain,
! [A: sum_su737395349um_b_c > $o,B: sum_su737395349um_b_c > $o] :
( ! [C: sum_su737395349um_b_c] :
( ( A @ C )
= ( B @ C ) )
=> ( ( collec2086029184um_b_c @ A )
= ( collec2086029184um_b_c @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(24,axiom,
! [A: produc190496183real_c] :
~ ! [B: finite1398487019real_c,C: finite1398487019real_c] :
( A
!= ( produc394644079real_c @ B @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_108_old_Oprod_Oexhaust) ).
thf(151,plain,
! [A: produc190496183real_c] :
~ ! [B: finite1398487019real_c,C: finite1398487019real_c] :
( A
!= ( produc394644079real_c @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(69,axiom,
( ( denota1997846518gree_c @ nu @ nu2 @ ( static_FVDiff_a_c @ t1 ) )
=> ( ( denota69106024_a_b_c @ i @ j
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ t1 ) ) ) ) )
=> ( ( denota229585092_a_b_c @ i @ t1 @ ( produc2010422875real_c @ nu ) @ ( produc314122909real_c @ nu ) )
= ( denota229585092_a_b_c @ j @ t1 @ ( produc2010422875real_c @ nu2 ) @ ( produc314122909real_c @ nu2 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_IH1) ).
thf(300,plain,
( ( denota1997846518gree_c @ nu @ nu2 @ ( static_FVDiff_a_c @ t1 ) )
=> ( ( denota69106024_a_b_c @ i @ j
@ ( collec2086029184um_b_c
@ ^ [A: sum_su737395349um_b_c] :
? [B: a] :
( ( A
= ( sum_In2139678582um_b_c @ B ) )
& ( member_a @ B @ ( static_SIGT_a_c @ t1 ) ) ) ) )
=> ( ( denota229585092_a_b_c @ i @ t1 @ ( produc2010422875real_c @ nu ) @ ( produc314122909real_c @ nu ) )
= ( denota229585092_a_b_c @ j @ t1 @ ( produc2010422875real_c @ nu2 ) @ ( produc314122909real_c @ nu2 ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(59,axiom,
! [A: finite1398487019real_c > finite1398487019real_c > $o,B: produc190496183real_c] :
( ( A @ ( produc314122909real_c @ B ) @ ( produc2010422875real_c @ B ) )
=> ~ ! [C: finite1398487019real_c,D: finite1398487019real_c] :
~ ( A @ D @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_259_exE__realizer_H) ).
thf(273,plain,
! [A: finite1398487019real_c > finite1398487019real_c > $o,B: produc190496183real_c] :
( ( A @ ( produc314122909real_c @ B ) @ ( produc2010422875real_c @ B ) )
=> ~ ! [C: finite1398487019real_c,D: finite1398487019real_c] :
~ ( A @ D @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(10,axiom,
! [A: produc190496183real_c,B: produc190496183real_c] :
( ( ( ( produc2010422875real_c @ A )
= ( produc2010422875real_c @ B ) )
& ( ( produc314122909real_c @ A )
= ( produc314122909real_c @ B ) ) )
=> ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_159_prod_Oexpand) ).
thf(107,plain,
! [A: produc190496183real_c,B: produc190496183real_c] :
( ( ( ( produc2010422875real_c @ A )
= ( produc2010422875real_c @ B ) )
& ( ( produc314122909real_c @ A )
= ( produc314122909real_c @ B ) ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(49,axiom,
! [A: a,B: a] :
( ( ( sum_In2139678582um_b_c @ A )
= ( sum_In2139678582um_b_c @ B ) )
=> ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_301_Inl__inject) ).
thf(239,plain,
! [A: a,B: a] :
( ( ( sum_In2139678582um_b_c @ A )
= ( sum_In2139678582um_b_c @ B ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(37,axiom,
! [A: set_Su1783761653um_b_c] :
( ( collec2086029184um_b_c
@ ^ [B: sum_su737395349um_b_c] : ( member1893232190um_b_c @ B @ A ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_Collect__mem__eq) ).
thf(195,plain,
! [A: set_Su1783761653um_b_c] :
( ( collec2086029184um_b_c
@ ^ [B: sum_su737395349um_b_c] : ( member1893232190um_b_c @ B @ A ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(62,axiom,
! [A: produc190496183real_c > $o,B: produc190496183real_c] :
( ! [C: finite1398487019real_c,D: finite1398487019real_c] : ( A @ ( produc394644079real_c @ C @ D ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_old_Oprod_Oinducts) ).
thf(283,plain,
! [A: produc190496183real_c > $o,B: produc190496183real_c] :
( ! [C: finite1398487019real_c,D: finite1398487019real_c] : ( A @ ( produc394644079real_c @ C @ D ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(66,axiom,
! [A: produc190496183real_c,B: set_Sum_sum_c_c] : ( denota1997846518gree_c @ A @ A @ B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_agree__refl) ).
thf(294,plain,
! [A: produc190496183real_c,B: set_Sum_sum_c_c] : ( denota1997846518gree_c @ A @ A @ B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(15,axiom,
( ( (=) @ produc190496183real_c )
= ( ^ [A: produc190496183real_c,B: produc190496183real_c] :
( ( ( produc2010422875real_c @ A )
= ( produc2010422875real_c @ B ) )
& ( ( produc314122909real_c @ A )
= ( produc314122909real_c @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_156_prod__eq__iff) ).
thf(126,plain,
( ( (=) @ produc190496183real_c )
= ( ^ [A: produc190496183real_c,B: produc190496183real_c] :
( ( ( produc2010422875real_c @ A )
= ( produc2010422875real_c @ B ) )
& ( ( produc314122909real_c @ A )
= ( produc314122909real_c @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(17,axiom,
! [A: denota231621370t_unit,B: denota231621370t_unit,C: set_Su1783761653um_b_c] :
( ( denota69106024_a_b_c @ A @ B @ C )
=> ( denota69106024_a_b_c @ B @ A @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_Iagree__comm) ).
thf(131,plain,
! [A: denota231621370t_unit,B: denota231621370t_unit,C: set_Su1783761653um_b_c] :
( ( denota69106024_a_b_c @ A @ B @ C )
=> ( denota69106024_a_b_c @ B @ A @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(33,axiom,
! [A: a] : ( member_a @ A @ top_top_set_a ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_320_UNIV__I) ).
thf(178,plain,
! [A: a] : ( member_a @ A @ top_top_set_a ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(84,axiom,
! [A: produc190496183real_c,B: produc190496183real_c,C: trm_a_c,D: trm_a_c] :
( ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ ( plus_a_c @ C @ D ) ) )
=> ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_agree__plus2) ).
thf(337,plain,
! [A: produc190496183real_c,B: produc190496183real_c,C: trm_a_c,D: trm_a_c] :
( ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ ( plus_a_c @ C @ D ) ) )
=> ( denota1997846518gree_c @ A @ B @ ( static_FVDiff_a_c @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(74,axiom,
! [A: produc190496183real_c,B: produc190496183real_c,C: set_Sum_sum_c_c] :
( ( denota1997846518gree_c @ A @ B @ C )
=> ( denota1997846518gree_c @ B @ A @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_agree__comm) ).
thf(309,plain,
! [A: produc190496183real_c,B: produc190496183real_c,C: set_Sum_sum_c_c] :
( ( denota1997846518gree_c @ A @ B @ C )
=> ( denota1997846518gree_c @ B @ A @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(41,axiom,
! [A: sum_su737395349um_b_c,B: sum_su737395349um_b_c > $o] :
( ( member1893232190um_b_c @ A @ ( collec2086029184um_b_c @ B ) )
= ( B @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_mem__Collect__eq) ).
thf(215,plain,
! [A: sum_su737395349um_b_c,B: sum_su737395349um_b_c > $o] :
( ( member1893232190um_b_c @ A @ ( collec2086029184um_b_c @ B ) )
= ( B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(346,plain,
$false,
inference(e,[status(thm)],[142,110,93,224,291,159,182,246,138,101,333,88,170,276,308,120,269,185,288,257,164,321,253,147,280,221,133,265,307,292,233,117,260,297,339,212,244,266,311,128,237,180,296,172,230,318,98,303,345,323,91,155,198,330,135,226,167,209,145,95,327,336,175,314,250,87,218,104,304,158,114,151,300,273,107,239,195,283,294,126,131,178,337,309,215]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP038^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.08/0.22 % Computer : n009.cluster.edu
% 0.08/0.22 % Model : x86_64 x86_64
% 0.08/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.22 % Memory : 8046.5625MB
% 0.08/0.22 % OS : Linux 6.8.0-71-generic
% 0.08/0.22 % CPULimit : 300
% 0.08/0.22 % WCLimit : 300
% 0.08/0.22 % DateTime : Tue Sep 29 19:40:15 UTC 2026
% 0.08/0.23 % CPUTime :
% 0.08/0.23 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.03/0.80 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.41/1.24 % [INFO] Parsing done (435ms).
% 2.41/1.26 % [INFO] Running in sequential loop mode.
% 3.90/1.65 % [INFO] eprover registered as external prover.
% 3.90/1.66 % [INFO] Scanning for conjecture ...
% 4.36/1.84 % [INFO] Found a conjecture (or negated_conjecture) and 357 axioms. Running axiom selection ...
% 4.55/1.95 % [INFO] Axiom selection finished. Selected 84 axioms (removed 273 axioms).
% 4.92/2.10 % [INFO] Problem is higher-order (TPTP THF).
% 4.92/2.12 % [INFO] Type checking passed.
% 4.92/2.13 % [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 ...
% 11.97/3.93 % External prover 'e' found a proof!
% 11.97/3.93 % [INFO] Killing All external provers ...
% 11.97/3.94 % Time passed: 3574ms (effective reasoning time: 2667ms)
% 11.97/3.94 % 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)>
% 11.97/3.94 % Axioms used in derivation (84): fact_6_agree__plus1, fact_34_IA2, fact_33_IA1, fact_254_fst__mono, fact_51_dfree__Times__simps, fact_156_prod__eq__iff, fact_4_dfree2, fact_167_dfree__Times, fact_171_trm_Odistinct_I25_J, fact_261_old_Osum_Oinject_I1_J, fact_65_old_Oprod_Oinject, fact_100_agree__sub, fact_303_Collect__subset, fact_30_coincidence__frechet, fact_3_agree1, fact_32_IA, fact_135_fst__conv, fact_141_fst__eqD, fact_86_mem__Collect__eq, fact_35_IH1, fact_260_sum_Oinject_I1_J, fact_246_Pair__mono, fact_180_surjective__pairing, fact_220_less__eq__prod__def, fact_102_agree__supset, fact_98_Collect__cong, fact_70_prod_Oinject, fact_2_agree, fact_242_subset__CollectI, fact_267_subsetI, fact_79_trm_Oinject_I5_J, fact_256_snd__mono, fact_339_Vagree__univ, fact_1_agree__plus2, fact_315_FVDiff__sub, fact_118_prod__cases, fact_8_agree__comm, fact_36_Iagree__comm, fact_47_prod_Ocollapse, fact_186_prod_Oexhaust__sel, fact_329_UNIV__witness, fact_296_Collect__mono, fact_301_Inl__inject, fact_331_UNIV__eq__I, fact_259_exE__realizer_H, fact_213_conjI__realizer, fact_16_agree__times1, fact_20_agree__func, fact_123_surj__pair, fact_174_trm_Odistinct_I31_J, fact_159_prod_Oexpand, fact_219_exI__realizer, fact_22_IH2, fact_320_UNIV__I, fact_289_Collect__mono__iff, fact_147_snd__conv, fact_55_dfree__Fun__simps, fact_11_dfree1, fact_169_trm_Odistinct_I23_J, fact_10_agree__refl, fact_230_Iagree__sub, fact_92_Collect__mem__eq, fact_197_directional__derivative__def, fact_39_subs_I1_J, fact_310_coincidence__sterm_H, fact_108_old_Oprod_Oexhaust, fact_37_Iagree__refl, fact_113_Pair__inject, fact_162_prod__eqI, fact_38_subs_I2_J, fact_153_snd__eqD, fact_337_top__set__def, fact_236_subset__Collect__iff, fact_103_old_Oprod_Oinducts, fact_166_dfree_Odfree__Plus, fact_190_Pair__le, fact_18_agree__times2, fact_78_trm_Oinject_I4_J, fact_340_agree__UNIV__eq, fact_54_dfree__Plus__simps, fact_75_trm_Oinject_I3_J, fact_305_sterm__determines__frechet, fact_207_BNF__Greatest__Fixpoint_Osubst__Pair, fact_163_dfree__Fun
% 11.97/3.94 % No. of inferences in proof: 172
% 11.97/3.94 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 3574 ms resp. 2667 ms w/o parsing
% 12.64/4.07 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 12.64/4.08 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------