%------------------------------------------------------------------------------
% File : Refute---2015
% Problem : NUM567+3 : TPTP v6.4.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : isabelle tptp_refute %d %s
% Computer : n004.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 16091.75MB
% OS : Linux 3.10.0-327.10.1.el7.x86_64
% CPULimit : 300s
% DateTime : Thu Apr 14 01:56:05 EDT 2016
% Result : Timeout 300.08s
% Output : None
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM567+3 : TPTP v6.4.0. Released v4.0.0.
% 0.00/0.04 % Command : isabelle tptp_refute %d %s
% 0.03/0.23 % Computer : n004.star.cs.uiowa.edu
% 0.03/0.23 % Model : x86_64 x86_64
% 0.03/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.03/0.23 % Memory : 16091.75MB
% 0.03/0.23 % OS : Linux 3.10.0-327.10.1.el7.x86_64
% 0.03/0.23 % CPULimit : 300
% 0.03/0.23 % DateTime : Wed Apr 6 05:12:24 CDT 2016
% 0.03/0.23 % CPUTime :
% 6.26/6.07 > val it = (): unit
% 6.56/6.36 Trying to find a model that refutes: EX W0.
% 6.56/6.36 bnd_aElementOf0 W0 bnd_xT &
% 6.56/6.36 (EX W1.
% 6.56/6.36 ((bnd_aSet0 W1 &
% 6.56/6.36 (ALL W2. bnd_aElementOf0 W2 W1 --> bnd_aElementOf0 W2 bnd_xS) |
% 6.56/6.36 bnd_aSubsetOf0 W1 bnd_xS) &
% 6.56/6.36 bnd_isCountable0 W1) &
% 6.56/6.36 (ALL W2.
% 6.56/6.36 (((bnd_aSet0 W2 &
% 6.56/6.36 (ALL W3. bnd_aElementOf0 W3 W2 --> bnd_aElementOf0 W3 W1)) &
% 6.56/6.36 bnd_aSubsetOf0 W2 W1) &
% 6.56/6.36 bnd_sbrdtbr0 W2 = bnd_xK) &
% 6.56/6.36 bnd_aElementOf0 W2 (bnd_slbdtsldtrb0 W1 bnd_xK) -->
% 6.56/6.36 bnd_sdtlpdtrp0 bnd_xc W2 = W0))
% 9.36/9.12 Unfolded term: [| ALL W0.
% 9.36/9.12 bnd_aFunction0 W0 -->
% 9.36/9.12 (ALL W1.
% 9.36/9.12 bnd_aSubsetOf0 W1 (bnd_szDzozmdt0 W0) -->
% 9.36/9.12 (ALL W2.
% 9.36/9.12 (W2 = bnd_sdtexdt0 W0 W1) =
% 9.36/9.12 ((bnd_aFunction0 W2 & bnd_szDzozmdt0 W2 = W1) &
% 9.36/9.12 (ALL W3.
% 9.36/9.12 bnd_aElementOf0 W3 W1 -->
% 9.36/9.12 bnd_sdtlpdtrp0 W2 W3 = bnd_sdtlpdtrp0 W0 W3))));
% 9.36/9.12 ALL W0.
% 9.36/9.12 bnd_aFunction0 W0 -->
% 9.36/9.12 (ALL W1.
% 9.36/9.12 bnd_aSubsetOf0 W1 (bnd_szDzozmdt0 W0) -->
% 9.36/9.12 (ALL W2.
% 9.36/9.12 (W2 = bnd_sdtlcdtrc0 W0 W1) =
% 9.36/9.12 (bnd_aSet0 W2 &
% 9.36/9.12 (ALL W3.
% 9.36/9.12 bnd_aElementOf0 W3 W2 =
% 9.36/9.12 (EX W4.
% 9.36/9.12 bnd_aElementOf0 W4 W1 &
% 9.36/9.12 bnd_sdtlpdtrp0 W0 W4 = W3)))));
% 9.36/9.12 ALL W0 W1.
% 9.36/9.12 bnd_aFunction0 W0 & bnd_aElement0 W1 -->
% 9.36/9.12 (ALL W2.
% 9.36/9.12 (W2 = bnd_sdtlbdtrb0 W0 W1) =
% 9.36/9.12 (bnd_aSet0 W2 &
% 9.36/9.12 (ALL W3.
% 9.36/9.12 bnd_aElementOf0 W3 W2 =
% 9.36/9.12 (bnd_aElementOf0 W3 (bnd_szDzozmdt0 W0) &
% 9.36/9.12 bnd_sdtlpdtrp0 W0 W3 = W1))));
% 9.36/9.12 ALL W0 W1.
% 9.36/9.12 bnd_aSet0 W0 & bnd_aElementOf0 W1 bnd_szNzAzT0 -->
% 9.36/9.12 (ALL W2.
% 9.36/9.12 (W2 = bnd_slbdtsldtrb0 W0 W1) =
% 9.36/9.12 (bnd_aSet0 W2 &
% 9.36/9.12 (ALL W3.
% 9.36/9.12 bnd_aElementOf0 W3 W2 =
% 9.36/9.12 (bnd_aSubsetOf0 W3 W0 & bnd_sbrdtbr0 W3 = W1))));
% 9.36/9.12 ALL W0.
% 9.36/9.12 bnd_aElementOf0 W0 bnd_szNzAzT0 -->
% 9.36/9.12 (ALL W1.
% 9.36/9.12 (W1 = bnd_slbdtrb0 W0) =
% 9.36/9.12 (bnd_aSet0 W1 &
% 9.36/9.12 (ALL W2.
% 9.36/9.12 bnd_aElementOf0 W2 W1 =
% 9.36/9.12 (bnd_aElementOf0 W2 bnd_szNzAzT0 &
% 9.36/9.12 bnd_sdtlseqdt0 (bnd_szszuzczcdt0 W2) W0))));
% 9.36/9.12 ALL W0.
% 9.36/9.12 (bnd_aSubsetOf0 W0 bnd_szNzAzT0 & bnd_isFinite0 W0) &
% 9.36/9.12 ~ W0 = bnd_slcrc0 -->
% 9.36/9.12 (ALL W1.
% 9.36/9.12 (W1 = bnd_szmzazxdt0 W0) =
% 9.36/9.12 (bnd_aElementOf0 W1 W0 &
% 9.36/9.12 (ALL W2. bnd_aElementOf0 W2 W0 --> bnd_sdtlseqdt0 W2 W1)));
% 9.36/9.12 ALL W0.
% 9.36/9.12 bnd_aSubsetOf0 W0 bnd_szNzAzT0 & ~ W0 = bnd_slcrc0 -->
% 9.36/9.12 (ALL W1.
% 9.36/9.12 (W1 = bnd_szmzizndt0 W0) =
% 9.36/9.12 (bnd_aElementOf0 W1 W0 &
% 9.36/9.12 (ALL W2. bnd_aElementOf0 W2 W0 --> bnd_sdtlseqdt0 W1 W2)));
% 9.36/9.12 ALL W0 W1.
% 9.36/9.12 bnd_aSet0 W0 & bnd_aElement0 W1 -->
% 9.36/9.12 (ALL W2.
% 9.36/9.12 (W2 = bnd_sdtmndt0 W0 W1) =
% 9.36/9.12 (bnd_aSet0 W2 &
% 9.36/9.12 (ALL W3.
% 9.36/9.12 bnd_aElementOf0 W3 W2 =
% 9.36/9.12 ((bnd_aElement0 W3 & bnd_aElementOf0 W3 W0) & ~ W3 = W1))));
% 9.36/9.12 ALL W0 W1.
% 9.36/9.12 bnd_aSet0 W0 & bnd_aElement0 W1 -->
% 9.36/9.12 (ALL W2.
% 9.36/9.12 (W2 = bnd_sdtpldt0 W0 W1) =
% 9.36/9.12 (bnd_aSet0 W2 &
% 9.36/9.12 (ALL W3.
% 9.36/9.12 bnd_aElementOf0 W3 W2 =
% 9.36/9.12 (bnd_aElement0 W3 & (bnd_aElementOf0 W3 W0 | W3 = W1)))));
% 9.36/9.12 ALL W0.
% 9.36/9.12 bnd_aSet0 W0 -->
% 9.36/9.12 (ALL W1.
% 9.36/9.12 bnd_aSubsetOf0 W1 W0 =
% 9.36/9.12 (bnd_aSet0 W1 &
% 9.36/9.12 (ALL W2. bnd_aElementOf0 W2 W1 --> bnd_aElementOf0 W2 W0)));
% 9.36/9.12 ALL W0.
% 9.36/9.12 (W0 = bnd_slcrc0) = (bnd_aSet0 W0 & ~ (EX W1. bnd_aElementOf0 W1 W0));
% 9.36/9.12 ~ bnd_xK = bnd_sz00;
% 9.36/9.12 ALL W0.
% 9.36/9.12 bnd_aElementOf0 W0 bnd_szNzAzT0 -->
% 9.36/9.12 (ALL W1.
% 9.36/9.12 (bnd_aSet0 W1 &
% 9.36/9.12 (ALL W2.
% 9.36/9.12 bnd_aElementOf0 W2 W1 --> bnd_aElementOf0 W2 bnd_szNzAzT0) |
% 9.36/9.12 bnd_aSubsetOf0 W1 bnd_szNzAzT0) &
% 9.36/9.12 bnd_isCountable0 W1 -->
% 9.36/9.12 (ALL W2.
% 9.36/9.12 (bnd_aFunction0 W2 &
% 9.36/9.12 ((ALL W3.
% 9.36/9.12 (bnd_aElementOf0 W3 (bnd_szDzozmdt0 W2) -->
% 9.36/9.12 (bnd_aSet0 W3 &
% 9.36/9.12 (ALL W4.
% 9.36/9.12 bnd_aElementOf0 W4 W3 --> bnd_aElementOf0 W4 W1) |
% 9.36/9.12 bnd_aSubsetOf0 W3 W1) &
% 9.36/9.12 bnd_sbrdtbr0 W3 = W0) &
% 9.36/9.12 (((bnd_aSet0 W3 &
% 9.36/9.12 (ALL W4.
% 9.36/9.12 bnd_aElementOf0 W4 W3 -->
% 9.36/9.12 bnd_aElementOf0 W4 W1)) &
% 9.36/9.12 bnd_aSubsetOf0 W3 W1) &
% 9.36/9.12 bnd_sbrdtbr0 W3 = W0 -->
% 9.36/9.12 bnd_aElementOf0 W3 (bnd_szDzozmdt0 W2))) |
% 9.36/9.12 bnd_szDzozmdt0 W2 = bnd_slbdtsldtrb0 W1 W0)) &
% 9.36/9.12 (bnd_aSet0 (bnd_sdtlcdtrc0 W2 (bnd_szDzozmdt0 W2)) &
% 9.36/9.12 (ALL W3.
% 9.36/9.12 bnd_aElementOf0 W3
% 9.36/9.12 (bnd_sdtlcdtrc0 W2 (bnd_szDzozmdt0 W2)) =
% 9.36/9.12 (EX W4.
% 9.36/9.12 bnd_aElementOf0 W4 (bnd_szDzozmdt0 W2) &
% 9.36/9.12 bnd_sdtlpdtrp0 W2 W4 = W3)) -->
% 9.36/9.12 (ALL W3.
% 9.36/9.12 bnd_aElementOf0 W3
% 9.36/9.12 (bnd_sdtlcdtrc0 W2 (bnd_szDzozmdt0 W2)) -->
% 9.36/9.12 bnd_aElementOf0 W3 bnd_xT) |
% 9.36/9.12 bnd_aSubsetOf0 (bnd_sdtlcdtrc0 W2 (bnd_szDzozmdt0 W2))
% 9.36/9.12 bnd_xT) -->
% 9.36/9.12 bnd_iLess0 W0 bnd_xK -->
% 9.36/9.12 (EX W3.
% 9.36/9.12 bnd_aElementOf0 W3 bnd_xT &
% 9.36/9.12 (EX W4.
% 9.36/9.12 (((bnd_aSet0 W4 &
% 9.36/9.12 (ALL W5.
% 9.36/9.12 bnd_aElementOf0 W5 W4 -->
% 9.36/9.12 bnd_aElementOf0 W5 W1)) &
% 9.36/9.12 bnd_aSubsetOf0 W4 W1) &
% 9.36/9.12 bnd_isCountable0 W4) &
% 9.36/9.12 (ALL W5.
% 9.36/9.12 (bnd_aSet0 W5 &
% 9.36/9.12 (ALL W6.
% 9.36/9.12 bnd_aElementOf0 W6 W5 -->
% 9.36/9.12 bnd_aElementOf0 W6 W4) |
% 9.36/9.12 bnd_aSubsetOf0 W5 W4) &
% 9.36/9.12 bnd_sbrdtbr0 W5 = W0 |
% 9.36/9.12 bnd_aElementOf0 W5 (bnd_slbdtsldtrb0 W4 W0) -->
% 9.36/9.12 bnd_sdtlpdtrp0 W2 W5 = W3)))));
% 9.36/9.12 (((((bnd_aFunction0 bnd_xc &
% 9.36/9.12 (ALL W0.
% 9.36/9.12 (bnd_aElementOf0 W0 (bnd_szDzozmdt0 bnd_xc) -->
% 9.36/9.12 ((bnd_aSet0 W0 &
% 9.36/9.12 (ALL W1.
% 9.36/9.12 bnd_aElementOf0 W1 W0 --> bnd_aElementOf0 W1 bnd_xS)) &
% 9.36/9.12 bnd_aSubsetOf0 W0 bnd_xS) &
% 9.36/9.12 bnd_sbrdtbr0 W0 = bnd_xK) &
% 9.36/9.12 ((bnd_aSet0 W0 &
% 9.36/9.12 (ALL W1.
% 9.36/9.12 bnd_aElementOf0 W1 W0 --> bnd_aElementOf0 W1 bnd_xS) |
% 9.36/9.12 bnd_aSubsetOf0 W0 bnd_xS) &
% 9.36/9.12 bnd_sbrdtbr0 W0 = bnd_xK -->
% 9.36/9.12 bnd_aElementOf0 W0 (bnd_szDzozmdt0 bnd_xc)))) &
% 9.36/9.12 bnd_szDzozmdt0 bnd_xc = bnd_slbdtsldtrb0 bnd_xS bnd_xK) &
% 9.36/9.12 bnd_aSet0 (bnd_sdtlcdtrc0 bnd_xc (bnd_szDzozmdt0 bnd_xc))) &
% 9.36/9.12 (ALL W0.
% 9.36/9.12 bnd_aElementOf0 W0
% 9.36/9.12 (bnd_sdtlcdtrc0 bnd_xc (bnd_szDzozmdt0 bnd_xc)) =
% 9.36/9.12 (EX W1.
% 9.36/9.12 bnd_aElementOf0 W1 (bnd_szDzozmdt0 bnd_xc) &
% 9.36/9.12 bnd_sdtlpdtrp0 bnd_xc W1 = W0))) &
% 9.36/9.12 (ALL W0.
% 9.36/9.12 bnd_aElementOf0 W0
% 9.36/9.12 (bnd_sdtlcdtrc0 bnd_xc (bnd_szDzozmdt0 bnd_xc)) -->
% 9.36/9.12 bnd_aElementOf0 W0 bnd_xT)) &
% 9.36/9.12 bnd_aSubsetOf0 (bnd_sdtlcdtrc0 bnd_xc (bnd_szDzozmdt0 bnd_xc)) bnd_xT;
% 9.36/9.12 ((bnd_aSet0 bnd_xS &
% 9.36/9.12 (ALL W0.
% 9.36/9.12 bnd_aElementOf0 W0 bnd_xS --> bnd_aElementOf0 W0 bnd_szNzAzT0)) &
% 9.36/9.12 bnd_aSubsetOf0 bnd_xS bnd_szNzAzT0) &
% 9.36/9.12 bnd_isCountable0 bnd_xS;
% 9.36/9.12 bnd_aElementOf0 bnd_xK bnd_szNzAzT0;
% 9.36/9.12 bnd_aSet0 bnd_xT & bnd_isFinite0 bnd_xT;
% 9.36/9.12 ALL W0.
% 9.36/9.12 bnd_aFunction0 W0 -->
% 9.36/9.12 bnd_isCountable0 (bnd_szDzozmdt0 W0) &
% 9.36/9.12 bnd_isFinite0 (bnd_sdtlcdtrc0 W0 (bnd_szDzozmdt0 W0)) -->
% 9.36/9.12 bnd_aElement0 (bnd_szDzizrdt0 W0) &
% 9.36/9.12 bnd_isCountable0 (bnd_sdtlbdtrb0 W0 (bnd_szDzizrdt0 W0));
% 9.36/9.12 ALL W0.
% 9.36/9.12 bnd_aFunction0 W0 -->
% 9.36/9.12 (ALL W1.
% 9.36/9.12 bnd_aSubsetOf0 W1 (bnd_szDzozmdt0 W0) & bnd_isCountable0 W1 -->
% 9.36/9.12 (ALL W2 W3.
% 9.36/9.12 (bnd_aElementOf0 W2 (bnd_szDzozmdt0 W0) &
% 9.36/9.12 bnd_aElementOf0 W3 (bnd_szDzozmdt0 W0)) &
% 9.36/9.12 ~ W2 = W3 -->
% 9.36/9.12 ~ bnd_sdtlpdtrp0 W0 W2 = bnd_sdtlpdtrp0 W0 W3) -->
% 9.36/9.12 bnd_isCountable0 (bnd_sdtlcdtrc0 W0 W1));
% 9.36/9.12 ALL W0.
% 9.36/9.12 bnd_aFunction0 W0 -->
% 9.36/9.12 (ALL W1.
% 9.36/9.12 bnd_aElementOf0 W1 (bnd_szDzozmdt0 W0) -->
% 9.36/9.12 bnd_aElementOf0 (bnd_sdtlpdtrp0 W0 W1)
% 9.36/9.12 (bnd_sdtlcdtrc0 W0 (bnd_szDzozmdt0 W0)));
% 9.36/9.12 ALL W0 W1.
% 9.36/9.12 bnd_aFunction0 W0 & bnd_aElement0 W1 -->
% 9.36/9.12 bnd_aSubsetOf0 (bnd_sdtlbdtrb0 W0 W1) (bnd_szDzozmdt0 W0);
% 9.36/9.12 ALL W0.
% 9.36/9.12 bnd_aFunction0 W0 -->
% 9.36/9.12 (ALL W1.
% 9.36/9.12 bnd_aElementOf0 W1 (bnd_szDzozmdt0 W0) -->
% 9.36/9.12 bnd_aElement0 (bnd_sdtlpdtrp0 W0 W1));
% 9.36/9.12 ALL W0. bnd_aFunction0 W0 --> bnd_aSet0 (bnd_szDzozmdt0 W0);
% 9.36/9.12 ALL W0. bnd_aFunction0 W0 --> True;
% 9.36/9.12 ALL W0 W1.
% 9.36/9.12 bnd_aSet0 W0 & bnd_aElementOf0 W1 bnd_szNzAzT0 -->
% 9.36/9.12 (ALL W2.
% 9.36/9.12 bnd_aSubsetOf0 W2 (bnd_slbdtsldtrb0 W0 W1) & bnd_isFinite0 W2 -->
% 9.36/9.12 (EX W3.
% 9.36/9.12 (bnd_aSubsetOf0 W3 W0 & bnd_isFinite0 W3) &
% 9.36/9.12 bnd_aSubsetOf0 W2 (bnd_slbdtsldtrb0 W3 W1)));
% 9.36/9.12 ALL W0.
% 9.36/9.12 bnd_aElementOf0 W0 bnd_szNzAzT0 -->
% 9.36/9.12 (ALL W1 W2.
% 9.36/9.12 (bnd_aSet0 W1 & bnd_aSet0 W2) & ~ W0 = bnd_sz00 -->
% 9.36/9.12 bnd_aSubsetOf0 (bnd_slbdtsldtrb0 W1 W0) (bnd_slbdtsldtrb0 W2 W0) &
% 9.36/9.12 ~ bnd_slbdtsldtrb0 W1 W0 = bnd_slcrc0 -->
% 9.36/9.12 bnd_aSubsetOf0 W1 W2);
% 9.36/9.12 ALL W0.
% 9.36/9.12 bnd_aSet0 W0 & bnd_isCountable0 W0 -->
% 9.36/9.12 (ALL W1.
% 9.36/9.12 bnd_aElementOf0 W1 bnd_szNzAzT0 & ~ W1 = bnd_sz00 -->
% 9.36/9.12 bnd_isCountable0 (bnd_slbdtsldtrb0 W0 W1));
% 9.36/9.12 ALL W0.
% 9.36/9.12 bnd_aSet0 W0 & ~ bnd_isFinite0 W0 -->
% 9.36/9.12 (ALL W1.
% 9.36/9.12 bnd_aElementOf0 W1 bnd_szNzAzT0 -->
% 9.36/9.12 ~ bnd_slbdtsldtrb0 W0 W1 = bnd_slcrc0);
% 9.36/9.12 ALL W0.
% 9.36/9.12 bnd_aSet0 W0 & bnd_isFinite0 W0 -->
% 9.36/9.12 (ALL W1.
% 9.36/9.12 bnd_aElementOf0 W1 bnd_szNzAzT0 -->
% 9.36/9.12 bnd_isFinite0 (bnd_slbdtsldtrb0 W0 W1));
% 9.36/9.12 ALL W0.
% 9.36/9.12 bnd_aElementOf0 W0 bnd_szNzAzT0 -->
% 9.36/9.12 bnd_sbrdtbr0 (bnd_slbdtrb0 W0) = W0;
% 9.36/9.12 ALL W0.
% 9.36/9.12 bnd_aSubsetOf0 W0 bnd_szNzAzT0 & bnd_isFinite0 W0 -->
% 9.36/9.12 (EX W1.
% 9.36/9.12 bnd_aElementOf0 W1 bnd_szNzAzT0 &
% 9.36/9.12 bnd_aSubsetOf0 W0 (bnd_slbdtrb0 W1));
% 9.36/9.12 ALL W0 W1.
% 9.36/9.12 bnd_aElementOf0 W0 bnd_szNzAzT0 & bnd_aElementOf0 W1 bnd_szNzAzT0 -->
% 9.36/9.12 bnd_sdtlseqdt0 W0 W1 =
% 9.36/9.12 bnd_aSubsetOf0 (bnd_slbdtrb0 W0) (bnd_slbdtrb0 W1);
% 9.36/9.12 ALL W0 W1.
% 9.36/9.12 bnd_aElementOf0 W0 bnd_szNzAzT0 & bnd_aElementOf0 W1 bnd_szNzAzT0 -->
% 9.36/9.12 bnd_aElementOf0 W0 (bnd_slbdtrb0 (bnd_szszuzczcdt0 W1)) =
% 9.36/9.12 (bnd_aElementOf0 W0 (bnd_slbdtrb0 W1) | W0 = W1);
% 9.36/9.12 bnd_slbdtrb0 bnd_sz00 = bnd_slcrc0;
% 9.36/9.12 ALL W0.
% 9.36/9.12 bnd_aElementOf0 W0 bnd_szNzAzT0 --> bnd_isFinite0 (bnd_slbdtrb0 W0);
% 9.36/9.12 ALL W0 W1.
% 9.36/9.12 ((bnd_aSubsetOf0 W0 bnd_szNzAzT0 & bnd_aSubsetOf0 W1 bnd_szNzAzT0) &
% 9.36/9.12 ~ W0 = bnd_slcrc0) &
% 9.36/9.12 ~ W1 = bnd_slcrc0 -->
% 9.36/9.12 bnd_aElementOf0 (bnd_szmzizndt0 W0) W1 &
% 9.36/9.13 bnd_aElementOf0 (bnd_szmzizndt0 W1) W0 -->
% 9.36/9.13 bnd_szmzizndt0 W0 = bnd_szmzizndt0 W1;
% 9.36/9.13 ALL W0 W1.
% 9.36/9.13 bnd_aSet0 W0 & bnd_aElementOf0 W1 bnd_szNzAzT0 -->
% 9.36/9.13 bnd_isFinite0 W0 & bnd_sdtlseqdt0 W1 (bnd_sbrdtbr0 W0) -->
% 9.36/9.13 (EX W2. bnd_aSubsetOf0 W2 W0 & bnd_sbrdtbr0 W2 = W1);
% 9.36/9.13 ALL W0.
% 9.36/9.13 bnd_aSet0 W0 -->
% 9.36/9.13 (ALL W1.
% 9.36/9.13 bnd_isFinite0 W0 & bnd_aSubsetOf0 W1 W0 -->
% 9.36/9.13 bnd_sdtlseqdt0 (bnd_sbrdtbr0 W1) (bnd_sbrdtbr0 W0));
% 9.36/9.13 ALL W0.
% 9.36/9.13 bnd_aSet0 W0 -->
% 9.36/9.13 (ALL W1.
% 9.36/9.13 bnd_isFinite0 W0 & bnd_aElementOf0 W1 W0 -->
% 9.36/9.13 bnd_szszuzczcdt0 (bnd_sbrdtbr0 (bnd_sdtmndt0 W0 W1)) =
% 9.36/9.13 bnd_sbrdtbr0 W0);
% 9.36/9.13 ALL W0.
% 9.36/9.13 bnd_aSet0 W0 & bnd_isFinite0 W0 -->
% 9.36/9.13 (ALL W1.
% 9.36/9.13 bnd_aElement0 W1 -->
% 9.36/9.13 ~ bnd_aElementOf0 W1 W0 -->
% 9.36/9.13 bnd_sbrdtbr0 (bnd_sdtpldt0 W0 W1) =
% 9.36/9.13 bnd_szszuzczcdt0 (bnd_sbrdtbr0 W0));
% 9.36/9.13 ALL W0.
% 9.36/9.13 bnd_aSet0 W0 --> (bnd_sbrdtbr0 W0 = bnd_sz00) = (W0 = bnd_slcrc0);
% 9.36/9.13 ALL W0.
% 9.36/9.13 bnd_aSet0 W0 -->
% 9.36/9.13 bnd_aElementOf0 (bnd_sbrdtbr0 W0) bnd_szNzAzT0 = bnd_isFinite0 W0;
% 9.36/9.13 ALL W0. bnd_aSet0 W0 --> bnd_aElement0 (bnd_sbrdtbr0 W0);
% 9.36/9.13 ALL W0.
% 9.36/9.13 bnd_aElementOf0 W0 bnd_szNzAzT0 -->
% 9.36/9.13 bnd_iLess0 W0 (bnd_szszuzczcdt0 W0);
% 9.36/9.13 ALL W0 W1.
% 9.36/9.13 bnd_aElementOf0 W0 bnd_szNzAzT0 & bnd_aElementOf0 W1 bnd_szNzAzT0 -->
% 9.36/9.13 bnd_iLess0 W0 W1 --> True;
% 9.36/9.13 ALL W0 W1.
% 9.36/9.13 bnd_aElementOf0 W0 bnd_szNzAzT0 & bnd_aElementOf0 W1 bnd_szNzAzT0 -->
% 9.36/9.13 bnd_sdtlseqdt0 W0 W1 | bnd_sdtlseqdt0 (bnd_szszuzczcdt0 W1) W0;
% 9.36/9.13 ALL W0 W1 W2.
% 9.36/9.13 (bnd_aElementOf0 W0 bnd_szNzAzT0 & bnd_aElementOf0 W1 bnd_szNzAzT0) &
% 9.36/9.13 bnd_aElementOf0 W2 bnd_szNzAzT0 -->
% 9.36/9.13 bnd_sdtlseqdt0 W0 W1 & bnd_sdtlseqdt0 W1 W2 --> bnd_sdtlseqdt0 W0 W2;
% 9.36/9.13 ALL W0 W1.
% 9.36/9.13 bnd_aElementOf0 W0 bnd_szNzAzT0 & bnd_aElementOf0 W1 bnd_szNzAzT0 -->
% 9.36/9.13 bnd_sdtlseqdt0 W0 W1 & bnd_sdtlseqdt0 W1 W0 --> W0 = W1;
% 9.36/9.13 ALL W0. bnd_aElementOf0 W0 bnd_szNzAzT0 --> bnd_sdtlseqdt0 W0 W0;
% 9.36/9.13 ALL W0.
% 9.36/9.13 bnd_aElementOf0 W0 bnd_szNzAzT0 -->
% 9.36/9.13 bnd_sdtlseqdt0 W0 (bnd_szszuzczcdt0 W0);
% 9.36/9.13 ALL W0 W1.
% 9.36/9.13 bnd_aElementOf0 W0 bnd_szNzAzT0 & bnd_aElementOf0 W1 bnd_szNzAzT0 -->
% 9.36/9.13 bnd_sdtlseqdt0 W0 W1 =
% 9.36/9.13 bnd_sdtlseqdt0 (bnd_szszuzczcdt0 W0) (bnd_szszuzczcdt0 W1);
% 9.36/9.13 ALL W0.
% 9.36/9.13 bnd_aElementOf0 W0 bnd_szNzAzT0 -->
% 9.36/9.13 ~ bnd_sdtlseqdt0 (bnd_szszuzczcdt0 W0) bnd_sz00;
% 9.36/9.13 ALL W0. bnd_aElementOf0 W0 bnd_szNzAzT0 --> bnd_sdtlseqdt0 bnd_sz00 W0;
% 9.36/9.13 ALL W0 W1.
% 9.36/9.13 bnd_aElementOf0 W0 bnd_szNzAzT0 & bnd_aElementOf0 W1 bnd_szNzAzT0 -->
% 9.36/9.13 bnd_sdtlseqdt0 W0 W1 --> True;
% 9.36/9.13 ALL W0. bnd_aElementOf0 W0 bnd_szNzAzT0 --> ~ W0 = bnd_szszuzczcdt0 W0;
% 9.36/9.13 ALL W0.
% 9.36/9.13 bnd_aElementOf0 W0 bnd_szNzAzT0 -->
% 9.36/9.13 W0 = bnd_sz00 |
% 9.36/9.13 (EX W1. bnd_aElementOf0 W1 bnd_szNzAzT0 & W0 = bnd_szszuzczcdt0 W1);
% 9.36/9.13 ALL W0 W1.
% 9.36/9.13 bnd_aElementOf0 W0 bnd_szNzAzT0 & bnd_aElementOf0 W1 bnd_szNzAzT0 -->
% 9.36/9.13 bnd_szszuzczcdt0 W0 = bnd_szszuzczcdt0 W1 --> W0 = W1;
% 9.36/9.13 ALL W0.
% 9.36/9.13 bnd_aElementOf0 W0 bnd_szNzAzT0 -->
% 9.36/9.13 bnd_aElementOf0 (bnd_szszuzczcdt0 W0) bnd_szNzAzT0 &
% 9.36/9.13 ~ bnd_szszuzczcdt0 W0 = bnd_sz00;
% 9.36/9.13 bnd_aElementOf0 bnd_sz00 bnd_szNzAzT0;
% 9.36/9.13 bnd_aSet0 bnd_szNzAzT0 & bnd_isCountable0 bnd_szNzAzT0;
% 9.36/9.13 ALL W0.
% 9.36/9.13 bnd_aElement0 W0 -->
% 9.36/9.13 (ALL W1.
% 9.36/9.13 bnd_aSet0 W1 & bnd_isFinite0 W1 -->
% 9.36/9.13 bnd_isFinite0 (bnd_sdtmndt0 W1 W0));
% 9.36/9.13 ALL W0.
% 9.36/9.13 bnd_aElement0 W0 -->
% 9.36/9.13 (ALL W1.
% 9.36/9.13 bnd_aSet0 W1 & bnd_isFinite0 W1 -->
% 9.36/9.13 bnd_isFinite0 (bnd_sdtpldt0 W1 W0));
% 9.36/9.13 ALL W0.
% 9.36/9.13 bnd_aElement0 W0 -->
% 9.36/9.13 (ALL W1.
% 9.36/9.13 bnd_aSet0 W1 & bnd_isCountable0 W1 -->
% 9.36/9.13 bnd_isCountable0 (bnd_sdtmndt0 W1 W0));
% 9.36/9.13 ALL W0.
% 9.36/9.13 bnd_aElement0 W0 -->
% 9.36/9.13 (ALL W1.
% 9.36/9.13 bnd_aSet0 W1 & bnd_isCountable0 W1 -->
% 9.36/9.13 bnd_isCountable0 (bnd_sdtpldt0 W1 W0));
% 9.36/9.13 ALL W0 W1.
% 9.36/9.13 bnd_aElement0 W0 & bnd_aSet0 W1 -->
% 9.36/9.13 ~ bnd_aElementOf0 W0 W1 --> bnd_sdtmndt0 (bnd_sdtpldt0 W1 W0) W0 = W1;
% 9.36/9.13 ALL W0.
% 9.36/9.13 bnd_aSet0 W0 -->
% 9.36/9.13 (ALL W1.
% 9.36/9.13 bnd_aElementOf0 W1 W0 -->
% 9.36/9.13 bnd_sdtpldt0 (bnd_sdtmndt0 W0 W1) W1 = W0);
% 9.36/9.13 ALL W0 W1 W2.
% 9.36/9.13 (bnd_aSet0 W0 & bnd_aSet0 W1) & bnd_aSet0 W2 -->
% 9.36/9.13 bnd_aSubsetOf0 W0 W1 & bnd_aSubsetOf0 W1 W2 --> bnd_aSubsetOf0 W0 W2;
% 9.36/9.13 ALL W0 W1.
% 9.36/9.13 bnd_aSet0 W0 & bnd_aSet0 W1 -->
% 9.36/9.13 bnd_aSubsetOf0 W0 W1 & bnd_aSubsetOf0 W1 W0 --> W0 = W1;
% 9.36/9.13 ALL W0. bnd_aSet0 W0 --> bnd_aSubsetOf0 W0 W0;
% 9.36/9.13 ALL W0.
% 9.36/9.13 bnd_aSet0 W0 & bnd_isFinite0 W0 -->
% 9.36/9.13 (ALL W1. bnd_aSubsetOf0 W1 W0 --> bnd_isFinite0 W1);
% 9.36/9.13 ALL W0. bnd_aSet0 W0 & bnd_isCountable0 W0 --> ~ W0 = bnd_slcrc0;
% 9.36/9.13 ALL W0. bnd_aSet0 W0 & bnd_isCountable0 W0 --> ~ bnd_isFinite0 W0;
% 9.36/9.13 ALL W0. bnd_aSet0 W0 --> bnd_isCountable0 W0 --> True;
% 9.36/9.13 bnd_isFinite0 bnd_slcrc0;
% 9.36/9.13 ALL W0. bnd_aSet0 W0 --> bnd_isFinite0 W0 --> True;
% 9.36/9.13 ALL W0.
% 9.36/9.13 bnd_aSet0 W0 --> (ALL W1. bnd_aElementOf0 W1 W0 --> bnd_aElement0 W1);
% 9.36/9.13 ALL W0. bnd_aElement0 W0 --> True; ALL W0. bnd_aSet0 W0 --> True |]
% 9.36/9.13 ==> EX W0.
% 9.36/9.13 bnd_aElementOf0 W0 bnd_xT &
% 9.36/9.13 (EX W1.
% 9.36/9.13 ((bnd_aSet0 W1 &
% 9.36/9.13 (ALL W2. bnd_aElementOf0 W2 W1 --> bnd_aElementOf0 W2 bnd_xS) |
% 9.36/9.13 bnd_aSubsetOf0 W1 bnd_xS) &
% 9.36/9.13 bnd_isCountable0 W1) &
% 9.36/9.13 (ALL W2.
% 9.36/9.13 (((bnd_aSet0 W2 &
% 9.36/9.13 (ALL W3.
% 9.36/9.13 bnd_aElementOf0 W3 W2 --> bnd_aElementOf0 W3 W1)) &
% 9.36/9.13 bnd_aSubsetOf0 W2 W1) &
% 9.36/9.13 bnd_sbrdtbr0 W2 = bnd_xK) &
% 9.36/9.13 bnd_aElementOf0 W2 (bnd_slbdtsldtrb0 W1 bnd_xK) -->
% 9.36/9.13 bnd_sdtlpdtrp0 bnd_xc W2 = W0))
% 9.36/9.13 Adding axioms...
% 9.36/9.13 Typedef.type_definition_def
% 22.88/22.60 ...done.
% 22.88/22.62 Ground types: ?'b, TPTP_Interpret.ind
% 22.88/22.62 Translating term (sizes: 1, 1) ...
% 31.40/31.18 Invoking SAT solver...
% 31.40/31.18 No model exists.
% 31.40/31.18 Translating term (sizes: 2, 1) ...
% 40.72/40.47 Invoking SAT solver...
% 40.72/40.47 No model exists.
% 40.72/40.47 Translating term (sizes: 1, 2) ...
% 95.07/94.65 Invoking SAT solver...
% 95.07/94.68 No model exists.
% 95.07/94.68 Translating term (sizes: 3, 1) ...
% 106.80/106.33 Invoking SAT solver...
% 106.80/106.33 No model exists.
% 106.80/106.33 Translating term (sizes: 2, 2) ...
% 168.85/168.19 Invoking SAT solver...
% 168.97/168.23 No model exists.
% 168.97/168.23 Translating term (sizes: 1, 3) ...
% 300.08/298.32 /export/starexec/sandbox/solver/lib/scripts/run-polyml-5.5.2: line 82: 7143 CPU time limit exceeded (core dumped) "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS
% 300.08/298.32 7144 (core dumped) | { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
% 300.08/298.33 /export/starexec/sandbox/solver/src/HOL/TPTP/lib/Tools/tptp_refute: line 26: 7089 Exit 152 "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP
% 300.08/298.33 7090 CPU time limit exceeded (core dumped) | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
%------------------------------------------------------------------------------