%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : ITP077^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Oct 7 10:24:01 AM UTC 2026
% Result : Theorem 3.76s 0.84s
% Output : CNFRefutation 3.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 13
% Syntax : Number of formulae : 98 ( 68 unt; 0 typ; 0 def)
% Number of atoms : 473 ( 203 equ; 0 cnn)
% Maximal formula atoms : 5 ( 4 avg)
% Number of connectives : 698 ( 86 ~; 90 |; 0 &; 501 @)
% ( 0 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Number of types : 44 ( 43 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 147 ( 144 usr; 9 con; 0-3 aty)
% Number of variables : 159 ( 11 ^; 148 !; 0 ?; 159 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_a,type,
a: $tType ).
thf(tp_list_a,type,
list_a: $tType ).
thf(tp_list_list_a,type,
list_list_a: $tType ).
thf(tp_list_list_list_a,type,
list_list_list_a: $tType ).
thf(tp_list_list_set_a,type,
list_list_set_a: $tType ).
thf(tp_list_multiset_a,type,
list_multiset_a: $tType ).
thf(tp_list_multiset_list_a,type,
list_multiset_list_a: $tType ).
thf(tp_list_nat,type,
list_nat: $tType ).
thf(tp_list_set_a,type,
list_set_a: $tType ).
thf(tp_list_set_list_a,type,
list_set_list_a: $tType ).
thf(tp_list_set_list_list_a,type,
list_set_list_list_a: $tType ).
thf(tp_list_set_list_set_a,type,
list_set_list_set_a: $tType ).
thf(tp_list_set_multiset_a,type,
list_set_multiset_a: $tType ).
thf(tp_list_set_nat,type,
list_set_nat: $tType ).
thf(tp_list_set_set_a,type,
list_set_set_a: $tType ).
thf(tp_list_set_set_list_a,type,
list_set_set_list_a: $tType ).
thf(tp_list_set_set_set_a,type,
list_set_set_set_a: $tType ).
thf(tp_multis971982480list_a,type,
multis971982480list_a: $tType ).
thf(tp_multiset_a,type,
multiset_a: $tType ).
thf(tp_multiset_list_a,type,
multiset_list_a: $tType ).
thf(tp_multiset_multiset_a,type,
multiset_multiset_a: $tType ).
thf(tp_multiset_nat,type,
multiset_nat: $tType ).
thf(tp_multiset_set_a,type,
multiset_set_a: $tType ).
thf(tp_multiset_set_list_a,type,
multiset_set_list_a: $tType ).
thf(tp_multiset_set_set_a,type,
multiset_set_set_a: $tType ).
thf(tp_nat,type,
nat: $tType ).
thf(tp_set_a,type,
set_a: $tType ).
thf(tp_set_list_a,type,
set_list_a: $tType ).
thf(tp_set_list_list_a,type,
set_list_list_a: $tType ).
thf(tp_set_list_list_list_a,type,
set_list_list_list_a: $tType ).
thf(tp_set_list_list_set_a,type,
set_list_list_set_a: $tType ).
thf(tp_set_list_multiset_a,type,
set_list_multiset_a: $tType ).
thf(tp_set_list_nat,type,
set_list_nat: $tType ).
thf(tp_set_list_set_a,type,
set_list_set_a: $tType ).
thf(tp_set_list_set_list_a,type,
set_list_set_list_a: $tType ).
thf(tp_set_list_set_set_a,type,
set_list_set_set_a: $tType ).
thf(tp_set_multiset_a,type,
set_multiset_a: $tType ).
thf(tp_set_multiset_list_a,type,
set_multiset_list_a: $tType ).
thf(tp_set_nat,type,
set_nat: $tType ).
thf(tp_set_set_a,type,
set_set_a: $tType ).
thf(tp_set_set_list_a,type,
set_set_list_a: $tType ).
thf(tp_set_set_nat,type,
set_set_nat: $tType ).
thf(tp_set_set_set_a,type,
set_set_set_a: $tType ).
thf(tp_a2,type,
a2: set_a ).
thf(tp_a3,type,
a3: a ).
thf(tp_bij_be94573046list_a,type,
bij_be94573046list_a: ( list_a > list_a ) > set_list_a > set_list_a > $o ).
thf(tp_bij_betw_a_a,type,
bij_betw_a_a: ( a > a ) > set_a > set_a > $o ).
thf(tp_bij_betw_a_list_a,type,
bij_betw_a_list_a: ( a > list_a ) > set_a > set_list_a > $o ).
thf(tp_bij_betw_list_a_a,type,
bij_betw_list_a_a: ( list_a > a ) > set_list_a > set_a > $o ).
thf(tp_bij_betw_nat_nat,type,
bij_betw_nat_nat: ( nat > nat ) > set_nat > set_nat > $o ).
thf(tp_collect_a,type,
collect_a: ( a > $o ) > set_a ).
thf(tp_collect_list_a,type,
collect_list_a: ( list_a > $o ) > set_list_a ).
thf(tp_collect_list_list_a,type,
collect_list_list_a: ( list_list_a > $o ) > set_list_list_a ).
thf(tp_collect_list_set_a,type,
collect_list_set_a: ( list_set_a > $o ) > set_list_set_a ).
thf(tp_collect_multiset_a,type,
collect_multiset_a: ( multiset_a > $o ) > set_multiset_a ).
thf(tp_collect_nat,type,
collect_nat: ( nat > $o ) > set_nat ).
thf(tp_collect_set_a,type,
collect_set_a: ( set_a > $o ) > set_set_a ).
thf(tp_comm_m1100186507et_nat,type,
comm_m1100186507et_nat: multiset_nat > nat ).
thf(tp_comm_m2145643721iset_a,type,
comm_m2145643721iset_a: multiset_multiset_a > multiset_a ).
thf(tp_comm_m324867663list_a,type,
comm_m324867663list_a: multis971982480list_a > multiset_list_a ).
thf(tp_comm_m543484931mset_a,type,
comm_m543484931mset_a: multiset_a > a ).
thf(tp_f,type,
f: nat > nat ).
thf(tp_g,type,
g: nat > nat ).
thf(tp_groups1271887971list_a,type,
groups1271887971list_a: list_multiset_list_a > multiset_list_a ).
thf(tp_groups1592617181iset_a,type,
groups1592617181iset_a: list_multiset_a > multiset_a ).
thf(tp_groups1792256535list_a,type,
groups1792256535list_a: list_a > a ).
thf(tp_groups921905271st_nat,type,
groups921905271st_nat: list_nat > nat ).
thf(tp_hilber1014902394mp_nat,type,
hilber1014902394mp_nat: set_nat > list_set_nat > $o ).
thf(tp_hilber165648082list_a,type,
hilber165648082list_a: set_a > ( a > list_a ) > list_a > a ).
thf(tp_hilber2024005914iset_a,type,
hilber2024005914iset_a: set_multiset_a > list_set_multiset_a > $o ).
thf(tp_hilber2037636820comp_a,type,
hilber2037636820comp_a: set_a > list_set_a > $o ).
thf(tp_hilber2125729734st_a_a,type,
hilber2125729734st_a_a: set_list_a > ( list_a > a ) > a > list_a ).
thf(tp_hilber815131374at_nat,type,
hilber815131374at_nat: set_nat > ( nat > nat ) > nat > nat ).
thf(tp_hilber921249868list_a,type,
hilber921249868list_a: set_list_a > ( list_a > list_a ) > list_a > list_a ).
thf(tp_hilbert_inv_into_a_a,type,
hilbert_inv_into_a_a: set_a > ( a > a ) > a > a ).
thf(tp_image_a_a,type,
image_a_a: ( a > a ) > set_a > set_a ).
thf(tp_image_a_list_a,type,
image_a_list_a: ( a > list_a ) > set_a > set_list_a ).
thf(tp_image_list_a_a,type,
image_list_a_a: ( list_a > a ) > set_list_a > set_a ).
thf(tp_image_list_a_list_a,type,
image_list_a_list_a: ( list_a > list_a ) > set_list_a > set_list_a ).
thf(tp_image_list_nat_nat,type,
image_list_nat_nat: ( list_nat > nat ) > set_list_nat > set_nat ).
thf(tp_image_nat_nat,type,
image_nat_nat: ( nat > nat ) > set_nat > set_nat ).
thf(tp_inj_on_a_a,type,
inj_on_a_a: ( a > a ) > set_a > $o ).
thf(tp_inj_on_a_list_a,type,
inj_on_a_list_a: ( a > list_a ) > set_a > $o ).
thf(tp_inj_on_list_a_a,type,
inj_on_list_a_a: ( list_a > a ) > set_list_a > $o ).
thf(tp_inj_on_list_a_list_a,type,
inj_on_list_a_list_a: ( list_a > list_a ) > set_list_a > $o ).
thf(tp_inj_on_nat_nat,type,
inj_on_nat_nat: ( nat > nat ) > set_nat > $o ).
thf(tp_list_ex_a,type,
list_ex_a: ( a > $o ) > list_a > $o ).
thf(tp_list_ex_set_a,type,
list_ex_set_a: ( set_a > $o ) > list_set_a > $o ).
thf(tp_list_update_a,type,
list_update_a: list_a > nat > a > list_a ).
thf(tp_list_update_set_a,type,
list_update_set_a: list_set_a > nat > set_a > list_set_a ).
thf(tp_listset_a,type,
listset_a: list_set_a > set_list_a ).
thf(tp_listset_list_a,type,
listset_list_a: list_set_list_a > set_list_list_a ).
thf(tp_listset_list_list_a,type,
listset_list_list_a: list_set_list_list_a > set_list_list_list_a ).
thf(tp_listset_list_set_a,type,
listset_list_set_a: list_set_list_set_a > set_list_list_set_a ).
thf(tp_listset_multiset_a,type,
listset_multiset_a: list_set_multiset_a > set_list_multiset_a ).
thf(tp_listset_nat,type,
listset_nat: list_set_nat > set_list_nat ).
thf(tp_listset_set_a,type,
listset_set_a: list_set_set_a > set_list_set_a ).
thf(tp_listset_set_list_a,type,
listset_set_list_a: list_set_set_list_a > set_list_set_list_a ).
thf(tp_listset_set_set_a,type,
listset_set_set_a: list_set_set_set_a > set_list_set_set_a ).
thf(tp_member101195155list_a,type,
member101195155list_a: list_set_list_a > set_list_set_list_a > $o ).
thf(tp_member1511395513list_a,type,
member1511395513list_a: list_list_list_a > set_list_list_list_a > $o ).
thf(tp_member518144627iset_a,type,
member518144627iset_a: list_multiset_a > set_list_multiset_a > $o ).
thf(tp_member528267379list_a,type,
member528267379list_a: multiset_list_a > set_multiset_list_a > $o ).
thf(tp_member814963949_set_a,type,
member814963949_set_a: list_set_set_a > set_list_set_set_a > $o ).
thf(tp_member954073875_set_a,type,
member954073875_set_a: list_list_set_a > set_list_list_set_a > $o ).
thf(tp_member_a,type,
member_a: a > set_a > $o ).
thf(tp_member_list_a,type,
member_list_a: list_a > set_list_a > $o ).
thf(tp_member_list_list_a,type,
member_list_list_a: list_list_a > set_list_list_a > $o ).
thf(tp_member_list_nat,type,
member_list_nat: list_nat > set_list_nat > $o ).
thf(tp_member_list_set_a,type,
member_list_set_a: list_set_a > set_list_set_a > $o ).
thf(tp_member_multiset_a,type,
member_multiset_a: multiset_a > set_multiset_a > $o ).
thf(tp_member_nat,type,
member_nat: nat > set_nat > $o ).
thf(tp_member_set_a,type,
member_set_a: set_a > set_set_a > $o ).
thf(tp_member_set_list_a,type,
member_set_list_a: set_list_a > set_set_list_a > $o ).
thf(tp_member_set_nat,type,
member_set_nat: set_nat > set_set_nat > $o ).
thf(tp_member_set_set_a,type,
member_set_set_a: set_set_a > set_set_set_a > $o ).
thf(tp_mset_a,type,
mset_a: list_a > multiset_a ).
thf(tp_mset_list_a,type,
mset_list_a: list_list_a > multiset_list_a ).
thf(tp_mset_multiset_a,type,
mset_multiset_a: list_multiset_a > multiset_multiset_a ).
thf(tp_mset_multiset_list_a,type,
mset_multiset_list_a: list_multiset_list_a > multis971982480list_a ).
thf(tp_mset_nat,type,
mset_nat: list_nat > multiset_nat ).
thf(tp_mset_set_a,type,
mset_set_a: list_set_a > multiset_set_a ).
thf(tp_mset_set_list_a,type,
mset_set_list_a: list_set_list_a > multiset_set_list_a ).
thf(tp_mset_set_set_a,type,
mset_set_set_a: list_set_set_a > multiset_set_set_a ).
thf(tp_nth_a,type,
nth_a: list_a > nat > a ).
thf(tp_nth_list_a,type,
nth_list_a: list_list_a > nat > list_a ).
thf(tp_nth_list_list_a,type,
nth_list_list_a: list_list_list_a > nat > list_list_a ).
thf(tp_nth_list_set_a,type,
nth_list_set_a: list_list_set_a > nat > list_set_a ).
thf(tp_nth_multiset_a,type,
nth_multiset_a: list_multiset_a > nat > multiset_a ).
thf(tp_nth_nat,type,
nth_nat: list_nat > nat > nat ).
thf(tp_nth_set_a,type,
nth_set_a: list_set_a > nat > set_a ).
thf(tp_nth_set_list_a,type,
nth_set_list_a: list_set_list_a > nat > set_list_a ).
thf(tp_nth_set_list_list_a,type,
nth_set_list_list_a: list_set_list_list_a > nat > set_list_list_a ).
thf(tp_nth_set_list_set_a,type,
nth_set_list_set_a: list_set_list_set_a > nat > set_list_set_a ).
thf(tp_nth_set_multiset_a,type,
nth_set_multiset_a: list_set_multiset_a > nat > set_multiset_a ).
thf(tp_nth_set_nat,type,
nth_set_nat: list_set_nat > nat > set_nat ).
thf(tp_nth_set_set_a,type,
nth_set_set_a: list_set_set_a > nat > set_set_a ).
thf(tp_nth_set_set_list_a,type,
nth_set_set_list_a: list_set_set_list_a > nat > set_set_list_a ).
thf(tp_nth_set_set_set_a,type,
nth_set_set_set_a: list_set_set_set_a > nat > set_set_set_a ).
thf(tp_ord_le1301786372list_a,type,
ord_le1301786372list_a: set_list_a > set_list_a > $o ).
thf(tp_ord_less_eq_nat,type,
ord_less_eq_nat: nat > nat > $o ).
thf(tp_ord_less_eq_o_nat,type,
ord_less_eq_o_nat: ( $o > nat ) > ( $o > nat ) > $o ).
thf(tp_ord_less_eq_set_a,type,
ord_less_eq_set_a: set_a > set_a > $o ).
thf(tp_ord_less_eq_set_nat,type,
ord_less_eq_set_nat: set_nat > set_nat > $o ).
thf(tp_ord_less_nat,type,
ord_less_nat: nat > nat > $o ).
thf(tp_ord_less_set_a,type,
ord_less_set_a: set_a > set_a > $o ).
thf(tp_ord_less_set_list_a,type,
ord_less_set_list_a: set_list_a > set_list_a > $o ).
thf(tp_ord_less_set_nat,type,
ord_less_set_nat: set_nat > set_nat > $o ).
thf(tp_perm_a,type,
perm_a: list_a > list_a > $o ).
thf(tp_perm_set_a,type,
perm_set_a: list_set_a > list_set_a > $o ).
thf(tp_qs,type,
qs: list_a ).
thf(tp_qs2,type,
qs2: list_a ).
thf(tp_rev_a,type,
rev_a: list_a > list_a ).
thf(tp_rev_list_a,type,
rev_list_a: list_list_a > list_list_a ).
thf(tp_rev_nat,type,
rev_nat: list_nat > list_nat ).
thf(tp_rev_set_a,type,
rev_set_a: list_set_a > list_set_a ).
thf(tp_rev_set_list_a,type,
rev_set_list_a: list_set_list_a > list_set_list_a ).
thf(tp_rev_set_set_a,type,
rev_set_set_a: list_set_set_a > list_set_set_a ).
thf(tp_sK1_SX0,type,
sK1_SX0: list_a ).
thf(tp_set_ms1660427399list_a,type,
set_ms1660427399list_a: multis971982480list_a > set_multiset_list_a ).
thf(tp_set_mset_a,type,
set_mset_a: multiset_a > set_a ).
thf(tp_set_mset_list_a,type,
set_mset_list_a: multiset_list_a > set_list_a ).
thf(tp_set_mset_multiset_a,type,
set_mset_multiset_a: multiset_multiset_a > set_multiset_a ).
thf(tp_set_mset_set_a,type,
set_mset_set_a: multiset_set_a > set_set_a ).
thf(tp_set_or1164043265_set_a,type,
set_or1164043265_set_a: set_a > set_set_a ).
thf(tp_set_or1578766727list_a,type,
set_or1578766727list_a: set_list_a > set_set_list_a ).
thf(tp_set_or1597314339et_nat,type,
set_or1597314339et_nat: set_nat > set_set_nat ).
thf(tp_set_ord_lessThan_nat,type,
set_ord_lessThan_nat: nat > set_nat ).
thf(tp_size_s1427607542list_a,type,
size_s1427607542list_a: list_list_a > nat ).
thf(tp_size_s1635937238list_a,type,
size_s1635937238list_a: list_set_list_a > nat ).
thf(tp_size_s1657263798iset_a,type,
size_s1657263798iset_a: list_multiset_a > nat ).
thf(tp_size_s240404444list_a,type,
size_s240404444list_a: list_set_list_list_a > nat ).
thf(tp_size_s341332310_set_a,type,
size_s341332310_set_a: list_list_set_a > nat ).
thf(tp_size_s469631926list_a,type,
size_s469631926list_a: list_set_set_list_a > nat ).
thf(tp_size_s575106428list_a,type,
size_s575106428list_a: list_list_list_a > nat ).
thf(tp_size_s577819178et_nat,type,
size_s577819178et_nat: list_set_nat > nat ).
thf(tp_size_s657334288_set_a,type,
size_s657334288_set_a: multiset_set_a > nat ).
thf(tp_size_s726512144_set_a,type,
size_s726512144_set_a: list_set_set_set_a > nat ).
thf(tp_size_s739728560_set_a,type,
size_s739728560_set_a: list_set_set_a > nat ).
thf(tp_size_s802269334iset_a,type,
size_s802269334iset_a: list_set_multiset_a > nat ).
thf(tp_size_s926492982_set_a,type,
size_s926492982_set_a: list_set_list_set_a > nat ).
thf(tp_size_size_list_a,type,
size_size_list_a: list_a > nat ).
thf(tp_size_size_list_nat,type,
size_size_list_nat: list_nat > nat ).
thf(tp_size_size_list_set_a,type,
size_size_list_set_a: list_set_a > nat ).
thf(tp_size_size_multiset_a,type,
size_size_multiset_a: multiset_a > nat ).
thf(tp_ss1,type,
ss1: list_set_a ).
thf(tp_ss2,type,
ss2: list_set_a ).
thf(93,axiom,
! [A: set_a,Ss: list_set_a] :
( ( hilber2037636820comp_a @ A @ Ss )
=> ( inj_on_list_a_a @ groups1792256535list_a @ ( listset_a @ Ss ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_260_direct__decompD_I2_J) ).
thf(171,axiom,
( hilber2037636820comp_a
= ( ^ [A4: set_a,Ss2: list_set_a] : ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ Ss2 ) @ A4 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_direct__decomp__def) ).
thf(327,axiom,
! [A: set_a,Ss: list_set_a] :
( ( hilber2037636820comp_a @ A @ Ss )
=> ( ( image_list_a_a @ groups1792256535list_a @ ( listset_a @ Ss ) )
= A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_direct__decompD_I3_J) ).
thf(329,axiom,
! [Xs: list_a] :
( ( comm_m543484931mset_a @ ( mset_a @ Xs ) )
= ( groups1792256535list_a @ Xs ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_sum__mset__sum__list) ).
thf(335,axiom,
! [Xs: list_a] :
( ( groups1792256535list_a @ ( rev_a @ Xs ) )
= ( groups1792256535list_a @ Xs ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_sum__list_Orev) ).
thf(337,axiom,
! [A: set_a,Ss: list_set_a,Qs2: list_a,Qs3: list_a] :
( ( hilber2037636820comp_a @ A @ Ss )
=> ( ( member_list_a @ Qs2 @ ( listset_a @ Ss ) )
=> ( ( member_list_a @ Qs3 @ ( listset_a @ Ss ) )
=> ( ( ( groups1792256535list_a @ Qs2 )
= ( groups1792256535list_a @ Qs3 ) )
=> ( Qs2 = Qs3 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_direct__decomp__unique) ).
thf(348,axiom,
member_list_a @ qs2 @ ( listset_a @ ss2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_qs2__in) ).
thf(349,axiom,
~ ! [Qs: list_a] :
( ( a3
= ( groups1792256535list_a @ Qs ) )
=> ~ ( member_list_a @ Qs @ ( listset_a @ ss1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062qs_O_A_092_060lbrakk_062a_A_061_Asum__list_Aqs_059_Aqs_A_092_060in_062_Alistset_Ass1_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062) ).
thf(350,axiom,
( ( size_size_list_a @ qs2 )
= ( size_size_list_a @ qs ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_len__qs2) ).
thf(351,axiom,
( a3
= ( groups1792256535list_a @ qs ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_a) ).
thf(352,axiom,
member_a @ a3 @ a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1__092_060open_062a_A_092_060in_062_AA_092_060close_062) ).
thf(353,axiom,
( ( mset_a @ qs2 )
= ( mset_a @ qs ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0__092_060open_062mset_Aqs2_A_061_Amset_Aqs_092_060close_062) ).
thf(354,conjecture,
( a3
= ( groups1792256535list_a @ qs2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
thf(355,negated_conjecture,
( ( a3
= ( groups1792256535list_a @ qs2 ) )
= $false ),
inference(negate_conjecture,[status(cth)],[354]) ).
thf(356,plain,
( ( a3
= ( groups1792256535list_a @ qs2 ) )
= $false ),
inference(unfold_def,[status(thm)],[355]) ).
thf(357,plain,
( ( ! [A: set_a,Ss: list_set_a] :
( ( hilber2037636820comp_a @ A @ Ss )
=> ( inj_on_list_a_a @ groups1792256535list_a @ ( listset_a @ Ss ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[93]) ).
thf(358,plain,
( ( hilber2037636820comp_a
= ( ^ [A4: set_a,Ss2: list_set_a] : ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ Ss2 ) @ A4 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[171]) ).
thf(359,plain,
( ( ! [A: set_a,Ss: list_set_a] :
( ( hilber2037636820comp_a @ A @ Ss )
=> ( ( image_list_a_a @ groups1792256535list_a @ ( listset_a @ Ss ) )
= A ) ) )
= $true ),
inference(unfold_def,[status(thm)],[327]) ).
thf(360,plain,
( ( ! [Xs: list_a] :
( ( comm_m543484931mset_a @ ( mset_a @ Xs ) )
= ( groups1792256535list_a @ Xs ) ) )
= $true ),
inference(unfold_def,[status(thm)],[329]) ).
thf(361,plain,
( ( ! [Xs: list_a] :
( ( groups1792256535list_a @ ( rev_a @ Xs ) )
= ( groups1792256535list_a @ Xs ) ) )
= $true ),
inference(unfold_def,[status(thm)],[335]) ).
thf(362,plain,
( ( ! [A: set_a,Ss: list_set_a,Qs2: list_a,Qs3: list_a] :
( ( hilber2037636820comp_a @ A @ Ss )
=> ( ( member_list_a @ Qs2 @ ( listset_a @ Ss ) )
=> ( ( member_list_a @ Qs3 @ ( listset_a @ Ss ) )
=> ( ( ( groups1792256535list_a @ Qs2 )
= ( groups1792256535list_a @ Qs3 ) )
=> ( Qs2 = Qs3 ) ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[337]) ).
thf(363,plain,
( ( member_list_a @ qs2 @ ( listset_a @ ss2 ) )
= $true ),
inference(unfold_def,[status(thm)],[348]) ).
thf(364,plain,
( ( ~ ! [Qs: list_a] :
( ( a3
= ( groups1792256535list_a @ Qs ) )
=> ~ ( member_list_a @ Qs @ ( listset_a @ ss1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[349]) ).
thf(365,plain,
( ( ( size_size_list_a @ qs2 )
= ( size_size_list_a @ qs ) )
= $true ),
inference(unfold_def,[status(thm)],[350]) ).
thf(366,plain,
( ( a3
= ( groups1792256535list_a @ qs ) )
= $true ),
inference(unfold_def,[status(thm)],[351]) ).
thf(367,plain,
( ( member_a @ a3 @ a2 )
= $true ),
inference(unfold_def,[status(thm)],[352]) ).
thf(368,plain,
( ( ( mset_a @ qs2 )
= ( mset_a @ qs ) )
= $true ),
inference(unfold_def,[status(thm)],[353]) ).
thf(369,plain,
( ( a3
!= ( groups1792256535list_a @ qs2 ) )
= $true ),
inference(polarity_switch,[status(thm)],[356]) ).
thf(370,plain,
( ( ( mset_a @ qs2 )
= ( mset_a @ qs ) )
= $true ),
inference(copy,[status(thm)],[368]) ).
thf(371,plain,
( ( member_a @ a3 @ a2 )
= $true ),
inference(copy,[status(thm)],[367]) ).
thf(372,plain,
( ( a3
= ( groups1792256535list_a @ qs ) )
= $true ),
inference(copy,[status(thm)],[366]) ).
thf(373,plain,
( ( ( size_size_list_a @ qs2 )
= ( size_size_list_a @ qs ) )
= $true ),
inference(copy,[status(thm)],[365]) ).
thf(374,plain,
( ( ~ ! [Qs: list_a] :
( ( a3
= ( groups1792256535list_a @ Qs ) )
=> ~ ( member_list_a @ Qs @ ( listset_a @ ss1 ) ) ) )
= $true ),
inference(copy,[status(thm)],[364]) ).
thf(375,plain,
( ( member_list_a @ qs2 @ ( listset_a @ ss2 ) )
= $true ),
inference(copy,[status(thm)],[363]) ).
thf(376,plain,
( ( ! [A: set_a,Ss: list_set_a,Qs2: list_a,Qs3: list_a] :
( ( hilber2037636820comp_a @ A @ Ss )
=> ( ( member_list_a @ Qs2 @ ( listset_a @ Ss ) )
=> ( ( member_list_a @ Qs3 @ ( listset_a @ Ss ) )
=> ( ( ( groups1792256535list_a @ Qs2 )
= ( groups1792256535list_a @ Qs3 ) )
=> ( Qs2 = Qs3 ) ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[362]) ).
thf(377,plain,
( ( ! [Xs: list_a] :
( ( groups1792256535list_a @ ( rev_a @ Xs ) )
= ( groups1792256535list_a @ Xs ) ) )
= $true ),
inference(copy,[status(thm)],[361]) ).
thf(378,plain,
( ( ! [Xs: list_a] :
( ( comm_m543484931mset_a @ ( mset_a @ Xs ) )
= ( groups1792256535list_a @ Xs ) ) )
= $true ),
inference(copy,[status(thm)],[360]) ).
thf(379,plain,
( ( ! [A: set_a,Ss: list_set_a] :
( ( hilber2037636820comp_a @ A @ Ss )
=> ( ( image_list_a_a @ groups1792256535list_a @ ( listset_a @ Ss ) )
= A ) ) )
= $true ),
inference(copy,[status(thm)],[359]) ).
thf(380,plain,
( ( hilber2037636820comp_a
= ( ^ [A4: set_a,Ss2: list_set_a] : ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ Ss2 ) @ A4 ) ) )
= $true ),
inference(copy,[status(thm)],[358]) ).
thf(381,plain,
( ( ! [A: set_a,Ss: list_set_a] :
( ( hilber2037636820comp_a @ A @ Ss )
=> ( inj_on_list_a_a @ groups1792256535list_a @ ( listset_a @ Ss ) ) ) )
= $true ),
inference(copy,[status(thm)],[357]) ).
thf(382,plain,
( ( a3
!= ( groups1792256535list_a @ qs2 ) )
= $true ),
inference(copy,[status(thm)],[369]) ).
thf(383,plain,
( ( ! [SX0: set_a,SX1: list_set_a,SX2: list_a,SX3: list_a] :
( ~ ( hilber2037636820comp_a @ SX0 @ SX1 )
| ~ ( member_list_a @ SX2 @ ( listset_a @ SX1 ) )
| ~ ( member_list_a @ SX3 @ ( listset_a @ SX1 ) )
| ( ( groups1792256535list_a @ SX2 )
!= ( groups1792256535list_a @ SX3 ) )
| ( SX2 = SX3 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[376]) ).
thf(384,plain,
( ( ! [SX0: set_a,SX1: list_set_a] :
( ~ ( hilber2037636820comp_a @ SX0 @ SX1 )
| ( ( image_list_a_a @ groups1792256535list_a @ ( listset_a @ SX1 ) )
= SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[379]) ).
thf(385,plain,
( ( ~ ! [SX0: list_a] :
( ( a3
!= ( groups1792256535list_a @ SX0 ) )
| ~ ( member_list_a @ SX0 @ ( listset_a @ ss1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[374]) ).
thf(386,plain,
( ( ! [SX0: set_a,SX1: list_set_a] :
( ~ ( hilber2037636820comp_a @ SX0 @ SX1 )
| ( inj_on_list_a_a @ groups1792256535list_a @ ( listset_a @ SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[381]) ).
thf(387,plain,
! [SV1: list_a] :
( ( ( groups1792256535list_a @ ( rev_a @ SV1 ) )
= ( groups1792256535list_a @ SV1 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[377]) ).
thf(388,plain,
! [SV2: list_a] :
( ( ( comm_m543484931mset_a @ ( mset_a @ SV2 ) )
= ( groups1792256535list_a @ SV2 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[378]) ).
thf(389,plain,
( ( ! [SV3: set_a] :
( ( hilber2037636820comp_a @ SV3 )
= ( ^ [SY13: list_set_a] : ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SY13 ) @ SV3 ) ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[380]) ).
thf(390,plain,
( ( hilber2037636820comp_a
= ( ^ [A4: set_a,Ss2: list_set_a] : ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ Ss2 ) @ A4 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[380]) ).
thf(391,plain,
( ( a3
= ( groups1792256535list_a @ qs2 ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[382]) ).
thf(392,plain,
! [SV4: set_a] :
( ( ! [SY14: list_set_a,SY15: list_a,SY16: list_a] :
( ~ ( hilber2037636820comp_a @ SV4 @ SY14 )
| ~ ( member_list_a @ SY15 @ ( listset_a @ SY14 ) )
| ~ ( member_list_a @ SY16 @ ( listset_a @ SY14 ) )
| ( ( groups1792256535list_a @ SY15 )
!= ( groups1792256535list_a @ SY16 ) )
| ( SY15 = SY16 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[383]) ).
thf(393,plain,
! [SV5: set_a] :
( ( ! [SY17: list_set_a] :
( ~ ( hilber2037636820comp_a @ SV5 @ SY17 )
| ( ( image_list_a_a @ groups1792256535list_a @ ( listset_a @ SY17 ) )
= SV5 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[384]) ).
thf(394,plain,
( ( ! [SX0: list_a] :
( ( a3
!= ( groups1792256535list_a @ SX0 ) )
| ~ ( member_list_a @ SX0 @ ( listset_a @ ss1 ) ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[385]) ).
thf(395,plain,
! [SV6: set_a] :
( ( ! [SY18: list_set_a] :
( ~ ( hilber2037636820comp_a @ SV6 @ SY18 )
| ( inj_on_list_a_a @ groups1792256535list_a @ ( listset_a @ SY18 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[386]) ).
thf(396,plain,
! [SV7: set_a] :
( ( ( hilber2037636820comp_a @ SV7 )
= ( ^ [SY19: list_set_a] : ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SY19 ) @ SV7 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[389]) ).
thf(397,plain,
! [SV8: list_set_a,SV4: set_a] :
( ( ! [SY20: list_a,SY21: list_a] :
( ~ ( hilber2037636820comp_a @ SV4 @ SV8 )
| ~ ( member_list_a @ SY20 @ ( listset_a @ SV8 ) )
| ~ ( member_list_a @ SY21 @ ( listset_a @ SV8 ) )
| ( ( groups1792256535list_a @ SY20 )
!= ( groups1792256535list_a @ SY21 ) )
| ( SY20 = SY21 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[392]) ).
thf(398,plain,
! [SV9: list_set_a,SV5: set_a] :
( ( ~ ( hilber2037636820comp_a @ SV5 @ SV9 )
| ( ( image_list_a_a @ groups1792256535list_a @ ( listset_a @ SV9 ) )
= SV5 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[393]) ).
thf(399,plain,
( ( ( a3
!= ( groups1792256535list_a @ sK1_SX0 ) )
| ~ ( member_list_a @ sK1_SX0 @ ( listset_a @ ss1 ) ) )
= $false ),
inference(extcnf_forall_neg,[status(esa)],[394]) ).
thf(400,plain,
! [SV10: list_set_a,SV6: set_a] :
( ( ~ ( hilber2037636820comp_a @ SV6 @ SV10 )
| ( inj_on_list_a_a @ groups1792256535list_a @ ( listset_a @ SV10 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[395]) ).
thf(401,plain,
! [SV7: set_a] :
( ( ! [SV11: list_set_a] :
( ( hilber2037636820comp_a @ SV7 @ SV11 )
= ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV11 ) @ SV7 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[396]) ).
thf(402,plain,
! [SV7: set_a] :
( ( ( hilber2037636820comp_a @ SV7 )
= ( ^ [SY19: list_set_a] : ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SY19 ) @ SV7 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[396]) ).
thf(403,plain,
! [SV12: list_a,SV8: list_set_a,SV4: set_a] :
( ( ! [SY22: list_a] :
( ~ ( hilber2037636820comp_a @ SV4 @ SV8 )
| ~ ( member_list_a @ SV12 @ ( listset_a @ SV8 ) )
| ~ ( member_list_a @ SY22 @ ( listset_a @ SV8 ) )
| ( ( groups1792256535list_a @ SV12 )
!= ( groups1792256535list_a @ SY22 ) )
| ( SV12 = SY22 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[397]) ).
thf(404,plain,
! [SV9: list_set_a,SV5: set_a] :
( ( ( ~ ( hilber2037636820comp_a @ SV5 @ SV9 ) )
= $true )
| ( ( ( image_list_a_a @ groups1792256535list_a @ ( listset_a @ SV9 ) )
= SV5 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[398]) ).
thf(405,plain,
( ( a3
!= ( groups1792256535list_a @ sK1_SX0 ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[399]) ).
thf(406,plain,
( ( ~ ( member_list_a @ sK1_SX0 @ ( listset_a @ ss1 ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[399]) ).
thf(407,plain,
! [SV10: list_set_a,SV6: set_a] :
( ( ( ~ ( hilber2037636820comp_a @ SV6 @ SV10 ) )
= $true )
| ( ( inj_on_list_a_a @ groups1792256535list_a @ ( listset_a @ SV10 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[400]) ).
thf(408,plain,
! [SV13: list_set_a,SV7: set_a] :
( ( ( hilber2037636820comp_a @ SV7 @ SV13 )
= ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[401]) ).
thf(409,plain,
! [SV14: list_a,SV12: list_a,SV8: list_set_a,SV4: set_a] :
( ( ~ ( hilber2037636820comp_a @ SV4 @ SV8 )
| ~ ( member_list_a @ SV12 @ ( listset_a @ SV8 ) )
| ~ ( member_list_a @ SV14 @ ( listset_a @ SV8 ) )
| ( ( groups1792256535list_a @ SV12 )
!= ( groups1792256535list_a @ SV14 ) )
| ( SV12 = SV14 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[403]) ).
thf(410,plain,
! [SV9: list_set_a,SV5: set_a] :
( ( ( hilber2037636820comp_a @ SV5 @ SV9 )
= $false )
| ( ( ( image_list_a_a @ groups1792256535list_a @ ( listset_a @ SV9 ) )
= SV5 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[404]) ).
thf(411,plain,
( ( a3
= ( groups1792256535list_a @ sK1_SX0 ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[405]) ).
thf(412,plain,
( ( member_list_a @ sK1_SX0 @ ( listset_a @ ss1 ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[406]) ).
thf(413,plain,
! [SV10: list_set_a,SV6: set_a] :
( ( ( hilber2037636820comp_a @ SV6 @ SV10 )
= $false )
| ( ( inj_on_list_a_a @ groups1792256535list_a @ ( listset_a @ SV10 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[407]) ).
thf(414,plain,
! [SV13: list_set_a,SV7: set_a] :
( ( ~ ( ( hilber2037636820comp_a @ SV7 @ SV13 )
| ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 ) )
| ~ ( ~ ( hilber2037636820comp_a @ SV7 @ SV13 )
| ~ ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[408]) ).
thf(415,plain,
! [SV13: list_set_a,SV7: set_a] :
( ( ( hilber2037636820comp_a @ SV7 @ SV13 )
= ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[408]) ).
thf(416,plain,
! [SV14: list_a,SV12: list_a,SV8: list_set_a,SV4: set_a] :
( ( ( ~ ( hilber2037636820comp_a @ SV4 @ SV8 ) )
= $true )
| ( ( ~ ( member_list_a @ SV12 @ ( listset_a @ SV8 ) )
| ~ ( member_list_a @ SV14 @ ( listset_a @ SV8 ) )
| ( ( groups1792256535list_a @ SV12 )
!= ( groups1792256535list_a @ SV14 ) )
| ( SV12 = SV14 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[409]) ).
thf(417,plain,
! [SV13: list_set_a,SV7: set_a] :
( ( ( ~ ( ( hilber2037636820comp_a @ SV7 @ SV13 )
| ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 ) ) )
= $true )
| ( ( ~ ( ~ ( hilber2037636820comp_a @ SV7 @ SV13 )
| ~ ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[414]) ).
thf(418,plain,
! [SV14: list_a,SV12: list_a,SV8: list_set_a,SV4: set_a] :
( ( ( hilber2037636820comp_a @ SV4 @ SV8 )
= $false )
| ( ( ~ ( member_list_a @ SV12 @ ( listset_a @ SV8 ) )
| ~ ( member_list_a @ SV14 @ ( listset_a @ SV8 ) )
| ( ( groups1792256535list_a @ SV12 )
!= ( groups1792256535list_a @ SV14 ) )
| ( SV12 = SV14 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[416]) ).
thf(419,plain,
! [SV13: list_set_a,SV7: set_a] :
( ( ( ( hilber2037636820comp_a @ SV7 @ SV13 )
| ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 ) )
= $false )
| ( ( ~ ( ~ ( hilber2037636820comp_a @ SV7 @ SV13 )
| ~ ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[417]) ).
thf(420,plain,
! [SV4: set_a,SV14: list_a,SV8: list_set_a,SV12: list_a] :
( ( ( ~ ( member_list_a @ SV12 @ ( listset_a @ SV8 ) ) )
= $true )
| ( ( ~ ( member_list_a @ SV14 @ ( listset_a @ SV8 ) )
| ( ( groups1792256535list_a @ SV12 )
!= ( groups1792256535list_a @ SV14 ) )
| ( SV12 = SV14 ) )
= $true )
| ( ( hilber2037636820comp_a @ SV4 @ SV8 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[418]) ).
thf(421,plain,
! [SV13: list_set_a,SV7: set_a] :
( ( ( hilber2037636820comp_a @ SV7 @ SV13 )
= $false )
| ( ( ~ ( ~ ( hilber2037636820comp_a @ SV7 @ SV13 )
| ~ ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[419]) ).
thf(422,plain,
! [SV7: set_a,SV13: list_set_a] :
( ( ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 )
= $false )
| ( ( ~ ( ~ ( hilber2037636820comp_a @ SV7 @ SV13 )
| ~ ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[419]) ).
thf(423,plain,
! [SV4: set_a,SV14: list_a,SV8: list_set_a,SV12: list_a] :
( ( ( member_list_a @ SV12 @ ( listset_a @ SV8 ) )
= $false )
| ( ( ~ ( member_list_a @ SV14 @ ( listset_a @ SV8 ) )
| ( ( groups1792256535list_a @ SV12 )
!= ( groups1792256535list_a @ SV14 ) )
| ( SV12 = SV14 ) )
= $true )
| ( ( hilber2037636820comp_a @ SV4 @ SV8 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[420]) ).
thf(424,plain,
! [SV13: list_set_a,SV7: set_a] :
( ( ( ~ ( hilber2037636820comp_a @ SV7 @ SV13 )
| ~ ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 ) )
= $false )
| ( ( hilber2037636820comp_a @ SV7 @ SV13 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[421]) ).
thf(425,plain,
! [SV13: list_set_a,SV7: set_a] :
( ( ( ~ ( hilber2037636820comp_a @ SV7 @ SV13 )
| ~ ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 ) )
= $false )
| ( ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[422]) ).
thf(426,plain,
! [SV4: set_a,SV12: list_a,SV8: list_set_a,SV14: list_a] :
( ( ( ~ ( member_list_a @ SV14 @ ( listset_a @ SV8 ) ) )
= $true )
| ( ( ( ( groups1792256535list_a @ SV12 )
!= ( groups1792256535list_a @ SV14 ) )
| ( SV12 = SV14 ) )
= $true )
| ( ( member_list_a @ SV12 @ ( listset_a @ SV8 ) )
= $false )
| ( ( hilber2037636820comp_a @ SV4 @ SV8 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[423]) ).
thf(427,plain,
! [SV13: list_set_a,SV7: set_a] :
( ( ( ~ ( hilber2037636820comp_a @ SV7 @ SV13 ) )
= $false )
| ( ( hilber2037636820comp_a @ SV7 @ SV13 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[424]) ).
thf(428,plain,
! [SV7: set_a,SV13: list_set_a] :
( ( ( ~ ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 ) )
= $false )
| ( ( hilber2037636820comp_a @ SV7 @ SV13 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[424]) ).
thf(429,plain,
! [SV13: list_set_a,SV7: set_a] :
( ( ( ~ ( hilber2037636820comp_a @ SV7 @ SV13 ) )
= $false )
| ( ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[425]) ).
thf(430,plain,
! [SV7: set_a,SV13: list_set_a] :
( ( ( ~ ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 ) )
= $false )
| ( ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[425]) ).
thf(431,plain,
! [SV4: set_a,SV12: list_a,SV8: list_set_a,SV14: list_a] :
( ( ( member_list_a @ SV14 @ ( listset_a @ SV8 ) )
= $false )
| ( ( ( ( groups1792256535list_a @ SV12 )
!= ( groups1792256535list_a @ SV14 ) )
| ( SV12 = SV14 ) )
= $true )
| ( ( member_list_a @ SV12 @ ( listset_a @ SV8 ) )
= $false )
| ( ( hilber2037636820comp_a @ SV4 @ SV8 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[426]) ).
thf(432,plain,
! [SV13: list_set_a,SV7: set_a] :
( ( ( hilber2037636820comp_a @ SV7 @ SV13 )
= $true )
| ( ( hilber2037636820comp_a @ SV7 @ SV13 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[427]) ).
thf(433,plain,
! [SV7: set_a,SV13: list_set_a] :
( ( ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 )
= $true )
| ( ( hilber2037636820comp_a @ SV7 @ SV13 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[428]) ).
thf(434,plain,
! [SV13: list_set_a,SV7: set_a] :
( ( ( hilber2037636820comp_a @ SV7 @ SV13 )
= $true )
| ( ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[429]) ).
thf(435,plain,
! [SV7: set_a,SV13: list_set_a] :
( ( ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 )
= $true )
| ( ( bij_betw_list_a_a @ groups1792256535list_a @ ( listset_a @ SV13 ) @ SV7 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[430]) ).
thf(436,plain,
! [SV4: set_a,SV8: list_set_a,SV14: list_a,SV12: list_a] :
( ( ( ( groups1792256535list_a @ SV12 )
!= ( groups1792256535list_a @ SV14 ) )
= $true )
| ( ( SV12 = SV14 )
= $true )
| ( ( member_list_a @ SV14 @ ( listset_a @ SV8 ) )
= $false )
| ( ( member_list_a @ SV12 @ ( listset_a @ SV8 ) )
= $false )
| ( ( hilber2037636820comp_a @ SV4 @ SV8 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[431]) ).
thf(437,plain,
! [SV4: set_a,SV8: list_set_a,SV14: list_a,SV12: list_a] :
( ( ( ( groups1792256535list_a @ SV12 )
= ( groups1792256535list_a @ SV14 ) )
= $false )
| ( ( SV12 = SV14 )
= $true )
| ( ( member_list_a @ SV14 @ ( listset_a @ SV8 ) )
= $false )
| ( ( member_list_a @ SV12 @ ( listset_a @ SV8 ) )
= $false )
| ( ( hilber2037636820comp_a @ SV4 @ SV8 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[436]) ).
thf(438,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[370,437,435,434,433,432,415,413,412,411,410,402,391,390,388,387,375,373,372,371]) ).
thf(439,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[438]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP077^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.18 % Computer : n016.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Oct 6 11:22:17 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.76/0.84 ..
% 3.76/0.84
% 3.76/0.84 No.of.Axioms: 12
% 3.76/0.84
% 3.76/0.84 Length.of.Defs: 0
% 3.76/0.84
% 3.76/0.84 Contains.Choice.Funs: false
% 3.76/0.84 .....
% 3.76/0.84
% 3.76/0.84 ********************************
% 3.76/0.84 * All subproblems solved! *
% 3.76/0.84 ********************************
% 3.76/0.84 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:12,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:438,loop_count:0,foatp_calls:1,translation:fof_full)
% 3.76/0.84
% 3.76/0.84 %**** Beginning of derivation protocol ****
% 3.76/0.84 % SZS output start CNFRefutation
% See solution above
% 3.76/0.85
% 3.76/0.85 %**** End of derivation protocol ****
% 3.76/0.85 %**** no. of clauses in derivation: 98 ****
% 3.76/0.85 %**** clause counter: 438 ****
% 3.76/0.85
% 3.76/0.85 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:12,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:438,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------