%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SWW508_5 : TPTP v9.3.1. Released v6.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n007.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 : Sun Sep 27 09:10:42 AM UTC 2026
% Result : Theorem 226.94s 79.04s
% Output : Refutation 226.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 140
% Syntax : Number of formulae : 570 ( 184 unt; 0 typ; 10 def)
% Number of atoms : 2967 ( 580 equ; 0 cnn)
% Maximal formula atoms : 36 ( 5 avg)
% Number of connectives : 14067 ( 459 ~; 288 |; 124 &;12920 @)
% ( 24 <=>; 252 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 9 avg)
% Number of types : 9 ( 8 usr)
% Number of type conns : 8 ( 8 >; 0 *; 0 +; 0 <<)
% Number of symbols : 55 ( 52 usr; 17 con; 0-10 aty)
% Number of variables : 1609 ( 14 ^;1520 !; 65 ?;1609 :)
% ( 0 !>; 0 ?*; 0 @-; 10 @+)
% Comments :
%------------------------------------------------------------------------------
thf(a_type,type,
a: $tType ).
thf(com_type,type,
com: $tType ).
thf(loc_type,type,
loc: $tType ).
thf(pname_type,type,
pname: $tType ).
thf(state_type,type,
state: $tType ).
thf(vname_type,type,
vname: $tType ).
thf(bool_type,type,
bool: $tType ).
thf(nat_type,type,
nat: $tType ).
thf(cl_Groups_Ominus_decl,type,
cl_Groups_Ominus:
!>[TA: $tType] : $o ).
thf(bot_decl,type,
bot:
!>[TA: $tType] : $o ).
thf(finite_finite_decl,type,
finite_finite:
!>[TA: $tType] : $o ).
thf(combb_decl,type,
combb:
!>[TA: $tType,TB: $tType,TC: $tType] : ( ( TB @ ( TC @ fun ) ) > ( TC @ ( TA @ fun ) ) > ( TB @ ( TA @ fun ) ) ) ).
thf(combc_decl,type,
combc:
!>[TA: $tType,TB: $tType,TC: $tType] : ( ( TA @ ( TB @ fun ) @ ( TC @ fun ) ) > TB > ( TA @ ( TC @ fun ) ) ) ).
thf(combk_decl,type,
combk:
!>[TA: $tType,TB: $tType] : ( TB > ( TB @ ( TA @ fun ) ) ) ).
thf(combs_decl,type,
combs:
!>[TA: $tType,TB: $tType,TC: $tType] : ( ( TA @ ( TB @ fun ) @ ( TC @ fun ) ) > ( TB @ ( TC @ fun ) ) > ( TA @ ( TC @ fun ) ) ) ).
thf(skip_decl,type,
skip: com ).
thf(semi_decl,type,
semi: com > com > com ).
thf(com_case_decl,type,
com_case:
!>[TA: $tType] : ( TA > ( TA @ ( nat @ ( state @ fun ) @ fun ) @ ( vname @ fun ) ) > ( TA @ ( com @ fun ) @ ( nat @ ( state @ fun ) @ fun ) @ ( loc @ fun ) ) > ( TA @ ( com @ fun ) @ ( com @ fun ) ) > ( TA @ ( com @ fun ) @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ fun ) ) > ( TA @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ fun ) ) > ( TA @ ( pname @ fun ) ) > ( TA @ ( nat @ ( state @ fun ) @ fun ) @ ( pname @ fun ) @ ( vname @ fun ) ) > com > TA ) ).
thf(finite_finite1_decl,type,
finite_finite1:
!>[TA: $tType] : ( ( bool @ ( TA @ fun ) ) > $o ) ).
thf(finite_fold1Set_decl,type,
finite_fold1Set:
!>[TA: $tType] : ( ( TA @ ( TA @ fun ) @ ( TA @ fun ) ) > ( bool @ ( TA @ fun ) ) > TA > $o ) ).
thf(finite_fold_graph_decl,type,
finite_fold_graph:
!>[TA: $tType,TB: $tType] : ( ( TA @ ( TA @ fun ) @ ( TB @ fun ) ) > TA > ( bool @ ( TB @ fun ) ) > TA > $o ) ).
thf(finite_folding_one_decl,type,
finite_folding_one:
!>[TA: $tType] : ( ( TA @ ( TA @ fun ) @ ( TA @ fun ) ) > ( TA @ ( bool @ ( TA @ fun ) @ fun ) ) > $o ) ).
thf(minus_minus_decl,type,
minus_minus:
!>[TA: $tType] : ( TA > TA > TA ) ).
thf(hoare_992312373derivs_decl,type,
hoare_992312373derivs:
!>[TA: $tType] : ( ( bool @ ( TA @ hoare_28830079triple @ fun ) ) > ( bool @ ( TA @ hoare_28830079triple @ fun ) ) > $o ) ).
thf(hoare_1841697145triple_decl,type,
hoare_1841697145triple:
!>[TA: $tType] : ( ( bool @ ( state @ fun ) @ ( TA @ fun ) ) > com > ( bool @ ( state @ fun ) @ ( TA @ fun ) ) > ( TA @ hoare_28830079triple ) ) ).
thf(hoare_376461865e_case_decl,type,
hoare_376461865e_case:
!>[TA: $tType,TB: $tType] : ( ( TA @ ( bool @ ( state @ fun ) @ ( TB @ fun ) @ fun ) @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ ( TB @ fun ) @ fun ) ) > ( TB @ hoare_28830079triple ) > TA ) ).
thf(hoare_678420151le_rec_decl,type,
hoare_678420151le_rec:
!>[TA: $tType,TB: $tType] : ( ( TA @ ( bool @ ( state @ fun ) @ ( TB @ fun ) @ fun ) @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ ( TB @ fun ) @ fun ) ) > ( TB @ hoare_28830079triple ) > TA ) ).
thf(bot_bot_decl,type,
bot_bot:
!>[TA: $tType] : TA ).
thf(inv_imagep_decl,type,
inv_imagep:
!>[TA: $tType,TB: $tType] : ( ( bool @ ( TB @ fun ) @ ( TB @ fun ) ) > ( TB @ ( TA @ fun ) ) > TA > TA > $o ) ).
thf(collect_decl,type,
collect:
!>[TA: $tType] : ( ( bool @ ( TA @ fun ) ) > ( bool @ ( TA @ fun ) ) ) ).
thf(insert_decl,type,
insert:
!>[TA: $tType] : ( TA > ( bool @ ( TA @ fun ) ) > ( bool @ ( TA @ fun ) ) ) ).
thf(the_elem_decl,type,
the_elem:
!>[TA: $tType] : ( ( bool @ ( TA @ fun ) ) > TA ) ).
thf(aa_decl,type,
aa:
!>[TA: $tType,TB: $tType] : ( ( TA @ ( TB @ fun ) ) > TB > TA ) ).
thf(fFalse_decl,type,
fFalse: bool ).
thf(fNot_decl,type,
fNot: bool @ ( bool @ fun ) ).
thf(fTrue_decl,type,
fTrue: bool ).
thf(fconj_decl,type,
fconj: bool @ ( bool @ fun ) @ ( bool @ fun ) ).
thf(fdisj_decl,type,
fdisj: bool @ ( bool @ fun ) @ ( bool @ fun ) ).
thf(fequal_decl,type,
fequal:
!>[TA: $tType] : ( bool @ ( TA @ fun ) @ ( TA @ fun ) ) ).
thf(fimplies_decl,type,
fimplies: bool @ ( bool @ fun ) @ ( bool @ fun ) ).
thf(member_decl,type,
member:
!>[TA: $tType] : ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ fun ) ) ).
thf(pp_decl,type,
pp: bool > $o ).
thf(g_decl,type,
g: bool @ ( a @ hoare_28830079triple @ fun ) ).
thf(p_decl,type,
p: a > state > $o ).
thf(p1_decl,type,
p1: bool @ ( state @ fun ) @ ( a @ fun ) ).
thf(q_decl,type,
q: a > state > $o ).
thf(q1_decl,type,
q1: bool @ ( state @ fun ) @ ( a @ fun ) ).
thf(c_decl,type,
c: com ).
thf(sk1_decl,type,
sk1: a ).
thf(sk2_decl,type,
sk2: state ).
thf(sk3_decl,type,
sk3: ( bool @ ( state @ fun ) @ ( a @ fun ) ) > ( bool @ ( state @ fun ) @ ( a @ fun ) ) > state ).
thf(sk4_decl,type,
sk4: com > com > com ).
thf(sk5_decl,type,
sk5: com > com > com ).
thf(sk6_decl,type,
sk6:
!>[TA: $tType] : ( ( bool @ ( TA @ fun ) ) > ( bool @ ( bool @ ( TA @ fun ) @ fun ) ) > TA ) ).
thf(sk7_decl,type,
sk7:
!>[TA: $tType] : ( ( bool @ ( TA @ fun ) ) > ( bool @ ( bool @ ( TA @ fun ) @ fun ) ) > ( bool @ ( TA @ fun ) ) ) ).
thf(sk10_decl,type,
sk10:
!>[TA: $tType] : ( ( bool @ ( TA @ fun ) ) > TA ) ).
thf(sk12_decl,type,
sk12:
!>[TA: $tType] : ( ( bool @ ( TA @ fun ) ) > ( bool @ ( TA @ fun ) ) ) ).
thf(sk13_decl,type,
sk13:
!>[TA: $tType] : ( ( bool @ ( TA @ fun ) ) > TA ) ).
thf(sk1_def,definition,
( sk1
= ( @+[A: a] :
~ ! [B: state] :
( ? [C: bool @ ( state @ fun ) @ ( a @ fun ),D: bool @ ( state @ fun ) @ ( a @ fun )] :
( ! [E: state] :
( ( E @ ( A @ q ) )
| ? [F: a] :
( ~ ( E @ ( F @ ( D @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
& ( B @ ( F @ ( C @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ) )
& ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( D @ ( c @ ( C @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) ) )
| ~ ( B @ ( A @ p ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: state] :
~ ( ? [B: bool @ ( state @ fun ) @ ( a @ fun ),C: bool @ ( state @ fun ) @ ( a @ fun )] :
( ! [D: state] :
( ( D @ ( sk1 @ q ) )
| ? [E: a] :
( ~ ( D @ ( E @ ( C @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
& ( A @ ( E @ ( B @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ) )
& ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( C @ ( c @ ( B @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) ) )
| ~ ( A @ ( sk1 @ p ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: bool @ ( state @ fun ) @ ( a @ fun ),B: bool @ ( state @ fun ) @ ( a @ fun )] :
@+[C: state] :
~ ( ( C @ ( sk1 @ q ) )
| ? [D: a] :
( ~ ( C @ ( D @ ( A @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
& ( sk2 @ ( D @ ( B @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: com > com > com] :
! [B: com,C: com] :
( ( C @ ( B @ semi ) @ ( C @ A ) )
= B ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: com > com > com] :
! [B: com,C: com] :
( ( C @ ( B @ semi ) @ ( B @ A ) )
= C ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( bool @ ( TA @ fun ) @ fun )] :
@+[C: TA] :
~ ! [D: bool @ ( TA @ fun )] :
( ( D @ ( TA @ finite_finite1 ) )
=> ( ~ ( D @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( D @ ( B @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( D @ ( C @ ( TA @ insert ) ) @ ( B @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( bool @ ( TA @ fun ) @ fun )] :
@+[C: bool @ ( TA @ fun )] :
~ ( ( C @ ( TA @ finite_finite1 ) )
=> ( ~ ( C @ ( B @ ( A @ ( TA @ sk6 ) ) @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( C @ ( B @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( C @ ( B @ ( A @ ( TA @ sk6 ) ) @ ( TA @ insert ) ) @ ( B @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( ^ [TA: $tType,A: bool @ ( TA @ fun )] :
@+[B: TA] :
~ ~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( ^ [TA: $tType,A: bool @ ( TA @ fun )] :
@+[B: bool @ ( TA @ fun )] :
? [C: TA] :
( ( B @ ( TA @ finite_finite1 ) )
& ( A
= ( B @ ( C @ ( TA @ insert ) ) ) ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( ^ [TA: $tType,A: bool @ ( TA @ fun )] :
@+[B: TA] :
( ( A @ ( TA @ sk12 ) @ ( TA @ finite_finite1 ) )
& ( A
= ( A @ ( TA @ sk12 ) @ ( B @ ( TA @ insert ) ) ) ) ) ) ) ).
thf(4,axiom,
! [A: bool] :
( ( A = fFalse )
| ( A = fTrue ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_T) ).
thf(140,plain,
! [A: bool] :
( ( A = fFalse )
| ( A = fTrue ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(141,plain,
! [A: bool] :
( ( A = fFalse )
| ( A = fTrue ) ),
inference(cnf,[status(esa)],[140]) ).
thf(142,plain,
! [A: bool] :
( ( A = fFalse )
| ( A = fTrue ) ),
inference(lifteq,[status(thm)],[141]) ).
thf(103,axiom,
fTrue @ pp,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_pp_2_1_U) ).
thf(544,plain,
fTrue @ pp,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[103]) ).
thf(20,axiom,
! [A: bool] :
( ~ ( A @ pp )
| ~ ( A @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fNot_1_1_U) ).
thf(208,plain,
! [A: bool] :
( ~ ( A @ pp )
| ~ ( A @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ pp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(209,plain,
! [A: bool] :
( ~ ( A @ pp )
| ~ ( A @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ pp ) ),
inference(cnf,[status(esa)],[208]) ).
thf(1755,plain,
! [A: bool] :
( ( ( fTrue @ pp )
!= ( A @ pp ) )
| ~ $true
| ~ ( A @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ pp ) ),
inference(paramod_ordered,[status(thm)],[544,209]) ).
thf(1756,plain,
! [A: bool] :
( ( ( fTrue @ pp )
!= ( A @ pp ) )
| ~ ( A @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ pp ) ),
inference(simp,[status(thm)],[1755]) ).
thf(1757,plain,
~ ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ pp ),
inference(pattern_uni,[status(thm)],[1756:[bind(A,$thf( fTrue ))]]) ).
thf(1789,plain,
( ( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ pp )
!= ( fTrue @ pp ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[544,1757]) ).
thf(1790,plain,
( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ pp )
!= ( fTrue @ pp ) ),
inference(simp,[status(thm)],[1789]) ).
thf(1796,plain,
( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) )
!= fTrue ),
inference(simp,[status(thm)],[1790]) ).
thf(1803,plain,
! [A: bool] :
( ( A
!= ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) ) )
| ( fTrue != fTrue )
| ( A = fFalse ) ),
inference(paramod_ordered,[status(thm)],[142,1796]) ).
thf(1804,plain,
! [A: bool] :
( ( A
!= ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) ) )
| ( A = fFalse ) ),
inference(simp,[status(thm)],[1803]) ).
thf(1805,plain,
( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) )
= fFalse ),
inference(pattern_uni,[status(thm)],[1804:[bind(A,$thf( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) ))]]) ).
thf(3,axiom,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( TA @ collect ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_Collect__def) ).
thf(137,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( TA @ collect ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(138,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( TA @ collect ) )
= A ),
inference(cnf,[status(esa)],[137]) ).
thf(139,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( TA @ collect ) )
= A ),
inference(lifteq,[status(thm)],[138]) ).
thf(122,axiom,
! [TA: $tType] :
( ( bool @ ( TA @ fun ) @ bot_bot )
= ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( TA @ collect ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_empty__def) ).
thf(614,plain,
! [TA: $tType] :
( ( bool @ ( TA @ fun ) @ bot_bot )
= ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( TA @ collect ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[122]) ).
thf(615,plain,
! [TA: $tType] :
( ( bool @ ( TA @ fun ) @ bot_bot )
= ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( TA @ collect ) ) ),
inference(cnf,[status(esa)],[614]) ).
thf(616,plain,
! [TA: $tType] :
( ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( TA @ collect ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(lifteq,[status(thm)],[615]) ).
thf(697,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( ( A @ ( TB @ collect ) )
!= ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( TB @ collect ) ) )
| ( A
= ( bool @ ( TB @ fun ) @ bot_bot ) ) ),
inference(paramod_ordered,[status(thm)],[139,616]) ).
thf(698,plain,
! [TB: $tType] :
( ( fFalse @ ( TB @ ( bool @ combk ) ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ),
inference(pattern_uni,[status(thm)],[697:[bind(A,$thf( fFalse @ ( TB @ ( bool @ combk ) ) ))]]) ).
thf(701,plain,
! [TA: $tType] :
( ( fFalse @ ( TA @ ( bool @ combk ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(simp,[status(thm)],[698]) ).
thf(1816,plain,
! [TA: $tType] :
( ( fFalse != fFalse )
| ( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ) ),
inference(paramod_ordered,[status(thm)],[1805,701]) ).
thf(1817,plain,
! [TA: $tType] :
( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(pattern_uni,[status(thm)],[1816:[]]) ).
thf(1935,plain,
! [TB: $tType] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) )
= ( fFalse @ ( TB @ ( bool @ combk ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1817,701]) ).
thf(1936,plain,
! [TB: $tType] :
( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) )
= ( fFalse @ ( TB @ ( bool @ combk ) ) ) ),
inference(pattern_uni,[status(thm)],[1935:[]]) ).
thf(2031,plain,
! [TA: $tType] :
( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) )
= ( fFalse @ ( TA @ ( bool @ combk ) ) ) ),
inference(simp,[status(thm)],[1936]) ).
thf(1753,plain,
! [A: bool] :
( ( ( fTrue @ pp )
!= ( A @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ pp ) )
| ~ ( A @ pp )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[544,209]) ).
thf(1754,plain,
! [A: bool] :
( ( ( fTrue @ pp )
!= ( A @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ pp ) )
| ~ ( A @ pp ) ),
inference(simp,[status(thm)],[1753]) ).
thf(1767,plain,
! [A: bool] :
( ( fTrue
!= ( A @ ( fNot @ ( bool @ ( bool @ aa ) ) ) ) )
| ~ ( A @ pp ) ),
inference(simp,[status(thm)],[1754]) ).
thf(32,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun ),C: TA] :
( ~ ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ~ ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( ( B @ ( C @ ( TA @ insert ) ) )
= ( A @ ( C @ ( TA @ insert ) ) ) )
<=> ( B = A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_insert__ident) ).
thf(249,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun ),C: TA] :
( ~ ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ~ ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( ( B = A )
=> ( ( B @ ( C @ ( TA @ insert ) ) )
= ( A @ ( C @ ( TA @ insert ) ) ) ) )
& ( ( ( B @ ( C @ ( TA @ insert ) ) )
= ( A @ ( C @ ( TA @ insert ) ) ) )
=> ( B = A ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(108,axiom,
! [TA: $tType,TB: $tType,TC: $tType,A: TA,B: TB @ ( TA @ fun ),C: TC @ ( TB @ fun ) @ ( TA @ fun )] :
( ( A @ ( B @ ( C @ ( TC @ ( TB @ ( TA @ combs ) ) ) ) @ ( TC @ ( TA @ aa ) ) ) )
= ( A @ ( B @ ( TB @ ( TA @ aa ) ) ) @ ( A @ ( C @ ( TC @ ( TB @ fun ) @ ( TA @ aa ) ) ) @ ( TC @ ( TB @ aa ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBS_1_1_U) ).
thf(555,plain,
! [TA: $tType,TB: $tType,TC: $tType,A: TA,B: TB @ ( TA @ fun ),C: TC @ ( TB @ fun ) @ ( TA @ fun )] :
( ( A @ ( B @ ( C @ ( TC @ ( TB @ ( TA @ combs ) ) ) ) @ ( TC @ ( TA @ aa ) ) ) )
= ( A @ ( B @ ( TB @ ( TA @ aa ) ) ) @ ( A @ ( C @ ( TC @ ( TB @ fun ) @ ( TA @ aa ) ) ) @ ( TC @ ( TB @ aa ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[108]) ).
thf(41,axiom,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ! [B: TA] :
~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
<=> ( A
= ( bool @ ( TA @ fun ) @ bot_bot ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_all__not__in__conv) ).
thf(282,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( ( A
= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ! [B: TA] :
~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) )
& ( ! [B: TA] :
~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( A
= ( bool @ ( TA @ fun ) @ bot_bot ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(283,plain,
! [TA: $tType,B: TA,A: bool @ ( TA @ fun )] :
( ( ~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ( A
!= ( bool @ ( TA @ fun ) @ bot_bot ) ) )
& ( ( A
= ( bool @ ( TA @ fun ) @ bot_bot ) )
| ( A @ ( A @ ( TA @ sk10 ) @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ),
inference(cnf,[status(esa)],[282]) ).
thf(285,plain,
! [TA: $tType,B: TA,A: bool @ ( TA @ fun )] :
( ~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ( A
!= ( bool @ ( TA @ fun ) @ bot_bot ) ) ),
inference(cnfConj,[status(thm)],[283]) ).
thf(287,plain,
! [TA: $tType,B: TA,A: bool @ ( TA @ fun )] :
( ~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ( A
!= ( bool @ ( TA @ fun ) @ bot_bot ) ) ),
inference(lifteq,[status(thm)],[285]) ).
thf(288,plain,
! [TA: $tType,A: TA] :
~ ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ),
inference(simp,[status(thm)],[287]) ).
thf(667,plain,
! [TA: $tType,A: TA] :
( ( ( fTrue @ pp )
!= ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[544,288]) ).
thf(668,plain,
! [TA: $tType,A: TA] :
( ( fTrue @ pp )
!= ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
inference(simp,[status(thm)],[667]) ).
thf(670,plain,
! [TA: $tType,A: TA] :
( fTrue
!= ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) ) ),
inference(simp,[status(thm)],[668]) ).
thf(884,plain,
! [TA: $tType,B: TA,A: bool] :
( ( A
!= ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) ) )
| ( fTrue != fTrue )
| ( A = fFalse ) ),
inference(paramod_ordered,[status(thm)],[142,670]) ).
thf(885,plain,
! [TA: $tType,B: TA,A: bool] :
( ( A
!= ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) ) )
| ( A = fFalse ) ),
inference(simp,[status(thm)],[884]) ).
thf(886,plain,
! [TA: $tType,A: TA] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
= fFalse ),
inference(pattern_uni,[status(thm)],[885:[bind(A,$thf( bool @ ( TA @ fun ) @ bot_bot @ ( F @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) )),bind(B,$thf( F ))]]) ).
thf(891,plain,
! [TA: $tType,A: TA] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
= fFalse ),
inference(simp,[status(thm)],[886]) ).
thf(1210,plain,
! [TA: $tType,TB: $tType,A: TA] :
( ( fFalse != fFalse )
| ( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) @ ( TB @ collect ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ) ),
inference(paramod_ordered,[status(thm)],[891,616]) ).
thf(1211,plain,
! [TA: $tType,TB: $tType,A: TA] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) @ ( TB @ collect ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ),
inference(pattern_uni,[status(thm)],[1210:[]]) ).
thf(97,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ? [C: bool @ ( TA @ fun )] :
( ~ ( C @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
& ( A
= ( C @ ( B @ ( TA @ insert ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_mk__disjoint__insert) ).
thf(523,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ? [C: bool @ ( TA @ fun )] :
( ~ ( C @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
& ( A
= ( C @ ( B @ ( TA @ insert ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[97]) ).
thf(50,axiom,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA] :
( ( A @ ( B @ ( C @ ( TA @ insert ) ) @ ( bool @ ( TA @ aa ) ) ) @ pp )
<=> ( ( A @ ( B @ ( bool @ ( TA @ aa ) ) ) @ pp )
| ( C = A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_insert__code) ).
thf(308,plain,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA] :
( ( ( ( A @ ( B @ ( bool @ ( TA @ aa ) ) ) @ pp )
| ( C = A ) )
=> ( A @ ( B @ ( C @ ( TA @ insert ) ) @ ( bool @ ( TA @ aa ) ) ) @ pp ) )
& ( ( A @ ( B @ ( C @ ( TA @ insert ) ) @ ( bool @ ( TA @ aa ) ) ) @ pp )
=> ( ( A @ ( B @ ( bool @ ( TA @ aa ) ) ) @ pp )
| ( C = A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(85,axiom,
! [TA: $tType,A: TA,B: TA,C: TA,D: TA] :
( ( ( bool @ ( TA @ fun ) @ bot_bot @ ( C @ ( TA @ insert ) ) @ ( D @ ( TA @ insert ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( TA @ insert ) ) ) )
<=> ( ( ( C = B )
& ( D = A ) )
| ( ( C = A )
& ( D = B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_doubleton__eq__iff) ).
thf(449,plain,
! [TA: $tType,A: TA,B: TA,C: TA,D: TA] :
( ( ( ( ( C = B )
& ( D = A ) )
| ( ( C = A )
& ( D = B ) ) )
=> ( ( bool @ ( TA @ fun ) @ bot_bot @ ( C @ ( TA @ insert ) ) @ ( D @ ( TA @ insert ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( TA @ insert ) ) ) ) )
& ( ( ( bool @ ( TA @ fun ) @ bot_bot @ ( C @ ( TA @ insert ) ) @ ( D @ ( TA @ insert ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( TA @ insert ) ) ) )
=> ( ( ( C = B )
& ( D = A ) )
| ( ( C = A )
& ( D = B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(82,axiom,
! [TA: $tType,A: TA @ hoare_28830079triple] :
~ ! [B: bool @ ( state @ fun ) @ ( TA @ fun ),C: com,D: bool @ ( state @ fun ) @ ( TA @ fun )] :
( A
!= ( D @ ( C @ ( B @ ( TA @ hoare_1841697145triple ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_triple_Oexhaust) ).
thf(440,plain,
! [TA: $tType,A: TA @ hoare_28830079triple] :
~ ! [B: bool @ ( state @ fun ) @ ( TA @ fun ),C: com,D: bool @ ( state @ fun ) @ ( TA @ fun )] :
( A
!= ( D @ ( C @ ( B @ ( TA @ hoare_1841697145triple ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(18,axiom,
! [TA: $tType,TB: $tType,A: TA,B: TA,C: TB @ ( TA @ fun ),D: bool @ ( TB @ fun ) @ ( TB @ fun )] :
( ( A @ ( B @ ( C @ ( D @ ( TA @ ( TB @ inv_imagep ) ) ) ) ) )
<=> ( A @ ( C @ ( TB @ ( TA @ aa ) ) ) @ ( B @ ( C @ ( TB @ ( TA @ aa ) ) ) @ ( D @ ( bool @ ( TB @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( TB @ aa ) ) ) @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_in__inv__imagep) ).
thf(202,plain,
! [TA: $tType,TB: $tType,A: TA,B: TA,C: TB @ ( TA @ fun ),D: bool @ ( TB @ fun ) @ ( TB @ fun )] :
( ( ( A @ ( C @ ( TB @ ( TA @ aa ) ) ) @ ( B @ ( C @ ( TB @ ( TA @ aa ) ) ) @ ( D @ ( bool @ ( TB @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( TB @ aa ) ) ) @ pp )
=> ( A @ ( B @ ( C @ ( D @ ( TA @ ( TB @ inv_imagep ) ) ) ) ) ) )
& ( ( A @ ( B @ ( C @ ( D @ ( TA @ ( TB @ inv_imagep ) ) ) ) ) )
=> ( A @ ( C @ ( TB @ ( TA @ aa ) ) ) @ ( B @ ( C @ ( TB @ ( TA @ aa ) ) ) @ ( D @ ( bool @ ( TB @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( TB @ aa ) ) ) @ pp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(33,axiom,
bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( q1 @ ( c @ ( p1 @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
thf(256,plain,
bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( q1 @ ( c @ ( p1 @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(705,plain,
( ( ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot )
!= ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot ) )
| ( fFalse @ ( a @ hoare_28830079triple @ ( bool @ combk ) ) @ ( q1 @ ( c @ ( p1 @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) ) ),
inference(paramod_ordered,[status(thm)],[701,256]) ).
thf(706,plain,
fFalse @ ( a @ hoare_28830079triple @ ( bool @ combk ) ) @ ( q1 @ ( c @ ( p1 @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ),
inference(pattern_uni,[status(thm)],[705:[]]) ).
thf(1854,plain,
( ( fFalse != fFalse )
| ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( a @ hoare_28830079triple @ ( bool @ combk ) ) @ ( q1 @ ( c @ ( p1 @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) ) ),
inference(paramod_ordered,[status(thm)],[1805,706]) ).
thf(1855,plain,
fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( a @ hoare_28830079triple @ ( bool @ combk ) ) @ ( q1 @ ( c @ ( p1 @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ),
inference(pattern_uni,[status(thm)],[1854:[]]) ).
thf(58,axiom,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( TA @ finite_finite1 ) )
<=> ( ? [B: bool @ ( TA @ fun ),C: TA] :
( ( B @ ( TA @ finite_finite1 ) )
& ( A
= ( B @ ( C @ ( TA @ insert ) ) ) ) )
| ( A
= ( bool @ ( TA @ fun ) @ bot_bot ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_finite_Osimps) ).
thf(346,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( ( ? [B: bool @ ( TA @ fun ),C: TA] :
( ( B @ ( TA @ finite_finite1 ) )
& ( A
= ( B @ ( C @ ( TA @ insert ) ) ) ) )
| ( A
= ( bool @ ( TA @ fun ) @ bot_bot ) ) )
=> ( A @ ( TA @ finite_finite1 ) ) )
& ( ( A @ ( TA @ finite_finite1 ) )
=> ( ? [B: bool @ ( TA @ fun ),C: TA] :
( ( B @ ( TA @ finite_finite1 ) )
& ( A
= ( B @ ( C @ ( TA @ insert ) ) ) ) )
| ( A
= ( bool @ ( TA @ fun ) @ bot_bot ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(347,plain,
! [TA: $tType,C: TA,B: bool @ ( TA @ fun ),A: bool @ ( TA @ fun )] :
( ( ( A @ ( TA @ finite_finite1 ) )
| ~ ( B @ ( TA @ finite_finite1 ) )
| ( A
!= ( B @ ( C @ ( TA @ insert ) ) ) ) )
& ( ( A @ ( TA @ finite_finite1 ) )
| ( A
!= ( bool @ ( TA @ fun ) @ bot_bot ) ) )
& ( ( A @ ( TA @ sk12 ) @ ( TA @ finite_finite1 ) )
| ( A
= ( bool @ ( TA @ fun ) @ bot_bot ) )
| ~ ( A @ ( TA @ finite_finite1 ) ) )
& ( ( A
= ( A @ ( TA @ sk12 ) @ ( A @ ( TA @ sk13 ) @ ( TA @ insert ) ) ) )
| ( A
= ( bool @ ( TA @ fun ) @ bot_bot ) )
| ~ ( A @ ( TA @ finite_finite1 ) ) ) ),
inference(cnf,[status(esa)],[346]) ).
thf(350,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( TA @ finite_finite1 ) )
| ( A
!= ( bool @ ( TA @ fun ) @ bot_bot ) ) ),
inference(cnfConj,[status(thm)],[347]) ).
thf(354,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( TA @ finite_finite1 ) )
| ( A
!= ( bool @ ( TA @ fun ) @ bot_bot ) ) ),
inference(lifteq,[status(thm)],[350]) ).
thf(355,plain,
! [TA: $tType] : ( bool @ ( TA @ fun ) @ bot_bot @ ( TA @ finite_finite1 ) ),
inference(simp,[status(thm)],[354]) ).
thf(711,plain,
! [TB: $tType] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( TB @ finite_finite1 ) ) ),
inference(paramod_ordered,[status(thm)],[701,355]) ).
thf(712,plain,
! [TB: $tType] : ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( TB @ finite_finite1 ) ),
inference(pattern_uni,[status(thm)],[711:[]]) ).
thf(719,plain,
! [TA: $tType] : ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( TA @ finite_finite1 ) ),
inference(simp,[status(thm)],[712]) ).
thf(1199,plain,
! [TA: $tType,TB: $tType,A: TA] :
( ( fFalse != fFalse )
| ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) @ ( TB @ finite_finite1 ) ) ),
inference(paramod_ordered,[status(thm)],[891,719]) ).
thf(1200,plain,
! [TA: $tType,TB: $tType,A: TA] : ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) @ ( TB @ finite_finite1 ) ),
inference(pattern_uni,[status(thm)],[1199:[]]) ).
thf(77,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun ),C: TA] :
( ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ~ ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_DiffD2) ).
thf(408,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun ),C: TA] :
( ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ~ ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(10,axiom,
! [TA: $tType] :
( ( TA @ finite_finite )
=> ! [A: bool @ ( TA @ fun )] : ( A @ ( TA @ finite_finite1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_finite) ).
thf(170,plain,
! [TA: $tType] :
( ( TA @ finite_finite )
=> ! [A: bool @ ( TA @ fun )] : ( A @ ( TA @ finite_finite1 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(1,conjecture,
! [A: a,B: state] :
( ? [C: bool @ ( state @ fun ) @ ( a @ fun ),D: bool @ ( state @ fun ) @ ( a @ fun )] :
( ! [E: state] :
( ( E @ ( A @ q ) )
| ? [F: a] :
( ~ ( E @ ( F @ ( D @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
& ( B @ ( F @ ( C @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ) )
& ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( D @ ( c @ ( C @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) ) )
| ~ ( B @ ( A @ p ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_2) ).
thf(2,negated_conjecture,
~ ! [A: a,B: state] :
( ? [C: bool @ ( state @ fun ) @ ( a @ fun ),D: bool @ ( state @ fun ) @ ( a @ fun )] :
( ! [E: state] :
( ( E @ ( A @ q ) )
| ? [F: a] :
( ~ ( E @ ( F @ ( D @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
& ( B @ ( F @ ( C @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ) )
& ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( D @ ( c @ ( C @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) ) )
| ~ ( B @ ( A @ p ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(132,plain,
~ ! [A: a,B: state] :
( ? [C: bool @ ( state @ fun ) @ ( a @ fun ),D: bool @ ( state @ fun ) @ ( a @ fun )] :
( ! [E: state] :
( ( E @ ( A @ q ) )
| ? [F: a] :
( ~ ( E @ ( F @ ( D @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
& ( B @ ( F @ ( C @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ) )
& ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( D @ ( c @ ( C @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) ) )
| ~ ( B @ ( A @ p ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(133,plain,
! [C: a,B: bool @ ( state @ fun ) @ ( a @ fun ),A: bool @ ( state @ fun ) @ ( a @ fun )] :
( ( ~ ( A @ ( B @ sk3 ) @ ( sk1 @ q ) )
| ~ ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( B @ ( c @ ( A @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) ) )
& ( ( A @ ( B @ sk3 ) @ ( C @ ( B @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
| ~ ( sk2 @ ( C @ ( A @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
| ~ ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( B @ ( c @ ( A @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) ) )
& ( sk2 @ ( sk1 @ p ) ) ),
inference(cnf,[status(esa)],[132]) ).
thf(136,plain,
! [B: bool @ ( state @ fun ) @ ( a @ fun ),A: bool @ ( state @ fun ) @ ( a @ fun )] :
( ~ ( A @ ( B @ sk3 ) @ ( sk1 @ q ) )
| ~ ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( B @ ( c @ ( A @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) ) ),
inference(cnfConj,[status(thm)],[133]) ).
thf(675,plain,
! [B: bool @ ( state @ fun ) @ ( a @ fun ),A: bool @ ( state @ fun ) @ ( a @ fun )] :
( ( ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( q1 @ ( c @ ( p1 @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) )
!= ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( B @ ( c @ ( A @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) ) )
| ~ ( A @ ( B @ sk3 ) @ ( sk1 @ q ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[256,136]) ).
thf(676,plain,
! [B: bool @ ( state @ fun ) @ ( a @ fun ),A: bool @ ( state @ fun ) @ ( a @ fun )] :
( ( ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( q1 @ ( c @ ( p1 @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) )
!= ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( B @ ( c @ ( A @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) ) )
| ~ ( A @ ( B @ sk3 ) @ ( sk1 @ q ) ) ),
inference(simp,[status(thm)],[675]) ).
thf(677,plain,
~ ( p1 @ ( q1 @ sk3 ) @ ( sk1 @ q ) ),
inference(pattern_uni,[status(thm)],[676:[bind(A,$thf( p1 )),bind(B,$thf( q1 ))]]) ).
thf(68,axiom,
! [TA: $tType,A: TA,B: TA] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( B = A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_singletonE) ).
thf(384,plain,
! [TA: $tType,A: TA,B: TA] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( B = A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(106,axiom,
! [TA: $tType,TB: $tType,A: TB,B: TA] :
( ( A @ ( B @ ( TB @ ( TA @ combk ) ) @ ( TA @ ( TB @ aa ) ) ) )
= B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBK_1_1_U) ).
thf(550,plain,
! [TA: $tType,TB: $tType,A: TB,B: TA] :
( ( A @ ( B @ ( TB @ ( TA @ combk ) ) @ ( TA @ ( TB @ aa ) ) ) )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[106]) ).
thf(57,axiom,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA @ ( bool @ ( TA @ fun ) @ fun ),D: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( C @ ( D @ ( TA @ finite_folding_one ) ) )
=> ( ( B @ ( TA @ finite_finite1 ) )
=> ( ( ( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
!= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ( ( B @ ( A @ ( TA @ insert ) ) @ ( C @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( A @ ( D @ ( TA @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) ) ) )
& ( ( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ( ( B @ ( A @ ( TA @ insert ) ) @ ( C @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
= A ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_folding__one_Oinsert__remove) ).
thf(340,plain,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA @ ( bool @ ( TA @ fun ) @ fun ),D: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( C @ ( D @ ( TA @ finite_folding_one ) ) )
=> ( ( B @ ( TA @ finite_finite1 ) )
=> ( ( ( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
!= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ( ( B @ ( A @ ( TA @ insert ) ) @ ( C @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( A @ ( D @ ( TA @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) ) ) )
& ( ( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ( ( B @ ( A @ ( TA @ insert ) ) @ ( C @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
= A ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(54,axiom,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( A @ ( B @ ( C @ ( TA @ finite_fold1Set ) ) ) )
=> ( B
!= ( bool @ ( TA @ fun ) @ bot_bot ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_fold1Set__nonempty) ).
thf(327,plain,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( A @ ( B @ ( C @ ( TA @ finite_fold1Set ) ) ) )
=> ( B
!= ( bool @ ( TA @ fun ) @ bot_bot ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(328,plain,
! [TA: $tType,C: TA @ ( TA @ fun ) @ ( TA @ fun ),B: bool @ ( TA @ fun ),A: TA] :
( ( B
!= ( bool @ ( TA @ fun ) @ bot_bot ) )
| ~ ( A @ ( B @ ( C @ ( TA @ finite_fold1Set ) ) ) ) ),
inference(cnf,[status(esa)],[327]) ).
thf(329,plain,
! [TA: $tType,C: TA @ ( TA @ fun ) @ ( TA @ fun ),B: bool @ ( TA @ fun ),A: TA] :
( ~ ( A @ ( B @ ( C @ ( TA @ finite_fold1Set ) ) ) )
| ( B
!= ( bool @ ( TA @ fun ) @ bot_bot ) ) ),
inference(lifteq,[status(thm)],[328]) ).
thf(330,plain,
! [TA: $tType,B: TA @ ( TA @ fun ) @ ( TA @ fun ),A: TA] :
~ ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ finite_fold1Set ) ) ) ),
inference(simp,[status(thm)],[329]) ).
thf(1340,plain,
! [TB: $tType,B: TB @ ( TB @ fun ) @ ( TB @ fun ),A: TB] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ~ ( A @ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( B @ ( TB @ finite_fold1Set ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[701,330]) ).
thf(1341,plain,
! [TB: $tType,B: TB @ ( TB @ fun ) @ ( TB @ fun ),A: TB] :
~ ( A @ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( B @ ( TB @ finite_fold1Set ) ) ) ),
inference(pattern_uni,[status(thm)],[1340:[]]) ).
thf(1344,plain,
! [TA: $tType,B: TA @ ( TA @ fun ) @ ( TA @ fun ),A: TA] :
~ ( A @ ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( B @ ( TA @ finite_fold1Set ) ) ) ),
inference(simp,[status(thm)],[1341]) ).
thf(1866,plain,
! [TA: $tType,B: TA @ ( TA @ fun ) @ ( TA @ fun ),A: TA] :
( ( fFalse != fFalse )
| ~ ( A @ ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( B @ ( TA @ finite_fold1Set ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1805,1344]) ).
thf(1867,plain,
! [TA: $tType,B: TA @ ( TA @ fun ) @ ( TA @ fun ),A: TA] :
~ ( A @ ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( B @ ( TA @ finite_fold1Set ) ) ) ),
inference(pattern_uni,[status(thm)],[1866:[]]) ).
thf(93,axiom,
! [TA: $tType,A: bool @ ( bool @ ( TA @ fun ) @ fun ),B: bool @ ( TA @ fun )] :
( ( B @ ( TA @ finite_finite1 ) )
=> ( ( B @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ! [C: TA,D: bool @ ( TA @ fun )] :
( ( D @ ( TA @ finite_finite1 ) )
=> ( ( D @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( D @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( bool @ ( TA @ fun ) @ bot_bot @ ( C @ ( TA @ insert ) ) @ ( D @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ) )
=> ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_finite__empty__induct) ).
thf(500,plain,
! [TA: $tType,A: bool @ ( bool @ ( TA @ fun ) @ fun ),B: bool @ ( TA @ fun )] :
( ( B @ ( TA @ finite_finite1 ) )
=> ( ( B @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ! [C: TA,D: bool @ ( TA @ fun )] :
( ( D @ ( TA @ finite_finite1 ) )
=> ( ( D @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( D @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( bool @ ( TA @ fun ) @ bot_bot @ ( C @ ( TA @ insert ) ) @ ( D @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ) )
=> ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).
thf(101,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( B @ ( TA @ insert ) ) )
!= ( bool @ ( TA @ fun ) @ bot_bot ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_insert__not__empty) ).
thf(538,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( B @ ( TA @ insert ) ) )
!= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[101]) ).
thf(6,axiom,
! [A: com,B: com,C: com,D: com] :
( ( ( C @ ( D @ semi ) )
= ( A @ ( B @ semi ) ) )
<=> ( ( C = A )
& ( D = B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_com_Osimps_I3_J) ).
thf(147,plain,
! [A: com,B: com,C: com,D: com] :
( ( ( ( C = A )
& ( D = B ) )
=> ( ( C @ ( D @ semi ) )
= ( A @ ( B @ semi ) ) ) )
& ( ( ( C @ ( D @ semi ) )
= ( A @ ( B @ semi ) ) )
=> ( ( C = A )
& ( D = B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(148,plain,
( ! [A: com,B: com,C: com,D: com] :
( ( ( C = A )
& ( D = B ) )
=> ( ( C @ ( D @ semi ) )
= ( A @ ( B @ semi ) ) ) )
& ! [A: com,B: com,C: com,D: com] :
( ( ( C @ ( D @ semi ) )
= ( A @ ( B @ semi ) ) )
=> ( ( C = A )
& ( D = B ) ) ) ),
inference(miniscope,[status(thm)],[147]) ).
thf(149,plain,
! [H: com,G: com,F: com,E: com,D: com,C: com,B: com,A: com] :
( ( ( ( G @ ( H @ semi ) )
= ( E @ ( F @ semi ) ) )
| ( G != E )
| ( H != F ) )
& ( ( C = A )
| ( ( C @ ( D @ semi ) )
!= ( A @ ( B @ semi ) ) ) )
& ( ( D = B )
| ( ( C @ ( D @ semi ) )
!= ( A @ ( B @ semi ) ) ) ) ),
inference(cnf,[status(esa)],[148]) ).
thf(150,plain,
! [D: com,C: com,B: com,A: com] :
( ( D = B )
| ( ( C @ ( D @ semi ) )
!= ( A @ ( B @ semi ) ) ) ),
inference(cnfConj,[status(thm)],[149]) ).
thf(153,plain,
! [D: com,C: com,B: com,A: com] :
( ( D = B )
| ( ( C @ ( D @ semi ) )
!= ( A @ ( B @ semi ) ) ) ),
inference(lifteq,[status(thm)],[150]) ).
thf(11,axiom,
! [TA: $tType,A: bool @ ( bool @ ( TA @ fun ) @ fun ),B: bool @ ( TA @ fun )] :
( ( B @ ( TA @ finite_finite1 ) )
=> ( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ! [C: TA,D: bool @ ( TA @ fun )] :
( ( D @ ( TA @ finite_finite1 ) )
=> ( ~ ( D @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( D @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( D @ ( C @ ( TA @ insert ) ) @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ) )
=> ( B @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_finite__induct) ).
thf(172,plain,
! [TA: $tType,A: bool @ ( bool @ ( TA @ fun ) @ fun ),B: bool @ ( TA @ fun )] :
( ( B @ ( TA @ finite_finite1 ) )
=> ( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ! [C: TA,D: bool @ ( TA @ fun )] :
( ( D @ ( TA @ finite_finite1 ) )
=> ( ~ ( D @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( D @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( D @ ( C @ ( TA @ insert ) ) @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ) )
=> ( B @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(173,plain,
! [TA: $tType,B: bool @ ( TA @ fun ),A: bool @ ( bool @ ( TA @ fun ) @ fun )] :
( ( ( B @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( A @ ( B @ ( TA @ sk7 ) ) @ ( A @ ( B @ ( TA @ sk6 ) ) @ ( TA @ insert ) ) @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( B @ ( TA @ finite_finite1 ) ) )
& ( ( B @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ( A @ ( B @ ( TA @ sk7 ) ) @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( B @ ( TA @ finite_finite1 ) ) )
& ( ( B @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( A @ ( B @ ( TA @ sk7 ) ) @ ( A @ ( B @ ( TA @ sk6 ) ) @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( B @ ( TA @ finite_finite1 ) ) )
& ( ( B @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ( A @ ( B @ ( TA @ sk7 ) ) @ ( TA @ finite_finite1 ) )
| ~ ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( B @ ( TA @ finite_finite1 ) ) ) ),
inference(cnf,[status(esa)],[172]) ).
thf(174,plain,
! [TA: $tType,B: bool @ ( TA @ fun ),A: bool @ ( bool @ ( TA @ fun ) @ fun )] :
( ( B @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ( A @ ( B @ ( TA @ sk7 ) ) @ ( TA @ finite_finite1 ) )
| ~ ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( B @ ( TA @ finite_finite1 ) ) ),
inference(cnfConj,[status(thm)],[173]) ).
thf(13,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
<=> ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_mem__def) ).
thf(183,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp )
=> ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) )
& ( ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(184,plain,
! [TA: $tType,B: TA,A: bool @ ( TA @ fun )] :
( ( ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp ) )
& ( ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp )
| ~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ),
inference(cnf,[status(esa)],[183]) ).
thf(185,plain,
! [TA: $tType,B: TA,A: bool @ ( TA @ fun )] :
( ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp )
| ~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
inference(cnfConj,[status(thm)],[184]) ).
thf(91,axiom,
! [TA: $tType,A: bool @ ( TA @ hoare_28830079triple @ fun )] : ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( A @ ( TA @ hoare_992312373derivs ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_empty) ).
thf(496,plain,
! [TA: $tType,A: bool @ ( TA @ hoare_28830079triple @ fun )] : ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( A @ ( TA @ hoare_992312373derivs ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(497,plain,
! [TA: $tType,A: bool @ ( TA @ hoare_28830079triple @ fun )] : ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( A @ ( TA @ hoare_992312373derivs ) ) ),
inference(cnf,[status(esa)],[496]) ).
thf(713,plain,
! [TB: $tType,A: bool @ ( TB @ hoare_28830079triple @ fun )] :
( ( ( bool @ ( TB @ hoare_28830079triple @ fun ) @ bot_bot )
!= ( bool @ ( TB @ hoare_28830079triple @ fun ) @ bot_bot ) )
| ( fFalse @ ( TB @ hoare_28830079triple @ ( bool @ combk ) ) @ ( A @ ( TB @ hoare_992312373derivs ) ) ) ),
inference(paramod_ordered,[status(thm)],[701,497]) ).
thf(714,plain,
! [TB: $tType,A: bool @ ( TB @ hoare_28830079triple @ fun )] : ( fFalse @ ( TB @ hoare_28830079triple @ ( bool @ combk ) ) @ ( A @ ( TB @ hoare_992312373derivs ) ) ),
inference(pattern_uni,[status(thm)],[713:[]]) ).
thf(720,plain,
! [TA: $tType,A: bool @ ( TA @ hoare_28830079triple @ fun )] : ( fFalse @ ( TA @ hoare_28830079triple @ ( bool @ combk ) ) @ ( A @ ( TA @ hoare_992312373derivs ) ) ),
inference(simp,[status(thm)],[714]) ).
thf(1903,plain,
! [TA: $tType,A: bool @ ( TA @ hoare_28830079triple @ fun )] :
( ( fFalse != fFalse )
| ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ hoare_28830079triple @ ( bool @ combk ) ) @ ( A @ ( TA @ hoare_992312373derivs ) ) ) ),
inference(paramod_ordered,[status(thm)],[1805,720]) ).
thf(1904,plain,
! [TA: $tType,A: bool @ ( TA @ hoare_28830079triple @ fun )] : ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ hoare_28830079triple @ ( bool @ combk ) ) @ ( A @ ( TA @ hoare_992312373derivs ) ) ),
inference(pattern_uni,[status(thm)],[1903:[]]) ).
thf(34,axiom,
! [A: bool,B: bool] :
( ( A @ ( B @ ( fdisj @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp )
| ~ ( B @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fdisj_1_1_U) ).
thf(257,plain,
! [A: bool,B: bool] :
( ( A @ ( B @ ( fdisj @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp )
| ~ ( B @ pp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(112,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( B @ ( TA @ insert ) ) @ ( TA @ finite_finite1 ) )
<=> ( A @ ( TA @ finite_finite1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_finite__insert) ).
thf(565,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( ( A @ ( TA @ finite_finite1 ) )
=> ( A @ ( B @ ( TA @ insert ) ) @ ( TA @ finite_finite1 ) ) )
& ( ( A @ ( B @ ( TA @ insert ) ) @ ( TA @ finite_finite1 ) )
=> ( A @ ( TA @ finite_finite1 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[112]) ).
thf(135,plain,
! [C: a,B: bool @ ( state @ fun ) @ ( a @ fun ),A: bool @ ( state @ fun ) @ ( a @ fun )] :
( ( A @ ( B @ sk3 ) @ ( C @ ( B @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
| ~ ( sk2 @ ( C @ ( A @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
| ~ ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( B @ ( c @ ( A @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) ) ),
inference(cnfConj,[status(thm)],[133]) ).
thf(672,plain,
! [C: a,B: bool @ ( state @ fun ) @ ( a @ fun ),A: bool @ ( state @ fun ) @ ( a @ fun )] :
( ( ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( q1 @ ( c @ ( p1 @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) )
!= ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( B @ ( c @ ( A @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) ) )
| ( A @ ( B @ sk3 ) @ ( C @ ( B @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
| ~ ( sk2 @ ( C @ ( A @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[256,135]) ).
thf(673,plain,
! [C: a,B: bool @ ( state @ fun ) @ ( a @ fun ),A: bool @ ( state @ fun ) @ ( a @ fun )] :
( ( ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( q1 @ ( c @ ( p1 @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) )
!= ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot @ ( B @ ( c @ ( A @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) ) )
| ( A @ ( B @ sk3 ) @ ( C @ ( B @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
| ~ ( sk2 @ ( C @ ( A @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ),
inference(simp,[status(thm)],[672]) ).
thf(674,plain,
! [A: a] :
( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
| ~ ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ),
inference(pattern_uni,[status(thm)],[673:[bind(A,$thf( p1 )),bind(B,$thf( q1 ))]]) ).
thf(678,plain,
! [A: a] :
( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
| ~ ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ),
inference(simp,[status(thm)],[674]) ).
thf(685,plain,
! [A: a] :
( ( ( fTrue @ pp )
!= ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) )
| ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[544,678]) ).
thf(686,plain,
! [A: a] :
( ( ( fTrue @ pp )
!= ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) )
| ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ),
inference(simp,[status(thm)],[685]) ).
thf(692,plain,
! [A: a] :
( ( fTrue
!= ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) ) )
| ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ),
inference(simp,[status(thm)],[686]) ).
thf(80,axiom,
~ ( fFalse @ pp ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_pp_1_1_U) ).
thf(432,plain,
~ ( fFalse @ pp ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(433,plain,
~ ( fFalse @ pp ),
inference(polarity_switch,[status(thm)],[432]) ).
thf(744,plain,
! [A: a] :
( ( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
!= ( fFalse @ pp ) )
| ~ $true
| ( fTrue
!= ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[692,433]) ).
thf(745,plain,
! [A: a] :
( ( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
!= ( fFalse @ pp ) )
| ( fTrue
!= ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) ) ) ),
inference(simp,[status(thm)],[744]) ).
thf(750,plain,
! [A: a] :
( ( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )
!= fFalse )
| ( fTrue
!= ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) ) ) ),
inference(simp,[status(thm)],[745]) ).
thf(898,plain,
! [B: a,A: bool] :
( ( A
!= ( sk2 @ ( B @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) ) )
| ( ( p1 @ ( q1 @ sk3 ) @ ( B @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )
!= fFalse )
| ( fTrue != fTrue )
| ( A = fFalse ) ),
inference(paramod_ordered,[status(thm)],[142,750]) ).
thf(899,plain,
! [B: a,A: bool] :
( ( A
!= ( sk2 @ ( B @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) ) )
| ( ( p1 @ ( q1 @ sk3 ) @ ( B @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )
!= fFalse )
| ( A = fFalse ) ),
inference(simp,[status(thm)],[898]) ).
thf(900,plain,
! [A: a] :
( ( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )
!= fFalse )
| ( ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )
= fFalse ) ),
inference(pattern_uni,[status(thm)],[899:[bind(A,$thf( sk2 @ ( F @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )),bind(B,$thf( F ))]]) ).
thf(907,plain,
! [A: a] :
( ( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )
!= fFalse )
| ( ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )
= fFalse ) ),
inference(simp,[status(thm)],[900]) ).
thf(1365,plain,
! [TA: $tType,A: a] :
( ( fFalse != fFalse )
| ( ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( TA @ collect ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) )
| ( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )
!= fFalse ) ),
inference(paramod_ordered,[status(thm)],[907,616]) ).
thf(1366,plain,
! [TA: $tType,A: a] :
( ( ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( TA @ collect ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) )
| ( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )
!= fFalse ) ),
inference(pattern_uni,[status(thm)],[1365:[]]) ).
thf(70,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA @ ( bool @ ( TA @ fun ) @ fun ),C: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( B @ ( C @ ( TA @ finite_folding_one ) ) )
=> ( ( A @ ( TA @ finite_finite1 ) )
=> ( ( A
!= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ( ! [D: TA,E: TA] : ( bool @ ( TA @ fun ) @ bot_bot @ ( E @ ( TA @ insert ) ) @ ( D @ ( TA @ insert ) ) @ ( E @ ( D @ ( C @ ( TA @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( A @ ( A @ ( B @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_folding__one_Oclosed) ).
thf(389,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA @ ( bool @ ( TA @ fun ) @ fun ),C: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( B @ ( C @ ( TA @ finite_folding_one ) ) )
=> ( ( A @ ( TA @ finite_finite1 ) )
=> ( ( A
!= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ( ! [D: TA,E: TA] : ( bool @ ( TA @ fun ) @ bot_bot @ ( E @ ( TA @ insert ) ) @ ( D @ ( TA @ insert ) ) @ ( E @ ( D @ ( C @ ( TA @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( A @ ( A @ ( B @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(124,axiom,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA] :
( ( ~ ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( C = A ) )
=> ( B @ ( A @ ( TA @ insert ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_insertCI) ).
thf(619,plain,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA] :
( ( ~ ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( C = A ) )
=> ( B @ ( A @ ( TA @ insert ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[124]) ).
thf(130,axiom,
! [TA: $tType,TB: $tType,A: bool @ ( state @ fun ) @ ( TA @ fun ),B: com,C: bool @ ( state @ fun ) @ ( TA @ fun ),D: TB @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ fun ) @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ fun )] :
( ( A @ ( B @ ( C @ ( TA @ hoare_1841697145triple ) ) ) @ ( D @ ( TB @ ( TA @ hoare_376461865e_case ) ) ) )
= ( A @ ( B @ ( C @ ( D @ ( TB @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ fun ) @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ aa ) ) ) @ ( TB @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ fun ) @ ( com @ aa ) ) ) @ ( TB @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ aa ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_triple_Osimps_I2_J) ).
thf(638,plain,
! [TA: $tType,TB: $tType,A: bool @ ( state @ fun ) @ ( TA @ fun ),B: com,C: bool @ ( state @ fun ) @ ( TA @ fun ),D: TB @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ fun ) @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ fun )] :
( ( A @ ( B @ ( C @ ( TA @ hoare_1841697145triple ) ) ) @ ( D @ ( TB @ ( TA @ hoare_376461865e_case ) ) ) )
= ( A @ ( B @ ( C @ ( D @ ( TB @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ fun ) @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ aa ) ) ) @ ( TB @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ fun ) @ ( com @ aa ) ) ) @ ( TB @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ aa ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[130]) ).
thf(14,axiom,
! [TA: $tType,A: TA,B: TA,C: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( C @ ( TA @ finite_fold1Set ) ) ) )
<=> ( B = A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_48_fold1Set__sing) ).
thf(187,plain,
! [TA: $tType,A: TA,B: TA,C: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( ( B = A )
=> ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( C @ ( TA @ finite_fold1Set ) ) ) ) )
& ( ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( C @ ( TA @ finite_fold1Set ) ) ) )
=> ( B = A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(188,plain,
! [TA: $tType,C: TA @ ( TA @ fun ) @ ( TA @ fun ),B: TA,A: TA] :
( ( ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( C @ ( TA @ finite_fold1Set ) ) ) )
| ( B != A ) )
& ( ( B = A )
| ~ ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( C @ ( TA @ finite_fold1Set ) ) ) ) ) ),
inference(cnf,[status(esa)],[187]) ).
thf(189,plain,
! [TA: $tType,C: TA @ ( TA @ fun ) @ ( TA @ fun ),B: TA,A: TA] :
( ( B = A )
| ~ ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( C @ ( TA @ finite_fold1Set ) ) ) ) ),
inference(cnfConj,[status(thm)],[188]) ).
thf(191,plain,
! [TA: $tType,C: TA @ ( TA @ fun ) @ ( TA @ fun ),B: TA,A: TA] :
( ~ ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( C @ ( TA @ finite_fold1Set ) ) ) )
| ( B = A ) ),
inference(lifteq,[status(thm)],[189]) ).
thf(134,plain,
sk2 @ ( sk1 @ p ),
inference(cnfConj,[status(thm)],[133]) ).
thf(9673,plain,
! [C: a @ ( a @ fun ) @ ( a @ fun ),B: a,A: a] :
( ( B != sk1 )
| ( sk2 @ ( A @ p ) )
| ~ ( A @ ( bool @ ( a @ fun ) @ bot_bot @ ( B @ ( a @ insert ) ) @ ( C @ ( a @ finite_fold1Set ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[191,134]) ).
thf(9674,plain,
! [B: a @ ( a @ fun ) @ ( a @ fun ),A: a] :
( ( sk2 @ ( A @ p ) )
| ~ ( A @ ( bool @ ( a @ fun ) @ bot_bot @ ( sk1 @ ( a @ insert ) ) @ ( B @ ( a @ finite_fold1Set ) ) ) ) ),
inference(pattern_uni,[status(thm)],[9673:[bind(A,$thf( A )),bind(B,$thf( sk1 ))]]) ).
thf(11609,plain,
! [B: a @ ( a @ fun ) @ ( a @ fun ),A: a] :
( ( sk2 @ ( A @ p ) )
| ~ ( A @ ( bool @ ( a @ fun ) @ bot_bot @ ( sk1 @ ( a @ insert ) ) @ ( B @ ( a @ finite_fold1Set ) ) ) ) ),
inference(simp,[status(thm)],[9674]) ).
thf(782,plain,
! [B: a,A: bool] :
( ( A
!= ( sk2 @ ( B @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) ) )
| ( fTrue != fTrue )
| ( p1 @ ( q1 @ sk3 ) @ ( B @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
| ( A = fFalse ) ),
inference(paramod_ordered,[status(thm)],[142,692]) ).
thf(783,plain,
! [B: a,A: bool] :
( ( A
!= ( sk2 @ ( B @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) ) )
| ( p1 @ ( q1 @ sk3 ) @ ( B @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
| ( A = fFalse ) ),
inference(simp,[status(thm)],[782]) ).
thf(784,plain,
! [A: a] :
( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
| ( ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )
= fFalse ) ),
inference(pattern_uni,[status(thm)],[783:[bind(A,$thf( sk2 @ ( F @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )),bind(B,$thf( F ))]]) ).
thf(803,plain,
! [A: a] :
( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
| ( ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )
= fFalse ) ),
inference(simp,[status(thm)],[784]) ).
thf(1114,plain,
! [TA: $tType,A: a] :
( ( fFalse != fFalse )
| ( ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) )
| ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ),
inference(paramod_ordered,[status(thm)],[803,701]) ).
thf(1115,plain,
! [TA: $tType,A: a] :
( ( ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) )
| ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ),
inference(pattern_uni,[status(thm)],[1114:[]]) ).
thf(42,axiom,
! [A: bool,B: bool] :
( ( A @ pp )
| ~ ( B @ pp )
| ~ ( A @ ( B @ ( fimplies @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fimplies_3_1_U) ).
thf(289,plain,
! [A: bool,B: bool] :
( ( A @ pp )
| ~ ( B @ pp )
| ~ ( A @ ( B @ ( fimplies @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(1814,plain,
! [TA: $tType] :
( ( fFalse != fFalse )
| ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( TA @ finite_finite1 ) ) ),
inference(paramod_ordered,[status(thm)],[1805,719]) ).
thf(1815,plain,
! [TA: $tType] : ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( TA @ finite_finite1 ) ),
inference(pattern_uni,[status(thm)],[1814:[]]) ).
thf(72,axiom,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_empty__Diff) ).
thf(395,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(396,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(cnf,[status(esa)],[395]) ).
thf(397,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(lifteq,[status(thm)],[396]) ).
thf(737,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ( ( A @ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( bool @ ( TB @ fun ) @ minus_minus ) ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ) ),
inference(paramod_ordered,[status(thm)],[701,397]) ).
thf(738,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( A @ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( bool @ ( TB @ fun ) @ minus_minus ) ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ),
inference(pattern_uni,[status(thm)],[737:[]]) ).
thf(739,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(simp,[status(thm)],[738]) ).
thf(707,plain,
! [TB: $tType] :
( ( ( fFalse @ ( TB @ ( bool @ combk ) ) )
!= ( fFalse @ ( TB @ ( bool @ combk ) ) ) )
| ( ( bool @ ( TB @ fun ) @ bot_bot @ ( TB @ collect ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ) ),
inference(paramod_ordered,[status(thm)],[701,616]) ).
thf(708,plain,
! [TB: $tType] :
( ( bool @ ( TB @ fun ) @ bot_bot @ ( TB @ collect ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ),
inference(pattern_uni,[status(thm)],[707:[]]) ).
thf(718,plain,
! [TA: $tType] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( TA @ collect ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(simp,[status(thm)],[708]) ).
thf(841,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ( ( A @ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( bool @ ( TB @ fun ) @ minus_minus ) ) @ ( TB @ collect ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ) ),
inference(paramod_ordered,[status(thm)],[739,718]) ).
thf(842,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( A @ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( bool @ ( TB @ fun ) @ minus_minus ) ) @ ( TB @ collect ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ),
inference(pattern_uni,[status(thm)],[841:[]]) ).
thf(852,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ collect ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(simp,[status(thm)],[842]) ).
thf(1846,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( fFalse != fFalse )
| ( ( A @ ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ collect ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ) ),
inference(paramod_ordered,[status(thm)],[1805,852]) ).
thf(1847,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ collect ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(pattern_uni,[status(thm)],[1846:[]]) ).
thf(51,axiom,
! [A: bool,B: bool] :
( ( B @ ( A @ ( fimplies @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp )
| ~ ( B @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fimplies_2_1_U) ).
thf(316,plain,
! [A: bool,B: bool] :
( ( B @ ( A @ ( fimplies @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp )
| ~ ( B @ pp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(1361,plain,
! [TA: $tType,A: a] :
( ( fFalse != fFalse )
| ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( TA @ finite_finite1 ) )
| ( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )
!= fFalse ) ),
inference(paramod_ordered,[status(thm)],[907,719]) ).
thf(1362,plain,
! [TA: $tType,A: a] :
( ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( TA @ finite_finite1 ) )
| ( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )
!= fFalse ) ),
inference(pattern_uni,[status(thm)],[1361:[]]) ).
thf(1926,plain,
! [TB: $tType,A: TB] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ~ ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) @ ( A @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) @ pp ) ),
inference(paramod_ordered,[status(thm)],[1817,288]) ).
thf(1927,plain,
! [TB: $tType,A: TB] :
~ ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) @ ( A @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) @ pp ),
inference(pattern_uni,[status(thm)],[1926:[]]) ).
thf(2027,plain,
! [TA: $tType,A: TA] :
~ ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ),
inference(simp,[status(thm)],[1927]) ).
thf(83,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA,C: TA] :
( ( A @ ( B @ ( TA @ insert ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( C != B )
=> ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_insertE) ).
thf(443,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA,C: TA] :
( ( A @ ( B @ ( TA @ insert ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( C != B )
=> ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(53,axiom,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA @ ( bool @ ( TA @ fun ) @ fun ),D: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( C @ ( D @ ( TA @ finite_folding_one ) ) )
=> ( ( B @ ( TA @ finite_finite1 ) )
=> ( ( B @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( ( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
!= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ( ( B @ ( C @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( A @ ( D @ ( TA @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) ) ) )
& ( ( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ( ( B @ ( C @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
= A ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_folding__one_Oremove) ).
thf(321,plain,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA @ ( bool @ ( TA @ fun ) @ fun ),D: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( C @ ( D @ ( TA @ finite_folding_one ) ) )
=> ( ( B @ ( TA @ finite_finite1 ) )
=> ( ( B @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( ( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
!= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ( ( B @ ( C @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( A @ ( D @ ( TA @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) ) ) )
& ( ( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ( ( B @ ( C @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
= A ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(66,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun ),C: TA] :
( ( ~ ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( B @ ( A @ ( C @ ( TA @ insert ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( B @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ insert ) ) ) ) )
& ( ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( B @ ( A @ ( C @ ( TA @ insert ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( B @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_insert__Diff__if) ).
thf(376,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun ),C: TA] :
( ( ~ ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( B @ ( A @ ( C @ ( TA @ insert ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( B @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ insert ) ) ) ) )
& ( ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( B @ ( A @ ( C @ ( TA @ insert ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( B @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(186,plain,
! [TA: $tType,B: TA,A: bool @ ( TA @ fun )] :
( ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp ) ),
inference(cnfConj,[status(thm)],[184]) ).
thf(7763,plain,
! [TA: $tType,TB: $tType,C: TB,B: TA,A: bool @ ( TA @ fun )] :
( ( ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
!= ( bool @ ( TB @ fun ) @ bot_bot @ ( C @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) @ pp ) )
| ~ $true
| ~ ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp ) ),
inference(paramod_ordered,[status(thm)],[186,288]) ).
thf(7764,plain,
! [TA: $tType,TB: $tType,C: TB,B: TA,A: bool @ ( TA @ fun )] :
( ( ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
!= ( bool @ ( TB @ fun ) @ bot_bot @ ( C @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) @ pp ) )
| ~ ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp ) ),
inference(simp,[status(thm)],[7763]) ).
thf(7765,plain,
! [TB: $tType,A: TB] :
~ ( A @ ( bool @ ( TB @ fun ) @ bot_bot @ ( bool @ ( TB @ aa ) ) ) @ pp ),
inference(pattern_uni,[status(thm)],[7764:[bind(A,$thf( bool @ ( TB @ fun ) @ bot_bot )),bind(B,$thf( B )),bind(C,$thf( B )),bind_type(TA,$thf( TB ))]]) ).
thf(7904,plain,
! [TA: $tType,A: TA] :
~ ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ aa ) ) ) @ pp ),
inference(simp,[status(thm)],[7765]) ).
thf(7940,plain,
! [TB: $tType,A: TB] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ~ ( A @ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( bool @ ( TB @ aa ) ) ) @ pp ) ),
inference(paramod_ordered,[status(thm)],[701,7904]) ).
thf(7941,plain,
! [TB: $tType,A: TB] :
~ ( A @ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( bool @ ( TB @ aa ) ) ) @ pp ),
inference(pattern_uni,[status(thm)],[7940:[]]) ).
thf(7986,plain,
! [TA: $tType,A: TA] :
~ ( A @ ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( bool @ ( TA @ aa ) ) ) @ pp ),
inference(simp,[status(thm)],[7941]) ).
thf(825,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ( ( A @ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( bool @ ( TB @ fun ) @ minus_minus ) ) )
= ( fFalse @ ( TB @ ( bool @ combk ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[739,701]) ).
thf(826,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( A @ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( bool @ ( TB @ fun ) @ minus_minus ) ) )
= ( fFalse @ ( TB @ ( bool @ combk ) ) ) ),
inference(pattern_uni,[status(thm)],[825:[]]) ).
thf(851,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( fFalse @ ( TA @ ( bool @ combk ) ) ) ),
inference(simp,[status(thm)],[826]) ).
thf(913,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( ( fFalse @ ( TB @ ( bool @ combk ) ) )
!= ( fFalse @ ( TB @ ( bool @ combk ) ) ) )
| ( ( A @ ( bool @ ( TB @ fun ) @ bot_bot @ ( bool @ ( TB @ fun ) @ minus_minus ) ) )
= ( fFalse @ ( TB @ ( bool @ combk ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[701,851]) ).
thf(914,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( A @ ( bool @ ( TB @ fun ) @ bot_bot @ ( bool @ ( TB @ fun ) @ minus_minus ) ) )
= ( fFalse @ ( TB @ ( bool @ combk ) ) ) ),
inference(pattern_uni,[status(thm)],[913:[]]) ).
thf(926,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( fFalse @ ( TA @ ( bool @ combk ) ) ) ),
inference(simp,[status(thm)],[914]) ).
thf(1857,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( fFalse != fFalse )
| ( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) )
= ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ fun ) @ minus_minus ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1805,926]) ).
thf(1858,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) )
= ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ fun ) @ minus_minus ) ) ) ),
inference(pattern_uni,[status(thm)],[1857:[]]) ).
thf(44,axiom,
! [TA: $tType,A: TA] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( TA @ the_elem ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_the__elem__eq) ).
thf(293,plain,
! [TA: $tType,A: TA] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( TA @ the_elem ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(79,axiom,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun )] :
( ( B
= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ~ ( B @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_equals0D) ).
thf(428,plain,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun )] :
( ( B
= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ~ ( B @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(19,axiom,
! [A: bool,B: bool] :
( ( A @ ( B @ ( fconj @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp )
| ~ ( A @ pp )
| ~ ( B @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fconj_1_1_U) ).
thf(206,plain,
! [A: bool,B: bool] :
( ( A @ ( B @ ( fconj @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp )
| ~ ( A @ pp )
| ~ ( B @ pp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(1201,plain,
! [TA: $tType,TB: $tType,A: TA] :
( ( fFalse != fFalse )
| ( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ) ),
inference(paramod_ordered,[status(thm)],[891,701]) ).
thf(1202,plain,
! [TA: $tType,TB: $tType,A: TA] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ),
inference(pattern_uni,[status(thm)],[1201:[]]) ).
thf(1610,plain,
! [TA: $tType,TC: $tType,A: TA] :
( ( ( bool @ ( TC @ fun ) @ bot_bot )
!= ( bool @ ( TC @ fun ) @ bot_bot ) )
| ( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( TC @ ( bool @ combk ) ) )
= ( fFalse @ ( TC @ ( bool @ combk ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1202,701]) ).
thf(1611,plain,
! [TA: $tType,TC: $tType,A: TA] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( TC @ ( bool @ combk ) ) )
= ( fFalse @ ( TC @ ( bool @ combk ) ) ) ),
inference(pattern_uni,[status(thm)],[1610:[]]) ).
thf(1697,plain,
! [TA: $tType,TB: $tType,A: TA] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) )
= ( fFalse @ ( TB @ ( bool @ combk ) ) ) ),
inference(simp,[status(thm)],[1611]) ).
thf(37,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( B @ ( TA @ insert ) ) )
= A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_insert__Diff) ).
thf(265,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( B @ ( TA @ insert ) ) )
= A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(49,axiom,
bool @ finite_finite,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_HOL_Obool___Finite__Set_Ofinite) ).
thf(307,plain,
bool @ finite_finite,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(703,plain,
! [TB: $tType,A: TB] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ~ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( A @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) @ pp ) ),
inference(paramod_ordered,[status(thm)],[701,288]) ).
thf(704,plain,
! [TB: $tType,A: TB] :
~ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( A @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) @ pp ),
inference(pattern_uni,[status(thm)],[703:[]]) ).
thf(717,plain,
! [TA: $tType,A: TA] :
~ ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ),
inference(simp,[status(thm)],[704]) ).
thf(1063,plain,
! [TB: $tType,B: TB,A: bool @ ( TB @ fun )] :
( ( ( fFalse @ ( TB @ ( bool @ combk ) ) )
!= ( fFalse @ ( TB @ ( bool @ combk ) ) ) )
| ~ ( A @ ( bool @ ( TB @ fun ) @ bot_bot @ ( bool @ ( TB @ fun ) @ minus_minus ) ) @ ( B @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) @ pp ) ),
inference(paramod_ordered,[status(thm)],[926,717]) ).
thf(1064,plain,
! [TB: $tType,B: TB,A: bool @ ( TB @ fun )] :
~ ( A @ ( bool @ ( TB @ fun ) @ bot_bot @ ( bool @ ( TB @ fun ) @ minus_minus ) ) @ ( B @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) @ pp ),
inference(pattern_uni,[status(thm)],[1063:[]]) ).
thf(1074,plain,
! [TA: $tType,B: TA,A: bool @ ( TA @ fun )] :
~ ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ),
inference(simp,[status(thm)],[1064]) ).
thf(27,axiom,
! [A: bool,B: bool] :
( ( B @ pp )
| ~ ( A @ ( B @ ( fconj @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fconj_2_1_U) ).
thf(233,plain,
! [A: bool,B: bool] :
( ( B @ pp )
| ~ ( A @ ( B @ ( fconj @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(39,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ~ ! [C: bool @ ( TA @ fun )] :
( ( A
= ( C @ ( B @ ( TA @ insert ) ) ) )
=> ( C @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_Set_Oset__insert) ).
thf(270,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ~ ! [C: bool @ ( TA @ fun )] :
( ( A
= ( C @ ( B @ ( TA @ insert ) ) ) )
=> ( C @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(6989,plain,
! [TA: $tType,B: TA,A: bool @ ( TA @ fun )] :
( ( ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp )
!= ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ pp ) )
| ~ $true
| ~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
inference(paramod_ordered,[status(thm)],[185,1757]) ).
thf(6990,plain,
! [TA: $tType,B: TA,A: bool @ ( TA @ fun )] :
( ( ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp )
!= ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ pp ) )
| ~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
inference(simp,[status(thm)],[6989]) ).
thf(6991,plain,
~ ( fNot @ ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ fun ) @ aa ) ) ) @ pp ),
inference(pattern_uni,[status(thm)],[6990:[bind(A,$thf( fNot )),bind(B,$thf( fTrue )),bind_type(TA,$thf( bool ))]]) ).
thf(7069,plain,
( ( ( fNot @ ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ fun ) @ aa ) ) ) @ pp )
!= ( fTrue @ pp ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[544,6991]) ).
thf(7070,plain,
( ( fNot @ ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ fun ) @ aa ) ) ) @ pp )
!= ( fTrue @ pp ) ),
inference(simp,[status(thm)],[7069]) ).
thf(7078,plain,
( ( fNot @ ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ fun ) @ aa ) ) ) )
!= fTrue ),
inference(simp,[status(thm)],[7070]) ).
thf(56,axiom,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( ( bool @ ( TA @ fun ) @ bot_bot )
= ( A @ ( TA @ collect ) ) )
<=> ! [B: TA] :
~ ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_empty__Collect__eq) ).
thf(334,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( ! [B: TA] :
~ ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp )
=> ( ( bool @ ( TA @ fun ) @ bot_bot )
= ( A @ ( TA @ collect ) ) ) )
& ( ( ( bool @ ( TA @ fun ) @ bot_bot )
= ( A @ ( TA @ collect ) ) )
=> ! [B: TA] :
~ ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(47,axiom,
! [TA: $tType,A: TA,B: TA @ ( bool @ ( TA @ fun ) @ fun ),C: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( B @ ( C @ ( TA @ finite_folding_one ) ) )
=> ( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
= A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_folding__one_Osingleton) ).
thf(302,plain,
! [TA: $tType,A: TA,B: TA @ ( bool @ ( TA @ fun ) @ fun ),C: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( B @ ( C @ ( TA @ finite_folding_one ) ) )
=> ( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
= A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(71,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( A @ ( B @ ( TA @ insert ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_Diff__insert__absorb) ).
thf(392,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( A @ ( B @ ( TA @ insert ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(127,axiom,
! [TA: $tType,A: TA] :
~ ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_emptyE) ).
thf(630,plain,
! [TA: $tType,A: TA] :
~ ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[127]) ).
thf(8,axiom,
! [TA: $tType,A: TA @ ( nat @ ( state @ fun ) @ fun ) @ ( pname @ fun ) @ ( vname @ fun ),B: TA @ ( pname @ fun ),C: TA @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ fun ),D: TA @ ( com @ fun ) @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ fun ),E: TA @ ( com @ fun ) @ ( com @ fun ),F: TA @ ( com @ fun ) @ ( nat @ ( state @ fun ) @ fun ) @ ( loc @ fun ),G: TA @ ( nat @ ( state @ fun ) @ fun ) @ ( vname @ fun ),H: TA] :
( ( skip @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ ( G @ ( H @ ( TA @ com_case ) ) ) ) ) ) ) ) ) )
= H ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_com_Osimps_I64_J) ).
thf(163,plain,
! [TA: $tType,A: TA @ ( nat @ ( state @ fun ) @ fun ) @ ( pname @ fun ) @ ( vname @ fun ),B: TA @ ( pname @ fun ),C: TA @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ fun ),D: TA @ ( com @ fun ) @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ fun ),E: TA @ ( com @ fun ) @ ( com @ fun ),F: TA @ ( com @ fun ) @ ( nat @ ( state @ fun ) @ fun ) @ ( loc @ fun ),G: TA @ ( nat @ ( state @ fun ) @ fun ) @ ( vname @ fun ),H: TA] :
( ( skip @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ ( G @ ( H @ ( TA @ com_case ) ) ) ) ) ) ) ) ) )
= H ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(164,plain,
! [TA: $tType,H: TA,G: TA @ ( nat @ ( state @ fun ) @ fun ) @ ( vname @ fun ),F: TA @ ( com @ fun ) @ ( nat @ ( state @ fun ) @ fun ) @ ( loc @ fun ),E: TA @ ( com @ fun ) @ ( com @ fun ),D: TA @ ( com @ fun ) @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ fun ),C: TA @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ fun ),B: TA @ ( pname @ fun ),A: TA @ ( nat @ ( state @ fun ) @ fun ) @ ( pname @ fun ) @ ( vname @ fun )] :
( ( skip @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ ( G @ ( H @ ( TA @ com_case ) ) ) ) ) ) ) ) ) )
= H ),
inference(cnf,[status(esa)],[163]) ).
thf(165,plain,
! [TA: $tType,H: TA,G: TA @ ( nat @ ( state @ fun ) @ fun ) @ ( vname @ fun ),F: TA @ ( com @ fun ) @ ( nat @ ( state @ fun ) @ fun ) @ ( loc @ fun ),E: TA @ ( com @ fun ) @ ( com @ fun ),D: TA @ ( com @ fun ) @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ fun ),C: TA @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ fun ),B: TA @ ( pname @ fun ),A: TA @ ( nat @ ( state @ fun ) @ fun ) @ ( pname @ fun ) @ ( vname @ fun )] :
( ( skip @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ ( G @ ( H @ ( TA @ com_case ) ) ) ) ) ) ) ) ) )
= H ),
inference(lifteq,[status(thm)],[164]) ).
thf(1122,plain,
! [TA: $tType,A: a] :
( ( fFalse != fFalse )
| ( ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( TA @ collect ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) )
| ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ),
inference(paramod_ordered,[status(thm)],[803,616]) ).
thf(1123,plain,
! [TA: $tType,A: a] :
( ( ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( TA @ collect ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) )
| ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ),
inference(pattern_uni,[status(thm)],[1122:[]]) ).
thf(831,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ( A @ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( bool @ ( TB @ fun ) @ minus_minus ) ) @ ( TB @ finite_finite1 ) ) ),
inference(paramod_ordered,[status(thm)],[739,355]) ).
thf(832,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] : ( A @ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( bool @ ( TB @ fun ) @ minus_minus ) ) @ ( TB @ finite_finite1 ) ),
inference(pattern_uni,[status(thm)],[831:[]]) ).
thf(847,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] : ( A @ ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ finite_finite1 ) ),
inference(simp,[status(thm)],[832]) ).
thf(856,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( ( fFalse @ ( TB @ ( bool @ combk ) ) )
!= ( fFalse @ ( TB @ ( bool @ combk ) ) ) )
| ( A @ ( bool @ ( TB @ fun ) @ bot_bot @ ( bool @ ( TB @ fun ) @ minus_minus ) ) @ ( TB @ finite_finite1 ) ) ),
inference(paramod_ordered,[status(thm)],[701,847]) ).
thf(857,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] : ( A @ ( bool @ ( TB @ fun ) @ bot_bot @ ( bool @ ( TB @ fun ) @ minus_minus ) ) @ ( TB @ finite_finite1 ) ),
inference(pattern_uni,[status(thm)],[856:[]]) ).
thf(862,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] : ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ finite_finite1 ) ),
inference(simp,[status(thm)],[857]) ).
thf(40,axiom,
! [TA: $tType,A: TA,B: TA] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
<=> ( B = A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_singleton__iff) ).
thf(275,plain,
! [TA: $tType,A: TA,B: TA] :
( ( ( B = A )
=> ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) )
& ( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( B = A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(16,axiom,
! [TA: $tType,A: bool @ ( state @ fun ) @ ( TA @ fun ),B: com,C: bool @ ( state @ fun ) @ ( TA @ fun ),D: com,E: bool @ ( state @ fun ) @ ( TA @ fun ),F: bool @ ( TA @ hoare_28830079triple @ fun )] :
( ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( C @ ( D @ ( E @ ( TA @ hoare_1841697145triple ) ) ) @ ( TA @ hoare_28830079triple @ insert ) ) @ ( F @ ( TA @ hoare_992312373derivs ) ) )
=> ( ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( A @ ( B @ ( C @ ( TA @ hoare_1841697145triple ) ) ) @ ( TA @ hoare_28830079triple @ insert ) ) @ ( F @ ( TA @ hoare_992312373derivs ) ) )
=> ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( A @ ( B @ ( D @ semi ) @ ( E @ ( TA @ hoare_1841697145triple ) ) ) @ ( TA @ hoare_28830079triple @ insert ) ) @ ( F @ ( TA @ hoare_992312373derivs ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_Comp) ).
thf(197,plain,
! [TA: $tType,A: bool @ ( state @ fun ) @ ( TA @ fun ),B: com,C: bool @ ( state @ fun ) @ ( TA @ fun ),D: com,E: bool @ ( state @ fun ) @ ( TA @ fun ),F: bool @ ( TA @ hoare_28830079triple @ fun )] :
( ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( C @ ( D @ ( E @ ( TA @ hoare_1841697145triple ) ) ) @ ( TA @ hoare_28830079triple @ insert ) ) @ ( F @ ( TA @ hoare_992312373derivs ) ) )
=> ( ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( A @ ( B @ ( C @ ( TA @ hoare_1841697145triple ) ) ) @ ( TA @ hoare_28830079triple @ insert ) ) @ ( F @ ( TA @ hoare_992312373derivs ) ) )
=> ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( A @ ( B @ ( D @ semi ) @ ( E @ ( TA @ hoare_1841697145triple ) ) ) @ ( TA @ hoare_28830079triple @ insert ) ) @ ( F @ ( TA @ hoare_992312373derivs ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(7965,plain,
! [TA: $tType,A: TA] :
( ( ( fTrue @ pp )
!= ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ aa ) ) ) @ pp ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[544,7904]) ).
thf(7966,plain,
! [TA: $tType,A: TA] :
( ( fTrue @ pp )
!= ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ aa ) ) ) @ pp ) ),
inference(simp,[status(thm)],[7965]) ).
thf(7978,plain,
! [TA: $tType,A: TA] :
( fTrue
!= ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ aa ) ) ) ) ),
inference(simp,[status(thm)],[7966]) ).
thf(8002,plain,
! [TA: $tType,B: TA,A: bool] :
( ( A
!= ( B @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ aa ) ) ) ) )
| ( fTrue != fTrue )
| ( A = fFalse ) ),
inference(paramod_ordered,[status(thm)],[142,7978]) ).
thf(8003,plain,
! [TA: $tType,B: TA,A: bool] :
( ( A
!= ( B @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ aa ) ) ) ) )
| ( A = fFalse ) ),
inference(simp,[status(thm)],[8002]) ).
thf(8004,plain,
! [TA: $tType,A: TA] :
( ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ aa ) ) ) )
= fFalse ),
inference(pattern_uni,[status(thm)],[8003:[bind(A,$thf( D @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ aa ) ) ) )),bind(B,$thf( D ))]]) ).
thf(8036,plain,
! [TA: $tType,A: TA] :
( ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ aa ) ) ) )
= fFalse ),
inference(simp,[status(thm)],[8004]) ).
thf(8047,plain,
! [TA: $tType,TB: $tType,A: TA] :
( ( fFalse != fFalse )
| ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) @ ( TB @ finite_finite1 ) ) ),
inference(paramod_ordered,[status(thm)],[8036,719]) ).
thf(8048,plain,
! [TA: $tType,TB: $tType,A: TA] : ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) @ ( TB @ finite_finite1 ) ),
inference(pattern_uni,[status(thm)],[8047:[]]) ).
thf(125,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun ),C: TA] :
( ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ~ ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_DiffI) ).
thf(625,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun ),C: TA] :
( ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ~ ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[125]) ).
thf(1818,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( fFalse != fFalse )
| ( ( A @ ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ) ),
inference(paramod_ordered,[status(thm)],[1805,739]) ).
thf(1819,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(pattern_uni,[status(thm)],[1818:[]]) ).
thf(88,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA,C: bool @ ( TA @ fun )] :
( ( A @ ( B @ ( TA @ insert ) ) @ ( C @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( A @ ( C @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_Diff__insert) ).
thf(484,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA,C: bool @ ( TA @ fun )] :
( ( A @ ( B @ ( TA @ insert ) ) @ ( C @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( A @ ( C @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).
thf(878,plain,
! [TB: $tType,A: TB] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ( ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( A @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) )
!= fTrue ) ),
inference(paramod_ordered,[status(thm)],[701,670]) ).
thf(879,plain,
! [TB: $tType,A: TB] :
( ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( A @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) )
!= fTrue ),
inference(pattern_uni,[status(thm)],[878:[]]) ).
thf(893,plain,
! [TA: $tType,A: TA] :
( ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
!= fTrue ),
inference(simp,[status(thm)],[879]) ).
thf(1079,plain,
! [TA: $tType,B: TA,A: bool] :
( ( A
!= ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) ) )
| ( fTrue != fTrue )
| ( A = fFalse ) ),
inference(paramod_ordered,[status(thm)],[142,893]) ).
thf(1080,plain,
! [TA: $tType,B: TA,A: bool] :
( ( A
!= ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) ) )
| ( A = fFalse ) ),
inference(simp,[status(thm)],[1079]) ).
thf(1081,plain,
! [TA: $tType,A: TA] :
( ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
= fFalse ),
inference(pattern_uni,[status(thm)],[1080:[bind(A,$thf( fFalse @ ( TA @ ( bool @ combk ) ) @ ( F @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) )),bind(B,$thf( F ))]]) ).
thf(1089,plain,
! [TA: $tType,A: TA] :
( ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
= fFalse ),
inference(simp,[status(thm)],[1081]) ).
thf(648,plain,
( ( ( fTrue @ pp )
!= ( fFalse @ pp ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[544,433]) ).
thf(649,plain,
( ( fTrue @ pp )
!= ( fFalse @ pp ) ),
inference(simp,[status(thm)],[648]) ).
thf(650,plain,
fTrue != fFalse,
inference(simp,[status(thm)],[649]) ).
thf(151,plain,
! [D: com,C: com,B: com,A: com] :
( ( C = A )
| ( ( C @ ( D @ semi ) )
!= ( A @ ( B @ semi ) ) ) ),
inference(cnfConj,[status(thm)],[149]) ).
thf(156,plain,
! [D: com,C: com,B: com,A: com] :
( ( C = A )
| ( ( C @ ( D @ semi ) )
!= ( A @ ( B @ semi ) ) ) ),
inference(lifteq,[status(thm)],[151]) ).
thf(110,axiom,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_Diff__cancel) ).
thf(560,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[110]) ).
thf(561,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(cnf,[status(esa)],[560]) ).
thf(562,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(lifteq,[status(thm)],[561]) ).
thf(1477,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ( A @ ( A @ ( bool @ ( TB @ fun ) @ minus_minus ) ) @ ( TB @ finite_finite1 ) ) ),
inference(paramod_ordered,[status(thm)],[562,355]) ).
thf(1478,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] : ( A @ ( A @ ( bool @ ( TB @ fun ) @ minus_minus ) ) @ ( TB @ finite_finite1 ) ),
inference(pattern_uni,[status(thm)],[1477:[]]) ).
thf(1540,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] : ( A @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ finite_finite1 ) ),
inference(simp,[status(thm)],[1478]) ).
thf(120,axiom,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA] :
( ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( B @ ( A @ ( TA @ insert ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_insertI2) ).
thf(610,plain,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA] :
( ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( B @ ( A @ ( TA @ insert ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[120]) ).
thf(945,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( ( fFalse @ ( TB @ ( bool @ combk ) ) )
!= ( fFalse @ ( TB @ ( bool @ combk ) ) ) )
| ( ( A @ ( bool @ ( TB @ fun ) @ bot_bot @ ( bool @ ( TB @ fun ) @ minus_minus ) ) @ ( TB @ collect ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ) ),
inference(paramod_ordered,[status(thm)],[926,616]) ).
thf(946,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( A @ ( bool @ ( TB @ fun ) @ bot_bot @ ( bool @ ( TB @ fun ) @ minus_minus ) ) @ ( TB @ collect ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ),
inference(pattern_uni,[status(thm)],[945:[]]) ).
thf(980,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ collect ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(simp,[status(thm)],[946]) ).
thf(75,axiom,
! [A: bool] :
( ( A @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ pp )
| ( A @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fNot_2_1_U) ).
thf(403,plain,
! [A: bool] :
( ( A @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ pp )
| ( A @ pp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(190,plain,
! [TA: $tType,C: TA @ ( TA @ fun ) @ ( TA @ fun ),B: TA,A: TA] :
( ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( C @ ( TA @ finite_fold1Set ) ) ) )
| ( B != A ) ),
inference(cnfConj,[status(thm)],[188]) ).
thf(192,plain,
! [TA: $tType,C: TA @ ( TA @ fun ) @ ( TA @ fun ),B: TA,A: TA] :
( ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( C @ ( TA @ finite_fold1Set ) ) ) )
| ( B != A ) ),
inference(lifteq,[status(thm)],[190]) ).
thf(193,plain,
! [TA: $tType,B: TA @ ( TA @ fun ) @ ( TA @ fun ),A: TA] : ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( B @ ( TA @ finite_fold1Set ) ) ) ),
inference(simp,[status(thm)],[192]) ).
thf(90,axiom,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ? [B: TA] : ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
<=> ( A
!= ( bool @ ( TA @ fun ) @ bot_bot ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_ex__in__conv) ).
thf(489,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( ( A
!= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ? [B: TA] : ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) )
& ( ? [B: TA] : ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( A
!= ( bool @ ( TA @ fun ) @ bot_bot ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[90]) ).
thf(1946,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) )
= ( A @ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( bool @ ( TB @ fun ) @ minus_minus ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1817,739]) ).
thf(1947,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) )
= ( A @ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( bool @ ( TB @ fun ) @ minus_minus ) ) ) ),
inference(pattern_uni,[status(thm)],[1946:[]]) ).
thf(2038,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) )
= ( A @ ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) ) ),
inference(simp,[status(thm)],[1947]) ).
thf(105,axiom,
! [TA: $tType,TB: $tType,TC: $tType,A: TC,B: TA,C: TB @ ( TA @ fun ) @ ( TC @ fun )] :
( ( A @ ( B @ ( C @ ( TB @ ( TA @ ( TC @ combc ) ) ) ) @ ( TB @ ( TC @ aa ) ) ) )
= ( B @ ( A @ ( C @ ( TB @ ( TA @ fun ) @ ( TC @ aa ) ) ) @ ( TB @ ( TA @ aa ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBC_1_1_U) ).
thf(547,plain,
! [TA: $tType,TB: $tType,TC: $tType,A: TC,B: TA,C: TB @ ( TA @ fun ) @ ( TC @ fun )] :
( ( A @ ( B @ ( C @ ( TB @ ( TA @ ( TC @ combc ) ) ) ) @ ( TB @ ( TC @ aa ) ) ) )
= ( B @ ( A @ ( C @ ( TB @ ( TA @ fun ) @ ( TC @ aa ) ) ) @ ( TB @ ( TA @ aa ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[105]) ).
thf(22,axiom,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_Diff__empty) ).
thf(212,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(95,axiom,
! [TA: $tType,A: bool @ ( state @ fun ) @ ( TA @ fun ),B: com,C: bool @ ( TA @ hoare_28830079triple @ fun ),D: bool @ ( state @ fun ) @ ( TA @ fun )] :
( ! [E: TA,F: state] :
( ( F @ ( E @ ( D @ ( bool @ ( state @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
=> ? [G: bool @ ( state @ fun ) @ ( TA @ fun ),H: bool @ ( state @ fun ) @ ( TA @ fun )] :
( ! [I: state] :
( ! [J: TA] :
( ( F @ ( J @ ( G @ ( bool @ ( state @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
=> ( I @ ( J @ ( H @ ( bool @ ( state @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) )
=> ( I @ ( E @ ( A @ ( bool @ ( state @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) )
& ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( H @ ( B @ ( G @ ( TA @ hoare_1841697145triple ) ) ) @ ( TA @ hoare_28830079triple @ insert ) ) @ ( C @ ( TA @ hoare_992312373derivs ) ) ) ) )
=> ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( A @ ( B @ ( D @ ( TA @ hoare_1841697145triple ) ) ) @ ( TA @ hoare_28830079triple @ insert ) ) @ ( C @ ( TA @ hoare_992312373derivs ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_conseq) ).
thf(515,plain,
! [TA: $tType,A: bool @ ( state @ fun ) @ ( TA @ fun ),B: com,C: bool @ ( TA @ hoare_28830079triple @ fun ),D: bool @ ( state @ fun ) @ ( TA @ fun )] :
( ! [E: TA,F: state] :
( ( F @ ( E @ ( D @ ( bool @ ( state @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
=> ? [G: bool @ ( state @ fun ) @ ( TA @ fun ),H: bool @ ( state @ fun ) @ ( TA @ fun )] :
( ! [I: state] :
( ! [J: TA] :
( ( F @ ( J @ ( G @ ( bool @ ( state @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
=> ( I @ ( J @ ( H @ ( bool @ ( state @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) )
=> ( I @ ( E @ ( A @ ( bool @ ( state @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) )
& ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( H @ ( B @ ( G @ ( TA @ hoare_1841697145triple ) ) ) @ ( TA @ hoare_28830079triple @ insert ) ) @ ( C @ ( TA @ hoare_992312373derivs ) ) ) ) )
=> ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( A @ ( B @ ( D @ ( TA @ hoare_1841697145triple ) ) ) @ ( TA @ hoare_28830079triple @ insert ) ) @ ( C @ ( TA @ hoare_992312373derivs ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(7084,plain,
! [A: bool] :
( ( A
!= ( fNot @ ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ fun ) @ aa ) ) ) ) )
| ( fTrue != fTrue )
| ( A = fFalse ) ),
inference(paramod_ordered,[status(thm)],[142,7078]) ).
thf(7085,plain,
! [A: bool] :
( ( A
!= ( fNot @ ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ fun ) @ aa ) ) ) ) )
| ( A = fFalse ) ),
inference(simp,[status(thm)],[7084]) ).
thf(7086,plain,
( ( fNot @ ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ fun ) @ aa ) ) ) )
= fFalse ),
inference(pattern_uni,[status(thm)],[7085:[bind(A,$thf( fNot @ ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ fun ) @ aa ) ) ) ))]]) ).
thf(113,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( TA @ collect ) @ ( B @ ( TA @ insert ) ) )
= ( A @ ( B @ ( TA @ fequal @ ( bool @ ( TA @ ( TA @ combc ) ) ) ) @ ( fNot @ ( TA @ ( bool @ ( bool @ combb ) ) ) ) @ ( fimplies @ ( TA @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) ) ) @ ( bool @ ( bool @ ( TA @ combs ) ) ) ) @ ( TA @ collect ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_insert__Collect) ).
thf(569,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( TA @ collect ) @ ( B @ ( TA @ insert ) ) )
= ( A @ ( B @ ( TA @ fequal @ ( bool @ ( TA @ ( TA @ combc ) ) ) ) @ ( fNot @ ( TA @ ( bool @ ( bool @ combb ) ) ) ) @ ( fimplies @ ( TA @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) ) ) @ ( bool @ ( bool @ ( TA @ combs ) ) ) ) @ ( TA @ collect ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[113]) ).
thf(102,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( B @ ( TA @ insert ) ) @ ( B @ ( TA @ insert ) ) )
= ( A @ ( B @ ( TA @ insert ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_insert__absorb2) ).
thf(541,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( B @ ( TA @ insert ) ) @ ( B @ ( TA @ insert ) ) )
= ( A @ ( B @ ( TA @ insert ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[102]) ).
thf(73,axiom,
! [TA: $tType,TB: $tType] :
( ( TB @ cl_Groups_Ominus )
=> ! [A: TA,B: TB @ ( TA @ fun ),C: TB @ ( TA @ fun )] :
( ( A @ ( B @ ( C @ ( TB @ ( TA @ fun ) @ minus_minus ) ) @ ( TB @ ( TA @ aa ) ) ) )
= ( A @ ( B @ ( TB @ ( TA @ aa ) ) ) @ ( A @ ( C @ ( TB @ ( TA @ aa ) ) ) @ ( TB @ minus_minus ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_minus__apply) ).
thf(398,plain,
! [TA: $tType,TB: $tType] :
( ( TB @ cl_Groups_Ominus )
=> ! [A: TA,B: TB @ ( TA @ fun ),C: TB @ ( TA @ fun )] :
( ( A @ ( B @ ( C @ ( TB @ ( TA @ fun ) @ minus_minus ) ) @ ( TB @ ( TA @ aa ) ) ) )
= ( A @ ( B @ ( TB @ ( TA @ aa ) ) ) @ ( A @ ( C @ ( TB @ ( TA @ aa ) ) ) @ ( TB @ minus_minus ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(109,axiom,
! [TA: $tType] : ( bool @ ( TA @ fun ) @ bot_bot @ ( TA @ finite_finite1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_finite_OemptyI) ).
thf(558,plain,
! [TA: $tType] : ( bool @ ( TA @ fun ) @ bot_bot @ ( TA @ finite_finite1 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[109]) ).
thf(213,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= A ),
inference(cnf,[status(esa)],[212]) ).
thf(214,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= A ),
inference(lifteq,[status(thm)],[213]) ).
thf(1304,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ( ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( A @ ( bool @ ( TB @ fun ) @ minus_minus ) ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[701,214]) ).
thf(1305,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( A @ ( bool @ ( TB @ fun ) @ minus_minus ) ) )
= A ),
inference(pattern_uni,[status(thm)],[1304:[]]) ).
thf(1333,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= A ),
inference(simp,[status(thm)],[1305]) ).
thf(9,axiom,
! [A: com,B: com] :
( skip
!= ( A @ ( B @ semi ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_com_Osimps_I12_J) ).
thf(166,plain,
! [A: com,B: com] :
( skip
!= ( A @ ( B @ semi ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(8012,plain,
! [TB: $tType,A: TB] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ( ( A @ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( bool @ ( TB @ aa ) ) ) )
!= fTrue ) ),
inference(paramod_ordered,[status(thm)],[701,7978]) ).
thf(8013,plain,
! [TB: $tType,A: TB] :
( ( A @ ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( bool @ ( TB @ aa ) ) ) )
!= fTrue ),
inference(pattern_uni,[status(thm)],[8012:[]]) ).
thf(8040,plain,
! [TA: $tType,A: TA] :
( ( A @ ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( bool @ ( TA @ aa ) ) ) )
!= fTrue ),
inference(simp,[status(thm)],[8013]) ).
thf(7,axiom,
! [TA: $tType] :
( ( TA @ finite_finite )
=> ! [A: bool @ ( TA @ fun )] : ( A @ ( TA @ finite_finite1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_finite__code) ).
thf(161,plain,
! [TA: $tType] :
( ( TA @ finite_finite )
=> ! [A: bool @ ( TA @ fun )] : ( A @ ( TA @ finite_finite1 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(154,plain,
? [A: com > com > com] :
! [B: com,C: com] :
( ( C @ ( B @ semi ) @ ( C @ A ) )
= B ),
inference(detectInverse,[status(thm)],[153]) ).
thf(155,plain,
! [B: com,A: com] :
( ( B @ ( A @ semi ) @ ( B @ sk4 ) )
= A ),
inference(cnf,[status(esa)],[154]) ).
thf(1301,plain,
! [B: com,A: com] :
( ( B @ ( A @ semi ) @ ( B @ sk4 ) )
= A ),
inference(lifteq,[status(thm)],[155]) ).
thf(117,axiom,
! [TA: $tType,TB: $tType,A: TB @ ( TA @ fun ),B: TB @ ( TA @ fun )] :
( ! [C: TA] :
( ( C @ ( B @ ( TB @ ( TA @ aa ) ) ) )
= ( C @ ( A @ ( TB @ ( TA @ aa ) ) ) ) )
=> ( B = A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_ext) ).
thf(601,plain,
! [TA: $tType,TB: $tType,A: TB @ ( TA @ fun ),B: TB @ ( TA @ fun )] :
( ! [C: TA] :
( ( C @ ( B @ ( TB @ ( TA @ aa ) ) ) )
= ( C @ ( A @ ( TB @ ( TA @ aa ) ) ) ) )
=> ( B = A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[117]) ).
thf(12,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun ),C: TA] :
( ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
<=> ( ~ ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
& ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_Diff__iff) ).
thf(178,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun ),C: TA] :
( ( ( ~ ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
& ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) )
=> ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) )
& ( ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ~ ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
& ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(179,plain,
! [TA: $tType,C: TA,B: bool @ ( TA @ fun ),A: bool @ ( TA @ fun )] :
( ( ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) )
& ( ~ ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) )
& ( ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ),
inference(cnf,[status(esa)],[178]) ).
thf(180,plain,
! [TA: $tType,C: TA,B: bool @ ( TA @ fun ),A: bool @ ( TA @ fun )] :
( ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
inference(cnfConj,[status(thm)],[179]) ).
thf(45,axiom,
! [TA: $tType,A: TA,B: TA] :
( ( A @ ( B @ ( TA @ fequal @ ( bool @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( TA @ aa ) ) ) @ pp )
| ( B != A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fequal_2_1_T) ).
thf(296,plain,
! [TA: $tType,A: TA,B: TA] :
( ( A @ ( B @ ( TA @ fequal @ ( bool @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( TA @ aa ) ) ) @ pp )
| ( B != A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(176,plain,
! [TA: $tType,B: bool @ ( TA @ fun ),A: bool @ ( bool @ ( TA @ fun ) @ fun )] :
( ( B @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ( A @ ( B @ ( TA @ sk7 ) ) @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( B @ ( TA @ finite_finite1 ) ) ),
inference(cnfConj,[status(thm)],[173]) ).
thf(1614,plain,
! [TB: $tType,TC: $tType,A: TB] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ( ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( A @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) @ ( TC @ ( bool @ combk ) ) )
= ( bool @ ( TC @ fun ) @ bot_bot ) ) ),
inference(paramod_ordered,[status(thm)],[701,1202]) ).
thf(1615,plain,
! [TB: $tType,TC: $tType,A: TB] :
( ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( A @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) @ ( TC @ ( bool @ combk ) ) )
= ( bool @ ( TC @ fun ) @ bot_bot ) ),
inference(pattern_uni,[status(thm)],[1614:[]]) ).
thf(1699,plain,
! [TA: $tType,TB: $tType,A: TA] :
( ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ),
inference(simp,[status(thm)],[1615]) ).
thf(5121,plain,
! [TB: $tType] :
( ( fFalse @ ( TB @ ( bool @ combk ) ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ),
inference(rewrite,[status(thm)],[1699,1089]) ).
thf(116,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA,C: bool @ ( TA @ fun ),D: TA] :
( ~ ( C @ ( D @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( ( C @ ( D @ ( TA @ insert ) ) )
= ( A @ ( B @ ( TA @ insert ) ) ) )
<=> ( ( ( D != B )
=> ? [E: bool @ ( TA @ fun )] :
( ~ ( E @ ( D @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
& ( A
= ( E @ ( D @ ( TA @ insert ) ) ) )
& ~ ( E @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
& ( C
= ( E @ ( B @ ( TA @ insert ) ) ) ) ) )
& ( ( D = B )
=> ( C = A ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_insert__eq__iff) ).
thf(577,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA,C: bool @ ( TA @ fun ),D: TA] :
( ~ ( C @ ( D @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( ( ( ( D != B )
=> ? [E: bool @ ( TA @ fun )] :
( ~ ( E @ ( D @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
& ( A
= ( E @ ( D @ ( TA @ insert ) ) ) )
& ~ ( E @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
& ( C
= ( E @ ( B @ ( TA @ insert ) ) ) ) ) )
& ( ( D = B )
=> ( C = A ) ) )
=> ( ( C @ ( D @ ( TA @ insert ) ) )
= ( A @ ( B @ ( TA @ insert ) ) ) ) )
& ( ( ( C @ ( D @ ( TA @ insert ) ) )
= ( A @ ( B @ ( TA @ insert ) ) ) )
=> ( ( ( D != B )
=> ? [E: bool @ ( TA @ fun )] :
( ~ ( E @ ( D @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
& ( A
= ( E @ ( D @ ( TA @ insert ) ) ) )
& ~ ( E @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
& ( C
= ( E @ ( B @ ( TA @ insert ) ) ) ) ) )
& ( ( D = B )
=> ( C = A ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[116]) ).
thf(43,axiom,
! [TA: $tType,A: TA] :
~ ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_empty__iff) ).
thf(291,plain,
! [TA: $tType,A: TA] :
~ ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(104,axiom,
! [TA: $tType,A: TA,B: TA @ ( TA @ fun ) @ ( TA @ fun )] :
~ ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ finite_fold1Set ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_empty__fold1SetE) ).
thf(545,plain,
! [TA: $tType,A: TA,B: TA @ ( TA @ fun ) @ ( TA @ fun )] :
~ ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ finite_fold1Set ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[104]) ).
thf(35,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun )] :
( ( B @ ( TA @ finite_finite1 ) )
=> ( ( B @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ finite_finite1 ) )
<=> ( A @ ( TA @ finite_finite1 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_finite__Diff2) ).
thf(259,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun )] :
( ( B @ ( TA @ finite_finite1 ) )
=> ( ( ( A @ ( TA @ finite_finite1 ) )
=> ( B @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ finite_finite1 ) ) )
& ( ( B @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ finite_finite1 ) )
=> ( A @ ( TA @ finite_finite1 ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(131,axiom,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( ( A @ ( TA @ collect ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) )
<=> ! [B: TA] :
~ ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_Collect__empty__eq) ).
thf(641,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( ! [B: TA] :
~ ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp )
=> ( ( A @ ( TA @ collect ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ) )
& ( ( ( A @ ( TA @ collect ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ! [B: TA] :
~ ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[131]) ).
thf(67,axiom,
! [A: bool,B: bool] :
( ( A @ pp )
| ( B @ pp )
| ~ ( A @ ( B @ ( fdisj @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fdisj_3_1_U) ).
thf(382,plain,
! [A: bool,B: bool] :
( ( A @ pp )
| ( B @ pp )
| ~ ( A @ ( B @ ( fdisj @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(114,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun )] :
( ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ ( TA @ combc ) ) ) ) @ ( fNot @ ( TA @ ( bool @ ( bool @ combb ) ) ) ) @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ ( TA @ combc ) ) ) ) @ ( fconj @ ( TA @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) ) ) @ ( bool @ ( bool @ ( TA @ combs ) ) ) ) @ ( TA @ collect ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_set__diff__eq) ).
thf(572,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun )] :
( ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ ( TA @ combc ) ) ) ) @ ( fNot @ ( TA @ ( bool @ ( bool @ combb ) ) ) ) @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ ( TA @ combc ) ) ) ) @ ( fconj @ ( TA @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) ) ) @ ( bool @ ( bool @ ( TA @ combs ) ) ) ) @ ( TA @ collect ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[114]) ).
thf(181,plain,
! [TA: $tType,C: TA,B: bool @ ( TA @ fun ),A: bool @ ( TA @ fun )] :
( ~ ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
inference(cnfConj,[status(thm)],[179]) ).
thf(539,plain,
! [TA: $tType,B: TA,A: bool @ ( TA @ fun )] :
( ( A @ ( B @ ( TA @ insert ) ) )
!= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(cnf,[status(esa)],[538]) ).
thf(540,plain,
! [TA: $tType,B: TA,A: bool @ ( TA @ fun )] :
( ( A @ ( B @ ( TA @ insert ) ) )
!= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(lifteq,[status(thm)],[539]) ).
thf(1864,plain,
! [TA: $tType] :
( ( fFalse != fFalse )
| ( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( TA @ collect ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ) ),
inference(paramod_ordered,[status(thm)],[1805,616]) ).
thf(1865,plain,
! [TA: $tType] :
( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( TA @ collect ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(pattern_uni,[status(thm)],[1864:[]]) ).
thf(92,axiom,
! [TA: $tType,TB: $tType] :
( ( TA @ bot )
=> ( TA @ ( TB @ fun ) @ bot ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_fun___Orderings_Obot) ).
thf(498,plain,
! [TA: $tType,TB: $tType] :
( ( TA @ bot )
=> ( TA @ ( TB @ fun ) @ bot ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
thf(118,axiom,
! [TA: $tType,A: TA @ ( TA @ fun ) @ ( TA @ fun ),B: bool @ ( TA @ fun )] :
( ( B @ ( TA @ finite_finite1 ) )
=> ( ( B
!= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ? [C: TA] : ( C @ ( B @ ( A @ ( TA @ finite_fold1Set ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_finite__nonempty__imp__fold1Set) ).
thf(604,plain,
! [TA: $tType,A: TA @ ( TA @ fun ) @ ( TA @ fun ),B: bool @ ( TA @ fun )] :
( ( B @ ( TA @ finite_finite1 ) )
=> ( ( B
!= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ? [C: TA] : ( C @ ( B @ ( A @ ( TA @ finite_fold1Set ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[118]) ).
thf(25,axiom,
! [TA: $tType,A: bool @ ( state @ fun ) @ ( TA @ fun ),B: com,C: bool @ ( state @ fun ) @ ( TA @ fun ),D: bool @ ( state @ fun ) @ ( TA @ fun ),E: com,F: bool @ ( state @ fun ) @ ( TA @ fun )] :
( ( ( D @ ( E @ ( F @ ( TA @ hoare_1841697145triple ) ) ) )
= ( A @ ( B @ ( C @ ( TA @ hoare_1841697145triple ) ) ) ) )
<=> ( ( D = A )
& ( E = B )
& ( F = C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_triple_Oinject) ).
thf(219,plain,
! [TA: $tType,A: bool @ ( state @ fun ) @ ( TA @ fun ),B: com,C: bool @ ( state @ fun ) @ ( TA @ fun ),D: bool @ ( state @ fun ) @ ( TA @ fun ),E: com,F: bool @ ( state @ fun ) @ ( TA @ fun )] :
( ( ( ( D = A )
& ( E = B )
& ( F = C ) )
=> ( ( D @ ( E @ ( F @ ( TA @ hoare_1841697145triple ) ) ) )
= ( A @ ( B @ ( C @ ( TA @ hoare_1841697145triple ) ) ) ) ) )
& ( ( ( D @ ( E @ ( F @ ( TA @ hoare_1841697145triple ) ) ) )
= ( A @ ( B @ ( C @ ( TA @ hoare_1841697145triple ) ) ) ) )
=> ( ( D = A )
& ( E = B )
& ( F = C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(162,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( TA @ finite_finite1 ) )
| ~ ( TA @ finite_finite ) ),
inference(cnf,[status(esa)],[161]) ).
thf(2149,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( ( bool @ finite_finite )
!= ( TA @ finite_finite ) )
| ( A @ ( TA @ finite_finite1 ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[307,162]) ).
thf(2150,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( ( bool @ finite_finite )
!= ( TA @ finite_finite ) )
| ( A @ ( TA @ finite_finite1 ) ) ),
inference(simp,[status(thm)],[2149]) ).
thf(2151,plain,
! [A: bool @ ( bool @ fun )] : ( A @ ( bool @ finite_finite1 ) ),
inference(pattern_uni,[status(thm)],[2150:[bind_type(TA,$thf( bool ))]]) ).
thf(1893,plain,
! [TA: $tType,A: TA] :
( ( fFalse != fFalse )
| ( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1805,891]) ).
thf(1894,plain,
! [TA: $tType,A: TA] :
( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) ) ),
inference(pattern_uni,[status(thm)],[1893:[]]) ).
thf(26,axiom,
! [TA: $tType,A: TA,B: TA] :
( ( B = A )
| ~ ( A @ ( B @ ( TA @ fequal @ ( bool @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( TA @ aa ) ) ) @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fequal_1_1_T) ).
thf(230,plain,
! [TA: $tType,A: TA,B: TA] :
( ( B = A )
| ~ ( A @ ( B @ ( TA @ fequal @ ( bool @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( TA @ aa ) ) ) @ pp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(60,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] : ( A @ ( B @ ( TA @ insert ) ) @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_insertI1) ).
thf(362,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] : ( A @ ( B @ ( TA @ insert ) ) @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(52,axiom,
! [TA: $tType,TB: $tType,A: bool @ ( state @ fun ) @ ( TA @ fun ),B: com,C: bool @ ( state @ fun ) @ ( TA @ fun ),D: TB @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ fun ) @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ fun )] :
( ( A @ ( B @ ( C @ ( TA @ hoare_1841697145triple ) ) ) @ ( D @ ( TB @ ( TA @ hoare_678420151le_rec ) ) ) )
= ( A @ ( B @ ( C @ ( D @ ( TB @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ fun ) @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ aa ) ) ) @ ( TB @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ fun ) @ ( com @ aa ) ) ) @ ( TB @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ aa ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_triple_Orecs) ).
thf(318,plain,
! [TA: $tType,TB: $tType,A: bool @ ( state @ fun ) @ ( TA @ fun ),B: com,C: bool @ ( state @ fun ) @ ( TA @ fun ),D: TB @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ fun ) @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ fun )] :
( ( A @ ( B @ ( C @ ( TA @ hoare_1841697145triple ) ) ) @ ( D @ ( TB @ ( TA @ hoare_678420151le_rec ) ) ) )
= ( A @ ( B @ ( C @ ( D @ ( TB @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ fun ) @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ aa ) ) ) @ ( TB @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ fun ) @ ( com @ aa ) ) ) @ ( TB @ ( bool @ ( state @ fun ) @ ( TA @ fun ) @ aa ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(157,plain,
? [A: com > com > com] :
! [B: com,C: com] :
( ( C @ ( B @ semi ) @ ( B @ A ) )
= C ),
inference(detectInverse,[status(thm)],[156]) ).
thf(158,plain,
! [B: com,A: com] :
( ( B @ ( A @ semi ) @ ( A @ sk5 ) )
= B ),
inference(cnf,[status(esa)],[157]) ).
thf(1801,plain,
! [B: com,A: com] :
( ( B @ ( A @ semi ) @ ( A @ sk5 ) )
= B ),
inference(lifteq,[status(thm)],[158]) ).
thf(81,axiom,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA,D: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( A @ ( B @ ( C @ ( TA @ insert ) ) @ ( D @ ( TA @ finite_fold1Set ) ) ) )
=> ~ ! [E: TA,F: bool @ ( TA @ fun )] :
( ( ( B @ ( C @ ( TA @ insert ) ) )
= ( F @ ( E @ ( TA @ insert ) ) ) )
=> ( ( A @ ( F @ ( E @ ( D @ ( TA @ ( TA @ finite_fold_graph ) ) ) ) ) )
=> ( F @ ( E @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_insert__fold1SetE) ).
thf(434,plain,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA,D: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( A @ ( B @ ( C @ ( TA @ insert ) ) @ ( D @ ( TA @ finite_fold1Set ) ) ) )
=> ~ ! [E: TA,F: bool @ ( TA @ fun )] :
( ( ( B @ ( C @ ( TA @ insert ) ) )
= ( F @ ( E @ ( TA @ insert ) ) ) )
=> ( ( A @ ( F @ ( E @ ( D @ ( TA @ ( TA @ finite_fold_graph ) ) ) ) ) )
=> ( F @ ( E @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(69,axiom,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun )] :
( ( B @ ( TA @ finite_finite1 ) )
=> ( B @ ( A @ ( TA @ insert ) ) @ ( TA @ finite_finite1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_finite_OinsertI) ).
thf(387,plain,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun )] :
( ( B @ ( TA @ finite_finite1 ) )
=> ( B @ ( A @ ( TA @ insert ) ) @ ( TA @ finite_finite1 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(62,axiom,
! [TA: $tType,TB: $tType] :
( ( ( TB @ finite_finite )
& ( TA @ finite_finite ) )
=> ( TA @ ( TB @ fun ) @ finite_finite ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_fun___Finite__Set_Ofinite) ).
thf(367,plain,
! [TA: $tType,TB: $tType] :
( ( ( TB @ finite_finite )
& ( TA @ finite_finite ) )
=> ( TA @ ( TB @ fun ) @ finite_finite ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(100,axiom,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ! [B: TA] :
~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( A
= ( bool @ ( TA @ fun ) @ bot_bot ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_equals0I) ).
thf(535,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ! [B: TA] :
~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( A
= ( bool @ ( TA @ fun ) @ bot_bot ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[100]) ).
thf(7097,plain,
! [TA: $tType] :
( ( fFalse != fFalse )
| ( fNot @ ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ fun ) @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( TA @ finite_finite1 ) ) ),
inference(paramod_ordered,[status(thm)],[7086,719]) ).
thf(7098,plain,
! [TA: $tType] : ( fNot @ ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ fun ) @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( TA @ finite_finite1 ) ),
inference(pattern_uni,[status(thm)],[7097:[]]) ).
thf(96,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( B @ ( TA @ insert ) ) )
= ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ ( TA @ combc ) ) ) ) @ ( B @ ( TA @ fequal @ ( bool @ ( TA @ ( TA @ combc ) ) ) ) @ ( fdisj @ ( TA @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) ) ) @ ( bool @ ( bool @ ( TA @ combs ) ) ) ) @ ( TA @ collect ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_insert__compr) ).
thf(520,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( B @ ( TA @ insert ) ) )
= ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ ( TA @ combc ) ) ) ) @ ( B @ ( TA @ fequal @ ( bool @ ( TA @ ( TA @ combc ) ) ) ) @ ( fdisj @ ( TA @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) ) ) @ ( bool @ ( bool @ ( TA @ combs ) ) ) ) @ ( TA @ collect ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).
thf(687,plain,
! [A: a] :
( ( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
!= ( fFalse @ pp ) )
| ~ $true
| ~ ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ),
inference(paramod_ordered,[status(thm)],[678,433]) ).
thf(688,plain,
! [A: a] :
( ( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
!= ( fFalse @ pp ) )
| ~ ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ),
inference(simp,[status(thm)],[687]) ).
thf(695,plain,
! [A: a] :
( ( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )
!= fFalse )
| ~ ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ),
inference(simp,[status(thm)],[688]) ).
thf(1363,plain,
! [TA: $tType,A: a] :
( ( fFalse != fFalse )
| ( ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) )
| ( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )
!= fFalse ) ),
inference(paramod_ordered,[status(thm)],[907,701]) ).
thf(1364,plain,
! [TA: $tType,A: a] :
( ( ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) )
| ( ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) )
!= fFalse ) ),
inference(pattern_uni,[status(thm)],[1363:[]]) ).
thf(1112,plain,
! [TA: $tType,A: a] :
( ( fFalse != fFalse )
| ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( TA @ finite_finite1 ) )
| ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ),
inference(paramod_ordered,[status(thm)],[803,719]) ).
thf(1113,plain,
! [TA: $tType,A: a] :
( ( sk2 @ ( A @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( TA @ finite_finite1 ) )
| ( p1 @ ( q1 @ sk3 ) @ ( A @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) ),
inference(pattern_uni,[status(thm)],[1112:[]]) ).
thf(111,axiom,
~ ( fFalse @ pp ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
thf(563,plain,
~ ( fFalse @ pp ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[111]) ).
thf(87,axiom,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( A @ ( B @ ( C @ ( TA @ finite_fold1Set ) ) ) )
<=> ? [D: TA,E: bool @ ( TA @ fun ),F: TA] :
( ~ ( E @ ( D @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
& ( F @ ( E @ ( D @ ( C @ ( TA @ ( TA @ finite_fold_graph ) ) ) ) ) )
& ( A = F )
& ( B
= ( E @ ( D @ ( TA @ insert ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_fold1Set_Osimps) ).
thf(473,plain,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( ? [D: TA,E: bool @ ( TA @ fun ),F: TA] :
( ~ ( E @ ( D @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
& ( F @ ( E @ ( D @ ( C @ ( TA @ ( TA @ finite_fold_graph ) ) ) ) ) )
& ( A = F )
& ( B
= ( E @ ( D @ ( TA @ insert ) ) ) ) )
=> ( A @ ( B @ ( C @ ( TA @ finite_fold1Set ) ) ) ) )
& ( ( A @ ( B @ ( C @ ( TA @ finite_fold1Set ) ) ) )
=> ? [D: TA,E: bool @ ( TA @ fun ),F: TA] :
( ~ ( E @ ( D @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
& ( F @ ( E @ ( D @ ( C @ ( TA @ ( TA @ finite_fold_graph ) ) ) ) ) )
& ( A = F )
& ( B
= ( E @ ( D @ ( TA @ insert ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).
thf(1962,plain,
! [TB: $tType,A: TB] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) @ ( A @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) )
!= fTrue ) ),
inference(paramod_ordered,[status(thm)],[1817,670]) ).
thf(1963,plain,
! [TB: $tType,A: TB] :
( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) @ ( A @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) )
!= fTrue ),
inference(pattern_uni,[status(thm)],[1962:[]]) ).
thf(2054,plain,
! [TA: $tType,A: TA] :
( ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
!= fTrue ),
inference(simp,[status(thm)],[1963]) ).
thf(7046,plain,
! [TA: $tType,B: TA,A: bool @ ( TA @ fun )] :
( ( ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp )
!= ( fNot @ ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ fun ) @ aa ) ) ) @ pp ) )
| ~ $true
| ~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
inference(paramod_ordered,[status(thm)],[185,6991]) ).
thf(7047,plain,
! [TA: $tType,B: TA,A: bool @ ( TA @ fun )] :
( ( ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp )
!= ( fNot @ ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ fun ) @ aa ) ) ) @ pp ) )
| ~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
inference(simp,[status(thm)],[7046]) ).
thf(7048,plain,
~ ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( fNot @ ( bool @ ( bool @ fun ) @ member @ ( bool @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ aa ) ) ) @ pp ),
inference(pattern_uni,[status(thm)],[7047:[bind(A,$thf( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) )),bind(B,$thf( fNot )),bind_type(TA,$thf( bool @ ( bool @ fun ) ))]]) ).
thf(7369,plain,
! [TA: $tType,B: TA,A: bool @ ( TA @ fun )] :
( ( ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp )
!= ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( fNot @ ( bool @ ( bool @ fun ) @ member @ ( bool @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ aa ) ) ) @ pp ) )
| ~ $true
| ~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
inference(paramod_ordered,[status(thm)],[185,7048]) ).
thf(7370,plain,
! [TA: $tType,B: TA,A: bool @ ( TA @ fun )] :
( ( ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp )
!= ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( fNot @ ( bool @ ( bool @ fun ) @ member @ ( bool @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ aa ) ) ) @ pp ) )
| ~ ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
inference(simp,[status(thm)],[7369]) ).
thf(7371,plain,
~ ( fNot @ ( bool @ ( bool @ fun ) @ member @ ( bool @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ aa ) ) ) @ ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ member @ ( bool @ ( bool @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ fun ) @ fun ) @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ fun ) @ aa ) ) ) @ pp ),
inference(pattern_uni,[status(thm)],[7370:[bind(A,$thf( fNot @ ( bool @ ( bool @ fun ) @ member @ ( bool @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ aa ) ) ) )),bind(B,$thf( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) )),bind_type(TA,$thf( bool @ ( bool @ ( bool @ fun ) @ fun ) ))]]) ).
thf(123,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun ),C: TA] :
( ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_DiffD1) ).
thf(617,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun ),C: TA] :
( ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[123]) ).
thf(107,axiom,
! [TA: $tType,A: bool @ ( state @ fun ) @ ( TA @ fun ),B: bool @ ( TA @ hoare_28830079triple @ fun )] : ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( A @ ( skip @ ( A @ ( TA @ hoare_1841697145triple ) ) ) @ ( TA @ hoare_28830079triple @ insert ) ) @ ( B @ ( TA @ hoare_992312373derivs ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_hoare__derivs_OSkip) ).
thf(553,plain,
! [TA: $tType,A: bool @ ( state @ fun ) @ ( TA @ fun ),B: bool @ ( TA @ hoare_28830079triple @ fun )] : ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( A @ ( skip @ ( A @ ( TA @ hoare_1841697145triple ) ) ) @ ( TA @ hoare_28830079triple @ insert ) ) @ ( B @ ( TA @ hoare_992312373derivs ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[107]) ).
thf(15,axiom,
! [A: bool,B: bool] :
( ( A @ pp )
| ~ ( A @ ( B @ ( fconj @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fconj_3_1_U) ).
thf(194,plain,
! [A: bool,B: bool] :
( ( A @ pp )
| ~ ( A @ ( B @ ( fconj @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(99,axiom,
! [TA: $tType,A: TA] :
( ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ aa ) ) ) @ pp )
<=> ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_bot__empty__eq) ).
thf(531,plain,
! [TA: $tType,A: TA] :
( ( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ aa ) ) ) @ pp ) )
& ( ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ aa ) ) ) @ pp )
=> ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[99]) ).
thf(89,axiom,
! [A: bool,B: bool] :
( ( A @ ( B @ ( fimplies @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp )
| ( B @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fimplies_1_1_U) ).
thf(487,plain,
! [A: bool,B: bool] :
( ( A @ ( B @ ( fimplies @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp )
| ( B @ pp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(1844,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( fFalse != fFalse )
| ( A @ ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ finite_finite1 ) ) ),
inference(paramod_ordered,[status(thm)],[1805,847]) ).
thf(1845,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] : ( A @ ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ finite_finite1 ) ),
inference(pattern_uni,[status(thm)],[1844:[]]) ).
thf(294,plain,
! [TA: $tType,A: TA] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( TA @ the_elem ) )
= A ),
inference(cnf,[status(esa)],[293]) ).
thf(295,plain,
! [TA: $tType,A: TA] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) @ ( TA @ the_elem ) )
= A ),
inference(lifteq,[status(thm)],[294]) ).
thf(964,plain,
! [TB: $tType,B: bool @ ( TB @ hoare_28830079triple @ fun ),A: bool @ ( TB @ hoare_28830079triple @ fun )] :
( ( ( fFalse @ ( TB @ hoare_28830079triple @ ( bool @ combk ) ) )
!= ( fFalse @ ( TB @ hoare_28830079triple @ ( bool @ combk ) ) ) )
| ( A @ ( bool @ ( TB @ hoare_28830079triple @ fun ) @ bot_bot @ ( bool @ ( TB @ hoare_28830079triple @ fun ) @ minus_minus ) ) @ ( B @ ( TB @ hoare_992312373derivs ) ) ) ),
inference(paramod_ordered,[status(thm)],[926,720]) ).
thf(965,plain,
! [TB: $tType,B: bool @ ( TB @ hoare_28830079triple @ fun ),A: bool @ ( TB @ hoare_28830079triple @ fun )] : ( A @ ( bool @ ( TB @ hoare_28830079triple @ fun ) @ bot_bot @ ( bool @ ( TB @ hoare_28830079triple @ fun ) @ minus_minus ) ) @ ( B @ ( TB @ hoare_992312373derivs ) ) ),
inference(pattern_uni,[status(thm)],[964:[]]) ).
thf(971,plain,
! [TA: $tType,B: bool @ ( TA @ hoare_28830079triple @ fun ),A: bool @ ( TA @ hoare_28830079triple @ fun )] : ( A @ ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( bool @ ( TA @ hoare_28830079triple @ fun ) @ minus_minus ) ) @ ( B @ ( TA @ hoare_992312373derivs ) ) ),
inference(simp,[status(thm)],[965]) ).
thf(36,axiom,
! [TA: $tType,TB: $tType,A: TA,B: TA @ ( TA @ fun ) @ ( TB @ fun )] : ( A @ ( bool @ ( TB @ fun ) @ bot_bot @ ( A @ ( B @ ( TA @ ( TB @ finite_fold_graph ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_fold__graph_OemptyI) ).
thf(263,plain,
! [TA: $tType,TB: $tType,A: TA,B: TA @ ( TA @ fun ) @ ( TB @ fun )] : ( A @ ( bool @ ( TB @ fun ) @ bot_bot @ ( A @ ( B @ ( TA @ ( TB @ finite_fold_graph ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(17,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( A @ ( B @ ( TA @ insert ) ) )
= A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_insert__absorb) ).
thf(199,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( A @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( A @ ( B @ ( TA @ insert ) ) )
= A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(55,axiom,
! [TA: $tType,A: TA,B: TA] :
( ( ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) ) )
=> ( B = A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_singleton__inject) ).
thf(331,plain,
! [TA: $tType,A: TA,B: TA] :
( ( ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( TA @ insert ) ) ) )
=> ( B = A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(64,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( B @ ( TA @ insert ) ) )
= ( A @ ( B @ ( TA @ insert ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_insert__Diff__single) ).
thf(370,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( B @ ( TA @ insert ) ) )
= ( A @ ( B @ ( TA @ insert ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(1473,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ( ( A @ ( A @ ( bool @ ( TB @ fun ) @ minus_minus ) ) )
= ( fFalse @ ( TB @ ( bool @ combk ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[562,701]) ).
thf(1474,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( A @ ( A @ ( bool @ ( TB @ fun ) @ minus_minus ) ) )
= ( fFalse @ ( TB @ ( bool @ combk ) ) ) ),
inference(pattern_uni,[status(thm)],[1473:[]]) ).
thf(1538,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( fFalse @ ( TA @ ( bool @ combk ) ) ) ),
inference(simp,[status(thm)],[1474]) ).
thf(7393,plain,
( ( ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( fNot @ ( bool @ ( bool @ fun ) @ member @ ( bool @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ aa ) ) ) @ pp )
!= ( fTrue @ pp ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[544,7048]) ).
thf(7394,plain,
( ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( fNot @ ( bool @ ( bool @ fun ) @ member @ ( bool @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ aa ) ) ) @ pp )
!= ( fTrue @ pp ) ),
inference(simp,[status(thm)],[7393]) ).
thf(7398,plain,
( ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( fNot @ ( bool @ ( bool @ fun ) @ member @ ( bool @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ aa ) ) ) )
!= fTrue ),
inference(simp,[status(thm)],[7394]) ).
thf(177,plain,
! [TA: $tType,B: bool @ ( TA @ fun ),A: bool @ ( bool @ ( TA @ fun ) @ fun )] :
( ( B @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( A @ ( B @ ( TA @ sk7 ) ) @ ( A @ ( B @ ( TA @ sk6 ) ) @ ( TA @ insert ) ) @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( B @ ( TA @ finite_finite1 ) ) ),
inference(cnfConj,[status(thm)],[173]) ).
thf(182,plain,
! [TA: $tType,C: TA,B: bool @ ( TA @ fun ),A: bool @ ( TA @ fun )] :
( ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ),
inference(cnfConj,[status(thm)],[179]) ).
thf(175,plain,
! [TA: $tType,B: bool @ ( TA @ fun ),A: bool @ ( bool @ ( TA @ fun ) @ fun )] :
( ( B @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( A @ ( B @ ( TA @ sk7 ) ) @ ( A @ ( B @ ( TA @ sk6 ) ) @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( bool @ ( TA @ fun ) @ bot_bot @ ( A @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ~ ( B @ ( TA @ finite_finite1 ) ) ),
inference(cnfConj,[status(thm)],[173]) ).
thf(84,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA,C: bool @ ( TA @ fun )] :
( ( A @ ( B @ ( TA @ insert ) ) @ ( C @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( C @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_Diff__insert2) ).
thf(446,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA,C: bool @ ( TA @ fun )] :
( ( A @ ( B @ ( TA @ insert ) ) @ ( C @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( B @ ( TA @ insert ) ) @ ( C @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(121,axiom,
! [TA: $tType,TB: $tType,A: TA,B: TA,C: TA @ ( TA @ fun ) @ ( TB @ fun ),D: bool @ ( TB @ fun ),E: TB] :
( ~ ( D @ ( E @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) @ pp )
=> ( ( A @ ( D @ ( B @ ( C @ ( TA @ ( TB @ finite_fold_graph ) ) ) ) ) )
=> ( A @ ( E @ ( C @ ( TA @ ( TA @ fun ) @ ( TB @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) @ ( D @ ( E @ ( TB @ insert ) ) @ ( B @ ( C @ ( TA @ ( TB @ finite_fold_graph ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_fold__graph_OinsertI) ).
thf(612,plain,
! [TA: $tType,TB: $tType,A: TA,B: TA,C: TA @ ( TA @ fun ) @ ( TB @ fun ),D: bool @ ( TB @ fun ),E: TB] :
( ~ ( D @ ( E @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) @ pp )
=> ( ( A @ ( D @ ( B @ ( C @ ( TA @ ( TB @ finite_fold_graph ) ) ) ) ) )
=> ( A @ ( E @ ( C @ ( TA @ ( TA @ fun ) @ ( TB @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) @ ( D @ ( E @ ( TB @ insert ) ) @ ( B @ ( C @ ( TA @ ( TB @ finite_fold_graph ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[121]) ).
thf(5,axiom,
! [A: com,B: com] :
( ( A @ ( B @ semi ) )
!= skip ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_com_Osimps_I13_J) ).
thf(143,plain,
! [A: com,B: com] :
( ( A @ ( B @ semi ) )
!= skip ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(86,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA,C: TA] :
( ( A @ ( B @ ( TA @ insert ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
<=> ( ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ( C = B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_insert__iff) ).
thf(465,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA,C: TA] :
( ( ( ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ( C = B ) )
=> ( A @ ( B @ ( TA @ insert ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) )
& ( ( A @ ( B @ ( TA @ insert ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
| ( C = B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(126,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun )] :
( ( A @ ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_Diff__idemp) ).
thf(627,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun )] :
( ( A @ ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[126]) ).
thf(7176,plain,
! [TA: $tType] :
( ( fFalse != fFalse )
| ( ( fNot @ ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ fun ) @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ) ),
inference(paramod_ordered,[status(thm)],[7086,701]) ).
thf(7177,plain,
! [TA: $tType] :
( ( fNot @ ( fTrue @ ( bool @ member @ ( bool @ ( bool @ ( bool @ fun ) @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ ( bool @ fun ) @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(pattern_uni,[status(thm)],[7176:[]]) ).
thf(24,axiom,
bool @ cl_Groups_Ominus,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_HOL_Obool___Groups_Ominus) ).
thf(218,plain,
bool @ cl_Groups_Ominus,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(128,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( bool @ ( TA @ fun ) @ bot_bot )
!= ( A @ ( B @ ( TA @ insert ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_empty__not__insert) ).
thf(632,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
( ( bool @ ( TA @ fun ) @ bot_bot )
!= ( A @ ( B @ ( TA @ insert ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[128]) ).
thf(74,axiom,
! [TA: $tType,A: bool @ ( TA @ hoare_28830079triple @ fun ),B: TA @ hoare_28830079triple,C: bool @ ( TA @ hoare_28830079triple @ fun )] :
( ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( B @ ( TA @ hoare_28830079triple @ insert ) ) @ ( C @ ( TA @ hoare_992312373derivs ) ) )
=> ( ( A @ ( C @ ( TA @ hoare_992312373derivs ) ) )
=> ( A @ ( B @ ( TA @ hoare_28830079triple @ insert ) ) @ ( C @ ( TA @ hoare_992312373derivs ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_hoare__derivs_Oinsert) ).
thf(401,plain,
! [TA: $tType,A: bool @ ( TA @ hoare_28830079triple @ fun ),B: TA @ hoare_28830079triple,C: bool @ ( TA @ hoare_28830079triple @ fun )] :
( ( bool @ ( TA @ hoare_28830079triple @ fun ) @ bot_bot @ ( B @ ( TA @ hoare_28830079triple @ insert ) ) @ ( C @ ( TA @ hoare_992312373derivs ) ) )
=> ( ( A @ ( C @ ( TA @ hoare_992312373derivs ) ) )
=> ( A @ ( B @ ( TA @ hoare_28830079triple @ insert ) ) @ ( C @ ( TA @ hoare_992312373derivs ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(28,axiom,
! [A: a,B: state] :
( ( B @ ( A @ p ) )
=> ! [C: state] :
( ! [D: a] :
( ( B @ ( D @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
=> ( C @ ( D @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) )
=> ( C @ ( A @ q ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1) ).
thf(235,plain,
! [A: a,B: state] :
( ( B @ ( A @ p ) )
=> ! [C: state] :
( ! [D: a] :
( ( B @ ( D @ ( p1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp )
=> ( C @ ( D @ ( q1 @ ( bool @ ( state @ fun ) @ ( a @ aa ) ) ) @ ( bool @ ( state @ aa ) ) ) @ pp ) )
=> ( C @ ( A @ q ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(31,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun ),C: TA] :
( ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( B @ ( A @ ( C @ ( TA @ insert ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( B @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_insert__Diff1) ).
thf(246,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun ),C: TA] :
( ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( B @ ( A @ ( C @ ( TA @ insert ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( B @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(715,plain,
! [B: bool @ ( state @ fun ) @ ( a @ fun ),A: bool @ ( state @ fun ) @ ( a @ fun )] :
( ( ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot )
!= ( bool @ ( a @ hoare_28830079triple @ fun ) @ bot_bot ) )
| ~ ( A @ ( B @ sk3 ) @ ( sk1 @ q ) )
| ~ ( fFalse @ ( a @ hoare_28830079triple @ ( bool @ combk ) ) @ ( B @ ( c @ ( A @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) ) ),
inference(paramod_ordered,[status(thm)],[701,136]) ).
thf(716,plain,
! [B: bool @ ( state @ fun ) @ ( a @ fun ),A: bool @ ( state @ fun ) @ ( a @ fun )] :
( ~ ( A @ ( B @ sk3 ) @ ( sk1 @ q ) )
| ~ ( fFalse @ ( a @ hoare_28830079triple @ ( bool @ combk ) ) @ ( B @ ( c @ ( A @ ( a @ hoare_1841697145triple ) ) ) @ ( a @ hoare_28830079triple @ insert ) ) @ ( g @ ( a @ hoare_992312373derivs ) ) ) ),
inference(pattern_uni,[status(thm)],[715:[]]) ).
thf(78,axiom,
! [TA: $tType,TB: $tType,A: TA,B: bool @ ( TB @ fun ),C: TA,D: TA @ ( TA @ fun ) @ ( TB @ fun )] :
( ( A @ ( B @ ( C @ ( D @ ( TA @ ( TB @ finite_fold_graph ) ) ) ) ) )
<=> ( ? [E: TB,F: bool @ ( TB @ fun ),G: TA] :
( ( G @ ( F @ ( C @ ( D @ ( TA @ ( TB @ finite_fold_graph ) ) ) ) ) )
& ~ ( F @ ( E @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) @ pp )
& ( A
= ( G @ ( E @ ( D @ ( TA @ ( TA @ fun ) @ ( TB @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) ) )
& ( B
= ( F @ ( E @ ( TB @ insert ) ) ) ) )
| ( ( A = C )
& ( B
= ( bool @ ( TB @ fun ) @ bot_bot ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_fold__graph_Osimps) ).
thf(410,plain,
! [TA: $tType,TB: $tType,A: TA,B: bool @ ( TB @ fun ),C: TA,D: TA @ ( TA @ fun ) @ ( TB @ fun )] :
( ( ( ? [E: TB,F: bool @ ( TB @ fun ),G: TA] :
( ( G @ ( F @ ( C @ ( D @ ( TA @ ( TB @ finite_fold_graph ) ) ) ) ) )
& ~ ( F @ ( E @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) @ pp )
& ( A
= ( G @ ( E @ ( D @ ( TA @ ( TA @ fun ) @ ( TB @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) ) )
& ( B
= ( F @ ( E @ ( TB @ insert ) ) ) ) )
| ( ( A = C )
& ( B
= ( bool @ ( TB @ fun ) @ bot_bot ) ) ) )
=> ( A @ ( B @ ( C @ ( D @ ( TA @ ( TB @ finite_fold_graph ) ) ) ) ) ) )
& ( ( A @ ( B @ ( C @ ( D @ ( TA @ ( TB @ finite_fold_graph ) ) ) ) ) )
=> ( ? [E: TB,F: bool @ ( TB @ fun ),G: TA] :
( ( G @ ( F @ ( C @ ( D @ ( TA @ ( TB @ finite_fold_graph ) ) ) ) ) )
& ~ ( F @ ( E @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) @ pp )
& ( A
= ( G @ ( E @ ( D @ ( TA @ ( TA @ fun ) @ ( TB @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) ) )
& ( B
= ( F @ ( E @ ( TB @ insert ) ) ) ) )
| ( ( A = C )
& ( B
= ( bool @ ( TB @ fun ) @ bot_bot ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(144,plain,
~ ? [A: com,B: com] :
( ( A @ ( B @ semi ) )
= skip ),
inference(miniscope,[status(thm)],[143]) ).
thf(145,plain,
! [B: com,A: com] :
( ( A @ ( B @ semi ) )
!= skip ),
inference(cnf,[status(esa)],[144]) ).
thf(146,plain,
! [B: com,A: com] :
( ( A @ ( B @ semi ) )
!= skip ),
inference(lifteq,[status(thm)],[145]) ).
thf(76,axiom,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA @ ( bool @ ( TA @ fun ) @ fun ),D: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( C @ ( D @ ( TA @ finite_folding_one ) ) )
=> ( ( B @ ( TA @ finite_finite1 ) )
=> ( ~ ( B @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( B
!= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ( ( B @ ( A @ ( TA @ insert ) ) @ ( C @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
= ( B @ ( C @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( A @ ( D @ ( TA @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_folding__one_Oinsert) ).
thf(405,plain,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA @ ( bool @ ( TA @ fun ) @ fun ),D: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( C @ ( D @ ( TA @ finite_folding_one ) ) )
=> ( ( B @ ( TA @ finite_finite1 ) )
=> ( ~ ( B @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( ( B
!= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ( ( B @ ( A @ ( TA @ insert ) ) @ ( C @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) )
= ( B @ ( C @ ( TA @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( A @ ( D @ ( TA @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(1875,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( fFalse != fFalse )
| ( ( A @ ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( fFalse @ ( TA @ ( bool @ combk ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1805,851]) ).
thf(1876,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( fTrue @ ( fNot @ ( bool @ ( bool @ aa ) ) ) @ ( TA @ ( bool @ combk ) ) @ ( bool @ ( TA @ fun ) @ minus_minus ) ) )
= ( fFalse @ ( TA @ ( bool @ combk ) ) ) ),
inference(pattern_uni,[status(thm)],[1875:[]]) ).
thf(1580,plain,
! [TB: $tType,TC: $tType,A: TB] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( A @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) @ ( TC @ ( bool @ combk ) ) @ ( TC @ finite_finite1 ) ) ),
inference(paramod_ordered,[status(thm)],[701,1200]) ).
thf(1581,plain,
! [TB: $tType,TC: $tType,A: TB] : ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( A @ ( TB @ member @ ( bool @ ( bool @ ( TB @ fun ) @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( bool @ ( TB @ fun ) @ aa ) ) ) @ ( TC @ ( bool @ combk ) ) @ ( TC @ finite_finite1 ) ),
inference(pattern_uni,[status(thm)],[1580:[]]) ).
thf(1601,plain,
! [TA: $tType,TB: $tType,A: TA] : ( fFalse @ ( TA @ ( bool @ combk ) ) @ ( A @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) @ ( TB @ finite_finite1 ) ),
inference(simp,[status(thm)],[1581]) ).
thf(4597,plain,
! [TB: $tType] : ( fFalse @ ( TB @ ( bool @ combk ) ) @ ( TB @ finite_finite1 ) ),
inference(rewrite,[status(thm)],[1601,1089]) ).
thf(65,axiom,
! [TA: $tType,TB: $tType,TC: $tType,A: TA,B: TB @ ( TA @ fun ),C: TC @ ( TB @ fun )] :
( ( A @ ( B @ ( C @ ( TA @ ( TC @ ( TB @ combb ) ) ) ) @ ( TC @ ( TA @ aa ) ) ) )
= ( A @ ( B @ ( TB @ ( TA @ aa ) ) ) @ ( C @ ( TC @ ( TB @ aa ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBB_1_1_U) ).
thf(373,plain,
! [TA: $tType,TB: $tType,TC: $tType,A: TA,B: TB @ ( TA @ fun ),C: TC @ ( TB @ fun )] :
( ( A @ ( B @ ( C @ ( TA @ ( TC @ ( TB @ combb ) ) ) ) @ ( TC @ ( TA @ aa ) ) ) )
= ( A @ ( B @ ( TB @ ( TA @ aa ) ) ) @ ( C @ ( TC @ ( TB @ aa ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(46,axiom,
! [TA: $tType,TB: $tType] :
( ( TA @ cl_Groups_Ominus )
=> ( TA @ ( TB @ fun ) @ cl_Groups_Ominus ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_fun___Groups_Ominus) ).
thf(300,plain,
! [TA: $tType,TB: $tType] :
( ( TA @ cl_Groups_Ominus )
=> ( TA @ ( TB @ fun ) @ cl_Groups_Ominus ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(48,axiom,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA,D: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( A @ ( B @ ( C @ ( D @ ( TA @ ( TA @ finite_fold_graph ) ) ) ) ) )
=> ( ~ ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( A @ ( B @ ( C @ ( TA @ insert ) ) @ ( D @ ( TA @ finite_fold1Set ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_fold1Set_Ointros) ).
thf(305,plain,
! [TA: $tType,A: TA,B: bool @ ( TA @ fun ),C: TA,D: TA @ ( TA @ fun ) @ ( TA @ fun )] :
( ( A @ ( B @ ( C @ ( D @ ( TA @ ( TA @ finite_fold_graph ) ) ) ) ) )
=> ( ~ ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( A @ ( B @ ( C @ ( TA @ insert ) ) @ ( D @ ( TA @ finite_fold1Set ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(21,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun )] :
( ( B @ ( TA @ finite_finite1 ) )
=> ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ finite_finite1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_finite__Diff) ).
thf(210,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun )] :
( ( B @ ( TA @ finite_finite1 ) )
=> ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ finite_finite1 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(59,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun ),C: TA] :
( ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ~ ( ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_DiffE) ).
thf(358,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: bool @ ( TA @ fun ),C: TA] :
( ( A @ ( B @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ~ ( ( B @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
=> ( A @ ( C @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(129,axiom,
! [TA: $tType,TB: $tType,A: TA,B: TA,C: TA @ ( TA @ fun ) @ ( TB @ fun )] :
( ( A @ ( bool @ ( TB @ fun ) @ bot_bot @ ( B @ ( C @ ( TA @ ( TB @ finite_fold_graph ) ) ) ) ) )
=> ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_empty__fold__graphE) ).
thf(635,plain,
! [TA: $tType,TB: $tType,A: TA,B: TA,C: TA @ ( TA @ fun ) @ ( TB @ fun )] :
( ( A @ ( bool @ ( TB @ fun ) @ bot_bot @ ( B @ ( C @ ( TA @ ( TB @ finite_fold_graph ) ) ) ) ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[129]) ).
thf(29,axiom,
! [TA: $tType,TB: $tType] :
( ( TA @ bot )
=> ! [A: TB] :
( ( A @ ( TA @ ( TB @ fun ) @ bot_bot @ ( TA @ ( TB @ aa ) ) ) )
= ( TA @ bot_bot ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_bot__apply) ).
thf(239,plain,
! [TA: $tType,TB: $tType] :
( ( TA @ bot )
=> ! [A: TB] :
( ( A @ ( TA @ ( TB @ fun ) @ bot_bot @ ( TA @ ( TB @ aa ) ) ) )
= ( TA @ bot_bot ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(30,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA,C: bool @ ( TA @ fun )] :
( ( A @ ( B @ ( TA @ insert ) ) @ ( C @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ finite_finite1 ) )
<=> ( A @ ( C @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ finite_finite1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_finite__Diff__insert) ).
thf(242,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA,C: bool @ ( TA @ fun )] :
( ( ( A @ ( C @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ finite_finite1 ) )
=> ( A @ ( B @ ( TA @ insert ) ) @ ( C @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ finite_finite1 ) ) )
& ( ( A @ ( B @ ( TA @ insert ) ) @ ( C @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ finite_finite1 ) )
=> ( A @ ( C @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ finite_finite1 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(94,axiom,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A
!= ( bool @ ( TA @ fun ) @ bot_bot ) )
<=> ? [B: TA,C: bool @ ( TA @ fun )] :
( ~ ( C @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
& ( A
= ( C @ ( B @ ( TA @ insert ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_nonempty__iff) ).
thf(506,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( ? [B: TA,C: bool @ ( TA @ fun )] :
( ~ ( C @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
& ( A
= ( C @ ( B @ ( TA @ insert ) ) ) ) )
=> ( A
!= ( bool @ ( TA @ fun ) @ bot_bot ) ) )
& ( ( A
!= ( bool @ ( TA @ fun ) @ bot_bot ) )
=> ? [B: TA,C: bool @ ( TA @ fun )] :
( ~ ( C @ ( B @ ( TA @ member @ ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ aa ) ) ) @ ( bool @ ( bool @ ( TA @ fun ) @ aa ) ) ) @ pp )
& ( A
= ( C @ ( B @ ( TA @ insert ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).
thf(38,axiom,
! [A: bool,B: bool] :
( ( B @ ( A @ ( fdisj @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp )
| ~ ( B @ pp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fdisj_2_1_U) ).
thf(268,plain,
! [A: bool,B: bool] :
( ( B @ ( A @ ( fdisj @ ( bool @ ( bool @ fun ) @ ( bool @ aa ) ) ) @ ( bool @ ( bool @ aa ) ) ) @ pp )
| ~ ( B @ pp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(115,axiom,
! [TA: $tType,A: bool @ ( TA @ hoare_28830079triple @ fun ),B: bool @ ( TA @ hoare_28830079triple @ fun ),C: bool @ ( TA @ hoare_28830079triple @ fun )] :
( ( B @ ( C @ ( TA @ hoare_992312373derivs ) ) )
=> ( ( C @ ( A @ ( TA @ hoare_992312373derivs ) ) )
=> ( B @ ( A @ ( TA @ hoare_992312373derivs ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_cut) ).
thf(575,plain,
! [TA: $tType,A: bool @ ( TA @ hoare_28830079triple @ fun ),B: bool @ ( TA @ hoare_28830079triple @ fun ),C: bool @ ( TA @ hoare_28830079triple @ fun )] :
( ( B @ ( C @ ( TA @ hoare_992312373derivs ) ) )
=> ( ( C @ ( A @ ( TA @ hoare_992312373derivs ) ) )
=> ( B @ ( A @ ( TA @ hoare_992312373derivs ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[115]) ).
thf(98,axiom,
! [TA: $tType,TB: $tType] :
( ( TA @ bot )
=> ! [A: TB] :
( ( A @ ( TA @ ( TB @ fun ) @ bot_bot @ ( TA @ ( TB @ aa ) ) ) )
= ( TA @ bot_bot ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_bot__fun__def) ).
thf(528,plain,
! [TA: $tType,TB: $tType] :
( ( TA @ bot )
=> ! [A: TB] :
( ( A @ ( TA @ ( TB @ fun ) @ bot_bot @ ( TA @ ( TB @ aa ) ) ) )
= ( TA @ bot_bot ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[98]) ).
thf(1511,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( ( bool @ ( TB @ fun ) @ bot_bot )
!= ( bool @ ( TB @ fun ) @ bot_bot ) )
| ( ( A @ ( A @ ( bool @ ( TB @ fun ) @ minus_minus ) ) @ ( TB @ collect ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ) ),
inference(paramod_ordered,[status(thm)],[562,718]) ).
thf(1512,plain,
! [TB: $tType,A: bool @ ( TB @ fun )] :
( ( A @ ( A @ ( bool @ ( TB @ fun ) @ minus_minus ) ) @ ( TB @ collect ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ),
inference(pattern_uni,[status(thm)],[1511:[]]) ).
thf(1550,plain,
! [TA: $tType,A: bool @ ( TA @ fun )] :
( ( A @ ( A @ ( bool @ ( TA @ fun ) @ minus_minus ) ) @ ( TA @ collect ) )
= ( bool @ ( TA @ fun ) @ bot_bot ) ),
inference(simp,[status(thm)],[1512]) ).
thf(63,axiom,
bool @ bot,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_HOL_Obool___Orderings_Obot) ).
thf(369,plain,
bool @ bot,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(119,axiom,
! [TA: $tType,TB: $tType] :
( ( TB @ cl_Groups_Ominus )
=> ! [A: TB @ ( TA @ fun ),B: TB @ ( TA @ fun ),C: TA] :
( ( C @ ( A @ ( B @ ( TB @ ( TA @ fun ) @ minus_minus ) ) @ ( TB @ ( TA @ aa ) ) ) )
= ( C @ ( A @ ( TB @ ( TA @ aa ) ) ) @ ( C @ ( B @ ( TB @ ( TA @ aa ) ) ) @ ( TB @ minus_minus ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_fun__diff__def) ).
thf(607,plain,
! [TA: $tType,TB: $tType] :
( ( TB @ cl_Groups_Ominus )
=> ! [A: TB @ ( TA @ fun ),B: TB @ ( TA @ fun ),C: TA] :
( ( C @ ( A @ ( B @ ( TB @ ( TA @ fun ) @ minus_minus ) ) @ ( TB @ ( TA @ aa ) ) ) )
= ( C @ ( A @ ( TB @ ( TA @ aa ) ) ) @ ( C @ ( B @ ( TB @ ( TA @ aa ) ) ) @ ( TB @ minus_minus ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[119]) ).
thf(8124,plain,
! [TA: $tType,TB: $tType,A: TA] :
( ( fFalse != fFalse )
| ( ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ) ),
inference(paramod_ordered,[status(thm)],[8036,701]) ).
thf(8125,plain,
! [TA: $tType,TB: $tType,A: TA] :
( ( A @ ( bool @ ( TA @ fun ) @ bot_bot @ ( bool @ ( TA @ aa ) ) ) @ ( TB @ ( bool @ combk ) ) )
= ( bool @ ( TB @ fun ) @ bot_bot ) ),
inference(pattern_uni,[status(thm)],[8124:[]]) ).
thf(23,axiom,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA,C: TA] :
( ( A @ ( B @ ( TA @ insert ) ) @ ( C @ ( TA @ insert ) ) )
= ( A @ ( C @ ( TA @ insert ) ) @ ( B @ ( TA @ insert ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_insert__commute) ).
thf(215,plain,
! [TA: $tType,A: bool @ ( TA @ fun ),B: TA,C: TA] :
( ( A @ ( B @ ( TA @ insert ) ) @ ( C @ ( TA @ insert ) ) )
= ( A @ ( C @ ( TA @ insert ) ) @ ( B @ ( TA @ insert ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(61,axiom,
! [TA: $tType,A: com,B: com,C: TA @ ( nat @ ( state @ fun ) @ fun ) @ ( pname @ fun ) @ ( vname @ fun ),D: TA @ ( pname @ fun ),E: TA @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ fun ),F: TA @ ( com @ fun ) @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ fun ),G: TA @ ( com @ fun ) @ ( com @ fun ),H: TA @ ( com @ fun ) @ ( nat @ ( state @ fun ) @ fun ) @ ( loc @ fun ),I: TA @ ( nat @ ( state @ fun ) @ fun ) @ ( vname @ fun ),J: TA] :
( ( A @ ( B @ semi ) @ ( C @ ( D @ ( E @ ( F @ ( G @ ( H @ ( I @ ( J @ ( TA @ com_case ) ) ) ) ) ) ) ) ) )
= ( A @ ( B @ ( G @ ( TA @ ( com @ fun ) @ ( com @ aa ) ) ) @ ( TA @ ( com @ aa ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_com_Osimps_I67_J) ).
thf(364,plain,
! [TA: $tType,A: com,B: com,C: TA @ ( nat @ ( state @ fun ) @ fun ) @ ( pname @ fun ) @ ( vname @ fun ),D: TA @ ( pname @ fun ),E: TA @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ fun ),F: TA @ ( com @ fun ) @ ( com @ fun ) @ ( bool @ ( state @ fun ) @ fun ),G: TA @ ( com @ fun ) @ ( com @ fun ),H: TA @ ( com @ fun ) @ ( nat @ ( state @ fun ) @ fun ) @ ( loc @ fun ),I: TA @ ( nat @ ( state @ fun ) @ fun ) @ ( vname @ fun ),J: TA] :
( ( A @ ( B @ semi ) @ ( C @ ( D @ ( E @ ( F @ ( G @ ( H @ ( I @ ( J @ ( TA @ com_case ) ) ) ) ) ) ) ) ) )
= ( A @ ( B @ ( G @ ( TA @ ( com @ fun ) @ ( com @ aa ) ) ) @ ( TA @ ( com @ aa ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(50024,plain,
$false,
inference(e,[status(thm)],[2031,1767,249,555,1211,523,308,449,440,202,1855,1200,408,170,614,677,384,550,142,340,670,1867,500,538,153,174,185,288,1904,257,565,1366,389,719,619,638,11609,1115,289,1815,1847,316,1362,2027,443,321,376,7986,1858,147,397,692,293,1796,132,428,206,1697,265,307,1074,233,678,270,7078,334,302,392,630,165,1123,862,275,137,197,8048,625,852,1819,847,484,1089,650,156,1540,610,980,403,256,193,489,2038,547,212,706,701,515,8036,7086,569,1202,541,398,558,718,926,134,1333,750,166,8040,161,1301,601,180,296,562,176,191,5121,577,291,545,259,641,382,572,6991,181,540,1865,498,604,187,172,219,2151,1894,230,362,318,616,208,1801,434,387,367,535,140,7098,1344,330,7978,520,695,1364,851,1805,135,1113,563,473,2054,7371,617,355,553,194,162,531,209,487,1845,295,282,971,327,739,263,199,331,370,1538,7398,177,182,544,907,175,446,612,143,497,465,627,7177,7904,1817,891,218,186,632,401,139,433,346,235,246,716,214,432,410,146,405,1876,183,1757,4597,373,7048,300,305,210,136,358,635,720,239,242,506,268,395,575,528,1550,163,178,369,607,803,8125,215,560,496,364]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW508_5 : TPTP v9.3.1. Released v6.0.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.16/0.41 % Computer : n007.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Sat Sep 26 16:07:54 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.16/0.41 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.88/0.99 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.91/1.34 % [INFO] Parsing done (348ms).
% 1.91/1.35 % [INFO] Running in sequential loop mode.
% 2.77/1.74 % [INFO] eprover registered as external prover.
% 2.77/1.75 % [INFO] Scanning for conjecture ...
% 3.22/1.97 % [INFO] Found a conjecture (or negated_conjecture) and 129 axioms. Running axiom selection ...
% 3.58/2.13 % [INFO] Axiom selection finished. Selected 129 axioms (removed 0 axioms).
% 4.99/2.40 % [INFO] Problem is typed first-order (TPTP TFF).
% 4.99/2.44 % [INFO] Type checking passed.
% 4.99/2.44 % [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 ...
% 5.75/2.69 % [INFO] [Domain constraints] Detected constraint on bool
% 5.75/2.69 % [INFO] [Domain constraints] dom(bool) ⊆ {fTrue,fFalse}
% 226.94/79.03 % External prover 'e' found a proof!
% 226.94/79.03 % [INFO] Killing All external provers ...
% 226.94/79.04 % Time passed: 78488ms (effective reasoning time: 77678ms)
% 226.94/79.04 % 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)>
% 226.94/79.04 % Axioms used in derivation (129): help_fimplies_2_1_U, fact_48_fold1Set__sing, arity_HOL_Obool___Finite__Set_Ofinite, fact_86_finite_OemptyI, fact_32_insert__not__empty, fact_7_insertCI, help_COMBS_1_1_U, fact_4_insert__absorb2, fact_92_finite, fact_58_DiffI, fact_70_empty__fold__graphE, fact_88_finite__insert, help_fconj_3_1_U, fact_80_fold1Set_Osimps, arity_fun___Orderings_Obot, fact_12_emptyE, fact_66_DiffD2, fact_30_doubleton__eq__iff, fact_23_insert__code, fact_64_insert__Diff__if, fact_3_hoare__derivs_Oinsert, fact_35_bot__fun__def, fact_20_insertI2, arity_HOL_Obool___Groups_Ominus, fact_98_finite_Osimps, fact_68_set__diff__eq, fact_27_insertI1, fact_61_empty__Diff, fact_21_insert__eq__iff, fact_73_Diff__insert__absorb, help_fNot_2_1_U, fact_53_fold1Set_Ointros, fact_11_Collect__empty__eq, fact_5_insert__iff, fact_41_com_Osimps_I3_J, fact_16_equals0D, fact_1_empty, fact_29_singletonE, fact_6_insertE, fact_14_triple_Osimps_I2_J, help_fNot_1_1_U, fact_71_fold__graph_OinsertI, help_fFalse_1_1_T, fact_13_triple_Orecs, fact_2_cut, fact_38_triple_Oexhaust, fact_59_Diff__idemp, fact_0_triple_Oinject, help_COMBB_1_1_U, fact_19_insert__absorb, help_fdisj_1_1_U, fact_15_empty__not__insert, fact_62_Diff__cancel, fact_25_insert__Collect, fact_95_folding__one_Oclosed, fact_55_in__inv__imagep, help_fconj_2_1_U, fact_40_mk__disjoint__insert, fact_10_empty__iff, fact_44_equals0I, fact_49_com_Osimps_I64_J, fact_65_insert__Diff1, fact_22_insert__ident, fact_26_insert__compr, fact_81_fun__diff__def, fact_8_all__not__in__conv, help_fequal_1_1_T, fact_60_Diff__iff, fact_93_folding__one_Oinsert, fact_18_empty__def, fact_67_DiffD1, fact_79_insert__fold1SetE, fact_24_insert__commute, arity_fun___Finite__Set_Ofinite, fact_76_mem__def, fact_52_com_Osimps_I67_J, fact_31_singleton__iff, help_fdisj_2_1_U, help_COMBK_1_1_U, fact_46_nonempty__iff, fact_85_finite__code, fact_34_bot__apply, fact_33_the__elem__eq, fact_83_fold__graph_Osimps, fact_47_bot__empty__eq, help_COMBC_1_1_U, arity_HOL_Obool___Orderings_Obot, conj_1, help_fequal_2_1_T, help_fconj_1_1_U, help_fdisj_3_1_U, fact_84_folding__one_Oremove, fact_78_Diff__insert, fact_89_finite__Diff, fact_99_finite__induct, help_fFalse_1_1_U, fact_50_fold1Set__nonempty, fact_9_empty__Collect__eq, fact_63_Diff__empty, fact_77_Collect__def, fact_45_conseq, fact_51_empty__fold1SetE, help_pp_1_1_U, fact_42_com_Osimps_I13_J, fact_36_hoare__derivs_OSkip, fact_97_finite__nonempty__imp__fold1Set, fact_54_folding__one_Osingleton, fact_91_finite__Diff2, help_fimplies_1_1_U, fact_96_finite__empty__induct, fact_43_com_Osimps_I12_J, fact_57_DiffE, fact_56_insert__Diff__single, fact_17_ex__in__conv, fact_75_ext, fact_39_Set_Oset__insert, fact_28_singleton__inject, help_fimplies_3_1_U, conj_0, fact_69_fold__graph_OemptyI, help_pp_2_1_U, fact_94_folding__one_Oinsert__remove, fact_72_insert__Diff, fact_74_Diff__insert2, arity_fun___Groups_Ominus, fact_82_minus__apply, fact_37_Comp, fact_90_finite__Diff__insert, fact_87_finite_OinsertI
% 226.94/79.04 % No. of inferences in proof: 560
% 226.94/79.04 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 78488 ms resp. 77678 ms w/o parsing
% 226.19/79.36 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 226.19/79.36 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------