%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP256^2 : TPTP v9.3.1. Bugfixed v9.2.1.
% 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 : n013.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:07:25 AM UTC 2026
% Result : Theorem 85.53s 61.07s
% Output : Refutation 86.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 160
% Syntax : Number of formulae : 322 ( 142 unt; 0 typ; 0 def)
% Number of atoms : 1046 ( 392 equ; 10 cnn)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 5053 ( 76 ~; 14 |; 86 &;4447 @)
% ( 0 <=>; 430 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 8 avg)
% Number of types : 12 ( 11 usr)
% Number of type conns : 268 ( 268 >; 0 *; 0 +; 0 <<)
% Number of symbols : 40 ( 37 usr; 12 con; 0-5 aty)
% Number of variables : 1314 ( 52 ^;1210 !; 52 ?;1314 :)
% Comments :
%------------------------------------------------------------------------------
thf(vEBT_VEBT_type,type,
vEBT_VEBT: $tType ).
thf(code_integer_type,type,
code_integer: $tType ).
thf(code_term_type,type,
code_term: $tType ).
thf(product_unit_type,type,
product_unit: $tType ).
thf(extended_enat_type,type,
extended_enat: $tType ).
thf(complex_type,type,
complex: $tType ).
thf(real_type,type,
real: $tType ).
thf(rat_type,type,
rat: $tType ).
thf(num_type,type,
num: $tType ).
thf(nat_type,type,
nat: $tType ).
thf(int_type,type,
int: $tType ).
thf(size_decl,type,
size:
!>[TA: $tType] : $o ).
thf(append_decl,type,
append:
!>[TA: $tType] : ( ( list @ TA ) > ( list @ TA ) > ( list @ TA ) ) ).
thf(butlast_decl,type,
butlast:
!>[TA: $tType] : ( ( list @ TA ) > ( list @ TA ) ) ).
thf(distinct_decl,type,
distinct:
!>[TA: $tType] : ( ( list @ TA ) > $o ) ).
thf(find_decl,type,
find:
!>[TA: $tType] : ( ( TA > $o ) > ( list @ TA ) > ( option @ TA ) ) ).
thf(list_all2_decl,type,
list_all2:
!>[TA: $tType,TB: $tType] : ( ( TB > TA > $o ) > ( list @ TB ) > ( list @ TA ) > $o ) ).
thf(map_decl,type,
map:
!>[TA: $tType,TB: $tType] : ( ( TB > TA ) > ( list @ TB ) > ( list @ TA ) ) ).
thf(set2_decl,type,
set2:
!>[TA: $tType] : ( ( list @ TA ) > ( set @ TA ) ) ).
thf(list_update_decl,type,
list_update:
!>[TA: $tType] : ( ( list @ TA ) > nat > TA > ( list @ TA ) ) ).
thf(nth_decl,type,
nth:
!>[TA: $tType] : ( ( list @ TA ) > nat > TA ) ).
thf(sorted_wrt_decl,type,
sorted_wrt:
!>[TA: $tType] : ( ( TA > TA > $o ) > ( list @ TA ) > $o ) ).
thf(takeWhile_decl,type,
takeWhile:
!>[TA: $tType] : ( ( TA > $o ) > ( list @ TA ) > ( list @ TA ) ) ).
thf(size_size_decl,type,
size_size:
!>[TA: $tType] : ( TA > nat ) ).
thf(some_decl,type,
some:
!>[TA: $tType] : ( TA > ( option @ TA ) ) ).
thf(ord_less_decl,type,
ord_less:
!>[TA: $tType] : ( TA > TA > $o ) ).
thf(ord_less_eq_decl,type,
ord_less_eq:
!>[TA: $tType] : ( TA > TA > $o ) ).
thf(vEBT_V8194947554948674370ptions_decl,type,
vEBT_V8194947554948674370ptions: vEBT_VEBT > nat > $o ).
thf(vEBT_VEBT_high_decl,type,
vEBT_VEBT_high: nat > nat > nat ).
thf(vEBT_V5917875025757280293ildren_decl,type,
vEBT_V5917875025757280293ildren: nat > ( list @ vEBT_VEBT ) > nat > $o ).
thf(vEBT_VEBT_low_decl,type,
vEBT_VEBT_low: nat > nat > nat ).
thf(vEBT_VEBT_valid_decl,type,
vEBT_VEBT_valid: vEBT_VEBT > nat > $o ).
thf(vEBT_invar_vebt_decl,type,
vEBT_invar_vebt: vEBT_VEBT > nat > $o ).
thf(vEBT_vebt_delete_decl,type,
vEBT_vebt_delete: vEBT_VEBT > nat > vEBT_VEBT ).
thf(vEBT_VEBT_minNull_decl,type,
vEBT_VEBT_minNull: vEBT_VEBT > $o ).
thf(vEBT_vebt_member_decl,type,
vEBT_vebt_member: vEBT_VEBT > nat > $o ).
thf(vEBT_vebt_maxt_decl,type,
vEBT_vebt_maxt: vEBT_VEBT > ( option @ nat ) ).
thf(member_decl,type,
member:
!>[TA: $tType] : ( TA > ( set @ TA ) > $o ) ).
thf(m_decl,type,
m: nat ).
thf(ma_decl,type,
ma: nat ).
thf(maxi_decl,type,
maxi: nat ).
thf(mi_decl,type,
mi: nat ).
thf(na_decl,type,
na: nat ).
thf(treeList_decl,type,
treeList: list @ vEBT_VEBT ).
thf(xa_decl,type,
xa: nat ).
thf(107,axiom,
! [TA: $tType,A: nat,B: nat,C: list @ TA,D: TA,E: TA] :
( ( A != B )
=> ( ( list_update @ TA @ ( list_update @ TA @ C @ A @ D ) @ B @ E )
= ( list_update @ TA @ ( list_update @ TA @ C @ B @ E ) @ A @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_list__update__swap) ).
thf(629,plain,
! [TA: $tType,A: nat,B: nat,C: list @ TA,D: TA,E: TA] :
( ( A != B )
=> ( ( list_update @ TA @ ( list_update @ TA @ C @ A @ D ) @ B @ E )
= ( list_update @ TA @ ( list_update @ TA @ C @ B @ E ) @ A @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[107]) ).
thf(75,axiom,
! [A: vEBT_VEBT,B: nat,C: nat] :
( ( vEBT_invar_vebt @ A @ B )
=> ( ( vEBT_V8194947554948674370ptions @ A @ C )
=> ( vEBT_vebt_member @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_111_valid__member__both__member__options) ).
thf(479,plain,
! [A: vEBT_VEBT,B: nat,C: nat] :
( ( vEBT_invar_vebt @ A @ B )
=> ( ( vEBT_V8194947554948674370ptions @ A @ C )
=> ( vEBT_vebt_member @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(106,axiom,
ord_less @ nat @ mi @ ma,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_mimapr) ).
thf(628,plain,
ord_less @ nat @ mi @ ma,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[106]) ).
thf(86,axiom,
! [TA: $tType,A: list @ TA,B: list @ TA,C: TA > $o,D: TA > $o] :
( ( A = B )
=> ( ! [E: TA] :
( ( member @ TA @ E @ ( set2 @ TA @ A ) )
=> ( ( C @ E )
= ( D @ E ) ) )
=> ( ( takeWhile @ TA @ C @ A )
= ( takeWhile @ TA @ D @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6895_takeWhile__cong) ).
thf(518,plain,
! [TA: $tType,A: list @ TA,B: list @ TA,C: TA > $o,D: TA > $o] :
( ( A = B )
=> ( ! [E: TA] :
( ( member @ TA @ E @ ( set2 @ TA @ A ) )
=> ( ( C @ E )
= ( D @ E ) ) )
=> ( ( takeWhile @ TA @ C @ A )
= ( takeWhile @ TA @ D @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(73,axiom,
! [TA: $tType,A: list @ TA,B: TA > $o,C: list @ TA] :
( ( ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ A ) )
=> ( B @ D ) )
=> ( ( takeWhile @ TA @ B @ ( append @ TA @ A @ C ) )
= ( append @ TA @ A @ ( takeWhile @ TA @ B @ C ) ) ) )
& ( ~ ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ A ) )
=> ( B @ D ) )
=> ( ( takeWhile @ TA @ B @ ( append @ TA @ A @ C ) )
= ( takeWhile @ TA @ B @ A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6901_takeWhile__append) ).
thf(468,plain,
! [TA: $tType,A: list @ TA,B: TA > $o,C: list @ TA] :
( ( ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ A ) )
=> ( B @ D ) )
=> ( ( takeWhile @ TA @ B @ ( append @ TA @ A @ C ) )
= ( append @ TA @ A @ ( takeWhile @ TA @ B @ C ) ) ) )
& ( ~ ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ A ) )
=> ( B @ D ) )
=> ( ( takeWhile @ TA @ B @ ( append @ TA @ A @ C ) )
= ( takeWhile @ TA @ B @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(154,axiom,
size @ vEBT_VEBT,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_VEBT__Definitions_OVEBT___Nat_Osize_624) ).
thf(777,plain,
size @ vEBT_VEBT,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[154]) ).
thf(92,axiom,
! [TA: $tType,A: list @ TA,B: TA] :
( ( distinct @ TA @ A )
=> ( ( member @ TA @ B @ ( set2 @ TA @ A ) )
=> ? [C: nat] :
( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ A ) )
& ( ( nth @ TA @ A @ C )
= B )
& ! [D: nat] :
( ( ( ord_less @ nat @ D @ ( size_size @ ( list @ TA ) @ A ) )
& ( ( nth @ TA @ A @ D )
= B ) )
=> ( D = C ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3456_distinct__Ex1) ).
thf(555,plain,
! [TA: $tType,A: list @ TA,B: TA] :
( ( distinct @ TA @ A )
=> ( ( member @ TA @ B @ ( set2 @ TA @ A ) )
=> ? [C: nat] :
( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ A ) )
& ( ( nth @ TA @ A @ C )
= B )
& ! [D: nat] :
( ( ( ord_less @ nat @ D @ ( size_size @ ( list @ TA ) @ A ) )
& ( ( nth @ TA @ A @ D )
= B ) )
=> ( D = C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
thf(96,axiom,
size @ nat,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Nat_Osize) ).
thf(582,plain,
size @ nat,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).
thf(114,axiom,
! [TA: $tType,A: TA > TA > $o,B: list @ TA,C: nat,D: nat] :
( ( sorted_wrt @ TA @ A @ B )
=> ( ( ord_less @ nat @ C @ D )
=> ( ( ord_less @ nat @ D @ ( size_size @ ( list @ TA ) @ B ) )
=> ( A @ ( nth @ TA @ B @ C ) @ ( nth @ TA @ B @ D ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6808_sorted__wrt__nth__less) ).
thf(655,plain,
! [TA: $tType,A: TA > TA > $o,B: list @ TA,C: nat,D: nat] :
( ( sorted_wrt @ TA @ A @ B )
=> ( ( ord_less @ nat @ C @ D )
=> ( ( ord_less @ nat @ D @ ( size_size @ ( list @ TA ) @ B ) )
=> ( A @ ( nth @ TA @ B @ C ) @ ( nth @ TA @ B @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[114]) ).
thf(53,axiom,
! [TA: $tType,A: TA > TA > $o,B: list @ TA] :
( ! [C: TA] : ( A @ C @ C )
=> ( list_all2 @ TA @ TA @ A @ B @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7466_list__all2__refl) ).
thf(385,plain,
! [TA: $tType,A: TA > TA > $o,B: list @ TA] :
( ! [C: TA] : ( A @ C @ C )
=> ( list_all2 @ TA @ TA @ A @ B @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(89,axiom,
! [TA: $tType,A: list @ TA,B: list @ TA,C: TA > $o,D: TA > $o] :
( ( A = B )
=> ( ! [E: TA] :
( ( member @ TA @ E @ ( set2 @ TA @ B ) )
=> ( ( C @ E )
= ( D @ E ) ) )
=> ( ( find @ TA @ C @ A )
= ( find @ TA @ D @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_636_find__cong) ).
thf(538,plain,
! [TA: $tType,A: list @ TA,B: list @ TA,C: TA > $o,D: TA > $o] :
( ( A = B )
=> ( ! [E: TA] :
( ( member @ TA @ E @ ( set2 @ TA @ B ) )
=> ( ( C @ E )
= ( D @ E ) ) )
=> ( ( find @ TA @ C @ A )
= ( find @ TA @ D @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(157,axiom,
! [A: vEBT_VEBT,B: nat] :
( ( vEBT_VEBT_valid @ A @ B )
=> ( vEBT_invar_vebt @ A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_valid__eq2) ).
thf(782,plain,
! [A: vEBT_VEBT,B: nat] :
( ( vEBT_VEBT_valid @ A @ B )
=> ( vEBT_invar_vebt @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[157]) ).
thf(132,axiom,
! [TA: $tType,A: TA > $o,B: list @ TA] :
( ( ord_less @ nat @ ( size_size @ ( list @ TA ) @ ( takeWhile @ TA @ A @ B ) ) @ ( size_size @ ( list @ TA ) @ B ) )
=> ~ ( A @ ( nth @ TA @ B @ ( size_size @ ( list @ TA ) @ ( takeWhile @ TA @ A @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6899_nth__length__takeWhile) ).
thf(709,plain,
! [TA: $tType,A: TA > $o,B: list @ TA] :
( ( ord_less @ nat @ ( size_size @ ( list @ TA ) @ ( takeWhile @ TA @ A @ B ) ) @ ( size_size @ ( list @ TA ) @ B ) )
=> ~ ( A @ ( nth @ TA @ B @ ( size_size @ ( list @ TA ) @ ( takeWhile @ TA @ A @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[132]) ).
thf(60,axiom,
! [TA: $tType,A: TA > $o,B: list @ TA] :
( ( takeWhile @ TA @ A @ ( takeWhile @ TA @ A @ B ) )
= ( takeWhile @ TA @ A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6878_takeWhile__idem) ).
thf(417,plain,
! [TA: $tType,A: TA > $o,B: list @ TA] :
( ( takeWhile @ TA @ A @ ( takeWhile @ TA @ A @ B ) )
= ( takeWhile @ TA @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(37,axiom,
! [TA: $tType,TB: $tType,A: list @ TA,B: TA > TB,C: TA > TB] :
( ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ A ) )
=> ( ( B @ D )
= ( C @ D ) ) )
=> ( ( map @ TA @ TB @ B @ A )
= ( map @ TA @ TB @ C @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6193_list_Omap__cong0) ).
thf(288,plain,
! [TA: $tType,TB: $tType,A: list @ TA,B: TA > TB,C: TA > TB] :
( ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ A ) )
=> ( ( B @ D )
= ( C @ D ) ) )
=> ( ( map @ TA @ TB @ B @ A )
= ( map @ TA @ TB @ C @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(40,axiom,
! [TA: $tType,A: TA > $o,B: TA,C: TA > nat,D: nat] :
( ( A @ B )
=> ( ! [E: TA] :
( ( A @ E )
=> ( ord_less @ nat @ ( C @ E ) @ D ) )
=> ? [E: TA] :
( ( A @ E )
& ! [F: TA] :
( ( A @ F )
=> ( ord_less_eq @ nat @ ( C @ F ) @ ( C @ E ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_284_Lattices__Big_Oex__has__greatest__nat) ).
thf(301,plain,
! [TA: $tType,A: TA > $o,B: TA,C: TA > nat,D: nat] :
( ( A @ B )
=> ( ! [E: TA] :
( ( A @ E )
=> ( ord_less @ nat @ ( C @ E ) @ D ) )
=> ? [E: TA] :
( ( A @ E )
& ! [F: TA] :
( ( A @ F )
=> ( ord_less_eq @ nat @ ( C @ F ) @ ( C @ E ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(65,axiom,
! [TA: $tType] :
( ( map @ TA @ TA
@ ^ [A: TA] : A )
= ( ^ [A: list @ TA] : A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6155_map__ident) ).
thf(436,plain,
! [TA: $tType] :
( ( map @ TA @ TA
@ ^ [A: TA] : A )
= ( ^ [A: list @ TA] : A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(113,axiom,
! [TA: $tType] :
( ( size @ TA )
=> ! [A: TA,B: TA] :
( ( ( size_size @ TA @ A )
!= ( size_size @ TA @ B ) )
=> ( A != B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_size__neq__size__imp__neq) ).
thf(651,plain,
! [TA: $tType] :
( ( size @ TA )
=> ! [A: TA,B: TA] :
( ( ( size_size @ TA @ A )
!= ( size_size @ TA @ B ) )
=> ( A != B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[113]) ).
thf(136,axiom,
ord_less_eq @ nat @ mi @ ma,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21__C4_Ohyps_C_I7_J) ).
thf(724,plain,
ord_less_eq @ nat @ mi @ ma,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[136]) ).
thf(81,axiom,
! [TA: $tType,TB: $tType,A: TB > TA > $o,B: list @ TB,C: list @ TA,D: TB > TA > $o] :
( ( list_all2 @ TB @ TA @ A @ B @ C )
=> ( ! [E: TB,F: TA] :
( ( A @ E @ F )
=> ( D @ E @ F ) )
=> ( list_all2 @ TB @ TA @ D @ B @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7465_list__all2__mono) ).
thf(504,plain,
! [TA: $tType,TB: $tType,A: TB > TA > $o,B: list @ TB,C: list @ TA,D: TB > TA > $o] :
( ( list_all2 @ TB @ TA @ A @ B @ C )
=> ( ! [E: TB,F: TA] :
( ( A @ E @ F )
=> ( D @ E @ F ) )
=> ( list_all2 @ TB @ TA @ D @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(70,axiom,
! [A: nat,B: nat] :
( ( ord_less @ nat @ A @ B )
=> ( ord_less_eq @ nat @ A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_less__imp__le__nat) ).
thf(460,plain,
! [A: nat,B: nat] :
( ( ord_less @ nat @ A @ B )
=> ( ord_less_eq @ nat @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(110,axiom,
! [A: nat,B: nat] :
( ( A != B )
= ( ( ord_less @ nat @ A @ B )
| ( ord_less @ nat @ B @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_nat__neq__iff) ).
thf(638,plain,
! [A: nat,B: nat] :
( ( A != B )
= ( ( ord_less @ nat @ A @ B )
| ( ord_less @ nat @ B @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[110]) ).
thf(10,axiom,
! [TA: $tType,TB: $tType,A: TA > TB,B: list @ TA,C: list @ TB,D: list @ TB] :
( ( ( map @ TA @ TB @ A @ B )
= ( append @ TB @ C @ D ) )
= ( ? [E: list @ TA,F: list @ TA] :
( ( B
= ( append @ TA @ E @ F ) )
& ( C
= ( map @ TA @ TB @ A @ E ) )
& ( D
= ( map @ TA @ TB @ A @ F ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6409_map__eq__append__conv) ).
thf(189,plain,
! [TA: $tType,TB: $tType,A: TA > TB,B: list @ TA,C: list @ TB,D: list @ TB] :
( ( ( map @ TA @ TB @ A @ B )
= ( append @ TB @ C @ D ) )
= ( ? [E: list @ TA,F: list @ TA] :
( ( B
= ( append @ TA @ E @ F ) )
& ( C
= ( map @ TA @ TB @ A @ E ) )
& ( D
= ( map @ TA @ TB @ A @ F ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(151,axiom,
m = na,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0__C4_Ohyps_C_I3_J) ).
thf(770,plain,
m = na,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[151]) ).
thf(68,axiom,
! [TA: $tType,A: list @ TA,B: TA > $o,C: TA] :
( ! [D: nat] :
( ( ord_less @ nat @ D @ ( size_size @ ( list @ TA ) @ A ) )
=> ( B @ ( nth @ TA @ A @ D ) ) )
=> ( ( member @ TA @ C @ ( set2 @ TA @ A ) )
=> ( B @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_all__nth__imp__all__set) ).
thf(448,plain,
! [TA: $tType,A: list @ TA,B: TA > $o,C: TA] :
( ! [D: nat] :
( ( ord_less @ nat @ D @ ( size_size @ ( list @ TA ) @ A ) )
=> ( B @ ( nth @ TA @ A @ D ) ) )
=> ( ( member @ TA @ C @ ( set2 @ TA @ A ) )
=> ( B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(41,axiom,
! [TA: $tType,TB: $tType,A: list @ TB,B: list @ TB,C: list @ TA,D: list @ TA,E: TB > TA > $o,F: TB > TA > $o] :
( ( A = B )
=> ( ( C = D )
=> ( ! [G: TB,H: TA] :
( ( member @ TB @ G @ ( set2 @ TB @ B ) )
=> ( ( member @ TA @ H @ ( set2 @ TA @ D ) )
=> ( ( E @ G @ H )
= ( F @ G @ H ) ) ) )
=> ( ( list_all2 @ TB @ TA @ E @ A @ C )
= ( list_all2 @ TB @ TA @ F @ B @ D ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7499_list_Orel__cong) ).
thf(316,plain,
! [TA: $tType,TB: $tType,A: list @ TB,B: list @ TB,C: list @ TA,D: list @ TA,E: TB > TA > $o,F: TB > TA > $o] :
( ( A = B )
=> ( ( C = D )
=> ( ! [G: TB,H: TA] :
( ( member @ TB @ G @ ( set2 @ TB @ B ) )
=> ( ( member @ TA @ H @ ( set2 @ TA @ D ) )
=> ( ( E @ G @ H )
= ( F @ G @ H ) ) ) )
=> ( ( list_all2 @ TB @ TA @ E @ A @ C )
= ( list_all2 @ TB @ TA @ F @ B @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(145,axiom,
! [TA: $tType,A: nat,B: nat > TA > $o] :
( ( ! [C: nat] :
( ( ord_less @ nat @ C @ A )
=> ? [D: TA] : ( B @ C @ D ) ) )
= ( ? [C: list @ TA] :
( ( ( size_size @ ( list @ TA ) @ C )
= A )
& ! [D: nat] :
( ( ord_less @ nat @ D @ A )
=> ( B @ D @ ( nth @ TA @ C @ D ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_Skolem__list__nth) ).
thf(756,plain,
! [TA: $tType,A: nat,B: nat > TA > $o] :
( ( ! [C: nat] :
( ( ord_less @ nat @ C @ A )
=> ? [D: TA] : ( B @ C @ D ) ) )
= ( ? [C: list @ TA] :
( ( ( size_size @ ( list @ TA ) @ C )
= A )
& ! [D: nat] :
( ( ord_less @ nat @ D @ A )
=> ( B @ D @ ( nth @ TA @ C @ D ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[145]) ).
thf(161,axiom,
~ ( vEBT_VEBT_minNull @ ( vEBT_vebt_delete @ ( nth @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) ) @ ( vEBT_VEBT_low @ xa @ na ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_False) ).
thf(789,plain,
~ ( vEBT_VEBT_minNull @ ( vEBT_vebt_delete @ ( nth @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) ) @ ( vEBT_VEBT_low @ xa @ na ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[161]) ).
thf(7,axiom,
! [A: list @ nat,B: nat] :
( ( sorted_wrt @ nat @ ( ord_less @ nat ) @ A )
=> ( ( ord_less @ nat @ B @ ( size_size @ ( list @ nat ) @ A ) )
=> ( ord_less_eq @ nat @ B @ ( nth @ nat @ A @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6828_sorted__wrt__less__idx) ).
thf(179,plain,
! [A: list @ nat,B: nat] :
( ( sorted_wrt @ nat @ ( ord_less @ nat ) @ A )
=> ( ( ord_less @ nat @ B @ ( size_size @ ( list @ nat ) @ A ) )
=> ( ord_less_eq @ nat @ B @ ( nth @ nat @ A @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(26,axiom,
! [TA: $tType,A: TA,B: list @ TA,C: TA > $o,D: list @ TA] :
( ( member @ TA @ A @ ( set2 @ TA @ B ) )
=> ( ~ ( C @ A )
=> ( ( takeWhile @ TA @ C @ ( append @ TA @ B @ D ) )
= ( takeWhile @ TA @ C @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6880_takeWhile__append1) ).
thf(253,plain,
! [TA: $tType,A: TA,B: list @ TA,C: TA > $o,D: list @ TA] :
( ( member @ TA @ A @ ( set2 @ TA @ B ) )
=> ( ~ ( C @ A )
=> ( ( takeWhile @ TA @ C @ ( append @ TA @ B @ D ) )
= ( takeWhile @ TA @ C @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(149,axiom,
( ( nth @ vEBT_VEBT @ ( list_update @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) @ ( vEBT_vebt_delete @ ( nth @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) ) @ ( vEBT_VEBT_low @ xa @ na ) ) ) @ ( vEBT_VEBT_high @ xa @ na ) )
= ( vEBT_vebt_delete @ ( nth @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) ) @ ( vEBT_VEBT_low @ xa @ na ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_hprolist) ).
thf(766,plain,
( ( nth @ vEBT_VEBT @ ( list_update @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) @ ( vEBT_vebt_delete @ ( nth @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) ) @ ( vEBT_VEBT_low @ xa @ na ) ) ) @ ( vEBT_VEBT_high @ xa @ na ) )
= ( vEBT_vebt_delete @ ( nth @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) ) @ ( vEBT_VEBT_low @ xa @ na ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[149]) ).
thf(55,axiom,
! [TA: $tType,TB: $tType,A: list @ TA,B: list @ TA,C: TA > TB,D: TA > TB] :
( ( A = B )
=> ( ! [E: TA] :
( ( member @ TA @ E @ ( set2 @ TA @ B ) )
=> ( ( C @ E )
= ( D @ E ) ) )
=> ( ( map @ TA @ TB @ C @ A )
= ( map @ TA @ TB @ D @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6192_list_Omap__cong) ).
thf(397,plain,
! [TA: $tType,TB: $tType,A: list @ TA,B: list @ TA,C: TA > TB,D: TA > TB] :
( ( A = B )
=> ( ! [E: TA] :
( ( member @ TA @ E @ ( set2 @ TA @ B ) )
=> ( ( C @ E )
= ( D @ E ) ) )
=> ( ( map @ TA @ TB @ C @ A )
= ( map @ TA @ TB @ D @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(138,axiom,
! [TA: $tType,TB: $tType,A: TB > TA > $o,B: list @ TB,C: list @ TA,D: nat] :
( ( list_all2 @ TB @ TA @ A @ B @ C )
=> ( ( ord_less @ nat @ D @ ( size_size @ ( list @ TB ) @ B ) )
=> ( A @ ( nth @ TB @ B @ D ) @ ( nth @ TA @ C @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7502_list__all2__nthD) ).
thf(734,plain,
! [TA: $tType,TB: $tType,A: TB > TA > $o,B: list @ TB,C: list @ TA,D: nat] :
( ( list_all2 @ TB @ TA @ A @ B @ C )
=> ( ( ord_less @ nat @ D @ ( size_size @ ( list @ TB ) @ B ) )
=> ( A @ ( nth @ TB @ B @ D ) @ ( nth @ TA @ C @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[138]) ).
thf(153,axiom,
xa != mi,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_xmi) ).
thf(774,plain,
xa != mi,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[153]) ).
thf(30,axiom,
! [TA: $tType,TB: $tType,TC: $tType,A: TB > TC,B: list @ TB,C: TA > TC,D: list @ TA] :
( ( ( map @ TB @ TC @ A @ B )
= ( map @ TA @ TC @ C @ D ) )
=> ( ( size_size @ ( list @ TB ) @ B )
= ( size_size @ ( list @ TA ) @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6191_map__eq__imp__length__eq) ).
thf(265,plain,
! [TA: $tType,TB: $tType,TC: $tType,A: TB > TC,B: list @ TB,C: TA > TC,D: list @ TA] :
( ( ( map @ TB @ TC @ A @ B )
= ( map @ TA @ TC @ C @ D ) )
=> ( ( size_size @ ( list @ TB ) @ B )
= ( size_size @ ( list @ TA ) @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(51,axiom,
( ( ord_less @ nat )
= ( ^ [A: nat,B: nat] :
( ( ord_less_eq @ nat @ A @ B )
& ( A != B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_nat__less__le) ).
thf(380,plain,
( ( ord_less @ nat )
= ( ^ [A: nat,B: nat] :
( ( ord_less_eq @ nat @ A @ B )
& ( A != B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(66,axiom,
! [TA: $tType,A: list @ TA,B: list @ TA,C: list @ TA] :
( ( ( append @ TA @ A @ B )
= ( append @ TA @ C @ B ) )
= ( A = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6379_append__same__eq) ).
thf(439,plain,
! [TA: $tType,A: list @ TA,B: list @ TA,C: list @ TA] :
( ( ( append @ TA @ A @ B )
= ( append @ TA @ C @ B ) )
= ( A = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(90,axiom,
! [TA: $tType,A: TA,B: list @ TA] :
( ( member @ TA @ A @ ( set2 @ TA @ B ) )
= ( ? [C: nat] :
( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ B ) )
& ( ( nth @ TA @ B @ C )
= A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_in__set__conv__nth) ).
thf(546,plain,
! [TA: $tType,A: TA,B: list @ TA] :
( ( member @ TA @ A @ ( set2 @ TA @ B ) )
= ( ? [C: nat] :
( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ B ) )
& ( ( nth @ TA @ B @ C )
= A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[90]) ).
thf(147,axiom,
! [A: nat] :
~ ( ord_less @ nat @ A @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_less__not__refl) ).
thf(761,plain,
! [A: nat] :
~ ( ord_less @ nat @ A @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[147]) ).
thf(88,axiom,
! [TA: $tType,A: nat,B: TA > $o,C: list @ TA] :
( ! [D: nat] :
( ( ord_less @ nat @ D @ A )
=> ( B @ ( nth @ TA @ C @ D ) ) )
=> ( ( ord_less_eq @ nat @ A @ ( size_size @ ( list @ TA ) @ C ) )
=> ( ord_less_eq @ nat @ A @ ( size_size @ ( list @ TA ) @ ( takeWhile @ TA @ B @ C ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6902_length__takeWhile__less__P__nth) ).
thf(534,plain,
! [TA: $tType,A: nat,B: TA > $o,C: list @ TA] :
( ! [D: nat] :
( ( ord_less @ nat @ D @ A )
=> ( B @ ( nth @ TA @ C @ D ) ) )
=> ( ( ord_less_eq @ nat @ A @ ( size_size @ ( list @ TA ) @ C ) )
=> ( ord_less_eq @ nat @ A @ ( size_size @ ( list @ TA ) @ ( takeWhile @ TA @ B @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).
thf(44,axiom,
! [A: nat,B: nat] :
( ( ord_less_eq @ nat @ A @ B )
=> ( ( A != B )
=> ( ord_less @ nat @ A @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_le__neq__implies__less) ).
thf(334,plain,
! [A: nat,B: nat] :
( ( ord_less_eq @ nat @ A @ B )
=> ( ( A != B )
=> ( ord_less @ nat @ A @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(155,axiom,
( ( some @ nat @ maxi )
= ( vEBT_vebt_maxt @ ( nth @ vEBT_VEBT @ ( list_update @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) @ ( vEBT_vebt_delete @ ( nth @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) ) @ ( vEBT_VEBT_low @ xa @ na ) ) ) @ ( vEBT_VEBT_high @ xa @ na ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_109_maxidef) ).
thf(778,plain,
( ( some @ nat @ maxi )
= ( vEBT_vebt_maxt @ ( nth @ vEBT_VEBT @ ( list_update @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) @ ( vEBT_vebt_delete @ ( nth @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) ) @ ( vEBT_VEBT_low @ xa @ na ) ) ) @ ( vEBT_VEBT_high @ xa @ na ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[155]) ).
thf(101,axiom,
! [A: nat > $o,B: nat] :
( ! [C: nat] :
( ! [D: nat] :
( ( ord_less @ nat @ D @ C )
=> ( A @ D ) )
=> ( A @ C ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_nat__less__induct) ).
thf(598,plain,
! [A: nat > $o,B: nat] :
( ! [C: nat] :
( ! [D: nat] :
( ( ord_less @ nat @ D @ C )
=> ( A @ D ) )
=> ( A @ C ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[101]) ).
thf(11,axiom,
! [TA: $tType,TB: $tType,A: TB > TA > $o,B: list @ TB,C: list @ TA,D: list @ TB,E: list @ TA] :
( ( list_all2 @ TB @ TA @ A @ B @ C )
=> ( ( list_all2 @ TB @ TA @ A @ D @ E )
=> ( list_all2 @ TB @ TA @ A @ ( append @ TB @ B @ D ) @ ( append @ TA @ C @ E ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7455_list__all2__appendI) ).
thf(192,plain,
! [TA: $tType,TB: $tType,A: TB > TA > $o,B: list @ TB,C: list @ TA,D: list @ TB,E: list @ TA] :
( ( list_all2 @ TB @ TA @ A @ B @ C )
=> ( ( list_all2 @ TB @ TA @ A @ D @ E )
=> ( list_all2 @ TB @ TA @ A @ ( append @ TB @ B @ D ) @ ( append @ TA @ C @ E ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(160,axiom,
ord_less @ nat @ ( vEBT_VEBT_high @ xa @ na ) @ ( size_size @ ( list @ vEBT_VEBT ) @ treeList ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8__092_060open_062high_Ax_An_A_060_Alength_AtreeList_092_060close_062) ).
thf(788,plain,
ord_less @ nat @ ( vEBT_VEBT_high @ xa @ na ) @ ( size_size @ ( list @ vEBT_VEBT ) @ treeList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[160]) ).
thf(13,axiom,
! [TA: $tType,TB: $tType,A: TB > TA > $o,B: list @ TB,C: list @ TA,D: TB > TA > $o] :
( ( list_all2 @ TB @ TA @ A @ B @ C )
=> ( ! [E: TB,F: TA] :
( ( member @ TB @ E @ ( set2 @ TB @ B ) )
=> ( ( member @ TA @ F @ ( set2 @ TA @ C ) )
=> ( ( A @ E @ F )
=> ( D @ E @ F ) ) ) )
=> ( list_all2 @ TB @ TA @ D @ B @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7498_list_Orel__mono__strong) ).
thf(197,plain,
! [TA: $tType,TB: $tType,A: TB > TA > $o,B: list @ TB,C: list @ TA,D: TB > TA > $o] :
( ( list_all2 @ TB @ TA @ A @ B @ C )
=> ( ! [E: TB,F: TA] :
( ( member @ TB @ E @ ( set2 @ TB @ B ) )
=> ( ( member @ TA @ F @ ( set2 @ TA @ C ) )
=> ( ( A @ E @ F )
=> ( D @ E @ F ) ) ) )
=> ( list_all2 @ TB @ TA @ D @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(118,axiom,
! [TA: $tType,A: nat,B: list @ TA,C: nat] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( set2 @ TA @ ( list_update @ TA @ ( list_update @ TA @ B @ A @ ( nth @ TA @ B @ C ) ) @ C @ ( nth @ TA @ B @ A ) ) )
= ( set2 @ TA @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_48_set__swap) ).
thf(665,plain,
! [TA: $tType,A: nat,B: list @ TA,C: nat] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( set2 @ TA @ ( list_update @ TA @ ( list_update @ TA @ B @ A @ ( nth @ TA @ B @ C ) ) @ C @ ( nth @ TA @ B @ A ) ) )
= ( set2 @ TA @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[118]) ).
thf(97,axiom,
! [TA: $tType,A: ( list @ TA ) > $o,B: list @ TA] :
( ! [C: list @ TA] :
( ! [D: list @ TA] :
( ( ord_less @ nat @ ( size_size @ ( list @ TA ) @ D ) @ ( size_size @ ( list @ TA ) @ C ) )
=> ( A @ D ) )
=> ( A @ C ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_length__induct) ).
thf(583,plain,
! [TA: $tType,A: ( list @ TA ) > $o,B: list @ TA] :
( ! [C: list @ TA] :
( ! [D: list @ TA] :
( ( ord_less @ nat @ ( size_size @ ( list @ TA ) @ D ) @ ( size_size @ ( list @ TA ) @ C ) )
=> ( A @ D ) )
=> ( A @ C ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[97]) ).
thf(124,axiom,
! [TA: $tType,A: nat,B: list @ TA,C: nat] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( distinct @ TA @ ( list_update @ TA @ ( list_update @ TA @ B @ A @ ( nth @ TA @ B @ C ) ) @ C @ ( nth @ TA @ B @ A ) ) )
= ( distinct @ TA @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3432_distinct__swap) ).
thf(682,plain,
! [TA: $tType,A: nat,B: list @ TA,C: nat] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( distinct @ TA @ ( list_update @ TA @ ( list_update @ TA @ B @ A @ ( nth @ TA @ B @ C ) ) @ C @ ( nth @ TA @ B @ A ) ) )
= ( distinct @ TA @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[124]) ).
thf(94,axiom,
! [A: nat,B: nat > $o,C: nat] :
( ! [D: nat] :
( ( ord_less @ nat @ A @ D )
=> ( B @ D ) )
=> ( ! [D: nat] :
( ( ord_less_eq @ nat @ D @ A )
=> ( ! [E: nat] :
( ( ord_less @ nat @ D @ E )
=> ( B @ E ) )
=> ( B @ D ) ) )
=> ( B @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_380_nat__descend__induct) ).
thf(566,plain,
! [A: nat,B: nat > $o,C: nat] :
( ! [D: nat] :
( ( ord_less @ nat @ A @ D )
=> ( B @ D ) )
=> ( ! [D: nat] :
( ( ord_less_eq @ nat @ D @ A )
=> ( ! [E: nat] :
( ( ord_less @ nat @ D @ E )
=> ( B @ E ) )
=> ( B @ D ) ) )
=> ( B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).
thf(77,axiom,
! [TA: $tType,A: TA,B: list @ TA,C: list @ TA] :
( ( ( member @ TA @ A @ ( set2 @ TA @ ( butlast @ TA @ B ) ) )
| ( member @ TA @ A @ ( set2 @ TA @ ( butlast @ TA @ C ) ) ) )
=> ( member @ TA @ A @ ( set2 @ TA @ ( butlast @ TA @ ( append @ TA @ B @ C ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7346_in__set__butlast__appendI) ).
thf(484,plain,
! [TA: $tType,A: TA,B: list @ TA,C: list @ TA] :
( ( ( member @ TA @ A @ ( set2 @ TA @ ( butlast @ TA @ B ) ) )
| ( member @ TA @ A @ ( set2 @ TA @ ( butlast @ TA @ C ) ) ) )
=> ( member @ TA @ A @ ( set2 @ TA @ ( butlast @ TA @ ( append @ TA @ B @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(141,axiom,
! [TA: $tType,TB: $tType,A: nat,B: list @ TA,C: TA > TB] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( nth @ TB @ ( map @ TA @ TB @ C @ B ) @ A )
= ( C @ ( nth @ TA @ B @ A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6172_nth__map) ).
thf(742,plain,
! [TA: $tType,TB: $tType,A: nat,B: list @ TA,C: TA > TB] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( nth @ TB @ ( map @ TA @ TB @ C @ B ) @ A )
= ( C @ ( nth @ TA @ B @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[141]) ).
thf(137,axiom,
! [A: nat > $o,B: nat] :
( ! [C: nat] :
( ~ ( A @ C )
=> ? [D: nat] :
( ( ord_less @ nat @ D @ C )
& ~ ( A @ D ) ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_infinite__descent) ).
thf(725,plain,
! [A: nat > $o,B: nat] :
( ! [C: nat] :
( ~ ( A @ C )
=> ? [D: nat] :
( ( ord_less @ nat @ D @ C )
& ~ ( A @ D ) ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[137]) ).
thf(4,axiom,
! [A: nat,B: nat] :
( ( ord_less_eq @ nat @ A @ B )
=> ( ( ord_less_eq @ nat @ B @ A )
=> ( A = B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_le__antisym) ).
thf(169,plain,
! [A: nat,B: nat] :
( ( ord_less_eq @ nat @ A @ B )
=> ( ( ord_less_eq @ nat @ B @ A )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(61,axiom,
! [TA: $tType,A: TA > TA > $o,B: list @ TA] :
( ( list_all2 @ TA @ TA @ A @ B @ B )
= ( ! [C: TA] :
( ( member @ TA @ C @ ( set2 @ TA @ B ) )
=> ( A @ C @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7496_list__all2__same) ).
thf(420,plain,
! [TA: $tType,A: TA > TA > $o,B: list @ TA] :
( ( list_all2 @ TA @ TA @ A @ B @ B )
= ( ! [C: TA] :
( ( member @ TA @ C @ ( set2 @ TA @ B ) )
=> ( A @ C @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(27,axiom,
( ( mi = ma )
=> ! [A: vEBT_VEBT] :
( ( member @ vEBT_VEBT @ A @ ( set2 @ vEBT_VEBT @ treeList ) )
=> ~ ? [B: nat] : ( vEBT_V8194947554948674370ptions @ A @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22__C4_Ohyps_C_I6_J) ).
thf(256,plain,
( ( mi = ma )
=> ! [A: vEBT_VEBT] :
( ( member @ vEBT_VEBT @ A @ ( set2 @ vEBT_VEBT @ treeList ) )
=> ~ ? [B: nat] : ( vEBT_V8194947554948674370ptions @ A @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(78,axiom,
! [TA: $tType,A: list @ TA,B: TA > TA > $o] :
( ! [C: TA] :
( ( member @ TA @ C @ ( set2 @ TA @ A ) )
=> ( B @ C @ C ) )
=> ( list_all2 @ TA @ TA @ B @ A @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7497_list_Orel__refl__strong) ).
thf(488,plain,
! [TA: $tType,A: list @ TA,B: TA > TA > $o] :
( ! [C: TA] :
( ( member @ TA @ C @ ( set2 @ TA @ A ) )
=> ( B @ C @ C ) )
=> ( list_all2 @ TA @ TA @ B @ A @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(18,axiom,
! [TA: $tType,A: nat,B: list @ TA,C: TA] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( member @ TA @ C @ ( set2 @ TA @ ( list_update @ TA @ B @ A @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_set__update__memI) ).
thf(225,plain,
! [TA: $tType,A: nat,B: list @ TA,C: TA] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( member @ TA @ C @ ( set2 @ TA @ ( list_update @ TA @ B @ A @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(46,axiom,
! [TA: $tType,A: list @ TA] :
( ( map @ TA @ TA
@ ^ [B: TA] : B
@ A )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6185_list_Omap__ident) ).
thf(339,plain,
! [TA: $tType,A: list @ TA] :
( ( map @ TA @ TA
@ ^ [B: TA] : B
@ A )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(74,axiom,
! [TA: $tType,TB: $tType,A: TB > TA > $o,B: list @ TB,C: list @ TA] :
( ( list_all2 @ TB @ TA @ A @ B @ C )
=> ( ( size_size @ ( list @ TB ) @ B )
= ( size_size @ ( list @ TA ) @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7500_list__all2__lengthD) ).
thf(476,plain,
! [TA: $tType,TB: $tType,A: TB > TA > $o,B: list @ TB,C: list @ TA] :
( ( list_all2 @ TB @ TA @ A @ B @ C )
=> ( ( size_size @ ( list @ TB ) @ B )
= ( size_size @ ( list @ TA ) @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(87,axiom,
! [TA: $tType,TB: $tType,A: list @ TA,B: list @ TA,C: TA > TB,D: TA > TB] :
( ( A = B )
=> ( ! [E: TA] :
( ( member @ TA @ E @ ( set2 @ TA @ B ) )
=> ( ( C @ E )
= ( D @ E ) ) )
=> ( ( map @ TA @ TB @ C @ A )
= ( map @ TA @ TB @ D @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6197_map__cong) ).
thf(526,plain,
! [TA: $tType,TB: $tType,A: list @ TA,B: list @ TA,C: TA > TB,D: TA > TB] :
( ( A = B )
=> ( ! [E: TA] :
( ( member @ TA @ E @ ( set2 @ TA @ B ) )
=> ( ( C @ E )
= ( D @ E ) ) )
=> ( ( map @ TA @ TB @ C @ A )
= ( map @ TA @ TB @ D @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).
thf(123,axiom,
! [TA: $tType,A: TA,B: TA > $o,C: list @ TA] :
( ( ( some @ TA @ A )
= ( find @ TA @ B @ C ) )
= ( ? [D: nat] :
( ( ord_less @ nat @ D @ ( size_size @ ( list @ TA ) @ C ) )
& ( B @ ( nth @ TA @ C @ D ) )
& ( A
= ( nth @ TA @ C @ D ) )
& ! [E: nat] :
( ( ord_less @ nat @ E @ D )
=> ~ ( B @ ( nth @ TA @ C @ E ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_538_find__Some__iff2) ).
thf(679,plain,
! [TA: $tType,A: TA,B: TA > $o,C: list @ TA] :
( ( ( some @ TA @ A )
= ( find @ TA @ B @ C ) )
= ( ? [D: nat] :
( ( ord_less @ nat @ D @ ( size_size @ ( list @ TA ) @ C ) )
& ( B @ ( nth @ TA @ C @ D ) )
& ( A
= ( nth @ TA @ C @ D ) )
& ! [E: nat] :
( ( ord_less @ nat @ E @ D )
=> ~ ( B @ ( nth @ TA @ C @ E ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[123]) ).
thf(131,axiom,
! [A: nat] :
~ ( ord_less @ nat @ A @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_less__irrefl__nat) ).
thf(706,plain,
! [A: nat] :
~ ( ord_less @ nat @ A @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[131]) ).
thf(105,axiom,
! [TA: $tType,A: list @ TA,B: list @ TA] :
( ( ( size_size @ ( list @ TA ) @ A )
= ( size_size @ ( list @ TA ) @ B ) )
=> ( ! [C: nat] :
( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ A ) )
=> ( ( nth @ TA @ A @ C )
= ( nth @ TA @ B @ C ) ) )
=> ( A = B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_105_nth__equalityI) ).
thf(622,plain,
! [TA: $tType,A: list @ TA,B: list @ TA] :
( ( ( size_size @ ( list @ TA ) @ A )
= ( size_size @ ( list @ TA ) @ B ) )
=> ( ! [C: nat] :
( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ A ) )
=> ( ( nth @ TA @ A @ C )
= ( nth @ TA @ B @ C ) ) )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[105]) ).
thf(85,axiom,
! [TA: $tType,TB: $tType,TC: $tType,A: TB > TA > $o,B: TC > TB,C: list @ TC,D: list @ TA] :
( ( list_all2 @ TB @ TA @ A @ ( map @ TC @ TB @ B @ C ) @ D )
= ( list_all2 @ TC @ TA
@ ^ [E: TC] : ( A @ ( B @ E ) )
@ C
@ D ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7453_list__all2__map1) ).
thf(515,plain,
! [TA: $tType,TB: $tType,TC: $tType,A: TB > TA > $o,B: TC > TB,C: list @ TC,D: list @ TA] :
( ( list_all2 @ TB @ TA @ A @ ( map @ TC @ TB @ B @ C ) @ D )
= ( list_all2 @ TC @ TA
@ ^ [E: TC] : ( A @ ( B @ E ) )
@ C
@ D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(82,axiom,
! [TA: $tType,A: list @ TA] :
( ( distinct @ TA @ A )
=> ( distinct @ TA @ ( butlast @ TA @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7348_distinct__butlast) ).
thf(508,plain,
! [TA: $tType,A: list @ TA] :
( ( distinct @ TA @ A )
=> ( distinct @ TA @ ( butlast @ TA @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(115,axiom,
! [A: vEBT_VEBT] :
( ~ ( vEBT_VEBT_minNull @ A )
=> ? [B: nat] : ( vEBT_V8194947554948674370ptions @ A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_not__min__Null__member) ).
thf(657,plain,
! [A: vEBT_VEBT] :
( ~ ( vEBT_VEBT_minNull @ A )
=> ? [B: nat] : ( vEBT_V8194947554948674370ptions @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[115]) ).
thf(121,axiom,
! [TA: $tType] : ( size @ ( list @ TA ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_List_Olist___Nat_Osize_244) ).
thf(674,plain,
! [TA: $tType] : ( size @ ( list @ TA ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[121]) ).
thf(117,axiom,
! [A: vEBT_VEBT,B: nat] :
( ( ( vEBT_vebt_maxt @ A )
= ( some @ nat @ B ) )
=> ( vEBT_V8194947554948674370ptions @ A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_120_maxbmo) ).
thf(662,plain,
! [A: vEBT_VEBT,B: nat] :
( ( ( vEBT_vebt_maxt @ A )
= ( some @ nat @ B ) )
=> ( vEBT_V8194947554948674370ptions @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[117]) ).
thf(58,axiom,
! [TA: $tType,A: list @ TA,B: list @ TA,C: list @ TA] :
( ( append @ TA @ ( append @ TA @ A @ B ) @ C )
= ( append @ TA @ A @ ( append @ TA @ B @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6378_append__assoc) ).
thf(412,plain,
! [TA: $tType,A: list @ TA,B: list @ TA,C: list @ TA] :
( ( append @ TA @ ( append @ TA @ A @ B ) @ C )
= ( append @ TA @ A @ ( append @ TA @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(84,axiom,
( ( ord_less_eq @ nat )
= ( ^ [A: nat,B: nat] :
( ( ord_less @ nat @ A @ B )
| ( A = B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_le__eq__less__or__eq) ).
thf(513,plain,
( ( ord_less_eq @ nat )
= ( ^ [A: nat,B: nat] :
( ( ord_less @ nat @ A @ B )
| ( A = B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(142,axiom,
! [TA: $tType,A: nat,B: list @ TA,C: TA] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( nth @ TA @ ( list_update @ TA @ B @ A @ C ) @ A )
= C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_nth__list__update__eq) ).
thf(745,plain,
! [TA: $tType,A: nat,B: list @ TA,C: TA] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( nth @ TA @ ( list_update @ TA @ B @ A @ C ) @ A )
= C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[142]) ).
thf(39,axiom,
! [TA: $tType,TB: $tType,TC: $tType,A: TB > TC > $o,B: TC > TA > $o,C: TB > TA > $o,D: list @ TB,E: list @ TC,F: list @ TA] :
( ! [G: TB,H: TC,I: TA] :
( ( A @ G @ H )
=> ( ( B @ H @ I )
=> ( C @ G @ I ) ) )
=> ( ( list_all2 @ TB @ TC @ A @ D @ E )
=> ( ( list_all2 @ TC @ TA @ B @ E @ F )
=> ( list_all2 @ TB @ TA @ C @ D @ F ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7467_list__all2__trans) ).
thf(296,plain,
! [TA: $tType,TB: $tType,TC: $tType,A: TB > TC > $o,B: TC > TA > $o,C: TB > TA > $o,D: list @ TB,E: list @ TC,F: list @ TA] :
( ! [G: TB,H: TC,I: TA] :
( ( A @ G @ H )
=> ( ( B @ H @ I )
=> ( C @ G @ I ) ) )
=> ( ( list_all2 @ TB @ TC @ A @ D @ E )
=> ( ( list_all2 @ TC @ TA @ B @ E @ F )
=> ( list_all2 @ TB @ TA @ C @ D @ F ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(62,axiom,
! [TA: $tType] :
( ( list_all2 @ TA @ TA @ ( (=) @ TA ) )
= ( (=) @ ( list @ TA ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7462_list_Orel__eq) ).
thf(423,plain,
! [TA: $tType] :
( ( list_all2 @ TA @ TA @ ( (=) @ TA ) )
= ( (=) @ ( list @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(152,axiom,
xa = ma,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_True) ).
thf(772,plain,
xa = ma,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[152]) ).
thf(36,axiom,
! [TA: $tType,A: TA > $o,B: list @ TA] : ( ord_less_eq @ nat @ ( size_size @ ( list @ TA ) @ ( takeWhile @ TA @ A @ B ) ) @ ( size_size @ ( list @ TA ) @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6893_length__takeWhile__le) ).
thf(286,plain,
! [TA: $tType,A: TA > $o,B: list @ TA] : ( ord_less_eq @ nat @ ( size_size @ ( list @ TA ) @ ( takeWhile @ TA @ A @ B ) ) @ ( size_size @ ( list @ TA ) @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(133,axiom,
! [TA: $tType,A: TA > $o,B: TA > nat,C: TA] :
( ! [D: TA] :
( ~ ( A @ D )
=> ? [E: TA] :
( ( ord_less @ nat @ ( B @ E ) @ ( B @ D ) )
& ~ ( A @ E ) ) )
=> ( A @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_infinite__descent__measure) ).
thf(711,plain,
! [TA: $tType,A: TA > $o,B: TA > nat,C: TA] :
( ! [D: TA] :
( ~ ( A @ D )
=> ? [E: TA] :
( ( ord_less @ nat @ ( B @ E ) @ ( B @ D ) )
& ~ ( A @ E ) ) )
=> ( A @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[133]) ).
thf(95,axiom,
! [TA: $tType,A: nat,B: list @ TA] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ ( butlast @ TA @ B ) ) )
=> ( ( nth @ TA @ ( butlast @ TA @ B ) @ A )
= ( nth @ TA @ B @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7356_nth__butlast) ).
thf(579,plain,
! [TA: $tType,A: nat,B: list @ TA] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ ( butlast @ TA @ B ) ) )
=> ( ( nth @ TA @ ( butlast @ TA @ B ) @ A )
= ( nth @ TA @ B @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(28,axiom,
! [TA: $tType,A: list @ TA,B: list @ TA,C: list @ TA,D: list @ TA] :
( ( ( append @ TA @ A @ B )
= ( append @ TA @ C @ D ) )
= ( ? [E: list @ TA] :
( ( ( A
= ( append @ TA @ C @ E ) )
& ( ( append @ TA @ E @ B )
= D ) )
| ( ( ( append @ TA @ A @ E )
= C )
& ( B
= ( append @ TA @ E @ D ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6445_append__eq__append__conv2) ).
thf(259,plain,
! [TA: $tType,A: list @ TA,B: list @ TA,C: list @ TA,D: list @ TA] :
( ( ( append @ TA @ A @ B )
= ( append @ TA @ C @ D ) )
= ( ? [E: list @ TA] :
( ( ( A
= ( append @ TA @ C @ E ) )
& ( ( append @ TA @ E @ B )
= D ) )
| ( ( ( append @ TA @ A @ E )
= C )
& ( B
= ( append @ TA @ E @ D ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(111,axiom,
! [TA: $tType,A: nat,B: list @ TA,C: nat,D: TA] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( ( A = C )
=> ( ( nth @ TA @ ( list_update @ TA @ B @ A @ D ) @ C )
= D ) )
& ( ( A != C )
=> ( ( nth @ TA @ ( list_update @ TA @ B @ A @ D ) @ C )
= ( nth @ TA @ B @ C ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_nth__list__update) ).
thf(641,plain,
! [TA: $tType,A: nat,B: list @ TA,C: nat,D: TA] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( ( A = C )
=> ( ( nth @ TA @ ( list_update @ TA @ B @ A @ D ) @ C )
= D ) )
& ( ( A != C )
=> ( ( nth @ TA @ ( list_update @ TA @ B @ A @ D ) @ C )
= ( nth @ TA @ B @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[111]) ).
thf(52,axiom,
! [TA: $tType,TB: $tType,A: TA > TB,B: list @ TA,C: list @ TA] :
( ( map @ TA @ TB @ A @ ( append @ TA @ B @ C ) )
= ( append @ TB @ ( map @ TA @ TB @ A @ B ) @ ( map @ TA @ TB @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6390_map__append) ).
thf(382,plain,
! [TA: $tType,TB: $tType,A: TA > TB,B: list @ TA,C: list @ TA] :
( ( map @ TA @ TB @ A @ ( append @ TA @ B @ C ) )
= ( append @ TB @ ( map @ TA @ TB @ A @ B ) @ ( map @ TA @ TB @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(21,axiom,
! [TA: $tType,A: TA > TA > $o,B: list @ TA,C: list @ TA] :
( ( sorted_wrt @ TA @ A @ ( append @ TA @ B @ C ) )
= ( ( sorted_wrt @ TA @ A @ B )
& ( sorted_wrt @ TA @ A @ C )
& ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ B ) )
=> ! [E: TA] :
( ( member @ TA @ E @ ( set2 @ TA @ C ) )
=> ( A @ D @ E ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6799_sorted__wrt__append) ).
thf(236,plain,
! [TA: $tType,A: TA > TA > $o,B: list @ TA,C: list @ TA] :
( ( sorted_wrt @ TA @ A @ ( append @ TA @ B @ C ) )
= ( ( sorted_wrt @ TA @ A @ B )
& ( sorted_wrt @ TA @ A @ C )
& ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ B ) )
=> ! [E: TA] :
( ( member @ TA @ E @ ( set2 @ TA @ C ) )
=> ( A @ D @ E ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(49,axiom,
! [A: nat > $o,B: nat,C: nat] :
( ( A @ B )
=> ( ! [D: nat] :
( ( A @ D )
=> ( ord_less_eq @ nat @ D @ C ) )
=> ~ ! [D: nat] :
( ( A @ D )
=> ~ ! [E: nat] :
( ( A @ E )
=> ( ord_less_eq @ nat @ E @ D ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_370_bounded__Max__nat) ).
thf(350,plain,
! [A: nat > $o,B: nat,C: nat] :
( ( A @ B )
=> ( ! [D: nat] :
( ( A @ D )
=> ( ord_less_eq @ nat @ D @ C ) )
=> ~ ! [D: nat] :
( ( A @ D )
=> ~ ! [E: nat] :
( ( A @ E )
=> ( ord_less_eq @ nat @ E @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(148,axiom,
( ( size_size @ ( list @ vEBT_VEBT ) @ treeList )
= ( size_size @ ( list @ vEBT_VEBT ) @ ( list_update @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) @ ( vEBT_vebt_delete @ ( nth @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) ) @ ( vEBT_VEBT_low @ xa @ na ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20__092_060open_062length_AtreeList_A_061_Alength_A_ItreeList_091high_Ax_An_A_058_061_Avebt__delete_A_ItreeList_A_B_Ahigh_Ax_An_J_A_Ilow_Ax_An_J_093_J_092_060close_062) ).
thf(764,plain,
( ( size_size @ ( list @ vEBT_VEBT ) @ treeList )
= ( size_size @ ( list @ vEBT_VEBT ) @ ( list_update @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) @ ( vEBT_vebt_delete @ ( nth @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) ) @ ( vEBT_VEBT_low @ xa @ na ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[148]) ).
thf(5,axiom,
! [TA: $tType,TB: $tType,A: TA > TB,B: list @ TA] :
( ( size_size @ ( list @ TB ) @ ( map @ TA @ TB @ A @ B ) )
= ( size_size @ ( list @ TA ) @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6163_length__map) ).
thf(172,plain,
! [TA: $tType,TB: $tType,A: TA > TB,B: list @ TA] :
( ( size_size @ ( list @ TB ) @ ( map @ TA @ TB @ A @ B ) )
= ( size_size @ ( list @ TA ) @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(16,axiom,
! [TA: $tType,TB: $tType,A: list @ TA,B: TB > TA] :
( ( ? [C: list @ TB] :
( A
= ( map @ TB @ TA @ B @ C ) ) )
= ( ! [C: TA] :
( ( member @ TA @ C @ ( set2 @ TA @ A ) )
=> ? [D: TB] :
( C
= ( B @ D ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6198_ex__map__conv) ).
thf(219,plain,
! [TA: $tType,TB: $tType,A: list @ TA,B: TB > TA] :
( ( ? [C: list @ TB] :
( A
= ( map @ TB @ TA @ B @ C ) ) )
= ( ! [C: TA] :
( ( member @ TA @ C @ ( set2 @ TA @ A ) )
=> ? [D: TB] :
( C
= ( B @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(33,axiom,
! [TA: $tType,TB: $tType,TC: $tType,A: TB > TA > $o,B: TC > TB,C: list @ TC,D: list @ TA] :
( ( list_all2 @ TB @ TA @ A @ ( map @ TC @ TB @ B @ C ) @ D )
= ( list_all2 @ TC @ TA
@ ^ [E: TC] : ( A @ ( B @ E ) )
@ C
@ D ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7452_list_Orel__map_I1_J) ).
thf(274,plain,
! [TA: $tType,TB: $tType,TC: $tType,A: TB > TA > $o,B: TC > TB,C: list @ TC,D: list @ TA] :
( ( list_all2 @ TB @ TA @ A @ ( map @ TC @ TB @ B @ C ) @ D )
= ( list_all2 @ TC @ TA
@ ^ [E: TC] : ( A @ ( B @ E ) )
@ C
@ D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(158,axiom,
? [A: nat] : ( vEBT_V8194947554948674370ptions @ ( vEBT_vebt_delete @ ( nth @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) ) @ ( vEBT_VEBT_low @ xa @ na ) ) @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_notemp) ).
thf(784,plain,
? [A: nat] : ( vEBT_V8194947554948674370ptions @ ( vEBT_vebt_delete @ ( nth @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) ) @ ( vEBT_VEBT_low @ xa @ na ) ) @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[158]) ).
thf(139,axiom,
! [TA: $tType,A: nat] :
? [B: list @ TA] :
( ( size_size @ ( list @ TA ) @ B )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_Ex__list__of__length) ).
thf(736,plain,
! [TA: $tType,A: nat] :
? [B: list @ TA] :
( ( size_size @ ( list @ TA ) @ B )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[139]) ).
thf(24,axiom,
! [TA: $tType,A: list @ TA,B: list @ TA,C: list @ TA,D: list @ TA] :
( ( ( ( size_size @ ( list @ TA ) @ A )
= ( size_size @ ( list @ TA ) @ B ) )
| ( ( size_size @ ( list @ TA ) @ C )
= ( size_size @ ( list @ TA ) @ D ) ) )
=> ( ( ( append @ TA @ A @ C )
= ( append @ TA @ B @ D ) )
= ( ( A = B )
& ( C = D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6389_append__eq__append__conv) ).
thf(245,plain,
! [TA: $tType,A: list @ TA,B: list @ TA,C: list @ TA,D: list @ TA] :
( ( ( ( size_size @ ( list @ TA ) @ A )
= ( size_size @ ( list @ TA ) @ B ) )
| ( ( size_size @ ( list @ TA ) @ C )
= ( size_size @ ( list @ TA ) @ D ) ) )
=> ( ( ( append @ TA @ A @ C )
= ( append @ TA @ B @ D ) )
= ( ( A = B )
& ( C = D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(64,axiom,
! [A: nat,B: nat] :
( ( ord_less_eq @ nat @ A @ B )
| ( ord_less_eq @ nat @ B @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_nat__le__linear) ).
thf(434,plain,
! [A: nat,B: nat] :
( ( ord_less_eq @ nat @ A @ B )
| ( ord_less_eq @ nat @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(32,axiom,
! [TA: $tType,A: list @ TA,B: TA > $o] :
( ( ! [C: TA] :
( ( member @ TA @ C @ ( set2 @ TA @ A ) )
=> ( B @ C ) ) )
= ( ! [C: nat] :
( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ A ) )
=> ( B @ ( nth @ TA @ A @ C ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_all__set__conv__all__nth) ).
thf(271,plain,
! [TA: $tType,A: list @ TA,B: TA > $o] :
( ( ! [C: TA] :
( ( member @ TA @ C @ ( set2 @ TA @ A ) )
=> ( B @ C ) ) )
= ( ! [C: nat] :
( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ A ) )
=> ( B @ ( nth @ TA @ A @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(48,axiom,
! [A: nat > nat,B: nat,C: nat] :
( ! [D: nat,E: nat] :
( ( ord_less @ nat @ D @ E )
=> ( ord_less @ nat @ ( A @ D ) @ ( A @ E ) ) )
=> ( ( ord_less_eq @ nat @ B @ C )
=> ( ord_less_eq @ nat @ ( A @ B ) @ ( A @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_less__mono__imp__le__mono) ).
thf(345,plain,
! [A: nat > nat,B: nat,C: nat] :
( ! [D: nat,E: nat] :
( ( ord_less @ nat @ D @ E )
=> ( ord_less @ nat @ ( A @ D ) @ ( A @ E ) ) )
=> ( ( ord_less_eq @ nat @ B @ C )
=> ( ord_less_eq @ nat @ ( A @ B ) @ ( A @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(129,axiom,
! [TA: $tType,A: nat,B: list @ TA,C: list @ TA,D: TA] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( list_update @ TA @ ( append @ TA @ B @ C ) @ A @ D )
= ( append @ TA @ ( list_update @ TA @ B @ A @ D ) @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6454_list__update__append1) ).
thf(700,plain,
! [TA: $tType,A: nat,B: list @ TA,C: list @ TA,D: TA] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( list_update @ TA @ ( append @ TA @ B @ C ) @ A @ D )
= ( append @ TA @ ( list_update @ TA @ B @ A @ D ) @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[129]) ).
thf(25,axiom,
! [A: nat] : ( ord_less_eq @ nat @ A @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_le__refl) ).
thf(251,plain,
! [A: nat] : ( ord_less_eq @ nat @ A @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(119,axiom,
! [TA: $tType] :
( ( distinct @ TA )
= ( ^ [A: list @ TA] :
! [B: nat] :
( ( ord_less @ nat @ B @ ( size_size @ ( list @ TA ) @ A ) )
=> ! [C: nat] :
( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ A ) )
=> ( ( B != C )
=> ( ( nth @ TA @ A @ B )
!= ( nth @ TA @ A @ C ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3453_distinct__conv__nth) ).
thf(668,plain,
! [TA: $tType] :
( ( distinct @ TA )
= ( ^ [A: list @ TA] :
! [B: nat] :
( ( ord_less @ nat @ B @ ( size_size @ ( list @ TA ) @ A ) )
=> ! [C: nat] :
( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ A ) )
=> ( ( B != C )
=> ( ( nth @ TA @ A @ B )
!= ( nth @ TA @ A @ C ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[119]) ).
thf(43,axiom,
! [A: vEBT_VEBT,B: nat,C: nat,D: nat] :
( ( vEBT_invar_vebt @ A @ B )
=> ( ( ( vEBT_vebt_maxt @ A )
= ( some @ nat @ C ) )
=> ( ( vEBT_vebt_member @ A @ D )
=> ( ord_less_eq @ nat @ D @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_125_maxt__corr__help) ).
thf(330,plain,
! [A: vEBT_VEBT,B: nat,C: nat,D: nat] :
( ( vEBT_invar_vebt @ A @ B )
=> ( ( ( vEBT_vebt_maxt @ A )
= ( some @ nat @ C ) )
=> ( ( vEBT_vebt_member @ A @ D )
=> ( ord_less_eq @ nat @ D @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(71,axiom,
! [TA: $tType,A: list @ TA,B: list @ TA,C: list @ TA] :
( ( ( append @ TA @ A @ B )
= ( append @ TA @ A @ C ) )
= ( B = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6380_same__append__eq) ).
thf(462,plain,
! [TA: $tType,A: list @ TA,B: list @ TA,C: list @ TA] :
( ( ( append @ TA @ A @ B )
= ( append @ TA @ A @ C ) )
= ( B = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(125,axiom,
! [TA: $tType,A: nat,B: list @ TA,C: TA] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( ( list_update @ TA @ B @ A @ C )
= B )
= ( ( nth @ TA @ B @ A )
= C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_list__update__same__conv) ).
thf(685,plain,
! [TA: $tType,A: nat,B: list @ TA,C: TA] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ( ( list_update @ TA @ B @ A @ C )
= B )
= ( ( nth @ TA @ B @ A )
= C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[125]) ).
thf(150,axiom,
! [A: vEBT_VEBT,B: nat] :
( ( vEBT_invar_vebt @ A @ B )
=> ( vEBT_VEBT_valid @ A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_valid__eq1) ).
thf(768,plain,
! [A: vEBT_VEBT,B: nat] :
( ( vEBT_invar_vebt @ A @ B )
=> ( vEBT_VEBT_valid @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[150]) ).
thf(128,axiom,
~ ! [A: nat] :
( ( some @ nat @ A )
!= ( vEBT_vebt_maxt @ ( nth @ vEBT_VEBT @ ( list_update @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) @ ( vEBT_vebt_delete @ ( nth @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) ) @ ( vEBT_VEBT_low @ xa @ na ) ) ) @ ( vEBT_VEBT_high @ xa @ na ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062maxi_O_ASome_Amaxi_A_061_Avebt__maxt_A_ItreeList_091high_Ax_An_A_058_061_Avebt__delete_A_ItreeList_A_B_Ahigh_Ax_An_J_A_Ilow_Ax_An_J_093_A_B_Ahigh_Ax_An_J_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062) ).
thf(695,plain,
~ ! [A: nat] :
( ( some @ nat @ A )
!= ( vEBT_vebt_maxt @ ( nth @ vEBT_VEBT @ ( list_update @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) @ ( vEBT_vebt_delete @ ( nth @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) ) @ ( vEBT_VEBT_low @ xa @ na ) ) ) @ ( vEBT_VEBT_high @ xa @ na ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[128]) ).
thf(156,axiom,
vEBT_VEBT_valid = vEBT_invar_vebt,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_valid__eq) ).
thf(780,plain,
vEBT_VEBT_valid = vEBT_invar_vebt,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[156]) ).
thf(93,axiom,
! [A: vEBT_VEBT,B: nat] :
( ( vEBT_VEBT_minNull @ A )
=> ~ ( vEBT_vebt_member @ A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_min__Null__member) ).
thf(563,plain,
! [A: vEBT_VEBT,B: nat] :
( ( vEBT_VEBT_minNull @ A )
=> ~ ( vEBT_vebt_member @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).
thf(63,axiom,
! [TA: $tType,A: TA > TA > $o,B: TA > TA > $o,C: list @ TA,D: list @ TA] :
( ! [E: TA,F: TA] :
( ( A @ E @ F )
=> ( ( B @ F @ E )
=> ( E = F ) ) )
=> ( ( list_all2 @ TA @ TA @ A @ C @ D )
=> ( ( list_all2 @ TA @ TA @ B @ D @ C )
=> ( C = D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7468_list__all2__antisym) ).
thf(426,plain,
! [TA: $tType,A: TA > TA > $o,B: TA > TA > $o,C: list @ TA,D: list @ TA] :
( ! [E: TA,F: TA] :
( ( A @ E @ F )
=> ( ( B @ F @ E )
=> ( E = F ) ) )
=> ( ( list_all2 @ TA @ TA @ A @ C @ D )
=> ( ( list_all2 @ TA @ TA @ B @ D @ C )
=> ( C = D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(98,axiom,
! [TA: $tType] :
( ( (=) @ ( list @ TA ) )
= ( ^ [A: list @ TA,B: list @ TA] :
( ( ( size_size @ ( list @ TA ) @ A )
= ( size_size @ ( list @ TA ) @ B ) )
& ! [C: nat] :
( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ A ) )
=> ( ( nth @ TA @ A @ C )
= ( nth @ TA @ B @ C ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_list__eq__iff__nth__eq) ).
thf(589,plain,
! [TA: $tType] :
( ( (=) @ ( list @ TA ) )
= ( ^ [A: list @ TA,B: list @ TA] :
( ( ( size_size @ ( list @ TA ) @ A )
= ( size_size @ ( list @ TA ) @ B ) )
& ! [C: nat] :
( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ A ) )
=> ( ( nth @ TA @ A @ C )
= ( nth @ TA @ B @ C ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[98]) ).
thf(1,conjecture,
vEBT_invar_vebt @ ( nth @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) ) @ na,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
thf(2,negated_conjecture,
~ ( vEBT_invar_vebt @ ( nth @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) ) @ na ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(162,plain,
~ ( vEBT_invar_vebt @ ( nth @ vEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ xa @ na ) ) @ na ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(104,axiom,
! [A: vEBT_VEBT] :
( ( member @ vEBT_VEBT @ A @ ( set2 @ vEBT_VEBT @ treeList ) )
=> ( ( vEBT_invar_vebt @ A @ na )
& ! [B: nat,C: nat] :
( ( vEBT_V8194947554948674370ptions @ ( vEBT_vebt_delete @ A @ B ) @ C )
= ( ( B != C )
& ( vEBT_V8194947554948674370ptions @ A @ C ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23__C4_OIH_C_I1_J) ).
thf(617,plain,
! [A: vEBT_VEBT] :
( ( member @ vEBT_VEBT @ A @ ( set2 @ vEBT_VEBT @ treeList ) )
=> ( ( vEBT_invar_vebt @ A @ na )
& ! [B: nat,C: nat] :
( ( vEBT_V8194947554948674370ptions @ ( vEBT_vebt_delete @ A @ B ) @ C )
= ( ( B != C )
& ( vEBT_V8194947554948674370ptions @ A @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[104]) ).
thf(47,axiom,
! [TA: $tType,TB: $tType,TC: $tType,A: TC > TB > $o,B: list @ TC,C: TA > TB,D: list @ TA] :
( ( list_all2 @ TC @ TB @ A @ B @ ( map @ TA @ TB @ C @ D ) )
= ( list_all2 @ TC @ TA
@ ^ [E: TC,F: TA] : ( A @ E @ ( C @ F ) )
@ B
@ D ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7454_list__all2__map2) ).
thf(342,plain,
! [TA: $tType,TB: $tType,TC: $tType,A: TC > TB > $o,B: list @ TC,C: TA > TB,D: list @ TA] :
( ( list_all2 @ TC @ TB @ A @ B @ ( map @ TA @ TB @ C @ D ) )
= ( list_all2 @ TC @ TA
@ ^ [E: TC,F: TA] : ( A @ E @ ( C @ F ) )
@ B
@ D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(12,axiom,
! [TA: $tType] :
( ( (=) @ ( list @ TA ) )
= ( list_all2 @ TA @ TA @ ( (=) @ TA ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7464_list__all2__eq) ).
thf(194,plain,
! [TA: $tType] :
( ( (=) @ ( list @ TA ) )
= ( list_all2 @ TA @ TA @ ( (=) @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(112,axiom,
! [A: nat,B: nat] :
( ( A != B )
=> ( ~ ( ord_less @ nat @ A @ B )
=> ( ord_less @ nat @ B @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_linorder__neqE__nat) ).
thf(648,plain,
! [A: nat,B: nat] :
( ( A != B )
=> ( ~ ( ord_less @ nat @ A @ B )
=> ( ord_less @ nat @ B @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[112]) ).
thf(15,axiom,
! [TA: $tType,TB: $tType,A: list @ TA,B: list @ TA,C: TA > TB,D: TA > TB] :
( ! [E: TA,F: TA] :
( ( member @ TA @ E @ ( set2 @ TA @ A ) )
=> ( ( member @ TA @ F @ ( set2 @ TA @ B ) )
=> ( ( ( C @ E )
= ( D @ F ) )
=> ( E = F ) ) ) )
=> ( ( ( map @ TA @ TB @ C @ A )
= ( map @ TA @ TB @ D @ B ) )
=> ( A = B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6194_list_Oinj__map__strong) ).
thf(209,plain,
! [TA: $tType,TB: $tType,A: list @ TA,B: list @ TA,C: TA > TB,D: TA > TB] :
( ! [E: TA,F: TA] :
( ( member @ TA @ E @ ( set2 @ TA @ A ) )
=> ( ( member @ TA @ F @ ( set2 @ TA @ B ) )
=> ( ( ( C @ E )
= ( D @ F ) )
=> ( E = F ) ) ) )
=> ( ( ( map @ TA @ TB @ C @ A )
= ( map @ TA @ TB @ D @ B ) )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(42,axiom,
! [TA: $tType,TB: $tType,A: list @ TB,B: list @ TA,C: TB > TA > $o,D: list @ TB,E: list @ TA] :
( ( ( size_size @ ( list @ TB ) @ A )
= ( size_size @ ( list @ TA ) @ B ) )
=> ( ( list_all2 @ TB @ TA @ C @ ( append @ TB @ A @ D ) @ ( append @ TA @ B @ E ) )
= ( ( list_all2 @ TB @ TA @ C @ A @ B )
& ( list_all2 @ TB @ TA @ C @ D @ E ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7493_list__all2__append) ).
thf(327,plain,
! [TA: $tType,TB: $tType,A: list @ TB,B: list @ TA,C: TB > TA > $o,D: list @ TB,E: list @ TA] :
( ( ( size_size @ ( list @ TB ) @ A )
= ( size_size @ ( list @ TA ) @ B ) )
=> ( ( list_all2 @ TB @ TA @ C @ ( append @ TB @ A @ D ) @ ( append @ TA @ B @ E ) )
= ( ( list_all2 @ TB @ TA @ C @ A @ B )
& ( list_all2 @ TB @ TA @ C @ D @ E ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(140,axiom,
! [TA: $tType,A: list @ TA,B: nat,C: TA] :
( ( ord_less_eq @ nat @ ( size_size @ ( list @ TA ) @ A ) @ B )
=> ( ( list_update @ TA @ A @ B @ C )
= A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_list__update__beyond) ).
thf(739,plain,
! [TA: $tType,A: list @ TA,B: nat,C: TA] :
( ( ord_less_eq @ nat @ ( size_size @ ( list @ TA ) @ A ) @ B )
=> ( ( list_update @ TA @ A @ B @ C )
= A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[140]) ).
thf(57,axiom,
! [TA: $tType,TB: $tType,A: TB > TB > $o,B: TA > TB,C: list @ TA] :
( ( sorted_wrt @ TB @ A @ ( map @ TA @ TB @ B @ C ) )
= ( sorted_wrt @ TA
@ ^ [D: TA,E: TA] : ( A @ ( B @ D ) @ ( B @ E ) )
@ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6771_sorted__wrt__map) ).
thf(409,plain,
! [TA: $tType,TB: $tType,A: TB > TB > $o,B: TA > TB,C: list @ TA] :
( ( sorted_wrt @ TB @ A @ ( map @ TA @ TB @ B @ C ) )
= ( sorted_wrt @ TA
@ ^ [D: TA,E: TA] : ( A @ ( B @ D ) @ ( B @ E ) )
@ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(8,axiom,
! [TA: $tType,A: list @ TA,B: list @ TA,C: list @ TA,D: list @ TA,E: list @ TA] :
( ( ( append @ TA @ A @ B )
= C )
=> ( ( D
= ( append @ TA @ B @ E ) )
=> ( ( append @ TA @ A @ D )
= ( append @ TA @ C @ E ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6444_append__eq__appendI) ).
thf(182,plain,
! [TA: $tType,A: list @ TA,B: list @ TA,C: list @ TA,D: list @ TA,E: list @ TA] :
( ( ( append @ TA @ A @ B )
= C )
=> ( ( D
= ( append @ TA @ B @ E ) )
=> ( ( append @ TA @ A @ D )
= ( append @ TA @ C @ E ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(134,axiom,
! [TA: $tType,A: TA > $o,B: list @ TA,C: TA] :
( ( ( find @ TA @ A @ B )
= ( some @ TA @ C ) )
= ( ? [D: nat] :
( ( ord_less @ nat @ D @ ( size_size @ ( list @ TA ) @ B ) )
& ( A @ ( nth @ TA @ B @ D ) )
& ( C
= ( nth @ TA @ B @ D ) )
& ! [E: nat] :
( ( ord_less @ nat @ E @ D )
=> ~ ( A @ ( nth @ TA @ B @ E ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_539_find__Some__iff) ).
thf(717,plain,
! [TA: $tType,A: TA > $o,B: list @ TA,C: TA] :
( ( ( find @ TA @ A @ B )
= ( some @ TA @ C ) )
= ( ? [D: nat] :
( ( ord_less @ nat @ D @ ( size_size @ ( list @ TA ) @ B ) )
& ( A @ ( nth @ TA @ B @ D ) )
& ( C
= ( nth @ TA @ B @ D ) )
& ! [E: nat] :
( ( ord_less @ nat @ E @ D )
=> ~ ( A @ ( nth @ TA @ B @ E ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[134]) ).
thf(130,axiom,
! [TA: $tType,A: list @ TA,B: nat,C: TA] :
( ( size_size @ ( list @ TA ) @ ( list_update @ TA @ A @ B @ C ) )
= ( size_size @ ( list @ TA ) @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_length__list__update) ).
thf(703,plain,
! [TA: $tType,A: list @ TA,B: nat,C: TA] :
( ( size_size @ ( list @ TA ) @ ( list_update @ TA @ A @ B @ C ) )
= ( size_size @ ( list @ TA ) @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[130]) ).
thf(103,axiom,
! [A: nat,B: nat] :
( ( ord_less @ nat @ A @ B )
=> ( A != B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_less__not__refl3) ).
thf(613,plain,
! [A: nat,B: nat] :
( ( ord_less @ nat @ A @ B )
=> ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[103]) ).
thf(6,axiom,
! [A: nat,B: nat] :
( ( A = B )
=> ( ord_less_eq @ nat @ A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_eq__imp__le) ).
thf(175,plain,
! [A: nat,B: nat] :
( ( A = B )
=> ( ord_less_eq @ nat @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(100,axiom,
! [TA: $tType,A: list @ TA,B: nat] :
( ( list_update @ TA @ A @ B @ ( nth @ TA @ A @ B ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_list__update__id) ).
thf(595,plain,
! [TA: $tType,A: list @ TA,B: nat] :
( ( list_update @ TA @ A @ B @ ( nth @ TA @ A @ B ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[100]) ).
thf(72,axiom,
! [TA: $tType,TB: $tType,A: TA > TB,B: list @ TA,C: nat,D: TA] :
( ( map @ TA @ TB @ A @ ( list_update @ TA @ B @ C @ D ) )
= ( list_update @ TB @ ( map @ TA @ TB @ A @ B ) @ C @ ( A @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6189_map__update) ).
thf(465,plain,
! [TA: $tType,TB: $tType,A: TA > TB,B: list @ TA,C: nat,D: TA] :
( ( map @ TA @ TB @ A @ ( list_update @ TA @ B @ C @ D ) )
= ( list_update @ TB @ ( map @ TA @ TB @ A @ B ) @ C @ ( A @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(120,axiom,
! [TA: $tType,TB: $tType] :
( ( list_all2 @ TA @ TB )
= ( ^ [A: TA > TB > $o,B: list @ TA,C: list @ TB] :
( ( ( size_size @ ( list @ TA ) @ B )
= ( size_size @ ( list @ TB ) @ C ) )
& ! [D: nat] :
( ( ord_less @ nat @ D @ ( size_size @ ( list @ TA ) @ B ) )
=> ( A @ ( nth @ TA @ B @ D ) @ ( nth @ TB @ C @ D ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7505_list__all2__conv__all__nth) ).
thf(671,plain,
! [TA: $tType,TB: $tType] :
( ( list_all2 @ TA @ TB )
= ( ^ [A: TA > TB > $o,B: list @ TA,C: list @ TB] :
( ( ( size_size @ ( list @ TA ) @ B )
= ( size_size @ ( list @ TB ) @ C ) )
& ! [D: nat] :
( ( ord_less @ nat @ D @ ( size_size @ ( list @ TA ) @ B ) )
=> ( A @ ( nth @ TA @ B @ D ) @ ( nth @ TB @ C @ D ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[120]) ).
thf(126,axiom,
! [TA: $tType,A: list @ TA,B: nat,C: TA,D: TA] :
( ( list_update @ TA @ ( list_update @ TA @ A @ B @ C ) @ B @ D )
= ( list_update @ TA @ A @ B @ D ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_list__update__overwrite) ).
thf(688,plain,
! [TA: $tType,A: list @ TA,B: nat,C: TA,D: TA] :
( ( list_update @ TA @ ( list_update @ TA @ A @ B @ C ) @ B @ D )
= ( list_update @ TA @ A @ B @ D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[126]) ).
thf(79,axiom,
! [TA: $tType,A: list @ TA,B: TA > $o,C: list @ TA] :
( ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ A ) )
=> ( B @ D ) )
=> ( ( takeWhile @ TA @ B @ ( append @ TA @ A @ C ) )
= ( append @ TA @ A @ ( takeWhile @ TA @ B @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6881_takeWhile__append2) ).
thf(495,plain,
! [TA: $tType,A: list @ TA,B: TA > $o,C: list @ TA] :
( ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ A ) )
=> ( B @ D ) )
=> ( ( takeWhile @ TA @ B @ ( append @ TA @ A @ C ) )
= ( append @ TA @ A @ ( takeWhile @ TA @ B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(146,axiom,
! [TA: $tType,TB: $tType,A: TB > TA > $o,B: list @ TB,C: list @ TA,D: nat] :
( ( list_all2 @ TB @ TA @ A @ B @ C )
=> ( ( ord_less @ nat @ D @ ( size_size @ ( list @ TA ) @ C ) )
=> ( A @ ( nth @ TB @ B @ D ) @ ( nth @ TA @ C @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7503_list__all2__nthD2) ).
thf(759,plain,
! [TA: $tType,TB: $tType,A: TB > TA > $o,B: list @ TB,C: list @ TA,D: nat] :
( ( list_all2 @ TB @ TA @ A @ B @ C )
=> ( ( ord_less @ nat @ D @ ( size_size @ ( list @ TA ) @ C ) )
=> ( A @ ( nth @ TB @ B @ D ) @ ( nth @ TA @ C @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[146]) ).
thf(76,axiom,
! [TA: $tType,A: nat,B: list @ TA] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( member @ TA @ ( nth @ TA @ B @ A ) @ ( set2 @ TA @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_nth__mem) ).
thf(482,plain,
! [TA: $tType,A: nat,B: list @ TA] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( member @ TA @ ( nth @ TA @ B @ A ) @ ( set2 @ TA @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(14,axiom,
! [TA: $tType,A: list @ TA,B: TA > TA] :
( ! [C: TA] :
( ( member @ TA @ C @ ( set2 @ TA @ A ) )
=> ( ( B @ C )
= C ) )
=> ( ( map @ TA @ TA @ B @ A )
= A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6196_map__idI) ).
thf(203,plain,
! [TA: $tType,A: list @ TA,B: TA > TA] :
( ! [C: TA] :
( ( member @ TA @ C @ ( set2 @ TA @ A ) )
=> ( ( B @ C )
= C ) )
=> ( ( map @ TA @ TA @ B @ A )
= A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(143,axiom,
( ( ord_less_eq @ nat @ mi @ xa )
& ( ord_less_eq @ nat @ xa @ ma ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34__092_060open_062mi_A_092_060le_062_Ax_A_092_060and_062_Ax_A_092_060le_062_Ama_092_060close_062) ).
thf(748,plain,
( ( ord_less_eq @ nat @ mi @ xa )
& ( ord_less_eq @ nat @ xa @ ma ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[143]) ).
thf(54,axiom,
! [TA: $tType,A: TA > $o,B: TA,C: TA > nat] :
( ( A @ B )
=> ? [D: TA] :
( ( A @ D )
& ! [E: TA] :
( ( A @ E )
=> ( ord_less_eq @ nat @ ( C @ D ) @ ( C @ E ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_279_ex__has__least__nat) ).
thf(390,plain,
! [TA: $tType,A: TA > $o,B: TA,C: TA > nat] :
( ( A @ B )
=> ? [D: TA] :
( ( A @ D )
& ! [E: TA] :
( ( A @ E )
=> ( ord_less_eq @ nat @ ( C @ D ) @ ( C @ E ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(9,axiom,
! [TA: $tType,A: TA > $o,B: list @ TA] :
( ( ( takeWhile @ TA @ A @ B )
= B )
= ( ! [C: TA] :
( ( member @ TA @ C @ ( set2 @ TA @ B ) )
=> ( A @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6879_takeWhile__eq__all__conv) ).
thf(186,plain,
! [TA: $tType,A: TA > $o,B: list @ TA] :
( ( ( takeWhile @ TA @ A @ B )
= B )
= ( ! [C: TA] :
( ( member @ TA @ C @ ( set2 @ TA @ B ) )
=> ( A @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(108,axiom,
! [TA: $tType] :
( ( sorted_wrt @ TA )
= ( ^ [A: TA > TA > $o,B: list @ TA] :
! [C: nat,D: nat] :
( ( ord_less @ nat @ C @ D )
=> ( ( ord_less @ nat @ D @ ( size_size @ ( list @ TA ) @ B ) )
=> ( A @ ( nth @ TA @ B @ C ) @ ( nth @ TA @ B @ D ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6807_sorted__wrt__iff__nth__less) ).
thf(632,plain,
! [TA: $tType] :
( ( sorted_wrt @ TA )
= ( ^ [A: TA > TA > $o,B: list @ TA] :
! [C: nat,D: nat] :
( ( ord_less @ nat @ C @ D )
=> ( ( ord_less @ nat @ D @ ( size_size @ ( list @ TA ) @ B ) )
=> ( A @ ( nth @ TA @ B @ C ) @ ( nth @ TA @ B @ D ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[108]) ).
thf(159,axiom,
( vEBT_V5917875025757280293ildren
= ( ^ [A: nat,B: list @ vEBT_VEBT,C: nat] : ( vEBT_V8194947554948674370ptions @ ( nth @ vEBT_VEBT @ B @ ( vEBT_VEBT_high @ C @ A ) ) @ ( vEBT_VEBT_low @ C @ A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_in__children__def) ).
thf(786,plain,
( vEBT_V5917875025757280293ildren
= ( ^ [A: nat,B: list @ vEBT_VEBT,C: nat] : ( vEBT_V8194947554948674370ptions @ ( nth @ vEBT_VEBT @ B @ ( vEBT_VEBT_high @ C @ A ) ) @ ( vEBT_VEBT_low @ C @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[159]) ).
thf(83,axiom,
! [TA: $tType,TB: $tType,A: list @ TB,B: list @ TB,C: TA > TB,D: list @ TA] :
( ( ( append @ TB @ A @ B )
= ( map @ TA @ TB @ C @ D ) )
= ( ? [E: list @ TA,F: list @ TA] :
( ( D
= ( append @ TA @ E @ F ) )
& ( A
= ( map @ TA @ TB @ C @ E ) )
& ( B
= ( map @ TA @ TB @ C @ F ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6410_append__eq__map__conv) ).
thf(510,plain,
! [TA: $tType,TB: $tType,A: list @ TB,B: list @ TB,C: TA > TB,D: list @ TA] :
( ( ( append @ TB @ A @ B )
= ( map @ TA @ TB @ C @ D ) )
= ( ? [E: list @ TA,F: list @ TA] :
( ( D
= ( append @ TA @ E @ F ) )
& ( A
= ( map @ TA @ TB @ C @ E ) )
& ( B
= ( map @ TA @ TB @ C @ F ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(91,axiom,
! [TA: $tType,A: list @ TA,B: TA > $o,C: nat] :
( ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ A ) )
=> ( B @ D ) )
=> ( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ A ) )
=> ( B @ ( nth @ TA @ A @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_inthall) ).
thf(549,plain,
! [TA: $tType,A: list @ TA,B: TA > $o,C: nat] :
( ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ A ) )
=> ( B @ D ) )
=> ( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ A ) )
=> ( B @ ( nth @ TA @ A @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(144,axiom,
! [TA: $tType,A: list @ TA,B: list @ TA] :
( ( ( size_size @ ( list @ TA ) @ A )
!= ( size_size @ ( list @ TA ) @ B ) )
=> ( A != B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_neq__if__length__neq) ).
thf(752,plain,
! [TA: $tType,A: list @ TA,B: list @ TA] :
( ( ( size_size @ ( list @ TA ) @ A )
!= ( size_size @ ( list @ TA ) @ B ) )
=> ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[144]) ).
thf(29,axiom,
! [TA: $tType,TB: $tType,TC: $tType,A: TC > TB > $o,B: list @ TC,C: TA > TB,D: list @ TA] :
( ( list_all2 @ TC @ TB @ A @ B @ ( map @ TA @ TB @ C @ D ) )
= ( list_all2 @ TC @ TA
@ ^ [E: TC,F: TA] : ( A @ E @ ( C @ F ) )
@ B
@ D ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7451_list_Orel__map_I2_J) ).
thf(262,plain,
! [TA: $tType,TB: $tType,TC: $tType,A: TC > TB > $o,B: list @ TC,C: TA > TB,D: list @ TA] :
( ( list_all2 @ TC @ TB @ A @ B @ ( map @ TA @ TB @ C @ D ) )
= ( list_all2 @ TC @ TA
@ ^ [E: TC,F: TA] : ( A @ E @ ( C @ F ) )
@ B
@ D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(56,axiom,
! [A: vEBT_VEBT,B: nat,C: nat] :
( ( vEBT_invar_vebt @ A @ B )
=> ( ( vEBT_V8194947554948674370ptions @ A @ C )
= ( vEBT_vebt_member @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_both__member__options__equiv__member) ).
thf(405,plain,
! [A: vEBT_VEBT,B: nat,C: nat] :
( ( vEBT_invar_vebt @ A @ B )
=> ( ( vEBT_V8194947554948674370ptions @ A @ C )
= ( vEBT_vebt_member @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(38,axiom,
! [TA: $tType,TB: $tType,A: TB > TA > $o,B: list @ TB,C: list @ TA,D: TB,E: TA,F: nat] :
( ( list_all2 @ TB @ TA @ A @ B @ C )
=> ( ( A @ D @ E )
=> ( list_all2 @ TB @ TA @ A @ ( list_update @ TB @ B @ F @ D ) @ ( list_update @ TA @ C @ F @ E ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7469_list__all2__update__cong) ).
thf(294,plain,
! [TA: $tType,TB: $tType,A: TB > TA > $o,B: list @ TB,C: list @ TA,D: TB,E: TA,F: nat] :
( ( list_all2 @ TB @ TA @ A @ B @ C )
=> ( ( A @ D @ E )
=> ( list_all2 @ TB @ TA @ A @ ( list_update @ TB @ B @ F @ D ) @ ( list_update @ TA @ C @ F @ E ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(31,axiom,
! [A: nat,B: nat,C: nat] :
( ( ord_less_eq @ nat @ A @ B )
=> ( ( ord_less_eq @ nat @ B @ C )
=> ( ord_less_eq @ nat @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_le__trans) ).
thf(268,plain,
! [A: nat,B: nat,C: nat] :
( ( ord_less_eq @ nat @ A @ B )
=> ( ( ord_less_eq @ nat @ B @ C )
=> ( ord_less_eq @ nat @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(109,axiom,
! [TA: $tType,A: list @ TA,B: nat,C: nat] :
( ( distinct @ TA @ A )
=> ( ( ord_less @ nat @ B @ ( size_size @ ( list @ TA ) @ A ) )
=> ( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ A ) )
=> ( ( ( nth @ TA @ A @ B )
= ( nth @ TA @ A @ C ) )
= ( B = C ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3452_nth__eq__iff__index__eq) ).
thf(635,plain,
! [TA: $tType,A: list @ TA,B: nat,C: nat] :
( ( distinct @ TA @ A )
=> ( ( ord_less @ nat @ B @ ( size_size @ ( list @ TA ) @ A ) )
=> ( ( ord_less @ nat @ C @ ( size_size @ ( list @ TA ) @ A ) )
=> ( ( ( nth @ TA @ A @ B )
= ( nth @ TA @ A @ C ) )
= ( B = C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[109]) ).
thf(135,axiom,
! [A: nat,B: nat] :
( ( ord_less @ nat @ A @ B )
=> ( B != A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_less__not__refl2) ).
thf(720,plain,
! [A: nat,B: nat] :
( ( ord_less @ nat @ A @ B )
=> ( B != A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[135]) ).
thf(35,axiom,
! [TA: $tType,A: list @ TA,B: list @ TA,C: list @ TA] :
( ( append @ TA @ ( append @ TA @ A @ B ) @ C )
= ( append @ TA @ A @ ( append @ TA @ B @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6377_append_Oassoc) ).
thf(283,plain,
! [TA: $tType,A: list @ TA,B: list @ TA,C: list @ TA] :
( ( append @ TA @ ( append @ TA @ A @ B ) @ C )
= ( append @ TA @ A @ ( append @ TA @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(59,axiom,
! [TA: $tType,A: list @ TA,B: TA > $o] :
( ( distinct @ TA @ A )
=> ( distinct @ TA @ ( takeWhile @ TA @ B @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6892_distinct__takeWhile) ).
thf(415,plain,
! [TA: $tType,A: list @ TA,B: TA > $o] :
( ( distinct @ TA @ A )
=> ( distinct @ TA @ ( takeWhile @ TA @ B @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(22,axiom,
! [TA: $tType,TB: $tType,A: TA > TB,B: list @ TA] :
( ( map @ TA @ TB @ A @ ( butlast @ TA @ B ) )
= ( butlast @ TB @ ( map @ TA @ TB @ A @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7354_map__butlast) ).
thf(239,plain,
! [TA: $tType,TB: $tType,A: TA > TB,B: list @ TA] :
( ( map @ TA @ TB @ A @ ( butlast @ TA @ B ) )
= ( butlast @ TB @ ( map @ TA @ TB @ A @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(23,axiom,
! [TA: $tType,TB: $tType,A: TB > TA > $o,B: list @ TB,C: list @ TB,D: list @ TA] :
( ( list_all2 @ TB @ TA @ A @ ( append @ TB @ B @ C ) @ D )
= ( ? [E: list @ TA,F: list @ TA] :
( ( D
= ( append @ TA @ E @ F ) )
& ( ( size_size @ ( list @ TA ) @ E )
= ( size_size @ ( list @ TB ) @ B ) )
& ( ( size_size @ ( list @ TA ) @ F )
= ( size_size @ ( list @ TB ) @ C ) )
& ( list_all2 @ TB @ TA @ A @ B @ E )
& ( list_all2 @ TB @ TA @ A @ C @ F ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7494_list__all2__append1) ).
thf(242,plain,
! [TA: $tType,TB: $tType,A: TB > TA > $o,B: list @ TB,C: list @ TB,D: list @ TA] :
( ( list_all2 @ TB @ TA @ A @ ( append @ TB @ B @ C ) @ D )
= ( ? [E: list @ TA,F: list @ TA] :
( ( D
= ( append @ TA @ E @ F ) )
& ( ( size_size @ ( list @ TA ) @ E )
= ( size_size @ ( list @ TB ) @ B ) )
& ( ( size_size @ ( list @ TA ) @ F )
= ( size_size @ ( list @ TB ) @ C ) )
& ( list_all2 @ TB @ TA @ A @ B @ E )
& ( list_all2 @ TB @ TA @ A @ C @ F ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(3,axiom,
! [A: nat,B: nat] :
( ( ( ord_less @ nat @ A @ B )
| ( A = B ) )
=> ( ord_less_eq @ nat @ A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_less__or__eq__imp__le) ).
thf(163,plain,
! [A: nat,B: nat] :
( ( ( ord_less @ nat @ A @ B )
| ( A = B ) )
=> ( ord_less_eq @ nat @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(67,axiom,
! [TA: $tType,A: list @ TA,B: TA > TA > $o,C: TA > TA > $o] :
( ! [D: TA,E: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ A ) )
=> ( ( member @ TA @ E @ ( set2 @ TA @ A ) )
=> ( ( B @ D @ E )
=> ( C @ D @ E ) ) ) )
=> ( ( sorted_wrt @ TA @ B @ A )
=> ( sorted_wrt @ TA @ C @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6801_sorted__wrt__mono__rel) ).
thf(442,plain,
! [TA: $tType,A: list @ TA,B: TA > TA > $o,C: TA > TA > $o] :
( ! [D: TA,E: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ A ) )
=> ( ( member @ TA @ E @ ( set2 @ TA @ A ) )
=> ( ( B @ D @ E )
=> ( C @ D @ E ) ) ) )
=> ( ( sorted_wrt @ TA @ B @ A )
=> ( sorted_wrt @ TA @ C @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(80,axiom,
! [TA: $tType,TB: $tType,A: TA > TB > $o,B: list @ TA,C: list @ TB,D: list @ TB] :
( ( list_all2 @ TA @ TB @ A @ B @ ( append @ TB @ C @ D ) )
= ( ? [E: list @ TA,F: list @ TA] :
( ( B
= ( append @ TA @ E @ F ) )
& ( ( size_size @ ( list @ TA ) @ E )
= ( size_size @ ( list @ TB ) @ C ) )
& ( ( size_size @ ( list @ TA ) @ F )
= ( size_size @ ( list @ TB ) @ D ) )
& ( list_all2 @ TA @ TB @ A @ E @ C )
& ( list_all2 @ TA @ TB @ A @ F @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7495_list__all2__append2) ).
thf(501,plain,
! [TA: $tType,TB: $tType,A: TA > TB > $o,B: list @ TA,C: list @ TB,D: list @ TB] :
( ( list_all2 @ TA @ TB @ A @ B @ ( append @ TB @ C @ D ) )
= ( ? [E: list @ TA,F: list @ TA] :
( ( B
= ( append @ TA @ E @ F ) )
& ( ( size_size @ ( list @ TA ) @ E )
= ( size_size @ ( list @ TB ) @ C ) )
& ( ( size_size @ ( list @ TA ) @ F )
= ( size_size @ ( list @ TB ) @ D ) )
& ( list_all2 @ TA @ TB @ A @ E @ C )
& ( list_all2 @ TA @ TB @ A @ F @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(102,axiom,
! [TA: $tType,TB: $tType,A: list @ TB,B: list @ TA,C: TB > TA > $o] :
( ( ( size_size @ ( list @ TB ) @ A )
= ( size_size @ ( list @ TA ) @ B ) )
=> ( ! [D: nat] :
( ( ord_less @ nat @ D @ ( size_size @ ( list @ TB ) @ A ) )
=> ( C @ ( nth @ TB @ A @ D ) @ ( nth @ TA @ B @ D ) ) )
=> ( list_all2 @ TB @ TA @ C @ A @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7504_list__all2__all__nthI) ).
thf(607,plain,
! [TA: $tType,TB: $tType,A: list @ TB,B: list @ TA,C: TB > TA > $o] :
( ( ( size_size @ ( list @ TB ) @ A )
= ( size_size @ ( list @ TA ) @ B ) )
=> ( ! [D: nat] :
( ( ord_less @ nat @ D @ ( size_size @ ( list @ TB ) @ A ) )
=> ( C @ ( nth @ TB @ A @ D ) @ ( nth @ TA @ B @ D ) ) )
=> ( list_all2 @ TB @ TA @ C @ A @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[102]) ).
thf(34,axiom,
! [TA: $tType,A: nat,B: list @ TA,C: TA > $o] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ B ) )
=> ( C @ D ) )
=> ( C @ ( nth @ TA @ B @ A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_list__ball__nth) ).
thf(277,plain,
! [TA: $tType,A: nat,B: list @ TA,C: TA > $o] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ B ) )
=> ( ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ B ) )
=> ( C @ D ) )
=> ( C @ ( nth @ TA @ B @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(127,axiom,
! [A: vEBT_VEBT,B: nat,C: nat] :
( ( vEBT_invar_vebt @ A @ B )
=> ( ( ( vEBT_vebt_maxt @ A )
= ( some @ nat @ C ) )
=> ( vEBT_vebt_member @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_maxt__member) ).
thf(691,plain,
! [A: vEBT_VEBT,B: nat,C: nat] :
( ( vEBT_invar_vebt @ A @ B )
=> ( ( ( vEBT_vebt_maxt @ A )
= ( some @ nat @ C ) )
=> ( vEBT_vebt_member @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[127]) ).
thf(19,axiom,
! [TA: $tType,A: TA > TA > $o,B: list @ TA] :
( ! [C: TA] : ( A @ C @ C )
=> ( list_all2 @ TA @ TA @ A @ B @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7463_list_Orel__refl) ).
thf(227,plain,
! [TA: $tType,A: TA > TA > $o,B: list @ TA] :
( ! [C: TA] : ( A @ C @ C )
=> ( list_all2 @ TA @ TA @ A @ B @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(45,axiom,
! [TA: $tType,A: TA,B: list @ TA] :
( ( member @ TA @ A @ ( set2 @ TA @ ( butlast @ TA @ B ) ) )
=> ( member @ TA @ A @ ( set2 @ TA @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7347_in__set__butlastD) ).
thf(337,plain,
! [TA: $tType,A: TA,B: list @ TA] :
( ( member @ TA @ A @ ( set2 @ TA @ ( butlast @ TA @ B ) ) )
=> ( member @ TA @ A @ ( set2 @ TA @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(116,axiom,
! [TA: $tType,A: TA,B: TA] :
( ( ( some @ TA @ A )
= ( some @ TA @ B ) )
= ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_256_option_Oinject) ).
thf(659,plain,
! [TA: $tType,A: TA,B: TA] :
( ( ( some @ TA @ A )
= ( some @ TA @ B ) )
= ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[116]) ).
thf(122,axiom,
! [TA: $tType,A: nat,B: nat,C: list @ TA,D: TA] :
( ( A != B )
=> ( ( nth @ TA @ ( list_update @ TA @ C @ A @ D ) @ B )
= ( nth @ TA @ C @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_nth__list__update__neq) ).
thf(676,plain,
! [TA: $tType,A: nat,B: nat,C: list @ TA,D: TA] :
( ( A != B )
=> ( ( nth @ TA @ ( list_update @ TA @ C @ A @ D ) @ B )
= ( nth @ TA @ C @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[122]) ).
thf(17,axiom,
! [TA: $tType,TB: $tType,A: TA > TB,B: list @ TA,C: TA > TB] :
( ( ( map @ TA @ TB @ A @ B )
= ( map @ TA @ TB @ C @ B ) )
= ( ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ B ) )
=> ( ( A @ D )
= ( C @ D ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6162_map__eq__conv) ).
thf(222,plain,
! [TA: $tType,TB: $tType,A: TA > TB,B: list @ TA,C: TA > TB] :
( ( ( map @ TA @ TB @ A @ B )
= ( map @ TA @ TB @ C @ B ) )
= ( ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ B ) )
=> ( ( A @ D )
= ( C @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(99,axiom,
! [TA: $tType,A: nat,B: TA > $o,C: list @ TA] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ ( takeWhile @ TA @ B @ C ) ) )
=> ( ( nth @ TA @ ( takeWhile @ TA @ B @ C ) @ A )
= ( nth @ TA @ C @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6900_takeWhile__nth) ).
thf(592,plain,
! [TA: $tType,A: nat,B: TA > $o,C: list @ TA] :
( ( ord_less @ nat @ A @ ( size_size @ ( list @ TA ) @ ( takeWhile @ TA @ B @ C ) ) )
=> ( ( nth @ TA @ ( takeWhile @ TA @ B @ C ) @ A )
= ( nth @ TA @ C @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[99]) ).
thf(69,axiom,
! [TA: $tType,TB: $tType,A: list @ TA,B: TA > TB,C: TA > TB] :
( ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ A ) )
=> ( ( B @ D )
= ( C @ D ) ) )
=> ( ( map @ TA @ TB @ B @ A )
= ( map @ TA @ TB @ C @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6195_map__ext) ).
thf(454,plain,
! [TA: $tType,TB: $tType,A: list @ TA,B: TA > TB,C: TA > TB] :
( ! [D: TA] :
( ( member @ TA @ D @ ( set2 @ TA @ A ) )
=> ( ( B @ D )
= ( C @ D ) ) )
=> ( ( map @ TA @ TB @ B @ A )
= ( map @ TA @ TB @ C @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(50,axiom,
! [A: nat > $o,B: nat,C: nat] :
( ( A @ B )
=> ( ! [D: nat] :
( ( A @ D )
=> ( ord_less_eq @ nat @ D @ C ) )
=> ? [D: nat] :
( ( A @ D )
& ! [E: nat] :
( ( A @ E )
=> ( ord_less_eq @ nat @ E @ D ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_Nat_Oex__has__greatest__nat) ).
thf(364,plain,
! [A: nat > $o,B: nat,C: nat] :
( ( A @ B )
=> ( ! [D: nat] :
( ( A @ D )
=> ( ord_less_eq @ nat @ D @ C ) )
=> ? [D: nat] :
( ( A @ D )
& ! [E: nat] :
( ( A @ E )
=> ( ord_less_eq @ nat @ E @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(20,axiom,
! [TA: $tType,A: TA,B: TA > $o,C: list @ TA] :
( ( member @ TA @ A @ ( set2 @ TA @ ( takeWhile @ TA @ B @ C ) ) )
=> ( ( member @ TA @ A @ ( set2 @ TA @ C ) )
& ( B @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6896_set__takeWhileD) ).
thf(232,plain,
! [TA: $tType,A: TA,B: TA > $o,C: list @ TA] :
( ( member @ TA @ A @ ( set2 @ TA @ ( takeWhile @ TA @ B @ C ) ) )
=> ( ( member @ TA @ A @ ( set2 @ TA @ C ) )
& ( B @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(792,plain,
$false,
inference(e,[status(thm)],[629,479,628,518,468,777,555,582,655,385,538,782,709,417,288,301,436,651,724,504,460,638,189,770,448,316,756,789,179,253,766,397,734,774,265,380,439,546,761,534,334,778,598,192,788,197,665,583,682,566,484,742,725,169,420,256,488,225,339,476,526,679,706,622,515,508,657,674,662,412,513,745,296,423,772,286,711,579,259,641,382,236,350,764,172,219,274,784,736,245,434,271,345,700,251,668,330,462,685,768,695,780,563,426,589,162,617,342,194,648,209,327,739,409,182,717,703,613,175,595,465,671,688,495,759,482,203,748,390,186,632,786,510,549,752,262,405,294,268,635,720,283,415,239,242,163,442,501,607,277,691,227,337,659,676,222,592,454,364,232]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP256^2 : TPTP v9.3.1. Bugfixed v9.2.1.
% 0.00/0.10 % 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.09/0.25 % Computer : n013.cluster.edu
% 0.09/0.25 % Model : x86_64 x86_64
% 0.09/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.25 % Memory : 8046.5625MB
% 0.09/0.25 % OS : Linux 6.8.0-71-generic
% 0.09/0.25 % CPULimit : 300
% 0.09/0.25 % WCLimit : 300
% 0.09/0.25 % DateTime : Tue Sep 29 20:39:06 UTC 2026
% 0.09/0.25 % CPUTime :
% 0.09/0.25 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
% 0.98/0.84 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 6.39/2.55 % [INFO] Parsing done (1703ms).
% 6.39/2.57 % [INFO] Running in sequential loop mode.
% 7.11/2.93 % [INFO] eprover registered as external prover.
% 7.11/2.94 % [INFO] Scanning for conjecture ...
% 9.02/3.54 % [INFO] Found a conjecture (or negated_conjecture) and 8975 axioms. Running axiom selection ...
% 10.62/4.29 % [INFO] Axiom selection finished. Selected 159 axioms (removed 8816 axioms).
% 11.28/4.52 % [INFO] Problem is higher-order (TPTP THF).
% 11.28/4.55 % [INFO] Type checking passed.
% 11.28/4.55 % [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 ...
% 85.06/61.06 % External prover 'e' found a proof!
% 85.53/61.06 % [INFO] Killing All external provers ...
% 85.53/61.06 % Time passed: 60663ms (effective reasoning time: 58487ms)
% 85.53/61.06 % 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)>
% 85.53/61.07 % Axioms used in derivation (159): fact_7455_list__all2__appendI, fact_52_eq__imp__le, fact_6377_append_Oassoc, fact_256_option_Oinject, fact_120_maxbmo, fact_111_valid__member__both__member__options, fact_54_le__refl, fact_51_le__antisym, fact_6454_list__update__append1, fact_84_less__not__refl, tcon_Nat_Onat___Nat_Osize, fact_3_valid__eq, fact_68_all__set__conv__all__nth, fact_6445_append__eq__append__conv2, fact_6378_append__assoc, fact_7495_list__all2__append2, tcon_VEBT__Definitions_OVEBT___Nat_Osize_624, fact_80_nat__less__induct, fact_81_less__irrefl__nat, fact_6379_append__same__eq, fact_86_size__neq__size__imp__neq, fact_6771_sorted__wrt__map, fact_7454_list__all2__map2, fact_49_Nat_Oex__has__greatest__nat, fact_72_nth__mem, fact_6881_takeWhile__append2, fact_3432_distinct__swap, fact_636_find__cong, fact_15_not__min__Null__member, fact_28_list__update__id, fact_7354_map__butlast, fact_6444_append__eq__appendI, fact_7499_list_Orel__cong, fact_60_less__mono__imp__le__mono, fact_6895_takeWhile__cong, fact_6902_length__takeWhile__less__P__nth, fact_119_min__Null__member, fact_6828_sorted__wrt__less__idx, fact_38_inthall, fact_105_nth__equalityI, fact_0__C4_Ohyps_C_I3_J, fact_43_list__update__beyond, fact_27_nth__list__update__neq, fact_22__C4_Ohyps_C_I6_J, fact_7469_list__all2__update__cong, fact_88_Ex__list__of__length, fact_39_list__update__overwrite, fact_35_nth__list__update, fact_6896_set__takeWhileD, fact_6155_map__ident, fact_6799_sorted__wrt__append, fact_7462_list_Orel__eq, fact_19_mimapr, fact_7463_list_Orel__refl, fact_6193_list_Omap__cong0, fact_538_find__Some__iff2, fact_106_list__update__same__conv, fact_83_less__not__refl2, fact_6390_map__append, fact_6380_same__append__eq, fact_103_list__eq__iff__nth__eq, fact_7493_list__all2__append, fact_6197_map__cong, fact_87_neq__if__length__neq, fact_7356_nth__butlast, fact_7500_list__all2__lengthD, fact_3453_distinct__conv__nth, fact_4_valid__eq1, fact_25_nth__list__update__eq, fact_7453_list__all2__map1, fact_7468_list__all2__antisym, fact_1_xmi, fact_14_hprolist, fact_8__092_060open_062high_Ax_An_A_060_Alength_AtreeList_092_060close_062, fact_7503_list__all2__nthD2, fact_62_less__or__eq__imp__le, fact_7496_list__all2__same, fact_65_nat__less__le, fact_7452_list_Orel__map_I1_J, fact_6185_list_Omap__ident, fact_7502_list__all2__nthD, fact_6162_map__eq__conv, fact_48_set__swap, fact_7504_list__all2__all__nthI, fact_6410_append__eq__map__conv, fact_6198_ex__map__conv, fact_110_both__member__options__equiv__member, fact_50_nat__le__linear, fact_63_le__eq__less__or__eq, fact_6880_takeWhile__append1, fact_6879_takeWhile__eq__all__conv, fact_10_False, fact_6807_sorted__wrt__iff__nth__less, fact_122_maxt__member, fact_6901_takeWhile__append, fact_6192_list_Omap__cong, fact_85_nat__neq__iff, fact_7451_list_Orel__map_I2_J, fact_370_bounded__Max__nat, fact_7464_list__all2__eq, fact_104_Skolem__list__nth, fact_71_list__ball__nth, fact_2_True, fact_3456_distinct__Ex1, fact_6900_takeWhile__nth, fact_6878_takeWhile__idem, tcon_List_Olist___Nat_Osize_244, fact_7346_in__set__butlast__appendI, fact_279_ex__has__least__nat, fact_109_maxidef, fact_7494_list__all2__append1, fact_3452_nth__eq__iff__index__eq, fact_6163_length__map, fact_6191_map__eq__imp__length__eq, fact_7347_in__set__butlastD, fact_6892_distinct__takeWhile, fact_73_set__update__memI, fact_21__C4_Ohyps_C_I7_J, fact_6194_list_Oinj__map__strong, fact_102_length__induct, fact_23__C4_OIH_C_I1_J, fact_7497_list_Orel__refl__strong, fact_7467_list__all2__trans, fact_53_le__trans, fact_7466_list__all2__refl, fact_82_less__not__refl3, fact_6196_map__idI, fact_34__092_060open_062mi_A_092_060le_062_Ax_A_092_060and_062_Ax_A_092_060le_062_Ama_092_060close_062, fact_539_find__Some__iff, fact_70_in__set__conv__nth, fact_20__092_060open_062length_AtreeList_A_061_Alength_A_ItreeList_091high_Ax_An_A_058_061_Avebt__delete_A_ItreeList_A_B_Ahigh_Ax_An_J_A_Ilow_Ax_An_J_093_J_092_060close_062, fact_79_infinite__descent, fact_6172_nth__map, fact_125_maxt__corr__help, fact_69_all__nth__imp__all__set, fact_7498_list_Orel__mono__strong, fact_380_nat__descend__induct, fact_6899_nth__length__takeWhile, fact_13_notemp, fact_6808_sorted__wrt__nth__less, fact_6195_map__ext, fact_24_in__children__def, fact_7348_distinct__butlast, fact_5_valid__eq2, fact_78_linorder__neqE__nat, fact_6389_append__eq__append__conv, fact_7465_list__all2__mono, fact_6801_sorted__wrt__mono__rel, fact_29_length__list__update, fact_64_less__imp__le__nat, fact_6189_map__update, fact_117__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062maxi_O_ASome_Amaxi_A_061_Avebt__maxt_A_ItreeList_091high_Ax_An_A_058_061_Avebt__delete_A_ItreeList_A_B_Ahigh_Ax_An_J_A_Ilow_Ax_An_J_093_A_B_Ahigh_Ax_An_J_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062, fact_6409_map__eq__append__conv, fact_77_infinite__descent__measure, fact_284_Lattices__Big_Oex__has__greatest__nat, fact_61_le__neq__implies__less, fact_7505_list__all2__conv__all__nth, fact_6893_length__takeWhile__le, fact_89_list__update__swap
% 85.53/61.07 % No. of inferences in proof: 322
% 85.53/61.07 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 60663 ms resp. 58487 ms w/o parsing
% 86.61/61.33 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 86.61/61.33 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------